Nathaniel pushed to branch bosn at Stefan / Typer
Commits: 1e7b80b3 by nbos at 2018-07-09T20:19:32Z Prettified boxes; fixed PTS definition; added impredicative R; gave explanations on E- vs R- rules
- - - - - 0881ba77 by nbos at 2018-07-09T21:45:50Z New macro
- - - - - a05b2179 by nbos at 2018-07-09T21:46:50Z Started CCw to Typer translation
- - - - -
2 changed files:
- doc/formal/commands.tex - doc/formal/typer_theory.tex
Changes:
===================================== doc/formal/commands.tex ===================================== @@ -66,3 +66,5 @@ \end{center}}
\renewcommand{:}{\hspace{-3pt}:\hspace{-3pt}} + +\newcommand{\CCdash}{\vdash_{\hspace{-2pt}_{CC}}} \ No newline at end of file
===================================== doc/formal/typer_theory.tex ===================================== @@ -33,7 +33,7 @@ We here formalize the Typer language and prove some of its properties. The gist \textsc{ (Wf-E)} \and %-------------------- \infer - {\Ga ~ T:s \ x \notin \dv{\Ga}} + {\Ga ~ T:s \ s \in \S \ x \notin \dv{\Ga}} {\Ga , x:T ~} \textsc{ (Wf-S)} \and %-------------------- @@ -62,24 +62,33 @@ Each type universe \textsf{Type} $\l$ has an index $\l$ of the type \textsf{Type
We call $\mathbb{L}$ the smallest set that is closed under the constructors for \textsf{TypeLevel}, such that we have countably infinite set of indexes $\l$. We have that \textsf{SortL} is the sort of type \textsf{TypeLevel}. And \textsf{Sort}$_\omega$ is the sort of universe polymorphic types. We define the union operator (\textsf{TypeLevel.\u} : \textsf{TypeLevel} $\to$ \textsf{TypeLevel} $\to$ \textsf{TypeLevel}) which returns the greater of two type levels.
-The above definitions allow the description of Typer as a Pure Type System \cite{barendregt}: +The above definitions allow the description of the explicit subset of Typer as a Pure Type System \cite{barendregt}: % \begin{empheq}[box=\fbox]{equation}
\begin{figure}[h] \begin{empheq}[box=\fbox]{align*} - \ - \S = { & \textsf{SortL}; \textsf{ Sort}_\omega; \textsf{ Type } \l; \textsf{ TypeLevel}} &\forall\l \in \mathbb{L} \[9pt] + \hspace{15mm} & \ & \ & \hspace{7mm} \ + \S = { & \textsf{SortL}; \textsf{ Sort}_\omega; \textsf{ Type } \l} &\forall\l \in \mathbb{L} \[9pt] \A = { &(\textsf{TypeLevel} : \textsf{SortL}); \ - &(\textsf{Type } \l : \textsf{Type } (\textsf{TypeLevel.s } \l))} \[9pt] + &(\textsf{Type } \l : \textsf{Type } (\textsf{TypeLevel.s } \l))} &\forall\l \in \mathbb{L} \[9pt] \R = { &(\textsf{SortL}, \textsf{ Type } \l, \textsf{ Sort}_\omega); &\forall\l \in \mathbb{L} \ &(\textsf{SortL}, \textsf{ Sort}_\omega, \textsf{ Sort}_\omega); \ - &(\textsf{Type } \l_1, \textsf{ Type } \l_2, \textsf{ Type } (\textsf{TypeLevel.\u}\ \l_1 \l_2))} &\forall\l_1,\l_2 \in \mathbb{L}\ + &(\textsf{Type } \l_1, \textsf{ Type } \l_2, \textsf{ Type } (\textsf{TypeLevel.\u}\ \l_1 \l_2))} &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] \end{empheq} \caption{Typer's Pure Type System} \end{figure}
+Because of the impredicativity of the erasable part of Typer, we need to define a separate set of impredicative rules, written $\R_I$, all of which will be referred as $(s_1,s_2)$ as an abreviation for $(s_1,s_2,s_2)$. +\begin{figure}[h] + \begin{empheq}[box=\fbox]{align*} + \hspace{15mm} & \ & \ & \hspace{7mm} \ + \R_{I} = { &( \textsf{Type } \l_1, \textsf{ Type } \l_2, \textsf{ Type } \l_2) } &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] + \end{empheq} + \caption{Typer's Impredicative Rules} +\end{figure} + \subsection{ICC in Typer} -Typer provides distinction between three kinds of terms to simplify both the writing and execution of programs. \emph{Explicit} terms are the usual expression that are written by the user and then executed. \emph{Implicit} terms are also used during execution, but Typer is able to infer them during elaboration such that they do not need to be written by the user. \emph{Erasable} terms are neither written by the user nor executed; they are infered during elaboration, participate in type checking and are then erased before execution. Compound terms of our calculus are therefore constructed in the following manner: +Typer provides distinction between three kinds of terms to simplify both the writing and execution of programs. \emph{Explicit} terms are the usual expression that are written by the user and then executed. \emph{Implicit} terms are also used during execution, but Typer is able to infer them during elaboration such that they do not need to be written by the user. \emph{Erasable} terms are neither written by the user nor executed; they are infered during elaboration, participate in type checking and are then erased before execution. The notation we adopt for compound terms are the following:
\begin{center} \begin{tabular}[h]{rclll} @@ -90,13 +99,7 @@ Typer provides distinction between three kinds of terms to simplify both the wri \end{tabular} \end{center}
-After elaboration, implicit terms behave exactly like explicit terms, so we will only present the semantics of explicit terms and it is assumed that they also hold for implicit terms. The typing rules for explicit and erasable terms are shown in Figure 2. They are the standard rules of a Church-style lambda calculus, duplicated for both kinds of terms. There are two differences between explicit and erasable typing rules: -\begin{enumerate} -\item In \textsc{R-Prod}, the sorts are of the form $(s_1,s_2,s_2)$ so that \todo -\item -\end{enumerate} - -An extractions function $M \mapsto M^*$ (as defined in \cite{bruno}) erases domains of abstraction, erasable abstractions and erasable applications. It also turns erasable products into a propositional form. +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*} s^* &= s & x^* &= x \[5pt] (\la(x:T)\explicit U)^* &= \la(x)\explicit U^* & ((x:T)\explicit U)^* &= (x:T^*)\explicit U^* \ @@ -104,6 +107,8 @@ An extractions function $M \mapsto M^*$ (as defined in \cite{bruno}) erases doma (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. + \begin{figure}[h] \ \ \ \ \fbox{ \begin{mathpar} @@ -124,7 +129,7 @@ An extractions function $M \mapsto M^*$ (as defined in \cite{bruno}) erases doma \textsc{ (E-App)} \\ \infer - {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2,s_2) \in \R} + {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2) \in \R_I} {\Ga ~ (x:T) \erasable U : s_2} \textsc{ (R-Prod)} \and %-------------------- @@ -144,6 +149,14 @@ An extractions function $M \mapsto M^*$ (as defined in \cite{bruno}) erases doma \end{figure}
+There are two differences between explicit and erasable typing rules: +\begin{enumerate} +\item In the ersasable product rule \textsc{R-Prod}, the set of rules is the impredicative $\R_I$ instead of $\R$ +\item In the erasable abstraction rule \textsc{R-Lam}, erasable abstraction are conditional on the bound variable not being free in the expression after erasure ($x \notin \fv{M^*}$). This ensures that the variable is only used in ``erasable'' ways inside the expression such that we are not left with incoherent terms. +\end{enumerate} + + + \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}|$.
@@ -170,7 +183,7 @@ The typing of the individual cases $G_i$ in $\textsf{Case}\ M: S \text{ of } < \S{(\vec{x}:\vec{M})C,I,Q,R} && = && (\vec{x}:\vec{M})\S{C,I,Q,(Rx)} && \text{if $X$ is not free in $M_i$ $\forall i \in |\vec{M}|$} \ \S{(X\vec{N}),I,Q,R} && = && (Q \vec{N} R) \end{align*} -The typing rules for inductive definitions and case analysis are presented in Figure 3. +The typing rules for inductive definitions and case analysis are presented in Figure X.
\begin{figure}[h] \ \ \ \ \fbox{ @@ -217,7 +230,7 @@ Recursion is specified through the use of a recursive operator \Letrec \todo
\textbf{Definition:} A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to stricly positive occurences [? not a form of constructor w.r.t $X$ ?], is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$ [? can't ?]. We abbreviate this property as $RP{i,C}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$.
-\textbf{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{f,k,x,M}$ is determined by structural induction on term $M$: +\textbf{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} \ @@ -257,22 +270,94 @@ Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $ \end{figure}
\section{Relative Expressivity to \CC} -In this section we will prove that the impredicative sorts and the universe hierarchy of Typer allow of at least equal expressivity to that of a subset of Luo's ECC \cite{luo}. Specifically, we will translate the typing derivations from the Caluclus of Constructions with an infinite hierarchy of universes, but without cumulativity (\CC) to Typer's rules made explicit in \textsection 2. +In this section we will prove that the impredicative rules and the universe hierarchy of Typer allow for a representation of all typing derivations from a Calculus of Constructions with an infinite hierarchy of (uncummulative) universes (\CC).
\subsection{Definition of \CC} +The typing rules for \CC\ are shown in Figure X. They are the standard rules for the Calulus of Constructions \cite{}, but the underlying PTS has an infinite hierarchy of universes (Figure X). + \begin{figure}[h] \begin{empheq}[box=\fbox]{align*} - \ - \S = { & \textsf{Prop}; \textsf{ Type}_i} &\forall i > 0 \[9pt] - \A = { &(\textsf{Prop} : \textsf{Type}_1); \ + \hspace{15mm} & \ & \ & \hspace{7mm} \ + \S_{CC} = { & \textsf{Prop}; \textsf{ Type}_i} &\forall i > 0 \[9pt] + \A_{CC} = { &(\textsf{Prop} : \textsf{Type}_1); \ &(\textsf{Type}_i : \textsf{Type}_{i+1})} &\forall i > 0 \[9pt] - \R = { &(\textsf{Type}_i, \textsf{ Prop }, \textsf{ Prop}); &\forall i > 0 \ + \R_{CC} = { &(\textsf{Type}_i, \textsf{ Prop }, \textsf{ Prop}); &\forall i > 0 \ &(\textsf{Type}_i,\textsf{Type}_i,\textsf{Type}_i); &\forall i > 0 \ \end{empheq} \caption{\CC's Pure Type System} \end{figure}
-\newpage -\bibliographystyle{acm} +\begin{figure}[h] + \ \ \ \ \fbox{ + \begin{mathpar} + \ + \infer + {\ } + {\emptyctx \CCdash} + \textsc{ (Wf-E)} + \and %-------------------- + \infer + {\Ga \CCdash T:s \ s \in \S_{CC} \ x \notin \dv{\Ga}} + {\Ga , x:T \CCdash} + \textsc{ (Wf-S)} + \and %-------------------- + \infer + {\Ga \CCdash \ (s_1:s_2) \in \A_{CC}} + {\Ga \CCdash s_1:s_2} + \textsc{ (Sort)} + \and %-------------------- + \infer + {\Ga \CCdash \ (x:T) \in \Ga} + {\Ga \CCdash x:T} + \textsc{ (Var)} + \and %-------------------- + \infer + {\Ga \CCdash T:s_1 \ \Ga, x:T \CCdash U:s_2 \ (s_1,s_2,s_3) \in \R_{CC}} + {\Ga \CCdash (x:T) \explicit U : s_3} + \textsc{ (CC-Prod)} + \and %-------------------- + \infer + {\Ga, x:T \CCdash M:U \ \Ga \CCdash (x:T) \explicit U : s} + {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U} + \textsc{ (CC-Lam)} + \and %-------------------- + \infer + {\Ga \CCdash M : (x:T) \explicit U \ \Ga \CCdash N:T} + {\Ga \CCdash M|N : U{N/x}} + \textsc{ (CC-App)} + \end{mathpar} + } + \caption{\CC's Typing Rules} +\end{figure} + +\subsection{Proof} + +\textbf{Theorem:} All derivable terms in \CC\ are also derivable terms of Typer's calculus. +\begin{proof}[Proof:]\ \ + \textbf{Case 1: Context and Sorts Rules} + + The translation is almost trivial as the four rules \textsc{Wf-E}, \textsc{Wf-S}, \textsc{Sort}, and \textsc{Var} are unchanged between the two calculi. The only necessary translation is between the universe hierarchies. We therefore have a mapping $\S_{CC} \to \S$: + \begin{align*} + \textsf{Prop} &\mapsto \textsf{Type TypeLevel.z} \ + \textsf{Type$_1$} &\mapsto \textsf{Type TypeLevel.s(TypeLevel.z)} \ + \textsf{Type$_2$} &\mapsto \textsf{Type TypeLevel.s(TypeLevel.s(TypeLevel.z))} \ + \vdots~~~~~ &\mapsto ~~~~~~~\vdots + \end{align*} + + Through this mapping, all axioms of $\A_{CC}$ are analogous to axiom scheme $(\textsf{Type } \l : \textsf{Type } (\textsf{TypeLevel.s } \l))}~\forall\l \in \mathbb{L}$ from $\A$. + + \textbf{Case 2: \textsc{CC-Prod}} + + $\R_{CC}$ has members analogous to members of both $\R$ and $\R_i$. Specifically [?] + + \textbf{Case 3: \textsc{CC-Lam}} + + + \textbf{Case 4: \textsc{CC-App}} + +\end{proof} + + \newpage +\bibliographystyle{alpha} \bibliography{typer_theory} \end{document} \ No newline at end of file
View it on GitLab: https://gitlab.com/monnier/typer/compare/27f86f6180f121dbf24c8ccce5b0e05b302...
Afficher les réponses par date