Proofs as Efficient Programs

Abstract

There may, indeed, be other uses of the system than its use as a logic. A. Church [8] Logic and theory of computation have been intertwined since their first days. The formalized notion(s) of effective computation are at first technical tools for the investigation of first order systems, and only ten years later-in the hands of John von Neumann-become the blueprints of engineered physical devices. Generally, however, one tends to forget that in those same years, in the newly-born proof-theory of Gerhard Gentzen [20] there is an implicit, powerful notion of computation-an effective, combinatorial procedure for the simplification of a proof. However, the complexity of the rules for the elimination of cuts (especially the commutative ones, in the modern jargon) hid the simplicity and generality of the basic computational notion those rules were based upon. We had to wait thirty more years before realizing in full glory that Gentzen's simplification mechanism and one of the formal systems for computability (Church's λ-calculus) were indeed one and the same notion. As far as we know, Haskell Curry is the first to explicitly realize [11] that the types of some of his basic combinators correspond to axioms of intuition-istic implicational calculus, and that, more generally, the types assignable to expressions made up of combinators are exactly the provable formulae of in-tuitionistic implicational logic. It is William Howard in 1969 to extend this formulas as types correspondence to the more general proofs as programs iso-morphism ([27], published in 1980 but widely circulated before). Under this interpretation, the two dynamics-proof normalization on one hand, and β-reduction on the other-are identified, so that techniques and results from one area are immediately available to the other. In this paper, we will discuss the use of the Curry-Howard correspondence in computational complexity theory, the area of theoretical computer science concerned with the definition and study of complexity classes and their relations. The standard approach to this discipline is to fix first a machine model (e.g., Turing machines) equipped with an explicit cost (e.g., number