Nathaniel pushed to branch bosn at Stefan / Typer

Commits: 54fcd9b8 by nbos at 2018-08-06T23:33:22Z Add labels and refs to figures in text

- - - - - cd8d5f59 by nbos at 2018-08-07T09:09:37Z Add labels and refs to equations; add (Prop, Prop, Prop) axiom to Rcc; define translation on applications; prove (most of) lemma 3.6

- - - - -

1 changed file:

- doc/formal/typer_theory.tex

Changes:

===================================== doc/formal/typer_theory.tex ===================================== @@ -98,7 +98,7 @@ After elaboration, implicit terms behave exactly like explicit terms so we will (M \ap N)^* &= M^*\ap N^* & (M \appp N)^* &= M^* \end{align*}

-The typing rules for explicit and erasable terms are shown in Figure X. They are the standard rules of a Church-style lambda calculus, duplicated for both kinds of terms. +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{ @@ -147,7 +147,8 @@ The typing rules for explicit and erasable terms are shown in Figure X. They are \ \end{mathpar} } - \caption{Typer's Typing Judgement Rules} + \caption{Typer's Typing Judgment Rules} + \label{fig:X-E-rules} \end{figure}

@@ -181,7 +182,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 X. +The typing rules for inductive definitions and case analysis are presented in Figure \ref{IND-rules}.

\begin{figure}[h] \ \ \ \ \fbox{ @@ -251,6 +252,7 @@ The typing rules for inductive definitions and case analysis are presented in Fi \end{mathpar} } \caption{Typer's Inductive and Case Typing Rules} + \label{fig:IND-rules} \end{figure}

\subsection{Fixpoint Operator} @@ -310,7 +312,7 @@ Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $ \caption{Typer's Conversion Rules} \end{figure}

-\section{Typer as an Extention of a Calculus of Constructions} +\section{Typer as an Extension of a Calculus of Constructions} In this section we will prove that the erasable terms of Typer allow for a representation of all typing derivations from a Calculus of Constructions with an impredicative $\mathsf{Prop}$ and an infinite hierarchy of predicative universes (\CC).

\subsection{Definition of \CC} @@ -321,12 +323,14 @@ In this section we will prove that the erasable terms of Typer allow for a repre \S_{CC} = { & \Prop; \Type_i} &\forall i > 0 \[9pt] \A_{CC} = { &(\Prop : \Type_1); \ &(\Type_i : \Type_{i+1})} &\forall i > 0 \[9pt] - \R_{CC} = { &(\Prop, \Type_i, \Type_i) &\forall i > 0 \ + \R_{CC} = { &(\Prop, \Prop, \Prop) \ + &(\Prop, \Type_i, \Type_i) &\forall i > 0 \ &(\Type_i, \Prop, \Prop); &\forall i > 0 \ &(\Type_i,\Type_j,(\Type_i\cup\Type_j)); &\forall i > 0 \ \end{empheq} \vspace{-5mm} \caption{\CC's Pure Type System} + \label{fig:CC-pts} \end{figure}

\begin{figure}[h] @@ -371,11 +375,12 @@ In this section we will prove that the erasable terms of Typer allow for a repre \end{mathpar} } \caption{\CC's Typing Rules} + \label{fig:CC-rules} \end{figure}

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 X. The typing rules for \CC\ are shown in Figure X. The structure of the PTS is derived from Luo's own extention of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\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, for example, Miquel's definition of \CC\ \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: @@ -396,15 +401,17 @@ We introduce a translator operator \rew{\ } defined on contexts and terms of \CC \end{cases}\ \rew{M \ap N} &= \begin{cases} - \rew{M}|||\rew{N} \todo \ - \rew{M}|\rew{N} \todo + \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 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: \begin{align} + \label{eq:iff-context} \Ga \CCdash & ~~ \iff ~~ \rew{\Ga} ~ \ + \label{eq:iff-judgment} \Ga \CCdash e:\tau & ~~ \iff ~~ \rew{\Ga} ~ \rew{e}:\rew{\tau} \end{align}

@@ -415,12 +422,12 @@ Before proceeding with the proof, 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$ \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 injectie 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$. 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 disctinct 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$ + 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$ \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 \begin{align*} @@ -430,30 +437,6 @@ Before proceeding with the proof, we will show the following lemmas: 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$ \end{proof} \end{lemma} -% Finally, rules in $\R_{CC}$ translate to rules either in $\R$ or $\R_e$, depending on whether they are predicative or impredicative. For example, consider the translation of the predicative rule -% \begin{align*} -% \rew{(\Prop,\Type_1,\Type_1)} &= (\rew{\Prop},\rew{\Type_1},\rew{\Type_1}) \ -% &= (\Type\ \z,\Type\ (\s\ \z),\Type\ (\s\ \z)) \in \R -% \end{align*} - -% and conversly, the translation of the impredicative rule -% \begin{align*} -% \rew{(\Type_1,\Prop,\Prop)} &= (\rew{\Type_1},\rew{\Prop},\rew{\Prop}) \ -% &= (\Type\ (\s\ \z),\Type\ \z,\Type\ \z) \in \R_e. -% \end{align*} -% In general, if a product type of \CC\ has a domain of higher sort than its codomain, i.e. it is impredicative, then it can only be of form $(\Type_i,\Prop,\Prop)$ (see Figure 7). In all other cases, i.e. the predicative rules $(\Prop, \Type_i, \Type_i)$ and $(\Type_i, \Type_j, (\Type_i \cup \Type_j))$, the sort of the product type will be $s_3 = (s_1 \cup s_2)$. - -% Thus, the translation of set theoric propositions is the following: -% \begin{align*} -% \rew{s \in \S_{CC}} &\leadsto\ \rew{s} \in \S \ -% \rew{(s_1:s_2) \in \A_{CC}} &\leadsto\ (\rew{s_1}:\rew{s_2}) \in \A \ -% \rew{(s_1,s_2,s_3) \in \R_{CC}} &\leadsto\ -% \begin{cases} -% (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e &\text{if $s_1 \neq \Prop$}\[-4pt] -% & \text{and $s_2 = \Prop$}\ -% (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R &\text{otherwise} -% \end{cases} -% \end{align*}

We define the translation on context recursively: \begin{align*} @@ -461,7 +444,7 @@ We define the translation on context recursively: \rew{\Ga, x:e} &= \rew{\Ga}, x:\rew{e} \end{align*}

-We now proceed by case analysis on typing derivation steps to show that (1) and (2) hold: +We now proceed by case analysis on typing derivation steps to show that equations \ref{eq:iff-context} and \ref{eq:iff-judgment} hold:

\underline{\textbf{CC-Wf-E:}} \begin{mathpar} @@ -502,7 +485,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 varaibles. 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 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. \end{proof} \end{lemma} \begin{lemma} @@ -598,7 +581,7 @@ We have the assumptions \end{mathpar} and we know that $$(\Type_i,\Prop,\Prop) \in \R_{CC} \iff (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e$$ -from which we can conlcude +from which we can conclude \begin{mathpar} \infer {\rew{\Ga} ~ \rew{T}:\rew{\Type_i} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{\Prop} \ (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e} @@ -674,19 +657,36 @@ but we have yet to show that the additional premise $x \notin \fv{\rew{M}^*}$ of $$x \notin \fv{\rew{M}^*}$$ \end{lemma}

-\begin{proof} - \todo - % Because we have a well typed erasable product type which can only be constructed by means of rule \textsc{E-Prod}, we can assume under the induction hypothesis that $T:\Type_i$ and that $U:\Prop$. With those additional assumptions, we will show that $x \notin \fv{\rew{M}^*}$ by case analysis on $\rew{M}$. - % \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{proof} - - +\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}$: + + \underline{\textbf{Case}} $\rew{M} = 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$:\ + $\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$:\ + 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)\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} = 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 \appp Q$:\ + The extraction is $(P \appp Q)^* = P^*$. This expands to $(\la (\iota:t) \erasable V)^*$ \todo + \end{proof}

+ + \subsection{Example}

\newpage

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