chap-norm.tex

\chapter{Normalization}\label{chap:normalization}

In Chapter~\ref{chap:binders}, we discussed the Simply Typed Lambda
Calculus (STLC), its grammar, operational semantics and typing
judgement.  In addition, we studied some meta-theoretic properties of
this formalism such as type preservation, the fact that type is
preserved under evaluation of the operational semantics, and type
uniqueness, the fact that each well-typed term has only one type. In
this chapter we will explore another meta-theoretical property,
normalization --i.e., the evaluation of well-typed terms always
terminates. We proved earlier in Section \ref{sec:termination}
termination of evaluation for a simple language containing arithmetic
and booleans. This proof was straightforward by structural induction
on the typing derivation. Unfortunately, proving this property for the
simply typed lambda-calculus is more challenging. A direct proof via
structural induction fails. Instead, we fall back to a technique
called proofs by logical relations going back to Tait  \cite{Tait67}
and was later refined by Girard
\citep{GirardLafontTaylor:proofsAndTypes}. The central idea of logical
relations is to specify relations on well-typed terms via structural
induction on the syntax of types instead of directly on the syntax of
terms themselves. Thus, for instance, logically related functions take
logically related arguments to related results, while  logically
related pairs consist of components that are related pairwise.

Mechanizing logical relations proofs is challenging: first, specifying logical relations themselves typically requires a logic which allows arbitrary nesting of quantification and implications; second, to establish soundness of a logical relation, one must prove the Fundamental Property which says that any well-typed term under a closing simultaneous substitution is in the relation. This latter part requires some notion of simultaneous substitution together with the appropriate equational theory of composing substitutions. As Altenkirch \cite{Altenkirch:TLCA93} remarked,

\begin{quote}
``I discovered that the core part of the proof (here proving lemmas about CR) is fairly straightforward and only requires a good understanding of the paper version. However, in completing the proof I observed that in certain places I had to invest much more work than expected, e.g. proving lemmas about substitution and weakening.''
\end{quote}

While logical normalization proofs often are not large, they are
conceptually intricate and mechanizing them has become a challenging
benchmark for proof environments. In \beluga, this proof and similar
logical relations proofs can be implemented concisely. In developing
this kind of proof in \beluga, we introduce several new ideas:

\begin{itemize}
\item We will start by revisiting well-typed lambda-terms together with a
simple call-by-name semantics and show an intrinsically.

\item Using inductive definitions to define reducibility candidates
  and other properties of derivations and contexts

\item Using first-class substitution variables

\end{itemize}


\section{Representing Well-Typed Terms}

Let's revisit the definition of STLC, starting with the grammar of terms, values and types:

\[
\begin{array}{ll@{\bnfas}l}
\mbox{Terms} & M, N & x \bnfalt \lam x.M \bnfalt M \app N \bnfalt c\\
\mbox{Types} & T, S & B \bnfalt T \arrow S\\
\mbox{Values} & V & \lam x.M \bnfalt c
\end{array}
\]

Please note that in this presentation, we added to the language base
type and a constant term.

Then we define the small-step operational semantics. In this
particular presentation we use rules are different to
Chapter~\ref{chap:binders}. This presentation corresponds to what is
typically referred to as a Call-By-Name operational semantics.

\[
\begin{array}{c}
\multicolumn{1}{l}{\fbox{$M \Steps M'$}~~ \mbox{Term $M$ steps to term $M'$}}
\\[1em]
\infer[\EAppBeta]{(\lam x.M) \app N \Steps [N/x]M}{} \qquad
\infer[\EAppArgStep]{M \app N \Steps M'\;N}{M \Steps M'} \quad
% \infer[\EAppFnStep]{V \app N \Steps V\;N'}{N \Steps N' & V \Value}
\\[1em]
\multicolumn{1}{l}{\fbox{$M \MSteps M'$}~~ \mbox{Term $M$ steps in
    multiple steps to term $M'$}}\\[1em]
\infer[\MRef]{M \MSteps M}{} \qquad
\infer[\MOne]{M \MSteps M'}{M \Steps N & N \MSteps M'} 
\end{array}
\]


Finally, we define the typing judgement. Note that we added the rule
\TBase for constants of base type.

\[
\begin{array}{c}
\multicolumn{1}{l}{\mbox{\fbox{$M:T$}~~ \mbox{Term $M$ has type $T$}}} \\[1em]
\infer[\TFn^{x,u}]{\lam x.M : T \arrow S}
                 {\infer*{M:S}{\infer[u]{x:T}{}}} \qquad
\infer[\TApp]{M\;N : S}{M : T \arrow S & N:T} \qquad
\infer[\TBase]{c : B}{}
\end{array}
\]

In Chapter~\ref{chap:binders}, the formalization in Beluga followed
very closely the paper presentation, in this case we will take a
slightly different approach in which we combine the syntax of terms
and the typing rules to obtain and \emph{intrinsically typed
  representation} of the language.

%\begin{extract}[norm.bel]
\begin{lstlisting}
LF tp : type =
| b :  tp
| arr : tp -> tp -> tp
;

LF tm : tp -> type =
| app : tm (arr T S) -> tm T -> tm S
| lam : (tm T -> tm S) -> tm (arr T S)
| c : tm b
;
\end{lstlisting}
%\end{extract}

The type family \bel{tm} defines simply-typed lambda terms by 
indexing \bel{tm} by the type \bel{tp}, the type of a term. In typical higher-order
abstract syntax (HOAS) fashion, lambda abstraction takes a function
representing the abstraction of a term over a variable. There is no
case for variables, as they are treated implicitly in HOAS.

We now encode the step relation of the operational semantics. In
particular, we create the \bel{step} type indexed by two well-typed terms that
represent each step of the computation. Hence our stepping relation is
intrinsically type-preserving. 

\begin{lstlisting}
LF step : tm A -> tm A -> type =
| beta    : step (app (lam M) N) (M N)
| stepapp : step M M' -> step (app M N) (app M' N)
;

LF mstep : tm A -> tm A -> type = 
| refl   : mstep M M
| onestep: step M N -> mstep N M' -> mstep M M'
;
\end{lstlisting}

Notice again how the \bel{beta} rule re-uses the LF notion of substitution by
computing the application of \bel{M} to \bel{N}.

Finally, we define values using the type family \bel{val} and a predicate \bel{halts} to encode that a term halts if it steps into a value.

\begin{lstlisting}
LF val : tm A -> type =
| val_c : val c
| val_lam : val (lam M)
;
\end{lstlisting}

To characterize values, instead of directly implementing the grammar
of values, we define a predicate on well-typed terms that selects the
values.

\begin{lstlisting}
LF halts : tm A -> type =
| halts_m : mstep M M' -> val M' -> halts M
;
\end{lstlisting}

Finally, a term \bel{M} halts (i.e. \bel{halts M}), if it eventually
step to a value. 
Thhe normalization proof will establish that for all terms \bel{M}, 
\bel{M halts}. At
this point, one might be tempted to prove this property by induction on the
structure of terms as we did in Section \ref{sec:termination} for a
language containing booleans and numbers. However, the na\"if direct approach
fails when we consider functions and function application. As we
reduce well-typed terms, we cannot guarantee that their size is
decreasing. We hence take a different approach.
\improvement{Perhaps one could add an exercise as in TAPL for this}

\section{Inductive and Stratified Definitions}
Instead of proving directly that the evaluation of well-typed terms
terminates on the size of terms, we characterize abstractly terms that
are reducible at a given type (written as $\rc A M$). We then prove
that evaluation of well-typed terms halts in two steps:

\begin{enumerate}
\item All well-typed terms are reducible. 
\item If a term is reducible, it will halt.
\end{enumerate}

We will be careful to define reducibility such that the second part of
this argument becomes trivial; proving the first part is more
challenging. 

The key insight in defining what it means for a term to be reducible
is to define it not on the size of the term which may in fact grow,
but on the type of the term. This will give us a strong enough
induction hypothesis for proving part 1. 

We define the \emph{Reducibility Candidates} predicate as:

\begin{itemize}
\item \rc B M iff $M$ halts
\item \rc{T\arrow S} M iff $M$ halts and for all $N$, if \rc {T} N then \rc{S}{M\app N}
\end{itemize}

The definitions states that a term of base type is in the relation if
it halts, and a term of function type is reducible when it halts and it is well
behaved under application. The general idea of the proof is to show
that the terms in \rc{T}{M} have the desired property. In our case the desired
property is that the evaluation of the term halts, and it straight
forward to show that if a term is reducible then its evaluation halts.

Reducibility cannot be directly encoded at the LF layer, since the
universal quantifier and implication in the definition of $\rc{T
  \arrow S} M$ are not merely describing a hypothetical and parametric
derivation. The definition is a statement in first-order logic! It
states an inductive property about terms which we should be able to prove
(possibly by induction). We often say it involves a strong implication
or strong computational function space vs the weak implication
(function space) LF provides. Hence we revisit to the
computation layer of \beluga. So far, the power of \beluga's language
corresponds to first-order logic. Here we now exploit the power of
defining inductive properties about our domain. This corresponds to
adding fix-points to our logic. From a programmers point of view, it
corresponds to adding the power of indexed recursive data types which
can be used to define properties and relations about contexts and
contextual objects. Here we define a relation \bel{Reduce} between
types \bel{A} and terms \bel{M} that corresponds to our reducibility
candidates $\rc A M$. We declare the kind of \bel{Reduce} as using the
keyword \bel{ctype} which distinguishes this definition from LF types
families. Computation-level type families such as \bel{Reduce} are
indexed by contexts and contextual objects which are embedded into
computation-level types and programs are written inside \bel{[ ]} (see
\cite{Cave:POPL12}). 


\begin{lstlisting}
stratified Reduce : {A:[|- tp]}{M:[|- tm A]} ctype =
| Rb : [|- halts M] -> Reduce [|- b ] [|- M]
| Rarr :  [|- halts M] ->
    ({N:[|- tm A]} Reduce [|- A ] [|- N] -> Reduce [|- B ] [|- app M N])
    -> Reduce [|- arr A B ] [|- M]
;
\end{lstlisting}


A term of base type \bel{b} is reducible if it halts, and a \bel{term M} of type
\bel{arr A B} is reducible if it halts, and moreover for every reducible
\bel{N} of type \bel{A}, the application \bel{app M N} is reducible. We write
\lstinline!{N:[|-tm A]}! for explicit $\Pi$-quantification over \bel{N}, a closed term
of type \bel{A}. To the left of the turnstile in \bel{[|- tm A]} is where one
writes the context the term is defined in -- in this case, it is empty.


Adding inductive definitions to a language is non-trivial and may
jeopardize is consistency. In \beluga there are two forms: stratified
definitions, as the definition of \bel{Reduce}, and inductive definitions.
What is this difference between LF types on the one hand and inductive and
stratified types on the other? - To understand these differences it is
worthwhile looking at some simpler examples.

We might be tempted to give an inductive
definition of \texttt{Tm} as follows

\begin{lstlisting}
inductive Tm : ctype =
| Lam : (Tm -> Tm) -> Tm;
\end{lstlisting}

On the surface, the function space \verb+Tm -> Tm+
is a strong function space; we cannot match and inspect the structure
of this function as we are able with the LF function space that we
used to define abstractions. We can only observe the behavior of
computation. However, there is a deeper problem which is best
illustrated with a slightly simpler example:

\begin{lstlisting}
inductive D : ctype = 
| Inj : (D -> D) -> D;

rec out : D -> (D -> D) = 
fn x => case x of Inj f =>  f;

let omega  : D = Inj (fn x -> (out x) x);
let omega' : D = (out omega) omega ; 
\end{lstlisting}

The definition of \verb+D+ seems sensible at first; but we can
cleverly create a non-terminating computation \verb+omega'+ that
will keep on reproducing itself. The problem is the negative occurrence
in the definition \verb+D+. 

To avoid such issues we commonly state that inductive definitions must
satisfy the positivity restriction, i.e. the type we are defining
cannot be used the the left hand side of an arrow. 

What is then a stratified type? - Clearly our definition of
\bel{Reduce} is not inductive as we have an occurrence in a negative
position in 

\begin{lstlisting}
 ({N:[|- tm A]} Reduce [|- A ] [|- N] -> Reduce [|- B ] [|- app M N])  
\end{lstlisting}


However, we observe that every computation we would be able to
construct of this type has the property that the input to that
computation is smaller when we concentrate on the first index
describing the type, i.e. \lstinline![|- A]! is smaller than
\lstinline![|- arr A B]!. While we still can never
pattern match on this function to inspect its shape and we can never
recurse on this definition directly, we can recurse on the index
\lstinline!A! instead. 


% In this definition, the arrows represent the usual computational
% function space, not the weak function space of LF. We note that this
% definition is not (strictly) positive, since \bel{Reduce} appears to the
% left of an arrow in the \bel{Rarr} case. Allowing unrestricted such
% definitions destroys the soundness of our system. Here we note that
% this definition is stratified by the type: the recursive occurrences
% of \bel{Reduce} are at types \bel{A} and \bel{B} which are smaller than \bel{arr A B}.
% \bel{Reduce} is defined by induction on the type of the reducible
% term(additionally this is why we cannot leave the type implicit).


\section{Normalization Proof}
\subsection{Auxiliary Lemma}
With the main definitions in place we now prove some more or less trivial lemmas that are
sometimes omitted in paper presentations.First, we state and prove a
simple lemma which stats that halts is closed under single step expansion.

\begin{lemma}[]
If $\proofderiv{\S}{M \Steps M'}$ and $M'$ halts then $M$ halts.
\end{lemma}

The proof is straightforward. As $M'$ halts, we have a value $V$ and a
derivation $\proofderiv{\S'}{M' \MSteps V}$. By using the rule $\MOne$ together with
$\S$ and $\S'$ we have a witness for $M \MSteps V$ which shows that $M$ halts.
This can be encoded directly in \beluga.

\begin{lstlisting}
rec halts_step : {S:[|- step M M']} [|- halts M'] -> [|- halts M] =
mlam S => fn h =>
let [|- halts_m MS' V] = h in
 [|- halts_m (onestep S MS') V]
;
\end{lstlisting}

Next we prove closure of reducibility candidates under expansion. 

  \begin{lemma}[Backward closed]
   If $M \Steps M'$ and $\rc T {M'}$ then $\rc T M$.    
  \end{lemma}

The proof is by induction on the type $T$. In the base case we appeal to \bel{halts_step}, while in the \bel{Rarr} case
we must also appeal to the induction hypothesis at the range type,
going inside the function position of applications.

\begin{lstlisting}
rec bwd_closed' : {T:[|- tp]}{M:[|- tm T]}{M':[|- tm T]}{S:[ |- step M M']} Reduce [|- T] [ |- M'] -> Reduce [|- T] [ |- M] =
/ total a (bwd_closed' a) /
 mlam T, M, M' => mlam SS => fn r => case [|- T] of 
| [|- b] => let I ha = r in I (halts_step [ |- SS] ha)
| [|- arr T S] => 
  let Arr ha f = r in
    Arr (halts_step [ |- MS] ha)
	(mlam N => fn rn =>
	 bwd_closed' [|- S] [|- _ ] [|- _ ] [ |- stepapp MS] (f [ |- N] rn))
;

rec bwd_closed : {S:[ |- step M M']} Reduce [|- T] [ |- M'] -> Reduce [|- T] [ |- M] = 
/ total (bwd_closed) /
mlam S => fn r => 
let [|- S] : [|- step M M'] = [|- S] in 
let [|- M] : [|- tm T]    = [|- M] in
  bwd_closed' [|- T] [|- M ] [|- M' ]  [|- S] r;
\end{lstlisting}

\todo{Add informal proof and provide more explanation to this function
-bp}

The trivial fact that reducible terms halt has a corresponding
trivial proof, analyzing the construction of the the proof of
\bel{Reduce[|- T] [|- M]}.

Finally we prove that that if a term $M$ is reducible at type $T$ then
it halts.

\begin{lemma}
If $\rc T M$ then $M$ halts.  
\end{lemma}
The proof is trivial and follows directly from the definition of $\rc
T M$. This can be translated direct into \beluga as follows.

\begin{lstlisting}
rec reduce_halts : Reduce [|- T] [|- M] -> [|- halts M] =
fn r => case r of
| Rb h => h
| Rarr h f => h
;
\end{lstlisting}

It is at this point, that we may start thinking on the proof of the
main theorem. The main theorem states that all terms are reducible, so
a first approximation to this could be to try to prove this theorem:

\begin{lstlisting}
rec main : {M:[|- tm A]} Reduce [|- A] [|- M] =
  ?
;
\end{lstlisting}

However, if we try to prove this theorem, we very quickly realize that
we need to have appeals to the induction hypothesis for open term. In
particular, when trying to build the reducibility candidate for
$\lambda$-terms. We hence need to generalize this statement.

\subsection{Fundamental Lemma and Main Theorem}
% \subsection{Reducibility of substitutions}
It is worthwhile to revisit the proof of the fundamental lemma on
paper. The right generalization is often stated as follows:


\begin{lemma}[Main lemma]
If $\D:\Gamma \vdash M : T$ and $\rc {\Gamma}{\sigma}$ then
$\rc T {[\sigma]M}$ where $\rc {\Gamma}{\sigma}$ is defined as:

\begin{itemize}
\item $\rc \cdot \cdot$ (i.e. empty substitutions are reducible at the
  empty context)
\item $\rc {\Gamma, x:T} {\sigma, N/x}$ iff $\rc \Gamma \sigma$ and  $\rc T N$
\end{itemize}
 % \[
 % \begin{array}{c}
 % \infer{\rc \cdot \cdot }{} \qquad \qquad
 % \infer{\rc {\Gamma, x:T} {\sigma, N/x}}
 % {\rc \Gamma \sigma & \rc T N }
 % \end{array}
 % \]
\end{lemma}

\begin{proof} By structural induction on the typing derivation $\D$.
\\[0.5em]
\noindent
\textbf{Case}  ${\mathcal{D}}=\begin{array}{l}\infer[lam]{\Gamma \vdash \mathsf{lam}~ x.M : T \arrow
    S}{
    \begin{array}{c}
      {\mathcal{D}}_1\\
      \Gamma,x{:}T \vdash M : S
    \end{array}
}\end{array}$
\\[0.5em]
$[\sigma](\mathsf{lam}~x.M) = \mathsf{lam}~ x.([\sigma,x/x]M)$ \hfill 
by \emphFact{properties of substitution} \\
$\mathsf{lam}~ x.[\sigma,x/x]M$ halts \hfill since it is a value\\
Suppose $\rc T N$.
\begin{enumerate}
\item $\rc S {[\sigma,N/x]M}$ \hfill by I.H. on ${\mathcal{D}}_1$ since $\rc {\Gamma}{\sigma}$
\item $\rc S {[N/x][\sigma,x/x]M}$ \hfill by \emphFact{properties of
  substitution}
\item $\rc S {\mathsf{app}~(\mathsf{lam}~ x.~[\sigma,x/x]M)\; N}$ \hfill by Backwards closure
\end{enumerate}
Hence $\rc {T \arrow S}{[\sigma]\mathsf{lam}~ x.M}$ \hfill by definition

\end{proof}

In the proof we spelled out explicitly where we rely on substitution properites
such as composition of substitution and associativity. This highlights
the important and often hidden role substitutions play. In \beluga,
where we have first-class simultaneous substitutions together with their
equational theory, the uses of such substitution properties will be
silently taken care of. This in turn leads to a very elegant and
compact encoding of the fundamental lemma as it only reflects the main
structure of the proof.

As the statement talks about open terms, i.e. terms in a context
$\Gamma$, we first define a context schema that classifies contexts
containg typing assumptions about variables. 

\begin{lstlisting}
schema ctx = tm T;
\end{lstlisting}

In the statement of the fundamental lemma, we also relied on the
concept of \emph{grounding substitutions}. This is again  
natively supported in \beluga using first-class substitutions that
provide a mapping from $\Gamma$ to an empty context. Finally,  we need to define what it means for a
substitution to be \emph{reducible}. In particular, a \emph{a
  reducible substitution} is a substitution where all the terms that
compose it are also reducible. We define that, using an inductive
data-type indexed by grounding substitutions. In the code below we
pretty print the composition of the substitution $\sigma$ with the
empty substitution (written as \bel{^}) by simply writing $\sigma$. 

\begin{lstlisting}
inductive Red_sub : {\gamma:ctx}{\sigma:[|- \gamma]} ctype =
| Nil : Red_sub  [ ] [|- ^ ]
| Dot : Red_sub  [\gamma] [|- \sigma ] -> Reduce [|- T] [|- M]
     -> Red_sub [\gamma, x:tm T[]] [|- \sigma,M ]
;

rec lookup : {\gamma:ctx}{#p:[\gamma |- tm T[]]}Red_sub [\gamma] [|- \sigma] ->
             Reduce [|- T] [|- #p[\sigma]] =
mlam \gamma=> mlam #p => fn rs => case [\gamma] of 
| [] => impossible [ |- #p]
| [\gamma', x:tm T] => (case [\gamma', x:tm T |- #p] of
 | [\gamma',x:tm T |-  x] =>    let (Dot rs' rN) = rs in rN
 | [\gamma',x:tm T |-  #q[..]] => let Dot rs' rN = rs in
                      lookup [\gamma'] [\gamma' |- #q] rs')
;
\end{lstlisting}

Recall all meta-variables are associated with substitutions, but we
are able to omit writing that substitution, if it is the identity substitution. The same
holds for substitution variables. They are associated with a
delayed substitution which intuitively represent a delayed composition of
a substitution variable with that substitution. If the substitution
variable is associated with the identity substitution or a trivial
empty substitution (i.e. from the empty context to another empty
context), we omit writing it. In other words we write simply $\sigma$
for $\sigma[..]$ (i.e. the composition of $\sigma$ with the identity
substitution) and $\sigma[^]$ (i.e. the composition of $\sigma$ with
the trivial empty substitution)\footnote{In ASCII we write \bel{#S}
  for $\sigma$.}.

We also show how to look-up a reducible term in a reducible
substitution by using the \bel{lookup} function. We can
read the type of \bel{lookup} as follows: For a context $\gamma$, for
all variables \bel{#p} of closed type \bel{T} from the context
$\gamma = $\bel{x$_1$:term T$_1$, $\ldots$, x$_n$:term T$_n$} , 
if $\rc {\sigma} {\gamma}$, i.e. $\sigma$ is a substitution
of the form \bel{N}$_1/$\bel{x}$_1,
\ldots,$\bel{N}$_n/$\bel{x}$_n$ that provides a term \bel{N}$_i$ 
for each variable \bel{x}$_i$ in $\gamma$ s.t. \bel{Reducible T$_i$  N$_i$ },
we know \bel{Reducible T #p[\sigma]}.This property may seem obvious,
but it must be shown by recursively checking it for each variable in
$\gamma$. We therefore pattern macht on the context $\gamma$. If the
context $\gamma$ is empty, then there is no variable and hence the
case is impossible (written as \lstinline!impossible [|- #p]!. 

If $\gamma =\gamma', x:tm T$, then we pattern match on the parameter
variable \lstinline!#p!. There are two cases: either 
\lstinline!#p = x!. in this case we simply analyze \lstinline!rs! which stands for the
proof \lstinline!Red_sub [\gamma', x:term T[]] [\sigma', N']! and return
the witness \lstinline!rN! for 
\lstinline!Reducible [|- N'] [|- T]!. 

Otherwise \lstinline!#p! stands for a variable other than
\lstinline!x! and must come from \lstinline!\gamma'!. This case is
written as \lstinline![\gamma', x:term T |- #q[..]]! where the
parameter variable \lstinline!#q! stands for a variable from
\lstinline!\gamma'! and we simply recurse on 
\lstinline![\gamma' |- #q]!. 

We make sure to associate the parameter variable
with the weakening substitution \lstinline![..]! in the pattern. Note that
\lstinline$[..]$ is not an identity substitution here. The identity
substitution in the context \lstinline!\gamma', x:term T[]! is
\lstinline![..,x]!. 

Finally, we can revisit the fundamental lemma and show its
implementation in \beluga. 

\begin{lstlisting}
rec main: {\gamma:ctx}{M:[\gamma |- tm T[]]} Red_sub [\gamma] [|- \sigma] -> Reduce [|- T] [|- M[\sigma]] =
 mlam \gamma => mlam M => fn rs => case [\gamma |- M] of
| [\gamma |- #p] => lookup [\gamma] [\gamma |- #p] rs
| [\gamma |- lam \x. M] =>
 Rarr [|- halts_m refl val_lam]
   (mlam N => fn rN =>
    bwd_closed [|- beta] (main [\gamma,x:tm _] [\gamma,x |- M] (Dot rs rN)))
 | [\gamma |- app M1 M2] =>
  let Rarr ha f = main [\gamma] [\gamma |- M1] rs in
  f [|- _ ] (main [\gamma] [\gamma |- M2] rs)
| [\gamma' |-  c] => Rb [|- halts_m refl val_c]
;
\end{lstlisting}

In the variable case, we simply use the \lstinline!lookup!-function to
guarantee that \lstinline!#p[\sigma]! is reducible. The case for
abstractions follows our on paper proof. To prove the 
\lstinline!Reducible [|- arr T S] [|- lam \x.M]!, we must prove two
things: first, we must show  \lstinline!halts (lam \x.M)!. We use 
\lstinline!val_lam!  to justify that abstractions are values and by
reflexivity abstrations step to themselves. Therefore their evaluation
halts. Note that we do not explicitly refer to properties of
substitutions in our implementation, although we highlighted such
reasoning in our previous proof. Such reasoning is hidden as part
of the equational theory our type checker uses.
%
Second, we show that
for all \lstinline!N!, if
\lstinline!Reduce [|-T] [|-N]! then 
\lstinline!Reduce [|-S] [|-app (lam \x.M) N]!.  



We first assume \lstinline!N! together with
\lstinline!rN:Reduce [|- T] [|- N]! by writing 
\lstinline!mlam N => fn rN =>  ... !. Then we use the IH and the lemma
\lstinline!bwd_closed! to finish the proof as described earlier. We
emphasize again that not explicit substitution reasoning is required
in the implementation, although it clearly is used in the proof.

Lastly, consider the case for applications, i.e. 
\lstinline![\gamma |- app M1 M2]!. By the IH we have that 
\lstinline!Reducible [|- arr S T] [|- M1[\sigma]]!. By definition of
\lstinline!Reduce!, we have that \lstinline!halts M1[\sigma]! and more
importantly, we have a function \lstinline!f! whose type says:
for all \lstinline!N!, if 
\lstinline!Reduce [|- S] [|- N]! then 
\lstinline!Reduce [|- T] [|- app M1[\sigma] N]!. 
%
We now simply use \lstinline!f! and pass to it 
\lstinline![|- M2[\sigma]! and a witness for 
\lstinline!Reduce [|- T] [|- M2[\sigma]]! which
is obtained by making a recursive call on 
\lstinline![\gamma |- M2]!.



And finally we have all the elements to prove that all well typed
terms eventually reduce to a value:
\begin{lstlisting}
rec weakNorm : {M:[|- tm A]} [|- halts M] =
mlam M => reduce_halts (main [] [|- M] Nil)
;
\end{lstlisting}

Let's retrace our steps. We set out to prove that all terms reduce to a
value. A simple proof by induction would not give us a powerful enough
induction hypothesis, so we defined the reducibility candidate
relation that was inductive on the type and allowed for a powerful enough
induction hypothesis. Then when proving that all terms are reducibl, We needed again a more powerful induction
hypothesis to be able to prove that all terms were in the reducibility
relation. In particular, we generalized the theorem to all terms and
their grounding substitutions, for this we needed a predicate on
grounding substitution, to be sure that all the terms in them were
reducible. With all this machinery in place the proof went through by
appealing to the lemmas we had proven earlier.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "book"
%%% End: