In the lambda calculus the
β-reduction rule can substitute
free variables into positions where they become bound.
Such a binding is called *parasitic*.

The following is a case of a non-parasitic binding:

`(λx.λy.x)z`

→_{β}`λy.z`

Here `z`

is free on both sides of the β-reduction.
The following is a case of a parasitic binding:

`(λx.λy.x)y`

→_{β}`λy.y`

Here `y`

is free on the left-hand side but bound on the right-hand side of the β-reduction.

W. Kluge. *Abstract Computing Machines. A Lambda Calculus Perspective.* Springer, 2005.

Copyright © 2014 Barry Watson. All rights reserved.