
%-------------------------------------------------------------------------------
% LF                                                                            
%-------------------------------------------------------------------------------

\section{LF: A Logical Framework}

The original LF logical framework was specified as follows:
$$
\begin{array}{llll}
\textbf{Kinds} & K & ::= & \Type \Spb \PiTyp{x}{A}{K} \\
\textbf{Families} & A & ::= & a \Spb \PiTyp{x}{A_2}{A} \Spb \Lam{x : A_2}{A} \Spb \Appl{A}{M} \\
\textbf{Terms} & M & ::= & c \Spb x \Spb \Lam{x : A}{M} \Spb \Appl{M}{M_2} \\
\textbf{Signatures} & \Sigma & ::= & \cdot \Spb \Sigma,\Of{c}{A} 
\Spb \Sigma,\Of{a}{K}\\
\textbf{Contexts} & \Gamma & ::= & \cdot \Spb \Gamma,\Of{x}{A}\\
% \textbf{Simple Types} & \alpha & ::= & a \Spb \Arr{\alpha_1}{\alpha_2} \\
\end{array}
$$

While this definition is the simplest, the meta-theory of LF was
significantly simplfied by the introduction of Canonical LF, admitting
only the so-called \emph{canonical forms} into the language.

%-------------------------------------------------------------------------------
% Canonical LF                                                                  
%-------------------------------------------------------------------------------

\section{Canonical LF}
We begin by describing Canonical LF, the language at the heart of our
work.  While the various representations will differ from the one presented here, 
(e.g., for efficiency) this language should always be kept in mind.

The main difference between Canonical LF and earlier versions
is the lack of explicit $\beta$-redices in types and terms.  
Also, a type annotation on $\lambda$-expressions is no longer required (or allowed).
See Harper and Licata\cite{Harper:2006:Mechanizing} for an extended
exposition.

$$
\begin{array}{llll}
\textbf{Kinds} & K & ::= & \Type \Spb \PiTyp{x}{A}{K} \\
\textbf{Canonical Type Families} & A & ::= & P \Spb \PiTyp{x}{A_2}{A} \\
\textbf{Atomic Type Families} & P & ::= & a \Spb \Appl{P}{M} \\
\textbf{Canonical Terms} & M & ::= & R \Spb \Lam{x}{M} \\
\textbf{Atomic Terms} & R & ::= &  x \Spb c \Spb \Appl{R}{M}\\
\textbf{Signatures} & \Sigma & ::= & \cdot \Spb \Sigma,\Of{c}{A} 
\Spb \Sigma,\Of{a}{K}\\
\textbf{Contexts} & \Gamma & ::= & \cdot \Spb \Gamma,\Of{x}{A}\\
% \textbf{Simple Types} & \alpha & ::= & a \Spb \Arr{\alpha_1}{\alpha_2} \\
\end{array}
$$

%-------------------------------------------------------------------------------
% Spine Form LF                                                                 
%-------------------------------------------------------------------------------

\subsection{Spine-Form Canonical LF}

There are a number of difficulties with the name-carrying 
representation\footnote{i.e., variable names associated with binders}
of Canonical LF.  The first is that we must
implement capture-avoiding substitution and $\alpha$-conversion,
a notoriously delicate and error-prone process.
We can circumvent this difficulty
by using DeBruijn indices\cite{DeBruijn:1972:Terms}. 

 A more significant 
difficulty lies in the implementation of hereditary substitution. 
\XXX{citation needed}
When applying a substitution, we often need to determine whether
the head of an expression is a constant or a variable in order
to know which rule to apply.  Thus, for a term of the form
$$f\ x_1\ x_2\ \ldots\ x_n = (\ldots((f\ x_1)\ x_2)\ \ldots\ x_n) $$
we need to take apart $n$ applications just to determine how
a substitution should be applied.  Later, when we implement
unification, that algorithm will need to compare the heads
of such terms for equality.  Thus, quick access to the head
of such a term is essential for a reasonably efficient implementation.
We thus define \emph{Spine-Form Canonical LF}.

$$
\begin{array}{llll}
\mathbf{Kinds} & K & ::= & \Type \Spb \SpPiTyp{A}{K} \\
\mathbf{Canonical\ Type\ Families} & A & ::= & P \Spb \SpPiTyp{A_1}{A_2} \\
\mathbf{Atomic\ Type\ Families} & P & ::= & a\cdot S \\
\mathbf{Canonical\ Terms} & M & ::= & R \Spb \SpLam{M} \\
\mathbf{Atomic\ Terms} & R & ::= & H\cdot S \\
\mathbf{Heads} & H & ::= & c \Spb i\\
\mathbf{Spines} & S & ::= & \Nil \Spb M;S\\
\end{array} 
$$

In the following judgments will have the same
form for different classes.  For instance,
the rules for $\Pi$-types and $\Pi$-kinds will
oftentimes be identical in structure.  To avoid the
repetition of rules, we introduce a convenient 
syntax.

$$
\begin{array}{llll}
\mathbf{Levels} & L & ::= & \Type \Spb \Kind \\
\mathbf{Expressions} & U & ::= & L \Spb \SpPiTyp{U_1}{U_2} \Spb \lambda U \Spb H\cdot S \\
\mathbf{Heads} & H & ::= & c \Spb i\\
\mathbf{Spines} & S & ::= & \Nil \Spb U;S\\
\end{array} 
$$

Constants $c$ are either type ($a$) or term ($c$) constants.
The rules that follow will refer to this basic syntax.  While this
is somewhat less precise than the more explicit separation of 
levels in the syntax above (indeed, we can easily write gramatically
correct nonsense in this language, such as $\SpLam{(\SpPiTyp{U1}{U2})}$)
we are willing to allow such terms to lessen the number of rules.
Terms that are not even gramatically correct (much less type-correct) 
in the original language, will be excluded by type-checking (rather than expression 
formation, as in the previous version).

We will freely mix the more concrete classes such as $K,A$ and $P$
above when the rules restrict the expressions to such cases.
We see no potential for confusion however, and again notational
convenience is our guide.  


