ch:type-theory-modulo: the λΠ-calculus modulo rewriting

Declare $$\mathsf{double}\mathsf{z}⟼\mathsf{z},\mathsf{double}(\mathsf{s}n)⟼\mathsf{s}(\mathsf{s}(\mathsf{double}n)).$$ Both sides have type $\mathsf{Nat}$ in the displayed rule telescope. Then $$\mathsf{double}(\mathsf{s}(\mathsf{s}\mathsf{z})){⟶}_{\mathrm{\Sigma }}\mathsf{s}(\mathsf{s}(\mathsf{double}(\mathsf{s}\mathsf{z}))){⟶}_{\mathrm{\Sigma }}{\mathsf{s}}^4(\mathsf{double}\mathsf{z}){⟶}_{\mathrm{\Sigma }}{\mathsf{s}}^4\mathsf{z}.$$ For neutral $x$, $\mathsf{double}x$ is stuck: $x$ matches neither $\mathsf{z}$ nor $\mathsf{s}n$.

Write the matching substitution as $\theta =(u/x,v/y)$. First substitute $u$ in the derivations $x:A,y:B(x)⊢\ell :T$ and $x:A,y:B(x)⊢r:T$. Typed substitution requires $\mathrm{\Gamma }⊢u:A$ and yields derivations in $\mathrm{\Gamma },y:B(u)$. The second component must therefore satisfy $\mathrm{\Gamma }⊢v:B(u)$, not $v:B(x)$. Substituting $v$ gives $\mathrm{\Gamma }⊢\ell \theta :T\theta$ and $\mathrm{\Gamma }⊢r\theta :T\theta$, as required.

The new right-zero rule overlaps the zero-left rule at $\mathsf{plus}\mathsf{z}\mathsf{z}$; both roots contract to $\mathsf{z}$. It overlaps the successor-left rule at $\mathsf{plus}(\mathsf{s}m)\mathsf{z}$. Right-zero contracts directly to $\mathsf{s}m$, while successor-left gives $\mathsf{s}(\mathsf{plus}m\mathsf{z})$, which contracts internally by right-zero to $\mathsf{s}m$. The two original roots do not unify, and each self-overlap is trivial. Joinability checks only local peaks. It supplies no well-founded measure on rewrite sequences, so termination remains a separate obligation.

Take one constant $a$ and the rule $a⟼a$. Every pair of finite reductions from a term has a common descendant, so the relation is confluent, but $a{⟶}_{\mathrm{\Sigma }}a{⟶}_{\mathrm{\Sigma }}\cdots$ is infinite and $a$ has no normal form. An algorithm that converts by normalizing both inputs therefore does not terminate even on $(a,a)$. Confluence gives uniqueness of normal forms when they exist; it neither produces them nor proves that normalization terminates.

The normal derivation assumes $f:A\Rightarrow B$ and $a:A$, eliminates $f$ at $a$ to obtain $B$, and introduces twice. Its term is $$\lambda f:\mathsf{prf}(\mathsf{imp}AB).\lambda a:\mathsf{prf}(A).fa.$$ Rule (Imp) converts the type of $f$ to $\mathsf{prf}(A)\to \mathsf{prf}(B)$ and converts the two lambda types back to $\mathsf{prf}((A\Rightarrow B)\Rightarrow A\Rightarrow B)$.

Conversely, a beta-eta-long normal inhabitant of that type converts to a function type, so canonical-form inversion exposes the outer lambda; applying the same inversion to its codomain exposes the inner lambda. Invert the remaining normal form recursively. A lambda reconstructs implication introduction. A neutral form has an assumption as head and a spine of normal arguments; typing inversion reconstructs one implication elimination for each argument. For the displayed inhabitant the head is $f$ and its one argument is the assumption derivation for $a$. These inversions reconstruct every normal derivation of the formula, including additional ones when $A$ or $B$ has implicational structure.