Delta Reduction

In the lambda calculus augmented with primitive functions and constants, the δ-reduction rule is a relation between λ-terms ((...(M N1)...)Nn)→δR, where

• M is a primitive function of arity n, and for all 1≤i≤n, Ni is normalised,
• R is the result of applying the primitive function to the arguments.

In the case where we have a δ-reduction of M→δN, M is called the δ-redex.

Examples

If we augment the λ-calculus with the natural numbers and the primitive addition operator (+), then:

• ((+ 1) 2) →_δ 3 is a δ-reduction.
• ((+ 1) ((+ 1) 1)) is a not a δ-redex.

References

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