Stefan pushed to branch report/itd at Stefan / Typer

Commits: 6686fdae by Stefan Monnier at 2018-11-15T17:25:06Z -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -1222,10 +1222,10 @@ be implemented as no-ops: \end{lemma} \begin{proof} By induction on the derivation of ${e_1}\JUstepArw{e_2}$ - resp. ${\Erase{e_1}}\JEstepArw{e_2}$. The proof is tedious because it - requires a various lemmas showing for example that if - $\Erase{e_1}=\tuple{_}{_}$ the terms that were erased cannot be - arbitrary but that \kw{fold} and \kw{unfold} come in pairs. + resp. ${\Erase{e_1}}\JEstepArw{e_2}$. The proof requires various lemmas + showing for example that if $\Erase{e_1}=\tuple{_}{_}$ the terms that + were erased cannot be arbitrary but that \kw{fold} and \kw{unfold} come + in pairs. \end{proof}

\section{Equivalence} @@ -1241,7 +1241,7 @@ be implemented as no-ops: Now that we have defined a calculus which provides us with the intended run-time cost, we show that this calculus is sound and complete with respect to a more classic presentation of inductive types. We will first present -a variant of our base calculus extended with inductive types in the style +a variant of the base calculus extended with inductive types in the style of~\citet{Gimenez94}, and then show that any expression of our CUC can be compiled to this CIC, and the reverse as well.

@@ -1449,7 +1449,7 @@ compiled to this CIC, and the reverse as well.

We add inductive types following the style of \citet{Gimenez94} which separates induction into case analysis and recursive definitions, -combined with a syntactic check that the recursive calls corresponds to +combined with a syntactic check that the recursive calls correspond to a structural induction. The syntax of the base language is extended as follows: %% @@ -1466,13 +1466,13 @@ follows: \end{array} \end{displaymath} $\Tind{x}{\tau}{\vec c}$ is an inductive type of kind $\tau$ with $|\vec c|$ -constructors where $c_i$ is the type of the $i^{th}$ constructor; \ +constructors where $c_i$ is the type of the $i^{th}$ constructor; $\Tcon{i}{e}$ -is the $i^{th}$ constructor of the inductive type $e$; \ +is the $i^{th}$ constructor of the inductive type $e$; $\TIcase{\tau_r}{e}{\tau_e}{\vec b}$ performs case analysis on an object $e$ of inductive type; for an object built with the $i^{th}$ constructor, branch $b_i$ will be called, passing to it the -arguments that were passed to the constructor; \ +arguments that were passed to the constructor; and finally $\Tfix{i}{x}{\tau}{e}$ defines a recursive function which performs a structural induction on its $i^{th}$ argument. @@ -1485,8 +1485,8 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \begin{itemize} \item We omitted the obvious congruence rules for the $\JIstepArw$ relation and the termination judgment; -\item Our rules are extended to a tower of universes; -\item The typing rule of \kw{Ind} enforces predicativity; +\item Our rules are extended to a tower of universes; and the typing rule of + \kw{Ind} enforces predicativity; \item Giménez does not include the \kw{Ind} rule of $\JIpos e$; which allows us to define for example an inductive type $t$ where one of the fields has type $\id{List}~t$. Most proof assistants allow such a relaxation of the @@ -1495,10 +1495,10 @@ system differs from that of~\citet{Gimenez94} in the following aspects: fields of an object to be smaller than the object analyzed, whereas Giménez limits this to the fields which are in a \emph{recursive position}. -\end{itemize} -Giménez needs this additional restriction because his \kw{Set} universe is -impredicative, so he needs to disallow recursions such as the one hinted at -in~\cite{Coquand92}: + %% + Giménez needs this additional restriction because his \kw{Set} universe is + impredicative, so he needs to disallow infinite recursions such as the + following one, hinted at in~\cite{Coquand92}: \begin{displaymath} \MAlign{ D = \Tind{D}{\kw{Set}}{\Tsarw{(\Tarw{t}{\kw{Set}}{\Tsarw{t}{t}})}{D}}; \ @@ -1510,6 +1510,7 @@ in~\cite{Coquand92}: \id{oops} = f~d; } \end{displaymath} +\end{itemize}

\subsection{CUC to CIC}

View it on GitLab: https://gitlab.com/monnier/typer/commit/6686fdaec12436f4bd4d1eaefc45e19263e3...