Topics

  • The Untyped λ-Calculus
  • β-reduction
  • λ-calculus Semantics and Normal Forms

The Untyped λ-Calculus

Today we will learn about one of the most central aspects of the course: Alonzo Church’s untyped λ-calculus. The λ-calculus is not at all like the integral calculus. Instead, the λ-calculus is a computationally “complete” system consisting of an extremely minimal number of syntax and semantic rules.

The syntax of the λ-calculus includes just three forms. We define untyped λ-calculus expressions in the following manner:

e ∈ Expr ::=   (read: "The set Expr, of expressions consists of...")
          | x             ← Variable references
          | (λ (x) e)     ← λ abstractions
          | (e e)         ← Application

That is the syntax of the λ-calculus. We will spend a long time studying the “semantics” of the λ calculus: the untyped λ-calculus has a fairly “nondeterministic” semantics defined in terms of rewriting rules—to turn the λ calculus into a programming language (such as Racket / Haskell / etc.), we will need to make some more decisions (we will cover this in later classes).

For now, let’s see some examples of λ-calculus terms:

  • λx. x, which I would write as (λ (x) x)
  • λx. λy. x, which I would write as (λ (x) (λ (y) x))
  • λx. x y, which I would write as (λ (x) (x y))

Notice that Racket’s syntax completely disambiguates what is going on, hence we will stick with the Scheme-style λ, compared to the more traditional λ-calculus notation.

QuickAnswer

Which of the following (possibly multiple) is in the lambda calculus?

  • (A) (λ (x) y)
  • (B) (λ (x y) x)
  • (C) (λ (x) (λ (y) (λ (z) (z x))))
  • (D) ((λ (x) e) 1)

β-reduction

β-reduction is the most fundamental operation in the λ calculus. It simply means the following:

((λ (x) e-b) e-a) β⟹ e-b [x ↦ e-a]

In other words: any expression (e-f e-a) is a candidate for β-reduction whenever e-f is of the form (λ (x) e-b). We call expressions of this form redexes for “reducible expressions.”

The “meaning” of a λ-calculus term is given by all of the possible different reductions (so far we have talked only about β) we can do to it. Some cases are easy, let’s see our first example of β reduction:

((λ (x) x) y) β⟹ x [x ↦ y] ≡ y

Notice how in this case, y is the argument. But we couldn’t write this in Racket:

((λ (x) x) y)   ← Syntax error: y is unbound variable

β-reduction, and the untyped λ-calculus in general, doesn’t care that the variable is unbound. β-reduction just says: “to apply a function (λ (x) e-b) to an argument expression e-a, substitute x by e-a in the body.”

QuickAnswer

Perform β-reduction on the term ((λ (x) (x (x y))) z)

QuickAnswer

Perform β-reduction on the term ((λ (x) (λ (y) (y x))) (λ (z) z))

QuickAnswer

Perform β-reduction on the term ((λ (x) (x x)) (λ (x) (x x)))

Substitution: Tricky, we will skip for now

One note: we are being colloquial about substitution. In fact, substitution is a bit tricky, and it requires some care. We will discuss these nuances in a future lecture, where we will cover some other reduction rules and technical details. For now, it is sufficient to say that you can intuit substitution as “plug and chug” from grade-school algebra / calculus.

Reducing deep into a term

Sometimes, the redex will not be obvious. In fact, in general, a term may have multiple redexes.

QuickAnswer

Give a term that contains two redexes, i.e., two subexpressions such that the expression could have β-reduction performed upon it.

In the untyped λ calculus, we typically construe β reduction to be any possible beta reduction deep down within the term. Ultimately we will see that this is not what we want for programming, but for now we will develop it.

QuickAnswer

The following term has two possible β-reductions:

((λ (x) y)
 ((λ (z) (z z)) (λ (a) (a a))))

Please perform both possible β reductions, what is the result?

λ-calculus Semantics and Normal Forms

We will see that, surprisingly, the λ-calculus is Turing complete. This is surprising because, essentially, β-reduction is the only computational rule in the whole system. There will be some other reduction rules (α and η), which will have their own place, but β is the main computational rule.

The λ-calculus is ruthlessly tiny, essentially the “assembly language” of functional programming, stripping down functional programming just to function calls.

The “semantics” of the untyped λ-calculus is defined by reduction rules. We have seen one already: the β rule. We can see each β-reduction as one “step” of computation in the λ-calculus. Most interesting programs will take—in general—multiple steps of β-reduction to reduce to a normal form.

Definition (Normal Form): The term “normal form” refers to a class of expressions which cannot be reduced any further according to some metric. For example, in β-normal form, there can be no unreduced β-reductions anywhere in the term.

QuickAnswer

Which of the following are in β-normal form:

  • (A) (λ (x) (λ (y) (x (λ (z) y))))
  • (B) (λ (x) ((λ (z) x) x))
  • (C) (z (λ (x) (x x)))
  • (D) (λ (x) (x ((λ (y) y) x)))

Fact: it is impossible, in general, to take an arbitrary λ-calculus expression and determine whether a β-normal form exists.

Explanation: Equivalent to the halting problem.

So far, our lecture has focused on the definition of the λ-calculus as a term rewriting system. In fact, this is precisely what the λ-calculus is: a formulation of functions as terms, where we can use β to drive computation via rewriting / substitution.

When we imagine computing with the λ-calculus, we imagine running many steps of β reduction, gradually reducing the term into a value (i.e., result). Thus, we can see normal forms as values, the results of fully-reducing an expression.

QuickAnswer

Fully-reduce the following term to β-normal form:

(((λ (x) (λ (y) (x y))) (λ (x) x)) (λ (b) a))

Show each step of each β-reduction.

As we will see, the “meaning” of a λ-calculus term is a large, non-deterministic tree of all possible ways in which it could potentially be reduced. Some of these will yield normal forms, and some of them will not.

QuickAnswer

Which of the following is true about the following term:

((λ (x) z) ((λ (x) (x x)) (λ (x) (x x))))

  • (A) The term reduces forever
  • (B) The term reduces to z
  • (C) Both (A) and (B)

Summary: Day one of the λ-calculus

  • A calculus refers to a system for manipulating and rewriting terms. The differential and integral calculus is a system for rewriting terms via symbolic differentiation/integration.

  • The untyped λ-calculus is a system of computing with terms that aims for absolute minimalism.

  • Only three forms: variables, application, and λ-abstraction.

  • The single computational rule is given by β, we will learn more reduction rules soon but β is the main (compute-relevant) one.

  • The “meaning” of a term in the λ-calculus is given by a reduction relation (in this case we have learned only of β-reduction): the idea is that the term will be reduced multiple times until it reaches some “normal form.”

  • A normal form is when you can’t reduce any further, by some metric. We learned one normal form today: β-normal form, in which there is no more β-reduction possible.

  • In the untyped λ-calculus, a given term may have a multitude of different possible redexes (reducible subexpressions). The untyped λ-calculus does not tell us which of those redexes must be applied, and so the meaning of a term in the λ-calculus may have some ambiguity: all different possible ways of reducing the term.

  • This leaves us with an obvious question: will all ways of reducing the term reach the same conclusion / normal form? It turns out the answer is Yes*, under some circumstances, which we will learn about in the next lectures. In short: the Church-Rosser theorem tells us that if a term does have a normal form, it will be unique up to variable renaming.

  • Church wasn’t trying to model hardware. He was trying to:

    • Characterize effective calculability.
    • Provide a logical foundation for mathematics.
    • β-reduction was a mathematical equality principle, not an execution model.