Delta (δ) rules in the lambda (λ) calculus

---

This article is part of a series of articles on the lambda calculus and is also available as a YouTube video.

1. What is the lambda (λ) calculus?
2. Bound vs. free variables in the lambda (λ) calculus
3. (This Article) Delta (δ) rules in the lambda (λ) calculus
4. Beta (β) reduction in the lambda (λ) calculus
5. Alpha (α) conversion in the lambda (λ) calculus
6. Eta (η) conversion in the lambda (λ) calculus
7. Summary of the lambda calculus (λ) evaluation rules
8. Lambda calculus (λ) reduction orders and normal form
9. The Church-Rosser theorem and the lambda (λ) calculus

---

With a simple lambda calculus expression like (+ 1 1) it is clear how it can easily be evaluated to give us a final result of 2.

But things are not so clear with larger programs that could include thousands, or even millions of expressions. We need rules to evaluate lambda calculus programs consistently, and these rules are what the next set of articles will focus on. These rules are sometimes called reduction rules because they take one expression and reduce it to another expression which is usually simpler.

The first of these rules is known as “delta (δ) rules”.

Delta rules are quite simple: they are what are used to evaluate “built-in” functions such as addition, and subtraction (among others).

Consider the following lambda expression: (+ 4 2). We instinctively know that 4 + 2 = 6. Whenever we reach a point in an expression where we can use a built in function, we can use a delta rule to reduce it. This is usually denoted with a right arrow showing the direction of the reduction with a delta symbol on top of the arrow like so:

\[(+\ 4 \ 2) \overset{\delta}{\longrightarrow} \ 6\]

Pretty simple to start of with.

The next article covers beta (β) reduction, which is more complicated!