Stefan pushed to branch report/tcvi at Stefan / Typer
Commits: 3bd4089e by Stefan Monnier at 2019-11-20T06:43:56Z -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -357,7 +357,7 @@ The contributions of this work are: \item As needed for some of the above contributions, we sketch a calculus with both inductive types and erasability annotations. While this is straightforward, we do not know of such a system published so far, the - closest we found being the one described by~\citet{Bernardo09}. + closest we found being the one described by Bernardo~\citet{Bernardo09}. %% \item The observation that ICC's stronger conversion rule may not be as %% strong as it seems. \FIXME{really?} \end{itemize} @@ -674,14 +674,14 @@ The calculus we use for that can be described by the following EPTS: (\Type \ell : \Type {\ell+1}) ~~|~~ \ell\in\mathbb{N} ~} \ \mathcal{R} &=& \begin{array}[t]{@{}l@{~~|~~}l} - {~ (k, \kw{Prop}, s, s) - & k \in {\kw{n},\kw{e}}, s \in \mathcal{S} ~} \ + {~ (k, \kw{Prop}, s, s) & + k \in {\kw{n},\kw{e}}, s \in \mathcal{S} ~} \ \SMInsertBefore{\ensuremath{\cup ~}}{~ - (k, \Type {\ell}, \kw{Prop}, \kw{Prop}) - & k \in {\kw{n},\kw{e}}, \ell \in \mathbb{N} ~} \ + (k, \Type {\ell}, \kw{Prop}, \kw{Prop}) & + k \in {\kw{n},\kw{e}}, \ell \in \mathbb{N} ~} \ \SMInsertBefore{\ensuremath{\cup ~}}{~ - (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\Tmax{\ell_1}{\ell_2}}) - & k \in {\kw{n},\kw{e}}, \ell_1,\ell_2 \in\mathbb{N} ~} + (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\Tmax{\ell_1}{\ell_2}}) & + k \in {\kw{n},\kw{e}}, \ell_1,\ell_2 \in\mathbb{N} ~} \end{array} \end{array} \end{displaymath} @@ -739,13 +739,17 @@ second is redundant: \vspace{-\baselineskip} \end{proof}
+Let's call \kw{e}CCω the restriction of CCω where all arguments to +impredicative functions are erasable, +i.e.~$(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ is removed. + \begin{theorem}[Erasability of impredicative arguments in CCω] \mbox{} \ \normalfont %% - CCω's rule $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ is redundant since for any - derivation $\Jtype e \tau$ in CCω there is a corresponding derivation $\Jtype[\Gamma'] - {e'} {\tau'}$ in CCω$'$ which does not use that rule and where - $\Fforget{\Jtype e \tau} = \Fforget{\Jtype[\Gamma'] {e'} {\tau'}}$ + CCω's rule $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ is redundant since for + any derivation $\Jtype e \tau$ in CCω there is a corresponding derivation + $\Jtype[\Gamma'] {e'} {\tau'}$ in \kw{e}CCω such that $\Fforget{\Jtype e \tau} = + \Fforget{\Jtype[\Gamma'] {e'} {\tau'}}$ \end{theorem} \begin{proof} By induction on the type derivation of $e$ where we systematically replace @@ -816,7 +820,7 @@ as well. {\Jcic{\Ind{x}{\tau}{\vec a}}{\tau}}
\Infer{\Jcic e {\AppM{\tau_I}{p}} \ - \tau_I = \Ind{x}{\ArwM{z}{\tau_z}{\kw{Prop}}}{\vec a} \ + \tau_I = \Ind{x}{\ArwM{z}{\tau_z}{{Prop}}}{\vec a} \ \Jcic {\tau_r}{\ArwM{z}{\tau_z}{\Arw[n]{_}{\AppM{\tau_I}{z}}s}} \\ \forall i. \ a_i = {\ArwM[\ensuremath{c}]{y}{\tau_y}{\AppM{x}{p'}}} \ @@ -917,7 +921,7 @@ Two important details are worth pointing out: result of the case analysis is not in \kw{Prop}, i.e.~when this is a form of strong elimination, the inductive type must be small, meaning that all its fields must be in \kw{Prop}. This restriction is taken from - \citet{Werner94} who presents it slightly differently because he splits + \citet{Werner94}, with a slightly different presentation because he splits the \kw{Case} rule into two: one for weak elimination and one for strong elimination. \end{itemize} @@ -928,16 +932,17 @@ that recursive calls are made on structurally smaller terms. Their definition is not affected by the presence of erasability annotations and does not impact our work here.
-To show that the $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ rule of non-erasable +To show that the $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ rule of non-erasable impredicativity is still redundant in this new system, we proceed in the same way: \begin{lemma}[Confinement of impredicativity in CIC] \label{lem:erasable-cic} \mbox{} \ \normalfont %% FIXME: Make it a bit more formal? - In CIC, if $\Jtype{x}{\tau_x : \Type \ell}$ and + In CIC, if $\Jtype{x}{\tau_x:\Type{\ell}}$ and $\Jtype[\Gamma,x:\tau_x,\Gamma']{e}{\tau_e:\kw{Prop}}$, then $x$ can only appear in - $\Ferase e$ within arguments of function calls where the function has type - $(y:\tau_1) \TEarw \tau_2$ where $\tau_1 : \Type {\ell'}$ and $\tau_2 : \kw{Prop}$. + $\Ferase e$ within arguments to functions of type + $(y:\tau_1) \TEarw \tau_2$ where $\tau_2:\kw{Prop}$ and $\exists \ell'$ such that + $\tau_1:\Type{\ell'}$. \end{lemma} \begin{proof} The proof stays the same, with the following additional cases: @@ -955,20 +960,26 @@ way: $b_i$ are as well, hence we can also invoke the induction hypothesis on every $b_i$. %% \qed \end{itemize} + \vspace{-\baselineskip} \end{proof} + +Let's call \kw{e}CIC the restriction of CIC where all arguments to +impredicative functions and all large fields of inductive definitions are +erasable, i.e.~$(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ is removed. + \begin{theorem}[Erasability of impredicative arguments in CIC] \mbox{} \ \normalfont %% - CIC's rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ is redundant since for any + CIC's rule $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ is redundant since for any derivation $\Jtype e \tau$ in CIC there is a corresponding derivation $\Jtype[\Gamma'] - {e'} {\tau'}$ in CIC$'$ which does not use that rule and where + {e'} {\tau'}$ in \kw{e}CIC such that $\Fforget{\Jtype e \tau} = \Fforget{\Jtype[\Gamma'] {e'} {\tau'}}$ \end{theorem} \begin{proof} As before, by induction on the type derivation of $e$ where we systematically replace $\kw{n}$ with $\kw{e}$ on all functions, arrows, - and applications that previously relied on the rule $(\kw{n}, s, - \kw{Prop}, \kw{Prop})$. + and applications that previously relied on the rule + $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$. The interesting new case is when $e$ is of the form $\Case{\tau_r}{e'}{\vec b}$: as mentioned, the vector $\vec c$ of erasability annotations placed on a given constructor $a_i$ must match the erasability @@ -981,8 +992,8 @@ way: for functions in \kw{Prop} can only be annotated as erasable. And when $s$ is a higher universe the property is also verified because the $\Jsmall {\vec {\tau_y}}$ constraint imposes that none of the arguments are - in higher universes so they don't use the $(\kw{n}, s, \kw{Prop}, - \kw{Prop})$ rule. %% \qed + in higher universes so they don't use the + $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ rule. %% \qed \end{proof}
This shows that the erasability of System-F's impredicative type @@ -994,7 +1005,7 @@ inductive types.
The reason behind the $\Jsmall e$ special constraint on strong eliminations of CIC in Figure~\ref{fig:cic} is pretty -straightforward: without this restriction, we could use an Inductive type +straightforward: without this restriction, we could use an inductive type such as the following to ``smuggle'' a value of universe $\Type \ell$ in a box of universe \kw{Prop}: \begin{verbatim} @@ -1009,7 +1020,7 @@ constraint rejects the \texttt{unbox} definition. If we remove the $\Jsmall e$ constraint, the effect of such a \texttt{box}/\texttt{unbox} pair would be to lower any value of a higher universe to the \kw{Prop} universe and would hence defeat the purpose of the stratification introduced by the tower of -universes. This was first shown to be inconsistent by \citet{Coquand86b}. +universes. This was first shown to be inconsistent in \cite{Coquand86b}.
This restriction makes the system more complex since elimination is allowed from any inductive type to any universe except for the one special case of @@ -1035,13 +1046,16 @@ applicability of large inductive types. \begin{displaymath} \begin{array}{lcl} \mathcal{R} &=& - \MAlign{ - {~ (k, \kw{Prop}, s, s); - (\kw{e}, s, \kw{Prop}, \kw{Prop}) ~|~ s \in \mathcal{S} ~} \ - \cup ~{~ - (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\Tmax{\ell_1}{\ell_2}}) - ~|~ \ell_1,\ell_2 \in\mathbb{N} ~} - } + \begin{array}[t]{@{}l@{~~|~~}l} + {~ (k, \kw{Prop}, s, s) & + k \in {\kw{n},\kw{e}}, s \in \mathcal{S} ~} \ + \SMInsertBefore{\ensuremath{\cup ~}}{~ + (\kw{e},\Type{\ell},\kw{Prop},\kw{Prop}) & + k \in {\kw{n},\kw{e}}, \ell \in \mathbb{N} ~} \ + \SMInsertBefore{\ensuremath{\cup ~}}{~ + (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\Tmax{\ell_1}{\ell_2}}) & + k \in {\kw{n},\kw{e}}, \ell_1,\ell_2 \in\mathbb{N} ~} + \end{array} \end{array} \end{displaymath} \medskip \begin{mathpar} @@ -1063,28 +1077,27 @@ applicability of large inductive types. \end{figure}
While the $\Jsmall e$ constraint was added to avoid an inconsistency, this -same $\Jsmall e$ is also the key to making it possible to erase all the -large fields of impredicative inductive definitions, as we saw in the -previous section. - -Figure~\ref{fig:ecic} shows a refinement of CIC we call ECIC: just like -CIC$'$, it only has the $(\kw{e},s,\kw{Prop},\kw{Prop})$ rule and not the -$(\kw{n},s,\kw{Prop},\kw{Prop})$ rule, meaning that impredicativity can only -be used with erasable arguments and fields. But additionally it has -a further difference to CIC and CIC$'$ which is that its \kw{Case} rule does -not have the $\Jsmall e$ constraint. - +same $\Jsmall e$ is also the key to making our proof of erasability of +impredicative arguments work for CIC: it is the detail which makes it +possible to erase all the large fields of impredicative inductive +definitions, as we saw in the previous section. +This might be a coincidence, of course, yet it suggests a close alignment +between the needs of consistency and the need to keep impredicative +elements erasable. + +Figure~\ref{fig:ecic} shows a refinement of \kw{e}CIC we call ECIC whose +\kw{Case} rule does not have the $\Jsmall e$ constraint. ECIC is more elegant and regular than CIC thanks to the absence of this -special corner case, and it allows typing more terms than CIC$'$ and hence +special corner case, and it allows typing more terms than \kw{e}CIC and hence CIC. For instance in ECIC we can define the above $\Omega$ inductive type with an erasable $k$ and then prove the mentioned property (again with erasable $K_1$ and $K_2$).
-Note also that the lack of a $(\kw{n},s,\kw{Prop},\kw{Prop})$ rule, means we -cannot define a \texttt{box} as above in this system; instead we are limited -to making its content erasable. This in turn prevents us from defining -\texttt{unbox} since the \texttt{x'} would now be erasable so it cannot be -returned as-is from the elimination form. In other words, forcing +Note also that the lack of a $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ rule, +means we cannot define a \texttt{box} as above in this system; instead we +are limited to making its content erasable. This in turn prevents us from +defining \texttt{unbox} since the \texttt{x'} would now be erasable so it +cannot be returned as-is from the elimination form. In other words, forcing impredicative fields to be erasable also avoids this source of inconsistency usually avoided with the $\Jsmall e$ constraint. Based on this circumstantial evidence, we venture to state the following: @@ -1093,11 +1106,56 @@ circumstantial evidence, we venture to state the following: The ECIC system is consistent. \end{conjecture}
+\section{Non-erasable impredicativity in Coq and UTT} + +As noted in Section~\ref{sec:cic}, we were careful to restrict our inductive +types to live in \kw{Prop}. This was no accident: we can see in the proof +of confinement that we rely on this property to show the erasability of +impredicative arguments in CIC. More specifically, the lack of confinement +appears when we do a case analysis from an inductive type in $\Type{\ell}$ to +a return value in \kw{Prop}. + +\FIXME{Rework the rest of this section} + +We could relax this constraint by allowing +inductive types in higher universes but disallowing elimination from those +types to \kw{Prop}. This would be a kind of opposite to the outlawing of +strong elimination of large inductive types. With such a restriction, we +could then still show the erasability of impredicative arguments. + +But systems such as Coq and UTT~\cite{Luo92} allow impredicative definitions +in \kw{Prop}, inductive types in higher universes, and elimination from +those inductive types to \kw{Prop}. So, these systems are examples of +impredicativity which is not erasable, showing clearly that while +impredicativity and erasability seem to be strongly correlated, the kind of +erasability used in EPTS is not a necessary condition for impredicativity to +be consistent. + +\FIXME{Where is this going?} + +Concretely, the lack of confinement appears when we do a case analysis from +an inductive type in $\Type{\ell}$ to a return value in \kw{Prop}. +For example: +\begin{verbatim} + Inductive Ω : Type := + | int : Ω + | arw : Ω -> Ω -> Ω + | all : forall k:Type, (k -> Ω) -> Ω. +\end{verbatim} + +But the +confinement proof only breaks down in this one spot, which means that we +still cannot do very much with an object from $\Type{\ell}$ when we are in +a \kw{Prop} context, other than select a particular branch in a case +statement. This suggests that we might be able to recover erasability in +the following way: + + \section{Multiple levels of impredicativity}
-CCω accepts impredicative definitions but only in the bottom universe. -This is a restriction shared by all systems that support impredicative -definitions. This is a direct consequence of various paradoxes formalized +Like all known consistent systems that support impredicative +definitions, CCω accepts them only in the bottom universe. This is a direct +consequence of various paradoxes formalized in systems which allow impredicative definitions in more than one universe, such as those shown by \citet{Girard72}, \citet{Coquand94}, and \citet{Hurkens95}. The last two showed a paradox in the system $\lambda U^-$ @@ -1108,16 +1166,18 @@ which can be defined as an EPTS as follows: \mathcal{A} &=& {~ (*,~\square), (\square,~\mathrm{\Delta}) ~} \ \mathcal{R} &=& {~ \MAlign{ - (k,*,*,*),~(k,\square,*,*),~(k,\mathrm{\Delta},*,*), \ + (k,*,*,*),~(k,\square,*,*),~%% ~(k,\mathrm{\Delta},*,*), + %% \ (k,\square,\square,\square),~(k,\mathrm{\Delta},\square,\square) \hspace{40pt}~|~ k \in {\kw{n},\kw{e}} ~} } \end{array} \end{displaymath} -Of the five pairs of rules, three are impredicative: $(k,\square,*,*)$, -$(k,\mathrm{\Delta},*,*)$, and $(k,\mathrm{\Delta},\square,\square)$, but since $*$ is the bottom -universe and hence corresponds to \kw{Prop} in CCω, the first two are -generally considered safe and are included in CCω. The new one is +Of the four pairs of rules, two are impredicative: $(k,\square,*,*)$ %% , +%% $(k,\mathrm{\Delta},*,*)$, +and $(k,\mathrm{\Delta},\square,\square)$, but since $*$ is the bottom +universe and hence corresponds to \kw{Prop} in CCω, the first is +generally considered safe and is included in System-F and CCω. The new one is $(k,\mathrm{\Delta},\square,\square)$ which introduces impredicativity in the second universe, $\square$.
@@ -1127,16 +1187,15 @@ be shown. The statement of the lemma would look like the following: \label{lem:erasable-lU} \mbox{} \ \normalfont In $\lambda U^-$, if $\Jtype{x}{\tau_x : s_1}$ and $\Jtype[\Gamma,x:\tau_x,\Gamma']{e}{\tau_e:s_2}$ and $s_1 > s_2$, then $x$ can only - appear in $\Ferase e$ within arguments to functions of type $(y:\tau_1) - \TEarw \tau_2$ where $\tau_1 : s_3$ and $\tau_2 : s_4$ and $s_3 > s_4$. + appear in $\Ferase e$ within arguments to functions of type + $(y:\tau_1)\TEarw \tau_2$ where $\tau_1 : s_3$ and $\tau_2 : s_4$ and $s_3 > s_4$. \end{lemma} -When we attempt to adapt the earlier proof for CCω, most of the proof works -largely unchanged, except when we get to the case where $e$ is of the form -$\Arw{y}{\tau_1}{\tau_2}$: we can invoke the induction hypothesis on $\tau_2$ because -it necessarily lives in the same universe as $e$, but we cannot invoke the -induction hypothesis on $\tau_1$ if $x$ is in the universe $\mathrm{\Delta}$, -because $\tau_1$ might itself also be in the universe $\mathrm{\Delta}$ because of -the $(k,\mathrm{\Delta},\square,\square)$ rule. +When we attempt to adapt the earlier proof for CCω, is breaks down when $e$ +is of the form $\Arw{y}{\tau_1}{\tau_2}$: we can invoke the induction hypothesis +on $\tau_2$ because it necessarily lives in the same universe as $e$, but we +cannot invoke the induction hypothesis on $\tau_1$ if $x$ is in the universe +$\mathrm{\Delta}$, because $\tau_1$ might itself also be in the universe +$\mathrm{\Delta}$ because of the $(k,\mathrm{\Delta},\square,\square)$ rule.
\begin{figure}[tb] \begin{displaymath} @@ -1172,15 +1231,15 @@ the $(k,\mathrm{\Delta},\square,\square)$ rule. \label{fig:hurkens} \end{figure}
-Following the same idea as in the previous section where we relied on -erasability to avoid inconsistency, we could thus define a new $\lambda EU^-$ -calculus that only allows the use of impredicativity with erasable +Following the same idea as in the previous section where we defined ECIC to +rely on erasability to avoid inconsistency, we could thus define a new $\lambda +EU^-$ calculus that only allows the use of impredicativity with erasable abstractions: \begin{displaymath} \begin{array}{lcl} \mathcal{R} &=& {~ \MAlign{ - (k,*,*,*),~(\kw{e},\square,*,*),~(\kw{e},\mathrm{\Delta},*,*), \ + (k,*,*,*),~(\kw{e},\square,*,*),~%% (\kw{e},\mathrm{\Delta},*,*), \ (k,\square,\square,\square),~(\kw{e},\mathrm{\Delta},\square,\square) \hspace{40pt}~|~ k \in {\kw{n},\kw{e}} ~} } @@ -1194,14 +1253,14 @@ this is not the case: $\lambda EU^-$ is not consistent. \end{theorem} \begin{proof} - The proof is the same as the proof of inconsistency of $\lambda U^-$ shown by + The proof is the same as the proof of inconsistency of $\lambda U^-$ shown in \citet{Hurkens95}. Figure~\ref{fig:hurkens} shows Hurken's original proof, using the same notation he used in his paper. To show that the proof also applies to $\lambda EU^-$, we need to make sure that all impredicative abstractions can be annotated as erasable. For that, it - suffices to know that the integers are variable names, the two - impredicative abstractions in $*$ are introduced by \kw{let}, the two - corresponding applications are denoted with $\langle e_1~e_2\rangle$, the + suffices to know that the integers are variable names, the + impredicative abstraction in $*$ is introduced by \kw{let}, the + corresponding application is denoted with $\langle e_1~e_2\rangle$, the impredicative abstraction in $\square$ is introduced by $\Lambda$, and the corresponding application is denoted with ${e_1~e_2}$: by inspection we can see that all the arguments introduced by impredicative abstractions @@ -1209,25 +1268,6 @@ this is not the case: impredicative functions. %% \qed \end{proof}
-\section{Non-erasable impredicativity} - -As noted in Section~\ref{sec:cic}, we were careful to restrict our inductive -types to live in \kw{Prop}. This was no accident: we can see in the proof -of confinement that we rely on this property to show the erasability of -impredicative arguments in CIC. We could relax this constraint by allowing -inductive types in higher universes but disallowing elimination from those -types to \kw{Prop}. This would be a kind of opposite to the outlawing of -strong elimination of large inductive types. With such a restriction, we -could then still show the erasability of impredicative arguments. - -But systems such as Coq and UTT~\cite{Luo92} allow impredicative definitions -in \kw{Prop}, inductive types in higher universes, and elimination from -those inductive types to \kw{Prop}. So, these systems are examples of -impredicativity which is not erasable (at least not in the sense we use -here), showing clearly that while impredicativity and erasability seem to be -correlated, erasability is not a necessary condition for impredicativity to -be consistent. - %% \section{Related work}
%% \nocite{Gimenez94}
View it on GitLab: https://gitlab.com/monnier/typer/commit/3bd4089e00cfe9f7c6495e792f8171c2d660...