> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/340-lambda-calculi/lambda-calculus-reductions/delta-reduction.md).

# Delta reduction

In the lambda calculus augmented with primitive functions and constants, the δ-reduction rule is a relation between λ-terms

((...(M N₁)...) Nₙ) ->ᵟ R

where:

* `M` is a primitive n-ary function and ∀i. 1<=i<=n, Nᵢ is normalised
* `R` is the result of applying the primitive function to the arg.

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.
