\documentclass[draft]{article}

\input theorem
\input prooftree
\input lineardvi

\def\rtype{{\mathrm{type}}}
\def\rctx{\ {\mathrm{ctx}}}
\def\rkind{{\mathrm{kind}}}
\def\rok{{\mathrm{ok}}}
\def\rid{\mathsf{id}}
\def\tcheck{\Leftarrow}
\def\synth{\Rightarrow}

\def\easyrule#1#2{
\begin{prooftree}
#1 \justifies #2
\end{prooftree}}
\title{TinyLF: A Compact Definition of a Logical Framework}
\author{Jason Reed}
\begin{document}
\maketitle
\section{Introduction}
By pushing some modern ideas concerning LF to their logical
conclusion, one can obtain a very concise definition of a logical
framework, which has a comparably simple metatheory. This logical
framework generalizes LF slightly by including a limited form of
polymorphism.  The main point, however, is not this extension per se,
but that we can support the {\em same} feature set as LF in a much
more compact way.

The central ideas are naturally the recently ubiquitous notion of {\em
restricting attention to only canonical forms} of
$\lambda$-expressions, and the consequent need to define {\em
hereditary substitution}, pioneered by Watkins et al in CLF.

Another main contributing idea is that of spine form, which
considers not just single function applications but applications of
heads to entire vectors of arguments at once. Spine form still
describes function abstractions in terms of one-at-a-time
$\lambda$-binding of variables. The motivation is to find a convenient
syntax in which variable binding also takes place in a `vectorized'
fashion. This is obviously related to the idea of pattern-matching in
functional languages. However, in the present case, given the usual
normal/atomic distinction that serves to enforce $\beta$-normal,
$\eta$-long terms, we are able to demand that functions provide the
{\em entire} pattern of their arguments, coalescing all potential
curried arguments into one sequence.

But the other salient recent piece of work where sequences of terms play an
important role is the Contextual Modal Type Theory designed to give a
logical account of operations such as raising and lowering of
metavariables in unification. In it, modal variables appear under {\em
substitutions} that fill in the variable's arguments all at once.  We
take essentially the same approach while dropping the {\em closedness}
requirement on substitutions for modal variables, making our variables
still `contextual' but not modal.

\section{Syntax}
The complete syntax of the language is as follows:
$$\begin{tabular}{rlll}
Base Classifiers&$v$&$::=$&$R \celse \rtype$\\
Classifiers&$V$&$::=$&$\Pi \Psi .v$\\
Atomic Terms&$R$&$::=$&$x[\sigma]$\\
Terms&$M$&$::=$&$ \lambda \hat \Psi  . R$\\
Substitutions&$ \sigma $&$::=$&$\rid \celse M . \sigma$\\
Contexts&$\Gamma$&$::=$&$\cdot \celse\Gamma, x : V$\\
\end{tabular}$$

The syntax $\hat \Psi$ stands for just the sequence of variables found
in $\Psi$, without their associated types. All contexts are to be understood
as dependent, with $V$s on the right being in the scope of variables on their left.
We will use $=$ to mean syntactic equality up to $\alpha$-conversion.

The terms $M$ of LF correspond to terms here; their consecutive
$\lambda$s have simply been merged into one context. For example, the LF
term 
$$\lambda x . \lambda y . \lambda z . z$$
corresponds to
$$\lambda (x,y,z) . z[\rid]$$ Variable occurrences are always {\em
under substitution}, the substitution being the analogue to the spine
attached to a root in spine form.  Indeed, all substitutions are are
vectors of terms. To carry out a substitution, we will write
$\{\sigma/\Psi\}$, substituting the items found in $\sigma$ for the
variables in $\Psi$. We call these term vectors substitutions rather
than spines because they associate the opposite way.

Both the types and kinds of LF become {\em classifiers} in the present
system. A base classifier is either a base type $x[\sigma]$, which corresponds to
a base type $a\cdot S$ in spine-form $LF$, or else it is the base kind $\rtype$.
This merger is reminiscent of (but not quite identical to) the
uniformity typical of Pure Type Systems. The difference is that while
we allow type variables $x : \rtype$ to appear in contexts, the only
things that can be substituted for $x$ are {\em base} types.

Because variables in the context can have classifiers such as $\Pi
\Psi . \rtype$ that are essentially kinds, we have no need for a
separate notion of signature: the context by itself can contain a
mixture of declarations of type families and constants.

\section{Typing}

The judgments are

$$\begin{tabular}{ll}
$\Gamma \prov V \tcheck \rok$&$V$ is a well-formed classifier\\
$\Gamma \prov N \tcheck V$&$N$ checks at classifier $V$\\
$\Gamma \prov R \synth v$&$R$ synthesizes classifier $v$\\
$\Gamma \prov \sigma \tcheck \Psi$&$\sigma$ is a valid substitution for $\Psi$\\
$\Gamma \prov \Psi \rctx $&$\Psi$ is a well-formed context\\
\end{tabular}$$

Well-formedness of classifiers is defined by two rules, one that 
allows formation of types and another that forms kinds:

$$
\easyrule
{\Gamma \prov \Psi \rctx \qquad 
\Gamma, \Psi \prov R \synth \rtype}
{\Gamma \prov \Pi \Psi . R \tcheck \rok}
\qquad
\easyrule
{\Gamma \prov \Psi \rctx}
{\Gamma \prov \Pi \Psi . \rtype \tcheck \rok}
$$

The remaining judgments are defined by the following rules:
$$
\easyrule
{\Gamma, \Psi \prov R \synth  v' \qquad v = v'}
{\Gamma \prov \lambda \hat \Psi . R \tcheck \Pi \Psi . v}
\qquad 
\easyrule
{ x : \Pi \Psi . v  \in \Gamma \qquad \Gamma \prov \sigma : \Psi}
{\Gamma \prov x[\sigma] \synth v\{\sigma/ \Psi\}}
$$

$$
\easyrule{}
{\Gamma \prov \rid \tcheck \cdot }
\qquad
\easyrule
{\Gamma \prov M \tcheck V\{\sigma / \Psi\} \qquad \Gamma \prov \sigma \tcheck \Psi}
{\Gamma \prov M.\sigma \tcheck (\Psi, x : V) }
$$

$$
\easyrule{}
{ \Gamma\prov \cdot  \rctx }
\qquad
\easyrule
{\Gamma\prov \Psi \rctx \qquad  \Gamma,\Psi \prov V \tcheck \rok }
{ \Gamma\prov \Psi, x : V \rctx}
$$

Let $X$ stand for any syntactic object $v,v,M,R,\sigma,\Gamma$.
All that remains to define is substitution $X\{\sigma/\Psi\}$. It is
defined recursively according to a lexicographic order on the structure of first $\Psi$,
then $X$.
We say $(M/x : V) \in \{\sigma/\Psi\}$ if, for some
$n$, the $n^{th}$ item from the left in $\sigma$ is $M$, and the
$n^{th}$ item from the right in $\Psi$ is $x : V$.
Almost all cases are homomorphic. Abbreviating $\theta = \{\sigma/\Psi\}$,
we have

$$(M_1.\ldots M_n. \rid)\theta = (M_1\theta. \ldots M_n\theta . \rid)$$
$$(V_1,\ldots, V_n)\theta = (V_1\theta, \ldots, V_n \theta)$$
$$(\Pi \Delta . v)\theta = \Pi (\Delta\theta) . (v\theta)
\qquad 
(\lambda \hat \Delta . R)\theta = \lambda \hat \Delta . (R\theta)$$
$$(\rtype)\theta = \rtype$$
The only interesting case is
$$( x[\rho])\theta = 
\cases{
 R\{\rho\theta/\Delta\}&if $(\lambda \hat \Delta . R/x:\Pi \Delta . V) \in \theta $;\cr
x[\rho\theta]&otherwise.
\cr
}$$
This completes the definition of TinyLF.
\section{Results}
The things we are trying to prove are fairly standard, and so too are the methods for the most part.
In preparation for the substitution property, we show that substitutions commute properly.
In preparation for the identity property, we show that $\eta$-expansions are two-sided units with respect to substitution.

\begin{lemma}
\label{simple.type}
$X \{\sigma / \Psi \} = X \{\sigma / \Psi\theta \}$.
\end{lemma}
\begin{proof}
By induction on $\Psi$, then $X$. The interesting case is when $X = x[\rho]$,
and $(\lambda \hat \Delta . R/x:\Pi \Delta . V) \in \{\sigma/\Psi\} $.
In this case $(\lambda\hat \Delta. R/ x : \Pi (\Delta\theta) . (V\theta)) \in \{\sigma / \Psi\theta\}$.
We reason that 
\begin{tabbing}
$R\{\rho\{\sigma/\Psi\} / \Delta\}$\\
$= R\{\rho \{\sigma / \Psi\theta \} / \Delta\}$\` i.h. on $\rho < x[\rho]$\\
$= R\{\rho \{\sigma / \Psi\theta \} / \Delta\theta\}$\` i.h. on $\Delta < \Psi$\\
\end{tabbing}
\cqed
\end{proof}
\begin{lemma}
If $FV(X) \cap \hat \Psi = \emptyset$, then 
$X \{\sigma/\Psi\} = X$.
\label{triv.subst}
\end{lemma}
\begin{proof}
Straightforward induction.
\cqed
\end{proof}

The above lemma is exemplary of the fact that substitution
$\{\sigma/\Psi\}$, as should be expected from a hereditary
substitution, does not really care about the exact structure of the
types $\Psi$, but only the $\Pi$-skeleton of them.

Let $J$ stand for an arbitrary judgment of the system.

\begin{lemma}[Weakening]
If $\Gamma, \Gamma' \prov J$, then $\Gamma, \Delta, \Gamma' \prov J$.
\label{weakening}
\end{lemma}
\begin{proof}
Straightforward induction.
\cqed
\end{proof}

\begin{lemma}
If $(M/x:V)\in \{\sigma/\Psi\}$ and $\Gamma \prov \sigma \tcheck \Psi$,
then $\Gamma \prov M \tcheck V\{\sigma/\Psi\}$.
\label{extract}
\end{lemma}
\begin{proof}
Straightforward induction.
\cqed
\end{proof}

\begin{lemma}[Interchange]
\label{interchange}
If $FV(\sigma) \cap \hat \Delta = \emptyset$, then 
$X \{\rho/\Delta\}\theta = X \theta \{\rho\theta / \Delta\}$
\end{lemma}
\begin{proof}
By induction on first the undordered pair $(\Delta,\Psi)$, and subsequently $X$.
For all the homomorphism cases, it's just $X$ that gets smaller. This includes
the case of $X = x[\omega]$ where $x$ is in neither $\hat \Delta$ nor $\hat \Psi$.
The interesting cases are
\begin{itemize}
\item $x\in \hat\Psi$ and $(\lambda \hat \Omega . R / x : \Pi \Omega . v) \in \{\sigma/\Psi\} = \theta$.
In this case we reason that
\begin{tabbing}
$x[\omega] \{\rho/\Delta\}\theta $\\
$= x[\omega\{\rho/\Delta\}] \theta $\\
$= R\{\omega\{\rho/\Delta\} \theta / \Omega\} $\\
$= R\{\omega\theta\{\rho\theta/\Delta\}  / \Omega\} $\` i.h. on $\rho < x[\rho]$\\
$= R\{\rho\theta/\Delta\}\{\omega\theta\{\rho\theta/\Delta\}  / \Omega\} $ \` Lemma~\ref{triv.subst}\\
$= R\{\omega\theta/\Omega\}  \{\rho\theta / \Delta\}$\` i.h. on $(\Omega,\Delta) < (\Delta,\Psi)$\\
$= x[\omega] \theta \{\rho\theta / \Delta\}$\\
\end{tabbing}
To justify the second induction hypothesis appeal, we need $FV(\rho\theta) \cap \hat \Omega = \emptyset $,
but this is true because the variables $\hat \Omega$ are bound inside $\sigma$.
\item $x\in \hat\Delta$ and $(\lambda \hat \Omega . R / x : \Pi \Omega . v) \in \{\rho/\Delta\}$.
In this case we reason that
\begin{tabbing}
$x[\omega] \{\rho/\Delta\}\theta$\\
$= R\{\omega\{\rho/\Delta\}/\Omega\} \theta$\\
$= R\theta\{\omega\{\rho/\Delta\}\theta/\Omega\} $\` i.h. on $(\Omega,\Psi) < (\Delta, \Psi)$\\
$= R\theta\{\omega\theta\{\rho\theta/\Delta\}/\Omega\} $\` i.h. on $\rho < x[\rho]$\\
$= R\{\omega \theta \{\rho\theta / \Delta\} / \Omega\}  $\` Lemma~\ref{triv.subst}\\
$= x[\omega \theta]  \{\rho\theta / \Delta\}$\\
$= x[\omega] \theta \{\rho\theta / \Delta\}$\\
\end{tabbing}
\end{itemize}
\cqed
\end{proof}

\begin{lemma}[Substitution]
If $\Gamma, \Psi, \Gamma' \prov J$, and $\Gamma \prov \sigma : \Psi$,
then $\Gamma, \Gamma'\theta \prov J\theta$.
\end{lemma}
\begin{proof}
By induction on first the $\Pi$-skeleton structure of $\Psi$ (ignoring the identity of all occurring variables and all embedded substitutions) and subsequently the derivation of $J$.
The interesting cases are:
\begin{itemize}
\item[Case:]
$$
\easyrule
{\Gamma,\Psi,\Gamma' \prov M \tcheck V\{\rho / \Delta\} \qquad \Gamma,\Psi,\Gamma' \prov \rho \tcheck \Delta}
{\Gamma,\Psi,\Gamma' \prov M.\rho \tcheck (\Delta, x : V) }
$$
Reason that
\begin{tabbing}
$\Gamma, \Gamma'\theta \prov \rho\theta \tcheck \Delta\theta$\` i.h.\\
$\Gamma, \Gamma'\theta \prov M \theta \tcheck V\{\rho/\Delta\}\theta$\` i.h.\\
$\Gamma, \Gamma'\theta \prov M \theta \tcheck V\theta\{\rho\theta/\Delta\}$\` Lemma~\ref{interchange}\\
$\Gamma, \Gamma'\theta \prov M \theta \tcheck V\theta\{\rho\theta/\Delta\theta\}$\` Lemma~\ref{simple.type}\\
\end{tabbing}
and form the derivation
$$
\easyrule
{\Gamma,\Gamma'\theta \prov M\theta \tcheck V\theta\{\rho\theta / \Delta\theta\} \qquad \Gamma,\Gamma'\theta \prov \rho\theta \tcheck \Delta\theta}
{\Gamma,\Gamma'\theta \prov M\theta.\rho\theta \tcheck (\Delta\theta, x : V\theta) }
$$

\item[Case:]
$$\easyrule
{ x : \Pi \Delta . v  \in \Gamma,\Psi,\Gamma' \qquad \Gamma,\Psi,\Gamma' \prov \rho : \Delta}
{\Gamma,\Psi,\Gamma' \prov x[\rho] \synth v\{\rho/ \Delta\}}
$$
To show:
$$\Gamma,\Gamma'\theta \prov x[\rho]\theta \synth v\{\rho/ \Delta\}\theta$$

By Lemmas~\ref{interchange} and~\ref{simple.type} it suffices to show
$$\Gamma,\Gamma'\theta \prov x[\rho]\theta \synth v\theta \{\rho\theta/ \Delta\theta\}$$
and we know already by i.h. that
$$\Gamma, \Gamma'\theta \prov \rho\theta \tcheck \Delta\theta$$
If $(\lambda \hat \Delta . R/x:\Pi \Delta . v) \in \theta $,
then by Lemma~\ref{extract} we know we have a derivation that looks like
$$
\easyrule
{\Gamma,\Delta\theta \prov R \tcheck  v\theta}
{\Gamma \prov \lambda \hat \Delta . R \tcheck (\Pi \Delta . v)\theta}$$
and by weakening and i.h. (on $\Delta\theta < \Psi$) and Lemma~\ref{simple.type} we get
$$\Gamma,\Gamma'\theta \prov R\{\rho\theta/\Delta\} \synth v\theta \{\rho\theta/ \Delta\theta\}$$
as required. Otherwise, observe that $(\Gamma,\Gamma')\theta = \Gamma,(\Gamma'\theta)$ by Lemma~\ref{triv.subst},
and form the derivation
$$
\easyrule
{ x : \Pi \Delta\theta . v\theta \in \Gamma,\theta \Gamma' \qquad \Gamma,\Gamma'\theta \prov \rho\theta : \Delta\theta }
{\Gamma,\Gamma'\theta \prov x[\rho\theta] \synth v\theta \{\rho\theta/ \Delta\theta\}}
$$
% &
%x[\rho\theta]&otherwise.
%\cr
%}$$

\end{itemize}
\cqed
\end{proof}

Here is how we define $\eta_V(x)$, the $\eta$-expansion of a variable at a classifier $V$,
and $I_\Psi$, the expanded identity substitution for the context $\Psi$.
$$\eta_{\Pi \Psi . v} (x) = \lambda\hat \Psi . x [I_\Psi]$$
$$I_{\cdot} = \rid \qquad I_{\Psi, x : V} = \eta_V(x) . I_\Psi$$
\begin{lemma}[Unit Laws for $\eta$-expansion]\ 
\begin{enumerate}
\item If $\Gamma \prov R \synth v$, then $R\{I_\Psi / \Psi\} = R$
\item If $\Gamma \prov \rho \tcheck \Delta$, then $I_\Delta\{\rho / \Delta\} = \rho$
\item If $\Gamma \prov \rho \tcheck \Delta$, then $\rho\{I_\Psi / \Psi\} = \rho$
\item If $\Gamma \prov N \tcheck V$, then $N\{I_\Psi / \Psi\} = N$
\item If $\Gamma \prov V \tcheck \rok$, then $V\{I_\Psi / \Psi\} = V$
\item If $\Gamma \prov \Delta \rctx$, then $\Delta\{I_\Psi / \Psi\} = \Delta$
\end{enumerate}
\end{lemma}
\begin{proof}
By induction.
\begin{enumerate}
\item Say $R = x[\rho]$. The interesting case is when $\lambda \hat \Delta . x[I_\Delta]/x:\Pi \Delta . v\in \{I_\Psi / \Psi\}$.
Here we want to show $x[\rho] = x[I_\Delta\{\rho\{I_\Psi/\Psi\} /\Delta\}]$. By one application of i.h. this
is the same as $x[I_\Delta\{\rho /\Delta\}]$, and by another we're done.
\item By typing, of $\rho$ we know that
$$I_\Delta = \eta_{V_1}(x_1).\ldots.\eta_{V_n}(x_n).\rid$$
$$\rho = \lambda \hat \Psi_1 . R_1, \ldots, \lambda \hat \Psi_n . R_n . \rid$$
supposing that $V_i = \Pi \Psi_i . v_i$. We want to show
$$(\eta_{V_1}(x_1).\ldots.\eta_{V_n}(x_n).\rid)\{\rho / \Delta\} = \rho$$
so it suffices to show
$$\eta_{V_i}(x_i)\{\rho / \Delta\} = \lambda \hat\Psi_i . R_i$$
Let's carry out the eta-expansion on the left:
$$\lambda \hat\Psi_i . x_i[I_{\Psi_i}]\{\rho / \Delta\}$$
We know that $\lambda \hat \Psi_i / x : V_i \in \{\rho/\Delta\}$, so this is
$$\lambda \hat\Psi_i . R_i\{I_{\Psi_i}\{\rho / \Delta\}/\Psi_i\}$$
However, $FV(I_{\Psi_i}) \cap \hat \Delta = \emptyset$, so this is
$$\lambda \hat\Psi_i . R_i\{I_{\Psi_i}/\Psi_i\}$$
which by induction hypothesis is
$$\lambda \hat\Psi_i . R_i$$
as required.
\item Straightforward.
\item Straightforward.
\item Straightforward.
\item Straightforward.
\end{enumerate}

\cqed
\end{proof}
\begin{lemma}[Identity]
Suppose $\prov \Gamma \rctx$.
\begin{enumerate}
\item If $x : V \in \Gamma$, then $\Gamma \prov \eta_V(x) \tcheck V$.
\item If $\Gamma\prov \Psi \rctx$, then $\Gamma, \Psi \prov I_\Psi \tcheck \Psi$.
\end{enumerate}
\end{lemma}
\begin{proof} By induction.
\begin{enumerate}
\item
Form the derivation
$$
\easyrule
{\[
x : \Pi \Psi . v \in \Gamma \qquad \Gamma,\Psi \prov I_\Psi \tcheck \Psi
\justifies
\Gamma,\Psi \prov  x [I_\Psi] \tcheck  v\{I_\Psi / \Psi\}
\]}
{\Gamma \prov \lambda\hat \Psi . x [I_\Psi] \tcheck \Pi \Psi . (v\{I_\Psi / \Psi\})}
$$
which by the previous lemma is as required.
\item The empty context case is immediate. Otherwise, form the derivation
$$
\easyrule
{
\Gamma, \Psi, x : V \prov \eta_V(x) \tcheck V \{I_\Psi / \Psi\}\qquad
\Gamma, \Psi \prov I_\Psi \tcheck \Psi
}
{\Gamma, \Psi, x : V \prov \eta_V(x) . I_\Psi \tcheck \Psi, x : V}
$$
from uses of the i.h. and previous lemma.
\end{enumerate}
\cqed
\end{proof}
\end{document}