Substitution

The notation E[E1/v] refers to the lambda expression obtained by replacing each free occurrence of the variable v in E by the lambda expression E1. Such a substitution is called valid or safe if no free variable in E1 becomes bound as a result of the substitution E[E1/v]. An invalid substitution involves a variable capture or name clash. For example, the naive substitution (λx.(mul y x))[x/y] to get (λx.(mul x x)) is unsafe since the result represents a squaring operation whereas the original lambda expression does not. The following notations are used in the definition of substitution: The substitution of an expression for a (free) variable in a lambda expression is denoted by E[E1/v] and is defined as follows.
  1. x[E1/x] = E1   for any variable x

  2. y[E1/x] = y   for any variable y ≠ x

  3. c[E1/x] = c   for any constant c

  4.   ( λy . E ) [E1/x]
    = λy.E                                if y=x
    = λz.(E[z/y][E1/x])       if y≠x, x free in E, y free in E1, new z
    = λy.(E[E1/x])                 otherwise

  5. ( E E1 ) [E2/x] = ( E [E2/x] ) ( E1 [E2/x] )

  6. ( E ) [E1/x] = ( E [E1/x] )
An example of substitution is given as follows: 
   ( λy . ( λf . f x ) y ) [ f y/x ]
 = λz . ( ( λf . f x ) z ) [ f y/x ]              by (d)
 = λz . ( ( λf . f x ) [ f y/x ]  z[ f y/x ] )    by (e)
 = λz . ( ( λf . f x ) [ f y/x ] z )              by (b)
 = λz . ( λg . ( g x ) [ f y/x ] ) z              by (d)
 = λz . ( λg . g ( f y ) ) z        by (e), (b), and (a)