Loading...
Please wait, while we are loading the content...
Similar Documents
Chapter 3 Proofs as Programs (2000)
| Content Provider | CiteSeerX |
|---|---|
| Abstract | In this chapter we investigate a computational interpretation of constructive proofs and relate it to functional programming. On the propositional fragment of logic this is referred to as the Curry-Howard isomorphism [How80]. From the very outset of the development of constructive logic and mathematics, a central idea has been that proofs ought to represent constructions. The Curry-Howard isomorphism is only a particularly poignant and beautiful realization of this idea. In a highly influential subsequent paper, Martin-Löf [ML80] developed it further into a more expressive calculus called type theory. 3.1 Propositions as Types In order to illustrate the relationship between proofs and programs we introduce a new judgment: M: A M is a proof term for proposition A We presuppose that A is a proposition when we write this judgment. We will also interpret M: A as “M is a program of type A”. These dual interpretations ofthesamejudgmentisthecoreoftheCurry-Howardisomorphism.Weeither think of M as a term that represents the proof of A true, or we think of A as the type of the program M. As we discuss each connective, we give both readings of the rules to emphasize the analogy. We intend that if M: A then A true. Conversely, if A true then M: A. But we want something more: every deduction of M: A should correspond to a deduction of A true with an identical structure and vice versa. In other words we annotate the inference rules of natural deduction with proof terms. The property above should then be obvious. Conjunction. Constructively, we think of a proof of A ∧ B true as a pair of proofs: one for A true and one for B true. |
| File Format | |
| Publisher Date | 2000-01-01 |
| Access Restriction | Open |
| Subject Keyword | Proof Term Beautiful Realization Weeither Think Martin-l Ml80 Vice Versa Curry-howard Isomorphism Expressive Calculus Constructive Proof Dual Interpretation Type Theory Propositional Fragment Central Idea Identical Structure Constructive Logic Influential Subsequent Paper Inference Rule New Judgment Curry-howard Isomorphism How80 Computational Interpretation Functional Programming Natural Deduction |
| Content Type | Text |
| Resource Type | Article |
