Terminology

TODO

• bound
• open, close
• fresh ($\lambda$x:Unit.t2) t1, where the variable x is chosen fresh - i.e. different from all the free variables of t2

From P55 Chapter 5.1 Basics (of lambda-calculus)

Bound

An occurrence of the vairable x is said to be bound when it occurs in the body t of an abstraction $\lambda x.t$

Free

An occurrence of x is free if it appears in a position where it is not bound by an enclosing abstraction on x. For example x in x y and $\lambda y. x y$

Closed

A term with no free variables is said to be closed; closed terms are also called combinators. The simplest combinator, called the identity function $id = \lambda x.x;$