\section{Canonical Forms}

%\subsection{Canonical forms for $\lc$}


We present the inductive definition of \emph{canonical} forms in 
$\lc$, \ie terms in $\be$-long normal form.  This is a generalization 
of canonicity for the simply-typed $\l$-calculus, as  described in 
\cite{Pfenning94un}.  It is realized by the two mutually recursive 
judgments depicted in Figure~\ref{fig:canon}:

\ben 
\item$\GG;\Omega;\Delta\prv M \da A$: $M$ is atomic of type $A$.
\item$\GG;\Omega;\Delta\prv M \bua A$: $M$ is canonical of type $A$.
\enen

\begin{figure}
\label{fig:canon}
\[
\begin{array}{c}
\ianc{c\oftp A\in\Sigma}{\GG; \Omega;\cdot  \prv  c\da A}{cIdc}\vsk
\ianc{}{(\GG,x\oftp A);\Omega; \cdot  \prv  x\da A}{cId^{u}}
\qquad \mbox{\textrm{no rule for }}cId^{0}
\qquad
\ianc{}{\GG;\Omega; x\oftp A \prv  x\da A} {cId^{1}}
\vsk
%\ianc{}{\GG;\Omega;\Delta\vd E\ \ol{x_{n}^{l}}\da P}{cPat}
%\qquad
\ianc{\GG;\Omega;\Delta \prv  M\da a}{\GG;\Omega;\Delta \prv  M\bua a} 
{cAt}\vsk
\ianc{(\GG,x\oftp A) ; \Omega;\Delta \prv M\bua B}{\GG;\Omega;\Delta\prv(\lamb{x^u}{A} M) \bua 
A\TImp B} {c\TImp I}
\vsk
\ianc{\GG ; \Omega; (\Delta,x\oftp A) \prv M\bua B}{\GG;\Delta\prv(\lamb{x^1}{A} M) \bua 
A\RImp B}{c\RImp I}
\vsk
\ianc{\GG ;(\Omega, x\oftp A) ;\Delta \prv M\bua B}{\GG;\Omega;\Delta\prv(\lamb{x^0}{A} M) \bua 
A\ZImp B}{c\ZImp I}
\vsk
 \ibnc{\Gamma; \Omega; \Delta \vd M \da A \TImp B}{(\Gamma, \Delta);
\O; \cdot \vd N \bua A}{\Gamma; \Omega; \Delta
\vd M\ N^u \da B}{c\GImp{u}E}
\vsk
\ianc{\GG;\Omega;\Delta\prv M \da A \ZImp B \quad (\GG,\Omega,\Delta);\cdot;\cdot \prv N \bua A
}
{\GG;\Omega;\Delta  \prv M  \ N^0 \da B}{c\ZImp E}\vsk

\ibnc{(\Gamma, \Delta_N); \Omega; \Delta_M \vd M \da A \RImp 
B}{(\Gamma, \Delta_M); \Omega; \Delta_N \vd N \bua A}{\Gamma; \Omega; 
(\Delta_M, \Delta_N) \vd M\ N^1 \da B}{c\RImp E}
\end{array}
\]
\caption{Canonical forms for $\lc$}
\end{figure}



\begin{Theorem}[Canonical Form Theorem]
\label{thm:canonical}
If $\god\vd M\hastype A$, then there is $N$ such that $\god\vd M\bua 
N\hastype A$.
% \ben 
% \item $\GG;\Omega;\Delta\prv M \da A$.
% \item $\GG;\Omega;\Delta\prv M \bua A$.
% \enen
\end{Theorem}
\begin{proof}
A suitable reformulation of Tait's method along the lines of 
\cite{Cervesato96phd}\footnote{\emph{Fill in}}.
\end{proof}

We sometimes abbreviate the statement of the canonical form Theorem as
$\GG;\Omega;\Delta\prv M \buda A$.

