Nathaniel pushed to branch bosn at Stefan / Typer

Commits: 7f3a4233 by nbos at 2018-08-08T07:49:41Z Finish proof of lemma 3.6; make it a case analysis on [M]* rather than [M]; make M -> M* definition a figure

- - - - - 58024bcd by nbos at 2018-08-08T10:40:51Z Enhance layout of translation section; define soundness/completeness of translation; label lemmas; clean A-equiv lemma; add R-equiv lemma; complete completeness (=>) proof

- - - - -

1 changed file:

- doc/formal/typer_theory.tex

Changes:

===================================== doc/formal/typer_theory.tex ===================================== @@ -90,15 +90,21 @@ Typer manipulates three separate kinds of terms to simplify both the writing and \end{tabular} \end{center}

-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}) that erases domains of abstraction, erasable abstractions and erasable applications. It also turns erasable products into a propositional form: -\begin{align*} +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{align*} - -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. + (M \ap N)^* &= M^*\ap N^* & (M \appp N)^* &= M^*\ + \end{empheq} + \vspace{-5mm} +\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.

\begin{figure}[h] \ \ \ \ \fbox{ @@ -182,7 +188,7 @@ We extend our abstract syntax with four terms introduced in \cite{gimenez} to ex \item $\Case\ M: S \text{ of } <\vec{G}>$ which is the function by case analysis on the expression $M$ of type $S$ and where $<\vec{G}>$ is the list of cases, represented as abstractions of the respective patterns of constructions. \end{itemize}

-The typing rules for inductive definitions and case analysis are presented in Figure \ref{IND-rules}. +The typing rules for inductive definitions and case analysis are presented in figure \ref{IND-rules}.

\begin{figure}[h] \ \ \ \ \fbox{ @@ -380,7 +386,7 @@ In this section we will prove that the erasable terms of Typer allow for a repre

Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, but with an added infinite hierarchy of universes above an impredicative \Prop. They are arranged in the series: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4 : ...$$

-\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}). +\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: @@ -406,8 +412,26 @@ We introduce a translator operator \rew{\ } defined on contexts and terms of \CC \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 valid if for each valid context and typing judgment of \CC, we get a valid contexts and typing judgments in Typer and vice versa: +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} ~ \ @@ -415,36 +439,59 @@ We will consider this translation valid if for each valid context and typing jud \Ga \CCdash e:\tau & ~~ \iff ~~ \rew{\Ga} ~ \rew{e}:\rew{\tau} \end{align}

-We will proceed by induction on typing derivation to show that each valid derivation of \CC\ translates to a valid derivation in the Typer system ($\Rightarrow$). For most typing rules, the proof is straightforward: we assume the translated premises by the induction hypothesis and then show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules. - -Before proceeding with the proof, we will show the following lemmas: +Before proceeding with the proofs, we will show the following lemmas:

\begin{lemma} - Each sort $s \in \S_{CC}$ of \CC\ has an distinct equivalent sort $\rew{s} \in \S$ in Typer; i.e. $s \in \S_{CC} \iff \rew{s} \in \S$ + \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$ \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}$ \end{proof} \end{lemma}

\begin{lemma} - Every axiom $(s_1:s_2) \in \A_{CC}$ of \CC\ has a distinct 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$ + \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$ \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 all $i$, we have + 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 \begin{align*} - (\rew{\Type_i}:\rew{\Type_{i+1}}) &= (\Type\ (\s^i\ \z):\Type\ (\s^{i+1}\ \z))\ - &= (\Type\ (\s^i\ \z):\Type\ (\s\ (\s^i\ \z)) + (\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} \end{align*} -which corresponds to the axiom scheme $(\Type\ \l:\Type\ \s\ \l) ~ \forall \l\in\mathbb{L}$ considering that $(\s^i\ \z) \in \mathbb{L} ~ \forall i>0$ + %%% + % 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}})$. \end{proof} \end{lemma}

-We define the translation on context recursively: -\begin{align*} - \rew{\cdot} &= \cdot \ - \rew{\Ga, x:e} &= \rew{\Ga}, x:\rew{e} -\end{align*} - -We now proceed by case analysis on typing derivation steps to show that equations \ref{eq:iff-context} and \ref{eq:iff-judgment} hold: +\begin{lemma} + \label{lem:R-equiv} + Each rule $(\Type_i,\Prop,\Prop) \in \R_{CC}$ has a distinct and equivalent rule $(\rew{\Type_i},\rew{Prop},\rew{Prop}) \in R_e$ and each other rule $(s_1,s_2,s_3) \in \R_{CC}$ has a distinct and equivalent rule $(\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$; i.e. + \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$} + \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} + \end{align*} + For $(\Prop, \Prop, \Prop)$, we have \todo + \end{proof} +\end{lemma} +\subsection{Completeness of translation} +We will proceed by structural induction on typing derivation to show that each valid derivation of \CC\ translates to a valid derivation in the Typer system ($\Rightarrow$). For most typing rules, the proof is straightforward: we assume the translated premises by the induction hypothesis and then show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules.

\underline{\textbf{CC-Wf-E:}} \begin{mathpar} @@ -482,6 +529,7 @@ We have yet to show that $$x \notin \dv{\rew{\Ga}}$$

\begin{lemma} + \label{lem:DV-equiv} We have the following equality: $$\dv{\Ga} = \dv{\rew{\Ga}}$$ \begin{proof} @@ -489,10 +537,11 @@ $$x \notin \dv{\rew{\Ga}}$$ \end{proof} \end{lemma} \begin{lemma} + \label{lem:not-DV-equiv} The following holds: $$x \notin \dv{\Ga} \iff x \notin \dv{\rew{\Ga}}$$ \begin{proof} - Follows directly from the previous lemma. + Follows directly from lemma \ref{lem:DV-equiv}. \end{proof} \end{lemma} We can now infer the translation of the conclusion by rule @@ -538,7 +587,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 3.3, 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 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. \end{proof} \end{lemma}

@@ -639,16 +688,10 @@ The predicative product type translates to an explicit product type $(x:\rew{T}) \tag{X-Lam} \end{mathpar} \textbf{Impredicative subcase:}\ -The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ which necessarily has sort \Prop. We would expect to apply the erasable \textsc{E-Lam} typing rule to derive the typing of the erasable lambda abstraction, -\begin{mathpar} - \infer - {\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U} \ \rew{\Ga} ~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop} \ x \notin \fv{\rew{M}^*}} - {\rew{\Ga} ~ \la(x:\rew{T}) \erasable \rew{M} : (x:\rew{T}) \erasable \rew{U}} - \tag{E-Lam} -\end{mathpar} -but we have yet to show that the additional premise $x \notin \fv{\rew{M}^*}$ of rule \textsc{E-Lam} holds in all cases. +The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ which necessarily has sort \Prop. We would expect to apply the erasable \textsc{E-Lam} typing rule to derive the typing of the erasable lambda abstraction, but we have yet to show that the additional premise $x \notin \fv{\rew{M}^*}$ of rule \textsc{E-Lam} holds in all cases. Thus, the following lemma:

\begin{lemma} + \label{lem:E-Lam-FV} If $$\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U}$$ and @@ -658,35 +701,49 @@ but we have yet to show that the additional premise $x \notin \fv{\rew{M}^*}$ of \end{lemma}

\begin{proof}\ \ - By structural induction, for every term of our calculus, we either show that $\rew{M}$ cannot be equal to it, or that $x$ cannot be free in its extraction, thus showing that $x \notin \fv{\rew{M}^*}$. First, we show how some terms cannot be $\rew{M}$: + 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}^*$:

- \underline{\textbf{Case}} $\rew{M} = x$:\ + \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.

- \underline{\textbf{Case}} $\rew{M} = (x:t)\explicit V$ or $(x:t)\erasable V$:\ + \underline{\textbf{Case}} $\rew{M}^* = ((x:t)\explicit V)^*$ or $((x:t)\erasable V)^*$:\ $\rew{M}$ cannot be a product type since it inhabits the type $\rew{U} : \rew{\Prop}$. Since $\rew{\Prop} = \Type\ \z$ is our smallest universe, we cannot have a type two levels down.

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$:\ + \underline{\textbf{Case}} $\rew{M}^* = (s)^*$ with $s \in \S$:\ The extraction is $s^* = s$. We know that $x$ cannot appear free in a sort.

- \underline{\textbf{Case}} $\rew{M} = \la(x:t)\explicit V$:\ - The extraction is $(\la(x:t)\explicit V)^* = \la(x)\explicit V^*$. The variable $x$ is not free in the expression because it is bound. + \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.

- \underline{\textbf{Case}} $\rew{M} = \la(x:t)\erasable V$:\ - The extraction is $(\la(x:t)\erasable V)^* = V^*$. By the induction hypothesis, we can assume that $x \notin \fv{V}$ holds true for the construction of the erasable abstraction (see rule \textsc{E-Lam}). + \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^*$. This can only expand to $(\la (\iota:t) \explicit V)^* | (\iota)^*$ \todo + \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^*$.

- - \underline{\textbf{Case}} $\rew{M} = P \appp Q$:\ - The extraction is $(P \appp Q)^* = P^*$. This expands to $(\la (\iota:t) \erasable V)^*$ \todo + \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. \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: +\begin{mathpar} + \infer + {\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U} \ \rew{\Ga} ~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop} \ x \notin \fv{\rew{M}^*}} + {\rew{\Ga} ~ \la(x:\rew{T}) \erasable \rew{M} : (x:\rew{T}) \erasable \rew{U}} + \tag{E-Lam} +\end{mathpar} + +\subsection{Soundness of translation} + + \subsection{Example}

\newpage

View it on GitLab: https://gitlab.com/monnier/typer/compare/cd8d5f59acd0366c123a90e3a7a0122171d...