Stefan pushed to branch report/itd at Stefan / Typer
Commits: d56b0626 by Stefan Monnier at 2018-10-04T20:40:21Z -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -86,6 +86,7 @@
\newcommand \Jcuc[2][\Gamma] {#1 \vdash_U #2 :} \newcommand \Jcic[2][\Gamma] {#1 \vdash_I #2 :} +\newcommand \Jconv[1] {#1 ;\simeq; }
\newcommand \MetaFunction[2] {\llbracket #2 \rrbracket_{#1}} \newcommand \Ftocic {\MetaFunction{I}} @@ -613,28 +614,16 @@ which is sound and complete.
\newcommand \Tind[3] {\kw{Ind}(#1:#2)\langle#3\rangle} \newcommand \Tcon[2] {\kw{Con}(#1,#2)} -\newcommand \Tcase[3] {{<}#1{>}\kw{Case}~#2~\kw{of}~\langle#3\rangle} +\newcommand \TIcase[4] {{<}#1{>}\kw{Case}~#2:#3~\kw{of}~\langle#4\rangle} \newcommand \Tfix[3] {\kw{Fix}_{#1}~#2:#3~=~}
\newcommand \JIcon[2][x] {#1 \vdash #2;;\kw{con}} \newcommand \JIpos[2][x] {#1 \vdash #2;;\kw{pos}} -\newcommand \Jdecreasing[3][x_f,i,x_i] {#1,#2 \vdash #3~\kw{decr}} +\newcommand \Jdecreasing[3][x_f,i,x_i] {#1,#2 \vdash #3~\kw{term}} \newcommand \BT[2] {\id{BT}\llbracket #1 \rrbracket_{#2}}
\begin{figure*} %% Syntax - \begin{displaymath} - \begin{array}{lc@{;;}c@{;;}l} - \textit{(index)} & i &\in& \mathbb{N} \ - \textit{(term)} & e,\tau &::=& - ... ~\MAlign{ - |~ \Tind{x}{\tau}{\vec e} \ - |~ \Tcon{i}{e} \ - |~ \Tcase{\tau}{e}{\vec e} \ - |~ \Tfix{i}{x}{\tau}{e} - } \ - \end{array} - \end{displaymath}
%% Typing rules \begin{mathpar} @@ -655,19 +644,20 @@ which is sound and complete. %% Actual typing rules \Infer{\Jtyper{\tau}{\Type{\ell}} \ \forall i \ - \Jtyper[\Gamma,x:\tau]{e_i}{\Type{\ell_i}} \ - \JIcon {e_i} \ + \Jtyper[\Gamma,x:\tau]{c_i}{\Type{\ell_i}} \ + \JIcon {c_i} \ \ell_i < \ell} - {\Jtyper{\Tind{x}{\tau}{\vec e}}{\tau}} + {\Jtyper{\Tind{x}{\tau}{\vec c}}{\tau}}
%% FIXME: This presentation doesn't allow `Con(0,Nat)` but requires %% substituting every `Nat` with its definition. %% Could it be that this is not needed in CUC? - \Infer{e = \Tind{x}{\tau}{\vec e} \ + \Infer{e = \Tind{x}{\tau}{\vec c} \ \Jtyper e \tau} - {\Jtyper{\Tcon{i}{e}}{\Subst{e_i}{x}{e}}} + {\Jtyper{\Tcon{i}{e}}{\Subst{c_i}{x}{e}}}
- \Infer{\Jtyper e {\tau_I~{\vec p}} \ + \Infer{\Jtyper e {\tau_e} \ + \tau_e = {\tau_I~{\vec p}} \ \tau_I = \Tind{x}{\Tmarw{z}{\tau_z}{s}}{\vec c} \ \Jtyper {\tau_r}~{\Tmarw{z}{\tau_z}{\Tsarw{\tau_I~\vec z}s}} \\ \forall i \ @@ -675,7 +665,7 @@ which is sound and complete. \Jtyper {b_i} {\Tmarw{y}{\Subst{\tau_y}{x}{\tau_I}} {\tau_r~\vec {p'}~{(\Tcon{i}{\tau_I}~\vec y)}}}} - {\Jtyper{\Tcase{\tau_r}{e}{\vec b}}{\tau_r~{\vec p}~e}} + {\Jtyper{\TIcase{\tau_r}{e}{\tau_e}{\vec b}}{\tau_r~{\vec p}~e}}
\Infer{\Jtyper \tau s \ \Jtyper[\Gamma,x:\tau] e \tau \ @@ -686,49 +676,100 @@ which is sound and complete.
%% Decreasing recursive calls \Infer{x_f \not\in \kw{fv}(e)} - {\Jdecreasing v {e}} + {\Jdecreasing \nu {e}}
- \Infer{\Jdecreasing v \tau \ \Jdecreasing v e} - {\Jdecreasing v {\Tlam x \tau e}} + \Infer{\Jdecreasing \nu \tau \ \Jdecreasing \nu e} + {\Jdecreasing \nu {\Tlam x \tau e}}
- \Infer{\Jdecreasing v \tau \ \Jdecreasing v e} - {\Jdecreasing v {\Tarw x \tau e}} + \Infer{\Jdecreasing \nu \tau \ \Jdecreasing \nu e} + {\Jdecreasing \nu {\Tarw x \tau e}}
- \Infer{\Jdecreasing v \tau \ \Jdecreasing v e} - {\Jdecreasing v {\Tfix{i'}{x}{\tau}{e}}} + \Infer{\Jdecreasing \nu \tau \ \Jdecreasing \nu e} + {\Jdecreasing \nu {\Tfix{i'}{x}{\tau}{e}}}
- \Infer{\Jdecreasing v {e_1} \ \Jdecreasing v {e_2}} - {\Jdecreasing v {\Tapp{e_1}{e_2}}} + \Infer{\Jdecreasing \nu {e_1} \ \Jdecreasing \nu {e_2}} + {\Jdecreasing \nu {\Tapp{e_1}{e_2}}}
- \Infer{\Jdecreasing v {\vec e} \ + \Infer{\Jdecreasing \nu {\vec e} \ i < |e| \ - e_i = \Tapp{x}{\vec e'} \ - x \in v} - {\Jdecreasing v {\Tapp{x_f}{\vec e}}} - - \Infer{\Jdecreasing v e \ - \Jdecreasing v {\tau_r} \ - \Jdecreasing v {\vec b}} - {\Jdecreasing v {\Tcase{\tau_r}{e}{\vec b}}} - - \Infer{\Jdecreasing v e \ - e = \Tapp{x}{\vec e'} \ - x \in v \cup { x_i } \ - ..FIXME.. \ - \Jdecreasing v {\tau_r} \ - \Jdecreasing v {\vec b}} - {\Jdecreasing v {\Tcase{\tau_r}{e}{\vec b}}} + e_i = \Tapp{x}{\vec {e'}} \ + x \in \nu} + {\Jdecreasing \nu {\Tapp{x_f}{\vec e}}} + + \Infer{\Jdecreasing \nu e \ + \Jdecreasing \nu {\tau_r} \ + \Jdecreasing \nu {\tau_e} \ + \Jdecreasing \nu {\vec b}} + {\Jdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}} + + \Infer{\Jdecreasing \nu e \ + \Jdecreasing \nu {\tau_r} \ + \Jdecreasing \nu {\tau_e} \\ + e = \Tapp{x_e}{\vec _} \ + x_e \in \nu \cup { x_i } \ + \tau_e = {\tau_I~{\vec _}} \ + \tau_I = \Tind{x_I}{_}{\vec c} \ + \Jdecreasing \nu {\vec b} \\ + \forall i \ + b_i = \Tmlam{y}{_}{e_i} \ + c_i = \Tmarw{_}{\tau_i}{_} \ + \nu' = {~ y_j ~|~ \tau_{ij} = \Tapp{x_I}{\vec _} ~} \ + \Jdecreasing {\nu \cup \nu'} {b_i}} + {\Jdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}} \end{mathpar}
%% Reduction rules \begin{mathpar} - + %% Congruence rules + \Infer{\Jconv{\tau}{\tau'} \ + |\vec c| = |\vec {c'}| \ + \forall i \ \Jconv{c_i}{c'_i}} + {\Jconv{\Tind{x}{\tau}{\vec c}}{\Tind{x}{\tau'}{\vec {c'}}}} + + \Infer{\Jconv{e}{e'}} + {\Jconv{\Tcon{i}{e}}{\Tcon{i}{e'}}} + + \Infer{\Jconv{e}{e'} \ + \Jconv{\tau}{\tau'}} + {\Jconv{\Tfix{i}{x}{\tau}{e}}{\Tfix{i}{x}{\tau'}{e'}}} + + \Infer{\Jconv{e}{e'} \ + \Jconv{\tau_r}{\tau'_r} \ + \Jconv{\tau_e}{\tau'_e} \ + |\vec b| = |\vec {b'}| \ + \forall i \ + \Jconv{b_i}{b'_i}} + {\Jconv{\TIcase{\tau_r}{e}{\tau_e}{\vec b}} + {\TIcase{\tau'_r}{e'}{\tau'_e}{\vec b'}}} + + %% Primitive reductions + FIXME!! \end{mathpar}
\caption{Inductive types} \label{fig:inductive} \end{figure*}
+We add inductive types following the presentation of \citet{Gimenez94} +which separates induction into case analysis and recursive definitions, +combined with a syntactic check that the recursive calls corresponds to +a structural induction. The syntax of the base language is extended as +follows: +%% +\begin{displaymath} + \begin{array}{lc@{;;}c@{;;}l} + \textit{(index)} & i &\in& \mathbb{N} \ + \textit{(term)} & e,b,c,\tau &::=& + ... ~\MAlign{ + |~ \Tind{x}{\tau}{\vec c} \ + |~ \Tcon{i}{e} \ + |~ \TIcase{\tau_r}{e}{\tau_e}{\vec b} \ + |~ \Tfix{i}{x}{\tau}{e} + } \ + \end{array} +\end{displaymath} + +
\subsection{CIC}
View it on GitLab: https://gitlab.com/monnier/typer/commit/d56b062666d03c3739f0d7fd305f2d1c5f61...
Afficher les réponses par date