Next: About this document
Up: classnote 14
Previous: de Bruijn indices
We will briefly introduce the concept of binding.
To describe binding, we need definitions for
bound variables,
free variables, and
substitution for free variables.
Informally, the 
-term 
has a binding occurrence
of the variable 
, and the scope of is 
:
Any occurrence of in is bound.
Note that binding occurs for the smallest scope,
eg. in 
, the 
in the body of 
is bound by that binding occurrence of rather than the binding
occurrence in the outer -expression.
A free variable is one that is not bound.
The substitution of 
for a free variable 
in 
is denoted by 
.
Informally, any free occurrence of in is replaced by .
It is important, however, that no free variable of becomes bound in .