Nathaniel pushed to branch bosn at Stefan / Typer
Commits: 16b5fb2e by nbos at 2018-07-24T07:13:51Z Changed notation for CCw; added abbrevs for keyworkds (sans serif)
- - - - - 5a751a66 by nbos at 2018-07-24T07:18:02Z Finished translation from CCw; changed presentation of CCw to be based on CC rather than ECC
- - - - -
2 changed files:
- doc/formal/commands.tex - doc/formal/typer_theory.tex
Changes:
===================================== doc/formal/commands.tex ===================================== @@ -6,14 +6,20 @@ \newcommand{\fv}[1]{\textsf{FV}(#1)}
%% Sans -\newcommand{\Ind}{\textsf{Ind}} -\newcommand{\Constr}{\textsf{Constr}} -\newcommand{\Case}{\textsf{Case}} -\newcommand{\Elim}{\textsf{Elim}} -\newcommand{\Fix}{\textsf{Fix}} -\newcommand{\Letrec}{\textsf{Letrec }} -\newcommand{\Let}{\textsf{Let }} -\newcommand{\In}{\textsf{ in }} +\newcommand{\Ind}{\ensuremath{\mathsf{Ind}}} +\newcommand{\Constr}{\ensuremath{\mathsf{Constr}}} +\newcommand{\Case}{\ensuremath{\mathsf{Case}}} +\newcommand{\Elim}{\ensuremath{\mathsf{Elim}}} +\newcommand{\Fix}{\ensuremath{\mathsf{Fix}}} +\newcommand{\Letrec}{\ensuremath{\mathsf{Letrec}}} +\newcommand{\Let}{\ensuremath{\mathsf{Let}}} +\newcommand{\In}{\ensuremath{\mathsf{in}}} + +\newcommand{\Prop}{\ensuremath{\mathsf{Prop}}} +\newcommand{\Type}{\ensuremath{\mathsf{Type}}} +\newcommand{\TypeLevel}{\ensuremath{\mathsf{TypeLevel}}} +\newcommand{\Sortw}{\ensuremath{\mathsf{Sort}_\omega}} +\newcommand{\SortL}{\ensuremath{\mathsf{SortL}}}
% Bolds \newcommand{\todo}{\textbf{ TODO }} @@ -59,7 +65,7 @@ \newcommand{\appp}{\raisebox{1.7pt}{\scalebox{0.8}{$|||$}}}
\renewcommand{\u}{$\scriptstyle\cup\ $} -\newcommand{\CC}{\text{CC$^{\npreceq}_{\omega}$}} +\newcommand{\CC}{\text{CC$\omega$}}
\newcommand{\SmallTitle}[1]{\vspace{3mm}\begin{center} \bf \underline{#1}
===================================== doc/formal/typer_theory.tex ===================================== @@ -3,7 +3,7 @@
\usepackage{amsmath,amsthm,amssymb,mathtools} \usepackage{mathpartir,mdframed,empheq} -\usepackage{parskip} +\usepackage{parskip,authblk}
\input{commands} \begin{document} @@ -43,22 +43,22 @@ We here formalize the Typer language and prove some of its properties. The gist \end{figure}
\subsection{Universes and Universe Polymorphism} -Each type universe \textsf{Type} $\l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \textsf{z} ~~|~~ \textsf{s}\ \l ~~|~~ \l_1 \cup \l_2 ~~|~~ l$$ +Each type universe $\mathsf{Type}\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \mathsf{z} ~~|~~ \mathsf{s}\ \l ~~|~~ \l_1 \cup \l_2 ~~|~~ l$$ %% FIXME: We'll need somewhere to clarify that those `l`s have to be present %% in the Γ environment with type TypeLevel. -All type levels $\l$ inhabit the type \textsf{TypeLevel} which itself belongs to the sort \textsf{SortL}. The two first constructs correspond to the constant zero and to the successor function, respectively. We define a set $\mathbb{L}$ which is closed under those two constructs and thus contains a type level $\l \in \mathbb{L}$ for every conventional natural number $n \in \mathbb{N}$. The operator $\cup$ returns the maximum of two type levels. The construct $l$ stands for a \emph{level variable} which will occur in universe polymorphic definitions. +All type levels $\l$ inhabit the type \TypeLevel\ which itself belongs to the sort \SortL. The two first constructs correspond to the constant zero and to the successor function, respectively. We define a set $\mathbb{L}$ which is closed under those two constructs and thus contains a type level $\l \in \mathbb{L}$ for every conventional natural number $n \in \mathbb{N}$. The operator $\cup$ returns the maximum of two type levels. The construct $l$ stands for a \emph{level variable} which will occur in universe polymorphic definitions.
-We have that \textsf{Sort}$_\omega$ is the unique sort of all the types of universe polymorphic functions. We can now describe the explicit subset of Typer as a Pure Type System \cite{barendregt}: +We have that \Sortw\ is the unique sort of all the types of universe polymorphic functions. We can now describe the explicit subset of Typer as a Pure Type System \cite{barendregt}:
\begin{figure}[h] \begin{empheq}[box=\fbox]{align*} \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{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 } (\l_1 \cup \l_2))} &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] + \S = { & \mathsf{SortL};\ \mathsf{Sort}_\omega;\ \mathsf{Type } \l} &\forall\l \in \mathbb{L} \[9pt] + \A = { &(\mathsf{TypeLevel} : \mathsf{SortL}); \ + &(\mathsf{Type}\ \l : \mathsf{Type}\ (\mathsf{s}\ \l))} &\forall\l \in \mathbb{L} \[9pt] + \R = { &(\mathsf{SortL},\ \mathsf{Type}\ \l,\ \mathsf{Sort}_\omega); &\forall\l \in \mathbb{L} \ + &(\mathsf{SortL},\ \mathsf{Sort}_\omega,\ \mathsf{Sort}_\omega); \ + &(\mathsf{Type}\ \l_1,\ \mathsf{Type}\ \l_2,\ \mathsf{Type}\ (\l_1 \cup \l_2))} &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] \end{empheq} \vspace{-5mm} \caption{Typer's Pure Type System} @@ -68,9 +68,9 @@ Because of the impredicativity of the erasable part of Typer, we need to define \begin{figure}[h] \begin{empheq}[box=\fbox]{align*} \hspace{15mm} & \ & \ & \hspace{7mm} \ - \R_e = { &(\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 } \l_2) } &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] + \R_e = { &(\mathsf{SortL},\ \mathsf{Type}\ \l,\ \mathsf{Sort}_\omega); &\forall\l \in \mathbb{L} \ + &(\mathsf{SortL},\ \mathsf{Sort}_\omega,\ \mathsf{Sort}_\omega); \ + &(\mathsf{Type}\ \l_1,\ \mathsf{Type}\ \l_2,\ \mathsf{Type}\ \l_2) } &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] \end{empheq} \vspace{-5mm} \caption{Typer's Impredicative Rules} @@ -129,8 +129,8 @@ The typing rules for explicit and erasable terms are shown in Figure X. They are \textsc{ (X-App)} \\ \infer - {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2) \in \R_e} - {\Ga ~ (x:T) \erasable U : s_2} + {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2,s_3) \in \R_e} + {\Ga ~ (x:T) \erasable U : s_3} \textsc{ (E-Prod)} \and %-------------------- \infer @@ -174,7 +174,7 @@ We extend our abstract syntax with four terms introduced in \cite{gimenez} to ex \setlength\itemsep{-3pt} \item $\Ind(X:A) <\vec{C}>$ which is an inductively defined type recursively bound to $X$. $\vec{C}$ is the list of constructor signatures which must be a \emph{form of constructor} w.r.t. $X$. \item $\Constr(i:I)$ stands for the $i$th constructor of an inductive type $I$. -\item $\textsf{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. +\item $\mathsf{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. @@ -212,10 +212,10 @@ The typing rules for inductive definitions and case analysis are presented in Fi %% %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq_refl : ((x : ?t) ≡> Eq x x); - %% Eq_cast : (x : ?) ≡> (y : ?) - %% ≡> (p : Eq x y) - %% ≡> (f : ? -> ?) - %% ≡> f x -> f y; + %% Eq_cast : (x : ?t) ≡> (y : ?t) + %% ≡> (p : Eq x y) + %% ≡> (f : ?t -> ?t') + %% ≡> f x -> f y; %% %% At run-time `Eq_cast` will be a no-op (i.e. `Eq_cast x` will reduce %% to `x`), but there is no corresponding normalization rule applied @@ -261,9 +261,7 @@ Recursion is specified through the use of a recursive operator \Letrec \todo \textsc{ (Let)} \end{mathpar}
- - -\textbf{Definition:} A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to strictly positive occurrences [? 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:} 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})$.
\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*} @@ -305,22 +303,20 @@ Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $ \caption{Typer's Conversion Rules} \end{figure}
-\section{Relative Expressivity to \CC} -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 (noncumulative) universes (\CC). +\section{Relative Expressivity to the 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} -Our definition of \CC\ is based on Luo's infinite hierarchy of universes designed for ECC \cite{luo}, but since Typer does not support subtyping, we remove the condition that the universes are cumulative. We also change the name of the universes so that they match more easily with Typer's during translation. Thus, instead of $$\textsf{Prop : Type$_0$ : Type$_1$ : Type$_2$ : ...},$$ we have $$\textsf{Prop : Type$_1$ : Type$_2$ : Type$_3$ : ...}.$$ But the semantics remain the same. - -\CC's PTS definition is shown in Figure X. The typing rules for \CC\ are shown in Figure X. They are the standard rules for the Calculus of Constructions \cite{}, but the underlying PTS has an infinite hierarchy of universes.
\begin{figure}[h] \begin{empheq}[box=\fbox]{align*} \hspace{20mm} & \ & \ & \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_{CC} = { &(\textsf{Type}_i, \textsf{ Prop }, \textsf{ Prop}); &\forall i > 0 \ - &(\textsf{Type}_i,\textsf{Type}_i,\textsf{Type}_i); &\forall i > 0 \ + \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 \ + &(\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} @@ -333,80 +329,75 @@ Our definition of \CC\ is based on Luo's infinite hierarchy of universes designe \infer {\ } {\emptyctx \CCdash} - \textsc{ (C-Wf-E)} + \textsc{ (CC-Wf-E)} \and %-------------------- \infer {\Ga \CCdash T:s \ s \in \S_{CC} \ x \notin \dv{\Ga}} {\Ga , x:T \CCdash} - \textsc{ (C-Wf-S)} + \textsc{ (CC-Wf-S)} \and %-------------------- \infer {\Ga \CCdash \ (s_1:s_2) \in \A_{CC}} {\Ga \CCdash s_1:s_2} - \textsc{ (C-Sort)} + \textsc{ (CC-Sort)} \and %-------------------- \infer {\Ga \CCdash \ (x:T) \in \Ga} {\Ga \CCdash x:T} - \textsc{ (C-Var)} + \textsc{ (CC-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{ (C-Prod)} + \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{ (C-Lam)} + \textsc{ (CC-Lam)} \and %-------------------- \infer {\Ga \CCdash M : (x:T) \explicit U \ \Ga \CCdash N:T} {\Ga \CCdash M|N : U{N/x}} - \textsc{ (C-App)} + \textsc{ (CC-App)} \ \end{mathpar} } \caption{\CC's Typing Rules} \end{figure}
-\subsection{Proof} - -%% FIXME: The term is "conservative extension". - -%% FIXME: ...the complexity will be in figuring out exactly when we need to -%% add those `erased` and when we need to remove them (by `case` analysis). -\textbf{Theorem:} All derivable terms in \CC\ are also derivable terms of Typer's calculus. -\begin{proof}[Proof:]\ \ - \textbf{Case 1: \textsc{C-Wf-E} and \textsc{C-Wf-S}} - - \textsc{Wf-E} translates trivially. To make erasure work in Typer, erasable arguments to a function must only occur in erasable positions. Erasability must thennot only be a property of abstractions and products, but of the variables which they instantiate. We thus include a type \todo +Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, but with an added infinite hierarchy of universes above the impredicative $\mathsf{Prop}$. They are arranged in the series: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4...$$
- - \textbf{Case 2: \textsc{C-Sort} and \textsc{C-Var}} - - A translation is necessary between the sets of sorts. We have a mapping $\S_{CC} \to \S$: +\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). +\subsection{Translation} + By induction on typing derivation steps. + \textsc{CC-Wf-E} and \textsc{CC-Var} both directly translate to \textsc{Wf-E} and \textsc{Var} respectively since they introduce nothing new. Because \textsc{CC-Sort} and \textsc{CC-Wf-S} call upon $\A_{CC}$ and $\S_{CC}$, we make a mapping between the universe hierarchies $\S_{CC} \to \S$: \begin{align*} - \textsf{Prop} &\mapsto \textsf{Type z} \ - \textsf{Type$_1$} &\mapsto \textsf{Type (s z)} \ - \textsf{Type$_2$} &\mapsto \textsf{Type (s (s z))} \ - \vdots~~~~~ &\mapsto ~~~~~~~\vdots + \mathsf{Prop} ~~~ &\mapsto ~~~ \mathsf{Type\ z} \ + \mathsf{Type_1} ~~~ &\mapsto ~~~ \mathsf{Type\ (s\ z)} \ + \mathsf{Type_2} ~~~ &\mapsto ~~~ \mathsf{Type\ (s\ (s\ z))} \ + \vdots~~~~~ ~~~ &\mapsto ~~~ ~~~~~~~\vdots \end{align*}
- As per this mapping, all axioms of $\A_{CC}$ are analogous to instances of the axiom scheme $(\textsf{Type } \l : \textsf{Type } (\textsf{s } \l))}~\forall\l \in \mathbb{L}$ from Typer's $\A$. + And axioms of $\A_{CC}$ become axioms of $\A$ by the translation of respective sorts, e.g. $\mathsf{(Prop : Type_1)}$ becomes $\mathsf{(Type\ z : Type\ (s\ z))}$. + + The typing rule \textsc{CC-Prod} calls upon the set of product rules $\R_{CC}$ which is analogous to both $\R$ and $\R_e$ at the same time. In particular, the first product rule scheme $$(\mathsf{Type}_i, \mathsf{Prop}, \mathsf{Prop}) \in R_{CC}$$ translates to + $$(\mathsf{Type}\ \l_, \mathsf{Type\ z}, \mathsf{Type\ z}) \in \R_e ~~~~~~ \forall \l \in \mathbb{L}$$ + and the second product rule scheme $$(\mathsf{Type}_i, \mathsf{Type}_i, \mathsf{Type}_i) \in R_{CC}$$ is a special case of + $$(\mathsf{Type}\ \l_1, \mathsf{Type}\ \l_2, \mathsf{Type}\ (\l_1 \cup \l_2))} \in \R ~~~~~~ \forall\l_1,\l_2 \in \mathbb{L}$$ + specifically when $\l_1 = \l_2$. Thus, use of the typing rule \textsc{CC-Prod} translate to use of \textsc{X-Prod} when a rule is of form $(\mathsf{Type}_i, \mathsf{Type}_i, \mathsf{Type}_i)$ and the resulting dependent product in Typer is explicit. \textsc{CC-Prod} translates to \textsc{E-Prod} when of form $(\Type_i, \Prop, \Prop)$.\
- \textbf{Case 3: \textsc{C-Prod}} - - $\R_{CC}$ has members analogous to members of both $\R$ and $\R_e$. Specifically, the first rule scheme $(\textsf{Type}_i, \textsf{ Prop}, \textsf{ Prop}) \in R_{CC}$ translates to the rule scheme - $$(\textsf{Type }\l_, \textsf{ Type z}, \textsf{ Type z}) \in \R_e ~~~~~~ \forall \l \in \mathbb{L}$$ - and the second rule $(\textsf{Type}_i, \textsf{Type}_i, \textsf{Type}_i) \in R_{CC}$ is a special case of the rule scheme - $$(\textsf{Type } \l_1, \textsf{ Type } \l_2, \textsf{ Type } (\l_1 \cup \l_2))} \in \R ~~~~~~ \forall\l_1,\l_2 \in \mathbb{L}$$ - specifically, when $\l_1 = \l_2$. Thus, use of the typing rule \textsc{C-Prod} translate to use of \textsc{X-Prod} in the case of a product of form $(\textsf{Type }\l_, \textsf{ Type z}, \textsf{ Type z})$ and \textsc{E-Prod} in the case of a product of form $(\textsf{Type}_i, \textsf{Type}_i, \textsf{Type}_i)$.\ +As for \textsc{CC-Lam} and \textsc{CC-App}, depending on whether the product type in the premises has already been translated as either explicit or erasable, the corresponding typing rules will apply, i.e. \textsc{X-Lam} and \textsc{X-App} if explicit or \textsc{E-Lam} and \textsc{E-App} if erasable.
- \textbf{Case 4: \textsc{C-Lam} and \textsc{C-App}} - - Depending on whether the product type in either sets of premises was constructed explicit or erasable, the corresponding typing rules will apply. -\end{proof} +\subsection{Example} +Suppose the following typing judgement on a universe polymorphic $\mathsf{pair}$ type in the \CC\ language. +\begin{align*} + ~ \quad & \la (t_1 : \Type_1) \explicit \la (t_2 : \Type_1) \explicit \la (x:t_1) \explicit \la (y:t_2) \explicit \la (t:\Prop) \explicit \ + & \la (f:t_1\explicit t_2\explicit t) \explicit f\ x\ y \[5pt] + & \hspace{-9pt}: (t_1 : \Type_1) \explicit (t_2 : \Type_1) \explicit (x:t_1) \explicit (y:t_2) \explicit (t:\Prop) \explicit \ + & (f:t_1\explicit t_2\explicit t) \explicit f\ x\ y +\end{align*} +The derivation by which we arrive to this typing judgement \todo
\newpage \bibliographystyle{alpha}
View it on GitLab: https://gitlab.com/monnier/typer/compare/6125b349935725e040c068a24d2c622df07...
Afficher les réponses par date