Parasitic Binding

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

Examples

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.

References

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