Nathaniel pushed to branch bosn at Stefan / Typer
Commits: 9887dcff by nbos at 2018-07-10T18:53:09Z Corrected typos; moved some rules and renamed rule groups; fixed boxes around figures
- - - - - 2110c130 by nbos at 2018-07-12T01:09:45Z Changed some notation
- - - - - 488c0fde by nbos at 2018-07-12T03:01:36Z Removed pmb style
- - - - - 9cbcda53 by nbos at 2018-07-17T15:56:58Z Modified TypeLevel definition and notation; described CCw; finished skeleton of proof
- - - - -
2 changed files:
- doc/formal/commands.tex - doc/formal/typer_theory.tex
Changes:
===================================== doc/formal/commands.tex ===================================== @@ -58,7 +58,7 @@ \newcommand{\app}{\raisebox{1.7pt}{\scalebox{0.8}{$||$}}} \newcommand{\appp}{\raisebox{1.7pt}{\scalebox{0.8}{$|||$}}}
-\renewcommand{\u}{$\pmb{\scriptstyle\cup}\ $} +\renewcommand{\u}{$\scriptstyle\cup\ $} \newcommand{\CC}{\text{CC$^{\npreceq}_{\omega}$}}
\newcommand{\SmallTitle}[1]{\vspace{3mm}\begin{center}
===================================== doc/formal/typer_theory.tex ===================================== @@ -14,19 +14,19 @@ We here formalize the Typer language and prove some of its properties. The gist \begin{itemize} \renewcommand{\labelitemi}{$-$} \setlength\itemsep{-3pt} -\item An infinite hierarchy of type universes `a la Russell similar to the one found in Luo's Extended Calculus of Constructions (ECC) \cite{luo}, but without cummulativity; -\item Universe polymorphism, i.e. allowing the parametrization of type universes; +\item An infinite hierarchy of type universes `a la Russell similar to the one found in Luo's Extended Calculus of Constructions (ECC) \cite{luo}, but without cumulativity; +\item Universe polymorphism allowing the parametrization of type universes; \item Erasure of propositional arguments with decidable type checking from Barras and Bernardo's variant of Miquel's Implicit Calculus of Constructions (ICC) \cite{bruno}\cite{miquel}; \item Inductive definitions as presented by Gim'enez in \cite{gimenez}. \end{itemize}
\section{Typer's Type Theory} - -\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 additional declarations with a comma (,). We write the empty context as a dot ($\cdot$) and the set of declared variables in a context $\Ga$ as $\dv{\Ga}$. The set of free variables in a term $T$ is written $\fv{M}$. The expression $M{N/x}$ denotes the substitution of free occurences 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 (;) and enriched with additional declarations with a comma (,). We write the empty context as a dot ($\cdot$) and the set of declared variables in a context $\Ga$ as $\dv{\Ga}$. The set of free variables in a term $T$ is written $\fv{M}$. The expression $M{N/x}$ denotes the substitution of free occurrences of variable $x$ for a term $N$ in term $M$.
\begin{figure}[h] - \ \ \ \ \fbox{ + \ \ \ \ \fbox{ \begin{mathpar} + \ \infer {\ } {\emptyctx ~} @@ -36,59 +36,48 @@ We here formalize the Typer language and prove some of its properties. The gist {\Ga ~ T:s \ s \in \S \ x \notin \dv{\Ga}} {\Ga , x:T ~} \textsc{ (Wf-S)} - \and %-------------------- - \infer - {\Ga ~ \ (s_1:s_2) \in \A} - {\Ga ~ s_1:s_2} - \textsc{ (Sort)} - \and %-------------------- - \infer - {\Ga ~ \ (x:T) \in \Ga} - {\Ga ~ x:T} - \textsc{ (Var)} + \ \end{mathpar} } - \caption{Typer's context and sorts rules} + \caption{Typer's Well-Formed Context Rules} \end{figure}
+\subsection{Universes and Universe Polymorphism} +Each type universe \textsf{Type} $\l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \textsf{z} ~~|~~ \textsf{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 \textsf{TypeLevel} which itself belongs to the sort \textsf{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.
- -\subsection{Universes} -Each type universe \textsf{Type} $\l$ has an index $\l$ of the type \textsf{TypeLevel} inductively defined as: -\begin{align*} - \textsf{(TypeLevel : SortL)} := &\textsf{ TypeLevel.z} : \textsf{TypeLevel} \ - | &\textsf{ TypeLevel.s} : \textsf{TypeLevel} \to \textsf{TypeLevel} -\end{align*} - -We call $\mathbb{L}$ the smallest set that is closed under the constructors for \textsf{TypeLevel}, such that we have countably infinite set of indexes $\l$. We have that \textsf{SortL} is the sort of type \textsf{TypeLevel}. And \textsf{Sort}$_\omega$ is the sort of universe polymorphic types. We define the union operator (\textsf{TypeLevel.\u} : \textsf{TypeLevel} $\to$ \textsf{TypeLevel} $\to$ \textsf{TypeLevel}) which returns the greater of two type levels. - -The above definitions allow the description of the explicit subset of Typer as a Pure Type System \cite{barendregt}: -% \begin{empheq}[box=\fbox]{equation} +We have that \textsf{Sort}$_\omega$ is the unique sort of all the types of universe polymorphic functions. We can now describe the explicit subset of Typer as a Pure Type System \cite{barendregt}:
\begin{figure}[h] \begin{empheq}[box=\fbox]{align*} \hspace{15mm} & \ & \ & \hspace{7mm} \ \S = { & \textsf{SortL}; \textsf{ Sort}_\omega; \textsf{ Type } \l} &\forall\l \in \mathbb{L} \[9pt] \A = { &(\textsf{TypeLevel} : \textsf{SortL}); \ - &(\textsf{Type } \l : \textsf{Type } (\textsf{TypeLevel.s } \l))} &\forall\l \in \mathbb{L} \[9pt] + &(\textsf{Type } \l : \textsf{Type } (\textsf{s } \l))} &\forall\l \in \mathbb{L} \[9pt] \R = { &(\textsf{SortL}, \textsf{ Type } \l, \textsf{ Sort}_\omega); &\forall\l \in \mathbb{L} \ &(\textsf{SortL}, \textsf{ Sort}_\omega, \textsf{ Sort}_\omega); \ - &(\textsf{Type } \l_1, \textsf{ Type } \l_2, \textsf{ Type } (\textsf{TypeLevel.\u}\ \l_1 \l_2))} &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] + &(\textsf{Type } \l_1, \textsf{ Type } \l_2, \textsf{ 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} \end{figure}
-Because of the impredicativity of the erasable part of Typer, we need to define a separate set of impredicative rules, written $\R_I$, all of which will be referred as $(s_1,s_2)$ as an abreviation for $(s_1,s_2,s_2)$. +Because of the impredicativity of the erasable part of Typer, we need to define a separate set of rules, written $\R_e$, some of which will be referred as $(s_1,s_2)$ as an abbreviation for $(s_1,s_2,s_2)$. \begin{figure}[h] \begin{empheq}[box=\fbox]{align*} \hspace{15mm} & \ & \ & \hspace{7mm} \ - \R_{I} = { &( \textsf{Type } \l_1, \textsf{ Type } \l_2, \textsf{ Type } \l_2) } &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] + \R_e = { &(\textsf{SortL}, \textsf{ Type } \l, \textsf{ Sort}_\omega); &\forall\l \in \mathbb{L} \ + &(\textsf{SortL}, \textsf{ Sort}_\omega, \textsf{ Sort}_\omega); \ + &( \textsf{Type } \l_1, \textsf{ Type } \l_2, \textsf{ Type } \l_2) } &\forall\l_1,\l_2 \in \mathbb{L}\[-4pt] \end{empheq} + \vspace{-5mm} \caption{Typer's Impredicative Rules} \end{figure}
\subsection{ICC in Typer} -Typer provides distinction between three kinds of terms to simplify both the writing and execution of programs. \emph{Explicit} terms are the usual expression that are written by the user and then executed. \emph{Implicit} terms are also used during execution, but Typer is able to 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 infered during elaboration, participate in type checking and are then erased before execution. The notation we adopt for compound terms are the following: +Typer provides distinction between three kinds of terms to simplify both the writing and execution of programs. \emph{Explicit} terms are the usual expression that are written by the user and then executed. \emph{Implicit} terms are also used during execution, but Typer is able to 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, participate in type checking and are then erased before execution. The notation we adopt for compound terms are the following:
\begin{center} \begin{tabular}[h]{rclll} @@ -114,45 +103,56 @@ The typing rules for explicit and erasable terms are shown in Figure X. They are \begin{mathpar} \ \infer + {\Ga ~ \ (s_1:s_2) \in \A} + {\Ga ~ s_1:s_2} + \textsc{ (Sort)} + \and %-------------------- + \infer + {\Ga ~ \ (x:T) \in \Ga} + {\Ga ~ x:T} + \textsc{ (Var)} + \and %-------------------- + \\ + \infer {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2,s_3) \in \R} {\Ga ~ (x:T) \explicit U : s_3} - \textsc{ (E-Prod)} + \textsc{ (X-Prod)} \and %-------------------- \infer {\Ga, x:T ~ M:U \ \Ga ~ (x:T) \explicit U : s} {\Ga ~ \la(x:T) \explicit M : (x:T) \explicit U} - \textsc{ (E-Lam)} + \textsc{ (X-Lam)} \and %-------------------- \infer {\Ga ~ M : (x:T) \explicit U \ \Ga ~ N:T} {\Ga ~ M|N : U{N/x}} - \textsc{ (E-App)} + \textsc{ (X-App)} \\ \infer - {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2) \in \R_I} + {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2) \in \R_e} {\Ga ~ (x:T) \erasable U : s_2} - \textsc{ (R-Prod)} + \textsc{ (E-Prod)} \and %-------------------- \infer {\Ga, x:T ~ M:U \ \Ga ~ (x:T) \erasable U : s \ x \notin \fv{M^*}} {\Ga ~ \la(x:T) \erasable M : (x:T) \erasable U} - \textsc{ (R-Lam)} + \textsc{ (E-Lam)} \and %-------------------- \infer {\Ga ~ M : (x:T) \erasable U \ \Ga ~ N:T} {\Ga ~ M|||N : U{N/x}} - \textsc{ (R-App)} + \textsc{ (E-App)} \ \end{mathpar} } - \caption{Typer's Explicit and Erasable typing rules} + \caption{Typer's Typing Judgement Rules} \end{figure}
There are two differences between explicit and erasable typing rules: \begin{enumerate} -\item In the ersasable product rule \textsc{R-Prod}, the set of rules is the impredicative $\R_I$ instead of $\R$ -\item In the erasable abstraction rule \textsc{R-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 incoherent terms. +\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 incoherent terms. \end{enumerate}
@@ -160,13 +160,13 @@ There are two differences between explicit and erasable typing rules: \subsection{Inductive Definitions} \textbf{Notation:} We use a vector notation to refer to an arbitrary countable number of instances of some kind of term, i.e. $(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 term vector $\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 an $i$ member of the set ${1,2,3,...,n}$ for $n = |\vec{N}|$.
-\textbf{Definition:} We say that $X$ is restricted to a \emph{strictly positive occurence} 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}|$. +\textbf{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}|$.
\textbf{Definition:} 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 occurences 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}|$. +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}|$.
We extend our abstract syntax with four terms introduced in \cite{gimenez} to express typing rules of inductive definitions. They are: \begin{itemize} @@ -174,15 +174,9 @@ 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 $\textsf{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, reprented as abstractions of the respective patterns of constructions. +\item $\textsf{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 of the individual cases $G_i$ in $\textsf{Case}\ M: S \text{ of } <\vec{G}>$ is captured with an expression $\S {C_i,I,Q,R}$ which is defined by structural induction on term $C_i$: -\begin{align*} - \S{P\to C,I,Q,R} && = && (y:P{I/X})\S{C,I,Q,(Ry)} && \text{if } P \equiv (\vec{x}:\vec{M})(X \vec{N}) \ - \S{(\vec{x}:\vec{M})C,I,Q,R} && = && (\vec{x}:\vec{M})\S{C,I,Q,(Rx)} && \text{if $X$ is not free in $M_i$ $\forall i \in |\vec{M}|$} \ - \S{(X\vec{N}),I,Q,R} && = && (Q \vec{N} R) -\end{align*} The typing rules for inductive definitions and case analysis are presented in Figure X.
\begin{figure}[h] @@ -206,12 +200,53 @@ The typing rules for inductive definitions and case analysis are presented in Fi \infer { \Ga ~ Q : (\vec{z}:\vec{Z})(I\ \vec{z}) \to \text{Type } \l_A \ \Ga ~ M:(I\ \vec{P}) \ - \Ga \stackrel{\forall i \in |\vec{G}|}{~} G_i:\S {C_i,Q,\Constr(i,I)}} + %% FIXME: Actually, each Gi returns the constant type Q + %% (it does take some parameters corresponding to the elements + %% carried by the constructor, of course), along with an + %% additional argument (P : Eq M (Ci \vec{x})) witnessing that + %% the case has found M to be of the form "Ci \vec{x}". + %% + %% FIXME: Before introducing inductive types (and hence `case`) + %% we thus need to introduce the built-in `Eq` type, defined in + %% .../typer/btl/builtins.typer as follow: + %% + %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l + %% Eq_refl : ((x : ?t) ≡> Eq x x); + %% Eq_cast : (x : ?) ≡> (y : ?) + %% ≡> (p : Eq x y) + %% ≡> (f : ? -> ?) + %% ≡> 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 + %% during type-checking (it would be unsound because it would be reduced + %% even in contexts where the `p : Eq x y` argument doesn't actually + %% exist, such as + %% + %% λ (P : Eq Int String) → concat "bug" (cast (p := P) 5) + %% + %% We'll probably want to add an additional builtin of the form: + %% + %% Eq_cast_eval : Eq (Eq_cast ?x) ?x; + %% + %% to axiomatize the runtime behavior of `Eq_cast`, but I haven't + %% bothered to do that yet. + %% + %% FIXME: Typer's `case` construct can have a "default" + %% branch; not sure how to provide that in this setting where + %% the branches implicitly specify their constructor by the position + %% of the branch. Maybe we should use a formalism closer to Typer's + %% real representation where we don't use natural numbers "i" but + %% labels (strings) to name each constructor. Let's keep using "i" + %% and forget about the default branch for now, tho. + \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)} \textsc{ (Case)} \end{mathpar} } - \caption{Typer's Inductive and Case typing rules} + \caption{Typer's Inductive and Case Typing Rules} \end{figure}
\subsection{Fixpoint Operator} @@ -228,7 +263,7 @@ Recursion is specified through the use of a recursive operator \Letrec \todo
-\textbf{Definition:} A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to stricly positive occurences [? not a form of constructor w.r.t $X$ ?], is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$ [? can't ?]. We abbreviate this property as $RP{i,C}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$. +\textbf{Definition:} A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to strictly positive occurrences [? not a form of constructor w.r.t $X$ ?], is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$ [? can't ?]. We abbreviate this property as $RP{i,C}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$.
\textbf{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, but $f$, $k$ and $x$ remain bound to their presence in full predicate $\D_\V{f,k,x,M}$. We also write $\D_\V{\vec{M}}$ instead of $\bigwedge_i \D_\V{M_i}$. The condition $\D_\V{M} = \D_\V{f,k,x,M}$ is determined by structural induction on term $M$: \begin{align*} @@ -264,26 +299,30 @@ Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $ \infer {B \cong B' \ N \cong N'} {\Letrec\ ? \todo} + \ \end{mathpar} } - \caption{Typer's conversion rules} + \caption{Typer's Conversion Rules} \end{figure}
\section{Relative Expressivity to \CC} -In this section we will prove that the impredicative rules and the universe hierarchy of Typer allow for a representation of all typing derivations from a Calculus of Constructions with an infinite hierarchy of (uncummulative) universes (\CC). +In this section we will prove that the impredicative rules and the universe hierarchy of Typer allow for a representation of all typing derivations from a Calculus of Constructions with an infinite hierarchy of (noncumulative) universes (\CC).
\subsection{Definition of \CC} -The typing rules for \CC\ are shown in Figure X. They are the standard rules for the Calulus of Constructions \cite{}, but the underlying PTS has an infinite hierarchy of universes (Figure X). +Our definition of \CC\ is based on Luo's infinite hierarchy of universes designed for ECC \cite{luo}, but since Typer does not support subtyping, we remove the condition that the universes are cumulative. We also change the name of the universes so that they match more easily with Typer's during translation. Thus, instead of $$\textsf{Prop : Type$_0$ : Type$_1$ : Type$_2$ : ...},$$ we have $$\textsf{Prop : Type$_1$ : Type$_2$ : Type$_3$ : ...}.$$ But the semantics remain the same. + +\CC's PTS definition is shown in Figure X. The typing rules for \CC\ are shown in Figure X. They are the standard rules for the Calculus of Constructions \cite{}, but the underlying PTS has an infinite hierarchy of universes.
\begin{figure}[h] \begin{empheq}[box=\fbox]{align*} - \hspace{15mm} & \ & \ & \hspace{7mm} \ + \hspace{20mm} & \ & \ & \hspace{7mm} \ \S_{CC} = { & \textsf{Prop}; \textsf{ Type}_i} &\forall i > 0 \[9pt] \A_{CC} = { &(\textsf{Prop} : \textsf{Type}_1); \ &(\textsf{Type}_i : \textsf{Type}_{i+1})} &\forall i > 0 \[9pt] \R_{CC} = { &(\textsf{Type}_i, \textsf{ Prop }, \textsf{ Prop}); &\forall i > 0 \ &(\textsf{Type}_i,\textsf{Type}_i,\textsf{Type}_i); &\forall i > 0 \ \end{empheq} + \vspace{-5mm} \caption{\CC's Pure Type System} \end{figure}
@@ -325,6 +364,7 @@ The typing rules for \CC\ are shown in Figure X. They are the standard rules for {\Ga \CCdash M : (x:T) \explicit U \ \Ga \CCdash N:T} {\Ga \CCdash M|N : U{N/x}} \textsc{ (CC-App)} + \ \end{mathpar} } \caption{\CC's Typing Rules} @@ -332,32 +372,38 @@ The typing rules for \CC\ are shown in Figure X. They are the standard rules for
\subsection{Proof}
+%% FIXME: The term is "conservative extension". + +%% FIXME: ...the complexity will be in figuring out exactly when we need to +%% 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: Context and Sorts Rules} + \textbf{Case 1: \textsc{Wf-E}, \textsc{Wf-S}, \textsc{Sort} and \textsc{Var}}
- The translation is almost trivial as the four rules \textsc{Wf-E}, \textsc{Wf-S}, \textsc{Sort}, and \textsc{Var} are unchanged between the two calculi. The only necessary translation is between the universe hierarchies. We therefore have a mapping $\S_{CC} \to \S$: + 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$: \begin{align*} - \textsf{Prop} &\mapsto \textsf{Type TypeLevel.z} \ - \textsf{Type$_1$} &\mapsto \textsf{Type TypeLevel.s(TypeLevel.z)} \ - \textsf{Type$_2$} &\mapsto \textsf{Type TypeLevel.s(TypeLevel.s(TypeLevel.z))} \ + \textsf{Prop} &\mapsto \textsf{Type z} \ + \textsf{Type$_1$} &\mapsto \textsf{Type (s z)} \ + \textsf{Type$_2$} &\mapsto \textsf{Type (s (s z))} \ \vdots~~~~~ &\mapsto ~~~~~~~\vdots \end{align*}
- Through this mapping, all axioms of $\A_{CC}$ are analogous to axiom scheme $(\textsf{Type } \l : \textsf{Type } (\textsf{TypeLevel.s } \l))}~\forall\l \in \mathbb{L}$ from $\A$. + 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}}
- $\R_{CC}$ has members analogous to members of both $\R$ and $\R_i$. Specifically [?] - - \textbf{Case 3: \textsc{CC-Lam}} - + $\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)$.\
- \textbf{Case 4: \textsc{CC-App}} + \textbf{Case 3: \textsc{CC-Lam} and \textsc{CC-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}
- \newpage +\newpage \bibliographystyle{alpha} \bibliography{typer_theory} -\end{document} \ No newline at end of file +\end{document}
View it on GitLab: https://gitlab.com/monnier/typer/compare/a05b2179317dfe0b67df7e1242a739d9a2f...
Afficher les réponses par date