%%%
%%%
%%%

\documentclass[copyright,creativecommons]{eptcs}
\providecommand{\event}{LFMTP 2010} % Name of the event you are submitting to
\usepackage{breakurl}             % Not needed if you use pdflatex only.

\newcommand{\thenetherlands}{%%% 
The Netherlands}

\newcommand{\ourinstitute}{%%% 
Radboud University Nijmegen}

\newcommand{\ouraffiliation}{%%% 
Institute for Computing and Information Sciences \\
Heyendaalseweg 135, 6525 AJ Nijmegen\\
\thenetherlands}

\newcommand{\tueinstitute}{%%% 
Technical University Eindhoven\\
\thenetherlands}


\newcommand{\ourtitle}{%%% 
Pure Type Systems without Explicit Contexts}

\title{\ourtitle}

\def\titlerunning{\ourtitle}
\def\authorrunning{H. Geuvers, R. Krebbers, J. McKinna \&\ F. Wiedijk}

\author{%%%
  Herman Geuvers
  \institute{\ourinstitute} 
  \institute{\tueinstitute} \and 
  Robbert Krebbers\qquad\qquad 
  James McKinna\qquad\qquad 
  Freek Wiedijk\institute{\ourinstitute\\\ouraffiliation} 
} 

%%%
%%% 
%%% 

   \usepackage{amsthm}
   \newtheorem{definition}{Definition} 
   \newtheorem{proposition}[definition]{Proposition} 
   \newtheorem{lemma}[definition]{Lemma} 
%%%   \newtheorem*{proof}{Proof} 
   \newtheorem{theorem}[definition]{Theorem} 
   \newtheorem{corollary}[definition]{Corollary} 

%%%
%%%
%%%

\usepackage{amssymb,url,alltt,graphicx}
\raggedbottom
\def\bar{\mathrel{|}}

\input{prooftree}

\newcommand{\gammainf}{\ensuremath{\Gamma_\infty}}

\def\SS{{\cal S}}
\newcommand\conv{{\rm conv}}
\newcommand\sort{{\rm sort}}
\newcommand\var{{\rm var}}
\newcommand\app{{\rm app}}
\newcommand\dom{{\rm dom}}
\newcommand{\type}{{\rm type}}
\newcommand\FV{{\rm FV}}
\newcommand\hfv{{\rm hfv}}
\newcommand\hfvt{{\rm hfvT}}
\newcommand\A{{\cal A}}
\newcommand\R{{\cal R}}
\newcommand\V{{\cal V}}
\newcommand\X{{\cal X}}
\newcommand{\oftype}{{:}}
\newcommand{\arr}{{\rightarrow}}
\newcommand{\redb}{\rightarrow_{\beta}}
\newcommand{\eqb}{=_{\beta}}
\newcommand{\Term}{{\rm Term}}
\newcommand{\Type}{{\rm Type}}
\newcommand{\Terminf}{{\rm Term}_{\infty}}
\newcommand\T{{\cal T}}
\newcommand\Tinf{{\T_\infty}}
\newcommand{\merge}{\ltimes}
\newcommand{\comp}{\mathrel{{|}{|}{|}}}
\newcommand\emb[1]{\overline{#1}}

%%% ocamlism

\newcommand{\ocamlcode}[1]{\texttt{#1}}

% defined terms need a typographic marker for declaration/first use! 
\newcommand{\demph}[1]{{\textbf{#1}}}%%%\emph
\newcommand{\realquote}[1]{{``{#1}''}}%%%\emph
\newcommand{\scarequote}[1]{{`{#1}'}}%%%\emph

\usepackage{color}
\definecolor{red}{rgb}{1.0,0.0,0.0}
\newcommand{\TODO}[1]{\NotForPublication{\textcolor{red}{TODO: {#1}}}}
\newcommand{\NotForPublication}[1]{}%%%change to {} for publication!!!

%%%
%%%
%%%

\begin{document}

\maketitle

%%%
%%%
%%%

\begin{abstract}
  We present an approach to type theory in which the typing judgments
  do not have explicit contexts.  Instead of judgments of shape
  $\Gamma \vdash A : B$, our systems just have judgments of shape 
  $A : B$.  A key feature is that we distinguish free and bound variables
  even in pseudo-terms.

  Specifically we give the rules of the \scarequote{Pure Type System}
  class of type theories in this style.  We prove that the typing
  judgments of these systems correspond in a natural way with those of
  Pure Type Systems as traditionally formulated.  I.e., our systems
  have exactly the same well-typed terms as traditional presentations
  of type theory.

  Our system can be seen as a type theory in which all type judgments
  share an identical, infinite, typing context that has infinitely
  many variables for each possible type.  For this reason we call our
  system \gammainf.  This name means to suggest that our type judgment
  $A : B$ should be read as $\gammainf \vdash A : B$, with a fixed
  infinite type context called \gammainf.
\end{abstract}


\section{Introduction}

\def\der#1#2#3{\setbox0=\hbox{$\strut #2$}%
\hbox to\wd0{$\hss\displaystyle{\strut{#1}\over\strut\box0}\rlap{\raise1pt\hbox{$\,#3$}}\hss$}}
\def\leaf#1{\displaystyle{\strut\atop\strut #1}}

\subsection{Problem}

One of the important insights type theory 
   gives 
us is the need to be aware of the \emph{context}
in which one 
   works. 
This was already stressed by de Bruijn in his 1979 
paper \emph{Wees contextbewust in WOT} \cite{bru:79}, 
Dutch for \realquote{Be context aware in the mathematical vernacular}.
In type theory a term always is considered with respect to a context $\Gamma$, 
   which gives 
the types of the variables occurring free in the term.
This is also apparent in 
   the shape $\Gamma \vdash M : A$ of 
the 
   judgments 
of type theory, 
where the context $\Gamma$ is made explicit.
   Thus 
a \scarequote{bound} variable is bound \emph{locally} in a term, 
while a \scarequote{free} variable actually is \emph{globally} bound, 
namely by the context. %%% of the term.

In 
   customary presentations 
of first order predicate logic 
\cite[for example]{mendelson:intro,vanDalen:LandS}, 
and in fact
in the presentation of most other logics as well, free variables are not
treated in such a way.
In these logics free variables are really \emph{free}.
They are taken from an infinite supply of variables that are just
available to be used in formulas and terms,
without them having to be declared first.

This difference between type theory and predicate logic means that when
we model predicate logic in type theory, actually we do not get
the customary version of predicate logic, but instead get a version
called \emph{free} logic~\cite{lambert:free-logic1963}.
In traditional treatments  
the formula 
\((\forall x.\, P(x)) \to (\exists x.\, P(x))\)
is usually provable.
For instance a natural deduction proof of this formula would look like:
\vspace{-\bigskipamount}
\[
\der{
\der{
\der{
\leaf{[\forall x.\, P(x)]}
}
{P(y)}{\forall E}
}
{\exists x.\, P(x)}{\exists I}
}
{(\forall x.\, P(x)) \to (\exists x.\, P(x))}{{\to}I}
\]
   This proof uses 
the free variable $y$.
If one cannot use any other variables than 
   those 
introduced
by earlier rules, then this proof 
   fails. 
   Indeed, 
the type corresponding to the formula 
   is not 
inhabited: there is no term \(M\) such that 
   the following judgment is derivable: 
\[D : {*},\, P : D \to {*} \vdash M : (\Pi x : D.\, P(x)) \to (\Sigma x : D.\, P(x))\]
because we cannot 
   avoid the case in which the domain \(D\) is empty, 
   where 
the formula is false.

Now there are two things one can do to 
%%%bridge this difference 
   bridge this gap 
between type theory and traditional logic:
\begin{itemize}
\item
Make predicate logic more like type theory, by explicitly keeping
track in the judgments of the set of variables that can be used in
the proof.

\item
Make type theory more like predicate logic, by having a version
of type theory that does not need contexts in the judgments,
i.e., in which free variables are just taken from 
%%%an infinite supply of variables. 
   some infinite supply. 

\end{itemize}

\noindent
Although the first option is interesting too, especially in categorical treatments of logic \cite[for example]{lambek-scott:hocl1988}, in this paper we
focus on the second.
We originally thought that the dependent types in type theory would
prevent a version of type theory without contexts
from being a viable option, but to our surprise it turns out that
one \emph{can} present type
theory in a style where there are no contexts and in which therefore
free variables are really free, provided we are prepared to pay the small price
of labelling variables in a rather involved manner. 

%%%In type theories that are actually implemented in interactive theorem provers, 
   In those type theories actually implemented in interactive theorem provers,
the context always consists of a part holding global \emph{definitions} and parameters and
a part holding the \emph{free variables} in the term 
(as in \cite[for example]{CSC:MKM2004,severi-poll:DPTS}).
For simplicity of exposition, 
and for the sake of proving an exact correspondence between 
a standard presentation of type theory and the variant 
%%%proposed in this paper, we consider here 
   we propose, in this paper we consider 
only the second part of such contexts.
We believe, however, 
that the other part can be treated in exactly the same way.

There is another reason why it is interesting to look at
a version of type theory where there are no explicit contexts.
One of the most popular architectures for proof assistants is the
\emph{LCF architecture}, named after the LCF system from the seventies \cite{LCF-book:1979}.
In the original form of such a system there is an abstract data type called \ocamlcode{term},
whose elements can only be created by a small number of functions exported
from the type-checking kernel.
Elements of this datatype always correspond to type-correct terms,
and those terms can contain free variables.

A system using this approach has 
   a kernel interface containing 
a function:
\begin{quote}
\begin{alltt}
app : term * term -> term
\end{alltt}
\end{quote}
\noindent
When this function is called, the kernel of the system makes sure that
the types of the arguments are compatible, i.e., that the result is 
again a type-correct term.

This is how the HOL family of theorem provers
is implemented.
These systems have a logical foundation that is based on a typed
lambda calculus.
However, in these systems the free variables in the terms are not recorded in
a context of variables.
The only context in these systems is the context of {definitions},
which is kept track of in a stateful variable.
Definitions are never allowed to be removed from this context,
as that would compromise the safety of the kernel.
Hence, these systems are stateful, although they can be made functional using a variant
of the approach presented here \cite{stateless}.

\newpage 
\noindent 
There are two classes of systems that can be said to implement a \emph{type theory},
%%%a typed lambda calculus. These two classes are: 
   a typed lambda calculus: 
\begin{itemize}
\item
The simpler type theories, in which no dependent types are allowed.
They often are a form of simple type theory with some enhancements,
   such as some 
form of polymorphism or type classes.
These include the systems from the HOL family: HOL4, HOL Light, ProofPower and
Isabelle.
These systems can be, and are, implemented following the LCF architecture 
just outlined.
In these systems variables come from an infinite \scarequote{sea} of free variables,
and in the logical theory 
   there is \emph{no} context keeping track of the variables. 

\item
   More  
advanced type theories, often called type theory with \emph{dependent types}.
These 
come from the Dutch \textsc{Automath} systems, the Swedish tradition
of Martin-L\"of type theory, the French tradition of the Calculus of
Constructions and variations on the Edinburgh Logical Framework. 
   Their implementations 
include Coq, NuPRL, Twelf, Agda, Lego, Plastic and Epigram.
In the logical theory of these systems 
   there \emph{is} a context keeping track of the variables. 
\end{itemize}
For this second style of type theory the pure LCF approach is not attractive.
The \ocamlcode{app} function will need to check whether the contexts in which
the terms live are compatible, which will be very expensive, if it needs
to be done for the type-checking of each function application.

For this reason actual type-theoretical proof assistants have a kernel
with a different kind of interface.
In such a kernel there is no abstract datatype of \emph{terms} (there
just is a---non-abstract---type of \emph{pseudo-terms}).
Instead there is an abstract type of well-typed \emph{contexts}, which we call
\ocamlcode{context} here.
(There is also a type \ocamlcode{pseudocontext}, but that is irrelevant here.)
The interface then looks like:
\begin{quote}
\begin{alltt}
mkApp : pseudoterm * pseudoterm -> pseudoterm
add_constant : string * pseudoterm -> context -> context
\end{alltt}
\end{quote}
where \ocamlcode{mkApp} is just the constructor of the data type of
pseudoterms, whereas \ocamlcode{add\_constant} is a function that does
the type-checking: a pseudoterm will only be added to the context
after it has been type-checked.  
%%%(The names of these functions are the actual names they have in the Coq system's kernel.  
   (These are the actual names of the functions in the kernel of the Coq system. 
The types of those functions in 
%%%the Coq system 
   Coq 
are essentially what is presented here.
The type \ocamlcode{pseudoterm} is called \ocamlcode{constr} %%%, 
    in Coq, 
while the type \ocamlcode{context} is called
\ocamlcode{safe\char`\_environment}.)  The system also has a global
variable
\begin{quote}
\begin{alltt}
global_env : context ref
\end{alltt}
\end{quote}
corresponding to the \emph{state} of the system in which the user 
   works. 
%%%This variable 
   It 
is not part of the kernel (and in fact is changed back
   by an undo operation), 
but as there are no
interesting operations combining two different \ocamlcode{context}s,
only one global \ocamlcode{context} is 
%%%relevant at any time, 
   ever relevant, 
%%%which is 
the one given by 
   the contents of 
this variable.

Although the architecture with contexts that we described
is purely functional (as is the Coq kernel), the fact that the actual
implementation has this global variable means that it is used in
a rather \scarequote{stateful} way.
The desire to investigate 
   a possible 
LCF-style kernel for
type theory that is \scarequote{less stateful} motivated this research.
In the conclusions we will address the question whether the style
of type theory we present here will lead to such a type-checking 
architecture.

\subsection{Approach}

The approach 
we will follow here is to imagine there to
be an \scarequote{infinite context} called \gammainf.
For each type-correct type $A$ this context will have infinitely
many variables $x_i^A$.
It should be stressed that this $A$ should be considered to just
be a label, a \emph{string}.
   Reduction will never happen  
inside these $A$s.
Also, $x_i^A$ and $x_i^B$ will be \emph{different} variables, even
when $A$ and $B$ are convertible, or even if they are $\alpha$-equivalent.
Note that the (free) variables in $A$ themselves will also be of shape
$y_j^B$: this means that 
   the variables themselves, as well as the  terms, 
have a recursive
tree-like structure. 

\noindent
For example, 
a variable corresponding to the successor function on natural numbers 
%%%will be something like: 
   looks like: 
$$s^{N^* \to N^*}$$
If we use numbered names for the variables, this might become:
$$x_0^{x_0^* \to x_0^*}$$
So the \realquote{small price} alluded to above is that a free variable $x_i^A$ in a well-typed term 
   carries 
with it the (well-founded) history of how it comes to be well-typed; 
   that is, the 
label $A$ 
   witnesses 
the validity of the context extension $\Gamma, x_i : A$.
 
Now our systems will have judgments $A : B$, which 
should be interpreted as $\gammainf \vdash A : B$.
For this reason we call the general approach to type theory 
   introduced here 
\scarequote{\gammainf} (reusing the name of the context
as the name of the system).
Note that \gammainf\ is not a single system: each type theory
will have a \scarequote{\gammainf-variant}.

The \gammainf\ approach has the essential feature that there
are two different classes of variables.
There are the variables that come from the \gammainf\ context
(the \scarequote{free} variables),
and then there is another kind of \scarequote{bound} variables.
When thinking about our systems one might imagine de Bruijn indices for
the bound variables, although the presentation 
   we give here uses 
named variables for them as well.

Although we expect 
%%%that many type theories will 
   many type theories to  
have a \gammainf-variant, 
   here we only consider  
the class
of type theories called Pure Type Systems \cite{bar-lics-hbk} (PTSs). 
That way 
   we keep everything 
concrete, and 
   it allows 
us to prove a precise correspondence between 
%%%Pure Type Systems 
   PTSs 
in the traditional style and our version 
   in \gammainf\ style. 

One should note that in 
   \gammainf\ 
any type will be inhabited, simply
because there are free variables of every type: in particular, just as in traditional treatments of logic, all domains are assumed to be inhabited. This is in essence the
same as in the version with contexts, except that 
   such variables are there explicitly recorded in the context. 

\subsection{Related Work}

To our surprise, we 
    found little 
published work investigating 
   such an approach to \emph{dependent} type theory.  
   In Church's original formulation of \emph{simple} type theory
   \cite{church:stt1940}, variables, both free \emph{and} bound, are
   annotated with their types, writing for example $\lambda
   x^{\alpha}. f^{\alpha\arr\alpha}\, x^{\alpha}$. (whereas in our formulation
   we would write $\lambda x \oftype {\alpha^*}. f^{\alpha^* \arr\alpha^*}\,
   x$.) Girard adopted \scarequote{Church-style} in the account of System F in his
   thesis \cite{girard:thesis}.
   %%%
   In neither system do \emph{term} variables occur in types, while
   \emph{type} variables are not regulated by an explicit context. In
   these non-dependent type theories, contexts are not strictly
   needed, because one can define the different 
   syntactic classes --- types, terms --- in stages.
   %%% 
   One can regard our approach as extending that of Church to
   dependent types, but optimised to avoid the need to consider
   substitution in labels on \emph{bound} variables which otherwise
   might arise in the application rule.

Conor McBride (private communication) observed that Pollack's \textsc{LEGO} 
implementation already supported the \gammainf\ idea, and this idea was then used 
in his \textsc{OLEG} extensions, and subsequently 
in the architecture of \textsc{Epigram 1}. 
However, this approach has not been treated theoretically as we do here. 

The explicit distinction between free and bound variables on a syntactic level
already can be found in \cite{mckinna-pollack:jar1999}. 
The motivation there was to avoid capture during substitution while keeping a close correspondence with the informal presentation of PTSs with named variables, rather than how to give a \scarequote{\gammainf} presentation, as here. 
Various approaches to representing 
   binding 
are discussed in \cite{Vaughan06areview}, 
   which considers 
named free variables and de Bruijn index bound variables 
one of the best options for mechanisation. 
Indeed, in ongoing work \cite{krebbers:gammainf} the second author has formalised 
one half of the correspondence proved in Section~\ref{sec:thms} in such a style. 
%%%For the sake of presentation, we leave the niceties of 
%%%such a formalisation to the enthusiastic reader. 
   We expand on the niceties of this formalisation 
   in Section \ref{sec:conclusion}.
   %%%below. 


Elsewhere, Pollack considered presentations of type theory separating
the typing judgment from that for context
well-formedness~\cite{randy:closure-under1993}, although judgments are
still \scarequote{in context}. This allows a subtle range of issues to be
explored, especially
   regarding 
closure under \(\alpha\)-conversion, 
%%%which we treat only informally here. 
   here treated only informally. 

Most significantly, but starting from a rather different point,
Sacerdoti Coen considered the problem of proof-checking in the setting
of a distributed library, and hence the problem of how to
\emph{reconstruct} a context in which a given term may be successfully
type-checked~\cite{CSC:MKM2004}. This work (elaborated in
\cite{CSC:PhD}, and forming the basis of the Matita system) goes
beyond the standard PTS setting considered in this paper. 
It identifies a subtle problem which arises when attempting to merge
contexts (including definitions) in the presence of global constraints
(such as universe levels). 

\textit{Added in proof.} Between acceptance of the final version of this paper and this final version, our attention was drawn to the recent work of Matthias Boespflug~\cite{boespflug}, which itself references an earlier (2009) account of our ideas. By contrast with our presentation, which is purely first-order, Boespflug uses higher-order abstract syntax (HOAS), with a view to implementation. 

\subsection{Contribution}

We present a different approach to type theory, 
much closer to the way logical systems
usually are presented than the standard presentation, 
in which free variables are
not bound in a finite context but are taken to be really free.

We 
   validate our approach 
by proving two theorems, 
\ref{thm:PTStoGinf} and \ref{thm:GinftoPTS} below, 
   establishing 
a straightforward correspondence between 
   the standard presentation 
and the variant 
   presented here.

\subsection{Outline}

The structure of the paper is as follows.
In Section~\ref{sec:pts} we recall the
PTS rules and some of its theory.
In Section~\ref{sec:Gi} we present the \gammainf-variant of the
PTS rules, in which the judgments do not have contexts.
In Section~\ref{sec:thms} we show that both systems
correspond to each other in a natural way.
In Section~\ref{sec:conclusion} we conclude with a prospectus for
an implementation based on our variant of the PTS rules.


\section{Pure Type Systems in the traditional style}\label{sec:pts}

Pure Type Systems (PTSs) 
%%%are a generalisation of 
   generalize 
many existing type
systems and thus the class of PTSs contains various well-known
systems, like 
%%%system F and system F$\omega$, 
   systems F and F$\omega$, 
dependent type theory $\lambda$P 
and the Calculus of Constructions.

\begin{definition}\label{def.pts} For $\SS$ a set (the set of \emph{sorts}), 
$\A \subseteq \SS\times\SS$ (the set of \emph{axioms}) and 
$\R \subseteq \SS\times \SS \times \SS$ (the set of \emph{rules}), 
the \emph{Pure Type System} $\lambda(\SS ,\A
,\R)$ is the typed
$\lambda$-calculus with inference rules as in 
Figure~\ref{fig:pts}. 
\begin{figure}[t]
{\normalsize
$$\begin{array}{|llr|}
\hline
%\hoog{1.5em}
(\mbox{sort})
&
\prooftree
\justifies
\vdash s_1 : s_2
\endprooftree &\mbox{if }(s_1 ,s_2)\in \A\\
&&\\
(\mbox{var})
&
\prooftree
\Gamma \vdash A : s
\justifies
\Gamma ,x\oftype A\vdash x : A
\endprooftree &\mbox{if }x\notin\Gamma \\
&&\\
(\mbox{weak})
&
\prooftree
\Gamma \vdash A : s\;\;\;\;
\Gamma \vdash M : C
\justifies
\Gamma ,x\oftype A \vdash M : C
\endprooftree &\mbox{if }x\notin\Gamma \\
&&\\
(\Pi)
&
\prooftree
\Gamma \vdash A : s_1\;\;\;\;
\Gamma ,x\oftype A \vdash B : s_2
\justifies
\Gamma \vdash \Pi x\oftype A .B : s_3
\endprooftree & \mbox{if }(s_1 ,s_2 ,s_3) \in \R \\
&&\\
(\lambda)
&
\prooftree
\Gamma ,x\oftype A \vdash M : B\;\;\;\;
\Gamma \vdash \Pi x\oftype A .B : s
\justifies
\Gamma  \vdash \lambda x\oftype A .M : \Pi x\oftype A.B
\endprooftree &\\
&&\\
(\mbox{app})
&
\prooftree
\Gamma \vdash M : \Pi x\oftype A.B\;\;\;\;
\Gamma \vdash N : A
\justifies
\Gamma  \vdash MN : B[x := N]
\endprooftree &\\
&&\\
(\mbox{conv})
&
\prooftree
\Gamma \vdash M : A\;\;\;\;
\Gamma \vdash B : s
\justifies
\Gamma  \vdash M : B
\endprooftree & A =_{\beta} B\\[1em]
\hline
\end{array}$$
}
\caption{Typing rules for PTSs\label{fig:pts}}
\end{figure}
In the 
rules, the expressions \(M,N,A,B,C\) are taken from the set of \emph{pseudo-terms} 
$\T$ defined by\label{pts-pseudo-terms}
$$ \T ::=
s \bar \V \bar \Pi \V \oftype \T .\T \bar \lambda \V \oftype \T .\T \bar \T \T .$$
with $\V$ 
   a set of variables, 
and the $\Gamma$ taken from the set of \emph{pseudo-contexts}
   \[x_1 : A_1, \ldots , x_n :A_n \quad (x_i \in \V, A_i\in\T, 1\le i\le n)\]
   with the $x_i$ all distinct. 
(We leave the choice of variable \emph{names} 
unspecified at this point, 
as this does not matter as long as 
   \(\V\) is countably infinite, but  
below we will take a specific choice 
   of names.) 
\end{definition}

There is a lot of theory about PTSs and various systems have been
studied in the context of PTSs. We do not give a complete overview but
refer to \cite{bar-lics-hbk,bargeu-ar-hbk,geuv93} for details and
explanation. Here we just give the results that we 
use in the rest of the paper to prove the equivalence between 
a PTS and its
   \gammainf-variant. 

\begin{definition}
The pseudo-term $A$ is called \emph{well-typed} if a pseudo-context $\Gamma$ 
and pseudo-term $B$ exist such that $\Gamma\vdash A:B$ or
$\Gamma\vdash B:A$ is derivable. A pseudo-context $\Gamma$ is 
\emph{well-formed} if pseudo-terms $A$ and $B$ exist such that
$\Gamma\vdash A:B$ is derivable; a \emph{context}  is 
   a well-formed pseudo-context. 
The set of variables declared in 
pseudo-context $\Gamma$ is called the \emph{domain} of $\Gamma$,
$\dom(\Gamma)$. For $x\in\dom(\Gamma)$, let $\type_{\Gamma}(x)$
denote the \scarequote{type} assigned to $x$ in $\Gamma$: if $x:A
\in\Gamma$, then $\type_{\Gamma}(x) = A$. The expression $\type(\Gamma)$ denotes the
set of such \scarequote{types} occurring in $\Gamma$. The set of well-typed terms of
$\lambda (\SS,\A,\R)$ is denoted by $\Term(\lambda (\SS,\A,\R))$.
\end{definition}

We adopt the usual notions of bound and free variable, 
$\alpha$-conversion ($\equiv$), 
   substitution (\(B[x := N]\), used in the rule (\mbox{app})), 
$\beta$-reduction ($\redb$) and
$\beta$-equality ($\eqb$, used in the rule (\mbox{conv})) on pseudo-terms. 

The following are well-known properties of PTSs. 
The relation $\Gamma\subseteq\Delta$ 
%%%just denotes set containment 
   denotes inclusion  
between $\Gamma$ and $\Delta$ 
regarded as sets of variable assignments. 
%%%The third property, 
   The third, 
Permutation, is a corollary of Strengthening.

\begin{proposition}\label{prop.metatheoryPTS}
\ 
\begin{description}
\item[Thinning] If $\Gamma \vdash M:A$ and $\Delta \supseteq \Gamma$ is
   well-formed, 
then $\Delta \vdash M:A$.
\item[Strengthening] If $\Gamma, x:B,\Delta \vdash M:A$ and
$x\notin\FV(\type(\Delta),M,A)$, 
then $\Gamma, \Delta \vdash M:A$.
\item[Permutation] If $\Gamma, x:B,y:C,\Delta \vdash M:A$ and
$x\notin\FV(C)$,  
then $\Gamma, y:C, x:B,\Delta \vdash M:A$.
\end{description}
\end{proposition}

In proving the equivalence between a PTS and its 
   \gammainf-variant, 
we need to merge two 
contexts to create a new one. Therefore
we introduce 
   the following:  

\begin{definition}\label{def.comp}
Let $\Gamma$ and $\Delta$ be two pseudo-contexts. 
%%%We say that 
   We say 
$\Gamma$ and $\Delta$ are \emph{compatible}, notation $\Gamma\comp\Delta$, if
$$\forall x\in \dom(\Gamma)\cap\dom(\Delta)( \type_{\Gamma}(x) \equiv \type_{\Delta}(x)).$$
The \emph{merge} of $\Gamma$ and $\Delta$, notation
$\Gamma\merge\Delta$, is the pseudo-context $\Gamma ,
(\Delta\setminus\Gamma)$. This is $\Gamma$ followed by the
declarations $x:B\in\Delta$ for which $x\notin\dom(\Gamma)$.
\end{definition}

Note the strong requirement in $\Gamma\comp\Delta$ that the types of
$x$ in $\Gamma$ and $\Delta$ should be $\alpha$-equal, and not just
$\beta$-convertible.

\begin{lemma}
If $\Gamma$ and $\Delta$ are 
contexts and $\Gamma \comp \Delta$, then $\Gamma \merge\Delta$ is well-formed.
\end{lemma}

\begin{proof}
We write $x_1:B_1, \ldots, x_n:B_n$ for $\Delta$.  $\Gamma \merge\Delta$
is the pseudo-context $\Gamma, (\Delta\setminus\Gamma)$.  As $\Gamma$
is well-formed, we only have to consider the part  
$\Delta\setminus\Gamma = x_{i_1} : B_{i_1}, \ldots, x_{i_n} : B_{i_n}$. 
%%%\\
   But 
$x_1:B_1, \ldots, x_{i_1 -1}: B_{i_1 -1} \subseteq \Gamma$, so by Thinning $\Gamma \vdash B_{i_1} :s$ for some sort $s$, so $\Gamma, x_{i_1} :B_{i_1}$ is well-formed.\\
The same reasoning applies to $x_{i_2}:B_{i_2}, \ldots, x_{i_n}:B_{i_n}$, 
so we conclude that $\Gamma, (\Delta\setminus\Gamma)$ is well-formed. 
\end{proof}

%%%%%%%%%%%%%%%%
In our system \gammainf, the free variables will have special names,
as they are labelled by their types. Of course, consistently renaming
the free variables in a judgment $\Gamma \vdash M:A$ does not change
its meaning, as the free variables in $M$ and $A$ are actually bound
in $\Gamma$. For clarity, we introduce this notion explicitly.

\begin{definition}\label{def:alpha-judg}
The judgment $\Gamma \vdash M:A$ is $\alpha$-equivalent to 
%%%the judgment 
$\Gamma ' \vdash M':A'$ in case one can be obtained from the
other by renaming bound variables, where we consider the free
variables in $M$ and $A$ to be bound by their declaration in $\Gamma$.
\end{definition}
%%%%%%%%%%%%%%%%

\section{Pure Type Systems in the \gammainf\ style}\label{sec:Gi}

We now make the set of 
   variables 
$\V$ explicit.
We have two kinds:  
variables $\dot x$ with a dot on top,  
   intended
to be bound by $\lambda$ and $\Pi$ binders; and variables $x^A$ 
   tagged with a pseudo-term $A$, 
   intended 
to be bound in the context.
This means we take $\V$ in Definition~\ref{def.pts} 
   as follows, where $\X$ supplies the \emph{names} 
   of 
variables: 
$$\begin{array}{rcl}
\V &::=& \dot\X \bar \X^\T \\
\X &::=& x \bar y \bar z \bar \dots \bar x_0 \bar x_1 \bar x_2 \bar \dots
\end{array}$$
Clearly the rules for $\T$ and $\V$ are mutually recursive.

Note that although the variables are \emph{intended} to be used in a certain
way (made precise in Definition~\ref{def.typeannotated} below), 
in the PTSs as defined
   above 
both kinds of $\V$ can be used for all purposes.
In particular $\dot x$ can be put in a context, $x^A$ can be bound, 
and the 
   label 
$A$ of $x^A$ need not correspond to the type of $x^A$.

Note also that the 
   definition of substitution, and hence the 
relation of $\beta$-equality, 
   is agnostic 
about the structure of the annotations of the variables.
(The definition
of $=_\beta$ in Section \ref{sec:pts} takes $\V$ just as a set).
This means that although
$$(\lambda \dot A:{*}. \dot A)\,B^{*} =_\beta B^{*}$$
we have that
$$x^{(\lambda \dot A:{*}. \dot A) B^{*}} \ne_\beta x^{B^{*}}$$

We will now define the rules of \gammainf.
To do this we first have to introduce the notion of \emph{hereditarily free variables of
the types of the free variables} in a term.
We first motivate the need for this notion.

In a PTS, the context takes care that one can only abstract over a
variable if nothing else depends on that variable. In the rules, this
is formalised by requiring that the $x:A$ 
   abstracted 
over in
the $\Pi$ or $\lambda$ rule must be the last declaration in the
context. This ensures that $x$ does not occur free in any of the other
types in the context. In \gammainf\ we do not have contexts, so we have to replace this by another side condition on the rules. We would like to have a $\Pi$ rule as follows:
$$
{
A : s_1
\quad\enskip
B : s_2
\over
\Pi \dot y {:} A.\, B[x^A := \dot y] : s_3
}
\rlap{ \small $(s_1,s_2,s_3)\in{\cal R}$}
$$
but that is wrong, because then we would be able to form (in PTS terminology)
the $\Pi$-type 
$$
{
\ldots \vdash A:* \quad \enskip A:*, P:A\arr *, Q:\Pi x\oftype A. P\, x \arr *,  a:A, h:P\, a \vdash  Q \, a\, h :*
\over
A:*, P:A\arr *, Q:\Pi x\oftype A. P\, x \arr *, h:P\, a \vdash  \Pi y :A.Q\,y\, h : *
}
$$
%%%This is not correct, 
   But this cannot be correct, 
because $h$ is not of type $P\, y$ in the conclusion. 
In \gammainf, this derivation would read (adding some brackets for readability):
$$
{
A^*:* \quad \enskip 
Q^{\Pi \dot x\oftype A^*. (P^{A^*\arr *}\, \dot x) \arr *} \, a^{A^*}\, h^{P^{A^*\arr *}\, a^{A^*}} :*
\over
\Pi \dot y :A^*. Q^{\Pi \dot x\oftype A^*. (P^{A^*\arr *}\, \dot x) \arr *} \, \dot y\, h^{P^{A^*\arr *}\, a^{A^*}} :*
}
$$
which would be 
   derivable 
according to the $\Pi$-rule above, but
clearly 
   undesirable. 


\begin{definition}\label{def:HFV}
Given $M\in \T$, we define the \emph{hereditarily free variables in $M$}, denoted $\hfv(M)$, as follows:
\begin{eqnarray*}
\hfv(s) =\hfv(\dot x) &=& \emptyset\\
\hfv(x^{A})&=& \{x^{A}\} \cup\hfv(A)\\
\hfv(F\,N) &=& \hfv(F)\cup\hfv(N)\\
\hfv(\lambda \dot x \oftype A.N) = \hfv(\Pi \dot x\oftype A.N) &=& \hfv(A)\cup\hfv(N)
\end{eqnarray*}
\end{definition}

So, where $=_\beta$ basically ignores the structure of
the type labels of 
free variables, we now take them seriously, 
collecting the variables (hereditarily) free in the type labels as well.

We put as a side condition in the $\Pi$-rule that $x^A$ should
not occur free in any of the \emph{types of the free variables in $B$}, and
similarly for the $\lambda$ rule. We give an explicit %%%direct 
definition of this notion.

\begin{definition}\label{def:HFVT}
Given $M\in \T$, we define the \emph{hereditarily free variables of the types of the free variables in $M$}, denoted $\hfvt(M)$, as follows:
\begin{eqnarray*}
\hfvt(s) =\hfvt(\dot x) &=& \emptyset\\
\hfvt(x^{A})&=& \hfv(A)\\
\hfvt(F\,N) &=& \hfvt(F)\cup\hfvt(N)\\
\hfvt(\lambda \dot x \oftype A.N) = \hfvt(\Pi \dot x\oftype A.N) &=& \hfvt(A)\cup\hfvt(N)
\end{eqnarray*}
\end{definition}

So, for example $\hfvt(h^{P^{A^*\arr *}\, a^{A^*}}) = \{ P^{A^*\arr *} , a^{A^*}, A^*\}$. An easy corollary of the definition is that
$$\hfvt (M) \subseteq \hfv(M)$$


We now give the derivation rules of the system.

\begin{definition}
The derivation rules of \gammainf\ are 
given by the inference rules in Figure~\ref{fig:gammainf}. 
\begin{figure}[t]
{\normalsize
$$
\begin{array}{|llr|}
\hline
(\mbox{\rm sort})
&
\prooftree
\justifies
s_1 : s_2
\endprooftree &\mbox{if }(s_1 ,s_2)\in \A\\
&&\\
(\mbox{\rm var})
&
\prooftree
A : s
\justifies
x^A : A
\endprooftree & \\
&&\\
(\Pi)
&
\prooftree
A : s_1\;\;\;\;
B : s_2
\justifies
\Pi \dot x\oftype A .B[y^A := \dot x] : s_3
\endprooftree & \hspace{-2em}\mbox{if }(s_1 ,s_2 ,s_3) \in \R\mbox{ and }y^A \notin\hfvt(B)\\
&&\\
(\lambda)
&
\prooftree
M : B\;\;\;\;
\Pi \dot x\oftype A .B[y^A := \dot x] : s
\justifies
\lambda \dot x\oftype A .M[y^A := \dot x] : \Pi \dot x\oftype A.B[y^A := \dot x]
\endprooftree & \mbox{if }y^A \notin\hfvt(M)\cup\hfvt(B)\\
&&\\
(\mbox{\rm app})
&
\prooftree
M : \Pi \dot x\oftype A.B\;\;\;\;
N : A
\justifies
MN : B[\dot x := N]
\endprooftree &\\
&&\\
(\mbox{\rm conv})
&
\prooftree
M : A\;\;\;\;
B : s
\justifies
M : B
\endprooftree & A =_\beta B\\[1em]
\hline
\end{array}
$$
}
\caption{Typing rules for \gammainf\label{fig:gammainf}}
\end{figure}
The $\Pi$ and $\lambda$ rules have the side condition that $\dot x$ 
should not be \emph{captured} in $B$ or $M$ when doing the substitution.
That is, $\dot x$ should not be bound by a binder under which $y^A$ occurs.
\end{definition}

The side condition on the $\Pi$ and $\lambda$ rules is no restriction as you can
go to an $\alpha$-equivalent version of the term afterwards.

\section{The correspondence theorems}\label{sec:thms}
We now prove that a PTS and its \gammainf-variant correspond to each
other. For a \gammainf\ judgment $M:A$ we generate a context $\Gamma$
such that $\Gamma\vdash M:A$ is 
   PTS-derivable.  
Conversely, if
$\Gamma \vdash M : A$ is 
   PTS-derivable,  
we always have an
$\alpha$-equivalent judgment (see Definition \ref{def:alpha-judg})
$\Gamma'\vdash M':A'$ such that $M' : A'$ is derivable in \gammainf.
This specific form $\Gamma' \vdash M' : A'$ we call a \emph{type
  annotated} judgment.

\begin{definition}\label{def.typeannotated}
A \emph{type annotated context} in a PTS is a context of the form
$$x^{B_1}_1 : B_1, \ldots, x^{B_n}_n:B_n$$
where we moreover assume that all bound variables in the $B_i$ are of the form $\dot x$.
\end{definition}

\begin{definition}\label{def.typeannotated1}
A \emph{type annotated judgment} in a PTS is 
   one 
of the form
$$x^{B_1}_1 : B_1, \ldots, x^{B_n}_n:B_n \vdash M:A$$
where: $x^{B_1}_1 : B_1, \ldots, x^{B_n}_n:B_n$ is a type annotated context; 
all free variables in
$M$ and $A$ are of the form \(x^{B_i}_i\); 
   and 
all bound variables are of the form $\dot x$.
\end{definition}

We now first show the easy direction of our correspondence result:

\begin{lemma}
Every judgment $\Gamma \vdash M:A$ in a PTS is $\alpha$-equivalent to a type annotated judgment $\Gamma' \vdash M':A'$.
\end{lemma}

\begin{proof}
From left to right we rename the variables in the context (and of course also in $M$ and $A$) to the \scarequote{standard} names
$$x_1^{B_1}:B_n,\dots,x_n^{B_n}:B_n$$
(Here $x_i$ is not a meta-variable for a variable name, but really
the \emph{explicit} variable name \realquote{$x_i$} in $\X$.)
We also $\alpha$-rename any bound variable of the form $x^A$ to a fresh
variable of the form $\dot x$. 
\end{proof}

As an example, consider the PTS judgment
$$A : {*},\, a : A \,\vdash (\lambda x\oftype A.\,x)\, a : A$$
This does not fit the variable names from our $\V$, so this does not
conform to the definitions in this paper.
Instead using our variables it should be something like:
$$\dot A : {*},\, a^{*} : \dot A \,\vdash (\lambda x^{\dot B}\oftype\dot A.\,x^{\dot B})\, a^{*} : \dot A$$
This of course is not a \emph{type annotated} judgment, the annotations 
   make no 
sense at all,
but still this is a perfectly
fine 
   PTS judgment 
as defined in Definition~\ref{def.pts}.

Now according to the theorem this is $\alpha$-equivalent to a judgment that \emph{is} type annotated.
And it is, for example it is $\alpha$-equivalent to
$$x_1^{*} : {*},\, x_2^{x_1^{*}} : x_1^{*} \,\vdash (\lambda \dot x\oftype x_1^{*}.\,\dot x)\, x_2^{x_1^{*}}$$
Or, if one uses more readable names, to
$$A^{*} : {*},\, a^{A^{*}} : A^{*} \,\vdash (\lambda \dot x\oftype A^{*}.\,\dot x)\, a^{A^{*}}$$

The other part of the easy direction of our correspondence is that
a type annotated PTS judgment essentially is the same as a \gammainf\ judgment:

\begin{theorem}\label{thm:PTStoGinf}
If 
   the type annotated PTS judgment $\Gamma \vdash M : A$ is derivable,  
then $M : A$ is a derivable judgment of the corresponding \gammainf\ type theory.
\end{theorem}

\begin{proof}
By induction on the size of the derivation of $\Gamma \vdash M : A$.
We do a case split on the last rule used in the derivation: %%%; we treat a few cases.
\begin{itemize}
\item[(sort)]
Immediate.

\item[(weak)]
Trivial, because if $\Gamma,x\oftype A$ is a type annotated context, then certainly
$\Gamma$ is a type annotated context.

\item[(\var)] 
By induction we have $A : s$ derivable in \gammainf, 
and because the context is type annotated
the variable name must be of the form $x^A$.
Hence $x^A : A$ in \gammainf.

\item[(\conv)] 
We know that $\Gamma \vdash M : A$ and $\Gamma \vdash B : s$.
Now $A$ need not have bound variables of the form $\dot x$, 
but 
one can rename them to obtain $A' \equiv A$ such that $\Gamma \vdash M : A'$ \emph{will} be
type annotated.
Then $M : A'$ and $B : s$ in \gammainf\ by induction and therefore also $M : B$ in \gammainf.

\item[(\app)] 
Again, we might need to change the bound variable in $\Gamma \vdash M : \Pi x\oftype A.B$ to the dotted kind, to get a type annotated judgment.
Apart from that this case is trivial, just like the previous one.

\item[($\Pi$)]
The conclusion will be of the form $\Gamma \vdash \Pi\dot x\oftype A.B : s_3$.
Now if we take $y^A$ a completely fresh variable, then $\Gamma,y^A:A \vdash B[\dot x := y^A] : s_2$ will be a type annotated judgment, as well as being $\alpha$-equivalent to 
$\Gamma,\dot x:A \vdash B : s_2$.
   Accordingly, let 
$B' := B[\dot x := y^A]$, so that $B \equiv B'[y^A := \dot x]$.

Clearly now $y^A \notin\hfvt(B')$ because $\Gamma,y^A:A \vdash B' : s_2$,
so all type annotations will be typable in $\Gamma$, which does not contain
$y^A$.

By induction $A : s_1$ and $B' : s_2$ in \gammainf\ and because
$y^A \notin\hfvt(B')$ we get that
$\Pi\dot x\oftype A.B'[y^A := \dot x] : s_3$ in \gammainf.
But this is precisely $\Pi\dot x\oftype A.B : s_3$.
\item[($\lambda$)]
This case essentially follows that of the previous one.

\end{itemize}
\end{proof}

The other direction of our correspondence---from \gammainf\ to
traditional PTS style---is a bit more involved.  We need to
\emph{synthesise} an appropriate context, and because we build this
context by recursion over the type derivation, we need to merge these
synthesised contexts using $\merge$.  For this we need a number of
lemmas involving type annotated contexts in PTSs.


\begin{lemma}\label{lem.annotctxt}
If $\Gamma$ and $\Delta$ are type annotated contexts, then $\Gamma\comp\Delta$.
\end{lemma}

\begin{proof}
If $x^A \in \dom(\Gamma)\cap\dom(\Delta)$, then $x^A : A\in\Gamma$ and
$x^A :A \in \Delta$, of course, $A \equiv A$ and this is what we need
to prove according to Definition \ref{def.comp}. 
\end{proof}

\begin{lemma}\label{lem.annothfvt}
If $\Gamma$ is a type annotated context with $x^A\in\dom(\Gamma)$, $\Gamma \vdash M:B$ and $x^A \notin\hfvt(M,B)$, then 
$$\exists \Delta \subset \Gamma (\Delta, x^A:A\vdash M:B)$$
\end{lemma}

\begin{proof}
Write $\Gamma =\Gamma_1, x^A :A, \Gamma_2$, and suppose $y^C \in
\dom(\Gamma_2)$ with $x^A\in\FV(C)$. If $y^C \in \FV(M,B)$, then $
x^A\in \hfvt(M,B)$, contradiction. So $y^C \notin\FV(M,B)$. This means
that all declarations $y^C:C$ in $\Gamma_2$ for which $x^A\in\FV(C)$
can be removed by Strengthening (Proposition \ref{prop.metatheoryPTS}),
starting from the rightmost declaration in $\Gamma_2$. We end up with a judgment
$$\Gamma_1, x^A :A, \Gamma'_2 \vdash M:B$$ with $\Gamma'_2 \subseteq
\Gamma_2$ and $x^A\notin\type(\Gamma'_2)$. Using Permutation
(Proposition \ref{prop.metatheoryPTS}), we conclude that $\Gamma_1,
\Gamma'_2, x^A :A \vdash M:B$ and we take $\Gamma_1, \Gamma'_2$ for $\Delta$. 
\end{proof}

\begin{corollary}\label{cor.annothfv}
If $\Gamma \vdash M:B$ is a type annotated judgment, there is a
$\Delta \subseteq \Gamma$ such that $\Delta \vdash M:A$ and
$\dom(\Delta) \subseteq \hfv(M,B)$.
\end{corollary}

\begin{proof}
Let $x^A\in \dom(\Gamma)$ and $x^A\notin \hfv(M,B)$. Then $x^A\notin
\hfvt(M,B)$, so (according to Lemma \ref{lem.annothfvt}), there is a $\Delta\subseteq
\Gamma$ such that $\Delta, x^A:A\vdash M:B$. But also $x^A\notin
\FV(M,B)$, so by Strengthening (Proposition \ref{prop.metatheoryPTS}),
$\Delta\vdash M:B$. 
\end{proof}

So, in $\Gamma \vdash M:B$, we can always make the context $\Gamma$ so
small that its domain is within the set of hereditarily free variables
of $M,B$. The other way around, the hereditarily free variables of
$M,B$ should be in $\dom(\Gamma)$:

\begin{lemma}\label{lem.hfvdom}
If $\Gamma \vdash M:B$ is type annotated, then $\hfv(M,B) \subseteq \dom(\Gamma)$.
\end{lemma}

\begin{proof}
We prove $\Gamma \vdash M:B \Rightarrow \hfv(M) \subseteq
\dom(\Gamma)$, by induction on the derivation and then we are done,
because if $\Gamma \vdash M:B$, then $\Gamma \vdash B:s$ for some sort
$s$, or $B$ is a sort. %%%We treat a few cases.
\begin{itemize}
\item[(\sort)] Immediate. 
\item[(\var)] By induction, $\hfv(A) \subseteq\dom(\Gamma)$, so
  $\hfv(x^A) \subseteq \dom(\Gamma, x^A : A)$.
\item[(\conv)] 
By induction, $\hfv(M)\subseteq\dom(\Gamma)$, so we are done.
\item[(\app)] 
By induction, $\hfv(F) \subseteq\dom(\Gamma)$ and $\hfv(M)\subseteq\dom(\Gamma)$, 
so $\hfv(F\,M) \subseteq\dom(\Gamma)$.  
\item[($\Pi$)]
By induction, $\hfv(A)\subseteq\dom(\Gamma)$ and $\hfv(B)\subseteq\dom(\Gamma, y^A:A)$, so 
$\hfv(\Pi \dot x\oftype A. B[y^A := \dot x]) \subseteq \dom(\Gamma)$. 
\item[($\lambda$)]
By induction, $\hfv(M)\subseteq\dom(\Gamma, y^A:A)$ and 
$\hfv(\Pi \dot x\oftype A. B[y^A := \dot x]) \subseteq \dom(\Gamma)$, so 
\(\hfv(A) \subset \dom(\Gamma)\), and hence 
$\hfv(\lambda \dot x\oftype A. M[y^A := \dot x]) \subseteq \dom(\Gamma)$.

\end{itemize}
\end{proof}

The more difficult direction of our correspondence now follows:

\begin{lemma}
Let $M : A$ be a derivable \gammainf\ judgment.
Then all free variables in $M$ and $A$ have the form $x^A$ and
all bound variables have the form $\dot x$.
\end{lemma}

\begin{proof}
By induction on the derivation of $M : A$. 
\end{proof}

\begin{theorem}\label{thm:GinftoPTS}
Let $M : A$ be a derivable \gammainf\ judgment. 
Then there is a type annotated judgment $\Gamma \vdash M:A$ 
derivable in the associated PTS, 
such that $\Gamma$ contains exactly the
variables in $\hfv(M) \cup \hfv(A)$.
\end{theorem}

\begin{proof}
By induction on the derivation of $M:A$ we show 
there exists
a type annotated context $\Gamma(M,A)$ 
   such that $\Gamma(M,A) \vdash M:A$. 
%%%We treat a few cases.
Note that 
$\Gamma(M,A)$ depends on the \emph{derivation} 
of the judgment $M:A$, not just on the terms 
$M$ and $A$.
\begin{itemize}
\item[(sort)]
Immediate.
\item[(\var)] 
By induction, $\Gamma(A,s) \vdash A:s$. So $\Gamma(A,s), x^A : A \vdash x^A : A$. 
\item[(\conv)] 
By induction, $\Gamma(M,A) \vdash M:A$ and $\Gamma(B,s) \vdash B:s$,
and we also know that $A\eqb B$. \\ So
$\Gamma(M,A)\merge\Gamma(B,s)\vdash M : B$ by Thinning and 
the (conv) rule. 
\item[(\app)] 
By induction, $\Gamma(F,\Pi \dot x\oftype A.B) \vdash F:\Pi \dot x \oftype A. B$ and $\Gamma(M,A) \vdash M:A$. \\ So
$\Gamma(F,\Pi \dot x\oftype A.B)\merge\Gamma(M,A)\vdash F\,M : B[\dot x := M]$ by Thinning and 
   the (app) rule. 
\item[($\Pi$)] By induction, $\Gamma(A,s_1) \vdash A:s_1$ and
  $\Gamma(B,s_2) \vdash B:s_2$.\\ 
If $y^A \notin\Gamma(B,s_2)$, then $\Gamma(A,s_1)\merge
\Gamma(B,s_2), y^A:A_i \vdash B:s_2$, so by
Thinning and the ($\Pi$) rule we have $\Gamma(A,s_1)\merge
\Gamma(B,s_2)\vdash \Pi \dot x\oftype A. B[y^A := \dot x] : s_3$.\\
If $y^A \in\dom(\Gamma(B,s_2))$, then $\Delta , y^A:A \vdash B:s_2$ for
some $\Delta \subset \Gamma(B,s_2)$. So  by
Thinning and the ($\Pi$) rule we have $\Gamma(A,s_1)\merge
\Delta\vdash \Pi \dot x\oftype A. B[y^A := \dot x] : s_3$.

\item[($\lambda$)]
By induction, we obtain 
$\Gamma(M,B) \vdash M:B$   
and $\Gamma(\Pi \dot x\oftype A. B[y^A := \dot x],s) \vdash \Pi \dot x\oftype A.\penalty100 B[y^A := \dot x]:s$.\\ 
If $y^A \notin\dom(\Gamma(M,B))$, then $\Gamma(A,s_1)\merge \Gamma(M,B),
y^A:A_i \vdash M:B$. So by Thinning and 
   the ($\lambda$) rule, we have 
 $\Gamma(\Pi \dot x\oftype A. B[y^A :=
  \dot x],s)\merge \Gamma(M,B)\vdash \lambda \dot x\oftype A. M[y^A :=
  \dot x]: \Pi \dot x\oftype A. B[y^A := \dot x]$. \\
If $y^A \in\dom(\Gamma(M,B))$, then $\Delta , y^A:A \vdash M:B$ for some
$\Delta \subset \Gamma(M,B)$, by Lemma \ref{lem.annothfvt}. So by Thinning and 
   the ($\lambda$) rule, we have 
$\Gamma(\Pi \dot x\oftype A. B[y^A :=
  \dot x],s)\merge \Delta\vdash \lambda \dot x\oftype A. M[y^A := \dot x]:
\Pi \dot x\oftype A. B[y^A \penalty 100 := \dot x]. $ 
\end{itemize}
By Lemma \ref{lem.hfvdom}, 
   $\dom(\Gamma(M,A)) \supseteq \hfv(M,A)$. 
Corollary \ref{cor.annothfv} lets us strengthen the
context to $\Delta \subseteq \Gamma(M,A)$ such that $\Delta \vdash
M:A$ and $\dom(\Delta) =\hfv(M,A)$.  
\end{proof}

\begin{corollary}
Let
$$M : A$$
be a derivable \gammainf\ judgment.
Take all variables of the form $x^A_i$ occurring
in $\hfv(M) \cup \hfv(A)$, and put them in \emph{any} order
$x^{A_1}_{i_1}, \dots, x^{A_n}_{i_n}$
such that if $x^{A_k}_{i_k}$ occurs in $A_l$ then $k < l$. 
Then the following judgment is derivable in the PTS: 
$$x^{A_1}_{i_1} : A_1, \dots, x^{A_n}_{i_n} : A_n \vdash M : A$$
\end{corollary}

\begin{proof} 
From the previous Theorem using Permutation. 
\end{proof}


%%%\section{Formalising the correspondence}\label{sec:formalisation}

\section{Conclusion and Further work}\label{sec:conclusion}

There are three obvious continuations of this work:
\begin{enumerate}
\item
The first is to investigate to what extent other type
theories than the PTSs admit a \gammainf\ presentation.

\item
The second is to see how well the approach presented here
can be used as a basis of an LCF-style kernel for type theory.

\item The third is to formally develop the theory presented in
	this paper in a proof assistant.
\end{enumerate}
\noindent
With respect to the first point: we expect most type theories to have
a \gammainf-variant,  
   although the observations about universe inconsistency \cite{CSC:MKM2004}
   arising from merging contexts may complicate the picture for applied type systems 
   such as that of Coq. 
More important is to
investigate how our approach needs to be adapted to support type
  theories with definitions. 
As previously noted, in any real implementation, 
the definitions for defined constants
   form 
a more significant part of the contexts $\Gamma$ we are
   eliminating 
than the free variables. 

   We are currently investigating the second point, developing an
OCaml implementation for the PTS $\lambda P$ extended with definitions
(a system corresponding to the logical framework LF) along the
lines of this paper.  
%%% 
The main question 
is how expensive, computationally, the two following operations are:
\begin{itemize}
\item
The substitutions $[y^A := \dot x]$ that occur in the $\lambda$
and $\Pi$ rules.

\item
The check of the side-condition $y^A \notin\hfvt(M,B)$ in the
$\lambda$ and $\Pi$ rules.

\end{itemize}
\noindent
The first is in some sense \scarequote{local}, because it does not look inside
   constant definitions 
in the environment.  To make the second %%%check
reasonably efficient will be harder.  It 
   is possible we
need to consider \emph{three} kinds of variables, 
   distinguishing
(1) $\dot x$ bound variables, (2) $y^A$ variables 
   to be
substituted with bound variables later (essentially, the \emph{eigenvariables} of the (\(\Pi\)) and (\(\lambda\)) rules), and (3) $x^A$ variables that 
   do 
remain free, so they may be 
   considered as 
\scarequote{axiomatic constants} of the
system. 

In such a system, it is essential that the implementation
language can use pointer equality to efficiently determine equality of
terms (and in particular, equality of annotations in variable
occurrences).  This motivated our choice of OCaml, which is such a
language.  Although in OCaml the comparison function \realquote{\ocamlcode{=}}
does not have this feature (because floating points NaNs are not 
taken to be equal
to themselves, the system never looks at pointer equality when
evaluating \realquote{\ocamlcode{x = y}}), the comparison function
\realquote{\ocamlcode{fun x y -> Pervasives.compare x y = 0}} does.

We are currently working on the third point as well. In ongoing work \cite{krebbers:gammainf} 
the second author has formalised a large part of the theory presented in this paper 
up to the first direction of the correspondence theorem in the proof assistant 
Coq. However, the presentation in this formal development 
is slightly different from that of this paper. 
\begin{itemize}
\item Firstly, we distinguish bound from free variables at the level
        of PTS pseudo-terms, following existing practice,
        established since the third author's work with Pollack in the
        1990s~\cite{mckinna-pollack:tlca1993,mckinna-pollack:jar1999}. 
        Our informal presentation
        above uses named variables in each case, the so-called
        \textit{locally named} approach, whereas the formalisation uses
        %%%More specifically, we have used the locally nameless representation: 
           the \textit{locally nameless} representation: 
        %%%
        de Bruijn indices for bound variables and 
	names for free variables. Because we make this difference at the level of 
	PTS pseudo-terms already, we have a canonical representative for each term and 
	therefore need not worry about $\alpha$-equivalence. 
        For further details of both approaches, see 
        \cite[for example]{mckinna-pollack:jar1999, aydemir:metatheory}. 
 
\item Secondly, variable binding in the ($\Pi$) and ($\lambda$) rules of 
	\gammainf\ is handled by substituting free variables for bound variables, 
        rather than bound for free as in Section~\ref{sec:Gi}. 
	%%%The choice for this presentation is motivated by the fact that it has been used 
	%%%successfully for other formalisations before. 
           This choice has been used successfully in other formalisations
           (\textit{ibid.}), and emphasises the conceptual priority of
           free variables over bound. 
           Recent work by Pollack and Sato compares the two approaches, 
           in a detailed account of canonical representation for languages 
           with binding~\cite{SatoPollack:JSC2010}. 

\end{itemize}

	Based on the methodology described in \cite{aydemir:metatheory},
	we have combined the locally nameless presentation 
        with co-finite quantification to obtain strong
	induction principles. To be sure that our co-finite presentation is
	adequate we have proved it to be equivalent to an exists-fresh presentation.

For example the ($\Pi$) rule, in respectively exists-fresh and co-finite presentation, 
is as follows.
$$
\begin{array}{llr}
(\Pi\mbox{ exists-fresh})
&
\prooftree
A : s_1\;\;\;\;
B[0:=x^A] : s_2
\justifies
\Pi A .B : s_3
\endprooftree & \mbox{if }(s_1 ,s_2 ,s_3) \in \R\mbox{ and }x^A \notin\hfv(B)\\
& & \\
(\Pi\mbox{ co-finite})
&
\prooftree
A : s_1\;\;\;\;
\forall x \notin L\ .\ B[0:=x^A] : s_2
\justifies
\Pi A .B : s_3
\endprooftree & \mbox{if }(s_1 ,s_2 ,s_3) \in \R\mbox{ and }L \subset_{\mbox{finite}} \V\\
\end{array}
$$
Observe that we require $x^A \notin\hfv(B)$ instead of $x^A \notin\hfvt(B)$ 
   (this was also observed by John Boyland).
The reason for this is that we have to bind every occurrence of the free variable 
$x^A$ in $B[0:=x^A]$, hence $x^A$ should not be in $\FV(B)$ either. While the condition is (potentially) more expensive to check, it removes the need for Definition~\ref{def:HFVT}, in favour of the (conceptually) simpler Definition~\ref{def:HFV}. 

The other direction of the correspondence theorem 
%%%requires a proof of the strengthening lemma. 
   uses the second property, Strengthening, of 
   Proposition~\ref{prop.metatheoryPTS} in an essential way. 
%%%However, previous research has learned that this 
%%%lemma is non-trivial to prove \cite{mckinna-pollack:jar1999}.
   This presents two difficulties: a practical one, since the existing
   formalisations of this lemma are highly
   non-trivial~\cite{mckinna-pollack:jar1999}; and a theoretical one,
   namely that we may \emph{not} be able to establish a correspondence
   between traditional and \gammainf{} presentations of a given type
   theory without first establishing strengthening.


More interestingly,  
   from the point of view of the pragmatics of formalisation,  
for this direction it is essential to abstract over
the kinds of free variables used in the definition of PTS judgments. At first this
does not seem troublesome, however, many definitions and theorems do not just depend on
the kind of free variables but also on finite sets of free variables. Hence we are 
also required to abstract over various operations on such finite sets. 
The recently developed finite set library 
%%%based on the new type classes feature in Coq \cite{lescuyer:containers} 
   \cite{lescuyer:containers}, based on the new type classes feature in Coq, 
might be very useful in implementing this abstraction.

\paragraph{Acknowledgments} 
Thanks to Jean-Christophe Filli\^atre for details about the
architecture of the Coq kernel.
We are grateful to the anonymous referees, and to the audience at LFMTP, especially John Boyland, Brigitte Pientka and Andrew Pitts, who made several helpful remarks, especially concerning related work. 
%%%
This research is partially funded by 
the NWO BRICKS/FOCUS project \realquote{ARPA: Advancing the Real use of Proof Assistants} 
and the NWO cluster \textsc{Diamant}. 

\bibliographystyle{eptcs}
\bibliography{Gi}

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 

% LocalWords:  Geuvers McKinna Freek Wiedijk Radboud Nijmegen Heyendaalseweg
% LocalWords:  AJ judgments pseudoterms judgment de Bruijn contextbewust Coq LCF
% LocalWords:  Conor Pollack's PTS PTSs var app conv datatype HOL stateful Agda
% LocalWords:  polymorphism ProofPower NuPRL Twelf pseudocontext pseudoterm LF
% LocalWords:  Pollack Sacerdoti Coen Matita hereditarily typable OCaml NWO env
% LocalWords:  formalization formalized Acknowledgments Diamant Mendelson Dalen
% LocalWords:  Automath mkApp alltt constr Girard optimised JHM formalised NaNs
% LocalWords:  synthesise synthesised eigenvariables Pervasives Christophe
