Nathaniel pushed to branch bosn at Stefan / Typer

Commits: 576bfd64 by nbos at 2018-09-02T04:26:20Z Add of sans-serif keyword command

- - - - - b15652de by nbos at 2018-09-02T04:29:15Z Restructure some sentences; add recursive definition of free variables; define beta- and iota-reductions; add transitivity to congruence relation

- - - - -

2 changed files:

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

Changes:

===================================== doc/formal/commands.tex ===================================== @@ -18,6 +18,7 @@ \newcommand{\Ind}{\textsf{Ind}} \newcommand{\Constr}{\textsf{Constr}} \newcommand{\Case}{\textsf{Case}} +\newcommand{\of}{\textsf{of}} \newcommand{\Elim}{\textsf{Elim}} \newcommand{\Fix}{\textsf{Fix}} \newcommand{\Letrec}{\textsf{Letrec}}

===================================== doc/formal/typer_theory.tex ===================================== @@ -49,6 +49,7 @@ The gist of the theory behind Typer is Coquand and Huet's Calculus of Constructi \end{figure}

\begin{figure} + \label{fig:Re} \begin{empheq}[box=\fbox]{align*} \hspace{15mm} & \ & \ & \hspace{7mm} \ \R_e = { &(\SortL,\ \Type\ \l,\ \Sortw); &\forall\l \in \mathbb{L} \ @@ -62,16 +63,15 @@ The gist of the theory behind Typer is Coquand and Huet's Calculus of Constructi Each type universe $\Type\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \z ~~|~~ \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. -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. We write $\s^i$ to abbreviate the application of the successor $i$ times. 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. All type levels $\l$ inhabit the type \TypeLevel\ which 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}$ closed under those two constructs. We write $\s^i$ to abbreviate the application of the successor $i$ times. When applied on type levels, the operator $\cup$ returns the greater of the two. The construct $l$ stands for a \emph{level variable} which will occur in universe polymorphic definitions. All type levels $\l$ inhabit the type \TypeLevel\ which belongs to the sort \SortL.

\Sortw\ is the unique sort of all the universe polymorphic function types. We describe the explicit part of Typer as a Pure Type System \cite{barendregt} in figure \ref{fig:PTS}. % FIXME: PDF prints 1.1 instead of 1 -Because of the erasable part of Typer allows for impredicative definitions, we define a separate set of rules $\R_e$. +Because erasable definitions can be impredicative in Typer, we define a separate set of rules $\R_e$ (figure \ref{fig:Re}). % FIXME: PDF prints 1.1 instead of 2

\subsection{Erasure in Typer} Typer manipulates three separate kinds of terms to simplify the writing and execution of programs. \emph{Explicit} terms are the usual expression that are written by the user and executed. \emph{Implicit} terms are also used during execution, but Typer can infer them during elaboration such that they do not need to be written by the user. \emph{Erasable} terms are neither written by the user nor executed; they are inferred during elaboration, provide type information during checking and are erased before execution.

-\textbf{Notation:} The notation we adopt in this document is meant to allow for the distinction between the three kinds of terms and also to evoke actual Typer code. The traditional explicit lambda term $\la(x:A).b$ will here be written $\la(x:A)\explicit b$ and similarly the product type $\Pi(x:A).B$ will be written $(x:A)\explicit B$. The type of arrow used will convey the kind of term being defined. Thus, compound terms of our calculus will all take one of the following forms: - +\textbf{Notation:} The notation we adopt in this document is meant to allow for the distinction between the three kinds of terms and also to evoke actual Typer code. The traditional explicit lambda term $\la(x:A).b$ are here be written $\la(x:A)\explicit b$ and similarly the product type $\Pi(x:A).B$ are written $(x:A)\explicit B$. The type of arrow used will convey the kind of term being defined. Compound terms of our calculus therefore all take one of the following forms: \begin{center} \begin{tabular}[h]{rclll} & & $\la$-abstraction & Product type & Application \[3mm] @@ -83,11 +83,27 @@ Typer manipulates three separate kinds of terms to simplify the writing and exec

After elaboration, implicit terms behave exactly like explicit terms so we will not explicitly include them in our calculus; they will be assumed to be a subset of the explicit terms.

-\textbf{Notation:} We define a context $\Ga$ as a list of typing declarations $(x_i:T_i)$ and write $\Ga ~$ to express that $\Ga$ is well formed. Contexts are concatenated with the semicolon (;) and enriched with an additional declarations with a comma (,). We write the empty context as a dot ($\cdot$). The set of declared variables in a context $\Ga$ is written $\dv{\Ga}$ and the set of free (i.e. unbound) variables in a term $T$ is written $\fv{T}$. The expression $M{N/x}$ denotes the substitution of free occurrences of variable $x$ for a term $N$ in term $M$. +\textbf{Notation:} We define a context $\Ga$ as a list of typing declarations $(x_i:T_i)$ and write $\Ga ~$ to express that $\Ga$ is well formed. Contexts are concatenated with the semicolon or enriched with an additional declarations with a comma. We write the empty context as a dot ($\cdot$). The set of declared variables in a context $\Ga$ is written $\dv{\Ga}$ and the set of free (i.e. unbound) variables in a term $T$ is written $\fv{T}$ (defined in figure \ref{fig:fv}). The expression $M{N/x}$ denotes the substitution of free occurrences of variable $x$ for a term $N$ in term $M$. +\begin{figure}[h] + \label{fig:fv} + \centering + \fbox{\begin{minipage}{0.9\linewidth} + Where $s \in \S$ + \begin{align*} + \fv{s} &= \emptyset & \fv{x} &= x \[5pt] + \fv{\la(x:T)\explicit M} &= \fv{T}\cup(\fv{M}\backslash{x}) & \fv{(x:T)\explicit U} &= \fv{T}\cup(\fv{U}\backslash{x}) \ + \fv{\la(x:T)\erasable M} &= \fv{T}\cup(\fv{M}\backslash{x}) & \fv{(x:T)\erasable U} &= \fv{T}\cup(\fv{U}\backslash{x}) \[5pt] + \fv{M \ap N} &= \fv{M}\cup\fv{N} & \fv{M \appp N} &= \fv{M}\cup\fv{N}\ + \end{align*} + \end{minipage}} + \caption{Definition of the set of free variables} +\end{figure}

\begin{figure}[h] + \label{fig:*} \centering \fbox{\begin{minipage}{0.9\linewidth} + Where $s \in \S$ \begin{align*} s^* &= s & x^* &= x \[5pt] (\la(x:T)\explicit M)^* &= \la(x)\explicit M^* & ((x:T)\explicit U)^* &= (x:T^*)\explicit U^* \ @@ -95,11 +111,10 @@ After elaboration, implicit terms behave exactly like explicit terms so we will (M \ap N)^* &= M^*\ap N^* & (M \appp N)^* &= M^*\ \end{align*} \end{minipage}} - \caption{Extraction function $M \mapsto M^*$} - \label{fig:*} \end{figure} -We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure \ref{fig:*}. It erases domains of abstraction, erasable abstractions and erasable applications and turns erasable products into a propositional form. The typing rules shown in figure \ref{fig:Typing-rules} are the rules from Barras and Bernardo's ICC \cite{bruno}. + +We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure \ref{fig:*}. It erases domains of abstraction, erasable abstractions and erasable applications and turns erasable products into a propositional form. The typing rules shown in figure \ref{fig:Typing-rules} are taken directly from Barras and Bernardo's ICC \cite{bruno}, but written in Typer's syntax.

\begin{figure}[h] \ \ \ \ \fbox{ @@ -165,23 +180,24 @@ We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure There are two notable differences between explicit and erasable typing rules: \begin{enumerate} \item In the erasable product rule \textsc{E-Prod}, the set of rules is the impredicative $\R_e$ instead of $\R$ -\item In the erasable abstraction rule \textsc{E-Lam}, erasable abstraction are conditional on the bound variable not being free in the expression after erasure ($x \notin \fv{M^*}$). This ensures that the variable is only used in ``erasable'' ways inside the expression such that we are not left with free terms after erasure. +\item In the erasable abstraction rule \textsc{E-Lam}, erasable abstraction are conditional on the bound variable not being free in the expression after erasure ($x \notin \fv{M^*}$). This ensures that the variable is only used in ``erasable'' ways inside the expression such that we are not left with new free terms after erasure. \end{enumerate}

\subsection{Inductive Definitions} -\textbf{Notation:} We abbreviate a list of terms $N_i$ as $\vec{N}$. For example, $(X \vec{N})$ refers to the identifier $X$ followed by $N_1$, $N_2$, ..., $N_n$ for $n = |\vec{N}|$ where $|\vec{N}|$ is the size of the list of terms $\vec{N}$. Similarly, $(\vec{x}:\vec{M})X$ refers to the term $(x_1:M_1)(x_2:M_2)...(x_n:M_n)X$ for $n = |\vec{x}| = |\vec{M}|$. We also write $i \in |\vec{N}|$ to refer to a member $i$ of the set ${1,2,3,...,n}$ for $n = |\vec{N}|$. +\textbf{Notation:} We abbreviate a list of terms $N_i$ as $\vec{N}$. For example, $(X \vec{N})$ refers to the identifier $X$ followed by $N_1$, $N_2$, ..., $N_n$ for $n = |\vec{N}|$ where $|\vec{N}|$ is the size of the list of terms $N_i$. Similarly, $(\vec{x}:\vec{M})X$ refers to the term $(x_1:M_1)(x_2:M_2)...(x_n:M_n)X$ for $n = |\vec{x}| = |\vec{M}|$. We also write $i \in |\vec{N}|$ to refer to a member $i$ of the set ${1,2,3,...,n}$ for $n = |\vec{N}|$. \ \begin{definition} We say that $X$ is restricted to a \emph{strictly positive occurrence} in a term $P$ if $P \equiv (\vec{x}:\vec{M})(X \vec{N})$ where $X$ is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. \end{definition} \begin{definition} + \label{def:foc} We say that $C$ is a \emph{form of constructor} w.r.t. $X$ if it can be constructed with the following syntax:

$$C ::= (X \vec{N}) ~~|~~ P\to C ~~|~~ (\vec{x}:\vec{M})C$$

Where $X$ is restricted to strictly positive occurrences in the term $P$ and is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. \end{definition} -We extend our abstract syntax with four terms from Gim'enez's inductive definitions \cite{gimenez}: +We extend our abstract syntax with three terms from Gim'enez's inductive definitions \cite{gimenez}: \begin{itemize} \renewcommand{\labelitemi}{$-$} \setlength\itemsep{-3pt} @@ -255,7 +271,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} + {\Ga ~ \Case\ M:(I\ \vec{P}) \of <\vec{G}> : Q} \textsc{ (Case)} \end{mathpar} } @@ -276,10 +292,10 @@ Recursion is specified through the use of a recursive operator \Letrec \todo \end{mathpar}

\begin{definition} - A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to strictly positive occurrences, is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$. We abbreviate this property as $RP{i,C}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$. + A \emph{recursive position} in the form of constructor $(\vec{x}:\vec{M}) (X \vec{N})$ is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$. Note that this is not in contradiction to definition \ref{def:foc} because some abstraction $(x_i:M_i)$ could be non-dependent (i.e. of form $P \explicit C$ in definition \ref{def:foc}), in which $X$ is free to appear. We abbreviate this property as $RP{i,C}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$. \end{definition} \begin{definition} - The \emph{guarded by destructors} condition is written as the predicate $\D_\V{f,k,x,M}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which represent the recursive components of $x$ in $M$. Below, we write $\D_\V{M}$ for brevity instead of the full $\D_\V{f,k,x,M}$. We also write $\D_\V{\vec{M}}$ instead of $\bigwedge_i \D_\V{M_i}$. By structural induction on term $M$, we describe when $\D_\V{M} = \D_\V{f,k,x,M}$ is true by assigning conjunctions of necessary conditions to each form of $M$: + The \emph{guarded by destructors} condition is written as the predicate $\D_\V{f,k,x,M}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which collects the recursive components of $x$ in $M$. Below, we write $\D_\V{M}$ for brevity instead of the full $\D_\V{f,k,x,M}$. We also write $\D_\V{\vec{M}}$ instead of $\D_\V{M_1} \land\D_\V{M_2}\land ...$. By structural induction on term $M$, we describe when $\D_\V{M}$ is true by assigning conjunctions of necessary conditions to each form of $M$: \begin{align*} \D_\V{M} & = \text{True} & \text{if } f \notin \fv{M}\ \D_\V{\la (z:P)\to Q} & = \D_\V{P} \land \D_\V{Q} \ @@ -288,18 +304,31 @@ Recursion is specified through the use of a recursive operator \Letrec \todo \D_\V{\Ind(X:A)<\vec{C}>} & = \D_\V{A} \land \D_\V{\vec{C}} \ \D_\V{f \vec{P}} & = (|\vec{P}| > k) \land (P_{k+1} \equiv (z\ \vec{Q})) \land \D_\V{\vec{P}} & \text{with $z \in \V$}\ \D_\V{N \vec{P}} & = \D_\V{N} \land \D_\V{\vec{P}} &\text{if $N \neq f$}\ - \D_\V{\Case\ (z\ \vec{P}):S \text{ of } <\vec{G}>} & = \D_\V{Q} \land \D_\V{S} \land \D_\V{\vec{P}} &\text{with $z \in \V \cup {x}$}\ - & \quad \land S \equiv I\vec{R} & \text{with }I =\Ind (X:A)<\vec{C}> \ - & \quad \land \text{if } + \D_\V{\Case\ (z\ \vec{P}):S\ \of\ <\vec{G}>} & = + % \D_\V{Q} \land \D_\V{S} \land \D_\V{\vec{P}} &\text{with $z \in \V \cup {x}$}\ + % & \quad \land S \equiv I\vec{R} & \text{with }I =\Ind (X:A)<\vec{C}> \ + % & \quad \land \text{if } \end{align*} \end{definition}

\subsection{Conversion Rules} -Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $\cong$. [Expand \todo] +Typer admits $\beta$- and $\iota$-conversions. The congruence relation between converted terms is written $\cong$. $\beta$-reduction is defined as +$$(\la (x:T)\explicit e_1)|e_2 ~ \cong_\beta ~ e_1{e_2/x}$$ +$$(\la (x:T)\erasable e_1)|||e_2 ~ \cong_\beta ~ e_1{e_2/x}$$ + +$\iota$-reduction concerns case analyses: +$$\Case\ (\Constr (i,I)\vec{P}):S\ \of\ <\vec{G}> \cong_{\iota} (G_i\vec{P})$$ +Conversion rules are exposed in figure \ref{fig:conv}.

\begin{figure}[h] + \label{fig:conv} \ \ \ \ \fbox{ \begin{mathpar} + \infer + {M \cong N \ N \cong P} + {M \cong P} + \and %-------------------- + %% FIXME: Add conversion rules for other terms? (lambda, product type, application) \infer {A \cong A' \ |\vec{C}| = |\vec{C'}| \ C_i \stackrel{\forall i \in |\vec{C}|}{\cong} C_i'} {\Ind (X:A)<\vec{C}> \cong \Ind (X:A')<\vec{C'}>} @@ -323,7 +352,7 @@ Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $ \end{figure}

\section{Typer as an Extension of a Calculus of Constructions} -In this section we will show that the erasable terms of Typer allows 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). This will be demonstrated through a translation and its proof of correctness. +In this section we show 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). This will be demonstrated through a translation and a proof of its correctness.

\subsection{Definition of \CC}

@@ -390,7 +419,7 @@ In this section we will show that the erasable terms of Typer allows for a repre

Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, to which we add an infinite hierarchy of predicative universes above an impredicative \Prop. Thus we have: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4 : ...$$

-\CC's PTS definition is shown in figure \ref{fig:CC-pts}. The typing rules for \CC\ are shown in figure \ref{fig:CC-rules}. The structure of the PTS is derived from Luo's own extension of CC (ECC) \cite{luo}, where the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop, \Prop, \Prop)$, $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, \Type_{\max (i,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\ might therefore behave differently than other definitions of \CC\ (for example \cite{miquel}). +\CC's PTS definition is shown in figure \ref{fig:CC-pts}. The typing rules for \CC\ are shown in figure \ref{fig:CC-rules}. The structure of the PTS is derived from Luo's own extension of CC (ECC) \cite{luo}, where the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop, \Prop, \Prop)$, $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, \Type_{\max (i,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 (e.g. dependent types or polymorphic functions). Our definition of \CC\ might therefore behave differently than other definitions of \CC\ (for example \cite{miquel}).

\subsection{Translation} \begin{figure}[h] @@ -495,14 +524,7 @@ Before proving the correctness of the equality, we show the following lemmas: \end{cases} \quad \forall \l_1,\l_2 \in \mathbb{L} \ &= (\Type\ (\s\ \l_1), \Type\ (\s\ \l_2), \Type\ ((\s\ \l_1) \cup (\s\ \l_2))) \quad \in \R \quad \forall \l_1,\l_2 \in \mathbb{L} \end{align*} - Conversely, since the translation on sorts is defined on elements of $S_{CC}$, sorts $\rew{s}$ match with sorts of the form $\Type\ (\s^i\ \z)\in \S\ \forall i \ge 0$ (lemma \ref{lem:S-equiv}). It follows that rules $(\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$ match with rules of the form $$(\Type\ \l_1, \Type\ \l_2, \Type\ (\l_1 \cup \l_2)) \in \R ~~ \forall \l_1,\l_2 \in \mathbb{L}$$ By the equalities established in the forward direction, each such rule has a single corresponding rule in $(s_1,s_2,s_3) \in \R_{CC}$, as long as $s_1 \neq \Type_i \text{ or } s_2 \neq \Prop$ - - % The condition $\text{ if } s_1 \neq \Type_i \text{ or } s_2 \neq \Prop$ ensures that the rule scheme - % \begin{align*} - % (\rew{\Type_i},\rew{\Prop},\rew{\Type_i}) = (\Type\ \l_1, \Type\ \z, \Type\ \l_1) &\in \R \ - % (\Type_i,\Prop,\Type_i) &\notin \R_{CC} - % \end{align*} - % is not considered. + Conversely, since the translation on sorts is defined on elements of $S_{CC}$, sorts $\rew{s}$ match with sorts of the form $\Type\ (\s^i\ \z)\in \S\ \forall i \ge 0$ (lemma \ref{lem:S-equiv}). It follows that rules $(\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$ match with rules of the form $$(\Type\ \l_1, \Type\ \l_2, \Type\ (\l_1 \cup \l_2)) \in \R ~~ \forall \l_1,\l_2 \in \mathbb{L}$$ By the equalities established in the forward direction, each such rule has a single corresponding rule in $(s_1,s_2,s_3) \in \R_{CC}$, as long as $s_1 \neq \Type_i \text{ or } s_2 \neq \Prop$.

\end{proof} \end{lemma} @@ -599,141 +621,7 @@ Before proving the correctness of the equality, we show the following lemmas: Here $P = M|N$ and $W = U{N/x}$. $y \notin \fv{\rew{P}^*}$ will hold if we can show that $y \notin \fv{\rew{M}^*}$ and---unless $N$ is an impredicative argument---$y \notin \fv{\rew{N}^*}$. By assumption $U{N/x} : \Prop$ %% Does this step really hold? and therefore also $U : \Prop$. It follows that $(x:T)\explicit U : \Prop$ by the typing rule \textsc{CC-Prod}. Thus, by induction hypothesis, we have $y \notin \fv{\rew{M}^*}$ because $M : (x:T)\explicit U : \Prop$. If $N : T : \Prop$, then we can also apply the induction hypothesis. Otherwise, the extraction on the translation erases the impredicative argument completely. - \end{proof} - - %% **PURGATORY** ATTEMPTED PROOF ON TYPER DERIVATIONS - %\textbf{Sort:}\ - % \begin{mathpar} - % \infer - % {\rew{\Ga, y:V} ~ \ (\rew{s_1}:\rew{s_2}) \in \A} - % {\rew{\Ga, y:V} ~ \rew{s_1}:\rew{s_2}} - % \tag{Sort} - % \end{mathpar} - % \textsc{Sort} is not applicable to this derivation because $\rew{W}$ is set to have sort $\Type\ \z$ but there is no sort $\rew{s_2}$ that has sort $\Type\ \z$ because it is itself the smallest sort. - - % \textbf{Var:}\ - % \begin{mathpar} - % \infer - % {\rew{\Ga, y:V} ~ \ (x:\rew{T}) \in \rew{\Ga, y:V}} - % {\rew{\Ga, y:V} ~ x:\rew{T}} - % \tag{Var} - % \end{mathpar} - % It is not possible that $x = y$ because that would imply that their types satisfy $\rew{T} = \rew{V}$ (i.e. $\rew{W} = \rew{V}$) and, further, that their unverses satisfy $\Type\ (\s\ \l) = \Type\ \z$ which is false. Then, $x \neq y$ and we have that $$y \notin \fv{x^*} ~~ \equiv ~~ y \notin \fv{x}$$ because $x$ and $y$ are different variables. - - % \textbf{X-Prod & E-Prod:}\ - % Both \textsc{X-Prod} and \textsc{E-Prod} do not apply because both would set $\rew{W}$ to be a sort: - % $${\rew{\Ga, y:V} ~ (x:\rew{T}) \explicit \rew{U} : \rew{s_3}}$$ - % $$\rew{\Ga, y:V} ~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop}$$ - - % but $\rew{W} : \Type\ \z$ and there is no sort that has sort $\Type\ \z$, because it is the smallest sort. - - % \textbf{X-Lam:}\ - % \begin{mathpar} - % \infer - % {\rew{\Ga, y:V, x:T} ~ \rew{M}:\rew{U} \ \rew{\Ga, y:V} ~ (x:\rew{T}) \explicit \rew{U} : s} - % {\rew{\Ga, y:V} ~ \la(x:\rew{T}) \explicit \rew{M} : (x:\rew{T}) \explicit \rew{U}} - % \tag{X-Lam} - % \end{mathpar} - - % We know that $s = \Type\ \z$ because here $\rew{W} = (x:\rew{T})\explicit \rew{U}$ and by assumption $\rew{W} : \Type\ \z$. By the construction of the explicit product $(x:\rew{T}) \explicit \rew{U}$, we have - % \begin{mathpar} - % \infer - % {\rew{\Ga, y:V} ~ \rew{T}:s_1 \ \rew{\Ga, y:V, x:T} ~ \rew{U}:s_2 \ (s_1,s_2,\Type\ \z) \in \R} - % {\rew{\Ga, y:V} ~ (x:\rew{T}) \explicit \rew{U} : \Type\ \z} - % \tag{X-Prod} - % \end{mathpar} - % The only rule in $\R$ that matches $(s_1,s_2,\Type\ \z)$ is $(\Type\ \z, \Type\ \z, \Type\ \z)$ where, in particular, $s_2 = \Type\ \z$ and therefore $\rew{U} : \Type\ \z$. The extraction $\rew{P}^*$ here is: - % $$(\la(x:\rew{T}) \explicit \rew{M})^* = \la (x) \explicit \rew{M}^*$$ - % Therefore, - % $$\fv{(\la(x:\rew{T}) \explicit \rew{M})^*} = \fv{\rew{M}^*}$$ - % And we have - % \begin{mathpar} - % {\rew{\Ga, y:V, x:T} ~ \rew{M}:\rew{U} \ \rew{\Ga, y:V} ~ \rew{U} : \Type\ \z} - % \end{mathpar} - % so by the induction hypothesis, we can assume - % $$y \notin \fv{\rew{M}^*}$$ - - % \textbf{E-Lam:}\ - % \begin{mathpar} - % \infer - % {\rew{\Ga, y:V, x:T} ~ \rew{M}:\rew{U} \ \rew{\Ga, y:V} ~ (x:\rew{T}) \erasable \rew{U} : s \ x \notin \fv{\rew{M}^*}} - % {\rew{\Ga, y:V} ~ \la(x:\rew{T}) \erasable \rew{M} : (x:\rew{T}) \erasable \rew{U}} - % \tag{E-Lam} - % \end{mathpar} - - % Similarly, here we know that $s = \Type\ \z$ because $\rew{W} : \Type\ \z$. By the construction of the erasable product $(x:\rew{T}) \erasable \rew{U}$, we have - % \begin{mathpar} - % \infer - % {\rew{\Ga, y:V} ~ \rew{T}:s_1 \ \rew{\Ga, y:V, x:T} ~ \rew{U}:\Type\ \z \ (s_1,\Type\ \z,\Type\ \z) \in \R_e} - % {\rew{\Ga, y:V} ~ (x:\rew{T}) \erasable \rew{U} : \Type\ \z} - % \tag{E-Prod} - % \end{mathpar} - % The extraction is - % $$(\la(x:\rew{T}) \erasable \rew{M})^* = \la (x) \erasable \rew{M}^*$$ - % Therefore, - % $$\fv{(\la(x:\rew{T}) \erasable \rew{M})^*} = \fv{\rew{M}^*}$$ - % And we have - % \begin{mathpar} - % {\rew{\Ga, y:V, x:T} ~ \rew{M}:\rew{U} \ \rew{\Ga, y:V} ~ \rew{U} : \Type\ \z} - % \end{mathpar} - % so by the induction hypothesis, we can assume - % $$y \notin \fv{\rew{M}^*}$$ - - % \textbf{X-App:}\ - % \begin{mathpar} - % \infer - % {\rew{\Ga, y:V} ~ \rew{M} : (x:T) \explicit \rew{U} \ \rew{\Ga, y:V} ~ \rew{N}:T} - % {\rew{\Ga, y:V} ~ \rew{M}|\rew{N} : \rew{U}{\rew{N}/x}} - % \tag{X-App} - % \end{mathpar} - % We know that $\rew{U}{\rew{N}/x} : \Type\ \z$ because here $\rew{W} = \rew{U}{\rew{N}/x}$ and by assumption $\rew{W} : \Type\ \z$. - % %% FIXME: Does the next sentence really hold? - % Because $\rew{U}{\rew{N}/x} : \Type\ \z$, we also have $\rew{U} : \Type\ \z$. By the construction of the explicit product, we have - % \begin{mathpar} - % \infer - % {\rew{\Ga, y:V} ~ T:s_1 \ \rew{\Ga, y:V}, x:T ~ \rew{U}:\Type\ \z \ (s_1,\Type\ \z,s_3) \in \R} - % {\rew{\Ga, y:V} ~ (x:T) \explicit \rew{U} : s_3} - % \tag{X-Prod} - % \end{mathpar} - % The only rule in $\R$ that matches $(s_1,\Type\ \z,s_3)$ is $(\Type\ \z, \Type\ \z, \Type\ \z)$ where, in particular, $\rew{U} : \Type\ \z$. - - % Because $\rew{M}|\rew{N}$ is a translated term $\rew{P} = \rew{M|N}$ whose translation is not an erasable application, by the definition of the translation (figure \ref{fig:[]}): - % \begin{align*} - % \rew{M \ap N} &= - % \begin{cases} - % \rew{M}|||\rew{N} &\text{if $(M:\tau:\Prop)$ and $(N:\tau':\Type_i)$} \ - % \rew{M}|\rew{N} &\text{otherwise} - % \end{cases} - % \end{align*} - % we infer that either $M$ has a type of a sort other than $\Prop$ or $N$ has a type of sort \Prop. We know that - % \begin{align*} - % sssss - % \end{align*} - - - % The extraction $\rew{P}^*$ here is: - % $$(\la(x:\rew{T}) \explicit \rew{M})^* = \la (x) \explicit \rew{M}^*$$ - % Therefore, - % $$\fv{(\la(x:\rew{T}) \explicit \rew{M})^*} = \fv{\rew{M}^*}$$ - % And we have - % \begin{mathpar} - % {\rew{\Ga, y:V, x:T} ~ \rew{M}:\rew{U} \ \rew{\Ga, y:V} ~ \rew{U} : \Type\ \z} - % \end{mathpar} - % so by the induction hypothesis, we can assume - % $$y \notin \fv{\rew{M}^*}$$ - - - % \textbf{E-App:}\ - % \begin{mathpar} - % \infer - % {\rew{\Ga, y:V} ~ \rew{M} : (x:\rew{T}) \erasable \rew{U} \ \rew{\Ga, y:V} ~ \rew{N}:\rew{T}} - % {\rew{\Ga, y:V} ~ \rew{M}|||\rew{N} : \rew{U}{\rew{N}/x}} - % \tag{E-App} - % \end{mathpar} - - % \end{proof} - \end{lemma}

\subsection{Completeness of translation} @@ -1039,7 +927,7 @@ This case considers the typing derivation of term $\rew{(x:T)\explicit U}$. If \

By induction hypothesis we assume \begin{mathpar} - {\Ga \CCdash T:s_1 \ \Ga, x:T \CCdash U:s_2} + {\Ga \CCdash T:s_1 \ \Ga, x:T \CCdash U:s_2} \end{mathpar} By lemma \ref{lem:R-equiv} we infer $$(s_1,s_2,s_3) \in \R_{CC}$$

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