## Formalized Name Weak Normalization for the Simply Typed Lambda Calculus with Products, Sums, Unit, and Empty Type ## Formalized Statement Let $\mathcal T$ be the simply typed lambda calculus whose types are generated from atomic types by $A \to B$, $A \times B$, $A+B$, $\top$, and $\bot$. Terms are generated by variables, lambda abstraction and application, pairing and projections, injections $\operatorname{inl}$ and $\operatorname{inr}$ and case analysis, the unit term $\star$ and unit elimination $\operatorname{let}_{\top}(t;r)$, and empty elimination $\operatorname{abort}_C(t)$. There is no recursion or fixpoint operator. Let $\to_\beta$ be the one-step contextual beta-reduction relation generated by the usual computation rules for these eliminators, and let $\to_\beta^*$ be its reflexive transitive closure. For every well-typed judgment $\Gamma \vdash t:A$, there exist a term $n$ and a finite beta-reduction sequence $t \to_\beta^* n$ such that $n$ is beta-normal, meaning that no term $n'$ satisfies $n \to_\beta n'$. ## Proof [proofplan] We prove weak normalization by Tait computability. The key repair is to use saturated reducibility candidates: besides defining reducibility by induction on types, we prove the closure properties needed for neutral terms, especially the neutral expansion lemma. This proves variables and empty eliminations reducible at compound types without circularity. The fundamental lemma then shows that every typed term sends reducible substitutions to reducible terms, and applying it to the identity substitution gives the desired normal form. [/proofplan] [step:Define weak normalization, reduction height, and reducibility] Write $\mathrm{WN}(t)$ to mean that there is a beta-normal term $n$ with $t \to_\beta^* n$. If $\mathrm{WN}(t)$ holds, define $h(t) \in \mathbb N$ to be the maximum length of a beta-reduction sequence starting at $t$. This maximum exists because the finitely branching reduction tree below a weakly normalizing term has no infinite branch. For each type $A$, define a predicate $\mathcal R_A(t)$ on well-typed terms $t:A$ by induction on $A$. If $A$ is atomic, $\mathcal R_A(t)$ means $\mathrm{WN}(t)$. Also $\mathcal R_{\top}(t)$ and $\mathcal R_{\bot}(t)$ mean $\mathrm{WN}(t)$. For $A=B\to C$, $\mathcal R_{B\to C}(t)$ means that $\mathrm{WN}(t)$ holds and, for every term $u:B$ with $\mathcal R_B(u)$, one has $\mathcal R_C(tu)$. For $A=B\times C$, $\mathcal R_{B\times C}(t)$ means that $\mathrm{WN}(t)$ holds, $\mathcal R_B(\pi_1 t)$ holds, and $\mathcal R_C(\pi_2 t)$ holds. For $A=B+C$, $\mathcal R_{B+C}(t)$ means that $\mathrm{WN}(t)$ holds and every case analysis from $t$ into a reducible target is reducible: for every type $D$ and every pair of branch terms $r$ and $s$ such that $r[a/x]$ is reducible at $D$ for every reducible $a:B$ and $s[b/y]$ is reducible at $D$ for every reducible $b:C$, the term $\operatorname{case}(t;x.r;y.s)$ is reducible at $D$. By definition, $\mathcal R_A(t)$ implies $\mathrm{WN}(t)$ for every type $A$. [/step] [step:Prove the saturated candidate properties] We use the following three closure properties of reducibility. [claim:Reducibility is closed under one-step reduction] If $\mathcal R_A(t)$ and $t \to_\beta t'$, then $\mathcal R_A(t')$. [/claim] [proof] The proof is by induction on $A$. Weak normalization is preserved by taking a reduct. At atomic, unit, and empty types this is the whole assertion. At a function type $B\to C$, let $u:B$ satisfy $\mathcal R_B(u)$. Since $tu \to_\beta t'u$, the induction hypothesis at $C$ applied to $\mathcal R_C(tu)$ gives $\mathcal R_C(t'u)$. The product case follows from the reductions $\pi_i t \to_\beta \pi_i t'$ and the induction hypothesis at the component types. The coproduct case follows from the reduction $\operatorname{case}(t;x.r;y.s) \to_\beta \operatorname{case}(t';x.r;y.s)$ and the induction hypothesis at the target type. [/proof] [claim:Reducibility is closed under one-step beta expansion] If $t \to_\beta t'$ and $\mathcal R_A(t')$, then $\mathcal R_A(t)$. [/claim] [proof] The proof is again by induction on $A$. Since $\mathcal R_A(t')$ implies $\mathrm{WN}(t')$, prefixing the reduction $t \to_\beta t'$ to a normalizing sequence for $t'$ gives $\mathrm{WN}(t)$. At atomic, unit, and empty types this proves the claim. At a function type $B\to C$, if $\mathcal R_B(u)$ then $tu \to_\beta t'u$ and $\mathcal R_C(t'u)$, so the induction hypothesis at $C$ gives $\mathcal R_C(tu)$. The product and coproduct cases are identical in form, using contextual closure through projections and case analysis. [/proof] [claim:Neutral beta expansion] Let $e:A$ be neutral. If every one-step reduct $e'$ of $e$ satisfies $\mathcal R_A(e')$, then $\mathcal R_A(e)$. [/claim] [proof] The proof is by induction on the pair consisting of the type $A$ and the reduction height $h(e)$, ordered lexicographically. The hypothesis on one-step reducts implies $\mathrm{WN}(e)$: every immediate reduct is weakly normalizing, and a beta-normal form is reached by choosing any finite branch in the finitely branching reduction tree. For atomic, unit, and empty types, reducibility is weak normalization, so $\mathcal R_A(e)$ follows. Let $A=B\to C$. To prove $\mathcal R_{B\to C}(e)$, let $u:B$ satisfy $\mathcal R_B(u)$. The term $eu$ is neutral. Every one-step reduct of $eu$ is either $e'u$ with $e \to_\beta e'$, or $eu'$ with $u \to_\beta u'$. In the first case $\mathcal R_{B\to C}(e')$ holds by hypothesis, hence $\mathcal R_C(e'u)$. In the second case, closure under reduction gives $\mathcal R_B(u')$, and the induction hypothesis on the smaller height of $eu'$ gives the required reducibility of that reduct. Thus all one-step reducts of $eu$ are reducible at $C$, so the induction hypothesis gives $\mathcal R_C(eu)$. Let $A=B\times C$. The terms $\pi_1 e$ and $\pi_2 e$ are neutral. A one-step reduct of $\pi_i e$ is either $\pi_i e'$ with $e \to_\beta e'$ or comes from a contextual reduction inside the projection. In the first case reducibility follows from $\mathcal R_{B\times C}(e')$; in the contextual case it follows by the secondary induction on reduction height. Therefore the induction hypothesis gives the reducibility of both projections, and hence $\mathcal R_{B\times C}(e)$. Let $A=B+C$. Fix a type $D$ and branch terms $r$ and $s$ satisfying the branch reducibility condition in the definition of $\mathcal R_{B+C}$. The term $\operatorname{case}(e;x.r;y.s)$ is neutral. Its one-step reducts either reduce the scrutinee, reduce inside one of the branches, or reduce inside a subterm already present in the whole case expression. If the scrutinee reduces to $e'$, then $\mathcal R_{B+C}(e')$ gives reducibility of the resulting case term. If a branch reduces, the branch condition is preserved by closure of reducibility under reduction. All remaining contextual reducts have smaller reduction height, so the induction hypothesis applies. Thus every one-step reduct of the case term is reducible at $D$, and neutral expansion gives $\mathcal R_D(\operatorname{case}(e;x.r;y.s))$. This proves the coproduct clause. [/proof] [guided] The point of this step is to avoid the circular argument that says a variable is reducible because its eliminations are reducible. Instead, we prove a genuine saturation fact: a neutral term is reducible when all of its immediate reducts are reducible. Variables then become reducible because they have no immediate reducts. First, reducibility is stable under reducing a term. For example, if $t:B\to C$ is reducible and $t \to_\beta t'$, then for every reducible argument $u:B$ the application $tu$ is reducible at $C$. Since $tu \to_\beta t'u$, the induction hypothesis at $C$ gives $\mathcal R_C(t'u)$. Thus $t'$ is reducible as a function. Products and sums use the same argument through the relevant eliminators. Second, reducibility is stable under one-step beta expansion. If $t \to_\beta t'$ and $t'$ is reducible, then $t$ weakly normalizes by taking the first step to $t'$ and then normalizing $t'$. At a compound type, every elimination of $t$ takes one contextual step to the corresponding elimination of $t'$, so the induction hypothesis transfers reducibility back across that step. Finally, let $e:A$ be neutral and assume every immediate reduct of $e$ is reducible at $A$. We prove $\mathcal R_A(e)$ by induction on the type and on the reduction height $h(e)$. At base types, reducibility is just weak normalization. At a function type $B\to C$, we must show that $eu$ is reducible whenever $u$ is reducible at $B$. The term $eu$ is neutral. A one-step reduct of $eu$ is either $e'u$, where $e \to_\beta e'$, or $eu'$, where $u \to_\beta u'$. In the first case $e'$ is reducible by hypothesis, so the function clause gives reducibility of $e'u$. In the second case reducibility of $u'$ follows from closure under reduction, and the induction on the smaller reduction height handles $eu'$. Therefore every immediate reduct of $eu$ is reducible, so neutral expansion at type $C$ gives $\mathcal R_C(eu)$. At a product type, the neutral terms $\pi_1 e$ and $\pi_2 e$ are handled in the same way. Reducing $e$ gives projections of reducible reducts of $e$, and any other contextual reduct has smaller reduction height. At a coproduct type, we test $e$ by an arbitrary case expression whose branches send reducible inputs to reducible outputs. A reduct of the case either reduces the scrutinee, in which case the reducibility of the scrutinee reduct applies, or reduces inside a branch, in which case branch reducibility is preserved by closure under reduction, or is a smaller contextual reduct. Thus the whole case term is reducible. This proves the saturation lemma needed for variables, open neutral terms, and empty eliminations. [/guided] [/step] [step:Show variables and reducible substitutions are available] A substitution $\rho$ for a context $\Gamma=x_1:A_1,\ldots,x_m:A_m$ assigns to each variable $x_i$ a term $\rho(x_i):A_i$. It is reducible, written $\mathcal R_\Gamma(\rho)$, if $\mathcal R_{A_i}(\rho(x_i))$ holds for every $i$. Every variable $x:A$ is neutral and has no one-step reduct. By neutral beta expansion, $\mathcal R_A(x)$ holds for every type $A$. Define $\operatorname{id}_\Gamma$ to be the identity substitution on $\Gamma$, namely the substitution with $\operatorname{id}_\Gamma(x)=x$ for each variable $x$ in $\Gamma$. Since every variable is reducible, $\mathcal R_\Gamma(\operatorname{id}_\Gamma)$ holds. [/step] [step:Prove the fundamental lemma by induction on typing derivations] We prove by induction on the derivation of $\Gamma\vdash t:A$ that, for every reducible substitution $\rho$ for $\Gamma$, the substituted term $t[\rho]$ satisfies $\mathcal R_A(t[\rho])$. For a variable $x:A$, the term $x[\rho]$ is $\rho(x)$, which is reducible by the definition of $\mathcal R_\Gamma(\rho)$. For lambda introduction, suppose $t=\lambda x:A.r$ and $\Gamma,x:A\vdash r:B$. Let $\rho$ be reducible for $\Gamma$. To prove reducibility at $A\to B$, let $u:A$ satisfy $\mathcal R_A(u)$. The extended substitution $\rho[x\mapsto u]$ is reducible for $\Gamma,x:A$, so the induction hypothesis gives $\mathcal R_B(r[\rho[x\mapsto u]])$. The beta step $(\lambda x:A.r[\rho])u \to_\beta r[\rho[x\mapsto u]]$ and beta expansion give $\mathcal R_B((\lambda x:A.r[\rho])u)$. The weak normalization part of $\lambda x:A.r[\rho]$ follows by applying the induction hypothesis to the reducible extension $\rho[x\mapsto x]$, because $x$ is reducible and reductions under the lambda are exactly reductions of the body. Thus the abstraction is reducible. For application, the induction hypotheses give $\mathcal R_{A\to B}(r[\rho])$ and $\mathcal R_A(s[\rho])$, and the function clause gives $\mathcal R_B(r[\rho]s[\rho])$. For pairing, the induction hypotheses give $\mathcal R_A(r[\rho])$ and $\mathcal R_B(s[\rho])$. The beta steps $\pi_1(r[\rho],s[\rho]) \to_\beta r[\rho]$ and $\pi_2(r[\rho],s[\rho]) \to_\beta s[\rho]$ plus beta expansion give reducibility of both projections. The pair weakly normalizes by normalizing its two components. Hence $(r,s)[\rho]$ is reducible at $A\times B$. For product elimination, reducibility of the pair term is supplied by the induction hypothesis, and the product clause gives reducibility of the required projection. For coproduct introduction, consider $\operatorname{inl}(r):A+B$; the right injection is symmetric. The induction hypothesis gives $\mathcal R_A(r[\rho])$. For any reducible case branches into a type $C$, the beta step $\operatorname{case}(\operatorname{inl}(r[\rho]);x.u;y.v) \to_\beta u[r[\rho]/x]$ has reducible target by the branch hypothesis. Beta expansion gives reducibility of the case expression. Weak normalization of the injection follows from weak normalization of $r[\rho]$. For case elimination, suppose $t=\operatorname{case}(r;x.u;y.v):C$. The induction hypothesis gives $\mathcal R_{A+B}(r[\rho])$. If $a:A$ is reducible, then $\rho[x\mapsto a]$ is reducible, so the induction hypothesis for $u$ gives $\mathcal R_C(u[\rho[x\mapsto a]])$. The same argument for a reducible $b:B$ gives $\mathcal R_C(v[\rho[y\mapsto b]])$. The coproduct clause for $r[\rho]$ gives $\mathcal R_C(t[\rho])$. For unit introduction, $\star$ is beta-normal, so $\mathcal R_\top(\star)$ holds. For unit elimination, write the term as $\operatorname{let}_{\top}(r;s):C$, where $r:\top$ and $s:C$ in the same substituted context, with computation rule $\operatorname{let}_{\top}(\star;s) \to_\beta s$. The induction hypotheses give $\mathcal R_\top(r[\rho])$ and $\mathcal R_C(s[\rho])$. The defining clause for $\top$ gives weak normalization of $r[\rho]$. If $r[\rho]$ reduces to $\star$, beta expansion from $s[\rho]$ gives reducibility of the corresponding eliminator. If the scrutinee reduces first, closure under reduction and induction on its normalizing sequence give reducibility of the eliminator. Hence $\mathcal R_C(\operatorname{let}_{\top}(r[\rho];s[\rho]))$. For empty elimination, suppose $t=\operatorname{abort}_C(r)$ and $r:\bot$. The induction hypothesis gives $\mathcal R_\bot(r[\rho])$, hence $\mathrm{WN}(r[\rho])$. The term $\operatorname{abort}_C(r[\rho])$ is neutral, and every immediate reduct is of the form $\operatorname{abort}_C(r')$ with $r[\rho]\to_\beta r'$. By closure under reduction, $r'$ is reducible at $\bot$, and the same argument on the smaller reduction height gives reducibility of each immediate reduct at $C$. Neutral beta expansion therefore gives $\mathcal R_C(\operatorname{abort}_C(r[\rho]))$. [/step] [step:Apply the fundamental lemma to the identity substitution] Let $\Gamma\vdash t:A$ be any well-typed judgment. The identity substitution $\operatorname{id}_\Gamma$ is reducible by the reducibility of variables. The fundamental lemma gives $\mathcal R_A(t[\operatorname{id}_\Gamma])$. Since $t[\operatorname{id}_\Gamma]=t$, we have $\mathcal R_A(t)$. By the definition of reducibility, $\mathcal R_A(t)$ implies $\mathrm{WN}(t)$. Therefore there is a beta-normal term $n$ with $t\to_\beta^* n$, as required. [/step]