Stefan pushed to branch report/tcvi at Stefan / Typer

Commits: dd80bc98 by Stefan Monnier at 2019-11-20T02:57:07Z Explain the Conv case in the CCw proof

- - - - -

2 changed files:

- paper.tex - refs.bib

Changes:

===================================== paper.tex ===================================== @@ -296,7 +296,7 @@ systems such as System-F are not predicative yet they are generally believed to be consistent. Some people reject impredicativity outright, and indeed systems like Agda~\cite{Bove09} demonstrate that impredicativity is not indispensable to get a powerful logic. Yet, many popular systems, like -Coq~~\cite{Coq00}, do include some limited form of impredicativity, +Coq~\cite{Coq00}, do include some limited form of impredicativity, although those limits tend to feel somewhat ad-hoc, making the overall system more complex, with unsatisfying corner cases. For this reason we feel there is a need to try and better understand what those limits to impredicativity @@ -312,14 +312,23 @@ might be acceptable as long as those arguments are not used in what we could describe as a ``significant'' way, so we investigate here whether erasability might be such a notion of ``insignificance''.

-Arguably, such a link between impredicativity and erasure is already -evidenced by systems like Coq whose impredicative universe is also erasable, -and even more so by the propositional resizing axiom~\cite{HoTT} which -allows impredicativity for all \emph{mere propositions}, i.e.~types whose -inhabitants are all provably equal and hence erasable. But we here link -impredicativity to the somewhat different notion of erasability of arguments -which are only used in type annotations, such as the \emph{implicit} -arguments in ICC* and EPTS~\cite{Barras08,MishraLinger08}. +The two main instances of impredicativity in modern type theory are probably +the typical Coq's \kw{Prop} universe, which is designed to be erasable, +and the propositional resizing axiom~\cite{HoTT} which allows +impredicativity for all \emph{mere propositions}, i.e.~types whose +inhabitants are all provably equal and hence erasable. For this reason, it +is no ground breaking revelation to claim that there is an affinity between +impredicativity and erasability, yet it is still unclear to what extent the +two belong together nor which particular form of erasability would be the +true soulmate or impredicativity. + +Coq and and the propositional resizing axiom basically link impredicativity +to the concept of erasure usually called \emph{proof irrelevance}, where an +argument is deemed erasable if its type has at most one inhabitant. In the +following sections, we show an affinity between impredicativity and the +somewhat different notion of erasability found in systems like ICC* and +EPTS~\cite{Barras08,MishraLinger08}, where an argument is deemed erasable if +the function only uses it in type annotations.

More specifically, we take various impredicative systems and refine them with annotations of \emph{erasability}, and then show that all impredicative @@ -335,13 +344,14 @@ may be able to recover consistency.%% While there is admittedly ample room in

The contributions of this work are: \begin{itemize} -\item A proof that in CCω all impredicative functions actually take - erasable arguments. -\item A proof that in CIC all impredicative functions take erasable - arguments and that all \emph{large} fields of inductive types are +\item A proof that in CCω all arguments to impredicative functions + are erasable. +\item A proof that in the CIC resulting from extending CCω with inductive + types in the impredicative universe, all arguments to impredicative + functions and all \emph{large} fields of inductive types are also erasable. -\item A potentially consistent extension of CIC with strong - elimination of large inductive types. +\item A proposal for how to extend CIC with strong elimination of large + inductive types that might plausibly preserve consistency. \item A proof that the same idea does not allow impredicativity in more than one universe. \item As needed for some of the above contributions, we sketch a calculus @@ -358,6 +368,8 @@ The contributions of this work are:

Here we present the notion of erasability we use in the rest of the paper.

+\subsection{Erasable Pure Type Systems} + %% \section{Core language}

\newcommand \TEarw[1][\ensuremath{k}] {\stackrel{\kw{#1}}{\to}} @@ -414,12 +426,12 @@ Here we present the notion of erasability we use in the rest of the paper. \end{figure}}

The calculi we use in this paper are erasable pure type systems (EPTS) -\cite{MishraLinger08}, which are pure type systems~\cite{Barendregt91b} -extended with a notion of erasability. We use a notation that makes it -more clear that the erasability is just an annotation like that of colored -pure type systems (CPTS) \cite{Bernardy12} where the color indicates which -arguments are \Char{\kw{n}}ormal and which are \Char{\kw{e}}rasable. -The syntax of the terms is defined as follows: +\cite{MishraLinger08}, which are pure type systems +(PTS)~\cite{Barendregt91b} extended with a notion of erasability. We use +a notation that makes it more clear that the erasability is just an +annotation like that of colored pure type systems (CPTS)~\cite{Bernardy12} +where the color indicates which arguments are \Char{\kw{n}}ormal and which +are \Char{\kw{e}}rasable. The syntax of the terms is defined as follows: \begin{displaymath} \begin{array}{lccl} %% \textsl{(level)} & \ell &\in& \mathbb{N} \ @@ -503,44 +515,48 @@ corresponding PTS is consistent, the EPTS is also consistent.

\subsection{Kinds of erasability}

-The claim that impredicative definitions can be erased could be considered -as trivial if we consider that Coq's only impredicative universe is -\kw{Prop} and that it is also the universe that gets erased during -program extraction. But the kind of erasability we use in this article is -different from that offered by Coq's irrelevance of \kw{Prop}: the only -thing you can do with an erasable argument in an EPTS is to pass it around -until you finally put it inside a type annotation. - -On a related note, the main difference between the rules of our EPTS and -those of ICC~\cite{Miquel01} and ICC*\cite{Barras08}, is that our -\textsc{Conv} rule requires convertibility of the fully explicit types, -whereas ICC and ICC* use a rule where convertibility is checked after -erasure, such as: +The claim that arguments to impredicative functions can be erased could be +considered as trivial if we consider that Coq's only impredicative universe +is \kw{Prop} and that it is also the universe that gets erased during +program extraction. + +But the kind of erasability we use in this article is different from that +offered by Coq's irrelevance of \kw{Prop}: on the one hand it's more +restrictive since the only thing you can do with an erasable argument in an +EPTS is to pass it around until you finally put it inside a type annotation, +on the other it's more flexible because any argument can be erasable, +regardless of its type. + +On a related note, the rules of our EPTS are slightly different from those +of ICC~\cite{Miquel01} and ICC*\cite{Barras08}, in that our \textsc{Conv} +rule requires convertibility of the fully explicit types, whereas ICC and +ICC* use a rule where convertibility is checked after erasure: \begin{displaymath} \Infer{\Jtype {e} {\tau_1} \ - \Jtype {\tau_2} s \ + \Jtype {\tau_2} s \ \Ferase{\tau_1} \simeq \Ferase{\tau_2}} {\Jtype {e} {\tau_2}} \end{displaymath} -We do not use this stronger rule here because it would make it untrue that -every well-typed term $e$ in an EPTS $S$ has a corresponding well-typed term -$\Fforget e$ in $\Fforget S$, so the consistency of the corresponding PTS -would not automatically carry over to the EPTS. - -\citet{Barras08} argue in favor of using such a stronger rule by showing -some example applications where it is able to equate more terms by erasing -(and hence ignoring) some proofs, in a sense internalizing a form of proof -irrelevance similar to that of Coq. But those examples all rely on -additional axioms. And in practice it appears this stronger rule brings -tangible benefits only after we add further axioms to the system. -More specifically, in a context like ours where we do not use -additional axioms, since erasable arguments can only appear in type -annotations, erasability is basically restricted to abstractions over the -``domain of discourse'' as is the case with the type abstractions of -System-F, rather than abstractions over witnesses, as used with Coq's -\kw{Prop}. Another way to say it is that, in types of the form -$\Arw[e]{x}{\tau_1}{\tau_2}$, the argument $x$ needs to appear in $\tau_2$ to be of -any use. +The rule we use is weaker but it is sufficient for our needs and makes it +immediately obvious that every well-typed term $e$ in an EPTS $S$ has +a corresponding well-typed term $\Fforget e$ in $\Fforget S$.%% otherwise the +%% consistency of the corresponding PTS might not automatically carry over to +%% the EPTS. + +%% \citet{Barras08} argue in favor of using such a stronger rule by showing +%% some example applications where it is able to equate more terms by erasing +%% (and hence ignoring) some proofs, in a sense internalizing a form of proof +%% irrelevance similar to that of Coq. But those examples all rely on +%% additional axioms. And in practice it appears this stronger rule brings +%% tangible benefits only after we add further axioms to the system. +%% More specifically, in a context like ours where we do not use +%% additional axioms, since erasable arguments can only appear in type +%% annotations, erasability is basically restricted to abstractions over the +%% ``domain of discourse'' as is the case with the type abstractions of +%% System-F, rather than abstractions over witnesses, as used with Coq's +%% \kw{Prop}. Another way to say it is that, in types of the form +%% $\Arw[e]{x}{\tau_1}{\tau_2}$, the argument $x$ needs to appear in $\tau_2$ to be of +%% any use.

%% FIXME: Maybe include the counter example, and maybe the second conjecture %% (especially if we can turn it into a lemma!) @@ -638,9 +654,18 @@ any use.

\section{Erasing impredicative arguments of CCω}

+\FIXME{Abel mentions in~\cite{Abel13} that in the pure CoC, dependent + arguments are always erasable, but that this doesn't hold any more + once we add inductive types and ``recursion''. Not sure why/how} + In this section we show that impredicative arguments in the calculus of constructions extended with a tower of universes (CCω) are always erasable. The calculus we use for that can be described by the following EPTS: + +\newcommand \SMInsertBefore[1]{ + \settowidth{\dimen0}{#1}\hspace{-\dimen0}#1 +} + \begin{displaymath} \begin{array}{lcl} \mathcal{S} &=& {~ \kw{Prop}; \Type \ell ~|~ \ell\in\mathbb{N} ~} \ @@ -648,14 +673,16 @@ The calculus we use for that can be described by the following EPTS: {~ (\kw{Prop} : \Type 0); (\Type \ell : \Type {\ell+1}) ~~|~~ \ell\in\mathbb{N} ~} \ \mathcal{R} &=& - \MAlign{ - {~ (k, \kw{Prop}, s, s); - (k, s, \kw{Prop}, \kw{Prop}) - ~~|~~ s \in \mathcal{S}, k \in {\kw{n},\kw{e}} ~} \ - \cup ~{~ + \begin{array}[t]{@{}l@{~~|~~}l} + {~ (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} ~} \ + \SMInsertBefore{\ensuremath{\cup ~}}{~ (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\Tmax{\ell_1}{\ell_2}}) - ~~|~~ \ell_1,\ell_2 \in\mathbb{N}, k \in {\kw{n},\kw{e}} ~} - } + & k \in {\kw{n},\kw{e}}, \ell_1,\ell_2 \in\mathbb{N} ~} + \end{array} \end{array} \end{displaymath} This calculus follows the tradition of having a special impredicative @@ -671,11 +698,12 @@ everywhere. Our calculus CCω is incidentally almost identical to the ICC* calculus of \citet{Barras08} (except for the \textsc{Conv} rule, as discussed above).

-With respect to impredicativity, the relevant rule in CCω is: $(k, s, -\kw{Prop}, \kw{Prop})$ which allows functions in \kw{Prop} to take arguments -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: +With respect to impredicativity, the relevant rule in CCω is: +$(k,\Type{\ell},\kw{Prop},\kw{Prop})$ which allows functions in \kw{Prop} to +take arguments in any $\Type \ell$. This rule is really a shorthand for two +separate rules: $(\kw{e},\Type{\ell},\kw{Prop},\kw{Prop})$ and +$(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$. And we will now show that the +second is redundant:

\begin{lemma}[Confinement of impredicativity in CCω] \label{lem:erasable} \mbox{} \ \normalfont @@ -692,6 +720,10 @@ And we will now show that the second is redundant: \item Given $\tau_e : \kw{Prop}$, clearly $e$ is too small to be a type like a sort $s$ or an arrow $\Arw{x}{\tau_1}{\tau_2}$, and it is also too small to be $x$ itself. + \item If the derivation uses the \textsc{Conv} rule to convert $e : \tau_e$ + to $e : \tau_e'$, we know that $\tau_e'$ also has type \kw{Prop}, by virtue of + the type preservation property, so we can use the induction hypothesis + on $e : \tau_e'$. \item If $e$ is a function $\Lam{y}{\tau_y}{e_y}$, then $\tau_y$ does not matter since it is erased from $\Ferase e$ and only occurrences of $x$ in $e_y$ is a concern, but since $\tau_e : \kw{Prop}$, we also know that the @@ -701,7 +733,8 @@ And we will now show that the second is redundant: induction hypothesis to $e_1$. As for $e_2$, there are two cases: either $e_1$ takes an argument of type $\tau_1:\kw{Prop}$ in which case we can again apply the induction hypothesis, or it takes an - argument of type $\tau_1:\Type \ell'$ in which case we're done. %% \qed + argument of type $\tau_1:\Type{\ell'}$ in which case we're done. + %% \qed \end{itemize} \vspace{-\baselineskip} \end{proof} @@ -709,7 +742,7 @@ And we will now show that the second is redundant: \begin{theorem}[Erasability of impredicative arguments in CCω] \mbox{} \ \normalfont %% - CCω's rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ is redundant since for any + 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'}}$ @@ -717,13 +750,13 @@ And we will now show that the second is redundant: \begin{proof} 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})$. + previously relied on the rule $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$. Since the erasability annotation is only used in the typing rule of $\lambda$-abstractions, the proof follows trivially for all cases except this one. For $\lambda$-abstractions that had an \kw{n} annotation that we need to convert to \kw{e}, we need to satisfy the additional condition that $x \not\in \kw{fv}(\Ferase e)$, which follows from Lemma~\ref{lem:erasable}: In the - absence of the rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$, all functions of + absence of the rule $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$, all functions of type $(y:\tau_1) \TEarw \tau_2$ where $\tau_2 : \kw{Prop}$ and $\tau_1 : \Type {\ell'}$ are necessarily erasable, so Lemma~\ref{lem:erasable} implies that $x$ can never occur in $\Ferase{e'}$. %% \qed

===================================== refs.bib ===================================== @@ -259,6 +259,68 @@ more accurate way.}, }

+@phdthesis{Abel13, + author = {Andreas Abel}, + month = mar, + school = {Institut für Informatik, + Ludwig-Maximilians-Universität}, + type = {Habilitation thesis}, + title = {Normalization by Evaluation: Dependent Types and + Impredicativity}, + year = {2013}, + abstract = {Normalization by evaluation (NbE) is a technique to + compute the normal form of a lambda-term, i.e., an + expression of a pure functional programming language. + While evaluation is only concerned with computing + closed expressions, normalization also applies to + function bodies, thus, needs to compute with open + expressions containing free variables. NbE reduces + normalization to evaluation of expressions in a + residualizing model, i.e., a computational structure + that has extra base values which are unknowns or + computations blocked by unknowns. Normalization by + evaluation, while not under this name, has been used + by Martin-Löf [1975] to prove normalization and + decidability of type checking for his predicative + intuitionistic type theory with a weak notion of term + equality that is not closed under function + abstraction. Independently, normalization by + evaluation has been discoverd by Berger and + Schwichtenberg [1991] as a tool to implement a + normalizer for simply-typed lambda-calculus with a + strong (extensional, “η”) notion of term + equality. Normalization invokes the evaluator of the + host programming language, leading to a concise and + efficient normalization procedure. In this thesis, we + join the two strands of research by developing NbE + for dependent type theory with extensional term + equality that does consider normalization of function + bodies. Further, we extend NbE to impredicative type + systems such as System F, Fω, and the Calculus of + Constructions. As NbE is a tool to connect syntax + (terms) to semantics (values), the study of NbE + enables us to semantically prove meta-theoretical + properties of the considered type systems such as + decidability of term equality, which entails the + decidability of type checking in the presence of + dependent types. For dependent types with universes + and extensional (η) equality at the level of types, + this is a novel result. The study of NbE provides us + with new insights into the nature of η-expansion + which we apply to dependent type theory with + singleton types. Further, we formulate the concept of + candidate space to equip semantic types with extra + structure that allows us to show the correctness of + NbE. Finally, we introduce typed Kripke structures to + unify semantic arguments by logical relations. The + results underlying this thesis were obtained partly + in collaboration with Klaus Aehlig, Thierry Coquand, + Peter Dybjer, and Miguel Pagano, as far as the design + of the NbE algorithm and its application to + predicative type theory are concerned.}, + url = {http://www.cse.chalmers.se/~abela/habil.pdf%7D, +} + @techreport{Gimenez94, author = {Eduardo Giménez}, institution = {École Normale Supérieure de Lyon},

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