Substitutions

Topic

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>.