Nathaniel pushed to branch bosn at Stefan / Typer

Commits: 2eb3b210 by nbos at 2018-07-31T15:55:21Z Introduce translation operator; reduce number of assumptions in sec.3 and prove new lemmas instead

- - - - -

1 changed file:

- doc/formal/typer_theory.tex

Changes:

===================================== doc/formal/typer_theory.tex ===================================== @@ -163,14 +163,14 @@ There are two notable differences between explicit and erasable typing rules: \textbf{Notation:} We use a vector notation to refer to an arbitrary countable number of instances of some kind of term, i.e. $(X \vec{N})$ refers to the identifier $X$ followed by $N_1$, $N_2$, ..., $N_n$ for $n = |\vec{N}|$ where $|\vec{N}|$ is the size of the term vector $\vec{N}$. Similarly, $(\vec{x}:\vec{M})X$ refers to the term $(x_1:M_1)(x_2:M_2)...(x_n:M_n)X$ for $n = |\vec{x}| = |\vec{M}|$. We also write $i \in |\vec{N}|$ to refer to an $i$ member of the set ${1,2,3,...,n}$ for $n = |\vec{N}|$.

\begin{definition} -We say that $X$ is restricted to a \emph{strictly positive occurrence} in a term $P$ if $P \equiv (\vec{x}:\vec{M})(X \vec{N})$ where $X$ is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. + We say that $X$ is restricted to a \emph{strictly positive occurrence} in a term $P$ if $P \equiv (\vec{x}:\vec{M})(X \vec{N})$ where $X$ is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. \end{definition} \begin{definition} -We say that $C$ is a \emph{form of constructor} w.r.t. $X$ if it can be constructed with the following syntax: + We say that $C$ is a \emph{form of constructor} w.r.t. $X$ if it can be constructed with the following syntax:

-$$C ::= (X \vec{N}) ~~|~~ P\to C ~~|~~ (\vec{x}:\vec{M})C$$ + $$C ::= (X \vec{N}) ~~|~~ P\to C ~~|~~ (\vec{x}:\vec{M})C$$

-Where $X$ is restricted to strictly positive occurrences in the term $P$ and is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. + Where $X$ is restricted to strictly positive occurrences in the term $P$ and is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. \end{definition} We extend our abstract syntax with four terms introduced in \cite{gimenez} to express typing rules of inductive definitions. They are: \begin{itemize} @@ -266,20 +266,20 @@ Recursion is specified through the use of a recursive operator \Letrec \todo \end{mathpar}

\begin{definition} -A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to strictly positive occurrences, is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$. We abbreviate this property as $RP{i,C}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$. + A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to strictly positive occurrences, is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$. We abbreviate this property as $RP{i,C}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$. \end{definition} \begin{definition} -The \emph{guarded by destructors} condition is written as the predicate $\D_\V{f,k,x,M}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which represent the recursive components of $x$ in $M$. Below, we write $\D_\V{M}$ for brevity, but $f$, $k$ and $x$ remain bound to their presence in full predicate $\D_\V{f,k,x,M}$. We also write $\D_\V{\vec{M}}$ instead of $\bigwedge_i \D_\V{M_i}$. The condition $\D_\V{M} = \D_\V{f,k,x,M}$ is determined by structural induction on term $M$: -\begin{align*} - \D_\V{M} && = && \text{True} && \text{if } f \notin \fv{M}\ - \D_\V{\la (z:P)\to Q} && = && \D_\V{P} \land \D_\V{Q} \ - \D_\V{(z:P)\to Q} && = && \D_\V{P} \land \D_\V{Q} \ - \D_\V{\Letrec ?} && = && \ ? \ - \D_\V{\Ind(X:A)<\vec{C}>} && = && \D_\V{A} \land \D_\V{\vec{C}} \ - \D_\V{f \vec{P}} && = && (|\vec{P}| > k) \land (P_{k+1} \equiv (z\vec{Q}) \land \D_\V{\vec{P}} \ - \D_\V{\Case\ N:S \text{ of } <\vec{G}>} \todo\ - \D_\V{N \vec{P}} \todo\ -\end{align*} + The \emph{guarded by destructors} condition is written as the predicate $\D_\V{f,k,x,M}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which represent the recursive components of $x$ in $M$. Below, we write $\D_\V{M}$ for brevity, but $f$, $k$ and $x$ remain bound to their presence in full predicate $\D_\V{f,k,x,M}$. We also write $\D_\V{\vec{M}}$ instead of $\bigwedge_i \D_\V{M_i}$. The condition $\D_\V{M} = \D_\V{f,k,x,M}$ is determined by structural induction on term $M$: + \begin{align*} + \D_\V{M} && = && \text{True} && \text{if } f \notin \fv{M}\ + \D_\V{\la (z:P)\to Q} && = && \D_\V{P} \land \D_\V{Q} \ + \D_\V{(z:P)\to Q} && = && \D_\V{P} \land \D_\V{Q} \ + \D_\V{\Letrec ?} && = && \ ? \ + \D_\V{\Ind(X:A)<\vec{C}>} && = && \D_\V{A} \land \D_\V{\vec{C}} \ + \D_\V{f \vec{P}} && = && (|\vec{P}| > k) \land (P_{k+1} \equiv (z\vec{Q}) \land \D_\V{\vec{P}} \ + \D_\V{\Case\ N:S \text{ of } <\vec{G}>} \todo\ + \D_\V{N \vec{P}} \todo\ + \end{align*} \end{definition}

\subsection{Conversion Rules} @@ -376,10 +376,17 @@ 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 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}. + \subsection{Translation} +We introduce a translator operator \rew{\ } which is defined on all expressions of our syntax for \CC. We will consider a translation valid if for each context and each typing judgement of \CC, we have the following: +\begin{align} + \Ga \CCdash & ~~ \Rightarrow ~~ \rew{\Ga} ~ \ + \Ga \CCdash e:\tau & ~~ \Rightarrow ~~ \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. For most typing rules, the proof is straightforward: we assume the translated type theoric premises by the induction hypothesis and and the translated set theoric premises by an injective map from \CC's to Typer's PTS; we then show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules.

-We set up a correspondance between \CC's and Typer's PTS structures to allow for the translation of set theoric judgements found in typing rules. We first define the translation between universes $\rew{\ } : \S_{CC} \to \S$: +The correspondance between \CC's and Typer's PTS structures is first defined between the universe hierarchies $\rew{\ } : \S_{CC} \to \S$: \begin{align*} \rew{\Prop} ~~~ &= ~~~ \Type\ \mathsf{z} \ \rew{\Type_1} ~~~ &= ~~~ \Type\ \mathsf{(s\ z)} \ @@ -387,31 +394,31 @@ We set up a correspondance between \CC's and Typer's PTS structures to allow for \vdots~~~~~ ~~~ &= ~~~ ~~~~~~~\vdots \end{align*}

-Axioms of $\A_{CC}$ translate to axioms of $\A$ by the translation of respective sorts, e.g. $\rew{(\Prop : \Type_1)} = (\rew{\Prop} : \rew{\Type_1}) = (\Type\ \mathsf{z} : \Type\ \mathsf{(s\ z)})$. We note that the mapping of axioms is injective because $\A$ has an axiom scheme structurally identical to $\A_{CC}$'s. +Then, axioms of $\A_{CC}$ translate to axioms of $\A$ by the translation of respective sorts, e.g. $\rew{(\Prop : \Type_1)} = (\rew{\Prop} : \rew{\Type_1}) = (\Type\ \mathsf{z} : \Type\ \mathsf{(s\ z)})$. We note that the mapping of axioms is injective because $\A$ has an axiom scheme structurally identical to $\A_{CC}$'s.

-Finally, the translation of a rules in $\R_{CC}$ will 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 +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 + \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}) \ + \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 rule of \CC\ has a domain of higher sort than its range, i.e. it is impredicative, then it can only be of form $(\Type_i,\Prop,\Prop)$. 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 rule will be $s_3 = (s_1 \cup s_2)$. +In general, if a product type of \CC\ has a domain of higher sort than its range, 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} + \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: @@ -420,15 +427,6 @@ We define the translation on context recursively: \rew{\Ga, x:e} &\leadsto\ \rew{\Ga}, x:\rew{e} \end{align*}

-The translation on terms is the one which maintains the provability of translated judgements: -\begin{align} - \Ga \CCdash & ~~ \Rightarrow ~~ \rew{\Ga} ~ \ - \Ga \CCdash e:\tau & ~~ \Rightarrow ~~ \rew{\Ga} ~ \rew{e}:\rew{\tau} -\end{align} - -We proceed by induction on typing derivation to show that each valid derivation of \CC\ translates to a valid derivation in the Typer system. For most typing rules, the proof is straightforward: we assume the translated premises by the induction hypothesis and show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules. - - \underline{\textbf{Case 1:}} \begin{mathpar} \infer @@ -456,10 +454,22 @@ The translation is immediately true under Typer by rule \textsc{Wf-E}. \tag{CC-Wf-S} \end{mathpar} By the induction hypothesis we can assume -\begin{mathpar} - {\rew{\Ga} ~ \rew{T}:\rew{s} \ \rew{s} \in \S \ x \notin \dv{\rew{\Ga}}} -\end{mathpar} -which allows us to infer the translation of the conclusion by rule +$$\rew{\Ga} ~ \rew{T}:\rew{s}$$ + +and we have that +$$\rew{s \in S_{CC}} \leadsto \rew{s} \in \S.$$ + +We have yet to show that +$$x \notin \dv{\rew{\Ga}}$$ + +\begin{lemma} + The following holds: + $$x \notin \dv{\Ga} \Rightarrow x \notin \dv{\rew{\Ga}}$$ + \begin{proof} + \todo + \end{proof} +\end{lemma} +We can now infer the translation of the conclusion by rule \begin{mathpar} \infer {\rew{\Ga} ~ \rew{T}:\rew{s} \ \rew{s} \in \S \ x \notin \dv{\rew{\Ga}}} @@ -475,10 +485,12 @@ which allows us to infer the translation of the conclusion by rule \tag{CC-Sort} \end{mathpar} By the induction hypothesis we can assume -\begin{mathpar} - {\rew{\Ga} ~ \ (\rew{s_1}:\rew{s_2}) \in \A} -\end{mathpar} -and reach the translation of the conclusion by rule +$$\rew{\Ga} ~$$ + +and we have that +$$\rew{(s_1:s_2) \in \A_{CC}} \leadsto (\rew{s_1}:\rew{s_2}) \in \A.$$ + +We reach the translation of the conclusion by rule \begin{mathpar} \infer {\rew{\Ga} ~ \ (\rew{s_1}:\rew{s_2}) \in \A} @@ -494,9 +506,16 @@ and reach the translation of the conclusion by rule \tag{CC-Var} \end{mathpar} By the induction hypothesis we can assume -\begin{mathpar} - {\rew{\Ga} ~ \ (x:\rew{T}) \in \rew{\Ga}} -\end{mathpar} +$$\rew{\Ga} ~$$ + +\begin{lemma} + The following holds: + $$(x:T) \in \Ga \Rightarrow (x:\rew{T}) \in \rew{\Ga}$$ + \begin{proof} + If $\Ga = \cdot\ $, then the implication is true by the fact that the antecedant is false. Else, if $\Ga = \Delta, (x : T)$, then + \end{proof} +\end{lemma} + and reach the translation of the conclusion by rule \begin{mathpar} \infer @@ -517,8 +536,10 @@ By the induction hypothesis, there are two subcases to consider---a predicative \textbf{Predicative subcase:}\ We have the assumptions \begin{mathpar} - {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{s_2} \ (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R} + {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{s_2}} \end{mathpar} +and we know that +$$\rew{(s_1,s_2,s_3) \in \R_{CC}} \leadsto (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$$ from which we can conclude \begin{mathpar} \infer @@ -530,8 +551,10 @@ from which we can conclude \textbf{Impredicative subcase:}\ We have the assumptions \begin{mathpar} - {\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} + {\rew{\Ga} ~ \rew{T}:\rew{\Type_i} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{\Prop}} \end{mathpar} +and we know that +$$\rew{(\Type_i,\Prop,\Prop) \in \R_{CC}} \Rightarrow (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e$$ from which we can conlcude \begin{mathpar} \infer @@ -540,14 +563,14 @@ from which we can conlcude \tag{E-Prod} \end{mathpar}

-\begin{remark} The only way to construct a product type in \CC\ is through the application of typing rule \textsc{CC-Prod}, so all translations of product types will follow this rule: -\begin{align*} - \rew{(x:T)\explicit U} \leadsto - \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} -\end{align*} +\begin{remark} The only way to construct a product type in \CC\ is through the application of typing rule \textsc{CC-Prod}, so we know that all translations of product types will follow the rule: + \begin{align*} + \rew{(x:T)\explicit U} \leadsto + \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} + \end{align*} \end{remark}

\underline{\textbf{Case 6:}\} @@ -610,7 +633,7 @@ The impredicative product type translates to an erasable product type $(x:\rew{T but we have yet to show that the additional premise $x \notin \fv{\rew{M}^*}$ of rule \textsc{E-Lam} holds in all cases.

\begin{lemma} - By our currently defined translation \rew{\ }, the following holds: \vspace{-5mm} + The following holds: \vspace{-5mm} \end{lemma} \begin{mathpar} \infer @@ -620,12 +643,12 @@ but we have yet to show that the additional premise $x \notin \fv{\rew{M}^*}$ of \end{mathpar} \begin{proof} 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*} + \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}

View it on GitLab: https://gitlab.com/monnier/typer/commit/2eb3b21039b42625aefadf9dece27105959b...