Stefan pushed to branch report/tcvi at Stefan / Typer

Commits: ca86b2d0 by Stefan Monnier at 2018-11-13T07:04:37Z -

- - - - -

2 changed files:

- paper.tex - refs.bib

Changes:

===================================== paper.tex ===================================== @@ -65,6 +65,14 @@ \DeclareUnicodeCharacter{2980}{\ensuremath{|||}} \DeclareUnicodeCharacter{2081}{\ensuremath{_1}} \DeclareUnicodeCharacter{2082}{\ensuremath{_2}} +\DeclareUnicodeCharacter{21D2}{\ensuremath{\Rightarrow}} +\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}} +\DeclareUnicodeCharacter{03C3}{\ensuremath{\sigma}} +\DeclareUnicodeCharacter{03BB}{\ensuremath{\lambda}} +\DeclareUnicodeCharacter{03C4}{\ensuremath{\tau}} +\DeclareUnicodeCharacter{0394}{\ensuremath{\Delta}} +\DeclareUnicodeCharacter{1D4C5}{\ensuremath{\wp}} +\DeclareUnicodeCharacter{1D4B0}{\ensuremath{\mathcal{U}}}

%% The doc says `vcenter` should work, but I get an error :-( %% \newcommand \Infer[1][] [\inferrule*[vcenter,right=#1]] @@ -159,18 +167,18 @@ %% \input{commands}

\begin{abstract} - Of all the threats to the consistency of a type system, such as side - effects and recursion, impredicativity is arguably the least understood. - In this paper, we revisit several type systems which do include some form - of impredicativity and show that they can be refined to equivalent systems - where impredicativity can be erased, in a stricter sense than the kind of - proof irrelevance notion used for example for \kw{Prop} terms in systems - like Coq. - - We hope these observations will lead to a better understanding of why and - when impredicativity is sound. As a first step in this direction, we - discuss how these results suggest some extensions of those systems which - might still enjoy consistency. +Of all the threats to the consistency of a type system, such as side +effects and recursion, impredicativity is arguably the least understood. +In this paper, we revisit several type systems which do include some form +of impredicativity and show that they can be refined to equivalent systems +where impredicativity can be erased, in a stricter sense than the kind of +proof irrelevance notion used for example for \kw{Prop} terms in systems +like Coq. + +We hope these observations will lead to a better understanding of why and +when impredicativity is sound. As a first step in this direction, we +discuss how these results suggest some extensions of those systems which +might still enjoy consistency. \end{abstract}

%% 2012 ACM Computing Classification System (CSS) concepts @@ -179,7 +187,8 @@ %% %% ... %% \end{CCSXML}

-%% \keywords{Inductive types} +%% \keywords{Impredicativity, Pure type systems, Inductive types, Erasable +%% arguments, Proof irrelevance, Implicit arguments}

%% Note: \begin{abstract}...\end{abstract} environment must come %% before \maketitle command in ACM style. @@ -253,14 +262,14 @@ The contributions of this work are: fields of inductive types are also erasable. \item A suggestion for how to consistently extend CIC with strong elimination of large inductive types. -\item A suggestion for how to consistently extend CCω with impredicativity - in other universes than the bottom one. \FIXME{really?} +\item A proof that the same idea cannot similarly be used to consistently + extend CCω with impredicativity in other universes than the bottom one. \item A sketch of 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}. -\item The observation that ICC's stronger conversion rule may not be as - strong as it seems. \FIXME{really?} +%% \item The observation that ICC's stronger conversion rule may not be as +%% strong as it seems. \FIXME{really?} \end{itemize}

\section{Background} @@ -583,13 +592,13 @@ in any $\Type \ell$. This rule is really a shorthand for two separate rules: $(\kw{e}, s, \kw{Prop}, \kw{Prop})$ and $(\kw{n}, s, \kw{Prop}, \kw{Prop})$. And we will now show that the second is redundant:

-\begin{lemma}[Confinement of impredicativity] +\begin{lemma}[Confinement of impredicativity in CCω] \label{lem:erasable} \ \normalfont %% FIXME: Make it a bit more formal? In CCω, 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 to functions of type $(y:\tau_1) \TEarw \tau_2$ where - $\tau_2 : \kw{Prop}$ and $\tau_1 : \Type {\ell'}$. + $\tau_1 : \Type {\ell'}$ and $\tau_2 : \kw{Prop}$. \end{lemma} \begin{proof} %% FIXME: Expand! @@ -611,7 +620,7 @@ And we will now show that the second is redundant: \end{itemize} \end{proof}

-\begin{theorem}[Erasability of impredicative arguments] +\begin{theorem}[Erasability of impredicative arguments in CCω] \ \normalfont %% CCω's rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ is redundant since for any @@ -639,6 +648,7 @@ abstractions can be extended to all of CCω's impredicative abstractions as well.

\section{Erasing impredicative arguments of CIC} +\label{sec:cic}

\newcommand \Ind[3] {\kw{Ind}(#1:#2)\langle#3\rangle} \newcommand \Con[2] {\kw{Con}(#1,#2)} @@ -652,6 +662,11 @@ as well. \newcommand \Jdecreasing[3][x_f;i;x_i] {#1;#2 \vdash #3;;\kw{term}} \newcommand \Jsmall[2][\Gamma] {#1 \vdash #2;;\kw{small}}

+\newcommand \IndE[2] {\kw{Ind}(#1)\langle#2\rangle} +\newcommand \ConE[1] {\kw{Con}(#1)} +\newcommand \CaseE[2] {\kw{Case}~#1 ~\kw{of}~\langle#2\rangle} +\newcommand \FixE[1] {\kw{Fix}~#1~=~} + \begin{figure}[tb] \begin{mathpar} %% \ovalbox{\ensuremath{ @@ -755,11 +770,6 @@ not, is available within the corresponding \kw{Case} branch but those marked as erasable in the \kw{Ind} definition will accordingly only be available as erasable within \kw{Case}.

-\newcommand \IndE[2] {\kw{Ind}(#1)\langle#2\rangle} -\newcommand \ConE[1] {\kw{Con}(#1)} -\newcommand \CaseE[2] {\kw{Case}~#1 ~\kw{of}~\langle#2\rangle} -\newcommand \FixE[1] {\kw{Fix}~#1~=~} - Figure~\ref{fig:cic} shows the typing rules corresponding to each of those four new constructs. We use $_$ at a few places where the actual element does not matter enough to give it a name. The notation $\AppM f e$ @@ -800,13 +810,13 @@ and does not impact our work here. To show that the $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ rule of non-erasable impredicativity is still redundant in this new system, we proceed in the say way: -\begin{lemma}[Confinement of impredicativity] +\begin{lemma}[Confinement of impredicativity in CIC] \label{lem:erasable-cic} \ \normalfont %% FIXME: Make it a bit more formal? 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_2 : \kw{Prop}$ and $\tau_1 : \Type {\ell'}$. + $(y:\tau_1) \TEarw \tau_2$ where $\tau_1 : \Type {\ell'}$ and $\tau_2 : \kw{Prop}$. \end{lemma} \begin{proof} The proof stays the same, with the following additional cases: @@ -825,14 +835,14 @@ way: every $b_i$. \qed \end{itemize} \end{proof} -\begin{corollary}[Erasability of impredicative arguments] +\begin{theorem}[Erasability of impredicative arguments in CIC] \ \normalfont %% CIC's rule $(\kw{n}, s, \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 $\Fforget{\Jtype e \tau} = \Fforget{\Jtype[\Gamma'] {e'} {\tau'}}$ -\end{corollary} +\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, @@ -863,38 +873,28 @@ 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 make 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} + Inductive Box (t : Type): Prop := + | box : t -> Prop. + Definition unbox (t : Type) (x : Box t) := match x with + | box x' => x' + end. +\end{verbatim} +Note that such a box is perfectly valid in CIC, but the $\Jsmall e$ +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}. + +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 +strong elimination of large inductive types. It also significantly weakens +the system. For example while we can define in Coq a large inductive type like: -\begin{displaymath} - FIXME -\end{displaymath} -. The reason - -If we extend ICC* with inductive types like those of \citet{Werner94}, -i.e.~inductive types that can be impredicative but that are confined to the -bottom universe (i.e. \kw{Prop}/\kw{Set}), then the property expressed by -the previous lemma still holds: we can make all the impredicative arguments -to functions and constructors erasable! - -I put a ``!'' here because it doesn't come straightforwardly: a field of an -inductive type is a data that will become available again in different -contexts, and depending on the elimination form in which it appears, some of -those contexts will return values in the \kw{Prop} universe, while other -will return it in other universes. - -An inductive object may appear in an \kw{Elim} which returns a \kw{Prop} but -also an in \kw{Elim} which returns a $\Type\ell$. In the first case, -a field of type $\Type{\ell'}$ could just as well be erasable, according to -the induction hypothesis of the lemma. But what about the second case? -Well, the second case is impossible: -%% -CIC has a special restriction that large inductive types (i.e.~inductive -types that belong to a universe that is smaller than some of the values it -carries) cannot be used in a strong elimination (i.e.~a \kw{case} analysis -that returns a type in a universe larger than that of the object analyzed). - -This restriction means for example that while we can define in Coq -a large inductive type like: \begin{verbatim} Inductive Ω : Set := | int : Ω @@ -907,53 +907,207 @@ while working on~\cite{Monnier07}): forall K₁ K₂ F₁ F₂ P, all K₁ F₁ = all K₂ F₂ -> P K₁ F₁ -> P K₂ F₂. \end{verbatim} -This important restriction significantly reduces the applicability of large -inductive types, but is needed because it would be otherwise possible -to ``smuggle'' a large element within an inductive object of a smaller -universe and take it back out later, resulting in -unsoundness~\cite{Coquand86b}. - -Since Typer's impredicativity is limited to erasable elements, those large -elements cannot really be taken back out later anyway, by virtue of their -erasability. For this reason, we \emph{conjecture} that our form of -impredicativity does not require this restriction on strong elimination. -As a consequence, in Typer we can define the above inductive type (with an -erasable $k$) and prove its property (again with erasable $K_1$ and $K_2$). - -The weak justification behind it, is a philosophical one: erasable arguments -are not \emph{significant}, so a function that takes an erasable argument -could be considered as a mere ``schema'' or ``prototype'' which stands for -all the specialized versions of the function. A similar argument is -discussed by Fruchart and Longo in~\cite{Fruchart96}. - -So Typer's ``impredicative erasables'' is a superset of ICC* and of -the version of CIC described in \citet{Werner94}. - -The first question is: is it sound to extend CIC by allowing \emph{strong - elimination} on large inductive types, under the condition that all the -``large'' fields are erasable? - -\subsection{Non-erasable impredicativity} +In practice, this important restriction significantly reduces the +applicability of large inductive types. + +\begin{figure}[bt] + \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 {\ell_1 \sqcup \ell_2}) + ~|~ \ell_1,\ell_2 \in\mathbb{N} ~} + } + \end{array} + \end{displaymath} \medskip + \begin{mathpar} + \Infer{\Jcic e {\AppM{\tau_I}{p}} \ + \tau_I = \Ind{x}{\ArwM{z}{\tau_z}{\kw{Prop}}}{\vec a} \ + \Jcic {\tau_r}{\ArwM{z}{\tau_z}{\Arw[n]{_}{\AppM{\tau_I}{z}}s}} \\ + \forall i.\hspace{-1pt} \ + a_i = {\ArwM[\ensuremath{c}]{y}{\tau_y}{\AppM{x}{p'}}} \ + %% \\ + %% \forall i. \ + \Jcic {b_i} + {\ArwM[\ensuremath{c}]{y}{\Subst{\tau_y}{x}{\tau_I}} + {\App[n]{\AppM{\tau_r}{p'}}{(\AppM[\ensuremath{c}]{\Con{i}{\tau_I}}{y})}}} + } + {\Jcic{\Case{\tau_r}{e}{\vec b}}{\App[n]{\AppM{\tau_r}{p}}e}} + \end{mathpar} + \caption{Rules of the ECIC system} + \label{fig:ecic} +\end{figure}

-If we extend the system yet further in the direction of Coq, i.e. we allow -inductive types that live in other universes than \kw{Prop}, -Lemma~\ref{lem:erasable} does not hold any more because we can perform -a \kw{case} analysis on an argument in universe $\Type\ell$ and return -something in universe \kw{Prop}. +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. + +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 +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 +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: + +\begin{conjecture} + The ECIC system is consistent. +\end{conjecture} + +\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 +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^-$ +which can be defined as an EPTS as follows: +\begin{displaymath} + \begin{array}{lcl} + \mathcal{S} &=& {~ *,~\square,~\mathrm{\Delta} ~} \ + \mathcal{A} &=& {~ (*,~\square), (\square,~\mathrm{\Delta}) ~} \ + \mathcal{R} &=& + {~ \MAlign{ + (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 sets 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 +$(k,\mathrm{\Delta},\square,\square)$ which introduces impredicativity in the second +universe, $\square$. + +In such a system, the lemma of confinement of impredicativity cannot +be shown. The statement of the lemma would look like the following: +\begin{lemma}[Confinement of impredicativity in $\lambda U^-$] + \label{lem:erasable-lU} \ \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$. +\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. + +\begin{figure} + \begin{displaymath} + \begin{array}{c} + \begin{array}{l@{;;=;;}l} + \mathcal{U} & + \Pi\mathcal{X}:\square.((𝓅𝓅\mathcal{X}\to\mathcal{X})\to 𝓅𝓅\mathcal{X}) \ + \tau t & + \Lambda\mathcal{X}:\square.\lambda f:(𝓅𝓅\mathcal{X}\to\mathcal{X}).\lambda p:𝓅\mathcal{X}. + (t~\lambda x:\mathcal{U}.(p~(f~({x~\mathcal{X}}~f)))) \ + \sigma s & + ({s~\mathcal{U}}~\lambda t:𝓅𝓅\mathcal{U}.\tau t) \ + \Delta & \lambda y:\mathcal{U}.\neg \forall p:𝓅\mathcal{U}.[(\sigma y~p) \Rightarrow (p~\tau \sigma y)] \ + \Omega & \tau~\lambda p:𝓅\mathcal{U}.\forall x:\mathcal{U}.[(\sigma x~p) \Rightarrow (p~x)] + \end{array} \bigskip \bigskip \ + \MAlign{ + [~\MAlign{ + \kw{suppose}~0:∀p : 𝓅𝒰. [∀x : 𝒰. [(σx~p) ⇒ (p~x)] ⇒ (p~Ω)]. \{} + [~\MAlign{ + [\langle0 Δ\rangle~\MAlign{ + \kw{let}~x:𝒰 . \ + \kw{suppose}~2:(σx~Δ). \ + \kw{suppose}~3:(∀p : 𝓅𝒰. [(σx~p) ⇒ (p~τσx)]). \{} + [[\langle3~Δ\rangle~2]~\kw{let}~p:𝓅𝒰. \langle3~λy:𝒰.(p~τσy)\rangle]] } \ + \kw{let}~p:𝓅𝒰. \langle0~λy:𝒰.(p~τσy)\rangle] } \ + \kw{let}~p:𝓅𝒰. \ + \kw{suppose}~1:∀x:𝒰.[(σx~p) ⇒ (p~x)]. \{} + [\langle1~Ω\rangle~\kw{let}~x : 𝒰 . \langle1~τσx\rangle]] + }} + \end{array} + \end{displaymath} + \caption{Hurken's paradox} + \label{fig:hurkens} +\end{figure}

-So, here we finally meet a system with impredicativity where that -impredicativity applies to arguments which are \emph{not} erasable! -To me, these sound fishy. -I'd like to see a proof of consistency of such a system. +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 +abstractions: +\begin{displaymath} + \begin{array}{lcl} + \mathcal{R} &=& + {~ \MAlign{ + (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}} ~} + } + \end{array} +\end{displaymath} +The failure to prove the confinement lemma in $\lambda U^-$ shows clearly that $\lambda +EU^-$ can type fewer terms than $\lambda U^-$. This might make us hopeful that +maybe it's sufficiently weaker to avoid the inconsistency of $\lambda U^-$. Alas, +this is not the case: +\begin{theorem} + $\lambda EU^-$ is not consistent. +\end{theorem} +\begin{proof} + The proof is the same as the proof of inconsistency of $\lambda U^-$ shown by + \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 + 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 + are exclusively used either in type annotations or in arguments to other + impredicative functions. \qed +\end{proof}

-For this reason, while the restriction of impredicativity to erasable -functions does not make Typer weaker than ICC*or CIC it does make it in this -respect weaker than Coq. But Typer is incomparable to Coq because in -another respects it allows things that Coq does not. +\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 of 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} +%% \section{Related work}

%% \nocite{Gimenez94} %% \nocite{Blume06,Castagna16} %Union types and extensible sums @@ -963,6 +1117,19 @@ another respects it allows things that Coq does not.

\section{Conclusion}

+We have taken a tour of the interactions between impredicativity and +erasability of arguments in EPTS. We have shown that 3 of the most well +known systems that admit impredicativity do it in a way to constrains all +impredicative abstractions and fields to be erasable. We have also shown +while impredicativity and erasability seem to be correlated, erasability is +neither a necessary nor a sufficient condition for impredicativity to +be consistent, by showing that UTT's impredicative definitions are not all +erasable and showing that $\lambda EU^-$ is not consistent. + +It remains to be seen whether erasability as used in ECIC allows us to lift +the restriction that strong elimination cannot be used on large inductive +types without breaking consistency. + \newenvironment{acks}{\subsection*{Acknowledgments}}{} \newcommand \grantsponsor[3] {#2 (#1)} \newcommand \grantnum[2] {#2}

===================================== refs.bib ===================================== @@ -293,6 +293,16 @@ url = {http://www.cs.rhul.ac.uk/~zhaohui/TVER92.ps%7D, }

+@inproceedings{Coquand86b, + author = {Thierry Coquand}, + booktitle = {Annual Symposium on Logic in Computer Science}, + key = {LICS'86}, + note = {Also published as INRIA tech-report RR-0531}, + title = {An Analysis of {G}irard's Paradox}, + year = {1986}, + url = {https://hal.inria.fr/inria-00076023%7D, +} + @inproceedings{Monnier07, address = {Freiburg, Germany}, author = {Stefan Monnier}, @@ -338,12 +348,40 @@ \kw{cast} more obvious.}, }

-@inproceedings{Coquand86b, +@phdthesis{Girard72, + author = {J. Y. Girard}, + school = {University of Paris VII}, + title = {Interprétation Fonctionnelle et Élimination des + Coupures dans l'Arithmétique d'Ordre Supérieur}, + year = {1972}, +} + +@inproceedings{Coquand94, author = {Thierry Coquand}, - booktitle = {Annual Symposium on Logic in Computer Science}, - key = {LICS'86}, - title = {An Analysis of {G}irard's Paradox}, - year = {1986}, + booktitle = {Logic, Methodology, and Philosophy of Science}, + pages = {7-14}, + title = {A New Paradox in Type Theory}, + year = {1994}, + abstract = {This paper is to present a new paradox for Type + Theory, which is a type-theoretic refinement of + Reynolds' result [24] that there is no set-theoretic + model of polymorphism. We discuss then one + application of this paradox, which shows unexpected + connections between the principle of excluded middle + and the axiom of description in impredicative Type + Theories.}, + url = {ftp://ftp.cs.chalmers.se/pub/users/coquand/nyparadox.ps.Z}, +} + +@inproceedings{Hurkens95, + author = {Antonius Hurkens}, + booktitle = {International conference on Typed Lambda Calculi and + Applications}, + key = {TLCA'95}, + pages = {266-278}, + title = {A simplification of {G}irard's paradox}, + year = {1995}, + url = {http://www.cs.cmu.edu/~kw/scans/hurkens95tlca.pdf%7D, }

@proceedings{FOSSACS08, @@ -377,6 +415,15 @@ year = {1986}, }

+@proceedings{TLCA95, + booktitle = {International conference on Typed Lambda Calculi and + Applications}, + key = {TLCA'95}, + title = {International conference on Typed Lambda Calculi and + Applications}, + year = {1995}, +} + @proceedings{LFCS92, booktitle = {Logical Foundations of Computer Science}, key = {Logic at TVER'92},

View it on GitLab: https://gitlab.com/monnier/typer/commit/ca86b2d07df75f380bd8263ed87c7167d723...