Communications of the ACM
Propositions as Types
Credit: iStockPhoto.com
Powerful insights arise from linking two fields of study previously thought separate. Examples include Descartes's coordinates, which links geometry to algebra, Planck's Quantum Theory, which links particles to waves, and Shannon's Information Theory, which links thermodynamics to communication. Such a synthesis is offered by the principle of Propositions as Types, which links logic to computation. At first sight it appears to be a simple coincidence—almost a pun—but it turns out to be remarkably robust, inspiring the design of automated proof assistants and programming languages, and continuing to influence the forefronts of computing.
Key Insights
Propositions as Types is a notion with many names and many origins. It is closely related to the BHK Interpretation, a view of logic developed by the intuitionists Brouwer, Heyting, and Kolmogorov in the 1930s. It is often referred to as the Curry–Howard Isomorphism, referring to a correspondence observed by Curry in 1934 and refined by Howard in 1969. Others draw attention to significant contributions from de Bruijn's Automath and Martin-Löf's Type Theory in the 1970s.
Comments
CACM Administrator
The following letter was published in the Letters to the Editor of the March 2016 CACM (http://cacm.acm.org/magazines/2016/3/198861).
--CACM Administrator
Contrary to what Philip Wadler suggested in his otherwise interesting and informative article "Propositions as Types" (Dec. 2015, page 76, middle column, third paragraph), the algorithmic decidability of an axiomatically defined theory, say, T (such as Set Theory, as in Hilbert's concern) does not presuppose the negation- or "Gdel-" completeness (not to be confused with the semantic completeness) of T. First, negation-completeness does not imply algorithmic decidability without further ado, and second, negation-incompleteness does not imply algorithmic undecidability. The negation-completeness of T does indeed imply the algorithmic decidability of T if the set of axioms of T is algorithmically decidable and T is consistent (recall Recursion Theory), and there are theories that are negation-incomplete but algorithmically decidable (such as temporal-logical theories), respectively.(1)
Simon Kramer
Lausanne, Switzerland
REFERENCE
(1) Kramer, S. Logic of negation-complete interactive proofs (formal theory of epistemic deciders). Electronic Notes in Theoretical Computer Science 300, 21 (Jan. 2014), 4770, section 1.1.1.
-----------------------------------------------
AUTHOR'S RESPONSE
Thank you to Simon Kramer for clarifying the relation between completeness and decidability. The word "presupposes" has two meanings: "require as a precondition of possibility or coherence" and "tacitly assume at the beginning of a line of argument or course of action that something is the case." Kramer presupposes I mean the former, when in fact I mean the latter; my apologies for any confusion. The logics in question are consistent and have algorithmically decidable axioms and inference rules, so completeness indeed implies decidability.
Philip Wadler
Edinburgh, Scotland
Displaying 1 comment