Reduction and Conversion

Reduction

Applying a $\lambda$-abstraction to an argument is computed by substituting the argument for the bound variable:

This step is beta-reduction, and a subterm of the form $(\tLam{x}{A}{t})\;s$ is a beta-redex. Part II added two more kinds of step: delta-reduction, which unfolds a definition (Chapter 7), and iota-reduction, which runs a recursor on a constructor (Figures 7.1 and 9.1, and the general rule of Chapter 8). We allow each step anywhere inside a term, and write $\to$ for a single step of any kind. A term in which no step applies is in normal form. For example, with $\mathit{Id} = \tLam{X}{\Sort{0}}{X}$,

and the last term is in normal form. Reducing the inner redex first leads to the same result.

Conversion

Definitional equality, also called conversion, identifies terms that compute to the same result, up to the names of bound variables.

To decide $s \conv t$, the kernel normalizes both terms and compares the results with $\alphaeq$. This procedure relies on two facts.

• Reduction is confluent: different reduction orders cannot lead to different normal forms. So $s \conv t$ holds exactly when the normal forms of $s$ and $t$ are alpha-equivalent; there is no need to search for a clever sequence of steps.
• Every well-typed term has a normal form, so normalization terminates. This holds for our system, but it is a deep theorem (strong normalization, Chapter 14) [Barendregt 1992].

A practical kernel also caps the number of reduction steps, so that a bug cannot make it loop forever; our implementation stops after 20,000 steps with the error "reduction fuel exhausted".

Computation rules as data

Figures 7.1 and 9.1 write each iota-rule as a separate equation, which suggests that every new inductive type needs new reduction code in the kernel. It does not. A kernel stores the iota-rules as data in the signature, next to the recursor, and a single piece of code applies them for every inductive type.

Each recursor entry records the position of its major premise, the argument whose constructor decides which rule applies, and the constructors of its inductive type. For each constructor the kernel knows how many leading arguments are parameters (which the rule ignores) and how many are fields (which the rule passes on), and which fields are recursive. For three of our recursors, the data and the resulting right-hand sides are as follows; type annotations on $\lambda$ are omitted.

The right-hand side takes the arguments before the major premise, then the fields of the constructor. For example, $\NatRec{u}\;M\;z\;s\;(\suc\;n)$ selects the second rule and becomes

which beta-reduces to the right-hand side of the second equation in Figure 7.1. Likewise, the only rule of $\EqRecDep{u,v}$ fires on $\EqRecDep{u,v}\;A\;a\;M\;m\;b\;(\refl{u}\;A'\;c)$. The constructor $\refl{u}$ has two parameters, $A'$ and $c$, and no fields, so the right-hand side receives just $A\;a\;M\;m\;b$ and returns $m$.

Weak head normal form and normalization

Algorithm 12.1 defines the three functions that Algorithm 5.1 left open. Both $\Whnf$ and $\Normalize$ view a term as a spine $h\;a_1 \cdots a_n$: a head $h$ that is not an application, applied to $n \ge 0$ arguments (Chapter 2). Every term has exactly one such decomposition.

Whnf(t):
  loop:
    write t as a spine h a_1 ... a_n
    if h = λ(x : A). b and n ≥ 1:                               -- beta
        t ← (b[x ↦ a_1]) a_2 ... a_n
    else if h = c and (c : C := d) ∈ Σ:                         -- delta
        t ← d a_1 ... a_n
    else if h = c is a recursor with major position p ≤ n:      -- iota
        k b_1 ... b_j ← Whnf(a_p)
        if k is a constructor of c's inductive type with q parameters:
            t ← rhs_k a_1 ... a_{p-1} b_{q+1} ... b_j a_{p+1} ... a_n
        else return t                                           -- stuck, e.g. on a variable
    else return t

Normalize(t):
  t ← Whnf(t)
  if t = Π(x : A). B:  return Π(x : Normalize(A)). Normalize(B)
  if t = λ(x : A). b:  return λ(x : Normalize(A)). Normalize(b)
  else write t as a spine h a_1 ... a_n and return h Normalize(a_1) ... Normalize(a_n)

IsDefEq(s, t):
  return  · ; · ⊢ Normalize(s) =α Normalize(t)                  -- Figure 11.1

$\Whnf$ reduces only at the head of a term, until no rule applies there; the result is the weak head normal form. It never looks inside a $\lambda$, a $\Pi$, or the arguments of a stuck head. This is enough when a caller only needs the outermost shape of a type, such as a $\Pi$ in the application case of $\Infer$, and it is cheaper than full normalization. $\Normalize$ first computes the weak head normal form and then normalizes every immediate subterm. For example, with $t = \tLam{h}{\mathit{Id}\;P}{h}$ and $\mathit{Id}$ as above,

because the head of $t$ is a $\lambda$ with no arguments, while $\Normalize$ continues into the annotation $\mathit{Id}\;P$. Likewise, $\Whnf(\mathit{Id}\;(\mathit{Id}\;P \to P)) = \mathit{Id}\;P \to P$, which already shows a $\Pi$ although its domain is not yet normal. Both are visible below: no head step applies, yet the normal form differs.

The three cases of $\Whnf$ have the following properties.

• The iota case contains no reference to $\Nat$, $\Eq{}$, or $\mathsf{Tree}$. It reads the major position and the constructor data from the signature. It is written once; after that, each new inductive type adds rows of data, not code.
• The major premise is put in weak head normal form before the rules are consulted, because it may become a constructor only after computation. For $2 + 1$ in Chapter 7, the major premise is the numeral $1 = \suc\;\zero$, already a constructor; for $\mathit{double}\;(1 + 1)$, it is $1 + 1$, which $\Whnf$ turns into $\suc\;(1 + 0)$ first.
• If the major premise does not become a constructor, for instance because it is a variable, the term is stuck and stays as it is; this is why $0 + n$ does not reduce (Chapter 9).

Here is $\Whnf$ at work on $\mathit{double}\;(1 + 1)$, with $\mathit{double}$ as in Chapter 7, computed live. Only the head is ever reduced, but reducing the major premise forces an inner computation.

def add : Nat -> Nat -> Nat := fun (m : Nat) => fun (n : Nat) => Nat.rec1 (fun (_n : Nat) => Nat) m (fun (k : Nat) => fun (r : Nat) => Nat.succ r) n
def double : Nat -> Nat := fun (n : Nat) => Nat.rec1 (fun (_n : Nat) => Nat) Nat.zero (fun (k : Nat) => fun (r : Nat) => Nat.succ (Nat.succ r)) n

The step marked whnf is the inner computation: the recursor needs its major premise to be a constructor, so $1 + 1$ is reduced at its head first. The final weak head normal form still contains a stuck inner recursor; the normal form below it is what $\Normalize$ produces by continuing inside.

For simplicity, $\IsDefEq$ fully normalizes both terms, as our implementation does. Practical kernels instead compare lazily: they reduce both sides to weak head normal form, compare the heads, and inspect arguments only when needed. This avoids fully normalizing large terms whose heads already differ. Strong normalization guarantees that all three functions terminate on well-typed terms.

In the code

One subtlety in normalize_with_fuel deserves mention. After normalizing the function and argument of an application, it calls whnf on the rebuilt term once more. Normalizing an argument can expose a new redex at the head: for a stuck recursor application whose major premise becomes a constructor only after its own arguments are normalized, the head must be reduced again. Without this re-check, is_def_eq would miss some equalities, and the test conversion_renormalizes_exposed_redex in src/proof.rs guards it.

Exercises