\documentclass{entcs}
\usepackage{entcsmacro}
\usepackage{amssymb}

\def\lP{$\lambda P$}
\def\lH{$\lambda H$}
\def\lF{$\lambda F$}
\def\alt{\mathrel{|}}
\def\V{{\cal V}}
\def\T{{\cal T}}
\def\E{{\cal E}}
\def\C{{\cal C}}
\def\J{{\cal J}}
\def\vdashP{\vdash_{\lambda P}}
\def\vdashH{\vdash_{\lambda H}}
\def\Star{\mathord{*}}
\def\qqed{\hfill$\Box$}
\def\qed{}
\def\tto{\to\hspace{-.75em}\to}
\let\D=\partial
\def\toolong{$\hspace{-4pt}$}
\def\breakentry{\\\noalign{\vspace{-.5\smallskipamount}}&&}
%%HERMAN:
\newcommand{\weg}[1]{}
\newcommand{\oftype}{{:}}
\newcommand{\pip}[2]{\{ #1, #2 \}}
\newcommand{\lap}[2]{\langle #1, #2 \rangle}
\newcommand{\abs}[1]{[#1]}
\newcommand{\eqlf}{\mathrel{=_{\lambda H}}}
\newcommand{\Ty}{\mbox{type}}
\newcommand{\TyG}{\Ty_{\Gamma}}
\newcommand{\TyC}[1]{\Ty_{\Gamma,#1}}
\newcommand{\Wf}{\mbox{wf}}
\newcommand{\Comp}{\mbox{comp}}
\newcommand{\lth}{\mbox{lth}}
\newcommand{\iif}{\,{\sf if}\,}
\newcommand{\then}{\,{\sf then}\,}
\newcommand{\eelse}{\,{\sf else}\,}
\newcommand{\true}{{\sf true}}
\newcommand{\false}{{\sf false}}
%%

\def\lastname{Geuvers and Wiedijk}

\begin{document}

\begin{frontmatter}
\title{A logical framework with explicit conversions}
\author{Herman Geuvers \and Freek Wiedijk\thanksref{ALL}\thanksref{ouremail}}
\address{Department of Computer Science, University of Nijmegen\\
Toernooiveld 1, 6525 ED Nijmegen, The Netherlands}
\thanks[ALL]{Thanks to Thorsten Altenkirch for the suggestion to
use John-Major equality in our system.}
\thanks[ouremail]{Email:
\{\href{mailto:herman@cs.kun.nl}{\texttt{\normalshape herman}},%
\href{mailto:freek@cs.kun.nl}{\texttt{\normalshape freek}}\}\texttt{\normalshape{@cs.kun.nl}}}

\begin{abstract}
The type theory {\lP} corresponds to the logical framework LF.
In this paper we present {\lH}, a variant of {\lP}
where convertibility is not implemented by means of the
customary \emph{conversion rule},
but instead type conversions are made explicit in the terms.
This means that the time to type check a {\lH} term is proportional
to the size of the term itself.

We define an \emph{erasure} map from {\lH} to {\lP}, and
show that through this map the type theory {\lH} corresponds exactly
to {\lP}:
any {\lH} judgment will be erased to a {\lP} judgment,
and conversely each {\lP} judgment can be \emph{lifted} to a {\lH} judgment.

We also show a version of subject reduction:
if two {\lH} terms are provably convertible
then their types are also provably convertible.
\end{abstract}

\end{frontmatter}

\section{Introduction}

\subsection{Problem}

This paper addresses the question whether a formal proof should
be allowed to contain the formal equivalent of the
sentence `\emph{this is left as an exercise to the reader}.'
To explain what we mean here, consider the following `proof':
\begin{quote}\label{pseudoproof}
\textbf{Theorem.}\enskip
The non-trivial zeroes of Riemann's $\zeta(s)$ function
all lie on the complex line $\Re s = {1\over 2}$.
\medskip

\noindent
\textit{Proof.}\enskip
There exists a derivation\footnote{%
The formal system in which this derivation is constructed does not
really matter.
Take any system in which one can do practical
formal proofs.
Some version of ZFC, like Mizar.
Or HOL.
Or Coq.
It does not matter.
}
of this statement with a length less than
$10^{10^{100}}$ symbols
(finding it is left as an exercise to the reader).
Therefore the statement is true.
\qqed
\end{quote}
\noindent
Now suppose that the statement in the proof about the existence of the
derivation is true.\footnote{%
Which of course we do not know.
But suppose.
}
Then would this be an acceptable proof of the Riemann hypothesis?
Can we really accept the number $10^{10^{100}}$ (which
is the only interesting thing that this `proof' contains)
to be a \emph{proof} here?
Somehow it does not seem to contain enough relevant information.

At the TYPES meeting in Kloster Irsee in 1998, there was an
interesting discussion after the talk by Henk Barendregt, where he
had explained and advocated how to use the
$\beta\delta\iota$-reduction of type theory to make Coq \cite{coq:02}
automatically do calculations during its type check phase. This uses
the technique of \emph{reflection} (see e.g.\
\cite{gwz:00,oos:geu:02} for examples and a discussion), where part of the object language is reflected in itself to make computations and reasoning on the meta-level possible within the system.

Most people clearly considered this way of using Coq's convertibility
check to be a \emph{feature}.  The only dissenting voice came from Per
Martin-L\"of, who did not like it at all and seemed to consider this
to be a \emph{bug}.
%The discussion that followed was very much `Per
%against the rest'.\footnote{Henk told us that in the meantime Per has
%changed his opinions about this.  
We do not have an overview of todays opinions, but the community seems
to be quite unanimous that this kind of `automatic calculations by
type checking' is a good thing.

In the Automath system \cite{ned:geu:vri:94}
the main performance bottleneck was the convertibility check
(if the calculated type of a term $M$ is $N$, but it is used
in a context where the type should be $N'$, then the system needs
to verify that $N =_{\beta\delta} N'$.)
In fact, the inefficiency of the convertibility check meant that
correctness of Automath was in practice only semi-decidable.
Although in theory it is decidable whether an Automath text is
type correct, in practice when it is \emph{not} correct the system
often just would be endlessly reducing and would not terminate in
an acceptable time anymore.\footnote{%
This problem is less noticeable in Coq because there many definitions
are `opaque' (they cannot be unfolded).
}
For this reason
the Automath system from the seventies just gave up after having
failed to establish convertibility after some given number of reduction
steps.
Automath apparently \emph{searched} for a `convertibility proof'.
This proof would have to be rediscovered every time the Automath terms would
be type checked, and it would not be stored in a `convertibility proof term'.

The LF system \cite{pfe:sch:99} (currently implemented in the Twelf system \cite{har:hon:plo:87}),
which is the best known \emph{logical framework},
has -- like Automath and Coq -- a conversion rule.
But the HOL system \cite{gor:mel:93,har:00} does not.
In HOL $\beta$-reduction is not automatically tried by the
system, but is one of the derivation rules of the logic.
Similarly $\delta$- and $\iota$-reductions are
performed using the rules of the logic.
If one considers a HOL `proof term' that stores the HOL rules that
have been used to obtain a certain theorem \cite{ber:00}, then
this proof term somehow documents the `reduction information'
that is not available in a proof term from the type theoretical/LF
world.\footnote{%
Of course, as the HOL logic does not have dependent types, this kind
of reduction is much less important in the first place.
}

The goal of this paper is to investigate whether it is possible
to have a system close to the systems from type theory, but in which
the convertibility of types \emph{is} explicitly stored in the proof terms
(like it is done in HOL).
In such a system the type checker will not need to do a convertibility
check on its own.
Instead the term will contain the information needed to establish
the convertibility.
In such a system the type of a term
will be \emph{unique},
instead of only being unique \emph{up to conversion}.\footnote{%
So in such a system the type of a term will be
$(\lambda x{:}A. B)\, a$, or it will be $B[x := a]$, but not \emph{both}.
}
Because of all this, type checking a term will be cheap.
If we consider the substitution operation
and term identity checking to take unit time,
the time to type check a term will be \emph{linear} in the size of the term.

In the system that we describe in this paper,
checking a proof matches much more the image of `following the proof with
your little finger, and checking locally that everything is correct'
than is the case with the standard type theoretical proof systems.

\subsection{Approach}

We define a system called {\lH}.\footnote{%
The `$H$' in the name of the system reflects the letter that we use
for the convertibility proof terms.
So {\lH} is `the logical framework with $H$s', i.e., with convertibility proofs.}
This system is very close to {\lP}, the proper type system that corresponds to LF.
However, there is no conversion rule.
Instead conversions are made explicit in the terms.
If $H$ is a term that shows that $A$ is convertible to $A'$,
which we will write as
$$\vdash H : A = A'$$
and if the term $a$ has type $A$,
then the term $a^H$ (the conversion $H$ applied to $a$)
will have type $A'$.

Note that in our system we have explicit `equality judgments'
just like in Martin-L\"of style type theory \cite{nor:pet:smi:90}.
However there is a significant difference.
In Martin-L\"of style type theory there are no terms that prove equalities.
The equality judgments in such theories look like:
$$\vdash A = A' : B$$
and the equality is on the \emph{left} of the colon.
In contrast, in our system two terms that are provably equal
do not need to have the same computed type, so there will not be a
common type to the right of the colon.
Instead we will have a proof term, and so our equality will be to
the \emph{right} of the colon.

The fact that two terms in our system that occur in an equality
judgment do not need to have
computed types that are syntactically equal,
means that our judgmental equality is a version
of \emph{John-Major equality} \cite{mcb:99}.

\subsection{Related Work}

Robin Adams is working on a version of pure type systems
that have judgmental equalities in the style of Martin-L\"of type theories \cite{ada:03}.
However, he does not have terms in his system that represent the derivation
of the equality judgments.
Also, he does not represent the conversions themselves in the terms.
Therefore in his system more terms are syntactically identical
than in our system.
Another difference is that
he develops his system for all functional pure type systems,
while we only have a system that corresponds to {\lP}.

\subsection{Contribution}

We define a system {\lH} in which type conversion is represented in the
proof term.
%
We show that this system corresponds exactly to the proper type system
{\lP}.
We also show that this system has a property closely related to subject
reduction.

The {\lH} system is quite a bit more complicated than the {\lP}
system.  It has 13 instead of 4 term constructors, and
15 instead of 7 derivation rules.

\subsection{Outline}

In Section~\ref{section:system} we define our system.  In
Section~\ref{section:correspondence} we show that it corresponds to
the {\lP} system.  In Section~\ref{section:SR} we show that an analog
of the subject reduction property of {\lP} holds for our system.  In
Section~\ref{section:reduction} we define a weak reduction relation
for our equality proof terms that is confluent and strongly
normalizing and that satisfies subject reduction.  Finally, in
Section~\ref{section.future} we present a slight modification of our
system, where we do not allow conversions to go through the ill-typed
terms. Such a system corresponds more closely to a semantical view
upon type theory.

\section{The system {\lH}}\label{section:system}

\begin{definition}
The {\lH} expressions are given by the following grammar (the syntactic category $\V$ are
the variable names):
\begin{eqnarray*}
\T &::=& \Box \alt \Star \alt \Pi \V{:}\T. \T \alt \lambda \V{:}\T. \T \alt \T \T \alt \T^\E \\
\E &::=& \bar\T \alt \E^\dagger \alt \E\cdot\E \alt \beta(\T) \alt \iota(\T) \alt \pip{\E}{\abs{\V}\E} \alt \lap{\E}{\abs{\V}\E} \alt \E \E \\
\noalign{\medskip}
\C &::=& {} \; \alt \C, \V:\T \\
\J &::=& \C \vdash \T:\T \;\alt\; \E:\T = \T
\end{eqnarray*}
\end{definition}

\noindent
The $\T$ are the terms of the system,
the $\E$ are convertibility proofs,
the $\C$ are the contexts, and
the $\J$ are the judgments.
%
The \emph{sorts} are the special cases of $\T$ that are the elements of $\{\Box,\Star\}$.

\begin{definition}
We define the \emph{erasure} operation recursively by:
\begin{eqnarray*}
|x| & \equiv & x \\
|\Box| & \equiv & \Box \\
|\Star| & \equiv & \Star \\
|\Pi x{:}A. B| & \equiv & \Pi x{:}|A|. |B| \\
|\lambda x{:}A. b| & \equiv & \lambda x{:}|A|. |b| \\
|Fa| & \equiv & |F| |a| \\
|a^H| & \equiv & |a|
\end{eqnarray*}
It maps {\lH} terms to {\lP} terms and is extended straightforwardly
to contexts.
\end{definition}

There are two kinds of judgments in {\lH}: {\em equality judgments\/}
and {\em typing judgments}. The first are of the form $H :a =
b$, where $H$ codes a proof of convertibility (through not
necessarily well-typed terms) of $a$ and $b$. The rules for equality
judgments are independent of typing judgments. In the rules for the
typing judgments, equality judgments appear as a side-condition (in
the rule for conversion). 

\begin{definition}
The rules that inductively generate the {\lH}
judgments are the following (in these rules $s$ only ranges over
sorts):
\vspace{-\smallskipamount}

\paragraph{definitional equality}

$$
\over
\bar{A} : A = A
$$

$$
H : A = A'
\over
H^\dagger : A' = A
$$

$$
H : A = A'
\quad
H' : A' = A''
\over
H \cdot H' : A = A''
$$

\paragraph{$\beta$-redex}
$$
\over
\beta((\lambda x{:}A. b)\, a) : (\lambda x{:}A. b)\, a = b[x := a]
$$

\paragraph{erasing equality proofs}
$$
\over
\iota(a) : a = |a|
$$

\paragraph{congruence rules}

$$
 H : A = A'
\quad
H' : B = B'
\over
\pip{H}{\abs{x} H'} : \Pi x{:}A. B = \Pi x{:}A'. B'
$$

$$
 H : A = A'
\quad
H' : B = B'
\over
\lap{H}{\abs{x} H'} : \lambda x{:}A. B = \lambda x{:}A'. B'
$$

$$
 H : F = F'
\quad
 H' : a = a'
\over
 H H' : F a = F' a'
$$

\paragraph{start \& weakening}

$$
\Gamma \vdash A : s
\over
\Gamma, x : A \vdash x : A
$$

$$
\Gamma \vdash A : s
\quad
\Gamma \vdash b : B
\over
\Gamma, x : A \vdash b : B
$$

\paragraph{box \& star}

$$
\vdash \Star : \Box
$$

\paragraph{typed lambda terms}

$$
\Gamma \vdash A : \Star
\quad
\Gamma, x : A \vdash B : s
\over
\Gamma \vdash \Pi x{:}A. B : s
$$

$$
\Gamma \vdash A : \Star
\quad
\Gamma, x : A \vdash b : B : s
\over
\Gamma \vdash \lambda x{:}A. b : \Pi x{:}A. B
$$

$$
\Gamma \vdash F : \Pi x{:}A. B
\quad
\Gamma \vdash a : A
\over
\Gamma \vdash F a : B[x := a]
$$

\paragraph{conversion}

$$
\Gamma \vdash a : A
\quad
 H : A = A'
\over
\Gamma \vdash a^H : A'
$$
\end{definition}


\noindent
%It will be clear that the variables in the two `binders' that are 
%introduced in
%the congruence rules, do not actually bind the $H$ but instead bind the 
%left hand side
%$A$ of the equality that is the type of $H$.

We write $\Gamma \vdash A : B : C$ as an abbreviation of $\Gamma \vdash A : B$ and
$\Gamma \vdash B : C$.
We write $A \eqlf A'$ if we have that
$H : A = A'$ for some $H$.
We write `$A$ is type correct in context $\Gamma$' if we have that
$\Gamma \vdash A : B$ for some $B$.
We write `$A$ is type correct' if it is type correct in some context.
We write `$\Gamma$ is well-formed' if some derivable judgment has
$\Gamma$ as the context.
Finally we will write derivability in {\lH} as
$\vdashH$ to distinguish it from derivability in {\lP} which is written
$\vdashP$.
(If we omit the subscript, it will be apparent from the context which
system is meant.)

The following lemmas about {\lH} are immediate:

\begin{lemma}
Any subterm of a type correct term is type correct (in the appropriate context).
\end{lemma}

%\begin{lemma}
%If $\Gamma \vdash A = A'$ then $A$ and $A'$ are type correct in
%context $\Gamma$.
%\end{lemma}

\begin{lemma}
If $\Gamma \vdash A : B : C$ then $C$ is a sort.
\end{lemma}

\begin{lemma}
If $\Gamma \vdash a : A$ then either
$\Gamma \vdash A : s$ for some sort $s$, or $A \equiv \Box$.
\end{lemma}

\begin{lemma}[uniqueness of types]
If $\Gamma \vdash a : A$ and $\Gamma \vdash a : A'$ then $A \equiv A'$.
\end{lemma}

We now show that typing is in linear time by defining a type checking algorithm.

\begin{definition}
Define the function $\Ty :\C \times \T \rightarrow \T\cup\{\false\}$
simultaneously with the functions $\Wf: \C \rightarrow \{\true,
\false\}$ and $\Comp : \E \times\T \rightarrow \T \cup\{\false\}$ as
follows.
\begin{eqnarray*}
\TyG(\Star) &=& \iif \Wf(\Gamma)\then \Box \eelse \false\\
\TyG(\Box) &=& \false\\
\TyG(x) &=& \iif \Wf(\Gamma)\wedge (x\oftype A) \in\Gamma \then A \eelse \false\\
\TyG(\Pi x\oftype A.B) &=& \iif \TyG(A) \equiv \Star \wedge 
\TyC{x\oftype A} (B) \in\{\Star, \Box\} \breakentry \then \TyC{x\oftype A} (B) \eelse \false \hspace{-33pt}\\
\TyG(\lambda x\oftype A.M) &=& \iif \TyG(A) \equiv \Star \wedge \TyC{x\oftype A} (M) \neq\Box
\breakentry \then \Pi x\oftype A.\TyC{x\oftype A} (M) \eelse \false \hspace{-33pt}\\
\TyG(MN) &=& \iif \TyG(M) \equiv \Pi x\oftype \TyG(N).B \breakentry \then B[x:=N] \eelse \false\\
\TyG(M^H) &=& \iif \TyG(M) \equiv A \then \Comp(H,A) \eelse \false \\
\noalign{\bigskip}
%\end{eqnarray*}
%
%\begin{eqnarray*}
\Wf(\langle -\rangle) &=& \true\\
\Wf(\Gamma, x\oftype A) &=& \TyG(A) \in\{\Star,\Box\} \\
\noalign{\bigskip}
%\end{eqnarray*}
%
%\begin{eqnarray*}
\Comp(\bar{A}, B) &=& \iif A \equiv B \then B \eelse \false\\
\Comp(H^{\dagger}, B) &=& \Comp^{-1}(H, B)\\
\Comp(H\cdot H', B) &=& \Comp(H',\Comp(H, B))\\
\Comp(\iota(A), B) &=& \iif A\equiv B \then |A| \eelse \false\\
\Comp(\beta((\lambda x\oftype A.M)N), B) &=& \iif B \equiv (\lambda x\oftype A.M)N \then M[x:= N]\eelse \false\\
\Comp(\pip{H}{[x]H'}, B) &=& \iif B \equiv \Pi y\oftype A.C \breakentry \then \Pi x\oftype \Comp(H,A).\Comp(H', C[y:=x]) \breakentry \eelse \false \hspace{-59pt}\\
\Comp(\lap{H}{[x]H'}, B) &=& \iif B \equiv \lambda y\oftype A.C \breakentry \then \lambda x\oftype \Comp(H,A).\Comp(H', C[y:=x]) \breakentry \eelse \false \hspace{-59pt}\\
\Comp(HH', B) &=& \iif B \equiv AC \breakentry \then \Comp(H,A)\Comp(H', C)\eelse \false
\end{eqnarray*}

\noindent
The function $\Comp^{-1}$ is defined totally similar to $\Comp$, with two exceptions:
\begin{eqnarray*}
\Comp^{-1}(\iota(A), B) &=& \iif |A|\equiv B \then A \eelse \false\\
\Comp^{-1}(\beta((\lambda x\oftype A.M)N), B) &=& \iif B \equiv  M[x:= N]\then (\lambda x\oftype A.M)N \eelse \false\mbox{\toolong}
\end{eqnarray*}
\end{definition}

\begin{proposition}[type checking] 
$\Gamma \vdashH a:A$ if and only if $\Ty(\Gamma, a) \equiv A$ and the
time for $\Ty$ to compute an answer is linear in the length of the
inputs.
\end{proposition}

\begin{proof}
One first proves the fact that, $H: B=C$ if and only if $\Comp(H,B)
=C$. Then $\Gamma \vdashH a:A$ implies $\Ty(\Gamma, a) \equiv A$ is
proved by induction on the derivation, simultaneously with `$\Gamma$
is well formed' implies $\Wf(\Gamma) =\true$. The other way around, one
proves simultaneously that $\Ty(\Gamma, a) \equiv A$ implies $\Gamma
\vdashH a:A$ and that $\Wf(\Gamma) =\true$ implies `$\Gamma$ is
well formed' (by induction over the length of the input: $\lth(\Gamma,
a)$, resp. $\lth(\Gamma)$).\\ $\Comp(H,A)$ is clearly linear in the
size of the equational proof term $H$. To make sure that $\Ty$
computes a type in linear time, one has to collect the `side
conditions' $\Wf(\Gamma)$ properly to avoid checking the
well-foundedness of the (local) context for every variable separately. \qed
\end{proof}



\section{Correspondence to {\lP}}\label{section:correspondence}

\begin{lemma}
If $A \eqlf A'$ then $|A| =_\beta |A'|$.
\end{lemma}

\begin{proof}
By induction on the derivation of $A \eqlf A'$.
\end{proof}


\begin{proposition}[`from {\lH} to {\lP}']\label{proposition:F-to-P}
If $\Gamma \vdashH a : A$ then $|\Gamma| \vdashP |a| : |A|$.
\end{proposition}

\begin{proof}
By induction on the derivation of $\Gamma \vdashH a : A$, using the
previous Lemma in the conversion rule.
\end{proof}

\weg{
\begin{definition}
We define the partial operation $\D$ recursively by:
\begin{eqnarray*}
\D(x) && \emph{undefined} \\
\D(\Box) && \emph{undefined} \\
\D(\Star) && \emph{undefined} \\
\D(\Pi x{:}A. B) & \equiv & A \\
\D(\lambda x{:}A. b) & \equiv & \lambda x{:}A. \D(b) \\
\D(Fa) & \equiv & \D(F)\, a \\
\D(a^H) & \equiv & \D(a)^H
\end{eqnarray*}
This definition should be read to be \emph{strict}, so
if the $\D(\ldots)$ on the right hand side is undefined,
the whole expression is undefined.
\end{definition}

\begin{lemma}\label{lemma:D-eq}
If $\Gamma \vdashH A = A'$ then $\D(A)$ is defined iff $\D(A')$ is defined,
and if both are defined then $\Gamma \vdashH \D(A) = \D(A')$.
\end{lemma}

\begin{lemma}
If $\Gamma \vdashH \Pi x{:}A. B = \Pi x{:}A'. B'$ then
$\Gamma \vdashH A = A'$.
\end{lemma}
\begin{proof}
Directly from Lemma~\ref{lemma:D-eq}.
\qed
\end{proof}

\begin{proposition}\label{proposition:P-to-F-conv}
If $A$ and $A'$ are type correct in context $\Gamma$ and
$|A| =_\beta |A'|$ then $\Gamma \vdashH A = A'$.
\end{proposition}

\begin{proposition}
If $\Gamma \vdashH A : B$ and $|\Gamma| \vdashP a' : |A|$ then
there exists a {\lH}-term $a$ such that $|a| \equiv a'$ and $\Gamma \vdashH a : A$.
\end{proposition}

\begin{corollary}[`from {\lP} to {\lH}']
If $\Gamma' \vdashP a' : A'$ then there exist $\Gamma$ and $a$ and $A$
with $|\Gamma| \equiv \Gamma'$ and $|a| \equiv a'$ and $|A| \equiv A'$ such that
$\Gamma \vdashH a : A$.
\end{corollary}
}

\begin{lemma}\label{lemma.eqlf}
For $A, A' \in \T$, 
\begin{enumerate}
\item if $|A|\equiv |A'|$, then $A\eqlf A'$,
\item if $|A|=_{\beta} |A'|$, then $A\eqlf A'$. 
\end{enumerate}
\end{lemma}

\begin{proof}
\begin{enumerate}
\item If $|A|\equiv |A'|$, then $\iota (A) \cdot \overline{\iota{A'}} : A = A'$.
\item If $|A|=_{\beta} |A'|$, we first prove that $|A|\eqlf |A'|$, by
induction on the proof (in the equational theory of the
$\lambda$-calculus) of $|A|=_{\beta} |A'|$. Then we conclude by using
that $\iota(A) : A=|A|$. We do some cases
\begin{itemize}
\item $A\equiv\Pi x\oftype B.C$ and $A'\equiv \Pi x\oftype B'.C'$ and 
$|\Pi x\oftype B.C| =_{\beta} |\Pi x\oftype B'.C'|$ was derived from
$|B|=_{\beta} |B'|$ and $|C|=_{\beta} |C'|$. By IH, $H_0: |B|=|B'|$ and $H_1 :
|C|=|C'|$ for some $H_0$, $H_1$, so $\pip{H_0}{\abs{x}H_1} : |\Pi x\oftype
B.C| = |\Pi x\oftype B'.C'|$.
\item $A\equiv (\lambda x{:}B.M)P$, $A'\equiv M'[P'/x]$ with $|(\lambda x{:}B.M)P| \rightarrow_{\beta} |M'[P'/x]|$. Then $\beta((\lambda x{:}B.M)P) : (\lambda x{:}B.M)P = M[P/x]$ and we are done by two applications of (i) (using $|M[P/x]|\equiv |M'[P'/x]|$).
\end{itemize}
\end{enumerate}
\end{proof}


\begin{proposition}[`from {\lP} to {\lH}']\label{proposition:P-to-F-conv}
Let $\Gamma$ be a {\lP}-context and $a,A$ be {\lP}-terms such that
$\Gamma \vdashP a:A$. Then the following two properties hold.
\begin{enumerate}
\item There is a correct {\lH}-context $\Gamma'$ such that $|\Gamma'| \equiv \Gamma$.
\item For all {\lH}-contexts $\Gamma'$ for which $|\Gamma'| \equiv \Gamma$, there are {\lH}-terms $a', A'$ such that $\Gamma'\vdashH a':A'$ and $|a'|\equiv a$, $|A'|\equiv A$. 
\end{enumerate}
\end{proposition}

\begin{proof}
Simultaneously by induction on the {\lP} derivation, distinguishing
cases according to the last applied rule. We treat four cases and
abbreviate `induction hypothesis' to IH.
\begin{itemize}
\item (application)
$$
\Gamma \vdashP F : \Pi x{:}A. B
\quad
\Gamma \vdashP a : A
\over
\Gamma \vdashP F a : B[x := a]
$$ 
The IH states that there is an {\lH}-context $\Gamma'$ such that
$|\Gamma'| \equiv \Gamma$. Furthermore, for $\Gamma'$ any
{\lH}-context such that $|\Gamma'|\equiv \Gamma$, by IH, there are
$F', a', A', A''$ and $B'$ such that $\Gamma' \vdashH F' :\Pi x\oftype
A'.B'$, $\Gamma' \vdashH a' : A''$ and $|F'| \equiv F$, $|a'|\equiv
a$, $|A'|\equiv |A''| \equiv A$ and $|B'|\equiv B$. By Lemma
\ref{lemma.eqlf}, we have $H: A''=A'$ for some $H$, so $\Gamma'
\vdashH a'^H :A'$ and $\Gamma' \vdash F a'^H : B'[a'^H/x]$. We are
done, because $|F a'^H| \equiv F a$ and $|B'[a'^H/x]| \equiv B[a/x]$.
\item ($\lambda$)
$$
\Gamma,x\oftype A \vdashP M:B 
\quad
\Gamma \vdashP  A :\star
\over
\Gamma \vdashP \lambda x\oftype A. M : \Pi x\oftype A.B
$$ The IH states that there is an {\lH}-context $\Gamma'$ such that
$|\Gamma'| \equiv \Gamma$. Furthermore, for $\Gamma'$ any
{\lH}-context such that $|\Gamma'|\equiv \Gamma$, by IH, there is an
$A'$ such that $\Gamma' \vdashH A' :\star$ and $|A'|\equiv A$. So
$\Gamma', x\oftype A'$ is a correct {\lH}-context. So, by IH there are
$M'$ and $B'$ such that $\Gamma', x\oftype A'\vdashH M':B'$ and
$|M'|\equiv M$ and $|B'|\equiv B$. Hence, $\Gamma' \vdash \lambda
x\oftype A'. M' : \Pi x\oftype A'.B'$ and we are done, because
$|\lambda x\oftype A'.M'| \equiv \lambda x\oftype A.M$ and $|\Pi
x\oftype a'.B'| \equiv \Pi x\oftype A.B$.
\item (conversion)
$$
\Gamma \vdashP M:A 
\quad
\Gamma \vdashP  B :s
\quad
A=_{\beta} B
\over
\Gamma \vdashP M^H : B
$$ The IH states that there is an {\lH}-context $\Gamma'$ such that
$|\Gamma'| \equiv \Gamma$. Furthermore, for $\Gamma'$ any
{\lH}-context such that $|\Gamma'|\equiv \Gamma$, by IH, there is are
$M', A', B'$ such that $\Gamma' \vdashH M' :A'$, $\Gamma \vdashH B'
:s$ and $|A'|\equiv A$, $|B'|\equiv B$, $|M'|\equiv M$.  So
$|A'|\equiv A =_{\beta} B\equiv |B'|$ and by Lemma \ref{lemma.eqlf},
$H:A'=B'$ for some $H$. Now, $\Gamma'\vdashH M':B'$ by the conversion
rule in {\lH} and we are done.
\item (weakening)
$$
\Gamma \vdashP  A :\star
\quad
\Gamma \vdashP M:B 
\over
\Gamma, x\oftype A \vdashP  M : B
$$ The IH states that there is an {\lH}-context $\Gamma'$ such that
$|\Gamma'| \equiv \Gamma$. By IH, there is an
$A'$ such that $\Gamma' \vdashH A' :\star$ and $|A'|\equiv A$. So
$\Gamma', x\oftype A'$ is a correct {\lH}-context, proving part (1). Now, for any {\lH} context $\Gamma',x\oftype A'$ such that $|\Gamma',x\oftype A'| \equiv \Gamma, x\oftype A$, we know that $|\Gamma'|\equiv \Gamma$, so, by IH there are
$M'$ and $B'$ such that $\Gamma'\vdashH M':B'$ and
$|M'|\equiv M$ and $|B'|\equiv B$. As $\Gamma',x\oftype A'$ is correct, we can weaken this to obtain $\Gamma',x\oftype A'\vdashH M':B'$ and we are done. 
\end{itemize}
\end{proof}

\begin{corollary}[conservativity of {\lP} over {\lH}]
Given a well-formed {\lH} context $\Gamma$ and {\lH} type $A$ in $\Gamma$,
$$|\Gamma|\vdashP M:|A| \Rightarrow \exists M'(\Gamma \vdashH M:A \wedge |M'|\equiv M)$$
\end{corollary}


\begin{proof}
The second part of the Proposition ensures that there are $N$ and $B$
such that $\Gamma \vdashH N:B$ and $|N|\equiv M$ and $|B|\equiv
|A|$. Then $B \eqlf A$, due to Lemma \ref{lemma.eqlf}, say $H: B =
A$. Then $\Gamma \vdashH N^H : A$. \qed
\end{proof}

\section{An analogue of subject reduction}\label{section:SR}

The following proposition is the equivalent for {\lH} of the subject
reduction property of {\lP}.  The system {\lH} does not have a notion
of $\beta$-reduction, so the statement $a \to_\beta a'$ in the
condition of the statement is replaced by $a \eqlf a'$.
Also, we do not get that the type is conserved, it just is conserved
up to convertibility (so if $a = a'$ and $a : A$ then we will not
always get that $a' : A$, but just that $a' : A'$ for some $A'$ with
$A = A'$.)

\begin{proposition}[`subject reduction']
If $\Gamma \vdashH a : A : s$ and $\Gamma \vdashH a' : A' : s'$ and $a \eqlf a'$
then $A \eqlf A'$ and $s \equiv s'$.
\end{proposition}
\begin{proof}
{}From Proposition~\ref{proposition:F-to-P} we get that
$|\Gamma| \vdashP |a| : |A| : s$ and $|\Gamma| \vdashP |a'| : |A'| : s'$ and $|a| =_\beta |a'|$.
By subject reduction of {\lP} and uniqueness of types in {\lP} we get that
$|A| =_\beta |A'|$ and $s \equiv s'$.
{}From Lemma \ref{lemma.eqlf} we finally get that
$A \eqlf A'$.
\qed
\end{proof}


\section{Conversion reduction}\label{section:reduction}

\begin{definition}
We define the \emph{conversion reduction} relation $\tto$
as the rewrite relation
of the following rewrite rules:%\footnote{%
%In the first rule, if the term is type correct, then $A' \equiv A$.}
\begin{eqnarray*}
A^{\overline {A'}} & \to & A \\
A^{H \cdot H'} & \to & {(A^H)}^{H'} \\
\strut{\bar A}^\dagger & \to & {\bar A} \\
{H^\dagger}{}^\dagger & \to & H \\
{(H \cdot H')}{}^\dagger & \to & {H'}^\dagger \cdot H^\dagger
\end{eqnarray*}
\end{definition}

\noindent
We will now list some simple properties of conversion reduction
(with some proofs omitted for space reasons):

\begin{proposition}
Conversion reduction is confluent.
\end{proposition}

\begin{proposition}
Conversion reduction is strongly normalizing.
\end{proposition}

\noindent
(These two propositions even hold for terms that are not type correct.)

\begin{proposition}[subject reduction for conversion reduction] \ \\
If $\Gamma \vdashH a : A$ and $a \tto a'$ then $\Gamma \vdashH a' : A$.
\end{proposition}
\begin{proof}
By induction on the derivation of $\Gamma \vdashH a : A$ one proves that, if $a\rightarrow a'$, then $\Gamma \vdashH a':A$, distinguishing cases according 
to the applied reduction step.
(The $a\tto a'$ case then follows immediately.)
\qed
\end{proof}

\noindent
Although this proposition is a subject reduction property,
it is \emph{not} related to the subject reduction property of {\lP},
as it does not involve $\beta$-reduction.

\begin{proposition}
If $\Gamma \vdashH a : A$ and $a \tto a'$ then $a \eqlf a'$.
\end{proposition}
\begin{proof}
If $a \tto a'$, then $|a| \equiv |a'|$ and hence $a 
\eqlf a'$ by Lemma \ref{lemma.eqlf}.
\qed
\end{proof}

\begin{proposition}
A term that is in conversion reduction normal form
does not contain the operations $\bar A$ and $H \cdot H'$,
and it only contains the operation $H^\dagger$ in the combinations
$\beta(\ldots)^\dagger$ and $\iota(\ldots)^\dagger$.
\end{proposition}

\noindent
This last proposition shows that we can do away with the $\bar A$
and $H \cdot H'$ operations in our system.


%\section{Conclusion}
\section{Discussion}

Imagine formalizing the `proof' of the Riemann hypothesis on
page~\pageref{pseudoproof} in Coq.
Using reflection this would be doable
(even constructively)
and, if the Riemann hypothesis
has a proof, it would actually be a correct proof too.
However, type checking this proof would be completely infeasible.

Now imagine a version of Coq that is built on top of the logical
framework {\lH}.
When type checking this Coq `proof' the system would need to store
the reduction information in the explicit conversions in the {\lH}
proof term that it would build internally.
Therefore that proof term would be impractically big.
So in such a system the proof would not be considered to be a \emph{real} proof
as the
underlying {\lH} proof object would be impossible to construct.

For this reason {\lH} adequately represents both our unease with
our `proof' of the Riemann hypothesis, as well as Per's unease
with Henk's talk in Kloster Irsee.

(Note that this formalization of the `proof' of the Riemann hypothesis
needs $\iota$-reduction, so it is not possible in LF itself.
Therefore for our argument one needs to imagine a version of Coq's type
theory that has explicit conversions: a system that relates
to the calculus of inductive constructions CiC, in the same way that
the system {\lH} relates to {\lP}.)

\section{Future work}\label{section.future}

An interesting thing to do now is to implement {\lH} as the
basis of an actual proof assistant, to see whether it is a practical
system for doing actual proof checking.
Part of such a system might be a term \emph{lifter} that lifts
proof terms from {\lP} to {\lH}, inserting the conversions that were
needed to make the terms type check.

Another issue is whether it is possible to build such a system in a
way that the bulk of the proof terms will not actually be stored in
memory, but checked and discarded while it is being generated.
This is the way that HOL checks its proofs.
Henk Barendregt calls this \emph{ephemeral proofs}.
So the question is whether it will be possible to have a {\lH} implementation
with ephemeral proof terms.

\subsection{Avoiding ill-typed terms}
In the system {\lH}, we have avoided the conversion rule by
introducing proof terms that witness an equality (and that can be
checked in linear time). But the conversion goes through $\T$, the set
of `pseudo-terms'. This is in line with most implementations of proof
checkers, where equality checking is done by a separate algorithm that
does not take typing into account. But what if we restrict equalities
to conversions that pass through the well-typed terms only? This is
more in line with a semantical intuition, where the ill-typed terms
just do not exist. We can adapt the syntax of {\lH} to cover this
situation and we put the question whether this system is equivalent to
{\lH}. We call this new system {\lF}.\footnote{%
The `$F$' stands for `fully well-typed'.}

The system {\lF} has the same terms and equality proofs as {\lH}, but the judgments are different:
\begin{eqnarray*}
\J &::=& \C \vdash \T:\T \;\alt\; \C \vdash \E:\T = \T
\end{eqnarray*}
\noindent
So an equality in {\lF} is always stated and proved {\em within\/} a context, in which the terms are well-typed. The rules that inductively generate the {\lF} judgments are the same as for {\lH}, apart from the rules that involve equalities, which are as follows (in these rules $s$ only ranges over sorts):
\vspace{-\smallskipamount}

\paragraph{definitional equality}

$$
\Gamma \vdash A : B
\over
\Gamma \vdash \bar{A} : A = A
$$

$$
\Gamma \vdash H : A = A'
\over
\Gamma \vdash H^\dagger : A' = A
$$

$$
\Gamma \vdash H : A = A'
\quad
\Gamma \vdash H' : A' = A''
\over
\Gamma \vdash H \cdot H' : A = A''
$$

\paragraph{$\beta$-redex}
$$
\Gamma \vdash A : \Star
\quad
\Gamma, x : A \vdash b : B : s
\quad
\Gamma \vdash a : A
\over
\Gamma \vdash \beta((\lambda x{:}A. b)\, a) : (\lambda x{:}A. b)\, a = b[x := a]
$$

\paragraph{conversion}

$$
\Gamma \vdash a : A
\quad
\Gamma \vdash H : A = A'
\over
\Gamma \vdash a^H : A'
$$

$$
\Gamma \vdash a : A
\quad
\Gamma \vdash H : A = A'
\over
\Gamma \vdash \iota(a^H) : a = a^H
$$

\paragraph{congruence rules}

$$
\begin{array}{c}
\Gamma \vdash A : \Star
\quad
\Gamma, x : A \vdash B : s
\\
\noalign{\vspace{-\medskipamount}}
\Gamma \vdash A' : \Star
\quad
\Gamma, x' : A' \vdash B' : s
\\
\noalign{\vspace{-\medskipamount}}
\Gamma \vdash H : A = A'
\quad
\Gamma, x : A \vdash H' : B = B'[x' := x^H]
\end{array}
\over
\Gamma \vdash \pip{H}{[x{:}A]H'} : \Pi x{:}A. B = \Pi x'{:}A'. B'
$$

$$
\begin{array}{c}
\Gamma \vdash A : \Star
\quad
\Gamma, x : A \vdash b : B : s
\\
\noalign{\vspace{-\medskipamount}}
\Gamma \vdash A' : \Star
\quad
\Gamma, x : A' \vdash b' : B' : s
\\
\noalign{\vspace{-\medskipamount}}
\Gamma \vdash H : A = A'
\quad
\Gamma, x : A \vdash H' : b = b'[x' := x^H]
\end{array}
\over
\Gamma \vdash \lap{H}{[x{:}A]H'} : \lambda x{:}A. b = \lambda x{:}A'. b'
$$

$$
\begin{array}{c}
\Gamma \vdash F : \Pi x{:}A. B
\quad
\Gamma \vdash a : A
\\
\noalign{\vspace{-\medskipamount}}
\Gamma \vdash F' : \Pi x'{:}A'. B'
\quad
\Gamma \vdash a' : A'
\\
\noalign{\vspace{-\medskipamount}}
\Gamma \vdash H : F = F'
\quad
\Gamma \vdash H' : a = a'
\end{array}
\over
\Gamma \vdash H H' : F a = F' a'
$$

\medskip
\noindent
(Note that the $\iota(\dots)$ of {\lF} just removes one conversion,
in contrast to the $\iota(\dots)$ of {\lH} which removes all conversions
at once.
Removing all conversions generally leads to a term that is not
well-typed, so that is not an option for {\lF} where all terms have
to be well-typed, even in the conversion proofs.)

%\bibliographystyle{plain}
%\bibliography{frk}

\begin{thebibliography}{1}

\bibitem{ada:03}
Robin Adams.
\newblock {Pure Type Systems with Judgemental Equality}.
\newblock Unpublished, 2003.

\bibitem{ber:00}
Stefan Berghofer.
\newblock {New features of the Isabelle theorem prover -- proof terms and code
  generation}, 2000. \\
\newblock
  \href{http://www4.in.tum.de/~berghofe/papers/TYPES2000_slides.ps.gz}
  {\texttt{http://www4.in.tum.de/\char`\~berghofe/papers/TYPES2000\char`\_slides.ps.gz}}

\bibitem{gwz:00}
H. Geuvers, F. Wiedijk, J. Zwanenburg, Equational Reasoning via
Partial Reflection, in {\em Theorem Proving for Higher
Order Logics}, TPHOL 2000, Portland OR, USA, eds. M. Aagaard and
J. Harrison, LNCS 1869, pp. 162--178.

\bibitem{gor:mel:93}
M.J.C. Gordon and T.F. Melham, editors.
\newblock {\em Introduction to HOL}.
\newblock Cambridge University Press, Cambridge, 1993.

\bibitem{har:hon:plo:87}
Robert Harper, Furio Honsell, and Gordon Plotkin,
A framework for defining logics, in {\em Symposium on Logic in Computer Science\/}, IEEE Computer Society Press, 1987, pp. 194--204.

\bibitem{har:00}
John Harrison.
\newblock {\em The HOL Light manual (1.1)}, 2000. \\
\newblock \href{http://www.cl.cam.ac.uk/users/jrh/hol-light/manual-1.1.ps.gz}
{\texttt{http://www.cl.cam.ac.uk/users/jrh/hol-light/manual-1.1.ps.gz}}

\bibitem{mcb:99}
Conor McBride.
\newblock {\em Dependently Typed Functional Programs and their Proofs}.
\newblock PhD thesis, University of Edinburgh, 1999. \\
\newblock \href{http://www.dur.ac.uk/c.t.mcbride/thesis.ps.gz}
{\texttt{http://www.dur.ac.uk/c.t.mcbride/thesis.ps.gz}}

\bibitem{ned:geu:vri:94}
R.P. Nederpelt, J.H. Geuvers, and R.C. de~Vrijer.
\newblock {\em Selected Papers on Automath}, volume 133 of {\em Studies in
  Logic and the Foundations of Mathematics}.
\newblock Elsevier Science, Amsterdam, 1994.

\bibitem{nor:pet:smi:90}
Bengt Nordstr{\"o}m, Kent Petersson, and Jan~M. Smith.
\newblock {\em {Programming in Martin-L\"of's Type Theory, An Introduction}}.
\newblock Oxford University Press, 1990. \\
\newblock \href{http://www.cs.chalmers.se/Cs/Research/Logic/book/book.ps}
{\texttt{http://www.cs.chalmers.se/Cs/Research/Logic/book/book.ps}}

\bibitem{oos:geu:02}
M. Oostdijk and H. Geuvers, Proof by Computation in the Coq system,
{\em Theoretical Computer Science\/} 272 (1-2), 2001, pp. 293--314.

\bibitem{pfe:sch:99}
Frank Pfenning and Carsten Sch\"urmann. System description: Twelf -- a meta-logical framework for deductive systems,
in {\em Proceedings of the 16th International Conference on Automated Deduction\/} (CADE-16), ed. H. Ganzinger, LNAI 1632, 1999, pp. 202--206.

\bibitem{coq:02}
{The Coq Development Team}.
\newblock {\em The Coq Proof Assistant Reference Manual}, 2002. \\
\newblock
  \href{ftp://ftp.inria.fr/INRIA/coq/current/doc/Reference-Manual-all.ps.gz}
  {\texttt{ftp://ftp.inria.fr/INRIA/coq/current/doc/Reference-Manual-all.ps.gz}\toolong}

\end{thebibliography}

\end{document}
