[Git][monnier/typer][report/itd] - - Typer

14 Nov 2018


      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...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/commit/0b4b89d4b4df16c076425d12c1f2c4a173d5...
You're receiving this email because of your account on gitlab.com.



    