Stefan pushed to branch report/itd at Stefan / Typer
Commits: 0b4b89d4 by Stefan Monnier at 2018-11-14T23:22:18Z -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -865,25 +865,19 @@ the explicit equality witnesses can be used to get the same effect.
\JUstep{\TUcast{\tau}{\tau}e}{e}
- \Infer{e = \TUcast {\tau}{\tau_e} e' \ - e' = {\tuple \Delta {\vec e}} \ - \JOrder {\tau_e}{\tau_l}{\tau_d}} - {\JUstep{ - \TUcase {e} {\tau_e} - {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} - }{ - \Subst{e_\Ttagvar}{\id{refl}~{\tau_e}~e, \TUcast {\tau}{\tau_l} e'}{x_\equiv,x} - }} - \Infer{e = \TUcast {\tau}{\tau_e} e' \ e' = {\tuple[l'] \Delta {\vec e}} \ - l \not= l' \ \JOrder {\tau_e}{\tau_l}{\tau_d}} {\JUstep{ \TUcase {e}{\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} }{ - \Subst{e_d}{\id{refl}~{\tau_e}~e,\TUcast {\tau}{\tau_d} {e'}}{y_\equiv,y} + \left{\begin{array}[c]{l@{;;}l} + \Subst{e_d}{\Trefl{e},\TUcast {\tau}{\tau_d} {e'}}{y_\equiv,y} & + \text{if }l=l' \ + \Subst{e_\Ttagvar}{\Trefl{e}, \TUcast {\tau}{\tau_l} e'}{x_\equiv,x} & + \text{otherwise} + \end{array}\right. }} %% \end{array} \end{mathpar} @@ -1157,7 +1151,7 @@ The intention of our calculus is for \kw{cast}, \kw{fold}, and \kw{unfold} to have no run-time cost. In this section, we show that it is indeed the case, by defining an erasure function and showing that the evaluation and the erasure commute. - +%% The erasure function $\Erase{(\cdot)}$ is defined recursively on the syntax of terms in a straightforward manner: %% @@ -1180,7 +1174,7 @@ terms in a straightforward manner: \end{array} \end{displaymath} The $\cdots$ stand for all the remaining constructs where the function simply -recurses in the obvious way on all subterms. We do not need to introduce +recurses in the obvious way on all subterms. We do not introduce a new syntax for erased terms because they simply use a subset of the syntax of the non-erased terms. %% @@ -1191,32 +1185,22 @@ of the erased calculus are the following: \begin{mathpar} \JEstep{\Tapp{(\Tlam x \tau {e_1})}{e_2}}{\Subst{e_1}{e_2}x}
- \begin{array}{c} - \JEstep{ - \TUcase {(\tuple \Delta {\vec e})} {\tau_e} - {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} \ - }{ - \Subst{e_\Ttagvar} - {\id{refl},(\tuple \Delta {\vec e})} - {x_\equiv,x} - } - \end{array} - \JEstep{(\tuple \Delta {\vec e}).i}{e_i}
- \begin{array}{c} - \JEstep{ - \TUcase {(\tuple[l'] \Delta {\vec e})}{\tau_e} - {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} \ - }{ - \Subst{e_d} - {\id{refl},(\tuple[l'] \Delta {\vec e})} - {y_\equiv,y} - } - \end{array} - - \JEstep {J~_~_~_~_~_~(\id{refl}~_~_)~x}x + \JEstep {\TJ{(\Trefl{_})}{_}{x}}{x} + + \Infer{e = \tuple[l'] \Delta {\vec e}} + {\JEstep{ + \TUcase {e} {\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} + }{ + \left{\begin{array}[c]{l@{;;}l} + \Subst{e_\Ttagvar}{\Trefl{e},e}{x_\equiv,x} & + \text{if }l=l' \ + \Subst{e_d}{\Trefl{e},e}{y_\equiv,y} & \text{otherwise} + \end{array}\right. + }}
+ %% \JEstep{\Tunfold{_}{_}{(\Tfold{_}{_}{e})}}{e} \Infer{e_i = \tuple{_}{_} \ e = \Tmu[i]{x}{\tau}{e'}} {\JEstep{\Tapp{e}{\vec e}} {\Tapp{(\Subst{e'}{e}{x})}{\vec e}}} @@ -1228,17 +1212,20 @@ be implemented as no-ops: %% \begin{lemma}[Erasure] \label{lem:erasure} - Assuming $ \Jcuc e \tau$, we have: + Assuming $ \Jcuc {e_1} \tau$, we have: \begin{itemize} - \item If $e \JUstepArw {e_1}$ then either ${\Erase e} = {\Erase - {e_1}}$ or ${\Erase e}\JEstepArw{\Erase {e_1}}$. - \item If ${\Erase e}\JEstepArw{e_2}$ then there exists an $e_3$ such that - $\Erase{e_3} = e_2$ and $\JUstepr e {e_3}$. + \item If ${e_1}\JUstepArw{e_2}$ then either ${\Erase{e_1}}={\Erase{e_2}}$ + or ${\Erase{e_1}}\JEstepArw{\Erase{e_2}}$. + \item If ${\Erase{e_1}}\JEstepArw{e_2}$ then there exists an $e_3$ such + that $\Erase{e_3}=e_2$ and $\JUstepr{e_1}{e_3}$. \end{itemize} \end{lemma} \begin{proof} - The first part is proved by induction on the derivation of $e \JUstepArw - {e_1}$, + 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. \end{proof}
\section{Equivalence} @@ -1500,9 +1487,9 @@ system differs from that of~\citet{Gimenez94} in the following aspects: and the termination judgment; \item Our rules are extended to a tower of universes; \item The typing rule of \kw{Ind} enforces predicativity; -\item Giménez does not include the \kw{Ind} rule of $\JIpos e$; which allows 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 +\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 positivity requirement; \item The termination check on \kw{Case} is simpler in that it considers all fields of an object to be smaller than the object analyzed, whereas
View it on GitLab: https://gitlab.com/monnier/typer/commit/0b4b89d4b4df16c076425d12c1f2c4a173d5...