Stefan pushed to branch report/itd at Stefan / Typer
Commits: 3f11c53d by Stefan Monnier at 2018-11-16T05:07:26Z -
- - - - -
2 changed files:
- paper.tex - refs.bib
Changes:
===================================== paper.tex ===================================== @@ -112,7 +112,7 @@ %% \newcommand \Jstepr[1] {#1 \leadsto^{!*}} \newcommand \JUstepArw {\stackrel{U}{\leadsto}} \newcommand \JUstep[1] {#1 ;;\JUstepArw;; } -\newcommand \JUstepr[1] {#1 \JUstepArw{!!}^*~} +\newcommand \JUstepr[2][*] {#2 \JUstepArw{!!}^{#1}~}
%% \newcommand \MetaFunction[2] {\llbracket #2 \rrbracket_{#1}} \newcommand \MetaFunction[2] {\left\llbracket #2 \right\rrbracket_{#1}} @@ -278,7 +278,8 @@ The contributions of this article are:
\newcommand \Tind[3] {\kw{Ind}(#1:#2)\langle#3\rangle} \newcommand \Tcon[2] {\kw{Con}(#1,#2)} -\newcommand \TIcase[4] {\langle#1\rangle\kw{Case}~#2 :#3 ~\kw{of}~\langle#4\rangle} +\newcommand \TIcase[4] {\langle#1\rangle\kw{Case}~#2 %% :#3 + ~\kw{of}~\langle#4\rangle} \newcommand \Tfix[3] {\kw{Fix}_{#1}~#2:#3~=~}
In this section, we briefly present the two problems our design aims @@ -1183,13 +1184,13 @@ On the other hand, we do need to introduce a new reduction judgment $e_1 of the erased calculus are the following: %% \begin{mathpar} - \JEstep{\Tapp{(\Tlam x \tau {e_1})}{e_2}}{\Subst{e_1}{e_2}x} + \JEstep{\Tapp{(\Tlam x _ {e_1})}{e_2}}{\Subst{e_1}{e_2}x}
- \JEstep{(\tuple \Delta {\vec e}).i}{e_i} + \JEstep{(\tuple {_} {\vec e}).i}{e_i}
\JEstep {\TJ{(\Trefl{_})}{_}{x}}{x}
- \Infer{e = \tuple[l'] \Delta {\vec e}} + \Infer{e = \tuple[l'] {_} {_}} {\JEstep{ \TUcase {e} {\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} }{ @@ -1201,7 +1202,7 @@ of the erased calculus are the following: }}
%% \JEstep{\Tunfold{_}{_}{(\Tfold{_}{_}{e})}}{e} - \Infer{e_i = \tuple{_}{_} \ e = \Tmu[i]{x}{\tau}{e'}} + \Infer{e = \Tmu[i]{x}{_}{e'} \ e_i = \tuple{_}{_}} {\JEstep{\Tapp{e}{\vec e}} {\Tapp{(\Subst{e'}{e}{x})}{\vec e}}} \end{mathpar} @@ -1259,7 +1260,7 @@ compiled to this CIC, and the reverse as well. \newcommand \BT[2] {\id{BT}\llbracket #1 \rrbracket_{#2}} \newcommand \JIstepArw {\stackrel{I}{\leadsto}} \newcommand \JIstep[1] {#1 ;;\JIstepArw;; } -\newcommand \JIstepr[1] {#1 \JIstepArw{!!}^*~} +\newcommand \JIstepr[2][*] {#2 \JIstepArw{!!}^{#1}~}
\begin{figure*} %% Syntax @@ -1286,8 +1287,7 @@ compiled to this CIC, and the reverse as well. } {\Jcic{\Tind{x}{\tau}{\vec c}}{\tau}}
- \Infer{\Jcic e {\tau_e} \ - \tau_e = {\tau_I~{\vec p}} \ + \Infer{\Jcic e {\tau_I~{\vec p}} \ \tau_I = \Tind{x}{\Tmarw{z}{\tau_z}{s}}{\vec c} \ \Jcic {\tau_r}~{\Tmarw{z}{\tau_z}{\Tsarw{\tau_I~\vec z}s}} \\ \forall i. \ @@ -1485,7 +1485,7 @@ 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; and the typing rule of +\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 @@ -1523,26 +1523,42 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \newcommand \TIproj[2] {\pi_{#1}~#2}
\begin{figure} - Tags are erased, union types are converted to tagged sums, and \kw{cast} - replaced by a chunk of code \begin{displaymath} \begin{array}{l@{;=;}l} \Ftocic x & x \ - \Ftocic {\Tlam{x}{\tau}{e}} & \Tlam{x}{\Ftocic {\tau}}{\Ftocic {e}} \ + \Ftocic {\Tlam{x}{\tau_1}{e}} & \Tlam{x}{\Ftocic {\tau_1}}{\Ftocic {e}} \ \Ftocic {\Tapp{e_1}{e_2}} & \Tapp{\Ftocic {e_1}}{\Ftocic {e_2}} \ \Ftocic {\Tarw{x}{\tau_1}{\tau_2}} & \Tarw{x}{\Ftocic {\tau_1}}{\Ftocic {\tau_2}} \medskip \ \Ftocic {\Tuple \EmptyCtx} & \TIUnit \ - \Ftocic {\Tuple {x:\tau,\Delta}} & \TIPair{x}{\tau}{\Ftocic {\Tuple \Delta}} \ + \Ftocic {\Tuple {x:\tau_0,\Delta}} & \TIPair{x}{\tau_0}{\Ftocic {\Tuple \Delta}} \ \Ftocic {\tuple \Delta {\cdot}} & \TIunit \ \Ftocic {\tuple \Delta {e,\vec e}} & \TIpair e {\Ftocic {\tuple \Delta {\vec e}}}\ - \Ftocic {\Tproj e 0} & \TIproj 1 {\Ftocic {e}} \ - \Ftocic {\Tproj e i} & \TIproj 2 {\Ftocic {\Tproj e {i - 1}}} \ - \Ftocic {\Tapp{(\Tlam x {\tau} {e_1})}{\Tproj {e_2} 0}} & - \TIcase {\Tlam _ _ ?} {e_2} {?} - {\Tlam x \tau {\Tlam {x_2} _ {e_1}}} \ - \Ftocic {\Tapp{(\Tlam x {\tau} {e_1})}{\Tproj {e_2} i}} & - \TIproj 2 {\Ftocic {\Tproj e {i - 1}}} + %% Note: The translation has reduction steps that don't correspond + %% to any matching state in CUC. + \Ftocic {\Tproj e i} & + \TIproj 1 (\TIproj 2 {(\dots~{(\TIproj 2 {\Ftocic {e}})})}) \ + %% Combined proj and let-binding, used for termination checking! + \Ftocic {\Tapp{(\Tlam x {\tau_1} {e_1})}{\Tproj {e_2} 0}} & + \MAlign{ + \TIcase {\Tlam x {\tau_{e_2}} {\Subst{\tau_2}{\TIproj 1 x}{x}}} {e_2} {?} + {\Tlam x {\tau_1} {\Tlam {_} {\Ftocic{\Tuple \Delta}} {e_1}}} \ + ;;\text{where } + \MAlign{\Jtype{e_2}{\tau_{e_2}} + \text{ and }{\tau_{e_2} = \Tuple {y:\tau_0,\Delta}} \ + \Jtype[\Gamma,x:\tau_1]{e_1}{\tau_2}}} \ + \Ftocic {\Tapp{(\Tlam x {\tau_1} {e_1})}{\Tproj {e_2} i}} & + \MAlign{ + \TIcase {\Tlam _ {\tau_{e_2}} {?}} {e_2} {?} + {\Tlam {x_0} {\tau_0} {\Tlam {y} {\Ftocic{\Tuple \Delta}} {?}}} \ + ;;\text{where } + \MAlign{ + %% ¡¡FIXME: \tau_1 is not equal to the type of y.(i-1)!! + e' = \Ftocic{\Tapp{(\Tlam x {\tau_1} {e_1})} + {\Tproj {y} {(i - 1)}}} \ + \Jtype{e_2}{\tau_{e_2}} + \text{ and }{\tau_{e_2} = \Tuple {x_0:\tau_0,\Delta}} \ + \Jtype[\Gamma,x:\tau_1]{e_1}{\tau_2}}} \medskip \ \Ftocic {\id{Eq}} & \id{Eq} \ \Ftocic {\id{refl}} & \id{refl} \ @@ -1579,28 +1595,12 @@ The first question about CUC is whether this calculus is sound, meaning that if we consider it as a logic, we want to know that this logic is consistent. Rather than show it directly we do it by reducing the problem to that of the consistency of CIC. More specifically, we present a translation $\Ftocic \cdot$ -which takes any expression of CUC and translates it to an equivalent +which takes any type derivation of CUC and translates it to an equivalent expression in CIC; then we show that this translation is type preserving, and then we use this result to show that there can only be a proof of $\bot$ in -CUC if there is a proof of $\bot$ in CIC. - -If we have forall $e$ and $\tau$, -$\Jcuc e \tau$ then $\Jcic {\Ftocic e} {\Ftocic \tau}$. - -Corollary: CUC is as sound as CIC in the sense that there is an $e$ such that -$\Jcuc e \bot$ only if there's a $e'$ such that $\Jcic {e'} \bot$, because -$\Ftocic \bot = \bot$. - -\FIXME{Second take:} -%% This is much better, but we need to adjust the presentation accordingly: -%% - We can throw away some type annotations (yay!) -%% - We have to explain that while $\Ftocic\cdot$ is defined on derivations -%% we present it as if it was derived on the syntax of terms, to be -%% more concise. - -We define a translation function $\Ftocic\cdot$ which takes a derivation -$\Jcuc{e}{\tau}$ and returns an equivalent expression $e'$ in CIC. As an abuse -of notation, we will often write $\Ftocic e$ instead of $\Ftocic{\Jcuc{e}{\tau}}$. +CUC if there is a proof of $\bot$ in CIC. Figure~\ref{fig:cuc-to-cic} shows +the definition of $\Ftocic \cdot$. As an abuse of notation, we +often write $\Ftocic e$ instead of $\Ftocic{\Jcuc{e}{\tau}}$.
\begin{lemma}[Type Preserving translation] Given $\Jcuc e \tau$, we have $\Jcuc \tau s$ and @@ -1612,8 +1612,8 @@ of notation, we will often write $\Ftocic e$ instead of $\Ftocic{\Jcuc{e}{\tau}} done by induction on the derivation. It requires proving several side lemmas such as the fact that a strictly positive recursive type is translated to a strictly positive inductive type, same for terminating - recursive functions, as well as the fact that $\JUstepr{e}{e'}$ implies - $\JIstepr{\Ftocic e}{\Ftocic{e'}}$, which itself requires proving that + recursive functions, as well as the fact that $\JUstepr[]{e}{e'}$ implies + $\JIstepr[+]{\Ftocic e}{\Ftocic{e'}}$, which itself requires proving that reduction preserves types. \end{proof}
===================================== refs.bib ===================================== @@ -3,7 +3,7 @@ @techreport{Monnier19a, author = {Stefan Monnier}, institution = {Université de Montréal - DIRO}, - title = {Typer: ML boosted with type theory and Scheme}, + title = {Typer: {ML} boosted with type theory and {S}cheme}, year = {2019}, url = {https://www.iro.umontreal.ca/%5C~%7B%7Dmonnier/typer-overview- 2019.pdf},
View it on GitLab: https://gitlab.com/monnier/typer/commit/3f11c53d814be35621e2e06e05cad47fc513...
Afficher les réponses par date