9/16/2019
Definition
In an abstraction λ<variable>.<expr> the <expr> is known as the scope of the abstraction.
Egs. λx.λy.(m x) has scope λy.(m x), and λy.(m x) has scope (m x)
Definition
An occurrence of a variable v in a lambda expression is bound if it is within the scope of an λv.<expr> abstraction.
Eg. in λx.λy.(m x) the occurrence of x is bound, but the occurrence of m is not bound.
Definition
An occurrence of a variable v in a lambda expression is free if it is not within the scope of a λv.<expr> abstraction.
Eg. in λx.λy. (y (x z)) the occurrence of z is free.
Notice here that the occurrence of the variable immediately after the λ -- what might be called the binding occurrence-- is not really classified is either free or bound-- we do not have much interest in these occurrences.
The notation <expr1>/.<variable> -> <expr2> means the result of simultaneously substituting <expr2> for each free occurrence of <variable> in <expr1>.
Egs. λx.λy.(y (x z)) /. z->a is λx.λy.(y (x a)) and (λx.x x) /. x->a is (λx.x a) and λx.(x x) /. x->a is λx(x x)
When a substitution is made is is possible for a free occurrence of a variable in <expr2> to become bound or 'captured' in <expr1>/.<variable> -> <expr2> for example
λy.x /. x->y is λy.y
the occurrence of x in λy.x is free but when the substitution is made the y in λy.y is bound. Another example
λy.x /. x->λz.y is λy.λz.y
and again a free y has been captured.
Capturing is a bad thing, and we will be interested only in substitutions which avoid any capturing of free variables. Such substitutions are said to be sound (sometimes a sound substitution is described using the phrase 'free for' as in x is free for z in λy.x).
Definition
A substitution <expr1>/.<variable> -> <expr2> is sound if no free occurrence of a variable in <expr2> becomes bound in <expr1>/.<variable> -> <expr2>.