chap-binders.tex

\chapter{Variables, Binders, and Assumptions}
\label{chap:binders}
So far we have considered the representation of a simple language with
arithmetic expressions and booleans together with proofs about it. In this
chapter, we grow this language to include variables, functions, and function applications,
or more generally constructs that allow us to abstract over
variables. We begin by considering a small fragment of the
lambda-calculus where we define terms using variables, function
abstraction, and function application. We refer the reader to for
example \citep[Ch 5, Ch 9]{TAPL} for a more detailed introduction.

\[
\begin{array}{ll@{\bnfas}l}
\mbox{Terms} & M, N & x \bnfalt \lam x.M \bnfalt M \app N
\end{array}
\]

The main question we are interested in here is the following: how do we
represent this grammar in an proof assistant or programming environment? Clearly, we need to
face the issue of representing variables.

The most straightforward answer to this question is to use a standard "named" representation of
$\lambda$-terms, where variables are treated as labels or strings. In
this approach, one has to explicitly handle $\alpha$-conversion when
defining any operation on the terms. The standard Variable Convention
of Barendregt, which is often employed in on-paper proofs, is one such
approach where $\alpha$-conversion is applied as needed to ensure
that:

\begin{enumerate}[(i)]
\item bound variables are distinct from free variables, and
\item all binders bind variables not already in scope.
\end{enumerate}

In practice this approach is cumbersome, inefficient, and often error-prone. It
has therefore led to the search for different representations of such
terms. Many such approaches exist; see \cite{Aydemir:TechReport09} for
a good overview. Here we will focus on two of them:

\begin{itemize}
\item De Bruijn indices: As the name indicates, this approach
  goes back to Nicolaas Govert de Bruijn who used it in the
  implementation of Automath. Automath was a formal language in the
  60s, developed for expressing complete mathematical theories in such a way
  that an included automated proof checker can verify their
  correctness. De Bruijn indices are also fundamental to more advanced
  techniques such as \emph{explicit substitutions}
  \citep{Abadi:POPL90}.

\item Higher-order abstract syntax
  \citep{Pfenning88pldi}\index{Higher-order abstract syntax}: an appeal to
  higher-order representations where the binders are modelled using
  functions. These functions are typically very weak: they only model the
  scope of variables in an abstract syntax tree, not allowing for recursion or pattern
  matching. In such representations, the issues of
  $\alpha$-equivalence, substitution, etc. are identified with the
  same operations in a meta-logic.
\end{itemize}

\todo{I don't think these descriptions would mean much, if anything at all, to
	the desired audience reading this book. They certainly didn't make much sense
	to me on the first read. -ah}

It is worth pointing out that although we may prefer one of these two
representations for modelling binders in a proof and programming environment, the named
representation of $\lambda$-terms has one important advantage: it can be
immediately understood by others because the variables can be
given descriptive names. Thus, even if a system uses de Bruijn indexes
internally, it will present a user interface with names.


% \paragraph{Alternative name representations:}
% De Bruijn indexes are not the only representation of binders that
% obviates the problem of $\alpha$-conversion. Among named
% representations, the nominal approaches of Pitts and Gabbay
% \cite{Gabbay:LICS99} is one approach, where the representation of a
% binder is treated as an equivalence class of all terms rewritable to
% it using variable permutations. This approach is taken by the Nominal
% Datatype Package of Isabelle/HOL.

% When reasoning about the meta-theoretic properties of a deductive
% system in a proof assistant, it is sometimes desirable to limit
% oneself to first-order representations and to have the ability to
% (re)name assumptions. The locally nameless approach
% \cite{Aydemir:POPL08} uses a mixed representation of variables - De Bruijn indexes for bound variables and
% names for free variables - that is able to benefit from the
% $\alpha$-canonical form of De Bruijn indexed terms when appropriate.


\section{De Bruijn Indices}\label{sec:debruijn}

De Bruijn's idea was that we can represent terms more
straightforwardly and avoid issues related to $\alpha$-renaming by
choosing a canonical representation of variables. Variable occurrences
point directly to their binders rather than referring to them by
name. This is accomplished by replacing named variables by natural
numbers where the number $k$ stands for ``the variable bound by the
$k$th enclosing $\lambda$''.

Here are some examples:

\[
\begin{array}{l@{\qquad}l}
\lam x. x  & \lamdb 1 \\
\lam x. \lam y . x\;y & \lamdb\; \lamdb 2\; 1\\
\lam x. (\lam y. x \; y)\; x & \lamdb (\lamdb 2\;1) \;1
\end{array}
\]

De Bruijn representations are common in compiler and theorem proving
systems which rely on canonical representation of terms. They are
however tedious to manage. In particular, the same variable may have
different indices depending on where it occurs! This can make term
manipulations extremely challenging.

We can define a grammar for de Bruijn terms more formally as

\[
\begin{array}{ll@{\bnfas}l}
\mbox{Indices}         & I    & 1 \bnfalt \shift I \\
\mbox{De Bruijn Terms} & T, S & I \bnfalt \lamdb T \bnfalt T \app S
\end{array}
\]

The index $3$ is represented as $\shift (\shift 1)$. The distinction
between indices and de Bruijn terms is not really necessary; often we
see the following definition:
\[
\begin{array}{ll@{\bnfas}l}
\mbox{De Bruijn Terms} & T, S & 1 \bnfalt \shift T \bnfalt \lamdb T \bnfalt T \app S
\end{array}
\]

This allows us to shift arbitrary de Bruijn terms. Intuitively, the
meaning of shifting $\shift (\lamdb 1 \app 2)$ is that we increase by 1 all free
variable indices in this term and the result would be $\lamdb 1 \app 3$. We leave
out the exact definition of shifting arbitrary terms (see \cite{TAPL}
for details).
% \todo{It's now commented out -am}


% \section{Translating lambda-terms to de Bruijn}

Let us first consider the translation between lambda-terms and their
corresponding de Bruijn representation.

\begin{center}
\begin{tabular}{l@{ : }p{9cm}}
\fbox{$\Gamma \vdash M \Translates T$} & Term $M$ with the free variables
    in $\Gamma$ is translated to the de Bruijn representation $T$
\end{tabular}
\end{center}
% We can then define this translation using the following inference rules:
\[
\begin{array}{l@{\quad}l}
\infer[\TrLam]{\Gamma \vdash \lam x. M \Translates \lamdb S}{\Gamma,x \vdash M \Translates S} &
\infer[\TrApp]{\Gamma \vdash M \app N \Translates T \app S}
      { \Gamma \vdash M \Translates T &
        \Gamma \vdash N \Translates S}\\[1em]
\infer[\TrTop]{\Gamma, x \vdash x \Translates 1}{} &
\infer[\TrNext]{\Gamma, y \vdash x \Translates \shift I}
      { \Gamma \vdash x \Translates I &
        y \neq x}
\end{array}
\]

If we translate a lambda-term in the context $\Gamma$ to its de Bruijn
representation, then the de Bruijn representation is in fact closed,
i.e. it does not contain any variables declared from $\Gamma$.
\unsure{This is unclear: translating x |- x gives 1, which is not
closed, is it? -am It is, since 1 is a number. -bp}

To translate a de Bruijn term to a lambda-term, we accumulate
variables in a context and we look up the position of a variable in
it.

% \subsection*{Substitution} Substitution for de Bruijn terms is tedious
% and crucially relies on properly shifting variables.


% $\ShiftBy n c T$ means we shift all free variables in T (i.e. all
% variables greater than $c$) by $n$.

% For example, $\shiftn 2 (\lamdb \lamdb 1 \app (2 \app 4))$ should yield
% $(\lamdb \lamdb 1 \app (2 \app 6))$. We assume some simplification rules
% such as: $\shiftn n (\shiftn k I) = \shiftn {n+k} I$

% \[
% \begin{array}{l@{\;=\;}ll}
% \ShiftBy n c I & I  & \mbox{if } k < c \\
%                & \shiftn n I &\mbox{if } k \geq c \\
% \ShiftBy n c (\lamdb T) & \lamdb (\ShiftBy n {(c+1)} T)\\
% \ShiftBy n c (T \app S) & (\ShiftBy n c T) \app (\ShiftBy n c S)
% \end{array}
% \]


% Shifting terms is expensive. Therefore different mechanisms have
% been devised, such as the explicit substitution calculus, where we
% apply substitutions lazily, i.e. only when needed. In the explicit
% substitution calculus we always think of a term $T$ together with a
% simultaneous substitution $\sigma$. Only when we need to compare a term
% $T[\sigma]$ with another term $S[\sigma']$, will we start to apply
% $\sigma$ to $T$ and  apply $\sigma'$ to $S$. However, we will not
% eagerly \change{Reword}apply first compute the result of applying $\sigma$ to the
% term $T$ and similarly compute the result of applying $\sigma'$ to
% $S$. If $T$ and $S$ are large terms, this may require us to traverse
% two large terms; yet, if $T$ and $S$ differ with respect to their top
% symbol, we can detect early, before pushing the substitutions through
% that these two terms are different.



\section{Higher-Order Abstract Syntax}\label{sec:HOAS}
In general, managing binders and bound variables is a major pain. So,
several alternatives have been and are being developed.

\subsection{Representing variables}\label{sec:HOAS-var}
In Beluga (as in Twelf and Delphin), we support higher-order abstract
syntax\index{Higher-order abstract
syntax}: our foundation, called the logical framework LF
\citep{Harper93jacm}, allows us to represent binders via binders in our
meta-language.

For example, we can declare a type \lstinline!term! in Beluga,
which has two constructors.

\begin{lstlisting}
LF term : type =
| app : term  -> term  -> term
| lam : (term -> term) -> term
;
\end{lstlisting}

The constructor \lstinline!app! takes in two arguments; both of them
must be terms. The constructor \lstinline!lam! takes in one
argument which is in fact a function! Note that for simplicity, we do
not represent the type annotation on the function which is present in
our grammar.
%
Let's look at a few examples:
% \begin{center}
%   \begin{tabular}{lp{0.25cm}l}
% On Paper (Object language)     & & LF/Beluga (Meta-language)\\
% $\lam x{:}\Nat.x$ & & \lstinline!lam nat (\x. x)! \\
% $\lam x{:}\Nat \arrow \Bool.\lam y{:}\Nat. x\;y$ & &
% \lstinline!lam (arrow nat bool) (\x. lam nat \y. app x y)! \\
% $\lam w{:}\Nat arrow \Bool.\lam v{:}\Nat. w\;v$ & &
% \lstinline!lam (arrow nat bool) (\x. lam nat \y. app x y)! \\
% $\lam w{:}\Nat. (\lam v{:}\Nat \arrow nat \arrow nat. v\;w) \;w$
% && \lstinline!lam nat (\x. (app (lam (arrow nat (arrow nat nat))!\\
% && ~~~~~\lstinline!                    (\v. app v x)) x))!
%   \end{tabular}
% \end{center}
\begin{center}
\begin{tabular}{l@{\quad}|@{\quad}l}
  On Paper (Object language) & LF/Beluga (Meta-language)\\
  \hline
  $\lam x.x$ & \lstinline!lam \x. x! \\
  $\lam x.\lam y. x \app y$ &
  \lstinline!lam \x. lam \y. app x y! \\
  $\lam w.\lam v. w \app v$ &
  \lstinline!lam \x.lam \y. app x y)! \\
  $\lam w. (\lam v. v \app w) \app w$
  & \lstinline!lam \x. (app (lam \v. app v x) x)!
\end{tabular}
\end{center}

Note that the type of \lstinline!\x. x! is \lstinline!term -> term!. So,
we represent binders  via lambda-abstractions in our
meta-language. This idea goes back to Church. One major advantage is
that we push all $\alpha$-renaming issues to the Beluga developer. It
is not the user's business anymore to manipulate indices or
$\alpha$-convert terms manually; instead, the user inherits these
properties directly from the meta-language. Of course, Beluga developers and
implementors still have to battle with de Bruijn indices and all the issues
around variables.

Why is this great for the user of Beluga (or any other such system such as Twelf, Delphin, Hybrid, etc.)? Not only does this higher-order representation support $\alpha$-renaming, but we also get substitution for free! Why?  The meta-language is itself a lambda-calculus, and like every lambda-calculus it comes with some core properties such as $\alpha$-renaming and $\beta$-reduction. So, if we
have \lstinline!lam \x. lam \y. app x y! and we would like to replace
\lstinline!x! in \lstinline!lam \y. app x y! with the term
\lstinline!lam \z. z!, then we simply say
\lstinline!(\y. lam \y. app x y) (lam \z. z)!, i.e. we apply the
LF-abstraction \lstinline!(\y. lam \y. app x y)! to an argument.

This will come in particularly handy when we are representing our small-step
evaluation rules. Let us recall our rules for evaluating function application.

\[
\begin{array}{c}
\multicolumn{1}{l}{\fbox{$V \Value$}: \mbox{Term $V$ is a value}}\\[1em]
\infer[\VLam]{(\lam x.M) \Value}{}
\\[1em]
\multicolumn{1}{l}{\fbox{$M \Steps N$}: \mbox{Term $M$ steps to term $N$}}
\\[1em]
\infer[\EAppFnStep]{M \app N \Steps M'\;N}{M \Steps M'} \qquad
\infer[\EAppArgStep]{V \app N \Steps V\;N'}{N \Steps N' & V \Value}
\\[1em]
\infer[\EAppBeta]{(\lam x.M) \app V \Steps [V/x]M}{V \Value}
\end{array}
\]

To represent evaluation, we revisit our type families \lstinline!value! and
\lstinline!step! and define four constructors, each one corresponding to one of
the rules in the operational semantics. The representation for $\VLam$, $\EAppArgStep$,
and $\EAppFnStep$ follows the previous ideas and is straightforward. For
representing the rule $\EAppBeta$, we take advantage of the fact that
LF-functions (i.e. \lstinline!M! in \lstinline!lam M! has type
\lstinline!term -> term! and denotes a LF-function!) can be applied to an
argument. Hence, we can model the substitution $[V/x]M$ by simply writing
\lstinline!M V!.

\begin{lstlisting}
LF value : term -> type =
| v_lam : value (lam M)
;

LF step : term -> term -> type =
| e_app_1    : step M M'
             -> step (app M N) (app M' N)
| e_app_2    : step N N' -> value V
              -> step (app V N) (app V N')
| e_app_abs : value V
              -> step (app (lam M) V) (M V)
;
\end{lstlisting}

We can then use these constructors \lstinline!v_lam!, \lstinline!e_app_1!,
\lstinline!e_app_2!, and \lstinline!e_app_abs! to build objects that
correspond directly to derivations using the rules $\VLam$, $\EAppArgStep$,
$\EAppFnStep$, and  $\EAppBeta$. This follows the same principles as in the
previous chapter.

% We can also revisit and prove uniqueness of evaluation and the fact that values
% do not step. The proofs are encoded as recursive functions.

\paragraph{Exercises}$\;$\\
\begin{Exercise}
Extend the language with a let-value-construct.
\end{Exercise}
\begin{Answer}
This exercise needs a solution.
\end{Answer}

\begin{Exercise}
Extend the language with a let-name-construct.
\end{Exercise}
\begin{Answer}
This exercise needs a solution.
\end{Answer}

\begin{Exercise}
Extend the language with a match-construct that pattern matches on numbers.
\end{Exercise}
\begin{Answer}
This exercise needs a solution.
\end{Answer}

\begin{Exercise}
Extend the language with recursion.
\end{Exercise}
\begin{Answer}
This exercise needs a solution.
\end{Answer}


\begin{Exercise}
Extend the proof for uniqueness of evaluation we developed in the
previous Chapter in Section \ref{sec:unique-eval}.
\end{Exercise}
\begin{Answer}
This exercise needs a solution.
\end{Answer}

\subsection{Representing assumptions }\label{sec:HOAS-Assumptions}
We now consider how to represent typing derivations. Recall that we can
represent typing derivations with explicit contexts and without
(i.e. Gentzen-style).

\[
\begin{array}{c@{\qquad}c}
\multicolumn{2}{l}{ \fbox{$M:T$} \quad \mbox{$M$ has type $T$ (implicit contexts)}} \\[1em]
\infer[\TFn^{x,u}]{\lam x.M : T \arrow S}
                 {\hypo{\quad\infer[u]{x:T}{}}{M:S~~}} &
\infer[\TApp]{M\;N : S}{M : T \arrow S & N:T}
\end{array}
\]

We call the rule $\TFn$ parametric in $x$ and hypothetical in $u$.
In the implicit context formulation, we simply reason directly from
assumptions.


\[
\infer[\TFn^{x,u}]{\lam x. \lam y. x \app y : (\Nat \arrow \Nat) \arrow \Nat \arrow \Nat}
{\infer[\TFn^{y,v}]{\lam y.x \app y : \Nat \arrow \Nat}{
 \infer[\TApp]{x \app y : \Nat}
   {\infer[u]{x:\Nat \arrow \Nat}{} &
    \infer[v]{y:\Nat}{}
   }
 }
}
\]

As an alternative, we can re-state the rules using an explicit context for
book-keeping; this also is often useful when we want to state properties about
our system and about contexts in particular. To make the
relationship between the term $M$ and the type $T$ more explicit, we
re-formulate the previous typing rules using the judgment $\Gamma
\vdash \tmhastype M T$, which can be read as ``term $M$ has type $T$
in the context $\Gamma$.''

\[
\begin{array}{c}
\multicolumn{1}{l}{\fbox{$\Gamma \vdash \tmhastype M
    T$}\quad\mbox{Term $M$ has type $T$ in the context $\Gamma$
    (explicit contexts)} }
\\[1em]
\infer[u]{\Gamma \vdash \tmhastype x T}{u:\tmhastype x T \in \Gamma} \qquad
\infer[\TFn^{x,u}]{\Gamma \vdash \tmhastype {(\lam x.M)} {(T \arrow S)}}
                 {\Gamma,x, u:\tmhastype x T \vdash \tmhastype M S}
\\[1em]
\infer[\TApp]{\Gamma \vdash \tmhastype {(M \app N)} S}
             {\Gamma \vdash \tmhastype M (T \arrow S)
  & \Gamma \vdash \tmhastype N T}
\end{array}
\]

It should be intuitively clear that these two formulations of the typing rules
are essentially identical; while the first set of rules uses a two-dimensional
representation, the second set of rules makes the context of
assumptions explicit and provides an explicit rule for looking up variables.

When we encode typing rules as a data-type, the first formulation with implicit
contexts is particularly interesting and elegant. Why? Because we can read the
rule $\TFn$ in the implicit context formulation as follows: $\lam x.M$ has type $T \arrow S$, if given a variable
$x$ and an assumption $u$ that stands for $x:T$ we can show that $M$ has type
$S$, i.e. we can construct a derivation for $M:S$.

Note that ``given $x$ and $u$, we can construct a derivation $M:S$'' is our
informal description of a function that takes $x$ and $u$ as input and returns a
derivation $M:S$. This is a powerful idea, since viewing it as a function
directly enforces that the scope of $x$ and $u$ is only in the derivation for
$M:S$. It also means that if we provide a term $N$ for $x$ and $N:T$ for $u$, we
should be able to return a derivation $M:S$ where every $x$ has been replaced
by $N$ and every use of $u$ has been replaced by the proof that $N:T$. As a
consequence, the substitution lemma that we have proved for typing derivations
can be obtained for free by simply applying the function that stands for ``given
$x$ and $u$, we can construct a derivation $M:S$''.


Let's make this idea concrete. We define a type \lstinline!tp! consisting of the
natural numbers and functions type, and then define the relation \lstinline!hastype! as
a type in LF as follows:

\begin{lstlisting}
LF tp : type = 
| nat : tp
| arr : tp -> tp -> tp
;

LF hastype : term -> tp -> type =
| t_lam : ({x:term} hastype x T -> hastype (M x) S)
          -> hastype (lam M) (arr T S)
| t_app : hastype M1 (arr T S) -> hastype M2 T
          -> hastype (app M1 M2) S
;
\end{lstlisting}

Note that the argument to the constructor \lstinline!t_lam! must be of type
\lstinline!({x:term} hastype x T -> hastype (M x) S)!. We write curly braces
for universal quantification, to more formally express the sentence:
``Given a variable \lstinline!x! and an assumption \lstinline!hastype x T!, we can
construct \lstinline!hastype (M x) S!.''

One might ask, why do we have to write \lstinline!hastype (M x) S! and why can
we not write \lstinline!hastype M S!? Let's look carefully at the types for
each of the arguments. We note that we wrote \lstinline!(lam M)! and we also
know that \lstinline!lam! takes in one argument that has type
\lstinline!term -> term!, i.e. it is an LF-function. Hence writing \lstinline!hastype M S! would be
giving you a type-error, since the relation \lstinline!hastype! expects an
object of type \lstinline!term!, not of type \lstinline!term -> term!.
But is \lstinline!(M x)!? What does it correspond to in the informal rule? In the
informal rule, we required that $x$ is new. It might have been clearer not to
re-use the variable name $x$ that was occurring bound in $\lam
x.M$. We restate our previous rule $\TFn$ where we make the possibly necessary
renaming explicit below.

\[
\begin{array}{c}
\infer[\TFn^{y,u}]{\lam x.M : T \arrow S}
                 {\hypo{\quad\infer[u]{y:T}{}}{[y/x]M:S}}
\end{array}
\]

Here we see that indeed we replace all occurrences of $x$ in $M$ with a new
variable $y$. It is exactly this kind of renaming that is happening, when we
write \lstinline!hastype (M x) S!.
Let us revisit the typing derivation for $\lam x.\lam y.x~y : (\Nat \arrow
\Nat) \arrow \Nat \arrow \Nat$.
\[
\infer[\TFn^{x,u}]{\lam x.\lam y.x~y : (\Nat \arrow \Nat) \arrow \Nat \arrow \Nat}
 {\infer[\TFn^{y,v}]{\lam y.x~y :  \Nat  \arrow \Nat}
           {\infer[\TApp]{x~y :\Nat}
                      {\infer[u]{x: (\Nat \arrow \Nat) }{} &
                        \infer[v]{ y: \Nat }{} &
                      }
                    }
                  }
\]

How would we encode it? First we translate the
typing judgment to representation;
% \lstinline![|-hastype (lam \x.lam \y.app x y) (arrow (arrow nat nat) (arrow nat nat))]!.
then we construct an object of this type that will correspond to the typing
derivation. % for  $\lam x.\lam y.x~y : (\Nat \arrow \Nat) \arrow \Nat \arrow \Nat$.
%

\begin{lstlisting}
let d : [|- hastype (lam \x.lam \y.app x y) (arr (arr nat nat) (arr nat nat))] =
        [|- t_lam \x.\u.t_lam \y.\v.t_app u v];
\end{lstlisting}



\chapter{Proofs by Induction - Revisited}\label{chap:proofs-intermediate}
\section{Type Preservation}\label{chap:proofs-closed-derivations}

Let us revisit the type preservation proof for the functions and
function application, in particular we concentrate on the case for
abstractions.

\begin{theorem}
If $\proofderivc{\D}{~}{\tmhastype M T}$ and $\proofderiv{\S}{M \Steps N}$ then $\vdash N : T$.
\end{theorem}
\begin{proof}
By structural induction on the derivation $\proofderiv{\S}{M \Steps N}$.

\begin{case}{$\S = \ianc{\above{\V}{V \Value}}{(\lam x.M) \app V \Steps [V/x]M}{\EAppBeta}$}
$\proofderivc{~~~~}{~}{\tmhastype {((\lam x.M) \app V)} T}$
\hfill by assumption  \\
$\proofderivc{\D_1}{~}{\tmhastype{(\lam x.M)}{(S \arrow T)}}$ \\
$\proofderivc{\D_2}{~}{\tmhastype V S}$
\hfill by inversion using rule $\TApp$\\
$\proofderivc{\D~}{x, u:\tmhastype x S}{\tmhastype M T}$ \hfill by inversion on $\D_1$ using rule $\TFn$\\
$\proofderivc{~~~~}{~}{\tmhastype {[V/x]M} T}$ \hfill by substitution lemma using $V$ and
$\D_2$ in $\D$.
\end{case}

\end{proof}

The proof below reflects the structure of the proof.
Case-analyzing \lstinline!s! that stands for
\lstinline![|- step M N]! yields three different cases.

The case where
we have  \lstinline![|- e_app_abs V]!
corresponds directly to the case in the proof above that we
wrote out explicitly where \lstinline!V! corresponds to $\V$. We then
use inversion to analyze our assumption
\lstinline![|-hastype (app (lam M) V) T]!. We have written the two
inversion steps as one nested pattern in Beluga. More importantly, the
subderivation $\proofderivc{\D}{u:\tmhastype x S}{\tmhastype M T}$ in the proof is represented as
\lstinline!\x.\u. D! where
\lstinline!D! has type \lstinline!hastype (M x) T! in the context \lstinline!x:term, u:hastype x S!.

Recall that earlier we remarked that the
typing rule for functions does make two assumptions: that we have a
fresh variable \lstinline!x! and an assumption \lstinline!hastype x S!
which we call \lstinline!u! here. In the proof we then replaced all
occurrences of $x$ by the value $V$ and all assumptions $V:S$ are
replaced by the proof $\D_2$.

\begin{small}

\[
\begin{array}{l@{\quad}c@{\quad}l@{\quad}c}
& \qquad\infer[\TFn^{x,u}]
       {\vdash \tmhastype {(\lam x. M)}{(S \arrow T)}}
       {\above{\D^{x,u}}{x, u:\tmhastype x S \vdash \tmhastype M T}} & & \\[1em]
\mbox{replacing $x$ by $V$ in $\D$ yields} &
       {\above{[V/x]\D^u}{u:\tmhastype V S \vdash \tmhastype {([V/x]M)} T}} & \\[1em]
\mbox{replacing $u$ by $\D_2$ in $\D$ yields} &
\above{[\D_2/u, V/x]\D}{\tmhastype {([V/x]M)} T}
\end{array}
\]

\end{small}
% This is how the derivation evolves

% \[
% \begin{array}{c@{\quad}l@{\quad}c}
% \infer[\TFn^{x,u}]
%       {\lam x. M : S \arrow T}
%       {\deduce[\vspace{2pt}]{M:T}
%               {\deduce[\vspace{2pt}]{\D^{x,u}}
%                       {\infer[u]{x:S}{}}}} &
% \mbox{replacing $x$ by $V$ in $\D$ yields} &
% \infer[\TFn^{x,u}]
%       {\lam x. M : S \arrow T}
%       {\deduce[\vspace{2pt}]{[V/x] M:T}
%               {\deduce[\vspace{2pt}]{[V/x]\D^{u}}
%                       {\infer[u]{V:S}{}}}}\\[1em]
% \infer[\TFn^{x,u}]
%       {\lam x. M : S \arrow T}
%       {\deduce[\vspace{2pt}]{[V/x] M:T}
%               {\deduce[\vspace{2pt}]{[V/x]\D^{u}}
%                       {\infer[u]{V:S}{}}}} &
% \mbox{replacing $u$ by $\D_2$ in $\D$ yields} &
% \infer[\TFn^{x,u}]
%       {\lam x. M : S \arrow T}
%       {\deduce[\vspace{2pt}]{[V/x] M:T}
%               {\deduce[\vspace{2pt}]{[V/x][\D_2/u]\D}
%                       {\deduce[\vspace{2pt}]{V:S}{\D_2}}}}
% \end{array}
% \]

In \beluga where substitutions are first-class, we simply associate the derivation $\D$ with the substitution \lstinline![_, D2]!; the underscore stands for the value $V$ whose name is not explicitly available in the program. Beluga's type
reconstruction will however make sure that that the underscore is
exactly the value \lstinline!D2! refers to.


\begin{lstlisting}
rec tps: [ |- hastype M T] -> [ |- step M N] -> [ |- hastype N T] =
/ total s (tps m t n d s)/
fn d => fn s => case s of
| [ |- e_app_1 S1] =>
  let [ |- t_app D1 D2] = d in
  let [ |- F1] = tps  [ |- D1] [ |- S1] in
    [ |- t_app F1 D2 ]

| [ |- e_app_2 S2 _ ] =>
  let [ |- t_app D1 D2] = d in
  let [ |- F2] = tps  [ |- D2] [ |- S2] in
    [ |- t_app D1 F2]

| [ |- e_app_abs V] =>
  let [ |- t_app (t_lam \x.\u. D) D2] = d in
    [ |- D[_,  D2]]
;
\end{lstlisting}


\section{Type Uniqueness}\label{chap:proofs-open-derivations}
We also sometimes prove properties that hold only for non-empty
contexts. One such example is proving type uniqueness. In fact, this property does not hold unless we add some type annotations. So far we have
been working with lambda-terms $\lambda x.M$. However, consider the identity function $\lambda x.x$ - it has many types, not just one. However, annotating the variable bound by a lambda-abstractions will be sufficient to guarantee that every lambda-term has a unique type.

We therefore also revise our definition of terms and typing rules slightly,
highlighting the new parts in green. Finally we define type equality
explicitly using reflexivity.

\begin{lstlisting}
LF term : type =
| app : term  -> term  -> term
| lam : <<tp>> ->(term -> term) -> term
;

LF hastype: term -> tp -> type =
| t_lam : ({x:term} hastype x T -> hastype (M x) S)
	-> hastype (lam <<T>> M) (arr T S)
| t_app:  hastype M1 (arr T S) -> hastype M2 T
	-> hastype (app M1 M2) S
;

LF eq: term -> term -> type =
| refl: eq  M M ;
\end{lstlisting}

Let us now revisit the proof of type uniqueness. Note that as we traverse
abstractions, we are collecting assumptions about variables and their
types. We are therefore not able to prove every term has a unique type
in the empty context, but must state it more generally. To do so, we
silently revert to an explicit context formulation of our typing
rules, since this proves to be more convenient. To make the structure
of the proof even more apparent, we already use our LF encoding to
describe our typing judgments. This will also make the translation of
this proof into a Beluga program much easier.
\label{sec:thmunique}
\begin{theorem}[Type uniqueness]$\;$\\
If $\proofderivc{\D}{\Gamma}{\tmhastype M T}$ and $\proofderivc{\C}{\Gamma}{\tmhastype M S}$
then $\tmeq T S$.
\end{theorem}
\begin{proof}
By structural induction on the typing derivation $\proofderivc{\D}{\Gamma}{\tmhastype M T}$.


\begin{case}{$\D = \inferaa
            {\TApp}
            { \Gamma \vdash \tmhastype {(\tmapp M N)} S}
            { \deduce[\vspace{2pt}]{\Gamma \vdash \tmhastype M {(\tmarr T S)}}{\D_1}}
            { \deduce[\vspace{2pt}]{\Gamma \vdash \tmhastype N T}{\D_2}}$}
$\C = \inferaa
            {\TApp}
            { \Gamma \vdash \tmhastype {(\tmapp M N)} S'}
            { \deduce[\vspace{2pt}]{\Gamma \vdash \tmhastype M {(\tmarr {T'} S')}}{\C_1}}
            { \deduce[\vspace{2pt}]{\Gamma \vdash \tmhastype N T'}{\C_2}}$
\\[2em]
\noindent
$\proofderiv{\E}{\tmeq {(\tmarr T S)} {(\tmarr T' S')}}$ \hfill by i.h. using $\D_1$ and $\C_1$ \\
$\proofderiv{\E}{\tmeq {(\tmarr T S)} {(\tmarr T S)}}$  \; and \; \emphFact{$S = S'$} \; and \; \emphFact{$T=T'$} \hfill by inversion on reflexivity.\\[1em]

Therefore there is a proof for $\tmeq S S'$ by reflexivity (\emphFact{since we know $S=S'$}).
\end{case}

\begin{case}{$\D = \infera{\TAbs}
   {\Gamma \vdash \tmhastype {(\tmlam x T M)} {(\tmarr T S)}}
   {\deduce[\vspace{2pt}]{\Gamma, x, u : \tmhastype x T \vdash \tmhastype M S}{\D_1}}$}
$ \C = \infera{\TAbs}
   {\Gamma \vdash \tmhastype {(\tmlam x T M)} {(\tmarr T S')}}
   {\deduce[\vspace{2pt}]{\Gamma, x, u : \tmhastype x T \vdash \tmhastype M S'}{\D_1}}
$\\[2em]
\noindent
$\proofderiv{\E}{\tmeq S S'}$ \hfill by i.h. using $\D_{1}$ and $\C_1$ \\
$\proofderiv{\E}{\tmeq S S}$ \quad and \quad \emphFact{$S = S'$} \hfill by inversion using reflexivity\\[1em]
%ause

Therefore there is a proof for $\tmeq {(\tmarr T S)} {(\tmarr T S')}$ by reflexivity.
\end{case}

\begin{case}{
    $\D = \infera{u} {\Gamma \vdash \tmhastype x T}
    {x, u : \tmhastype x T \in \Gamma}$ \qquad
    $\C = \infera{v}{\Gamma \vdash \tmhastype x S}
    {x, v : \tmhastype x S \in \Gamma}$
}
Every variable $x$ is associated with a unique typing assumption
(\emphFact{property of the context}), hence $v = u$ and $S = T$.
\end{case}

\end{proof}

There are a number of interesting observations we can make about this
proof:

\begin{itemize}
\item We rely on the fact that every assumption is unique and there
  are not two assumptions about the same variable; this is in fact
  implicitly enforced in the rule $\TAbs$ where we ensure
  that the variable is new.
\item We extend our context in the rule $\TAbs$.
\item We reason about equality using reflexivity. We note that by
  using our rule \lstinline!refl!, we are able to learn that two types
  are actually the same (i.e. $T = T'$).
\item We have an explicit variable (base) case, as we stated our judgments
  within a context $\Gamma$.
\end{itemize}


The encoding of this proof is in fact straightforward in Beluga thanks to the support provided. We
first describe the shape (i.e. type) of our context using a
\emph{schema declaration}. Just as types classify terms, schemas
classify contexts. We observe that in our typing rules, we always
introduce a variable $x$ and the assumption $\tmhastype x T$ at the same
time.
To denote that these two assumptions always come in pairs, we
write the keyword \lstinline!block!.\index{Context Schema}

\begin{lstlisting}
schema tctx = some [t:tp] block (x:term,u:hastype x t);
\end{lstlisting}

The schema \bel{tctx} describes a context containing assumptions
\bel{x:term}, each associated with a typing assumption \bel{hastype x t}
for some type \bel{t}.  Formally, we are using a dependent product $\Sigma$
(used only in contexts) to tie \bel{x} to \bel{hastype x t}.
We thus do not need to establish separately that for every variable there is a
unique typing assumption: this is inherent in the definition of \bel{tctx}.
The schema classifies well-formed contexts and checking whether a
context satisfies a schema will be part of type checking. As a
consequence, type checking will ensure that we are manipulating only
well-formed contexts, that later declarations overshadow previous
declarations, and that all declarations are of the specified form.

To illustrate, we show some well-formed  and some ill-formed
contexts.

\begin{small}
\begin{center}
\begin{tabular}{p{8.65cm}@{}|@{~}p{6.25cm}}
%\multicolumn{1}{c}{Context} & \multicolumn{1}{c}{Is of schema
%  \lstinline!tctx!?}\\
\hspace{2cm}Context & \hspace{1.5cm}Is of schema \lstinline!tctx!?\\
\hline
\lstinline!b1:block(x:term,u:hastype x (arr nat nat)),!\newline\lstinline!b2:block(y:term,u:hastype y nat)!
& yes \\ \hline
\lstinline!x:term, u:hastype x (arr nat nat)! & no (not grouped in blocks)
\\\hline
\lstinline!y:term! & no; typing assumption for \lstinline!y! is missing\\\hline
\lstinline!b:block(x:term,u:hastype y nat)! & no (\lstinline!y! is free) \\
\hline
\lstinline!b1:block(x:term,u:hastype x (arr nat nat)),!\newline\lstinline!b2:block(y:term,u:hastype x nat)!
& no (wrong binding structure)
\end{tabular}
\end{center}
\end{small}


Let us now show the type of a recursive function in Beluga which
corresponds to the type uniqueness theorem.


\begin{lstlisting}[caption={Type Uniqueness Proof},label=list:8-6,captionpos=b,float,abovecaptionskip=-\medskipamount]
rec unique:(\gamma:tctx)[\gamma |-hastype M T[] ] -> [\gamma |-hastype M S[] ] -> [ |-equal T S] =
/ total d (unique _ _ _ _ d) /
fn d => fn f => case d of
| [\gamma |-t_app D1 D2] =>
  let[\gamma |-t_app F1 F2] = f in
  let[ |-ref]  = unique  [\gamma |-D1] [\gamma |-F1] in
    [ |-ref]

|[\gamma |-t_lam \x.\u. D] =>
  let[\gamma |-t_lam \x.\u. F] = f in
  let[ |-ref] = unique [\gamma,b:block(x:term,u:hastype x _)|-D[.. b.1 b.2] ]
                      [\gamma,b$\,$|-F[.. b.1 b.2] ] in
   [ |-ref]

| [\gamma |-#q.2] =>         % d : hastype #q.x T
  let[\gamma |-#r.2] = f  in  % f : hastype #q.x T'
    [ |-e_ref]
;
\end{lstlisting}


We can read this type as follows: For every context \lstinline!\gamma! of
schema \lstinline!tctx!, given a derivation for
\lstinline!hastype M T[]! in the context \lstinline!\gamma! and a derivation for
\lstinline!hastype M S[]! in the context \lstinline!\gamma!, we return a
derivation showing that \lstinline!eq T S! in the empty context.
Although we quantified over the context \lstinline!\gamma! at the outside,
it need not be passed explicitly to a function of this type, but
Beluga will be able to reconstruct it.

We call the type \lstinline![\gamma |-hastype M T[] ]! a contextual type and
the object inhabiting it a contextual object.
The term \lstinline!M! can depend on the variables declared in the
context \lstinline!\gamma!. Implicitely, all meta-variables occurring inside \lstinline![ ]! are associated with a post-poned substitution which can be omitted, if the substitution is the identity substitution (which can be written as \lstinline!..!). Hence, writing simply \lstinline!M! in the context $\gamma$, is equivalent to writing \lstinline!M[..]!. Why are meta-variables such as \lstinline!M! associated with post-poned substitutions? - Intuitively,
\lstinline!M! itself is a contextual object of type
\lstinline![\gamma |-term]! and \lstinline!..! is the identity substitution
which $\alpha$-renames the bound variables.
On the other hand, \lstinline!T! and \lstinline!S! stand for closed
objects of type \lstinline!tp! and they cannot refer to declarations
from the context \lstinline!\gamma!. Their declared type is \lstinline![|- tp]!. To use an object of type \lstinline![|-tp]! in a context $\gamma$, we need to weaken it. This is what we express in the statement by writing \lstinline!T[]! and \lstinline!S[]!. Here \lstinline![]! denotes a weakening substitution from the empty context to $\gamma$.
Note that these subtleties were not
captured in our original informal statement of the type uniqueness
theorem.

We subsequently omit writing weakening substitutions as they clutter the explanation and we should be in principle able to infer them.
We consider each case individually. Each case in the proof on page
\pageref{sec:thmunique} will correspond to one case in the
case-expression.
%
\paragraph{Application case:} If the first derivation \lstinline{d} concludes
with \lstinline{t_app}, it matches
the pattern \lstinline![\gamma |-t_app D1 D2]!, and is
a contextual object of type
\lstinline!hastype (app M N)$~$S! in the context \lstinline!\gamma!.  % We therefore know that
% $\lstinline{M$\;$..} =
% \lstinline{app$\;$(M$\;$..)\,(N$\;$..)}$.
\lstinline!D1! corresponds to the first
premise of the typing rule for applications and has the contextual type
\lstinline![\gamma |-hastype M (arr T S)]!.

Using a let-binding, we invert the second
argument, the derivation \lstinline{f} which
must have type
\lstinline![\gamma |-hastype (app M N)$~$ S']!. \lstinline!F1!
corresponds to the first premise of the typing rule for applications
and has type \lstinline![\gamma |-hastype M (arr T' S')]!.
The appeal to the induction hypothesis using \lstinline{D1} and \lstinline{F1} in the
on-paper proof
corresponds to the recursive call
 \lstinline!unique [\gamma |-D1] [\gamma |-F1]!.
Note that while \lstinline!unique!'s type says it takes a context variable \lstinline!{\gamma:tctx}!,
we do not pass it explicitly; Beluga infers it from the context in the first argument
passed.
The result of the recursive call is a contextual object of type
\lstinline![ |-eq (arr T S) (arr T' S')]!. The only rule that
could derive such an object is \lstinline{ref}, and pattern matching
establishes that \lstinline!arr T S!$=$\lstinline!arr T' S'! and hence
\lstinline!T! $=$ \lstinline!T'! and \lstinline!S! $=$ \lstinline!S'!.
Therefore, there is a proof of \lstinline![ |-eq S S']! using the
rule \lstinline!ref!.

 \paragraph{Abstraction case:}
  If the first derivation \lstinline{d} concludes with \lstinline{t_lam}, it matches
 the pattern \lstinline{[\gamma |-t_lam \x.\u.D]}, and is
 a contextual object in the context \lstinline!\gamma! of type
 \lstinline{hastype (lam T (\x.M))$~$(arr T S)}.
 %Thus, $\lstinline{M$\;$..} = \lstinline{lam$\;$T1$\;$($\lam$x.$\;$M0$\;$..$\;$x)}$
 % and $\lstinline{T} = \lstinline{arr$\;$T1$\;$T2}$.
 Pattern matching---through a let-binding---serves to invert the second derivation \lstinline{f}, which
 must have been by \lstinline{t_lam} with a subderivation
 \lstinline{F1} deriving \lstinline{hastype M S'} that can use \lstinline{x},
 \lstinline{u:hastype x T}, and assumptions from \lstinline!\gamma!\footnote{More precisely, \lstinline!F1! has type \lstinline!hastype M[..,x] S'[]!.}.
 %Hence, after pattern matching on \lstinline{d} and \lstinline{f}, we know that
 %$\lstinline{M} = \lstinline{lam~T1$\;$($\lam$x.$\;$M$\;$..x}$\lstinline{)} and
 %$\lstinline{T} = \lstinline{arr T1 T2}$ and $\lstinline{T'} = \lstinline{arr T1 T2'}$.

 The use of the induction hypothesis on \lstinline{D} and \lstinline{F} in a paper proof
 corresponds to the recursive call to \lstinline{unique}.  To appeal to the
 induction hypothesis, we need to extend the context by pairing up \lstinline{x} and
 the typing assumption \lstinline!hastype x T!. This is accomplished by creating
 the declaration \lstinline!b:block x:term,u:hastype x T!.  In the
 code, we wrote an underscore \lstinline!_! instead of \lstinline{T},
 which tells Beluga to reconstruct it.  (We cannot write \lstinline{T} there without binding it by
 explicitly giving the type of \lstinline{D}, so it is easier to write \lstinline!_!.)
 To retrieve \lstinline{x} we take the first projection
 \lstinline{b.1}, and to retrieve \lstinline{x}'s typing assumption we take the second projection \lstinline{b.2}.

 Now we can appeal to the induction hypothesis using
 \lstinline!D1[.., b.1, b.2]! and \lstinline!F1[.., b.1, b.2]! in the context
 \lstinline!g,b:block x:term,u:hastype x T1!. Note that we apply explicitly the substitution \lstinline!.., b.1, b.2! which allows us to transport a derivation \lstinline!D1! in the context \lstinline!\gamma, x:term, u:hastype x T1! to a derivation in the context \lstinline!\gamma, b:block(x:term, u:hastype x T1)!.
  From the i.h.\ we get a
 contextual object, a closed derivation of
 \lstinline![|-equal (arr T S) (arr T S')]!. The only rule that could
 derive this is \lstinline{ref}, and pattern matching establishes that \lstinline{S}
 must equal \lstinline{S'}, since we must have \lstinline!arr T S!$ =$
\lstinline!arr T1 S'!.  Therefore, there is a proof of
\lstinline![ |-equal S S']!,
 and we can finish with the reflexivity rule \lstinline{ref}.

 \paragraph{Assumption case:} Here, we must have used an assumption from the
 context \lstinline!\gamma! to construct the derivation \lstinline{d}.  Parameter variables
  allow a generic case that matches a declaration
\lstinline!block x:term, u:hastype x T! for any \lstinline{T} in \lstinline!\gamma!. Since our pattern match
 proceeds on typing derivations, we want the second component of the
 parameter \lstinline{#q}, written as \lstinline{#q.2} or \lstinline!#q.u!.  The pattern match on \lstinline{d}
 also establishes that \lstinline{M = #q.1} (or \lstinline!M = #q.x!).
 % and \lstinline{S = T}.
 Next, we pattern match on \lstinline{f}, which has type
\lstinline!hastype #q.1 S! in the context \lstinline!\gamma!.  Clearly, the only
 possible way to derive \lstinline{f} is by using an assumption from \lstinline!\gamma!. We call
 this assumption \lstinline{#r}, standing for a declaration
\lstinline!block y:term,u:hastype y S!, so \lstinline{#r.2} refers to the second component
\lstinline!hastype #r.1 S!. Pattern matching between \lstinline{#r.2} and \lstinline{f}
 also establishes that % both types are equal and that \lstinline{S' = T'} and
 \lstinline{#r.1 = #q.1}.  Finally, we observe that \lstinline{#r.1 = #q.1} only if
 \lstinline{#r} is equal to \lstinline{#q}. We can only instantiate the parameter
 variables \lstinline!#r! and \lstinline!#q! with bound variables from
 the context or other parameter variables. Consequently, the only
 solution to establish that \lstinline{#r.1 = #q.1} is the one where both the
 parameter variable \lstinline!#r! and the parameter variable
 \lstinline!#q! refer to the same bound variable in
 the context \lstinline!g!.  Therefore, we must have
 \lstinline!#r = #q!, and both
 parameters must have equal types, and \lstinline{S = S' = T = T'}.  (In general,
 unification in the presence
 of $\Sigma$-types does not yield a unique unifier, but in Beluga only
 parameter variables and variables from the context can be of $\Sigma$ type,
 yielding a unique solution.)




\chapter{Program Transformations }
\section{Translation of de Bruijn Terms to HOAS Terms}
We return here to the beginning of Chapter \ref{chap:binders} where we discussed two different representations for lambda-terms, namely using de Bruijn representation and using higher-order abstract syntax (HOAS). In Section \ref{sec:debruijn}, we defined de Bruijn terms and also showed how to translate lambda-terms in HOAS to their corresponding de Bruijn representation. Here, we implement de Bruijn terms and write a total function for the translation of lambda-terms in HOAS to their corresponding  de Bruijn representation.  To contrast we repeat our definition of lambda-terms using HOAS on the left and define de Bruijn terms on the right.

\begin{minipage}[t]{7cm}
\begin{lstlisting}
LF term   : type =
| app   : term  -> term  -> term
| lam   : (term -> term) -> term;
  \end{lstlisting}
\end{minipage}
\begin{minipage}[t]{7cm}
\begin{lstlisting}
LF dBruijn   : type =
| one    : dBruijn
| shift  : dBruijn  -> dBruijn
| lam'   : dBruijn  -> dBruijn
| app'   : dBruijn  -> dBruijn  -> dBruijn;
\end{lstlisting}
\end{minipage}

The translation from \lstinline!term! to \lstinline!deBruijn! is naturally recursive and as we travers a \lstinline!term!, we will go under binders. Hence, our translation must translate a \lstinline!term! in the context $\gamma$ to \lstinline!deBruijn! (see also Sec. \ref{sec:debruijn}).
We hence first define the shape and structure of our context $\gamma$. This is
simply done by : \lstinline!schema ctx = term ; !


Here \lstinline!ctx! is the name of a context schema and we declare
contexts to be containing only declarations of type \lstinline!term!.
We can now turn our inference rules defining how to translate
lambda-terms to de Bruijn terms into a recursive program:


\begin{lstlisting}
rec vhoas2db : {\gamma:ctx}{#p:[\gamma |-term]}  [ |-dBruijn] =
 / total \gamma (vhoas2db \gamma  ) /
mlam \gamma => mlam #p =>  case [\gamma] of
| [] => impossible [ |-#p ]
| [\gamma', x:term] => (case [\gamma', x:term |-#p ] of
 | [\gamma',x:term |-x] => [ |-one ]
 | [\gamma',x:term |-#q[..] ] =>
   let [ |-Db] = vhoas2db [\gamma'] [\gamma' |-#q] in
     [ |-shift Db])
;

rec hoas2db : (\gamma:ctx) [\gamma |-term] ->  [ |-dBruijn ] = / total e ( hoas2db _  e) /
 fn e =>  case e of
  | [\gamma |-#p ] => vhoas2db [\gamma] [\gamma |-#p]

 | [\gamma |-lam \x.M] =>
   let [ |-F] =  hoas2db  [\gamma,x:term |- M] in
     [ |-lam' F ]

 | [\gamma |-app M1 M2] =>
   let [ |-F1] = hoas2db  [\gamma |- M1]  in
   let [ |-F2] = hoas2db  [\gamma |- M2]  in
     [ |-app' F1 F2]
;
\end{lstlisting}

The type of the program reads as follows: Given a context
\lstinline!\gamma! of schema \lstinline!ctx!, and given an object of type
\lstinline!term! in the context \lstinline!\gamma!, we return an object
\lstinline!dBruijn! which is closed.

The type system will ensure we never work with variables outside their
scope; it will also ensure that we produce a closed de Bruijn term.

Let us look at the easy cases first, for example the case
\lstinline![\gamma |-app M1 M2]!.  We note again that by default \lstinline!M1! and \lstinline!M2! can depend on the variables declared in the context $\gamma$.

So, to translate \lstinline![\gamma |- app M1 M2]! we recursively
translate \lstinline![\gamma |- M1]! and \lstinline![\gamma |- M2]!. Each
recursive call will produce a closed de Bruijn term, namely
\lstinline![|-F1] ! and \lstinline![|-F2]!, which we can use to
re-assemble our proper de Bruijn term \lstinline![|-app' F1 F2]!.

When we translate a lambda-term, we must extend the context.


Finally, we must consider the variable cases. We implement the variable case using a separate function \lstinline!vhoas2db! whose type can be read as: For all $\gamma:$\lstinline!ctx! and for all parameters (variables) \lstinline!#p:[\gamma |- term]! there exists a \lstinline!deBruijn! term. \index{Quantification over parameter variables} We note that the algorithm in Section \ref{sec:debruijn}
took advantage of the shape of the context; for
example, we really took the context for being ordered. The same thing
happens in Beluga. We can match on the shape of contexts.

We implement the function \lstinline!vhoas2db! by pattern matching on the context $\gamma$. If the context is empty, then there are no variables and hence there is no \lstinline!#p!. If the context is not empty but has the shape \lstinline!\gamma', x:term!, we continue pattern matching on \lstinline!#p!. There are two possible cases for \lstinline!#p!:\index{Pattern matching on context}\index{Pattern matching on parameters}
\begin{enumerate}
\item \lstinline!#p! stands for \lstinline!x!, written as \lstinline![\gamma', x:term |- x]!. In this case we simply return \lstinline!one!.
\item \lstinline!#p! stands for a variable from $\gamma'$, written as \lstinline![\gamma', x:term |- #q[..]]!. Note that we associate \lstinline!#q! with the weakening substitution \lstinline!..! that provides a map from a context $\gamma'$ to the context \lstinline!\gamma', x:term!. Therefore, \lstinline!#q! can only be instantiated with a variable from \lstinline!\gamma'!, but not \lstinline!x!. In this latter case, we recursively call \lstinline!vhoas2db! on \lstinline!\gamma'! and \lstinline![\gamma' |- #q]! and shift the result.
\end{enumerate}




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