
\section{Lazy Typechecking}

There are two variations on lazy typechecking, with the
same distinction as the eager case, viz. the existence
of a syntactic composition of substitutions.

In the lazy case we relax the canonicity requirements and 
admit terms into the language with explicit $\beta$-redexes
and explicit substitutions.

%-------------------------------------------------------------------------------
% Terms                                                                         
%-------------------------------------------------------------------------------

\subsection{Terms}

$$
\begin{array}{llll}
\mathbf{Levels} & L & ::= & \Type \Spb \Kind \\
\mathbf{Expressions} & U,V & ::= & L \Spb \PiTyp{U_1}{U_2} \Spb \lambda U \Spb H\cdot S \Spb U[\sigma] \Spb M @ S\\
\mathbf{Heads} & H & ::= & c \Spb i\\
\mathbf{Spines} & S & ::= & \Nil \Spb U;S \Spb S[\sigma]\\
\mathbf{Eager\ Substitutions} & \sigma & ::= & M\cdot\sigma \Spb \Shift^n \\
\mathbf{Lazy\ Substitutions} & \sigma & ::= & M\cdot\sigma \Spb \Shift^n \Spb \sigma_1 \Comp \sigma_2\\
\end{array} 
$$

%-------------------------------------------------------------------------------
% Weak Head Normal Form                                                         
%-------------------------------------------------------------------------------

\subsection{Weak Head Normalization}

For terms With explicit substitutions $U[\sigma]$ and redexes $M @ S$,
we can usually not decide which rule to apply during typechecking.
We need to discover the top level structure of the term.  
The least work we need to do to discover this form is called 
\emph{weak head normalization}.  


\bigskip 
\framebox{$U\Weak U'$}
\bigskip 

$$
\begin{array}{cc}
\infer{L \Weak L}{} &
\infer{\PiTyp{U_1}{U_2} \Weak \PiTyp{U_1}{U_2}}{} \\\\
\infer{\Lam{U} \Weak \Lam{U}}{} &
\infer{H\cdot S \Weak H\cdot S}{} \\\\
\infer{L[\sigma] \Weak L}{}&
\infer{(\PiTyp{U_1}{U_2})[\sigma] \Weak \PiTyp{(U_1[\sigma])}{(U_2\Ssub)}}{} \\\\
\infer{(\Lam{U})[\sigma] \Weak \Lam{(U\Ssub)}}{} &
\infer{(c\cdot S)[\sigma] \Weak c\cdot (S[\sigma])}{} \\\\
\infer{(U[\sigma])[\sigma'] \Weak U'}{U[\sigma\Comp\sigma']\Weak U'} \\\\
\infer{M @ S \Weak H\cdot S}{M\Weak H\cdot S & S \Weak \Nil} &
\infer{M @ S \Weak M_3}{M\Weak \Lam{M_1} & S \Weak M_2;S' & M_1[M_2\cdot\IdSub] @ S'\Weak M_3} \\\\
\infer{(i\cdot S)[\sigma]\Weak j\cdot (S[\sigma])}{i[\sigma] \Weak j} &
\infer{(i\cdot S)[\sigma]\Weak M'}{i[\sigma] \Weak M & M@(S[\sigma])\Weak M'} \\\\
\end{array} 
$$

\bigskip 
\framebox{$S\Weak S'$}
\bigskip 

$$
\begin{array}{cc}
\infer{\Nil \Weak \Nil}{} &
\infer{M;S \Weak M;S}{} \\\\
\infer{\Nil[\sigma] \Weak \Nil}{} &
\infer{(M;S)[\sigma] \Weak M[\sigma];S[\sigma]}{} 
\end{array} 
$$

\bigskip 
\framebox{$i[\sigma] \Weak M$}
\bigskip 

$$
\begin{array}{cc}
\infer{i[\Shift^n] \Weak i + n}{} &
\infer{1[M;S] \Weak M'}{M\Weak M'} \\\\
\infer{(n+1)[M\cdot \sigma] \Weak M'}{n[\sigma]\Weak M'} &
\infer[(*)]{i[\sigma_1\Comp\sigma_2] \Weak M'}{i[\sigma_1] \Weak M & M[\sigma_2]\Weak M'} 
\end{array} 
$$

%-------------------------------------------------------------------------------
% Typecheck                                                                     
%-------------------------------------------------------------------------------

\subsection{Typechecking}

Typechecking is slightly more complicated in the lazy case, as
we need to return any terms that have been partially evaluated
by the typechecking process.

\bigskip 
\framebox{$\LzCheckTy{U}{V}{\Gamma'}{U'}{V'}$}
\bigskip 

$$
\begin{array}{c}
\infer{\LzCheckTy{U}{V}{\Gamma'}{U''}{V''}}{U\Weak U' & V\Weak V' & \LzCheckTy{U'}{V'}{\Gamma'}{U''}{V''}}\\\\
\infer{\LzCheckTy{\Type}{\Kind}{\Gamma}{\Type}{\Kind}}{} \\\\
\infer{\LzCheckTy{\PiTyp{A}{U}}{L}{\Gamma''}{\PiTyp{A''}{U'}}{L}}{\LzCheckTy{A}{\Type}{\Gamma'}{A'}{\Type} & \LzCheckTy[\Gamma',A']{U}{L}{\Gamma'',A''}{U'}{L}} \\\\
% \infer{\LzCheckTy{U[\sigma]}{V}{\Gamma'}{U''}{V'}}{U[\sigma]\Weak U' & \LzCheckTy{U'}{V}{\Gamma'}{U''}{V'}} \\\\
% \infer{\LzCheckTy{M @ S}{A}{\Gamma'}{M''}{A'}}{M@S\Weak M' & \LzCheckTy{M'}{A}{\Gamma'}{M''}{A'}} \\\\
\infer{\LzCheckTy{\Lam{M}}{A}{\Gamma'}{\Lam{M'}}{\PiTyp{A_1'}{A_2'}}}{A\Weak \PiTyp{A_1}{A_2} & \LzCheckTy[\Gamma,A_1]{M}{A_2}{\Gamma',A_1'}{M'}{A_2'}} \\\\
\infer{\LzCheckTy{c\cdot S}{V_1}{\Gamma'}{c\cdot S'}{V_1'}}{\Sigma(c) = V_2 & \LzFocus{S}{V_2}{\Gamma'}{S'}{V_2} & \LzEquiv{V_2}{V_1}{V_2}{V_1'}} \\\\
\infer{\LzCheckTy{i\cdot S}{A_1}{\Gamma'}{i\cdot S'}{A_1'}}{\Gamma(i) = A_2 & \LzFocus{S}{A_2}{\Gamma'}{S'}{A_2} & \LzEquiv{A_2}{A_1}{A_2}{A_1'}} \\\\
\end{array} 
$$

Note that in the rule for $c\cdot S$, $\Sigma$ contains only canonical terms,
thus the weak head normalization does not affect it.
Also recall note \ref{context:shift}.

\bigskip 
\framebox{$\LzFocus{S}{U}{\Gamma'}{S'}{U'}$}
\bigskip 

$$
\begin{array}{c}
\infer{\LzFocus{U}{V}{\Gamma'}{U''}{V''}}{U\Weak U' & V\Weak V' & \LzFocus{U'}{V'}{\Gamma'}{U''}{V''}}\\\\
\infer{\LzFocus{\Nil}{\Type}{\Gamma}{\Nil}{\Type}}{} \\\\
\infer{\LzFocus{P}{L}{\Gamma}{P}{L}}{} \\\\
\infer{\LzFocus{M;S}{\PiTyp{A}{V}}{\Gamma''}{M';S'}{\PiTyp{A'}{V'}}}{\LzCheckTy{M}{A}{\Gamma'}{M'}{A'} & \LzFocus[\Gamma']{S}{V[M'\cdot\IdSub]}{\Gamma''}{S'}{V'}} \\\\
\end{array} 
$$

The rules for evaluating composition of substitutions $\sigma_1\Comp\sigma_2$
are the same as for the eager case, though $M[\sigma]$ should be read
as the lazy explicit substitution.

%-------------------------------------------------------------------------------
% Equivalence                                                                   
%-------------------------------------------------------------------------------

\subsection{Equivalence} 

Note that we do not consider equivalence of substitutions or redexes, but rather
immediately consider the weak head normal form.  Would it be interesting
to try equivalence there?

\bigskip 
\framebox{$\LzEquiv{U_1}{U_2}{U_1'}{U_2'}$}
\bigskip 

$$
\begin{array}{c}
\infer{\LzEquiv{U_1}{U_2}{U_1''}{U_2''}}{U_1\Weak U_1' & U_2\Weak U_2' & \LzEquiv{U_1'}{U_2'}{U_1''}{U_2''}}\\\\
\infer{\LzEquiv{U_1}{U_2}{U_1'}{U_2'}}{\LzEquiv{U_2}{U_1}{U_2'}{U_1'}} \\\\
\infer{\LzEquiv{\PiTyp{U_1}{U_2}}{\PiTyp{U_3}{U_4}}{\PiTyp{U_1'}{U_2'}}{\PiTyp{U_3'}{U_4'}}}{\LzEquiv{U_1}{U_3}{U_1'}{U_3'} & \LzEquiv{U_2}{U_4}{U_2'}{U_4'}} \\\\
\infer{\LzEquiv{c\cdot S_1}{c\cdot S_2}{c\cdot S_1'}{c\cdot S_2'}}{\LzEquiv{S_1}{S_2}{S_1'}{S_2'}} \\\\
\infer{\LzEquiv{i\cdot S_1}{i\cdot S_2}{i\cdot S_1'}{i\cdot S_2'}}{\LzEquiv{S_1}{S_2}{S_1'}{S_2'}} \\\\
\infer{\LzEquiv{\Lam{M_1}}{\Lam{M_2}}{\Lam{M_1'}}{\Lam{M_2'}}}{\LzEquiv{M_1}{M_2}{M_1'}{M_2'}} \\\\
% \infer{\LzEquiv{U_1[\sigma_1]}{U_2[\sigma_2]}{U_1'[\sigma_1']}{U_2'[\sigma_2']}}{\LzEquiv{U_1}{U_2}{U_1'}{U_2'} & \LzEquiv{\sigma_1}{\sigma_2}{\sigma_1'}{\sigma_2'}} \\\\
\infer{\LzEquiv{c\cdot S}{M}{M''}{M'}}{c\StepsTo M' & \LzEquiv{M'@S}{M}{M''}{M'}} 
\end{array} 
$$

\bigskip 
\framebox{$\LzEquiv{S_1}{S_2}{S_1'}{S_2'}$}
\bigskip 

$$
\begin{array}{c}
\infer{\LzEquiv{S_1}{S_2}{S_1''}{S_2''}}{S_1\Weak S_1' & S_2\Weak S_2' & \LzEquiv{S_1'}{S_2'}{S_1''}{S_2''}}\\\\
\infer{\LzEquiv{\Nil}{\Nil}{\Nil}{\Nil}}{}\\\\
\infer{\LzEquiv{M_1;S_1}{M_2;S_2}{M_1';S_1'}{M_2';S_2'}}{\LzEquiv{M_1}{M_2}{M_1'}{M_2'} & \LzEquiv{S_1}{S_2}{S_1'}{S_2'}} \\\\
% \infer{\LzEquiv{S_1[\sigma_1]}{S_2[\sigma_2]}{S_1'[\sigma_1']}{S_2'[\sigma_2']}}{\LzEquiv{S_1}{S_2}{S_1'}{S_2'} & \LzEquiv{\sigma_1}{\sigma_2}{\sigma_1'}{\sigma_2'}} \\\\
\end{array} 
$$

