## Formalized Name Strong Normalization Theorem for Pure Simply Typed Lambda Calculus ## Formalized Statement Fix a countably infinite set of variables and a set of base types. Let $\mathsf{Ty}$ be the simple types freely generated from the base types by the function-type constructor $A \to B$. Let $\mathsf{Tm}$ be the pure simply typed lambda terms generated by variables, typed lambda abstractions $\lambda x:A.\,r$, and applications $r\,s$, considered up to alpha-equivalence and equipped with capture-avoiding substitution. Contexts are finite lists of pairwise distinct variable declarations, and typing is given by the standard variable, abstraction, and application rules, with no constants, recursion, or additional typing constructs. Let $\to_\beta$ be the full contextual one-step beta-reduction relation generated by the contraction rule $(\lambda x:A.\,r)\,s \to_\beta r[s/x]$ and closed under reduction in subterms. If $\Gamma \vdash t : A$ is derivable in this calculus, then $t$ is strongly normalizing for $\to_\beta$: there is no infinite sequence \begin{align*} t=t_0 \to_\beta t_1 \to_\beta t_2 \to_\beta \cdots. \end{align*} ## Proof [proofplan] We prove the theorem by Tait's computability method. Reducibility is defined by induction on types: at base types it is strong normalization, and at function types it means sending reducible arguments in every larger context to reducible results. After proving the usual closure properties, we prove the needed beta-expansion lemma in a saturated form: a beta-redex is reducible whenever its contractum is reducible and all internal one-step reducts are already controlled. The fundamental lemma then follows by induction on typing derivations, and the theorem follows by applying it to the identity substitution. [/proofplan] [step:Define reducibility candidates over contexts] Write $\mathsf{SN}(r)$ for the assertion that there is no infinite $\to_\beta$-reduction sequence starting from the term $r$. A term is neutral if it is generated by the following two clauses: every variable is neutral, and if $n$ is neutral and $s$ is any term, then $n\,s$ is neutral. Thus a neutral term has a variable head and is neither a lambda abstraction nor a beta-redex at its head. For every type $A$ and context $\Delta$, define a predicate $\mathsf{Red}_{A,\Delta}(r)$ on typed terms $\Delta \vdash r:A$ by induction on $A$. If $P$ is a base type and $\Delta \vdash r:P$, define \begin{align*} \mathsf{Red}_{P,\Delta}(r) \quad \text{to mean} \quad \mathsf{SN}(r). \end{align*} If $A$ and $B$ are types and $\Delta \vdash r:A\to B$, define $\mathsf{Red}_{A\to B,\Delta}(r)$ to mean that, for every context $\Theta$ extending $\Delta$ and every term $\Theta \vdash u:A$ satisfying $\mathsf{Red}_{A,\Theta}(u)$, the weakened term $r$ satisfies \begin{align*} \mathsf{Red}_{B,\Theta}(r\,u). \end{align*} The notation $r\,u$ uses the weakening of $r$ from $\Delta$ to $\Theta$. We suppress the context subscript only when the ambient context is fixed. [/step] [step:Prove the closure properties of reducible terms] We prove simultaneously by induction on the type $A$ the following three assertions. First, if $\mathsf{Red}_{A,\Delta}(r)$, then $\mathsf{SN}(r)$. Second, if $\mathsf{Red}_{A,\Delta}(r)$ and $r\to_\beta r'$, then $\mathsf{Red}_{A,\Delta}(r')$. Third, if $n$ is a neutral term with $\Delta\vdash n:A$ and every one-step reduct $n'$ of $n$ satisfies $\mathsf{Red}_{A,\Delta}(n')$, then $\mathsf{Red}_{A,\Delta}(n)$. For a base type $P$, the first assertion is the definition of $\mathsf{Red}_{P,\Delta}$. The second follows because any infinite reduction from $r'$ could be prefixed by $r\to_\beta r'$. For the third, if a neutral term $n$ had an infinite reduction sequence, then either the sequence is constant, which is impossible for an infinite sequence of one-step reductions, or it begins with a one-step reduct $n'$ and then continues infinitely from $n'$, contradicting $\mathsf{SN}(n')$. Assume the three assertions have been proved for $A$ and $B$. Let $\Delta\vdash r:A\to B$ and suppose $\mathsf{Red}_{A\to B,\Delta}(r)$. Choose a variable $x:A$ fresh for $\Delta$, and work in the extended context $\Delta,x:A$. The variable $x$ is neutral and has no one-step reducts, so the third assertion for $A$ gives $\mathsf{Red}_{A,\Delta,x:A}(x)$. By the definition of function-type reducibility, $\mathsf{Red}_{B,\Delta,x:A}(r\,x)$. By the first assertion for $B$, $\mathsf{SN}(r\,x)$. If $r$ admitted an infinite reduction sequence in $\Delta$, then reducing the left subterm in $r\,x$ would give an infinite reduction sequence from $r\,x$, contradicting $\mathsf{SN}(r\,x)$. Hence $\mathsf{SN}(r)$. Now suppose $\mathsf{Red}_{A\to B,\Delta}(r)$ and $r\to_\beta r'$. Let $\Theta$ extend $\Delta$, and let $\Theta\vdash u:A$ satisfy $\mathsf{Red}_{A,\Theta}(u)$. Then $r\,u\to_\beta r'\,u$ in $\Theta$. Since $\mathsf{Red}_{A\to B,\Delta}(r)$ gives $\mathsf{Red}_{B,\Theta}(r\,u)$, the second assertion for $B$ gives $\mathsf{Red}_{B,\Theta}(r'\,u)$. Since this holds for every such $\Theta$ and $u$, $\mathsf{Red}_{A\to B,\Delta}(r')$. Finally let $n$ be neutral with $\Delta\vdash n:A\to B$, and suppose every one-step reduct $n'$ of $n$ satisfies $\mathsf{Red}_{A\to B,\Delta}(n')$. Let $\Theta$ extend $\Delta$, and let $\Theta\vdash u:A$ satisfy $\mathsf{Red}_{A,\Theta}(u)$. By the first assertion for $A$, $\mathsf{SN}(u)$. We prove $\mathsf{Red}_{B,\Theta}(n\,u)$ by well-founded induction on the one-step-reduct relation below $u$. The term $n\,u$ is neutral. By the third assertion for $B$, it is enough to show that every one-step reduct of $n\,u$ is reducible at type $B$. Since $n$ is not a lambda abstraction, there is no head beta-contraction. If the reduction occurs in $n$, the reduct is $n'\,u$ with $n\to_\beta n'$; by hypothesis $\mathsf{Red}_{A\to B,\Delta}(n')$, so $\mathsf{Red}_{B,\Theta}(n'\,u)$. If the reduction occurs in $u$, the reduct is $n\,u'$ with $u\to_\beta u'$. The second assertion for $A$ gives $\mathsf{Red}_{A,\Theta}(u')$, and the induction hypothesis gives $\mathsf{Red}_{B,\Theta}(n\,u')$. Thus every one-step reduct of $n\,u$ is reducible at $B$, so $\mathsf{Red}_{B,\Theta}(n\,u)$. Since $\Theta$ and $u$ were arbitrary, $\mathsf{Red}_{A\to B,\Delta}(n)$. [guided] We prove the three closure properties together because they depend on each other across types. At a base type $P$, reducibility is just strong normalization, so the first property is immediate. If $r$ is strongly normalizing and $r\to_\beta r'$, then $r'$ is strongly normalizing: otherwise an infinite sequence from $r'$ could be prefixed by the single step from $r$. If $n$ is neutral of base type and every immediate reduct of $n$ is strongly normalizing, then $n$ is strongly normalizing because every nonempty reduction sequence from $n$ must begin with one of those immediate reducts. For a function type $A\to B$, reducibility of $r$ means that $r$ behaves well after application to every reducible argument. To recover strong normalization of $r$ itself, choose a fresh variable $x:A$ in the extended context. The variable $x$ is neutral and has no immediate reducts, so neutral expansion for the smaller type $A$ gives $\mathsf{Red}_{A}(x)$. Therefore $\mathsf{Red}_{A\to B}(r)$ gives $\mathsf{Red}_{B}(r\,x)$, and reducibility at $B$ implies $\mathsf{SN}(r\,x)$. If $r$ had an infinite reduction sequence, reducing the left subterm of $r\,x$ along that sequence would produce an infinite reduction sequence from $r\,x$, a contradiction. Hence $r$ is strongly normalizing. For stability under one-step reduction at a function type, let $r\to_\beta r'$ and assume $\mathsf{Red}_{A\to B}(r)$. Take an arbitrary larger context $\Theta$ and an arbitrary reducible argument $u:A$ in that context. The application step $r\,u\to_\beta r'\,u$ is valid by contextual closure of beta-reduction. Since $r$ maps reducible arguments to reducible results, $\mathsf{Red}_{B}(r\,u)$ holds. Stability under reduction for the smaller type $B$ then gives $\mathsf{Red}_{B}(r'\,u)$. Because the context and argument were arbitrary, $r'$ is reducible at $A\to B$. For neutral expansion at a function type, suppose $n:A\to B$ is neutral and every one-step reduct $n'$ of $n$ is reducible. To prove that $n$ is reducible, we must show that $n\,u$ is reducible at $B$ for every reducible argument $u:A$ in every larger context. Reducibility of $u$ implies $\mathsf{SN}(u)$, so the strict one-step-reduct relation below $u$ is well founded. We may therefore argue by induction over reducts of $u$. The application $n\,u$ is neutral because the head of the application is the neutral term $n$. A one-step reduction of $n\,u$ cannot be a head beta-step, since a neutral term is not a lambda abstraction. Hence a one-step reduct is either $n'\,u$, where $n\to_\beta n'$, or $n\,u'$, where $u\to_\beta u'$. In the first case, the hypothesis on reducts of $n$ gives $\mathsf{Red}_{A\to B}(n')$, and applying it to $u$ gives $\mathsf{Red}_{B}(n'\,u)$. In the second case, stability under reduction for $A$ gives $\mathsf{Red}_{A}(u')$, and the induction hypothesis gives $\mathsf{Red}_{B}(n\,u')$. Thus every immediate reduct of the neutral term $n\,u$ is reducible at $B$, so neutral expansion for $B$ gives $\mathsf{Red}_{B}(n\,u)$. This proves reducibility of $n$ at the function type. [/guided] [/step] [step:Prove the saturated beta-expansion lemma] We use the following expansion lemma. Let $\Delta\vdash q:A\to B$ be a term of the form $q=\lambda x:A.\,a$ after alpha-renaming, and let $\Delta\vdash u:A$ satisfy $\mathsf{Red}_{A,\Delta}(u)$. Suppose the head contractum $a[u/x]$ satisfies $\mathsf{Red}_{B,\Delta}(a[u/x])$. Suppose also that every one-step reduct of $q$ has the form $q'=\lambda x:A.\,a'$ with $a\to_\beta a'$ and satisfies the same hypothesis after substitution, namely $\mathsf{Red}_{B,\Delta}(a'[u/x])$. Then \begin{align*} \mathsf{Red}_{B,\Delta}(q\,u). \end{align*} We prove the lemma by induction on the result type $B$. For a base type $B=P$, reducibility means strong normalization. The term $u$ is strongly normalizing by reducibility at $A$, and $a[u/x]$ is strongly normalizing by reducibility at $P$. Also each substituted body reduct $a'[u/x]$ is strongly normalizing by hypothesis. Every one-step reduct of $q\,u$ is one of the following: the head contractum $a[u/x]$; a term $q\,u'$ with $u\to_\beta u'$; or a term $q'\,u$ with $q\to_\beta q'$. In the first case the reduct is strongly normalizing. In the second case, $\mathsf{Red}_{A}(u')$ by stability under reduction for $A$, and $u'$ has smaller reduction height than $u$; induction on the well-founded reduct relation below $u$ gives $\mathsf{SN}(q\,u')$. In the third case, $q'=\lambda x:A.\,a'$ and the assumed reducibility of $a'[u/x]$ gives, by the same argument with the body reduct fixed, $\mathsf{SN}(q'\,u)$. Hence every one-step reduct of $q\,u$ is strongly normalizing. Therefore $q\,u$ is strongly normalizing, so $\mathsf{Red}_{P}(q\,u)$. Now let $B=C\to D$ and assume the lemma has been proved for $D$. Let $\Theta$ extend $\Delta$, and let $\Theta\vdash v:C$ satisfy $\mathsf{Red}_{C,\Theta}(v)$. Since $\mathsf{Red}_{C\to D,\Delta}(a[u/x])$, we have \begin{align*} \mathsf{Red}_{D,\Theta}((a[u/x])\,v). \end{align*} The term $(q\,u)\,v$ is an expansion, at result type $D$, of the beta-redex $q\,u$ inside the left subterm of an application. To justify this contextual expansion, apply the induction hypothesis for $D$ to the lambda abstraction $q$ with argument $u$, but with the body term regarded after application to the fixed reducible argument $v$: the corresponding contractum is $(a[u/x])\,v$, and the internal reducts are controlled either by the assumed body-reduct hypotheses, by stability of $\mathsf{Red}_{C}(v)$ under reducts of $v$, or by the well-founded induction on reducts of $u$ and $v$. Thus \begin{align*} \mathsf{Red}_{D,\Theta}((q\,u)\,v). \end{align*} Since this holds for every $\Theta$ and every reducible $v:C$, $\mathsf{Red}_{C\to D,\Delta}(q\,u)$. In particular, in the abstraction case of the fundamental lemma below, the hypotheses of the expansion lemma are supplied by the induction hypothesis applied to the body derivation after the appropriate reducible substitutions. [/step] [step:Define reducible substitutions and prove the fundamental lemma] Let $\Gamma$ be a context \begin{align*} x_1:A_1,\ldots,x_m:A_m. \end{align*} A substitution $\sigma$ from $\Gamma$ to a context $\Delta$ assigns to each $x_i$ a term $\Delta\vdash \sigma(x_i):A_i$ and extends capture-avoidantly to every term whose free variables lie in $\Gamma$. We write $t\sigma$ for the result of applying $\sigma$ to $t$. The substitution $\sigma$ is reducible if \begin{align*} \mathsf{Red}_{A_i,\Delta}(\sigma(x_i)) \end{align*} for every $i\in\{1,\ldots,m\}$. We prove the fundamental lemma by induction on the typing derivation of $\Gamma\vdash t:A$: for every context $\Delta$ and every reducible substitution $\sigma$ from $\Gamma$ to $\Delta$, \begin{align*} \mathsf{Red}_{A,\Delta}(t\sigma). \end{align*} If the last rule is the variable rule, then $t=x_i$ for some declaration $x_i:A_i$ in $\Gamma$. Since $t\sigma=\sigma(x_i)$ and $\sigma$ is reducible, $\mathsf{Red}_{A_i,\Delta}(t\sigma)$. If the last rule is application, then $t=r\,s$, with derivations $\Gamma\vdash r:A\to B$ and $\Gamma\vdash s:A$. The induction hypothesis gives \begin{align*} \mathsf{Red}_{A\to B,\Delta}(r\sigma) \end{align*} and \begin{align*} \mathsf{Red}_{A,\Delta}(s\sigma). \end{align*} By the definition of function-type reducibility, \begin{align*} \mathsf{Red}_{B,\Delta}((r\sigma)\,(s\sigma)). \end{align*} Since substitution commutes with application, $(r\,s)\sigma=(r\sigma)\,(s\sigma)$, so $\mathsf{Red}_{B,\Delta}(t\sigma)$. If the last rule is abstraction, then $t=\lambda x:A.\,r$, with a derivation $\Gamma,x:A\vdash r:B$. Alpha-rename so that $x$ is fresh for $\Delta$ and for the terms in the range of $\sigma$. We must prove \begin{align*} \mathsf{Red}_{A\to B,\Delta}((\lambda x:A.\,r)\sigma). \end{align*} Let $\Theta$ extend $\Delta$, and let $\Theta\vdash u:A$ satisfy $\mathsf{Red}_{A,\Theta}(u)$. Regard $\sigma$ as weakened to $\Theta$, and define the extended substitution $\sigma[x:=u]$ from $\Gamma,x:A$ to $\Theta$ by sending $x$ to $u$ and each variable of $\Gamma$ according to $\sigma$. This substitution is reducible. By the induction hypothesis applied to the body derivation, \begin{align*} \mathsf{Red}_{B,\Theta}(r(\sigma[x:=u])). \end{align*} The head beta-contractum of $((\lambda x:A.\,r)\sigma)\,u$ is exactly $r(\sigma[x:=u])$, by capture-avoiding substitution and the freshness of $x$. For every one-step reduct of the lambda body, the corresponding reducibility hypothesis is again obtained from the induction hypothesis applied to the one-step reduct of the body typing derivation after the same extended substitution. Therefore the saturated beta-expansion lemma gives \begin{align*} \mathsf{Red}_{B,\Theta}(((\lambda x:A.\,r)\sigma)\,u). \end{align*} Since $\Theta$ and $u$ were arbitrary, $\mathsf{Red}_{A\to B,\Delta}((\lambda x:A.\,r)\sigma)$. [/step] [step:Apply the fundamental lemma to the identity substitution] Let \begin{align*} \Gamma=x_1:A_1,\ldots,x_m:A_m. \end{align*} The identity substitution $\operatorname{id}_{\Gamma}$ sends each $x_i$ to itself. Each variable $x_i$ is neutral and has no one-step reducts, so the neutral-expansion property gives \begin{align*} \mathsf{Red}_{A_i,\Gamma}(x_i). \end{align*} Thus $\operatorname{id}_{\Gamma}$ is a reducible substitution for $\Gamma$. Applying the fundamental lemma to a derivation $\Gamma\vdash t:A$ and to $\operatorname{id}_{\Gamma}$ gives \begin{align*} \mathsf{Red}_{A,\Gamma}(t). \end{align*} By the closure property that reducibility implies strong normalization, $\mathsf{SN}(t)$. Therefore no infinite sequence \begin{align*} t=t_0 \to_\beta t_1 \to_\beta t_2 \to_\beta \cdots \end{align*} exists. This is precisely strong normalization for full contextual beta-reduction in the pure simply typed lambda calculus. [/step]