From 8741ba58377ebbe69fb78047add3fc8eab352948 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 12 Feb 2019 08:38:12 -0500 Subject: [PATCH] intro and coq comparison --- Wtypes.tex | 2 +- abstract.tex | 4 ++-- axioms.tex | 35 +++++++++++++++++++++++++++++- intro.tex | 29 +++++++++++++++++++------ references.bib | 58 ++++++++++++++++++++++++++++++++++++++------------ typesys.tex | 2 +- 6 files changed, 104 insertions(+), 26 deletions(-) diff --git a/Wtypes.tex b/Wtypes.tex index 3dc84a0..367dfa1 100644 --- a/Wtypes.tex +++ b/Wtypes.tex @@ -1,4 +1,4 @@ -\section{Reduction of inductive types to $\W$-types} +\section{Reduction of inductive types to $\W$-types}\label{sec:wtype} Given the complicated structure involved in simply stating the axioms of inductive types, one may wonder if there is an easier way. In fact there is; we can replace the whole structure of inductive types with a few simple inductive type constructors. diff --git a/abstract.tex b/abstract.tex index d8c9728..aac4482 100644 --- a/abstract.tex +++ b/abstract.tex @@ -1,8 +1,8 @@ \section*{Abstract} % \addcontentsline{toc}{chapter}{abstract} -This thesis is a presentation of dependent type theory with inductive types, a hierarchy of universes, with an impredicative universe of propositions, proof irrelevance, and subsingleton elimination, along with axioms for propositional extensionality, quotient types, and the axiom of choice. This theory is notable for being the axiomatic framework of the Lean theorem prover. The axiom system is given here in complete detail, including ``optional'' features of the type system such as $\mathsf{let}$ binders and definitions. We provide a reduction of the theory to a finitely axiomatized fragment utilizing a fixed set of inductive types (the $\W$ -type plus a few others), to ease the study of this framework. +This thesis is a presentation of dependent type theory with inductive types, a hierarchy of universes, with an impredicative universe of propositions, proof irrelevance, and subsingleton elimination, along with axioms for propositional extensionality, quotient types, and the axiom of choice. This theory is notable for being the axiomatic framework of the Lean theorem prover. The axiom system is given here in complete detail, including ``optional'' features of the type system such as $\mathsf{let}$ binders and definitions. We provide a reduction of the theory to a finitely axiomatized fragment utilizing a fixed set of inductive types (the $\W$-type plus a few others), to ease the study of this framework. -The metatheory of this theory (which we will call Lean) is studied. In particular, we prove unique typing of the definitional equality, and use this to construct the expected set-theoretic model, from which we derive consistency of Lean relative to ZFC with $n$ inaccessible cardinals for all $n<\omega$ (a relatively weak large cardinal assumption). As Lean supports models of ZFC with $n$ inaccessible cardinals, this is optimal. +The metatheory of this theory (which we will call Lean) is studied. In particular, we prove unique typing of the definitional equality, and use this to construct the expected set-theoretic model, from which we derive consistency of Lean relative to $\mathsf{ZFC}+\{\mbox{there are }n\mbox{ inaccessible cardinals}\mid n<\omega\}$ (a relatively weak large cardinal assumption). As Lean supports models of ZFC with $n$ inaccessible cardinals, this is optimal. We also show a number of negative results, where the theory is less nice than we would like. In particular, type checking is undecidable, and the type checking as implemented by the Lean theorem prover is a decidable non-transitive underapproximation of the typing judgment. Non-transitivity also leads to lack of subject reduction, and the reduction relation does not satisfy the Church-Rosser property, so reduction to a normal form does not produce a decision procedure for definitional equality. However, a modified reduction relation allows us to restore the Church-Rosser property at the expense of guaranteed termination, so that unique typing is shown to hold. diff --git a/axioms.tex b/axioms.tex index 5febff0..eab0ad1 100644 --- a/axioms.tex +++ b/axioms.tex @@ -1,4 +1,4 @@ -\section{The axioms} +\section{The axioms}\label{sec:axioms} \subsection{Typing} @@ -244,3 +244,36 @@ \subsubsection{Axiom of choice} From the axiom of choice, the law of excluded middle is derived (it is not stated as a separate axiom). \subsection{Differences from \textsf{Coq}}\label{sec:notcoq} +As mentioned in the introduction, Coq is a theorem prover also based on the Calculus of Constructions with inductive types (CIC), and it is quite old and well studied \cite{barrassets, barrastypedec, coqincoq, coquandcoc, lee2011, ecc, notsosimple}. So a natural question is to what degree Lean and CIC are similar, and whether proofs that apply to one system generalize, straightforwardly or otherwise, to the other. See \cite{lee2011} for a concise description of the proof theory of CIC. The following is a summary of differences with Lean's axiomatization, and their effects on the theorems here: + +\begin{enumerate} +\item Coq has universe cumulativity. That is, the definitional equality relation is replaced by a cumulativity relation $\preceq$ that is roughly the same, except that $\Gamma\vdash\U_i\preceq \U_j$ when $i\le j$. This breaks the unique typing theorem \autoref{thm:unique}, and it is not clear whether there is an adequate replacement in conjunction with all the other axioms of Lean. Luo \cite{ecc} shows that a large subset of CIC including cumulative universes retains good type theoretic properties, including strong normalization, from which an analogue of unique typing can be derived. +\item Gallina, the underlying core syntax of Coq, uses primitives $\mathsf{fix}$ and $\mathsf{match}$ to implement inductive types, rather than $\mathsf{rec}$ as is done here, and this is difference usually reflected in theoretical presentations as well. The difference is that while $\mathsf{rec}$ performs structural recursion over an inductive type, $\mathsf{fix}$ performs unbounded recursion, while $\mathsf{match}$ does (primitive) pattern matching over inductive types. In order to prevent infinite recursion and inconsistency as a result, the body of a $\mathsf{fix}$ must be typechecked with a modified typing judgment to ensure that all recursive calls are to elements generated by a $\mathsf{match}$ on the input. + +While in theory these approaches are equivalent, the $\mathsf{fix}$/$\mathsf{match}$ approach is more expressive, and the equivalence is sensitive to the exact rules available in both systems. Lean addresses this mismatch by allowing definitions using (effectively) $\mathsf{fix}$ and $\mathsf{match}$ at the user level, and compiling these away to recursors in the kernel language. + +\item Definitions in Lean are universe polymorphic, in the sense that they may contain free universe variables that are implicitly universally quantified at the point of definition, and applications of the constants include substitutions for all the universe variables involved in the definition. Coq definitions live in ``indefinite universes'' -- that is, each constant lives in a concrete universe but the level of this universe is held variable globally over the whole database, and using constants together generates level inequalities as side conditions that are maintained as a partial order. Coq reports an error if this order becomes inconsistent, i.e. there is no assignment of natural numbers to these variables that respects all the side conditions. + +There are Lean terms that cannot be checked in Coq with this approach, because Lean can reuse the same constant at two different levels while Coq has to resolve both instances of the constant to the same level. But this does not affect the set of provable theorems, since ``universe polymorphism is a luxury''; for a concrete theorem at a fixed universe level we may make duplicates of Coq constants as necessary to represent different instantiations of Lean constants. + +\item Coq inductive types allow ``non-uniform parameters''. These are parameters that vary subject to the restriction that they appear as is in each constructor's target type. These can be encoded using regular inductive types. + +\item Coq also supports mutual inductives, nested inductive types, and coinductive types. These can all be encoded using regular inductives, although some definitional equalities may fail to hold in the encodings. + +\item On the other hand, Lean supports definitional proof irrelevance, while Coq merely has an axiom that asserts this as a propositional equality. This is a major departure for the theory, and the reason why the counterexamples in \autoref{sec:undecidable} don't work in Coq. + +\item Lean supports quotient types with a definitional reduction rule, but Coq doesn't. The Coq ecosystem has compensated for this by using \emph{setoids} in place of types in many places, which are types with a designated equivalence relation that plays the role of equality. Although we have not investigated this, it should be possible to eliminate quotients from Lean entirely by using setoids instead. (There are good ergonomic reasons to have quotient types though, lest we end up in ``setoid hell''.) + +\item Lean offers (and de facto uses) three axioms, for propositional extensionality, quotient types and the axiom of choice. Coq has a comparatively large list of common axioms: +\begin{itemize} + \item Proof irrelevance and axiom K are propositional versions of Lean's definitional proof irrelevance. They hold in Lean ``with no axioms''. + \item Propositional extensionality is the same in Coq and Lean. + \item Functional extensionality is proven in Lean as a consequence of propositional extensionality and quotient types. + \item Coq has many variations on the law of excluded middle -- $P\lor\neg P$, $P=\mathsf{true}\lor P=\mathsf{false}$, and $P+\neg P$ (using a sum type). The first is excluded middle, the second is propositional degeneracy, which follows from excluded middle and propositional extensionality, and the third follows from excluded middle and the axiom of choice. In Lean all of these are proven using the axiom of choice. + \item The axiom of choice can be stated as $(\forall x,\exists y,R(x,y))\to(\exists f,\forall x,R(x,f(x)))$ or\\ + $\exists f,\forall x,(\exists y,R(x,y))\to R(x,f(x))$. These assert the existence of choice functions over limited domains, which is of course implied by a global choice function as with Lean's $\mathsf{choice}:\nonempty\;\alpha\to\alpha$. + \item Indefinite description, $(\exists x, P(x))\to\Sigma x, P(x)$, is equivalent to Lean's $\mathsf{choice}$. + \item Hilbert's epsilon, $\epsilon:(\alpha\to\mathsf{Prop})\to \alpha$ such that $(\exists x,P(x))\to P(\epsilon(P))$, is also equivalent to $\mathsf{choice}$. +\end{itemize} +So all of Coq's axioms taken together are implied by Lean's axioms, and the converse is true except for definitional proof irrelevance and a computation rule for quotient types. (One can build set-quotients in Coq as well as Lean, but they lack the computation rule.) +\end{enumerate} diff --git a/intro.tex b/intro.tex index d1ee842..a513ca3 100644 --- a/intro.tex +++ b/intro.tex @@ -13,12 +13,27 @@ \subsection{Type theory in programming languages} By choosing to program in a formal language for constructive mathematics, like the theory of types, one gets access to the whole conceptual apparatus of pure mathematics, neglecting those parts that depend critically on the law of excluded middle, whereas even the best high level programming languages so far designed are wholly inadequate as mathematical languages (and, of course, nobody has claimed them to be so). In fact, I do not think that the search for logically ever more satisfactory high level programming languages can stop short of anything but a language in which (constructive) mathematics can be adequately expressed. \cite{martinlofprog} \end{quote} -This dream was converted to action by Thierry Coquand, who developed the Calculus of Constructions (CoC) \cite{coquandcoc} and developed an interactive proof assistant \textsf{Coq} to check proofs in this language \cite{coqart}. This type theory was extended with inductive types \cite{dybjer} to form the Calculus of Inductive Constructions (CIC) \cite{paulincic}. +This dream was converted to action by Coquand and Huet, who introduced the Calculus of Constructions (\textsf{CoC}) \cite{coquandcoc} and developed it into an interactive proof assistant \textsf{Coq} \cite{coqart}. This type theory was extended with inductive types \cite{dybjer} to form the Calculus of Inductive Constructions (\textsf{CIC}) \cite{paulincic}. -Lean \cite{demoura} is a theorem prover based on CIC as well, with some subtle but important differences. See \autoref{sec:notcoq} for an elaboration of the differences from Coq's axiomatics. The goal of this paper is to demonstrate the consequences of these differences, without leaving anything out. While CIC itself is well-studied \cite{barrassets, barrastypedec, coqincoq}, most papers study subsystems of the actual axiomatic system implemented in Coq, which might be called $\mathsf{CIC^+}$ for its many small extensions added over the years. While we will not analyze $\mathsf{CIC^+}$ in this paper, we will be able to analyze all the extensions that are in Lean CIC, so our proof of consistency is directly applicable to the full Lean kernel. +Lean \cite{demoura} is a theorem prover based on \textsf{CIC} as well, with some subtle but important differences. The goal of this paper is to demonstrate the consequences of these differences, all taken together. While \textsf{CIC} itself is well-studied \cite{barrassets, barrastypedec, coqincoq}, most papers study subsystems of the actual axiomatic system implemented in Coq, which might be called $\mathsf{CIC^+}$ for its many small extensions added over the years. While we will not analyze $\mathsf{CIC^+}$ in this paper, we will be able to analyze all the extensions that are in Lean \textsf{CIC}, so our proof of consistency is directly applicable to the full Lean kernel. (See \autoref{sec:notcoq} for the possible issues that can come up in trying to extend this analysis to $\mathsf{CIC^+}$.) -UNFINISHED: talk about: -\begin{itemize} -\item Werner \cite{setsintypes}: Sets in Types -\item Miquel \cite{notsosimple}: The not so simple proof irrelevant model of CC -\end{itemize} +\subsection{Set theoretic models of type theory} +Martin-L\"{o}f type theory has a relatively obvious model, in which types are interpreted as sets, and terms of that type are interpreted as elements of the corresponding sets. Essentially, this amounts to treating ``function types'' like $A\to B$ as literal sets of ZFC-encoded functions (sets of ordered pairs). Since most of the type theoretic intuition and terminology is inherited from this context, from the point of view of standard mathematics it is reasonable to expect that this should work as a model, and conversely we can use this model to guide our expectations for the reasonableness of variations on the rules of type theory. + +In this model the easiest way to accomodate propositions is to have a two element universe $\mathsf{Prop}=\{0,1\}$, where the two elements are propositions $0=\emptyset$ and $1=\{\bullet\}$, where $\bullet$ is the ``trivial proof of $\mathsf{true}$''. This makes the model \emph{proof-irrelevant}, in the sense that proofs of a proposition are not distinguished in the model. This is great for type theories that have proof irrelevance in some form (also known as axiom K or uniqueness of identity proofs (UIP)), but contradicts homotopy type theory (HoTT) \cite{hottbook}, since the axiom of univalence is inconsistent with UIP. (Since definitional UIP is an axiom of Lean, we will not pursue models of HoTT further in this paper.) + +This model is also tailored for \emph{impredicativity} of the universe of propositions. That is, the type theory allows propositions to quantify over elements in ``large universes''. To a mathematician accustomed to set theory, this may seem a non-issue, but impredicativity is quite axiomatically strong and corresponds to having ``full powersets'' in the ZFC sense. For predicative type theories, such as the axiom system used by Agda \cite{agda}, the impredicative model will work but is in some sense ``overkill''; here the preference is for models based on partial equivalence relations on terms, which avoids large cardinals. + +Universes of CIC are closed under function types and inductive types, which when translated to the set theoretic language implies that they are Grothendieck universes. If we limit our attention to levels of the cumulative hierarchy $V_\lambda$, this amounts to a requirement that $\lambda$ be an inaccessible cardinal. Since Lean has an infinite sequence of universes this translates to having $\omega$ many inaccessible cardinals in the ZFC universe from which to build the model, and this is the main large cardinal axiom we require. It is not difficult to see that this assumption (or something with similar consistency strength) is necessary, because with a suitably defined inductive type we can construct a model of ZFC in each universe above the first one, and moreover we can define particular inaccessible cardinals in the larger models, so that we can have models of ZFC with $n$ inaccessible cardinals. + +In ``Sets in Types, Types in Sets'' \cite{setsintypes}, Werner demonstrates the equiconsistency of $\mathsf{ZFC}_\omega$ and $\mathsf{CIC}_\omega$ by showing that $\mathsf{ZFC}_n\vdash\mathrm{Con}(\mathsf{CIC}_{n+1})$ and $\mathsf{CIC}_{n+2}\vdash\mathrm{Con}(\mathsf{ZFC}_n)$, where $\mathsf{ZFC}_n$ is $\mathsf{ZFC}$ with $n$ inaccessible cardinals and $\mathsf{CIC}_n$ is $\mathsf{CIC}$ with $n$ universes, and $\mathsf{ZFC}_\omega$ and $\mathsf{CIC}_\omega$ are the unions of these theories over $n<\omega$. Werner's construction of a model of set theory in CIC (in Coq) has been replicated in Lean with only minor modifications, so we can also claim $\mathsf{Lean}_{n+2}\vdash\mathrm{Con}(\mathsf{ZFC}_n)$ for essentially the same reasons. + +The present work establishes the reverse direction $\mathsf{ZFC}_{n+1}\vdash\mathrm{Con}(\mathsf{Lean}_{n+1})$, so that $\mathsf{Lean}_\omega$ (or just $\mathsf{Lean}$) is also equiconsistent with $\mathsf{ZFC}_\omega$ and $\mathsf{CIC}_\omega$. We don't attempt to be precise with the universe bounds, but if we wanted to get a result like Werner's $\mathsf{ZFC}_n\vdash\mathrm{Con}(\mathsf{CIC}_{n+1})$, we would have to assume an axiom of global choice in $\mathsf{ZFC}$ (i.e. there is a proper class choice function on the universe $V$) to interpret Lean's $\mathsf{choice}$ axiom. + +To some degree one can view this work as merely an elaboration of Werner's work in the context of Lean in place of Coq. However, we believe that inductive types in CIC, and Lean, are more complicated than they appear from simple worked examples, and we wanted to ensure that we correctly model the entire language, including all the edge case features that interact in unusual ways. In fact, as we shall see, a combination of subsingleton eliminating inductive types and definitional proof irrelevance breaks the decidability of Lean's type system, making a number of desirable properties fail to hold. In the light of this, as well as some historical soundness bugs in Coq as a result of unusual features in inductive specifications or pattern matching \cite{soundnessbug}, we felt it important to write down the complete axiomatic basis for Lean's type system, and work from there. See \autoref{sec:axioms} for the specification. + +In ``The not so simple proof irrelevant model of CC'' \cite{notsosimple}, Miquel and Werner detail an issue that arises in proof irrelevant models such as the one described here. In short, without knowing the universe in which an expression or type lives, it becomes difficult to translate the Pi type over propositions differently than the Pi type over other universes, as one must, in order to ensure that $U_0=\{\emptyset,\{\bullet\}\}$ can serve as the boolean universe of propositions. This issue arises here as well, and the key step in overcoming it is the unique typing property. While this is mostly trivial in the context of PTSs for \cite{notsosimple}, in Lean this is a tricky syntactic argument, proven in \autoref{sec:unique}. While it is inspired by the Tait--Martin-L\"{o}f proof of the Church--Rosser theorem \cite{taitmartinlof}, definitional proof irrelevance causes many new difficulties, and the proof is novel to our knowledge. + +In \cite{barrassets}, Barras uses a simple and ingenious trick to uniformize the treatment of the proof irrelevant universe of propositions with other universes - to use Aczel's encoding of functions, $f:=\{(x,y)\mid x\in\mathrm{dom}(f)\wedge y\in f(x)\}$, which has the property that $(x\in A\mapsto\bullet)=\bullet$ if we interpret $\bullet$ as the empty set. This simple property means that we don't need to determine the sorts of types and elements in the construction, and so we can avoid the dependency on unique typing in the proof of soundness. So if our only goal was proving soundness we could skip \autoref{sec:unique} entirely. Nevertheless, it is a useful property to have, and with it we can use the straightforward ZFC encoding for functions. + +The remainder of the paper is organized as follows. \hyperref[sec:axioms]{Section~\ref*{sec:axioms}} details the type system of Lean in formal notation. \hyperref[sec:props]{Section~\ref*{sec:props}} does some basic metatheory of the type system, and in particular shows a number of negative results stemming from lack of decidability of the type system. \hyperref[sec:unique]{Section~\ref*{sec:unique}} is the proof of unique typing of the type system (even including the undecidable bits). \hyperref[sec:wtype]{Section~\ref*{sec:wtype}} shows how all inductive types can be reduced to a finite basis of 8 particular, basic inductive types. \hyperref[sec:soundness]{Section~\ref*{sec:soundness}} is the soundness theorem, which constructs the aforementioned set theoretic model for the $\W$ basis in detail. diff --git a/references.bib b/references.bib index 86e5104..e6c26a1 100644 --- a/references.bib +++ b/references.bib @@ -37,7 +37,7 @@ @inproceedings{typesoftypes organization={Springer} } @article{frege, - title={Begriffsschrift, a formula language, modeled upon that of arithmetic, for pure thought}, + title={{Begriffsschrift, a formula language, modeled upon that of arithmetic, for pure thought}}, author={Frege, Gottlob}, journal={From Frege to G{\"o}del: A source book in mathematical logic}, volume={1931}, @@ -45,14 +45,14 @@ @article{frege year={1879} } @book{principia, - title={Principia mathematica}, + title={{Principia Mathematica}}, author={Whitehead, Alfred North and Russell, Bertrand}, volume={2}, year={1912}, publisher={University Press} } @article{quinenf, - title={New foundations for mathematical logic}, + title={{New Foundations for Mathematical Logic}}, author={Quine, Willard V}, journal={The American mathematical monthly}, volume={44}, @@ -62,7 +62,7 @@ @article{quinenf publisher={Taylor \& Francis} } @article{churchstt, - title={A formulation of the simple theory of types}, + title={{A Formulation of the Simple Theory of Types}}, author={Church, Alonzo}, journal={The journal of symbolic logic}, volume={5}, @@ -80,7 +80,7 @@ @article{curryhoward year={1980} } @incollection{martinlof, - title={An intuitionistic theory of types: Predicative part}, + title={{An Intuitionistic Theory of Types: Predicative Part}}, author={Martin-L{\"o}f, Per}, booktitle={Studies in Logic and the Foundations of Mathematics}, volume={80}, @@ -89,7 +89,7 @@ @incollection{martinlof publisher={Elsevier} } @incollection{martinlofprog, - title={Constructive mathematics and computer programming}, + title={{Constructive Mathematics and Computer Programming}}, author={Martin-L{\"o}f, Per}, booktitle={Studies in Logic and the Foundations of Mathematics}, volume={104}, @@ -98,19 +98,19 @@ @incollection{martinlofprog publisher={Elsevier} } @phdthesis{coquandcoc, - title={The calculus of constructions}, + title={{The Calculus of Constructions}}, author={Coquand, Thierry and Huet, G{\'e}rard}, year={1986}, school={INRIA} } @book{coqart, - title={Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions}, + title={{Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions}}, author={Bertot, Yves and Cast{\'e}ran, Pierre}, year={2013}, publisher={Springer Science \& Business Media} } @article{dybjer, - title={Inductive families}, + title={{Inductive Families}}, author={Dybjer, Peter}, journal={Formal aspects of computing}, volume={6}, @@ -120,13 +120,13 @@ @article{dybjer publisher={Springer} } @misc{paulincic, - title={Introduction to the calculus of inductive constructions}, + title={{Introduction to the Calculus of Inductive Constructions}}, author={Paulin-Mohring, Christine}, year={2015}, publisher={College Publications} } @inproceedings{demoura, - title={The Lean theorem prover (system description)}, + title={{The Lean Theorem Prover (system description)}}, author={de Moura, Leonardo and Kong, Soonho and Avigad, Jeremy and Van Doorn, Floris and von Raumer, Jakob}, booktitle={International Conference on Automated Deduction}, pages={378--388}, @@ -134,7 +134,7 @@ @inproceedings{demoura organization={Springer} } @inproceedings{barrastypedec, - title={On the role of type decorations in the calculus of inductive constructions}, + title={{On the Role of Type Decorations in the Calculus of Inductive Constructions}}, author={Barras, Bruno and Gr{\'e}goire, Benjamin}, booktitle={International Workshop on Computer Science Logic}, pages={151--166}, @@ -142,7 +142,7 @@ @inproceedings{barrastypedec organization={Springer} } @article{barrassets, - title={Sets in Coq, Coq in sets}, + title={{Sets in Coq, Coq in Sets}}, author={Barras, Bruno}, journal={Journal of Formalized Reasoning}, volume={3}, @@ -151,9 +151,39 @@ @article{barrassets year={2010} } @article{coqincoq, - title={Coq in coq}, + title={{Coq in Coq}}, author={Barras, Bruno and Werner, Benjamin}, journal={Available on the WWW}, year={1997}, publisher={Citeseer} } +@Book{hottbook, + author = {The {Univalent Foundations Program}}, + title = {Homotopy Type Theory: Univalent Foundations of Mathematics}, + publisher = {\url{https://homotopytypetheory.org/book}}, + address = {Institute for Advanced Study}, + year = 2013 +} +@inproceedings{agda, + title={{Dependently typed programming in Agda}}, + author={Norell, Ulf}, + booktitle={International School on Advanced Functional Programming}, + pages={230--266}, + year={2008}, + organization={Springer} +} +@misc{soundnessbug, + title={{Propositional extensionality is inconsistent in Coq}}, + url={https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html}, + journal={Coq-Club}, + publisher={INRIA}, + author={Dénès, Maxime}, + year={2013}, + month={Dec} +} +@article{taitmartinlof, + title={Polishing up the Tait-Martin-L{\"o}f proof of the Church-Rosser theorem}, + author={Pollack, Robert}, + year={1995}, + publisher={Citeseer} +} diff --git a/typesys.tex b/typesys.tex index 8834f6b..791309d 100644 --- a/typesys.tex +++ b/typesys.tex @@ -1,4 +1,4 @@ -\section{Properties of the type system} +\section{Properties of the type system}\label{sec:props} A theorem we would like to have of Lean's type system is that it is consistent, and sound with respect to some semantics in a well understood axiom system such as ZFC. Moreover, we want to relate this to Lean's actual typechecker, in the sense that anything Lean verifies as type-correct will be derivable in this axiom system and hence Lean will not certify a contradiction. But first we must understand some aspects of the type system itself, before relating it to other systems. It is important to note that \emph{Lean's typechecker is not complete.} Obviously Lean can fail on correct theorems due to, say, running out of resources, but the ``algorithmic equality'' relation does not validate all definitional equalities. In fact, we can show that definitional equality as defined here is undecidable.