Lectures on the Curry-Howard isomorphism (Q881453)

This book consists of fourteen chapters and two appendices. It yields a thorough self-contained introduction to the Curry-Howard isomorphism, i.e., the so-called propositions-as-types paradigm, whose central idea is to establish a link between formal systems and computational systems. The main point is that formulas are regarded as types, while their proofs are interpreted as suitable functions; in fact, following Kolmogorov, propositions are to be regarded as problems whose solutions are given by their own proofs. Chapter 1 offers a concise presentation of pure untyped lambda calculus. Fundamental results on reduction and conversion are stated and proved (the Church-Rosser theorem, normalization of leftmost reduction, existence of perpetual reductions). Lambda definability of partial recursive functions is also proved, together with fundamental undecidability results (e.g., the property of being strongly normalizing). In Chapter 2, motivations are given for the choice of a constructive logic, and the Brouwer-Heyting-Kolmogorov (BHK) interpretation is outlined, together with the natural deduction calculus NJ, which closely reflects the constructive meaning of the logical constants. An algebraic semantics is presented (via Heyting algebras) with a number of standard results (completeness, finite model property, Glivenko's theorem), as well as Kripke's semantics. Chapter 3 is devoted to simply typed \(\lambda\)-calculus, in its main variants à la Curry and à la Church). Lambda terms are used as proof notations and formulas are used as types; the issue is not provability, but proofs in themselves, as objects of investigation (the structure of proofs, normal form, identity of proofs). The main problems (type checking, typability, type inhabitation) and theorems are proved in detail (e.g., strong normalization, Newman's lemma). The chapter ends with the issue of expressibility (the extended polynomials being the \(\lambda\)-definable number-theoretic functions, according to a result of Schwichtenberg). The main topic of the monograph -- the Curry-Howard isomorphism -- deals with the relation between intuitionistic logic and simply typed lambda calculus, and is explicitly tackled in the fourth chapter. The essence is that lambda terms can be regarded as suitable refinements of proofs, while non-empty types correspond to provable formulas. More importantly, there is a basic correspondence between proof normalization and computation of terms (and hence between proofs and algorithms), which allows for instance to derive normalization of proofs from normalization of the corresponding lambda terms. Among the basic results of this chapter, it is also shown that the inhabitation problem is PSPACE-complete. On the other hand, the isomorphism issue is discussed also in its limits (while lambda-terms are annotated proofs, some proofs can be annotated in several ways). In the final part, the authors introduce the dialogic approach to constructive logics; winning prover strategies correspond to simply typed terms in \(\eta\)-long normal form. Chapter 5 introduces combinators and hence the correspondence between Hilbert-style proofs and terms of typed combinatory logic. The fact that combinatory logic is able to express functional abstraction corresponds to the deduction theorem. Chapter 6 deals with the extension of the Curry-Howard isomorphism to classical logic, following ideas of Griffin and Murthy. The basic observation is that the principle of double negation corresponds to the typing of a suitable control operator from programming language theory. This gives rise to an extension of simply typed lambda calculus -- the so-called \(\lambda \mu\)-calculus -- for which basic results are established (subject reduction, confluence and strong normalization); again, a dialogic approach is presented. The landscape of logical systems is enriched in Chapter 7 by the introduction of Gentzen's sequent calculi for sentential languages and a detailed proof of the cut-elimination theorem. Cut elimination is compared with normalization and a version of Lorenzen games for classical logic is introduced (in which both players can attack and defend). First-order logic is given in its variants (natural deduction, sequent calculi and Hilbert systems) in Chapter 8, which contains a treatment of Tarskian semantics for classical first-order logic as well as algebraic semantics and Kripke semantics for intuitionistic first-order logic. The completeness theorem is proved in details with respect to Kripke semantics. In the final part, the Curry-Howard isomorphism is extended to first-order logic; this leads to an extension of typed lambda calculus with new type constructors, dependent types, products and coproducts, and new operators, corresponding to \(\exists\)-introduction and \(\exists\)-elimination. The resulting extended lambda calculus is shown to have the Church-Rosser property and strong normalization. Undecidability of first-order intuitionistic logic is then proved by establishing a correspondence between the halting problem for two-counter automata and provability in the fragment of intuitionistic logic determined by \(\forall\) and \(\rightarrow\). Chapter 9 is a compact introduction to first-order arithmetic PA and some basic facts: (i) existence of non-standard models; (ii) representability of recursive functions in PA; (iii) Tarski's theorem about the non-arithmetical definability of first-order arithmetical truth; (iv) Gödel's incompleteness results. Intuitionistic (Heyting) arithmetic is introduced together with the interpretability of PA in HA, via Kolmogorov translation, and Kleene's realizability. From a computational point of view, both HA and PA are very powerful, being able to prove termination for a very large class of algorithms (those corresponding to provably recursive functions of PA). The subsequent chapter presents Gödel's system T of primitive recursive functionals of higher type. The strong normalization for T is proved using Tait's technique of computability predicates. T is used for characterizing the provably recursive functions of PA and also to define the so-called modified realizability interpretation. Chapters 11--12 offer an introduction to impredicative systems and polymorphism. The authors present intuitionistic second-order propositional logic with the completeness theorem with respect to Kripke's semantics and the corresponding polymorphic lambda-calculus F (Church's style). The main properties -- strong normalization, undecidability of inhabitation problem -- are developed in detail for the Curry variant of F. Adding type constructors to F leads to higher-order polymorphism. Chapter 12 is devoted to second-order arithmetic (in its classical and constructive versions); the main result is to prove that the class of provably recursive functions of second-order arithmetic coincides with the class of number-theoretic functions definable by algorithms which can be typed in the system F. To this aim, a suitable typed lambda-calculus corresponding to intuitionistic second-order arithmetic is designed, and confluence and strong normalization are proved. Chapter 13 outlines a system \(\lambda P\) of dependent types where there is no essential distinction between objects and proof objects. The resulting type assignment satisfies both strong normalization and the Church-Rosser property; however both type checking and the inhabitation problem are undecidable. The final chapter introduces a common abstraction of the different type systems, the so-called pure type systems PTS. The systems of the so-called Barendregt's cube are presented, from the simply typed lambda calculus, where objects depend on objects, through different kinds of dependence (types may depend on objects, objects may depend on types) to the Calculus of Constructions, which nevertheless enjoys normalization. The final section describes Girard's paradox for certain PTS in the presence of the axiom \textit{Type is a Type}. The text is supplemented by two Appendices, A and B. Appendix A gives mathematical prerequisites (from set theory and computability theory), while Appendix B offers a selection of solved exercises. Each chapter of the book is enriched by exercises and nicely supplemented with historical notes and a very large bibliography. The reviewer believes that this is a nice research monograph, which can be adequately used as a textbook at the level of graduate studies, especially for teaching typed lambda calculus and intuitionistic logic.