[Git][monnier/typer][report/tcvi] - - Typer

20 Nov 2019


      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...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/commit/3bd4089e00cfe9f7c6495e792f8171c2d660...
You're receiving this email because of your account on gitlab.com.





    