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.


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


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


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.