Nathaniel pushed to branch bosn at Stefan / Typer

Commits: 26b5c9c8 by nbos at 2018-07-27T02:27:37Z Cleaned text; fixed translation to account for new rules of CCw

- - - - - 25024193 by nbos at 2018-07-30T08:11:16Z New commands; removed unecesary math layer in sans keywords

- - - - - 618d6ae9 by nbos at 2018-07-30T08:15:13Z Restructured whole proof of extention of CCω

- - - - - b2fdff75 by nbos at 2018-07-30T09:59:21Z Added room for special case E-Lam

- - - - -

2 changed files:

- doc/formal/commands.tex - doc/formal/typer_theory.tex

Changes:

===================================== doc/formal/commands.tex ===================================== @@ -6,20 +6,24 @@ \newcommand{\fv}[1]{\textsf{FV}(#1)}

%% Sans -\newcommand{\Ind}{\ensuremath{\mathsf{Ind}}} -\newcommand{\Constr}{\ensuremath{\mathsf{Constr}}} -\newcommand{\Case}{\ensuremath{\mathsf{Case}}} -\newcommand{\Elim}{\ensuremath{\mathsf{Elim}}} -\newcommand{\Fix}{\ensuremath{\mathsf{Fix}}} -\newcommand{\Letrec}{\ensuremath{\mathsf{Letrec}}} -\newcommand{\Let}{\ensuremath{\mathsf{Let}}} -\newcommand{\In}{\ensuremath{\mathsf{in}}} - -\newcommand{\Prop}{\ensuremath{\mathsf{Prop}}} -\newcommand{\Type}{\ensuremath{\mathsf{Type}}} -\newcommand{\TypeLevel}{\ensuremath{\mathsf{TypeLevel}}} +\newcommand{\Ind}{\textsf{Ind}} +\newcommand{\Constr}{\textsf{Constr}} +\newcommand{\Case}{\textsf{Case}} +\newcommand{\Elim}{\textsf{Elim}} +\newcommand{\Fix}{\textsf{Fix}} +\newcommand{\Letrec}{\textsf{Letrec}} +\newcommand{\Let}{\textsf{Let}} +\newcommand{\In}{\textsf{in}} + +\newcommand{\Prop}{\textsf{Prop}} +\newcommand{\Type}{\textsf{Type}} +\newcommand{\TypeLevel}{\textsf{TypeLevel}} +\newcommand{\SortL}{\textsf{SortL}} +\newcommand{\Sort}{\textsf{Sort}} +\newcommand{\z}{\textsf{z}} +\newcommand{\s}{\textsf{s}} + \newcommand{\Sortw}{\ensuremath{\mathsf{Sort}_\omega}} -\newcommand{\SortL}{\ensuremath{\mathsf{SortL}}}

% Bolds \newcommand{\todo}{\textbf{ TODO }} @@ -72,5 +76,8 @@ \end{center}}

\renewcommand{:}{\hspace{-3pt}:\hspace{-3pt}} +\newcommand{\nottype}{/\hspace{-7pt}:} +\newcommand{\rew}[1]{\ensuremath{\llbracket #1 \rrbracket}}

-\newcommand{\CCdash}{\vdash_{\hspace{-2pt}_{CC}}} \ No newline at end of file +\newcommand{\CCdash}{\vdash_{\hspace{-2pt}_{CC}}} +\newcommand{\Tdash}{\vdash_{\hspace{-2pt}_{T}}} \ No newline at end of file

===================================== doc/formal/typer_theory.tex ===================================== @@ -1,7 +1,7 @@ \documentclass[10pt]{article} % \usepackage[a4paper,margin=1in,footskip=0.25in]{geometry}

-\usepackage{amsmath,amsthm,amssymb,mathtools} +\usepackage{amsmath,amsthm,amssymb,mathtools,stmaryrd} \usepackage{mathpartir,mdframed,empheq} \usepackage{parskip,authblk}

@@ -43,7 +43,7 @@ We here formalize the Typer language and prove some of its properties. The gist \end{figure}

\subsection{Universes and Universe Polymorphism} -Each type universe $\mathsf{Type}\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \mathsf{z} ~~|~~ \mathsf{s}\ \l ~~|~~ \l_1 \cup \l_2 ~~|~~ l$$ +Each type universe $\Type\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \mathsf{z} ~~|~~ \mathsf{s}\ \l ~~|~~ \l_1 \cup \l_2 ~~|~~ l$$ %% FIXME: We'll need somewhere to clarify that those `l`s have to be present %% in the Γ environment with type TypeLevel. All type levels $\l$ inhabit the type \TypeLevel\ which itself belongs to the sort \SortL. The two first constructs correspond to the constant zero and to the successor function, respectively. We define a set $\mathbb{L}$ which is closed under those two constructs and thus contains a type level $\l \in \mathbb{L}$ for every conventional natural number $n \in \mathbb{N}$. The operator $\cup$ returns the maximum of two type levels. The construct $l$ stands for a \emph{level variable} which will occur in universe polymorphic definitions. @@ -53,12 +53,12 @@ We have that \Sortw\ is the unique sort of all the types of universe polymorphic \begin{figure}[h] \begin{empheq}[box=\fbox]{align*} \hspace{15mm} & \ & \ & \hspace{7mm} \ - \S = { & \mathsf{SortL};\ \mathsf{Sort}_\omega;\ \mathsf{Type } \l} &\forall\l \in \mathbb{L} \[9pt] - \A = { &(\mathsf{TypeLevel} : \mathsf{SortL}); \ - &(\mathsf{Type}\ \l : \mathsf{Type}\ (\mathsf{s}\ \l))} &\forall\l \in \mathbb{L} \[9pt] - \R = { &(\mathsf{SortL},\ \mathsf{Type}\ \l,\ \mathsf{Sort}_\omega); &\forall\l \in \mathbb{L} \ - &(\mathsf{SortL},\ \mathsf{Sort}_\omega,\ \mathsf{Sort}_\omega); \ - &(\mathsf{Type}\ \l_1,\ \mathsf{Type}\ \l_2,\ \mathsf{Type}\ (\l_1 \cup \l_2))} &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] + \S = { & \SortL;\ \Sortw;\ \Type\ \l} &\forall\l \in \mathbb{L} \[9pt] + \A = { &(\TypeLevel : \SortL); \ + &(\Type\ \l : \Type\ (\mathsf{s}\ \l))} &\forall\l \in \mathbb{L} \[9pt] + \R = { &(\SortL,\ \Type\ \l,\ \Sortw); &\forall\l \in \mathbb{L} \ + &(\SortL,\ \Sortw,\ \Sortw); \ + &(\Type\ \l_1,\ \Type\ \l_2,\ \Type\ (\l_1 \cup \l_2))} &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] \end{empheq} \vspace{-5mm} \caption{Typer's Pure Type System} @@ -68,9 +68,9 @@ Because of the impredicativity of the erasable part of Typer, we need to define \begin{figure}[h] \begin{empheq}[box=\fbox]{align*} \hspace{15mm} & \ & \ & \hspace{7mm} \ - \R_e = { &(\mathsf{SortL},\ \mathsf{Type}\ \l,\ \mathsf{Sort}_\omega); &\forall\l \in \mathbb{L} \ - &(\mathsf{SortL},\ \mathsf{Sort}_\omega,\ \mathsf{Sort}_\omega); \ - &(\mathsf{Type}\ \l_1,\ \mathsf{Type}\ \l_2,\ \mathsf{Type}\ \l_2) } &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] + \R_e = { &(\SortL,\ \Type\ \l,\ \Sortw); &\forall\l \in \mathbb{L} \ + &(\SortL,\ \Sortw,\ \Sortw); \ + &(\Type\ \l_1,\ \Type\ \l_2,\ \Type\ \l_2) } &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] \end{empheq} \vspace{-5mm} \caption{Typer's Impredicative Rules} @@ -176,7 +176,7 @@ We extend our abstract syntax with four terms introduced in \cite{gimenez} to ex \setlength\itemsep{-3pt} \item $\Ind(X:A) <\vec{C}>$ which is an inductively defined type recursively bound to $X$. $\vec{C}$ is the list of constructor signatures which must be a \emph{form of constructor} w.r.t. $X$. \item $\Constr(i:I)$ stands for the $i$th constructor of an inductive type $I$. -\item $\mathsf{Case}\ M: S \text{ of } <\vec{G}>$ which is the function by case analysis on the expression $M$ of type $S$ and where $<\vec{G}>$ is the list of cases, represented as abstractions of the respective patterns of constructions. +\item $\Case\ M: S \text{ of } <\vec{G}>$ which is the function by case analysis on the expression $M$ of type $S$ and where $<\vec{G}>$ is the list of cases, represented as abstractions of the respective patterns of constructions. \end{itemize}

The typing rules for inductive definitions and case analysis are presented in Figure X. @@ -215,9 +215,9 @@ The typing rules for inductive definitions and case analysis are presented in Fi %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq_refl : ((x : ?t) ≡> Eq x x); %% Eq_cast : (x : ?t) ≡> (y : ?t) - %% ≡> (p : Eq x y) - %% ≡> (f : ?t -> ?t') - %% ≡> f x -> f y; + %% ≡> (p : Eq x y) + %% ≡> (f : ?t -> ?t') + %% ≡> f x -> f y; %% %% At run-time `Eq_cast` will be a no-op (i.e. `Eq_cast x` will reduce %% to `x`), but there is no corresponding normalization rule applied @@ -244,7 +244,7 @@ The typing rules for inductive definitions and case analysis are presented in Fi \Ga \stackrel{\forall i \in |\vec{G}|}{~} G_i:Q} %% FIXME: Similarly, here, the return type is just Q with no `\vec{P}` %% nor `M` argument. - {\Ga ~ \Case\ M:(I\ \vec{P}) \text{ of } <\vec{G}> : (Q \vec{P} M)} + {\Ga ~ \Case\ M:(I\ \vec{P}) \text{ of } <\vec{G}> : Q} \textsc{ (Case)} \end{mathpar} } @@ -305,7 +305,7 @@ Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $ \caption{Typer's Conversion Rules} \end{figure}

-\section{Relative Expressivity to the Calculus of Constructions} +\section{Typer as an Extention of a Calculus of Constructions} In this section we will prove that the erasable terms of Typer allow for a representation of all typing derivations from a Calculus of Constructions with an impredicative $\mathsf{Prop}$ and an infinite hierarchy of predicative universes (\CC).

\subsection{Definition of \CC} @@ -368,38 +368,249 @@ In this section we will prove that the erasable terms of Typer allow for a repre \caption{\CC's Typing Rules} \end{figure}

-Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, but with an added infinite hierarchy of universes above the impredicative $\mathsf{Prop}$. They are arranged in the series: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4...$$ +Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, but with an added infinite hierarchy of universes above an impredicative \Prop. They are arranged in the series: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4 : ...$$

\CC's PTS definition is shown in Figure X. The typing rules for \CC\ are shown in Figure X. The structure of the PTS is derived from Luo's own extention of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, (\Type_i\cup\Type_j))$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). Our definition of \CC\ will therefore behave differently than, for example, Miquel's definition of \CC\ \cite{miquel}. \subsection{Translation} - By induction on typing derivation steps. - \textsc{CC-Wf-E} and \textsc{CC-Var} both directly translate to \textsc{Wf-E} and \textsc{Var} respectively since they introduce nothing new. Because \textsc{CC-Sort} and \textsc{CC-Wf-S} call upon $\A_{CC}$ and $\S_{CC}$, we make a mapping between the universe hierarchies $\S_{CC} \to \S$: - \begin{align*} - \mathsf{Prop} ~~~ &\mapsto ~~~ \mathsf{Type\ z} \ - \mathsf{Type_1} ~~~ &\mapsto ~~~ \mathsf{Type\ (s\ z)} \ - \mathsf{Type_2} ~~~ &\mapsto ~~~ \mathsf{Type\ (s\ (s\ z))} \ - \vdots~~~~~ ~~~ &\mapsto ~~~ ~~~~~~~\vdots - \end{align*} +We set up a correspondance between \CC's and Typer's PTS structures such to allow for the translation of set theoric judgements found in typing rules. We first define the translation between universes $\rew{\ } : \S_{CC} \to \S$: +\begin{align*} + \rew{\Prop} ~~~ &= ~~~ \Type\ \mathsf{z} \ + \rew{\Type_1} ~~~ &= ~~~ \Type\ \mathsf{(s\ z)} \ + \rew{\Type_2} ~~~ &= ~~~ \Type\ \mathsf{(s\ (s\ z))} \ + \vdots~~~~~ ~~~ &= ~~~ ~~~~~~~\vdots +\end{align*}

- And axioms of $\A_{CC}$ become axioms of $\A$ by the translation of respective sorts, e.g. $\mathsf{(Prop : Type_1)}$ becomes $\mathsf{(Type\ z : Type\ (s\ z))}$. +Axioms of $\A_{CC}$ translate to axioms of $\A$ by the translation of respective sorts, e.g. $\rew{(\Prop : \Type_1)} = (\rew{\Prop} : \rew{\Type_1}) = (\Type\ \mathsf{z} : \Type\ \mathsf{(s\ z)})$. We note that the mapping of axioms is injective because $\A$ has an axiom scheme structurally identical to $\A_{CC}$'s.

- The typing rule \textsc{CC-Prod} calls upon the set of product rules $\R_{CC}$ which is analogous to both $\R$ and $\R_e$ at the same time. In particular, the first product rule scheme $$(\mathsf{Type}_i, \mathsf{Prop}, \mathsf{Prop}) \in R_{CC}$$ translates to - $$(\mathsf{Type}\ \l_, \mathsf{Type\ z}, \mathsf{Type\ z}) \in \R_e ~~~~~~ \forall \l \in \mathbb{L}$$ - and the second product rule scheme $$(\mathsf{Type}_i, \mathsf{Type}_i, \mathsf{Type}_i) \in R_{CC}$$ is a special case of - $$(\mathsf{Type}\ \l_1, \mathsf{Type}\ \l_2, \mathsf{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} when a rule is of form $(\mathsf{Type}_i, \mathsf{Type}_i, \mathsf{Type}_i)$ and the resulting dependent product in Typer is explicit. \textsc{CC-Prod} translates to \textsc{E-Prod} when of form $(\Type_i, \Prop, \Prop)$.\ +Finally, the translation of a rules in $\R_{CC}$ will translate to rules either in $\R$ or $\R_e$, depending on whether they are predicative or impredicative. For example, consider the translation of the predicative rule +\begin{align*} +\rew{(\Prop,\Type_1,\Type_1)} &= (\rew{\Prop},\rew{\Type_1},\rew{\Type_1}) \ + &= (\Type\ \z,\Type\ (\s\ \z),\Type\ (\s\ \z)) \in \R +\end{align*}

-As for \textsc{CC-Lam} and \textsc{CC-App}, depending on whether the product type in the premises has already been translated as either explicit or erasable, the corresponding typing rules will apply, i.e. \textsc{X-Lam} and \textsc{X-App} if explicit or \textsc{E-Lam} and \textsc{E-App} if erasable. +and conversly, the translation of the impredicative rule +\begin{align*} +\rew{(\Type_1,\Prop,\Prop)} &= (\rew{\Type_1},\rew{\Prop},\rew{\Prop}) \ + &= (\Type\ (\s\ \z),\Type\ \z,\Type\ \z) \in \R_e. +\end{align*} +In general, if a product rule of \CC\ has a domain of higher sort than its range, i.e. it is impredicative, then it can only be of form $(\Type_i,\Prop,\Prop)$. In all other cases, i.e. the predicative rules $(\Prop, \Type_i, \Type_i)$ and $(\Type_i, \Type_j, (\Type_i \cup \Type_j))$, the sort of the product rule will be $s_3 = (s_1 \cup s_2)$.

-\subsection{Example} -Suppose the following typing judgement on a universe polymorphic $\mathsf{pair}$ type in the \CC\ language. +Thus, the translation of set theoric propositions is the following: \begin{align*} - ~ \quad & \la (t_1 : \Type_1) \explicit \la (t_2 : \Type_1) \explicit \la (x:t_1) \explicit \la (y:t_2) \explicit \la (t:\Prop) \explicit \ - & \la (f:t_1\explicit t_2\explicit t) \explicit f\ x\ y \[5pt] - & \hspace{-9pt}: (t_1 : \Type_1) \explicit (t_2 : \Type_1) \explicit (x:t_1) \explicit (y:t_2) \explicit (t:\Prop) \explicit \ - & (f:t_1\explicit t_2\explicit t) \explicit f\ x\ y + \rew{s \in \S_{CC}} &\leadsto\ \rew{s} \in \S \ + \rew{(s_1:s_2) \in \A_{CC}} &\leadsto\ (\rew{s_1}:\rew{s_2}) \in \A \ + \rew{(s_1,s_2,s_3) \in \R_{CC}} &\leadsto\ + \begin{cases} + (\rew{s_1},\rew{\Prop},\rew{\Prop}) \in \R_e &\text{if $s_1 \neq \Prop$}\[-4pt] + & \text{and $s_2 = \Prop$}\ + (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R &\text{otherwise} + \end{cases} \end{align*} -The derivation by which we arrive to this typing judgement \todo + +We define the translation on context recursively: +\begin{align*} + \rew{\cdot} &\leadsto\ \cdot \ + \rew{\Ga, x:e} &\leadsto\ \rew{\Ga}, x:\rew{e} +\end{align*} + +The translation on terms is the one which maintains the provability of translated judgements: +\begin{align} + \Ga \CCdash & ~~ \Rightarrow ~~ \rew{\Ga} ~ \ + \Ga \CCdash e:\tau & ~~ \Rightarrow ~~ \rew{\Ga} ~ \rew{e}:\rew{\tau} +\end{align} + +We proceed by induction on typing derivation to show that each valid derivation of \CC\ translates to a valid derivation in the Typer system. For most typing rules, the proof is straightforward: we assume the translated premises by the induction hypothesis and show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules. + +\textbf{Case \textsc{CC-Wf-E}:} +\begin{mathpar} + \infer + {\ } + {\emptyctx \CCdash} +\end{mathpar} +The translation is immediately true under Typer by rule \textsc{Wf-E}. +\begin{mathpar} + \infer + {\ } + {\rew{\cdot} ~} + ~~~ \leadsto ~~~ + \infer + {\ } + {\cdot ~} + \tag{Wf-E} +\end{mathpar} + +\textbf{Case \textsc{CC-Wf-S}:} +\begin{mathpar} + \infer + {\Ga \CCdash T:s \ s \in \S_{CC} \ x \notin \dv{\Ga}} + {\Ga , x:T \CCdash} +\end{mathpar} +By the induction hypothesis we can assume +\begin{mathpar} + \infer + {\rew{\Ga} ~ \rew{T}:\rew{s} \ \rew{s} \in \S \ x \notin \dv{\rew{\Ga}}} + {\ } +\end{mathpar} +which allows us to infer the translation of the conclusion by rule +\begin{mathpar} + \infer + {\rew{\Ga} ~ \rew{T}:\rew{s} \ \rew{s} \in \S \ x \notin \dv{\rew{\Ga}}} + {\rew{\Ga} , x:\rew{T} ~} + \tag{WF-S} +\end{mathpar} + +\textbf{Case \textsc{CC-Sort}:}\ +\begin{mathpar} + \infer + {\Ga \CCdash \ (s_1:s_2) \in \A_{CC}} + {\Ga \CCdash s_1:s_2} +\end{mathpar} +By the induction hypothesis we can assume +\begin{mathpar} + \infer + {\rew{\Ga} ~ \ (\rew{s_1}:\rew{s_2}) \in \A} + {\ } +\end{mathpar} +and reach the translation of the conclusion by rule +\begin{mathpar} + \infer + {\rew{\Ga} ~ \ (\rew{s_1}:\rew{s_2}) \in \A} + {\rew{\Ga} ~ \rew{s_1}:\rew{s_2}} + \tag{Sort} +\end{mathpar} + +\textbf{Case \textsc{CC-Var}:}\ +\begin{mathpar} + \infer + {\Ga \CCdash \ (x:T) \in \Ga} + {\Ga \CCdash x:T} +\end{mathpar} +By the induction hypothesis we can assume +\begin{mathpar} + \infer + {\rew{\Ga} ~ \ (x:\rew{T}) \in \rew{\Ga}} + {\ } +\end{mathpar} +and reach the translation of the conclusion by rule +\begin{mathpar} + \infer + {\rew{\Ga} ~ \ (x:\rew{T}) \in \rew{\Ga}} + {\rew{\Ga} ~ x:\rew{T}} + \tag{Var} +\end{mathpar} + +\textbf{Case \textsc{CC-Prod}:}\ +\begin{mathpar} + \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} +\end{mathpar} +By the induction hypothesis, there are two subcases to consider---a predicative and an impredicative one: + +\underline{Predicative:}\ +We have the assumptions +\begin{mathpar} + \infer + {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{s_2} \ (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R} + {\ } +\end{mathpar} +from which we can conclude +\begin{mathpar} + \infer + {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{s_2} \ (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R} + {\rew{\Ga} ~ (x:\rew{T}) \explicit \rew{U} : \rew{s_3}} + \tag{X-Prod} +\end{mathpar} + +\underline{Impredicative:}\ +We have the assumptions +\begin{mathpar} + \infer + {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{\Prop} \ (\rew{s_1},\rew{\Prop},\rew{\Prop}) \in \R_e} + {\ } +\end{mathpar} +from which we can conlcude +\begin{mathpar} + \infer + {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{\Prop} \ (\rew{s_1},\rew{\Prop},\rew{\Prop}) \in \R_e} + {\rew{\Ga} ~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop}} + \tag{E-Prod} +\end{mathpar} +Thus we have that +\begin{align} + \rew{(x:T)\explicit U} \leadsto + \begin{cases} + (x:\rew{T})\erasable \rew{U} & \text{if $(U:\Prop)$ and $\neg(T:\Prop)$} \ + (x:\rew{T})\explicit \rew{U} & \text{otherwise} + \end{cases} +\end{align} + +\textbf{Case \textsc{CC-App}:}\ +\begin{mathpar} + \infer + {\Ga \CCdash M : (x:T) \explicit U \ \Ga \CCdash N:T} + {\Ga \CCdash M|N : U{N/x}} +\end{mathpar} +By the induction hypothesis we can assume +\begin{mathpar} + \infer + {\rew{\Ga} ~ \rew{M} : \rew{(x:T) \explicit U} \ \rew{\Ga} ~ \rew{N}:\rew{T}} + {\ } +\end{mathpar} +And we again have two subcases to consider for the translation $\rew{(x:T) \explicit U}$ (see (3)): + +\underline{Predicative:}\ +\begin{mathpar} + \infer + {\rew{\Ga} ~ \rew{M} : (x:\rew{T}) \explicit \rew{U} \ \rew{\Ga} ~ \rew{N}:\rew{T}} + {\rew{\Ga} ~ \rew{M}|\rew{N} : \rew{U}{\rew{N}/x}} + \tag{X-App} +\end{mathpar} +\underline{Impredicative:}\ +\begin{mathpar} + \infer + {\rew{\Ga} ~ \rew{M} : (x:\rew{T}) \erasable \rew{U} \ \rew{\Ga} ~ \rew{N}:\rew{T}} + {\rew{\Ga} ~ \rew{M}|||\rew{N} : \rew{U}{\rew{N}/x}} + \tag{E-App} +\end{mathpar} + +\textbf{Case \textsc{CC-Lam}:}\ +\begin{mathpar} + \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} +\end{mathpar} +By the induction hypothesis we can assume +\begin{mathpar} + \infer + {\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U} \ \rew{\Ga} ~ \rew{(x:T) \explicit U} : \rew{s}} + {\ } +\end{mathpar} +And by (3), we have two subcases to consider for the translation \rew{(x:T) \explicit U}: + +\underline{Predicative:}\ +The predicative product type translates to an explicit product type $(x:\rew{T}) \explicit \rew{U}$ and we apply the explicit \textsc{X-Lam} typing rule to derive the typing of the explicit lambda abstraction. +\begin{mathpar} + \infer + {\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U} \ \rew{\Ga} ~ (x:\rew{T}) \explicit \rew{U} : \rew{s}} + {\rew{\Ga} ~ \la(x:\rew{T}) \explicit \rew{M} : (x:\rew{T}) \explicit \rew{U}} + \tag{X-Lam} +\end{mathpar} +\underline{Impredicative:}\ +The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ and we apply the erasable \textsc{E-Lam} typing rule to derive the typing of the erasable lambda abstraction. However, an additional premise is required \todo +\begin{mathpar} + \infer + {\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U} \ \rew{\Ga} ~ (x:\rew{T}) \erasable \rew{U} : \rew{s} \ x \notin \fv{\rew{M}^*}} + {\rew{\Ga} ~ \la(x:\rew{T}) \erasable \rew{M} : (x:\rew{T}) \erasable \rew{U}} + \tag{E-Lam} +\end{mathpar} + +\textbf{Lemma:} \todo +\begin{proof} + +\end{proof} + +\subsection{Example}

\newpage \bibliographystyle{alpha}

View it on GitLab: https://gitlab.com/monnier/typer/compare/7d6653236691d857e2c2c6e7e445db74404...