The lambda-Pi-Calculus Modulo Rewriting

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

A logical framework can represent an object theory while failing to compute with it. If natural-number addition is encoded by a constant, the term $\mathsf{plus}(\mathsf{s}\mathsf{z})(\mathsf{s}\mathsf{z})$ is stuck until a proof explicitly rewrites it. The $\lambda \mathrm{\Pi }$-calculus modulo rewriting instead admits selected equations as part of conversion. This makes an encoded theory calculate, but it transfers a proof obligation to the signature: an ill-typed, nonconfluent, or nonterminating rule set can destroy the kernel properties on which checking depends.

The obstruction is therefore not the absence of computation but the absence of a disciplined boundary around computation. A typed rewrite signature supplies that boundary: its rules preserve classifiers, its overlaps are joinable, and its reduction relation terminates whenever conversion is to be decided by normal forms.

A typed rewrite signature

For a first derivation, assume $$\mathsf{Nat}:\mathsf{Type},\mathsf{z}:\mathsf{Nat},\mathsf{s}:\mathsf{Nat}\to \mathsf{Nat},\mathsf{plus}:\mathsf{Nat}\to \mathsf{Nat}\to \mathsf{Nat}.$$ Rule Mod-Const types $\mathsf{plus}$, Mod-App twice types $\mathsf{plus}\mathsf{z}n$, and Mod-Var supplies the final argument. Rule Mod-Pi forms the arrow types, while Mod-Lam types the beta redex $(\lambda x:\mathsf{Nat}.x)n$. Thus every rule on the card has a concrete use before rewrite rules enter the signature.

Add the two rules The first telescope is $n:\mathsf{Nat}$; the second is $m:\mathsf{Nat},n:\mathsf{Nat}$. Both sides of each rule have type $\mathsf{Nat}$. The two roots are disjoint and left-linear. The calculation $$\mathsf{plus}(\mathsf{s}\mathsf{z})(\mathsf{s}\mathsf{z}){⟶}_{\mathrm{\Sigma }}\mathsf{s}(\mathsf{plus}\mathsf{z}(\mathsf{s}\mathsf{z})){⟶}_{\mathrm{\Sigma }}\mathsf{s}(\mathsf{s}\mathsf{z})$$ uses Mod-Rewrite twice. By contrast, $\mathsf{plus}xn$ is stuck when $x$ is neutral: neither left-hand side matches. Rule Mod-Beta separately contracts $(\lambda x:\mathsf{Nat}.\mathsf{s}x)\mathsf{z}$ to $\mathsf{s}\mathsf{z}$.

Substitution and preservation

Proof of Lemma 97.3 — Typed substitution

Proof. Induct on the typing derivation. The variable case is the supplied judgment when the variable is $x$, and otherwise follows from the correspondingly substituted declaration. Constants and sorts are unchanged. For Mod-Pi and Mod-Lam, alpha-rename the bound variable away from $\mathrm{FV}(u)$, apply the induction hypothesis to the domain and body premises, and rebuild the same rule. The Mod-App case uses $$(B[v/y])[u/x]=B[u/x][v[u/x]/y],$$ the capture-avoiding substitution-composition equation. In the Mod-Conv case, compatibility of ${\equiv }_{\beta \mathrm{\Sigma }}$ with substitution transports $A{\equiv }_{\beta \mathrm{\Sigma }}B$ to $A[u/x]{\equiv }_{\beta \mathrm{\Sigma }}B[u/x]$, after which Mod-Conv rebuilds the conclusion. ◻

Proof of Lemma 97.4 — A typed rule remains typed after matching

Proof. Apply lemma 97.3 once for each declaration in the telescope $\mathrm{\Delta }$, from left to right. Dependency forces this order: a later component of $\theta$ is checked only after the earlier components have been substituted into its type. ◻

Proof of Theorem 97.5 — Subject reduction for the algebraic fragment

Proof. This is Saillard’s Subject Reduction Theorem 2.1 at the raw relation ${⟶}_{\beta \mathrm{\Sigma }}$ [Sai15]. Its induction is on the raw reduction derivation. Product compatibility supplies beta preservation under binders, and permanent well-typedness supplies user-rule preservation in every enclosing declaration context. Lemma 97.3, Lemma 97.4 are the corresponding local substitution mechanisms; they do not replace the permanent-extension hypothesis. ◻

The product-compatibility premise is not decoration. Without injectivity of dependent products modulo conversion, inversion of application does not identify the argument domain required by the lambda body. Likewise, well-typedness of a rule only in its declaration context is insufficient when later declarations can change conversion; Saillard therefore uses permanent well-typedness over well-formed extensions.

Confluence is not an algorithm

Proof of Theorem 97.6 — The conditional metatheorem chain

Proof. For (1), reduce convertible products to a common reduct. A product at the head cannot be erased by an algebraic root; comparing the common product gives convertible domains and codomains. Item (2) is theorem 97.5 plus induction on two typing derivations: after conversion is pushed to their leaves, product compatibility makes the function domains agree. For (3), termination produces a normal form, confluence makes it unique up to alpha-equivalence, and computable finite branching makes normalization effective. Conversely, a confluent relation may admit an infinite reduction path, so confluence alone supplies no normalizer. Items (1) and (2) are Saillard’s Theorems 2.3 and 2.1–2.2; item (3) is the effective normal-form corollary, whose extra hypotheses are stated here explicitly [Sai15]. ◻

For the addition rules, the number of leading successors in the first argument decreases at the recursive root, so the user-rule relation ${⟶}_{\mathrm{\Sigma }}$ terminates. The rules are left-linear and have no critical pair, so that relation is confluent. Saillard’s imported Theorem 2.4 states that a left-algebraic, left-linear, confluent user relation makes the combined beta-and-user relation confluent [Sai15]. It does not transfer termination: no termination proof for ${⟶}_{\beta \mathrm{\Sigma }}$ has been supplied here, so the normal-form decision procedure in item (3) is not discharged for this signature.

Left-hand lambdas require rewriting modulo beta

Ordinary matching treats beta-equivalent left sides as different syntax. A rule headed by a pattern containing an abstraction can therefore overlap with beta reduction even when its intended higher-order pattern is unambiguous. Writing the combined relation merely as ${⟶}_{\beta }\cup {⟶}_{\mathrm{\Sigma }}$ hides that overlap.

Proof of Theorem 97.8 — Modulo-beta boundary

Proof. Item (1) is Saillard’s Theorem 6.1: the HRS step factors into beta expansions, one typed rule instance, and beta contractions, with a well-typed intermediate chosen for a well-typed source. Lemma 6.1 defines the combined relation used in item (2), and Theorem 6.2 proves that it generates ${\equiv }_{\beta \mathrm{\Sigma }}$. Confluence then gives product compatibility by Theorem 6.3, and the lambda-Pi-pattern criterion is Theorem 6.4 [Sai15]. Combining these results with theorem 97.6 gives the conclusion. The proof does not replace HRS confluence by ordinary union confluence. ◻

An implicational encoding

Let the signature contain $$\mathsf{prop}:\mathsf{Type},\mathsf{prf}:\mathsf{prop}\to \mathsf{Type},\mathsf{imp}:\mathsf{prop}\to \mathsf{prop}\to \mathsf{prop}$$ and the rule $$\begin{array}{}\text{(}Imp\text{)}& \mathsf{prf}(\mathsf{imp}AB)⟼\mathsf{prf}(A)\to \mathsf{prf}(B).\end{array}$$ The rule is typed in $A:\mathsf{prop},B:\mathsf{prop}$. A natural- deduction introduction $$\frac{\mathrm{\Gamma },A⊢B}{\mathrm{\Gamma }⊢A\Rightarrow B}$$ is represented by lambda abstraction. If $p:\mathsf{prf}(A)⊢t:\mathsf{prf}(B)$, then Mod-Lam gives $$\lambda p:\mathsf{prf}(A).t:\mathsf{prf}(A)\to \mathsf{prf}(B),$$ and Mod-Conv with (Imp) gives it type $\mathsf{prf}(\mathsf{imp}AB)$. Elimination is ordinary Mod-App. A neutral proof variable remains stuck; only an application of an introduced implication produces a beta redex.

Proof of Theorem 97.9 — Adequacy for normal implicational derivations

Proof. Map hypothesis $H_i$ to its proof variable $p_i$, implication introduction to lambda, and implication elimination to application. Rule (Imp) makes the introduction and elimination classifiers definitionally equal to the corresponding function types. Conversely, canonical-form inversion at $\mathsf{prf}(\mathsf{imp}AB)$ exposes a lambda, while a neutral proof exposes a head assumption followed by applications. Induction on the normal term reconstructs the unique normal derivation. The two maps commute with alpha-renaming; beta-eta-longness removes the administrative redex and eta-short alternatives. The theorem is restricted to this signature and normal forms, so it asserts neither conservativity of every encoding nor normalization of arbitrary rewrite signatures. ◻

A concrete rule-registration boundary

Cockx’s Agda interface accepts a declaration with schema $$\mathrm{\forall }\mathrm{\Delta }.f\overline{p}:A⟼v.$$ Patterns are unapplied variables or applications of declared symbols to patterns. Registration checks that the pattern binds the variables of $\mathrm{\Delta }$, that both sides have the displayed type $A$, and that the left side is neutral. Non-linear occurrences become equality constraints during matching. These are the source’s concrete syntax and local admissibility checks [Coc20].

In the retained observational-type-theory Agda case, a proved equality is registered so that its left head and argument patterns populate $f\overline{p}$, its right side populates $v$, and its equality proof supplies the same-type check. The example then computes coercion equations through the registered rules. Registration establishes scope, typing, and a usable head pattern; it establishes neither confluence nor termination. Those global obligations remain exactly the hypotheses separated in theorem 97.6.

Dedukti and Lambdapi impose their own concrete parser and rule-admissibility contracts [Ded22, Ded25]. Their retained accept/reject tests are implementation evidence, not proofs of confluence, termination, adequacy, or conservativity. The Kappa companion below checks a finite first-order certificate boundary; it does not implement dependent conversion or higher-order matching.

Bibliographic notes

The rule and theorem boundary follows Saillard’s public EPTCS paper [Sai15]; its printed pp. 92 and 98 were inspected directly for Theorems 2.1–2.5 and 6.1–6.4. Blanqui’s course provides the longer implementation sequence [Bla25]. Dedukti and Lambdapi are pinned implementation evidence, not theorem owners. Cockx owns the Agda rule-registration boundary [Coc20]. Rewriting in conversion is not tactic rewriting, a quotient path constructor, or permission to add unchecked recursive equations.