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...