Skip to content
Commits on Source (3)
Hide whitespace changes
Inline Side-by-side
doc/formal/typer_theory.tex
View file @ d5a33c33
......@@ -93,16 +93,17 @@ Typer manipulates three separate kinds of terms to simplify both the writing and
After elaboration, implicit terms behave exactly like explicit terms so we will not explicitly include them in our calculus; they will be assumed to be a subset of the explicit terms. We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure \ref{fig:*}. It erases domains of abstraction, erasable abstractions and erasable applications and turns erasable products into a propositional form.
\begin{figure}[h]
\centering
\begin{empheq}[box=\fbox]{align*}
\hspace{20mm} & \ & \ & \hspace{7mm} \\
s^* &= s & x^* &= x \\[5pt]
(\la(x:T)\explicit U)^* &= \la(x)\explicit U^* & ((x:T)\explicit U)^* &= (x:T^*)\explicit U^* \\
(\la(x:T)\erasable U)^* &= U^* & ((x:T)\erasable U)^* &= \forall(x:T^*).U^* \\[5pt]
(M \ap N)^* &= M^*\ap N^* & (M \appp N)^* &= M^*\\
\end{empheq}
\vspace{-5mm}
\caption{Extraction function $M \mapsto M^*$}
\label{fig:*}
\fbox{\begin{minipage}{0.9\linewidth}
\begin{align*}
s^* &= s & x^* &= x \\[5pt]
(\la(x:T)\explicit U)^* &= \la(x)\explicit U^* & ((x:T)\explicit U)^* &= (x:T^*)\explicit U^* \\
(\la(x:T)\erasable U)^* &= U^* & ((x:T)\erasable U)^* &= \forall(x:T^*).U^* \\[5pt]
(M \ap N)^* &= M^*\ap N^* & (M \appp N)^* &= M^*\\
\end{align*}
\end{minipage}}
\caption{Extraction function $M \mapsto M^*$}
\label{fig:*}
\end{figure}
The typing rules for explicit and erasable terms are shown in figure \ref{fig:X-E-rules}. They are the standard rules of a Church-style lambda calculus, duplicated for both kinds of terms.
......@@ -389,49 +390,37 @@ Our definition of \CC\ is based on the original Calculus of Constructions (CC) \
\CC's PTS definition is shown in figure \ref{fig:CC-pts}. The typing rules for \CC\ are shown in figure \ref{fig:CC-rules}. The structure of the PTS is derived from Luo's own extension of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop, \Prop, \Prop)$, $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, (\Type_i\cup\Type_j))$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). Our definition of \CC\ will therefore behave differently than other definitions of \CC\ (see for example \cite{miquel}).
\subsection{Translation}
We introduce a translator operator \rew{\ } defined on contexts and terms of \CC:
\begin{align*}
\rew{\cdot} &= \cdot & \rew{\Prop} &= \Type\ \z \\
\rew{\Ga,x:T} &= \rew{\Ga},x:\rew{T} & \rew{\Type_{i}} &= \Type\ (\s^{i}\ \z) \\[-20pt]
\end{align*}
\begin{align*}
\rew{\la(x:T)\explicit U} &=
\begin{cases}
\la(x : \rew{T}) \erasable \rew{U} &\text{if $(U:\tau)$, $(\tau : \Prop)$ and $(T:\Type_i)$}\\
\la(x : \rew{T}) \explicit \rew{U} &\text{otherwise}
\end{cases}\\
\rew{(x:T)\explicit U} &=
\begin{cases}
(x : \rew{T})\erasable \rew{U} &\text{if $(U: \Prop)$ and $(T:\Type_i)$}\\
(x : \rew{T})\explicit \rew{U} &\text{otherwise}
\end{cases}\\
\rew{M \ap N} &=
\begin{cases}
\rew{M}|||\rew{N} &\text{if $(M:\tau:\Prop)$ and $(T:\tau':\Type_i)$} \\
\rew{M}|\rew{N} &\text{otherwise}
\end{cases}\\
\end{align*}
We define the translation on context recursively:
\begin{align*}
\rew{\cdot} &= \cdot \\
\rew{\Ga, x:e} &= \rew{\Ga}, x:\rew{e}
\end{align*}
%%%
% I'm tentatively calling the two directions soundness and completness
% inspired by the following definition. The article also states that
% sometimes the terms are interchanged in the literature:
% "The correctness of the translation is expressed by two properties:
% completeness and soundness. The first states that all the generated
% terms have the correct type. For example, the translation of a term
% of type A has type [A] while the translation of a proof of φ has
% type [φ]. The second states that if a proof term is well-typed in
% Dedukti, then the proof is correct in the original logic."
% src: https://arxiv.org/pdf/1507.08720.pdf
We will consider this translation correct if it is both complete and sound as per the following definitions. \emph{Completeness} of the translation ($\Rightarrow$) is established if every translated expression of \CC\ inhabits its translated type in the Typer system. \emph{Soundness} of the translation ($\Leftarrow$) is established if every valid typing derivation of translated terms in the Typer system implies a valid typing derivation in \CC:
\begin{figure}[h]
\fbox{
\begin{minipage}{1.0\linewidth}
\begin{align*}
\rew{\cdot} &= \cdot & \rew{\Prop} &= \Type\ \z \\
\rew{\Ga,x:T} &= \rew{\Ga},x:\rew{T} & \rew{\Type_{i}} &= \Type\ (\s^{i}\ \z) \\[-20pt]
\end{align*}
\begin{align*}
\rew{\la(x:T)\explicit U} &=
\begin{cases}
\la(x : \rew{T}) \erasable \rew{U} &\text{if $(U:\tau)$, $(\tau : \Prop)$ and $(T:\Type_i)$}\\
\la(x : \rew{T}) \explicit \rew{U} &\text{otherwise}
\end{cases}\\
\rew{(x:T)\explicit U} &=
\begin{cases}
(x : \rew{T})\erasable \rew{U} &\text{if $(U: \Prop)$ and $(T:\Type_i)$}\\
(x : \rew{T})\explicit \rew{U} &\text{otherwise}
\end{cases}\\
\rew{M \ap N} &=
\begin{cases}
\rew{M}|||\rew{N} &\text{if $(M:\tau:\Prop)$ and $(T:\tau':\Type_i)$} \\
\rew{M}|\rew{N} &\text{otherwise}
\end{cases}\\
\end{align*}
\end{minipage}
}
\caption{Definition of the translation}
\label{fig:[]}
\end{figure}
The translator operator \rew{\ } is defined on contexts and terms of \CC. We expose the translation on figure \ref{fig:[]}. We will consider this translation correct if it is both complete and sound as per the following definitions. \emph{Completeness} of the translation ($\Rightarrow$) is established if every translated expression of \CC\ inhabits its translated type in the Typer system. \emph{Soundness} of the translation ($\Leftarrow$) is established if every valid typing derivation of translated terms in the Typer system implies a valid typing derivation in \CC:
\begin{align}
\label{eq:iff-context}
\Ga \CCdash & ~~ \iff ~~ \rew{\Ga} \~ \\
......@@ -440,34 +429,32 @@ We will consider this translation correct if it is both complete and sound as pe
\end{align}
Before proceeding with the proofs, we will show the following lemmas:
\begin{lemma}
\label{lem:S-equiv}
Each sort $s \in \S_{CC}$ of \CC\ has an distinct and equivalent sort $\rew{s} \in \S$ in Typer; i.e. $s \in \S_{CC} \iff \rew{s} \in \S$
$s \in \S_{CC} \iff \rew{s} \in \S$
\begin{proof}
For \Prop, we know that $\rew{\Prop} = \Type\ \z$ with $\Type\ \z \in \S$. For \Type$_i$, we know that for all $i$ we have $\rew{\Type_i} = \Type\ (\s^i\ \z)$ with $\Type\ (\s^i\ \z) \in \S ~ \forall i > 0$. This translation is an injective function, so we also have a unique $s$ for every $\rew{s}$
For \Prop, we know that $\rew{\Prop} = \Type\ \z$ with $\Type\ \z \in \S$. For \Type$_i$, we know that for all $i$ we have $\rew{\Type_i} = \Type\ (\s^i\ \z)$ with $\Type\ (\s^i\ \z) \in \S ~ \forall i > 0$.
%% FIXME: Being injective is not sufficient.
%% If we defined [Typeω] = Typeω, it would still be injective, and Typeω
%% is in \S, yet Typeω is not in \S_CC so the reverse implication
%% wouldn't hold.
%% FIXME: But [] is only defined on terms of S_{CC} so if there
%% exists a '[s]', then there necessarily exists a 's'
Because the translation on sorts is defined on $S_{CC}$, it follows that if $\rew{s} \in S$, then $s \in S_{CC}$.
\end{proof}
\end{lemma}
\begin{lemma}
\label{lem:A-equiv}
Each axiom $(s_1:s_2) \in \A_{CC}$ of \CC\ has a distinct and equivalent axiom $(\rew{s_1}:\rew{s_2}) \in \A$ in Typer; i.e. $(s_1:s_2) \in \A_{CC} \iff (\rew{s_1}:\rew{s_2}) \in \A$
$(s_1:s_2) \in \A_{CC} \iff (\rew{s_1}:\rew{s_2}) \in \A$
\begin{proof}
For $(\Prop\:\Type_1)$, we know that $(\rew{\Prop}\:\rew{\Type_1}) = (\Type\ \z\:\Type\ (\s\ \z))$ with $(\Type\ \z\:\Type\ (\s\ \z)) \in A$. For $(\Type_i\:\Type_{i+1})$, we know that
For $(\Prop\:\Type_1)$, we know that $$(\rew{\Prop}:\rew{\Type_1}) = (\Type\ \z:\Type\ (\s\ \z)) \in A$$ For $(\Type_i\:\Type_{i+1})$, we know that
\begin{align*}
(\rew{\Type_i}:\rew{\Type_{i+1}}) &= (\Type\ (\s^i\ \z):\Type\ (\s^{i+1}\ \z)) &&\forall\ i>0\\
&= (\Type\ (\s^i\ \z):\Type\ (\s\ (\s^i\ \z)) &&\forall\ i>0\\
&= (\Type\ \l:\Type\ (\s\ \l)) &\in \A \quad &\forall\ \l \in \mathbb{L} \backslash \{\z\}
&= (\Type\ \l:\Type\ (\s\ \l)) &\in \A \quad &\forall\ \l \in \mathbb{L} \backslash \{\z\}
\end{align*}
%%%
% Do we write "\S \mapsto \S" or "s \mapsto s"? i.e. maps between
% sets or between variables covering the elements of the set?
% Usually we can use the arrow "\S \to \S", for functions between
% types but I don't want to cause confusion vs. explicit
% abstractions/types.
Since the mapping of $\S_{CC} \mapsto \rew{\S_{CC}}$ is injective
by lemma \ref{lem:S-equiv}, we can conclude that so is the mapping
$(\S_{CC}:\S_{CC}) \mapsto (\rew{\S_{CC}}:\rew{\S_{CC}})$.
Because the translation on sorts is defined on $S_{CC} = \{\Prop; \Type_i\}\ \forall i > 0$, the axioms of the form $(\rew{s_1}:\rew{s_2}) \in \A$ are $(\rew{\Prop}\:\rew{\Type_1})$ for which we have $$(\Prop\:\Type_1) \in \A_{CC}$$ and $(\rew{\Type_i}:\rew{\Type_{i+1}}) \forall i > 0$ for which we have $$(\Type_i:\Type_{i+1}) \in A_{CC} \quad \forall i > 0$$
\end{proof}
\end{lemma}
......@@ -477,15 +464,15 @@ Before proceeding with the proofs, we will show the following lemmas:
\begin{align*}
(\Type_i,\Prop,\Prop) \in \R_{CC} &\iff (\rew{\Type_i},\rew{Prop},\rew{Prop}) \in R_e\\
(s_1,s_2,s_3) \in \R_{CC} &\iff (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R &\text{if $s_1 \neq \Type_i$} \\[-5pt]
& &\text{or $s_2 \neq \Prop$}
& &\text{or $s_2 \neq \Prop$}
\end{align*}
\begin{proof}
For $(\Type_i,\Prop,\Prop) \in \R_{CC}$, we have
\begin{align*}
(\rew{\Type_i},\rew{Prop},\rew{Prop}) &= (\Type\ (\s^i\ \z),\Type\
\z, \Type\ \z) &&\forall\ i > 0\\
&= (\Type\ \l,\Type\
\z, \Type\ \z) & \in \R_e \quad &\forall\ \l \in \mathbb{L} \backslash \{\z\}
(\rew{\Type_i},\rew{Prop},\rew{Prop}) &= (\Type\ (\s^i\ \z),\Type\
\z, \Type\ \z) &&\forall\ i > 0\\
&= (\Type\ \l,\Type\
\z, \Type\ \z) & \in \R_e \quad &\forall\ \l \in \mathbb{L} \backslash \{\z\}
\end{align*}
For $(\Prop, \Prop, \Prop)$, we have \todo
\end{proof}
......@@ -505,10 +492,6 @@ The translation is immediately true under Typer by rule \textsc{Wf-E}.
\infer
{\ }
{\rew{\cdot} \~}
~~~ \leadsto ~~~
\infer
{\ }
{\cdot \~}
\tag{Wf-E}
\end{mathpar}
......@@ -533,7 +516,7 @@ $$x \notin \dv{\rew{\Ga}}$$
We have the following equality:
$$\dv{\Ga} = \dv{\rew{\Ga}}$$
\begin{proof}
By induction on the size of the context. The equality holds on the base case $\rew{\cdot} = \cdot$ since both the empty context and its translation have no declared variables. The equality holds on the recursive case $\rew{\Ga, x \: T} = \rew{\Ga}, x \: \rew{T}$ since the name of the declared variable is left unchanged.
By structural induction on $\Ga$. The equality holds on the base case $\rew{\cdot} = \cdot$ since both the empty context and its translation have no declared variables. The equality holds on the recursive case $\rew{\Ga, x \: T} = \rew{\Ga}, x \: \rew{T}$ since the name of the declared variable is left unchanged.
\end{proof}
\end{lemma}
\begin{lemma}
......@@ -587,7 +570,7 @@ $$\rew{\Ga} \~$$
The following holds:
$$(x:T) \in \Ga \iff (x:\rew{T}) \in \rew{\Ga}$$
\begin{proof}
By induction on the size of the context. The base case makes the proposition false on both sides. By lemma \ref{lem:DV-equiv}, the set of declared variables in a \CC\ context and in its translation are the same, so we must only show that they both have the appropriate types. It follows from the recursive definition of translation on contexts $\rew{\Ga, x \: T} = \rew{\Ga}, x \: \rew{T}$ that they do.
By structural induction on $\Ga$. The base case makes the proposition false on both sides. By lemma \ref{lem:DV-equiv}, the set of declared variables in a \CC\ context and in its translation are the same, so we must only show that they both have the appropriate types. It follows from the recursive definition of translation on contexts $\rew{\Ga, x \: T} = \rew{\Ga}, x \: \rew{T}$ that they do.
\end{proof}
\end{lemma}
......@@ -614,6 +597,7 @@ We have the assumptions
{\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{s_2}}
\end{mathpar}
and we know that
%% FIXME: This is only true if s1 != Type_i or s2 != Prop !!!
$$(s_1,s_2,s_3) \in \R_{CC} \iff (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$$
from which we can conclude
\begin{mathpar}
......@@ -703,6 +687,13 @@ The impredicative product type translates to an erasable product type $(x:\rew{T
\begin{proof}\ \\
By structural induction, for every term of the codomain of the extraction function (see figure \ref{fig:*}), we either show that $\rew{M}^*$ cannot be equal to it, or that $x$ cannot be free in it, thus showing that $x \notin \fv{\rew{M}^*}$. First, we show how some terms cannot be $\rew{M}^*$:
%% FIXME: This should be `y` (since it can be any variable, not only the
%% variable `x` that we're trying to prove isn't ∈ FV(M*).
%% FIXME: It's not? The rule is about making an abstraction of 'x', so
%% why do we care for 'y'? I understand that we could have a case with
%% a variable that is not 'x' (and the same for the cases where [M]* is
%% a function) but they are trivial like the case for 's'. Should we still
%% mention them?
\underline{\textbf{Case}} $\rew{M}^* = x^* = x$:\\
This is impossible because we know that $x : \rew{T}$ and since $$(x:\rew{T})\erasable\rew{U} : \Prop$$ then, under the only possible construction of an erasable product type, we know that $\rew{T} : \rew{\Type_i}$ and $\rew{U} : \rew{\Prop}$. Because $\rew{T}$ and $\rew{U}$ inhabit different universes, their inhabitants $x : \rew{T}$ and $\rew{M} : \rew{U}$ cannot be equal.
......@@ -712,25 +703,34 @@ The impredicative product type translates to an erasable product type $(x:\rew{T
Now for the cases where we can prove that $x$ is not free in the extraction of $\rew{M}$:
\underline{\textbf{Case}} $\rew{M}^* = (s)^*$ with $s \in \S$:\\
%% FIXME: More specifically, the sorts `s` are (closed) constants.
%% FIXME: This shows a problem in our presentation. We use FV(M*) and we
%% define * but we don't define FV. Another option is to forget about *
%% and only define FV*(M), the set of non-erasable free variables.
The extraction is $s^* = s$. We know that $x$ cannot appear free in a sort.
%% FIXME: Please don't re-use `x` it's just confusing!
\underline{\textbf{Case}} $\rew{M}^* = (\la(x:t)\explicit V)^*$:\\
The extraction makes this $\la(x)\explicit V^*$. The variable $x$ is not free in the expression because it is bound. Further, $x$ is not free in $V^*$ by the induction hypothesis.
%% FIXME: Please don't re-use `x` it's just confusing!
\underline{\textbf{Case}} $\rew{M}^* = (\la(x:t)\erasable V)^*$:\\
The extraction makes this $V^*$. By the induction hypothesis, $x$ is not free in $V^*$.
%%%
% I think we could use either induction hypotheses here, i.e. the
% one of our lemma that the abstracted variable does not appear in
% the body of the erasable abstraction, and the one of our current
% induction on extracted terms. I'm going with the second one as I
% did in the previous case.
\underline{\textbf{Case}} $\rew{M}^* = (P \ap Q)^*$:\\
The extraction is $(P \ap Q)^* = P^* \ap Q^*$. $P$ can only expand to an abstraction such that $P^* \ap Q^* = (\la (x:t) \explicit V)^* | Q^*$. We have shown that $x$ is not free in the explicit abstraction. By the induction hypothesis, $x$ is not free in $Q^*$.
The extraction is $(P \ap Q)^* = P^* \ap Q^*$.
%% FIXME: $P$ can be something else than an abstraction (e.g. it can be
%% a simple variable). What we can know is that P : T : Prop, because we
%% know that it returns something in Prop, so we can
%% apply the induction hypothesis to it.
$P$ can only expand to an abstraction such that $P^* \ap Q^* = (\la (x:t) \explicit V)^* | Q^*$. We have shown that $x$ is not free in the explicit abstraction.
%% FIXME: We can only use the induction hypothesis if Q : T : Prop!
By the induction hypothesis, $x$ is not free in $Q^*$.
\underline{\textbf{Case}} $\rew{M}^* = (P \appp Q)^*$:\\
The extraction is $(P \appp Q)^* = P^*$. $P$ can only expands to an abstraction $(\la (\iota:t) \erasable V)^*$ and we have shown that $x$ is not free in the erasable abstraction.
The extraction is $(P \appp Q)^* = P^*$.
%% FIXME: Again, $P$ can be something else than an abstraction.
$P$ can only expand to an abstraction $(\la (\iota:t) \erasable V)^*$ and we have shown that $x$ is not free in the erasable abstraction.
\end{proof}
Now we can appeal to lemma \ref{lem:E-Lam-FV} and we have the sufficient premises to apply rule \textsc{E-Lam} and we obtain the translation of the conclusion:
......