Nathaniel pushed to branch bosn at Stefan / Typer

Commits: 57ed864b by nbos at 2018-08-22T22:36:04Z Restructure sections and figures; correct some awkward phrasing

- - - - -

1 changed file:

- doc/formal/typer_theory.tex

Changes:

===================================== doc/formal/typer_theory.tex ===================================== @@ -17,49 +17,24 @@

\maketitle

-\section{Introduction} -We here formalize the Typer language and prove some of its properties. The gist of the theory behind Typer is Coquand and Huet's Calculus of Constructions (CC) \cite{CC} enriched with the following features: +We here formalize the Typer language and prove some of its properties. + +\section{Typer's Type Theory} +The gist of the theory behind Typer is Coquand and Huet's Calculus of Constructions (CC) \cite{CC} enriched with the following features:

\begin{itemize} \renewcommand{\labelitemi}{$-$} \setlength\itemsep{-3pt} -\item An infinite hierarchy of type universes `a la Russell similar to the one found in Luo's Extended Calculus of Constructions (ECC) \cite{luo}, but without cumulativity; +\item An infinite hierarchy of predicative type universes inspired by Luo's Extended Calculus of Constructions (ECC) \cite{luo} without cumulativity; +\item A parallel hierarchy of impredicative universes \item Universe polymorphism allowing the parametrization of type universes; \item Erasure of propositional arguments with decidable type checking from Barras and Bernardo's variant of Miquel's Implicit Calculus of Constructions (ICC) \cite{bruno}\cite{miquel}; \item Inductive definitions as presented by Gim'enez in \cite{gimenez}. \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 (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{ - \begin{mathpar} - \ - \infer - {\ } - {\emptyctx ~} - \textsc{ (Wf-E)} - \and %-------------------- - \infer - {\Ga ~ T:s \ s \in \S \ x \notin \dv{\Ga}} - {\Ga , x:T ~} - \textsc{ (Wf-S)} - \ - \end{mathpar} - } - \caption{Typer's Well-Formed Context Rules} -\end{figure} - \subsection{Universes and Universe Polymorphism} -Each type universe $\Type\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \z ~~|~~ \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 \TypeLevel\ which itself belongs to the sort \SortL. The two first constructs correspond to the constant zero and to the successor function, respectively. Sometimes we write $\s^i$ to abbreviate the application of the successor $i$ times. We define a set $\mathbb{L}$ which is closed under those two constructs. 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 \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{figure} + \label{fig:PTS} \begin{empheq}[box=\fbox]{align*} \hspace{15mm} & \ & \ & \hspace{7mm} \ \S = { & \SortL;\ \Sortw;\ \Type\ \l} &\forall\l \in \mathbb{L} \[9pt] @@ -73,8 +48,7 @@ We have that \Sortw\ is the unique sort of all the types of universe polymorphic \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 rules, written $\R_e$, some of which will be referred as $(s_1,s_2)$ as an abbreviation for $(s_1,s_2,s_2)$. -\begin{figure}[h] +\begin{figure} \begin{empheq}[box=\fbox]{align*} \hspace{15mm} & \ & \ & \hspace{7mm} \ \R_e = { &(\SortL,\ \Type\ \l,\ \Sortw); &\forall\l \in \mathbb{L} \ @@ -85,10 +59,18 @@ Because of the impredicativity of the erasable part of Typer, we need to define \caption{Typer's Impredicative Rules} \end{figure}

-\subsection{ICC in Typer} -Typer manipulates three separate 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 inferred during elaboration, participate in type checking and are then erased before execution. +Each type universe $\Type\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \z ~~|~~ \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. +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. We write $\s^i$ to abbreviate the application of the successor $i$ times. 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 belongs to the sort \SortL. + +\Sortw\ is the unique sort of all the universe polymorphic function types. We describe the explicit part of Typer as a Pure Type System \cite{barendregt} in figure \ref{fig:PTS}. % FIXME: PDF prints 1.1 instead of 1 +Because of the erasable part of Typer allows for impredicative definitions, we define a separate set of rules $\R_e$. + +\subsection{Erasure in Typer} +Typer manipulates three separate kinds of terms to simplify the writing and execution of programs. \emph{Explicit} terms are the usual expression that are written by the user and executed. \emph{Implicit} terms are also used during execution, but Typer can 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 inferred during elaboration, provide type information during checking and are erased before execution.

-\textbf{Notation:} The notation we adopt in this document is meant to both allow for the distinction between the three kinds of terms and to evoke actual Typer source code. The traditional explicit lambda term $\la(x:A).b$ will here be written $\la(x:A)\explicit b$ and similarly the product type $\Pi(x:A).B$ will be written $(x:A)\explicit B$. The type of arrow used will convey the kind of term being defined. Thus, compound terms of our calculus will all take one of the following forms: +\textbf{Notation:} The notation we adopt in this document is meant to allow for the distinction between the three kinds of terms and also to evoke actual Typer code. The traditional explicit lambda term $\la(x:A).b$ will here be written $\la(x:A)\explicit b$ and similarly the product type $\Pi(x:A).B$ will be written $(x:A)\explicit B$. The type of arrow used will convey the kind of term being defined. Thus, compound terms of our calculus will all take one of the following forms:

\begin{center} \begin{tabular}[h]{rclll} @@ -99,7 +81,10 @@ Typer manipulates three separate kinds of terms to simplify both the writing and \end{tabular} \end{center}

-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}) in figure \ref{fig:*}. It erases domains of abstraction, erasable abstractions and erasable applications and 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. + +\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 an additional declarations with a comma (,). We write the empty context as a dot ($\cdot$). The set of declared variables in a context $\Ga$ is written $\dv{\Ga}$ and 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] \centering \fbox{\begin{minipage}{0.9\linewidth} @@ -114,13 +99,23 @@ After elaboration, implicit terms behave exactly like explicit terms so we will \caption{Extraction function $M \mapsto M^*$} \label{fig:*} \end{figure} -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. +We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure \ref{fig:*}. It erases domains of abstraction, erasable abstractions and erasable applications and turns erasable products into a propositional form. The typing rules for Typer are shown in figure \ref{fig:Typing-rules}. They are the standard rules of a Church-style lambda calculus, duplicated for both kinds of terms.

\begin{figure}[h] \ \ \ \ \fbox{ \begin{mathpar} \ \infer + {\ } + {\emptyctx ~} + \textsc{ (Wf-E)} + \and %-------------------- + \infer + {\Ga ~ T:s \ s \in \S \ x \notin \dv{\Ga}} + {\Ga , x:T ~} + \textsc{ (Wf-S)} + \and %-------------------- + \infer {\Ga ~ \ (s_1:s_2) \in \A} {\Ga ~ s_1:s_2} \textsc{ (Sort)} @@ -163,22 +158,19 @@ The typing rules for explicit and erasable terms are shown in figure \ref{fig:X- \ \end{mathpar} } - \caption{Typer's Typing Judgment Rules} - \label{fig:X-E-rules} + \caption{Typer's Typing Rules} + \label{fig:Typing-rules} \end{figure}

- There are two notable differences between explicit and erasable typing rules: \begin{enumerate} \item In the erasable product rule \textsc{E-Prod}, the set of rules is the impredicative $\R_e$ instead of $\R$ -\item In the erasable abstraction rule \textsc{E-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. +\item In the erasable abstraction rule \textsc{E-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 free terms after erasure. \end{enumerate}

- - \subsection{Inductive Definitions} -\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}|$. - +\textbf{Notation:} We abbreviate a list of terms $N_i$ as $\vec{N}$. For example, $(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 list of terms $\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 a member $i$ 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}|$. \end{definition} @@ -189,16 +181,16 @@ There are two notable differences between explicit and erasable typing rules:

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: +We extend our abstract syntax with four terms from Gim'enez's inductive definitions \cite{gimenez}: \begin{itemize} \renewcommand{\labelitemi}{$-$} \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 $\Ind(X:A) <\vec{C}>$ 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 $\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 $\Case\ M: S \text{ of } <\vec{G}>$ 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 \ref{IND-rules}. +The typing rules for inductive definitions and case analysis are presented in figure \ref{fig:IND-rules}.

\begin{figure}[h] \ \ \ \ \fbox{ @@ -329,7 +321,7 @@ Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $ \end{figure}

\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). +In this section we will show that the erasable terms of Typer allows 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). This will be demonstrated through a translation and its proof of correctness.

\subsection{Definition of \CC}

@@ -394,9 +386,9 @@ 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}, 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 : ...$$ +Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, to which we add an infinite hierarchy of predicative universes above an impredicative \Prop. Thus we have: $$\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}). +\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\ might therefore behave differently than other definitions of \CC\ (for example \cite{miquel}).

\subsection{Translation} \begin{figure}[h] @@ -442,7 +434,7 @@ The translator operator \rew{_} is defined on contexts and terms of \CC. We exp \end{align*} \end{theorem}

-Before proving the correctness of the equality, we will need the following lemmas: +Before proving the correctness of the equality, we need the following lemmas: \begin{lemma} \label{lem:S-equiv} $s \in \S_{CC} \iff \rew{s} \in \S$

View it on GitLab: https://gitlab.com/monnier/typer/commit/57ed864b2272654ddc7041f5e882ccf4b80a...