In the lambda calculus augmented with primitive functions and constants,
the δ-reduction rule is a relation between λ-terms
((...(M N1)...)Nn)→δR, where
Mis a primitive function of arity n, and for all 1≤i≤n,
Ris the result of applying the primitive function to the arguments.
In the case where we have a δ-reduction of
M is called the δ-redex.
If we augment the λ-calculus with the natural numbers and the primitive addition operator (+), then:
((+ 1) 2)→δ
3is a δ-reduction.
((+ 1) ((+ 1) 1))is a not a δ-redex.
W. Kluge. Abstract Computing Machines. A Lambda Calculus Perspective. Springer, 2005.
Copyright © 2014 Barry Watson. All rights reserved.