In the lambda calculus augmented with primitive functions and constants,
the δ-reduction rule is a relation between λ-terms
((...(M N_{1})...)N_{n})→_{δ}R
, where
M
is a primitive function of arity n, and for all 1≤i≤n, N_{i}
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.
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.
W. Kluge. Abstract Computing Machines. A Lambda Calculus Perspective. Springer, 2005.
Copyright © 2014 Barry Watson. All rights reserved.