\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}