Chapter 115Optional

Rewriting, Simplification, and Reflection

Prerequisites. Direct starred prerequisites: The tactic chapter is required only for the tactic wrapper; the simplifier and certificate checker use the smaller routes stated at their definitions. No later core chapter depends on this route.

The kernel reduces $(λ x . x) a$ by definitional computation. It does not reduce $a + 0$ to $a$ when addition recurses on its first argument and $a$ is neutral. The equation $plusZero (a) : a + 0 = a$ permits a propositional rewrite, but a tactic that merely replaces the left side has not yet justified the replacement, chosen an orientation, or shown that repeated rewriting terminates. A simplifier must return both a result and a proof connecting it to the input.

A proof-producing simplifier

Fix a first-order family of well-typed expressions generated by variables, constants, and declared function symbols. The family is indexed by object types, so ill-typed applications are not expressions.

Definition 115.1 — Certified rewrite database ¶

A certified rewrite rule over a telescope $Δ$ consists of well-typed expressions $l, r : A$ , a kernel derivation $q$ of $Δ ⊢ l = r$ , and a natural-number measure $μ$ satisfying $μ (r ρ) < μ (l ρ)$ for every well-typed substitution $ρ$ . Variables of $r$ must occur in $l$ . A finite ordered list $D$ of such rules is a terminating rewrite database when every rule uses the same measure $μ$ , every proper subexpression has smaller measure, and $μ$ is monotone in arguments: if $μ (a_{i}) \leq μ (b_{i})$ for every $i$ , then $μ (f \vec{a}) \leq μ (f \vec{b})$ .

At a term $t$ , the function ${root}_{D} (t)$ selects the first pair $(q, ρ)$ for which $t$ is syntactically $l ρ$ , and returns $(r ρ, q ρ)$ . It returns failure when no rule matches.

Referenced from 6 locations

The decrease premise rejects the tempting pair of rules $a + 0 \mapsto a$ and $a \mapsto a + 0$ . Each rule is valid as an equality, but their union admits an infinite simplification sequence.

Definition 115.2 — Contextual congruence certificates ¶

For each $k$ -ary symbol $f : A_{1} \to \dots \to A_{k} \to B$ , the database contains the kernel-derived operation ${cong}_{f} : (a_{1} = b_{1}) \to \dots \to (a_{k} = b_{k}) \to f a_{1} \dots a_{k} = f b_{1} \dots b_{k} .$ When $A_{i}$ depends on earlier arguments, the $i$ -th equality is a transported equality in the fiber over $b_{1}, \dots, b_{i - 1}$ ; the certificate stores those transports explicitly. A symbol is traversed only when its certificate has the required dependent type.

Referenced from 4 locations

Without the transported fiber, rewriting $n = m$ inside $v : Vec A n$ would claim that the unchanged $v$ already has type $Vec A m$ . Dependent congruence instead inserts transport before rebuilding the outer expression.

Definition 115.3 — Simplification algorithm ¶

For a well-typed expression $t : A$ , define ${simp}_{D} (t) = (u, p)$ by well-founded recursion on $μ (t)$ .

Simplify the immediate arguments from left to right. Rebuild the head with its congruence certificate, obtaining $t^{'}$ and $p_{0} : t = t^{'}$ .
If ${root}_{D} (t^{'}) = (r ρ, q ρ)$ , recursively simplify $r ρ$ to $(u, p_{1})$ , and return $(u, p_{0} \cdot q ρ \cdot p_{1})$ .
If no root rule matches, return $(t^{'}, p_{0})$ .

Here $\cdot$ is transitivity of the identity type, with directions chosen to make the displayed endpoints agree.

Referenced from 3 locations

For $D = {x + 0 \mapsto x, 0 + x \mapsto x}$ , ordered as written, bottom-up simplification calculates $\begin{aligned} (a + 0) + (0 + b) & \overset{c o n g - +}{=} a + (0 + b) \\ \overset{c o n g - +}{=} a + b . \end{aligned}$ Both annotations name proof terms constructed by congruence and the selected rule proof. No equation has been added to kernel conversion.

Theorem 115.4 — Simplifier preservation ¶

For every terminating database $D$ and well-typed $t : A$ , ${simp}_{D} (t)$ terminates and returns $(u, p)$ such that $Γ ⊢ u : A, Γ ⊢ p : t = u, μ (u) \leq μ (t) .$

Referenced from 4 locations

Proof of Theorem 115.4 — Simplifier preservation

Proof. The recursive calls on immediate arguments strictly decrease $μ$ by the proper-subexpression premise. By the induction hypotheses and argument monotonicity, rebuilding the head produces $t^{'}$ with $μ (t^{'}) \leq μ (t)$ . A root rewrite produces $r ρ$ with $μ (r ρ) < μ (t^{'})$ . Thus the recursive call after a root rewrite also strictly decreases $μ$ , proving termination.

For preservation and the output bound, use well-founded induction on that measure. The induction hypotheses for the arguments return well-typed replacements, equality proofs, and nonincreasing measures. The certificate from definition 115.2 rebuilds a well-typed $t^{'}$ and gives $p_{0} : t = t^{'}$ , including every required transport. In the root case, the rule certificate instantiated by the well-typed substitution gives $q ρ : t^{'} = r ρ$ ; the induction hypothesis gives $p_{1} : r ρ = u$ and $μ (u) \leq μ (r ρ)$ . Equality transitivity gives $t = u$ , while $μ (u) < μ (t^{'}) \leq μ (t)$ . In the no-root case, $p_{0}$ is the requested proof and argument monotonicity gives $μ (u) = μ (t^{'}) \leq μ (t)$ . These are all clauses of the algorithm. ◻

Exercise 115.1 ¶

★☆☆ Take $μ (t)$ to be the number of additions in $t$ . Determine which orientation of $a + 0 = a$ can occur in a database using $μ$ , and give a three-term loop showing why admitting both orientations destroys the termination proof.

Referenced from 3 locations

Generalized rewriting

Equality is not the only relation preserved by a context. For example, monotonicity of addition transports inequalities.

Definition 115.5 — Dependent respectful function relation ¶

Let $A : U_{i}$ , $B : A \to U_{j}$ , and $R_{A} : A \to A \to U_{k}$ . A heterogeneous fiber relation has type $R_{B} : \prod_{x : A} \prod_{y : A} R_{A} x y \to B (x) \to B (y) \to U_{ℓ} .$ For $f, g : \prod_{x : A} B (x)$ , define $Resp (R_{A}, R_{B}) (f, g) : = \prod_{x : A} \prod_{y : A} \prod_{p : R_{A} x y} R_{B} x y p (f x) (g y) .$ A dependent function $f$ is respectful when it is equipped with ${proper}_{f} : Resp (R_{A}, R_{B}) (f, f)$ . If $B$ and $R_{B}$ are constant in $x, y, p$ , this specializes to the ordinary binary relation on functions. It is stronger than the pointwise relation $\prod_{x : A} R_{B} x x ({reflex}_{R_{A}} x) (f x) (g x)$ : the respectful witness also compares outputs in different fibers $B (x)$ and $B (y)$ . No unmentioned transport is required because its target relation is indexed by the evidence $p : R_{A} x y$ .

Referenced from 5 locations

A contextual rewrite is therefore an inductively defined relation, not a traversal. Write $Rw (Γ; R; t; u; v)$ for “in $Γ$ , the term $t$ rewrites to $u$ at the relation $R$ , witnessed by the kernel term $v$ ”. The relation is not a function: which respectful morphism and which subrelation step are used is resolved by search, and different searches may return different witnesses.

Definition 115.6 — Contextual rewriting judgment ¶

Fix a certified database $D$ and, for every traversed symbol, a respectful-morphism certificate in the sense of definition 115.5. The judgment is generated by five rules.

{root}_{D} (t) = (r ρ, q ρ)

Rw (Γ; =; t; r ρ; q ρ)

Rw-Root

Γ ⊢ t : A

Γ ⊢ {reflex}_{R} : \prod_{x : A} R x x

Rw (Γ; R; t; t; {reflex}_{R} t)

Rw-Atom

Rw (Γ; Resp (R_{A}, R_{B}); f; f^{'}; v_{f})

Rw (Γ; R_{A}; a; a^{'}; v_{a})

Rw (Γ; R_{B} a a^{'} v_{a}; f a; f^{'} a^{'}; v_{f} a a^{'} v_{a})

Rw-App

Rw (Γ, x : A, y : A, p : R_{A} x y; R_{B} x y p; b; b^{'}; v)

Rw (Γ; Resp (R_{A}, R_{B}); λ x . b; λ y . b^{'}; λ x . λ y . λ p . v)

Rw-Lam

Rw (Γ; R; t; u; v)

Γ ⊢ sub : \prod_{x : A} \prod_{y : A} R x y \to S x y

Rw (Γ; S; t; u; sub t u v)

Rw-Sub

Here $Resp (R_{A}, R_{B})$ is the dependent respectful relation of definition 115.5, so the witness $v_{f}$ in Rw-App is exactly a term of type $\prod_{x : A} \prod_{y : A} \prod_{p : R_{A} x y} R_{B} x y p (f x) (f^{'} y) .$ Rewriting at $=$ is the special case in which every relation is the identity type and every ${proper}_{f}$ is ${cong}_{f}$ .

Referenced from 5 locations

The corresponding constraint-generation rules may instead treat relations and morphisms as metavariables resolved by class search. This architecture does not prove termination of an arbitrary user database. Termination remains the explicit measure premise of definition 115.1.

Proposition 115.7 — Contextual preservation ¶

If $Rw (Γ; R; t; u; v)$ is derivable in definition 115.6, then $Γ ⊢ v : R t u$ .

Referenced from 4 locations

Proof of Proposition 115.7 — Contextual preservation

Proof. Rule induction on the derivation, one case per rule of definition 115.6.

Rw-Root: definition 115.1 supplies $Γ ⊢ q ρ : t = r ρ$ as the instantiated rule certificate.

Rw-Atom: the stored reflexivity proof has type $R t t$ at the instantiating argument $t$ .

Rw-App: the induction hypothesis for the function gives $Γ ⊢ v_{f} : \prod_{x : A} \prod_{y : A} \prod_{p : R_{A} x y} R_{B} x y p (f x) (f^{'} y)$ and the one for the argument gives $Γ ⊢ v_{a} : R_{A} a a^{'}$ . Three applications derive $Γ ⊢ v_{f} a a^{'} v_{a} : R_{B} a a^{'} v_{a} (f a) (f^{'} a^{'})$ .

Rw-Lam: the induction hypothesis in the context $Γ, x : A, y : A, p : R_{A} x y$ gives $Γ, x : A, y : A, p : R_{A} x y ⊢ v : R_{B} x y p b b^{'}$ . Three $Π$ -introductions produce $λ x . λ y . λ p . v : Resp (R_{A}, R_{B}) (λ x . b) (λ y . b^{'})$ , exactly the conclusion relation.

Rw-Sub: the induction hypothesis gives $Γ ⊢ v : R t u$ , and the stored implication carries it to $S t u$ .

These are the five rules of the judgment. ◻

The dependent case is now explicit in Rw-App. Its conclusion relation is $R_{B} a a^{'} v_{a}$ , whose left and right endpoints have types $B (a)$ and $B (a^{'})$ . A symbol without a witness of $Resp (R_{A}, R_{B})$ is not traversed; substituting a merely pointwise witness would leave the application at $a^{'}$ untyped.

Reflection with a small checker

Executing a normalizer inside the metaprogram does not justify its answer. Reflection reduces trust by making the kernel evaluate a small verified checker.

Definition 115.8 — Reflected commutative-monoid expressions ¶

For an environment $ρ : N \to M$ , where $(M, 0, +)$ is a commutative monoid, expressions and their denotation are $\begin{aligned} e & ::= var (i) ∣ zero ∣ add (e, e), \\ {eval}_{ρ} (var (i)) & = ρ (i), \\ {eval}_{ρ} (zero) & = 0, \\ {eval}_{ρ} (add (e_{1}, e_{2})) & = {eval}_{ρ} (e_{1}) + {eval}_{ρ} (e_{2}) . \end{aligned}$ The normal form $nf (e)$ is the finite vector of variable multiplicities, computed by vector addition. The checker $sameNF (e_{1}, e_{2})$ compares these vectors.

Referenced from 3 locations

Rewriting, Simplification, and Reflection

Lemma 115.9 — Evaluation of multiplicity normal forms ¶

For every expression $e$ and environment $ρ$ , ${eval}_{ρ} (e) = \sum_{i} \underset{nf (e) (i) times}{\underset{⏟}{ρ (i) + \dots + ρ (i)}} .$

Referenced from 3 locations

Rewriting, Simplification, and Reflection

Proof of Lemma 115.9 — Evaluation of multiplicity normal forms

Proof. By structural induction on $e$ . A variable contributes the unit vector at its index, and zero contributes the zero vector. For addition, the induction hypotheses give the two finite sums. Associativity and commutativity regroup their concatenation by index, and vector addition adds the two multiplicities. ◻

Theorem 115.10 — Reflection checker soundness ¶

If $sameNF (e_{1}, e_{2}) = true$ , then for every commutative monoid $M$ and environment $ρ$ , ${eval}_{ρ} (e_{1}) = {eval}_{ρ} (e_{2}) .$

Referenced from 4 locations

Proof of Theorem 115.10 — Reflection checker soundness

Proof. The Boolean result means that the two finite multiplicity vectors are equal component by component. Apply lemma 115.9 to both expressions and replace one vector by the other. The resulting finite sums are identical. ◻

Reification itself remains untrusted. The tactic constructs expressions $e_{1}, e_{2}$ and kernel proofs that their evaluations equal the original terms. The kernel then combines those proofs with theorem 115.10. A wrong reification proof is rejected.

Programming up to congruence. The simplifier above leaves kernel conversion alone and pays for every replacement with a proof term. A different design changes the conversion relation itself. It is a separate calculus with separate theorems, and it is frozen here so that nothing above is read as applying to it.

Convention 115.11 — Zombie source card ¶

Write Zombie for the comparison calculus, which has two layers.

The core language is dependently typed with erasable annotations and no automatic beta conversion. Its evaluation relation is a small-step reduction on erased terms, and beta equalities enter only through the explicit proof form $join$ , which reduces both sides a bounded number of steps and returns an equation. Recursion is unrestricted, so a well-typed term may diverge; type checking never evaluates a term except under a $join$ with its own step bound.
The surface language is bidirectional. Its type equality is defined to be the typed congruence closure $Γ ⊢ a = b$ of the equations available in $Γ$ , closed under reflexivity, symmetry, transitivity, congruence for labelled applications, injectivity of type constructors, and an assumption rule. Two types related by that closure are interchangeable without a written cast.

The source separates four boundaries. Theorem 1 proves soundness of elaboration from surface derivations to core terms, including preservation of erasure. Theorem 2 proves completeness with respect to the declarative surface system. Lemma 3 decides the finite, labelled, untyped congruence judgment used by the algorithm; it does not by itself establish a typed equality or construct its core proof. Theorem 4 supplies that missing bridge: from the source’s well-formed typed congruence judgment and its well-formed equality type, the elaborator constructs the corresponding core equality proof. Decidability therefore rests on finite labelled congruence closure together with the separate typing bridge, not on normalization of possibly diverging terms.

Referenced from 3 locations

Rewriting, Simplification, and Reflection

The move that this buys is visible in one equation. In the core language, $npluszero : \prod_{n : N} n + 0 = n$ is proved by induction on $n$ . In the successor case the hypothesis is $ih : m + 0 = m$ and the goal is $suc (m + 0) = suc m$ . Ordinary definitional conversion cannot close it: with addition recursing on its first argument and $m$ a variable, $m + 0$ is a neutral term and $suc (m + 0) \equiv suc m$ fails. The surface language closes it because $ih$ is in the context and congruence under the label $suc$ belongs to the equality relation, so the goal type is reached with no written cast. The same example shows the cost: the base case needs $0 + 0 = 0$ , which no assumption supplies, and the programmer must write $join$ to obtain it by reduction, because beta is not part of the surface equality either.

Three boundaries hold. The congruence relation of convention 115.11 is not added to the kernel conversion of this chapter, so theorem 115.4 and proposition 115.7 neither use it nor follow from it; conversely, nothing in that source proves the measure-based termination of definition 115.1. A neutral application may be equal by the generated congruence while remaining definitionally stuck, which is exactly the $suc (m + 0)$ case above. Finally, the congruence proof terms the algorithm returns are core terms, not kernel derivations of this chapter’s identity type, and Lemma 3 is a decision procedure for that source relation only.

Sources

The generalized-rewriting architecture follows Sozeau [Soz09]; its constraint rules are in Figure 1. The comparison calculus follows Sjöberg and Weirich [SW15].

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 115.2, then complete exercise 115.4.

Exercise 115.2 ¶

★★☆ Extend the opening database by associativity oriented toward right-associated terms. Give a lexicographic measure that proves termination, and simplify $(a + 0) + (b + (0 + c))$ with every equality step annotated.

Referenced from 4 locations

Exercise 115.3 ¶

★★★ Write the dependent congruence certificate for $transport : (n = m) \to Vec A n \to Vec A m .$ Exhibit the ill-typed intermediate term produced if the transport is omitted.

Referenced from 3 locations

Exercise 115.4 ¶

★★★ Practical project.proof-producing-commutative-monoid-simplifier Implement in Agda or Kappa the expressions, normalizer, and checker of definition 115.8, with no trailing zero multiplicities. Add a finite indexed relation with related indices whose fibers have different shapes, and check that a dependent function respects that relation. Print equal on commute and reassociate, not-equal on different, and dependent-respectful on the heterogeneous fiber case. Deleting the right summand must change the reassociate result. Replacing the heterogeneous fiber relation by a same-fiber test must change the final result to dependent-respectful-failed. These four named results are the acceptance test. They check the finite reflected theory and one finite model of dependent respectfulness, not arbitrary dependent rewriting.

Referenced from 5 locations