DOC PREVIEW
CMU CS 15816 - Lecture

This preview shows page 1-2-3 out of 10 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 10 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 10 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 10 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 10 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

IntroductionExamples in Multiple-World Intuitionistic Modal LogicNon-Local ActionsInterpreting ValidityIncompletenessAxiomatic Presentations of Modal Logic RevisitedLecture Notes onKripke Semantics for Validity15-816: Modal LogicFrank PfenningLecture 16March 23, 20101 IntroductionIn this lecture we continue the analysis of distributed computation throughmodal logic. We give a multiple-worlds interpretation of the modal logic ofvalidity and find that it corresponds to IS4. However, when we generalizethis to include possibility, we find that the our inference rules are soundfor IS4, but not complete. The counterexamples gives rise to a new form ofinterpretation of modal logic we develop in the next lecture.2 Examples in Multiple-World Intuitionistic Modal LogicWe reexamine the earlier examples in light of their proposed interpretationwith respect to distributed computation.K♦: (A ⊃ B) ⊃(♦A ⊃ ♦B) @ h= λx@h. λy@h. let hh ≤ αi z = y in hh ≤ αi((x [h ≤ α]) z)The function K♦takes a mobile function x and a reference to a remote valueat some world α, moves x to α, applies it there, and returns a reference tothe answer here.T : A ⊃ A= λx@h. x [h ≤ h]The function T takes a mobile value of type A and unpacks it here.LECTURE NOTES MARCH 23, 2010L16.2 Kripke Semantics for Validity4♦: ♦♦A ⊃ ♦A= λx@h. let hh ≤ αi y = x in let hα ≤ βi z = y in hh ≤ βizThe function 4♦takes a reference to a remote reference to a value V of typeA at some world β and return a direct reference to V .3 Non-Local ActionsAs discussed at the end of last lecture, disjunction creates the the necessityfor an effect at a distance. We write down the substructural operationalsemantics rules to clarify this. A similar remark applies to falsehood. Firstwe recall the located typing rules.Γ ` M : A @ wΓ ` inl M : A ∨ B @ w∨I1Γ ` N : B @ wΓ ` inr M : A ∨ B @ w∨I2Γ ` M : A ∨ B @ w Γ, x:A@w ` N : C @ w00Γ, y:B@w ` N : C @ w00Γ ` case M of inl x ⇒ N | inr y ⇒ O : C @ w00∨ENext the operational semantics. Observe that in the very first rule (eval/case)there is a non-local transfer of control, from w00to w, even though w00and wmay not be interaccessible. In order to effect this transfer, the case constructshould be annotated with the location of M . Then, when the value of M isreturned at w, one bit of information need to be communicated from w tow00so that the appropriate branch (either N or O) can be selected at w00.eval/case : eval (case M of inr x ⇒ N | inr y ⇒ O) w00 eval M w•cont (case of inr x ⇒ N | inr y ⇒ O)eval/inl : eval (inl M0) w  eval M0w•cont (inl ) weval/inr : eval (inr M0) w  eval M0w•cont (inr ) wcont/inl : ret V0w•cont (inl ) w  ret (inl V0) wcont/inr : ret V0w•cont (inr ) w  ret (inr V0) wret/inl : ret (inl V0) w•cont (case of inr x ⇒ N | inr y ⇒ O) w00 !bind x V0w•eval N w00ret/inr : ret (inr V0) w•cont (case of inr x ⇒ N | inr y ⇒ O) w00 !bind y V0w•eval O w00LECTURE NOTES MARCH 23, 2010Kripke Semantics for Validity L16.3If all worlds are interaccessible (that is, we are working in IS5), this isimplementable. But this oddity of the operational semantics also has itsreflection in the truths we can prove. Consider:♦/∨ : ♦(A ∨ B) ⊃(♦A ∨ ♦B) @ h= λx@h. let hh ≤ αi x0= x incase x0of inl y ⇒ hh ≤ αiy | inr z ⇒ hh ≤ αizWe see that possibility distributes over disjunction without any assump-tion about accssibility between worlds. For distributed computation, theintution is as follows. We have a remote value of type A ∨ B. This must beeither a left or a right injection of a value of type A or B, respective, so wehave a remote value of type A or a remote value of type B.What is not considered is why this information should be available here:we have to “peek” at the remote value to see which it is and also bind anew value remotely. And indeed, by invoking the sequent calculus we seethat possibility does not distribute over disjunction.·; ♦(A ∨ B) =⇒ ♦A ∨ ♦B·; · =⇒ ♦(A ∨ B) ⊃ ♦A ∨ ♦B⊃RAt this point in the proof attempt we are stuck, because neither ♦A nor ♦Bcan be proved by itself, and the ♦L rule is not applicable since the judgmenton the right concerns truth rather than possibility.4 Interpreting ValidityWe would hope that the necessity operator that internalizes the validityjudgment would coincide with the modality in one of the intuitionisticmodal logics we considered in the previous lecture. Instead of guessing apriori what this might be, we just develop it as we try to relate proofs in theearlier judgmental formulation and the multiple-worlds formulation. Forthis purpose it is convenient to work in the sequent calculus. We thereforepresent the multiple-worlds sequent calculus in Figure 1. We write Γ≤forthe restriction of Γ to assumptions of the form w ≤ w0. Also note thatw ≤ α in the context introduces a new α that should be distinct from allother worlds in the antecedent or conclusion. We write Γ≤` w ≤ w0if thehypotheses in Γ≤entail that w0is accessible from w according to the currentassumptions about the accessibility relation.How do we now interpret a sequent ∆; Γ =⇒ A from the modal logic ofvalidity? It is pretty easy to see that it should be something like -?-, Γ@h =⇒LECTURE NOTES MARCH 23, 2010L16.4 Kripke Semantics for ValidityP @ w ∈ ΓΓ =⇒ P @ winitΓ, A@w =⇒ B @ wΓ =⇒ A ⊃ B @ w⊃RΓ, A ⊃ B @ w =⇒ A @ w Γ, A ⊃ B @ w, B @ w =⇒ C @ w00Γ, A ⊃ B @ w =⇒ C @ w00⊃LΓ =⇒ A @ wΓ =⇒ A ∨ B @ w∨R1Γ =⇒ B @ wΓ =⇒ A ∨ B @ w∨R2Γ, A ∨ B@w, A@w =⇒ C @ w00Γ, A ∨ B@w, B@w =⇒ C @ w00Γ, A ∨ B@w =⇒ C @ w00∨Lno ⊥R Γ, ⊥@w =⇒ C @ w00⊥LΓ, w ≤ α =⇒ A @ αΓ =⇒ A @ w RαΓ≤` w ≤ w0Γ, A @ w, A @ w0=⇒ C @ w00Γ, A @ w =⇒ C @ w00 LΓ≤` w ≤ w0Γ =⇒ A @ w0Γ =⇒ ♦A @ w♦RΓ, ♦A @ w, w ≤ α, A @ α =⇒ C @ w00Γ, ♦A @ w =⇒ C @ w00♦LαFigure 1: Intuitionistic multiple-worlds sequent calculusA @ h so that the truth assumptions in Γ and the succedent A are in thesame world. The question is how to translation ∆. It is clear that they needto be assumptions about truth of formulas Bi@wisuch that h is reachablefrom wiso they can actually be used in the proof of A @ h.First, some notation. For a context Γ = (A1, . . . , An) we write Γ@h =(A1@h, . . . , An@h). Similarly, for a context ∆ = …


View Full Document

CMU CS 15816 - Lecture

Download Lecture
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 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 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?