[Git][monnier/typer][bosn] Separated Case 1 of proof into two; introducing Erasable constructor
Nathaniel pushed to branch bosn at Stefan / Typer Commits: 6125b349 by nbos at 2018-07-17T17:42:40Z Separated Case 1 of proof into two; introducing Erasable constructor - - - - - 1 changed file: - doc/formal/typer_theory.tex Changes: ===================================== doc/formal/typer_theory.tex ===================================== @@ -333,37 +333,37 @@ Our definition of \CC\ is based on Luo's infinite hierarchy of universes designe \infer {\ } {\emptyctx \CCdash} - \textsc{ (Wf-E)} + \textsc{ (C-Wf-E)} \and %-------------------- \infer {\Ga \CCdash T:s \\ s \in \S_{CC} \\ x \notin \dv{\Ga}} {\Ga , x:T \CCdash} - \textsc{ (Wf-S)} + \textsc{ (C-Wf-S)} \and %-------------------- \infer {\Ga \CCdash \\ (s_1:s_2) \in \A_{CC}} {\Ga \CCdash s_1:s_2} - \textsc{ (Sort)} + \textsc{ (C-Sort)} \and %-------------------- \infer {\Ga \CCdash \\ (x:T) \in \Ga} {\Ga \CCdash x:T} - \textsc{ (Var)} + \textsc{ (C-Var)} \and %-------------------- \infer {\Ga \CCdash T:s_1 \\ \Ga, x:T \CCdash U:s_2 \\ (s_1,s_2,s_3) \in \R_{CC}} {\Ga \CCdash (x:T) \explicit U : s_3} - \textsc{ (CC-Prod)} + \textsc{ (C-Prod)} \and %-------------------- \infer {\Ga, x:T \CCdash M:U \\ \Ga \CCdash (x:T) \explicit U : s} {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U} - \textsc{ (CC-Lam)} + \textsc{ (C-Lam)} \and %-------------------- \infer {\Ga \CCdash M : (x:T) \explicit U \\ \Ga \CCdash N:T} {\Ga \CCdash M|N : U\{N/x\}} - \textsc{ (CC-App)} + \textsc{ (C-App)} \\ \end{mathpar} } @@ -378,9 +378,14 @@ Our definition of \CC\ is based on Luo's infinite hierarchy of universes designe %% add those `erased` and when we need to remove them (by `case` analysis). \textbf{Theorem:} All derivable terms in \CC\ are also derivable terms of Typer's calculus. \begin{proof}[Proof:]\ \\ - \textbf{Case 1: \textsc{Wf-E}, \textsc{Wf-S}, \textsc{Sort} and \textsc{Var}} + \textbf{Case 1: \textsc{C-Wf-E} and \textsc{C-Wf-S}} + + \textsc{Wf-E} translates trivially. To make erasure work in Typer, erasable arguments to a function must only occur in erasable positions. Erasability must thennot only be a property of abstractions and products, but of the variables which they instantiate. We thus include a type \todo + + + \textbf{Case 2: \textsc{C-Sort} and \textsc{C-Var}} - The translation is almost trivial as the four rules are unchanged between the two calculi. The only necessary translation is between the sets of sorts. We therefore have a mapping $\S_{CC} \to \S$: + A translation is necessary between the sets of sorts. We have a mapping $\S_{CC} \to \S$: \begin{align*} \textsf{Prop} &\mapsto \textsf{Type z} \\ \textsf{Type$_1$} &\mapsto \textsf{Type (s z)} \\ @@ -390,15 +395,15 @@ Our definition of \CC\ is based on Luo's infinite hierarchy of universes designe As per this mapping, all axioms of $\A_{CC}$ are analogous to instances of the axiom scheme $(\textsf{Type } \l : \textsf{Type } (\textsf{s } \l))\}~\forall\l \in \mathbb{L}$ from Typer's $\A$. - \textbf{Case 2: \textsc{CC-Prod}} + \textbf{Case 3: \textsc{C-Prod}} $\R_{CC}$ has members analogous to members of both $\R$ and $\R_e$. Specifically, the first rule scheme $(\textsf{Type}_i, \textsf{ Prop}, \textsf{ Prop}) \in R_{CC}$ translates to the rule scheme $$(\textsf{Type }\l_, \textsf{ Type z}, \textsf{ Type z}) \in \R_e ~~~~~~ \forall \l \in \mathbb{L}$$ and the second rule $(\textsf{Type}_i, \textsf{Type}_i, \textsf{Type}_i) \in R_{CC}$ is a special case of the rule scheme $$(\textsf{Type } \l_1, \textsf{ Type } \l_2, \textsf{ Type } (\l_1 \cup \l_2))\} \in \R ~~~~~~ \forall\l_1,\l_2 \in \mathbb{L}$$ - specifically, when $\l_1 = \l_2$. Thus, use of the typing rule \textsc{CC-Prod} translate to use of \textsc{X-Prod} in the case of a product of form $(\textsf{Type }\l_, \textsf{ Type z}, \textsf{ Type z})$ and \textsc{E-Prod} in the case of a product of form $(\textsf{Type}_i, \textsf{Type}_i, \textsf{Type}_i)$.\\ + specifically, when $\l_1 = \l_2$. Thus, use of the typing rule \textsc{C-Prod} translate to use of \textsc{X-Prod} in the case of a product of form $(\textsf{Type }\l_, \textsf{ Type z}, \textsf{ Type z})$ and \textsc{E-Prod} in the case of a product of form $(\textsf{Type}_i, \textsf{Type}_i, \textsf{Type}_i)$.\\ - \textbf{Case 3: \textsc{CC-Lam} and \textsc{CC-App}} + \textbf{Case 4: \textsc{C-Lam} and \textsc{C-App}} Depending on whether the product type in either sets of premises was constructed explicit or erasable, the corresponding typing rules will apply. \end{proof} View it on GitLab: https://gitlab.com/monnier/typer/commit/6125b349935725e040c068a24d2c622df07b... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/6125b349935725e040c068a24d2c622df07b... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Nathaniel