DOC PREVIEW
CMU CS 15816 - Lecture Notes on Proofs as Programs

This preview shows page 1-2-23-24 out of 24 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 24 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 24 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 24 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 24 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 24 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

IntroductionPropositions as TypesReductionExpansionSummary of Proof TermsHypothetical Judgments in Localized FormNatural Deduction in Localized FormSubject ReductionLecture Notes onProofs as Programs15-816: Modal LogicFrank PfenningLecture 2January 14, 20101 IntroductionIn this lecture we investigate a computational interpretation of intuition-istic proofs and relate it to functional programming. On the propositionalfragment of logic this is called the Curry-Howard isomorphism [How80].From the very outset of the development of constructive logic and math-ematics, a central idea has been that proofs ought to represent construc-tions. The Curry-Howard isomorphism is only a particularly poignant andbeautiful realization of this idea. In a highly influential subsequent pa-per, Martin-L¨of [ML80] developed it further into a more expressive calculuscalled type theory.The computational interpretation of intuitionistic logic and type theoryunderlies many of the applications of intuitionistic modal logic in computerscience. In the context of this course it therefore important to gain a goodworking knowledge of the interpretation of proofs as programs.2 Propositions as TypesIn order to illustrate the relationship between proofs and programs we in-troduce a new judgment:M : A M is a proof term for proposition AWe presuppose that A is a proposition when we write this judgment. Wewill also interpret M : A as “M is a program of type A”. These dual inter-LECTURE NOTES JANUARY 14, 2010L2.2 Proofs as Programspretations of the same judgment is the core of the Curry-Howard isomor-phism. We either think of M as a term that represents the proof of A true, orwe 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 corre-spond to a deduction of A true with an identical structure and vice versa.In other words we annotate the inference rules of natural deduction withproof terms. The property above should then be obvious.Conjunction. Constructively, we think of a proof of A ∧ B true as a pairof proofs: one for A true and one for B true.M : A N : BhM, Ni : A ∧ B∧IThe elimination rules correspond to the projections from a pair to itsfirst and second elements.M : A ∧ Bπ1M : A∧ELM : A ∧ Bπ2M : B∧ERHence conjunction A ∧ B corresponds to the product type A × B.Truth. Constructively, we think of a proof of > true as a unit element thatcarries now information.h i : >>IHence > corresponds to the unit type 1 with one element. There is noelimination rule and hence no further proof term constructs for truth.Implication. Constructively, we think of a proof of A ⊃ B true as a func-tion which transforms a proof of A true into a proof of B true.In mathematics and many programming languages, we define a func-tion f of a variable x by writing f (x) = . . . where the right-hand side “. . .”depends on x. For example, we might write f(x) = x2+x−1. In functionalprogramming, we can instead write f = λx. x2+ x− 1, that is, we explicitlyform a functional object by λ-abstraction of a variable (x, in the example).LECTURE NOTES JANUARY 14, 2010Proofs as Programs L2.3We now use the notation of λ-abstraction to annotate the rule of impli-cation introduction with proof terms. In the official syntax, we label the ab-straction with a proposition (writing λu:A) in order to specify the domainof a function unambiguously. In practice we will often omit the label tomake expressions shorter—usually (but not always!) it can be determinedfrom the context.u : Au...M : Bλu:A. M : A ⊃ B⊃IuThe hypothesis label u acts as a variable, and any use of the hypothesislabeled u in the proof of B corresponds to an occurrence of u in M.As a concrete example, consider the (trivial) proof of A ⊃ A true:A trueuA ⊃ A true⊃IuIf we annotate the deduction with proof terms, we obtainu : Au(λu:A. u) : A ⊃ A⊃IuSo our proof corresponds to the identity function id at type A which simplyreturns its argument. It can be defined with id(u) = u or id = (λu:A. u).The rule for implication elimination corresponds to function applica-tion. Following the convention in functional programming, we write M Nfor the application of the function M to argument N , rather than the moreverbose M (N ).M : A ⊃ B N : AM N : B⊃EWhat is the meaning of A ⊃ B as a type? From the discussion above itshould be clear that it can be interpreted as a function type A → B. Theintroduction and elimination rules for implication can also be viewed asformation rules for functional abstraction λu:A. M and application M N.Note that we obtain the usual introduction and elimination rules forimplication if we erase the proof terms. This will continue to be true forLECTURE NOTES JANUARY 14, 2010L2.4 Proofs as Programsall rules in the remainder of this section and is immediate evidence for thesoundness of the proof term calculus, that is, if M : A then A true.As a second example we consider a proof of (A ∧ B) ⊃(B ∧ A) true.A ∧ B trueuB true∧ERA ∧ B trueuA true∧ELB ∧ A true∧I(A ∧ B) ⊃(B ∧ A) true⊃IuWhen we annotate this derivation with proof terms, we obtain a functionwhich takes a pair hM, N i and returns the reverse pair hN, Mi.u : A ∧ Buπ2u : B∧ERu : A ∧ Buπ1u : A∧ELhπ2u, π1ui : B ∧ A∧I(λu. hπ2u, π1ui) : (A ∧ B) ⊃(B ∧ A)⊃IuDisjunction. Constructively, we think of a proof of A ∨ B true as eithera proof of A true or B true. Disjunction therefore corresponds to a disjointsum type A + B, and the two introduction rules correspond to the left andright injection into a sum type.M : AinlBM : A ∨ B∨ILN : BinrAN : A ∨ B∨IRIn the official syntax, we have annotated the injections inl and inr withpropositions B and A, again so that a (valid) proof term has an unambigu-ous type. In writing actual programs we usually omit this annotation. Theelimination rule corresponds to a case construct which discriminates be-tween a left and right injection into a sum types.M : A ∨ Bu : Au...N : Cw : Bw...O : Ccase M of inl u ⇒ N | inr w ⇒ O : C∨Eu,wRecall that the hypothesis labeled u is available only in the proof of thesecond premise and the hypothesis labeled w only in the proof of the thirdpremise. This means that the scope of the variable u is N , while the scopeof the variable w is O.LECTURE


View Full Document

CMU CS 15816 - Lecture Notes on Proofs as Programs

Download Lecture Notes on Proofs as Programs
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Lecture Notes on Proofs as Programs and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Lecture Notes on Proofs as Programs 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?