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