Nathaniel pushed to branch bosn at Stefan / Typer

Commits: 70fac346 by nbos at 2018-08-22T09:14:43Z Fix part of lem:FV-E-Lam; expand on example Pack

- - - - -

1 changed file:

- doc/formal/typer_theory.tex

Changes:

===================================== doc/formal/typer_theory.tex ===================================== @@ -30,7 +30,7 @@ We here formalize the Typer language and prove some of its properties. The gist \end{itemize}

\section{Typer's Type Theory} -\textbf{Notation:} We define a context $\Ga$ as a list of typing declarations $(x_i:T_i)$ and write $\Ga ~$ to express that $\Ga$ is well formed. Contexts are concatenated with the semicolon (;) and enriched with additional declarations with a comma (,). We write the empty context as a dot ($\cdot$) and the set of declared variables in a context $\Ga$ as $\dv{\Ga}$. The set of free variables in a term $T$ is written $\fv{T}$. The expression $M{N/x}$ denotes the substitution of free occurrences of variable $x$ for a term $N$ in term $M$. +\textbf{Notation:} We define a context $\Ga$ as a list of typing declarations $(x_i:T_i)$ and write $\Ga ~$ to express that $\Ga$ is well formed. Contexts are concatenated with the semicolon (;) and enriched with additional declarations with a comma (,). We write the empty context as a dot ($\cdot$) and the set of declared variables in a context $\Ga$ as $\dv{\Ga}$. The set of free (i.e. unbound) variables in a term $T$ is written $\fv{T}$. The expression $M{N/x}$ denotes the substitution of free occurrences of variable $x$ for a term $N$ in term $M$.

\begin{figure}[h] \ \ \ \ \fbox{ @@ -105,8 +105,8 @@ After elaboration, implicit terms behave exactly like explicit terms so we will \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] + (\la(x:T)\explicit M)^* &= \la(x)\explicit M^* & ((x:T)\explicit U)^* &= (x:T^*)\explicit U^* \ + (\la(x:T)\erasable M)^* &= M^* & ((x:T)\erasable U)^* &= \forall(x:T^*).U^* \[5pt] (M \ap N)^* &= M^*\ap N^* & (M \appp N)^* &= M^*\ \end{align*} \end{minipage}} @@ -177,7 +177,7 @@ There are two notable differences between explicit and erasable typing rules:

\subsection{Inductive Definitions} -\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}|$. +\textbf{Notation:} We use a vector notation to refer to a series of finitely many 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}|$. @@ -394,7 +394,7 @@ In this section we will prove that the erasable terms of Typer allow for a repre \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 : ...$$ +Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, with an 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_{\max (i,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}).

@@ -449,13 +449,6 @@ Before proving the correctness of the equality, we will need the following lemma \begin{proof} In the forward direction, for $\Prop \in S_{CC}$, we know that $$\rew{\Prop} = \Type\ \z\ \in \S$$ And for $\Type_i \in \S_{CC}$, we know that $$\rew{\Type_i} = \Type\ (\s^i\ \z) \in \S \quad \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' Conversely, because the translation on sorts is defined on elements of $S_{CC}$, it follows that if $\rew{s} \in S$, then by necessity $s \in S_{CC}$. \end{proof} \end{lemma} @@ -532,65 +525,6 @@ Before proving the correctness of the equality, we will need the following lemma \end{proof} \end{lemma}

-%% FIXME: lem:E-Lam-FV was placed here because fitting it in the -%% impredicative subcase of CC-Lam case of the proof of completeness -%% required too many nested cases (subcase of a case to prove a subcase of -%% a case...) for the notation to remain consistent. -\begin{lemma} - \label{lem:E-Lam-FV} - If we have - \begin{mathpar} - %% TODO: Check if the condition `T:Type (s ℓ)` is really necessary - %% (If not, also fix on last case of completeness proof) - {\Ga, x:T ~ M:U \ \Ga ~ (x:T) \erasable U : \Type\ \z \ T : \Type\ \s\ \l} - \end{mathpar} - then the following always holds - $$x \notin \fv{M^*}$$ - - \begin{proof}\ \ - By structural induction on extracted terms (see figure \ref{fig:*}), either $M^*$ cannot be equal to it, or $x$ cannot be free within it, thus showing that $x \notin \fv{M^*}$. First, some terms that cannot be $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*). - \underline{\textbf{Case}} $M^* = x^* = x$:\ - This is impossible because we know that $x : T$ and since $$(x:T)\erasable U : \Prop$$ then, under the only possible construction of an erasable product type, we know that $T : \Type\ (\s\ \l)$ and $U : \Type\ \z$. Because $T$ and $U$ inhabit different universes, their inhabitants $x : T$ and $M : U$ cannot be equal. - - \underline{\textbf{Case}} $M^* = ((x:t)\explicit V)^*$ or $((x:t)\erasable V)^*$:\ - $M$ cannot be a product type since it inhabits the type $\Type\ \z$ which is our smallest universe so we cannot have a type two levels down. - - Now for the cases where $x$ is not free in the extraction of $M$: - - \underline{\textbf{Case}} $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}} $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}} $M^* = (\la(x:t)\erasable V)^*$:\ - The extraction makes this $V^*$. By the induction hypothesis, $x$ is not free in $V^*$. - - \underline{\textbf{Case}} $M^* = (P \ap 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}} $M^* = (P \appp Q)^*$:\ - 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} -\end{lemma}

\subsection{Completeness of translation} By structural induction on typing derivation, as per theorem \ref{thm:correctness-translation} ($\Rightarrow$), each valid derivation of \CC\ translates to a valid derivation in the Typer system. For most typing rules, the proof consists in assuming the translated premises by the induction hypothesis and then showing that the translation of the conclusion from them by one of Typer's typing rules. @@ -759,11 +693,58 @@ The predicative product type translates to an explicit product type $(x:\rew{T}) \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 $\rew{\Prop} = \Type\ \z$. We can appeal to lemma \ref{lem:E-Lam-FV} which states that if we have -\begin{mathpar} - {\Ga, x:T ~ M:U \ \Ga ~ (x:T) \erasable U : \Type\ \z \ T : \Type\ \s\ \l} -\end{mathpar} -then the following always holds +The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ which necessarily has sort $\rew{\Prop} = \Type\ \z$. To apply the corresponding Typer rule \textsc{E-Lam}, we must first show that $x \notin \fv{\rew{M}^*}$. + +\begin{lemma} + \label{lem:E-Lam-FV} + If we have + \begin{mathpar} + %% TODO: Check if the condition `T:Type (s ℓ)` is really necessary + %% (If not, also fix on last case of completeness proof) + {\Ga, x:T ~ M:U \ \Ga, x:T ~ U : \Type\ \z \ \Ga ~ T : \Type\ (\s\ \l)} + \end{mathpar} + then the following always holds + $$x \notin \fv{M^*}$$ + + \begin{proof}\ \ + By structural induction on extracted terms (figure \ref{fig:*}), either $M^*$ cannot be equal to it, or $x$ cannot be free within it, thus showing that $x \notin \fv{M^*}$. + + \textbf{Case} $M^* = y^*$:\ + The extraction is $y^* = y$. It cannot be that $y = x$ because $x : T : \Type (\s\ \l)$ and $y : U : \Type\ \z$ and equality is not defined between inhabitants of different types nor different universe. Therefore, $x \notin \fv{y}$ because $x \neq y$. + + \textbf{Case} $M^* = ((x:t)\explicit V)^*$ or $((x:t)\erasable V)^*$:\ + $M$ cannot be a product type since its type $U$ inhabits the smallest universe $\Type\ \z$ . + + %% 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. + \textbf{Case} $M^* = (s)^*$ with $s \in \S$:\ + The extraction is $s^* = s$. All $s \in S$ are closed constants and thus $x \notin \fv{s}$. + + \textbf{Case} $M^* = (\la(y:t)\explicit V)^*$:\ + The extraction makes this $\la(y)\explicit V^*$. By the rules in $\R$, if $M$ has sort $\Type\ \z$, then it is an upper bound for the sort of $V$. Thus, $V : U' : \Type\ \z$ and we have $x \notin \fv{V^*}$ by the induction hypothesis. + + \textbf{Case} $M^* = (\la(y:t)\erasable V)^*$:\ + The extraction makes this $V^*$. By the rules in $\R_e$, if $M$ has sort $\Type\ \z$, then $V$ also has sort $\Type\ \z$. Thus, by the induction hypothesis, $x \notin \fv{V^*}$. + + %% FIXME: + \textbf{Case} $M^* = (P \ap 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^*$. + + %% FIXME: Again, $P$ can be something else than an abstraction. + \textbf{Case} $M^* = (P \appp Q)^*$:\ + The extraction is $(P \appp Q)^* = P^*$. $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} +\end{lemma} + +By lemma \ref{lem:E-Lam-FV} above, we can infer $$x \notin \fv{M^*}$$

and we have the sufficient premises to apply rule \textsc{E-Lam} and we obtain the translation of the conclusion: @@ -952,9 +933,54 @@ Where $s_1 \neq \Type_1$ or $s_2 \neq \Prop$: Rules \textsc{Ind}, \textsc{Constr}, and \textsc{Case} cannot construct the judgment $\rew{\Ga} ~ \rew{e} : \rew{\tau}$ because inductive types are not part of the domain of the translation operator.

\subsection{Example} +Consider the impredicative encoding of the \texttt{pack} existential type constructor in \CC: + +\begin{align*} + \mathtt{pack}\ : \quad + &(\tau : \Type_1) \explicit (f : (x : \tau) \explicit \Prop) \explicit (w : \tau) \explicit (p : f| w) \explicit\ + &(t : \Prop) \explicit (b : (y : \tau) \explicit (z : f|y) \explicit t) \explicit t {w/y} {p/z}\[10pt] + :=\ &\la (\tau : \Type_1) \explicit \la (f : (x : \tau) \explicit \Prop) \explicit \la (w : \tau) \explicit \la (p : f|w) \explicit\ + &\la (t : \Prop) \explicit \la (b : (y : \tau) \explicit (z : f|y) \explicit t) \explicit b|w|p +\end{align*} + +The translation of \texttt{pack} to Typer will assign abstractions to be either explicit or erasable depending on them being predicative of impredicative, respectively. The translation of the product type of $f$ in \texttt{pack} for example will be explicit by its predicativity: +\begin{align*} + \Ga &\CCdash \tau : \Type_1\ + \Ga &\CCdash \Prop : \Type_1\ + \Ga &\CCdash (x : \tau)\explicit\Prop : \Type_1 &\quad\quad\text{by \texttt{CC-Prod} and rule $(\Type_1,\Type_1,\Type_1)$} +\end{align*} +\begin{align*} + \rew{\Ga} \CCdash \rew{(x : \tau)\explicit\Prop} : \rew{\Type_1} + &\quad\leadsto\quad \rew{\Ga} ~ (x : \rew{\tau}) \explicit \rew{\Prop} : \Type\ (\s\ \z)\ + &\quad\leadsto\quad \rew{\Ga} ~ (x : \tau) \explicit \Type\ \z : \Type\ (\s\ \z) +\end{align*} + +However, $b$ has both an erasable and an explicit component: + +\begin{align*} + \Ga &\CCdash t : \Prop \ + \Ga &\CCdash f|y : \Prop \ + \Ga &\CCdash (z : f|y)\explicit t : \Prop &\quad\quad\text{by \texttt{CC-Prod} and rule $(\Prop,\Prop,\Prop)$}\[10pt] + \Ga &\CCdash \tau : \Type_1 \ + \Ga &\CCdash (z : f|y)\explicit t : \Prop\ + \Ga &\CCdash (y : \tau)\explicit (z : f|y)\explicit t : \Prop &\quad\quad\text{by \texttt{CC-Prod} and rule $(\Type_1,\Prop,\Prop)$}\ +\end{align*} +\begin{align*} + \rew{\Ga} \CCdash \rew{(y : \tau)\explicit (z : f|y)\explicit t} : \rew{\Prop} + &\quad\leadsto\quad \rew{\Ga} ~ (y : \tau)\erasable \rew{(z : f|y)\explicit t} : \Type\ \z\ + &\quad\leadsto\quad \rew{\Ga} ~ (y : \tau)\erasable (z : f|y)\explicit \rew{t} : \Type\ \z\ + &\quad\leadsto\quad \rew{\Ga} ~ (y : \tau)\erasable (z : f|y)\explicit t : \Type\ \z\ +\end{align*} + +Thus, the application of $b$ to the witness and the proof will translate \todo + +RESULT: \begin{align*} - \mathtt{pack =}\ &\la (\tau : \Type_1) \explicit \la (f : (x : \tau) \explicit \Prop) \explicit \la (w : \tau) \explicit \la (p : f|w) \explicit\ &\la (t : \Prop) \explicit \la (b : (y : \tau) \explicit f|y \explicit t) \explicit (b|w)|p\[10pt] - \mathtt{pack :}\ & (\tau : \Type_1) \explicit (f : (x : \tau) \explicit \Prop) \explicit (w : \tau) \explicit (p : f| w) \explicit\ &(t : \Prop) \explicit (b : (y : \tau) \explicit (z : f|y) \explicit t) \explicit t {w/y} {p/z} + \mathtt{pack}\ : \quad + &(\tau : \Type\ (\s\ \z)) \erasable (f : (x : \tau) \explicit \Type\ \z) \erasable (w : \tau) \erasable (p : f| w) \explicit\ + &(t : \Type\ \z) \erasable (b : (y : \tau) \erasable (z : f|y) \explicit t) \explicit t {w/y} {p/z}\[10pt] + :=\ &\la (\tau : \Type\ (\s\ \z)) \erasable \la (f : (x : \tau) \explicit \Type\ \z) \erasable \la (w : \tau) \erasable \la (p : f|w) \explicit\ + &\la (t : \Type\ \z) \erasable \la (b : (y : \tau) \erasable (z : f|y) \explicit t) \explicit b|||w|p \end{align*}

View it on GitLab: https://gitlab.com/monnier/typer/commit/70fac34657d55b95b7c7cb36178c051577a7...