The Lumenary · Advanced undergraduate

The λ-calculus

Name: ______________________

Date: ______________________

You will learn to

Reduce λ-terms using capture-avoiding substitution, and encode booleans, pairs and natural numbers (Church numerals)
Use a fixed-point combinator to define recursive functions, and explain why untyped terms need not terminate
Prove the Church–Rosser theorem by parallel reduction and deduce that a term has at most one normal form
Prove that every simply typed λ-term has a normal form, and say what this costs in expressive power
State the equivalence of λ-definability with computability and the undecidability of β-equality

1.
List the free variables of the term $\lambda x.\, x\, y\, (\lambda y.\, y\, z)$ . Enter each variable name once.
2.
What does $(\lambda x.\, \lambda y.\, x)\, y$ reduce to in one β-step (with $y$ free)?
- A. $\lambda z.\, y$
- B. $\lambda y.\, y$
- C. $y$
- D. $\lambda y.\, x$
3.
With Church numerals $\bar n = \lambda f\, x.\, f^n\, x$ , the term $\bar 3\, \bar 2$ (the numeral $3$ applied to the numeral $2$ ) β-reduces to a Church numeral $\bar k$ . What is $k$ ?
4.
Which of these terms have no normal form? Here $\Omega = (\lambda x.\, x\, x)(\lambda x.\, x\, x)$ , $K = \lambda x\, y.\, x$ , $I = \lambda x.\, x$ . Choose all that apply.
- A. $\Omega$
- B. $\lambda z.\, \Omega$
- C. $K\, I\, \Omega$
- D. $(\lambda x.\, x\, x)(\lambda y.\, y)$
5.
Why does the proof of the Church–Rosser theorem go through parallel reduction $\Rightarrow$ instead of showing directly that one-step reduction $\to$ has the diamond property?
- A.Because $\to$ does not have the diamond property: contracting a redex can duplicate another redex, so joining may need several steps on one side.
- B.Because $\to$ is not terminating.
- C.Because $\Rightarrow$ is terminating while $\to$ is not.
- D.Because the diamond property for $\to$ is true but too hard to prove.
6.
In Turing's proof of weak normalisation we contract a redex $R = (\lambda x{:}A.\, P)\, Q$ of maximal degree $d$ chosen so that $Q$ contains no redex of degree $d$ . Which part of the argument needs this choice?
- A.Redexes inside $Q$ may be copied many times by the substitution $P[Q/x]$ ; the choice ensures all the copies have degree less than $d$ .
- B.It ensures that no new redexes are created.
- C.It ensures that the redexes inside $P$ survive.
- D.It ensures the term is typable after the step.
7.
Which of these terms has a type in the simply typed λ-calculus (for suitable types on the bound variables)?
- A. $\lambda f\, x.\, f\,(f\, x)$
- B. $\lambda x.\, x\, x$
- C. $Y = \lambda f.\, (\lambda x.\, f\,(x\, x))\,(\lambda x.\, f\,(x\, x))$
- D. $\Omega$
8.
In the lesson's Lean file, Step t u is one β-step and ReflTransGen Step t u is $t \twoheadrightarrow u$ . Which statement is the Church–Rosser theorem, as proved there?
- A.∀ {t u v}, ReflTransGen Step t u → ReflTransGen Step t v → ∃ w, ReflTransGen Step u w ∧ ReflTransGen Step v w
- B.Diamond Step
- C.∀ t, ∃ u, ReflTransGen Step t u ∧ Normal u
- D.∀ {t u v}, Step t u → Step t v → u = v
9.
Python's lambda can run Church numerals directly. With church(n) and to_int below, define times(m, n) and exp(m, n) returning the Church numerals for $m \cdot n$ and $m^n$ , using only application and lambda (no conversion to int inside them).
Computational — Practice

Answer key — The λ-calculus

1.
$\mathrm{FV}(\lambda y.\, y\, z) = \{z\}$ , so $\mathrm{FV}(x\, y\, (\lambda y.\, y\, z)) = \{x, y, z\}$ , and removing the variable bound by the outer $\lambda x$ leaves $\{y, z\}$ . The variable $y$ is free at its first occurrence and bound at its second: the same name can play both roles.
2.
Rename to $(\lambda x.\, \lambda z.\, x)\, y$ , then substitute: $(\lambda z.\, x)[y/x] = \lambda z.\, y$ . In de Bruijn notation the term is $(\lambda\, \lambda\, 1)\, y$ and the result is $\lambda\, (y \text{ shifted})$ ; no renaming is ever needed.
3.
$\bar 3\, \bar 2 \twoheadrightarrow \lambda x.\, \bar 2\,(\bar 2\,(\bar 2\, x))$ . As functions, $\bar 2\, f = f \circ f$ , so $\bar 2 \circ \bar 2 \circ \bar 2$ sends $f$ to $f^{2^3} = f^8$ , and the normal form is $\bar 8$ . In general $\bar n\, \bar m \twoheadrightarrow \overline{m^n}$ , which is why $\mathsf{EXP} = \lambda m\, n.\, n\, m$ .
4.
$\Omega$ and $\lambda z.\, \Omega$ have no normal form: every reduct still contains $\Omega$ (and by Church–Rosser no other route could reach a normal form). $K\, I\, \Omega \to (\lambda y.\, I)\, \Omega \to I$ and $(\lambda x.\, x\, x)\, I \to I\, I \to I$ do have normal forms.
5.
One-step reduction fails the diamond property because a β-step can copy a redex: $(\lambda x.\, x\, x)(I\, z) \to (I\, z)(I\, z)$ makes two copies of $I\, z$ . The other reduct $(\lambda x.\, x\, x)\, z$ reaches $z\, z$ in one step, but $(I\, z)(I\, z)$ needs two. Parallel reduction contracts any set of existing redexes at once, so $(I\, z)(I\, z) \Rightarrow z\, z$ in one parallel step, and the triangle property gives the diamond.
6.
Contracting $R$ replaces each occurrence of $x$ in $P$ by a copy of $Q$ , so redexes inside $Q$ are duplicated. If $Q$ contained a redex of degree $d$ , the number of degree- $d$ redexes could increase. Choosing the rightmost redex of maximal degree guarantees $Q$ has none, so after the step the redex $R$ is gone, copies and created redexes all have degree $< d$ , and the measure (maximal degree, number of redexes of that degree) decreases.
7.
$\lambda f\, x.\, f\,(f\, x)$ has type $(A \to A) \to A \to A$ . The other three contain the self-application $x\, x$ , which would force a type $A$ with $A = A \to B$ . Alternatively: typed terms are (strongly) normalising, while $Y\, I$ and $\Omega$ are not.
8.
Church–Rosser is confluence of $\twoheadrightarrow$ : option (a), Lumenary.LambdaCalculus.church_rosser. It is proved by diamond_confluent par_diamond and the fact that ReflTransGen Step and ReflTransGen Par coincide. Option (b) is false (duplication), (c) is false ( $\Omega$ ) and (d) is false (any term with two redexes).
9.
```
def church(n):
    return lambda f: (lambda x: x) if n == 0 else (lambda x: f(church(n - 1)(f)(x)))

def to_int(c):
    return c(lambda k: k + 1)(0)

def times(m, n):
    return lambda f: m(n(f))

def exp(m, n):
    return n(m)
```
These are $\mathsf{TIMES} = \lambda m\, n\, f.\, m\,(n\, f)$ and $\mathsf{EXP} = \lambda m\, n.\, n\, m$ . Python evaluates arguments first (call-by-value), which is harmless here because every numeral is a normalising function.