Nathaniel pushed to branch bosn at Stefan / Typer

Commits: 27f86f61 by nbos at 2018-07-07T04:41:05Z Added draft file presenting the theory behind Typer plus the file's dependencies

- - - - -

3 changed files:

- + doc/formal/commands.tex - + doc/formal/typer_theory.bib - + doc/formal/typer_theory.tex

Changes:

===================================== doc/formal/commands.tex ===================================== @@ -0,0 +1,68 @@ +\renewcommand{\rmdefault}{ptm} + +%% Defined/Free variables +\newcommand{\Dom}[1]{\textsf{Dom}(#1)} +\newcommand{\dv}[1]{\textsf{DV}(#1)} +\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 }} + +% Bolds +\newcommand{\todo}{\textbf{ TODO }} + +% Caligraphics +\renewcommand{\S}{\mathcal{S}} +\newcommand{\A}{\mathcal{A}} +\newcommand{\R}{\mathcal{R}} +\newcommand{\U}{\mathcal{U}} +\newcommand{\D}{\mathcal{D}} +\newcommand{\V}{\mathcal{V}} + +%% Abbrevs +\let~\vdash +\let\Ga\Gamma +\let\La\Lambda +\let\la\lambda +\let<\langle +\let>\rangle +\let\l\ell + +% Abstractions +\newlength{\ProdSpace} +\setlength{\ProdSpace}{-2.5pt} +\newcommand{\explicit}{\hspace{\ProdSpace}\rightarrow\hspace{\ProdSpace}} +\newcommand{\implicit}{\hspace{\ProdSpace}\Rightarrow\hspace{\ProdSpace}} +\newcommand{\erasable}{\hspace{\ProdSpace}\Rrightarrow\hspace{\ProdSpace}} + +% \infer options +\mprset {sep=6mm} + +% Misc +\renewcommand{\tag}[1]{\textsc{(#1)}} + +\newcommand{\emptyctx}{% + \mathchoice{\raisebox{1pt}{$\displaystyle\cdot$}} + {\raisebox{1pt}{$\cdot$}} + {\raisebox{0.5pt}{$\scriptstyle\cdot$}} + {\raisebox{0.2pt}{$\scriptscriptstyle\cdot$}}} + +\newcommand{\ap}{\raisebox{1.7pt}{\scalebox{0.8}{$|$}}} +\newcommand{\app}{\raisebox{1.7pt}{\scalebox{0.8}{$||$}}} +\newcommand{\appp}{\raisebox{1.7pt}{\scalebox{0.8}{$|||$}}} + +\renewcommand{\u}{$\pmb{\scriptstyle\cup}\ $} +\newcommand{\CC}{\text{CC$^{\npreceq}_{\omega}$}} + +\newcommand{\SmallTitle}[1]{\vspace{3mm}\begin{center} + \bf \underline{#1} + \end{center}} + +\renewcommand{:}{\hspace{-3pt}:\hspace{-3pt}}

===================================== doc/formal/typer_theory.bib ===================================== @@ -0,0 +1,59 @@ +@inproceedings{gimenez, + title={Codifying guarded definitions with recursive schemes}, + author={Gim{'e}nez, Eduarde}, + booktitle={International Workshop on Types for Proofs and Programs}, + pages={39--59}, + year={1994}, + organization={Springer} +} +@inproceedings{bruno, + title={The implicit calculus of constructions as a programming language with dependent types}, + author={Barras, Bruno and Bernardo, Bruno}, + booktitle={International Conference on Foundations of Software Science and Computational Structures}, + pages={365--379}, + year={2008}, + organization={Springer} +} +@article{barendregt, + title={Introduction to generalized type systems}, + author={Barendregt, Henk}, + journal={Journal of functional programming}, + volume={1}, + number={2}, + pages={125--154}, + year={1991}, + publisher={Cambridge University Press} +} +@article{miquel, + title={Le Calcul des Constructions implicite: syntaxe et s{'e}mantique}, + author={Miquel, Alexandre}, + journal={These de doctorat, Universit{'e} Paris}, + volume={7}, + year={2001} +} +@article{CC, + author = {Coquand, Thierry and Huet, Gerard}, + title = {The Calculus of Constructions}, + journal = {Inf. Comput.}, + issue_date = {February/March 1988}, + volume = {76}, + number = {2-3}, + month = feb, + year = {1988}, + issn = {0890-5401}, + pages = {95--120}, + numpages = {26}, + url = {http://dx.doi.org/10.1016/0890-5401(88)90005-3%7D, + doi = {10.1016/0890-5401(88)90005-3}, + acmid = {47725}, + publisher = {Academic Press, Inc.}, + address = {Duluth, MN, USA}, +} +@inproceedings{luo, + title={ECC, an extended calculus of constructions}, + author={Luo, Zhaohui}, + booktitle={Logic in Computer Science, 1989. LICS'89, Proceedings., Fourth Annual Symposium on}, + pages={386--395}, + year={1989}, + organization={IEEE} +}

===================================== doc/formal/typer_theory.tex ===================================== @@ -0,0 +1,278 @@ +\documentclass[10pt]{article} +% \usepackage[a4paper,margin=1in,footskip=0.25in]{geometry} + +\usepackage{amsmath,amsthm,amssymb,mathtools} +\usepackage{mathpartir,mdframed,empheq} +\usepackage{parskip} + +\input{commands} +\begin{document} + +\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: + +\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 cummulativity; +\item Universe polymorphism, i.e. 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 variables in a term $T$ is written $\fv{M}$. The expression $M{N/x}$ denotes the substitution of free occurences 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 \ 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)} + \and %-------------------- + \infer + {\Ga ~ \ (x:T) \in \Ga} + {\Ga ~ x:T} + \textsc{ (Var)} + \end{mathpar} + } + \caption{Typer's context and sorts rules} +\end{figure} + + + +\subsection{Universes} +Each type universe \textsf{Type} $\l$ has an index $\l$ of the type \textsf{TypeLevel} inductively defined as: +\begin{align*} + \textsf{(TypeLevel : SortL)} := &\textsf{ TypeLevel.z} : \textsf{TypeLevel} \ + | &\textsf{ TypeLevel.s} : \textsf{TypeLevel} \to \textsf{TypeLevel} +\end{align*} + +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}: +% \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] + \A = { &(\textsf{TypeLevel} : \textsf{SortL}); \ + &(\textsf{Type } \l : \textsf{Type } (\textsf{TypeLevel.s } \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}\ + \end{empheq} + \caption{Typer's Pure Type System} +\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: + +\begin{center} + \begin{tabular}[h]{rclll} + & & $\la$-abstraction & Product type & Application \[3mm] + Explicit: & & $\la(T:T)\explicit T$ & $(T:T)\explicit T$ & $T{\ap}T$ \ + Implicit: & & $\la(T:T)\implicit T$ & $(T:T)\implicit T$ & $T{\app}T$ \ + Erasable: & & $\la(T:T)\erasable T$ & $(T:T)\erasable T$ & $T{\appp}T$ \[10pt] + \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. +\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{figure}[h] + \ \ \ \ \fbox{ + \begin{mathpar} + \ + \infer + {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2,s_3) \in \R} + {\Ga ~ (x:T) \explicit U : s_3} + \textsc{ (E-Prod)} + \and %-------------------- + \infer + {\Ga, x:T ~ M:U \ \Ga ~ (x:T) \explicit U : s} + {\Ga ~ \la(x:T) \explicit M : (x:T) \explicit U} + \textsc{ (E-Lam)} + \and %-------------------- + \infer + {\Ga ~ M : (x:T) \explicit U \ \Ga ~ N:T} + {\Ga ~ M|N : U{N/x}} + \textsc{ (E-App)} + \\ + \infer + {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2,s_2) \in \R} + {\Ga ~ (x:T) \erasable U : s_2} + \textsc{ (R-Prod)} + \and %-------------------- + \infer + {\Ga, x:T ~ M:U \ \Ga ~ (x:T) \erasable U : s \ x \notin \fv{M^*}} + {\Ga ~ \la(x:T) \erasable M : (x:T) \erasable U} + \textsc{ (R-Lam)} + \and %-------------------- + \infer + {\Ga ~ M : (x:T) \erasable U \ \Ga ~ N:T} + {\Ga ~ M|||N : U{N/x}} + \textsc{ (R-App)} + \ + \end{mathpar} + } + \caption{Typer's Explicit and Erasable typing rules} +\end{figure} + + +\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{Definition:} We say that $X$ is restricted to a \emph{strictly positive occurence} 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}|$. + +\textbf{Definition:} 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$$ + +Where $X$ is restricted to strictly positive occurences 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}|$. + +We extend our abstract syntax with four terms introduced in \cite{gimenez} to express typing rules of inductive definitions. They are: +\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 $\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, reprented as abstractions of the respective patterns of constructions. +\end{itemize} + +The typing of the individual cases $G_i$ in $\textsf{Case}\ M: S \text{ of } <\vec{G}>$ is captured with an expression $\S {C_i,I,Q,R}$ which is defined by structural induction on term $C_i$: +\begin{align*} + \S{P\to C,I,Q,R} && = && (y:P{I/X})\S{C,I,Q,(Ry)} && \text{if } P \equiv (\vec{x}:\vec{M})(X \vec{N}) \ + \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. + +\begin{figure}[h] + \ \ \ \ \fbox{ + \begin{mathpar} + \infer + {\text{Where } I = \Ind(X:\text{Type }\l_A) <\vec{C}> \text{ and } i \in |\vec{C}|.\hspace{100mm}} + {} + \and + \infer + {\Ga ~ \text{Type } \l_{A}: \bigcup_{i\in|\vec{C}|} \text{Type } \l_i \ + \Ga, X:\text{Type } \l_A \stackrel{\forall i \in |\vec{C}|}{~} C_i:\text{Type } \l_i} + {\Ga ~ I : \text{Type } \l_A} + \textsc{ (Ind)} + \and %-------------------- + \infer + {\Ga ~ I:A} + {\Ga ~ \Constr(i,I) : C_i {I / X}} + \textsc{ (Constr)} + \and %-------------------- + \infer + { \Ga ~ Q : (\vec{z}:\vec{Z})(I\ \vec{z}) \to \text{Type } \l_A \ + \Ga ~ M:(I\ \vec{P}) \ + \Ga \stackrel{\forall i \in |\vec{G}|}{~} G_i:\S {C_i,Q,\Constr(i,I)}} + {\Ga ~ \Case\ M:(I\ \vec{P}) \text{ of } <\vec{G}> : (Q \vec{P} M)} + \textsc{ (Case)} + \end{mathpar} + } + \caption{Typer's Inductive and Case typing rules} +\end{figure} + +\subsection{Fixpoint Operator} + +Recursion is specified through the use of a recursive operator \Letrec \todo + +\begin{mathpar} + \infer + { \Ga ~ M:T \ + \Ga, x:=M:T ~ N : U} + {\Ga ~ \Let (x:T) = M \In N : U {T / x}} + \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 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$: +\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*} + +\subsection{Conversion Rules} +Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $\cong$. [Expand \todo] + +\begin{figure}[h] + \ \ \ \ \fbox{ + \begin{mathpar} + \infer + {A \cong A' \ |\vec{C}| = |\vec{C'}| \ C_i \stackrel{\forall i \in |\vec{C}|}{\cong} C_i'} + {\Ind (X:A)<\vec{C}> \cong \Ind (X:A')<\vec{C'}>} + \and %-------------------- + \infer + {I \cong I'} + {\Constr(i,I) \cong \Constr(i,I')} + \and %-------------------- + \infer + {M \cong M' \ S \cong S' \ |\vec{G}| = |\vec{G'}| \ + G_i \stackrel{\forall i \in |\vec{C}|}{\cong} G_i'} + {\Case\ M :S \text{ of } <\vec{G}> \cong \Case\ M' :S' \text{ of } <\vec{G'}>} + \and %-------------------- + \infer + {B \cong B' \ N \cong N'} + {\Letrec\ ? \todo} + \end{mathpar} + } + \caption{Typer's conversion rules} +\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. + +\subsection{Definition of \CC} +\begin{figure}[h] + \begin{empheq}[box=\fbox]{align*} + \ + \S = { & \textsf{Prop}; \textsf{ Type}_i} &\forall i > 0 \[9pt] + \A = { &(\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 \ + &(\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} +\bibliography{typer_theory} +\end{document} \ No newline at end of file

View it on GitLab: https://gitlab.com/monnier/typer/commit/27f86f6180f121dbf24c8ccce5b0e05b3023...