normalization.tex

\section{Strong normalization}
\subsection{Evaluation in the empty context}
In \autoref{sec:church_rosser}, we set up a reduction relation $\rightsquigarrow_\kappa$ which is plainly useless for a normalization algorithm, because of the following rule:
$$(K^+)\ \frac{P\mbox{ is SS inductive}\quad\Gamma\vdash \intro\;\inv[p,h]:\alpha}{\Gamma\vdash \rec_P\;C\;e\;p\;h\rightsquigarrow_\kappa e\;\inv[p,h]\;v}$$
Recall that $v$ is a sequence of lambdas $v_i=\lambda x::\xi_i.\;\rec_P(C,e,\pi_i[\inv[p,h],x],u_i\;x)$. That is, we reduce any $\rec_P$ term, regardless of its arguments, to a longer expression that contains another $\rec_P$ term (assuming that the inductive type has a recursive argument). If the embedded $\rec_P$ term in $v$ is also susceptible to the $K^+$ reduction (which is quite often the case), then this will not terminate, but it was sufficiently powerful to act as a semi-decision procedure for definitional equality where existing methods fail (by giving up early, they recover decidability at the cost of completeness).

Let us scale back the $K^+$ rule, then, to the original $K$ rule, which is the same as $K^+$ except that it only applies if no $\inv_i$ terms are produced on the RHS. We will also reinstate the standard $\iota$ rule for subsingleton inductives as well. We will call the resulting reduction relation $\rightsquigarrow_\sigma$.

$$\boxed{\Gamma\vdash e\rightsquigarrow_\sigma e'}\qquad
\frac{\Gamma\vdash e_1 \rightsquigarrow_\sigma e_1'}{\Gamma\vdash e_1\;e_2\rightsquigarrow_\sigma e_1'\;e_2}\qquad
\frac{\Gamma\vdash e_2 \rightsquigarrow_\sigma e_2'}{\Gamma\vdash e_1\;e_2\rightsquigarrow_\sigma e_1\;e_2'}$$
$$\frac{\Gamma\vdash \alpha \rightsquigarrow_\sigma\alpha'}{\Gamma\vdash \lambda x:\alpha.\;e\rightsquigarrow_\sigma \lambda x:\alpha'.\;e}\qquad
\frac{\Gamma,x:\alpha\vdash e \rightsquigarrow_\sigma e'}{\Gamma\vdash \lambda x:\alpha.\;e\rightsquigarrow_\sigma \lambda x:\alpha.\;e'}\qquad\dots$$
$$(\beta)\ \frac{}{\Gamma\vdash (\lambda x:\alpha.\;e)\;e'\rightsquigarrow_\sigma e[e'/x]}\qquad
(\delta)\ \frac{\mathsf{def}\;c:\alpha:=e}{\Gamma\vdash c\rightsquigarrow_\sigma e}\qquad
(\zeta)\ \frac{}{\Gamma\vdash \elet{x:\alpha:=e'}{e}\rightsquigarrow_\sigma e[e'/x]}$$
$$(\iota)\ \frac{P\mbox{ is inductive with ctor }c}{\Gamma\vdash \rec_P\;C\;e\;p\;(c\;b)\rightsquigarrow_\sigma e_c\;b\;v}\qquad
(\iota_q)\ \frac{}{\Gamma\vdash \lift\;R\;f\;h\;(\mk_R\;a)\rightsquigarrow_\sigma f\;a}$$
$$(K)\ \frac{P\mbox{ is SS inductive}\quad\inv_i\notin\inv[p]\quad\Gamma\vdash \intro\;\inv[p]:\alpha}{\Gamma\vdash \rec_P\;C\;e\;p\;h\rightsquigarrow_\sigma e\;\inv[p]\;v}$$

We have indicated that $\inv$ consists only of $p_i$ terms and not $\inv_i\;h$ by the notation $\inv_i\notin\inv[p]$.

UNFINISHED