CMU CS 15816 - Lecture Notes on Computational Interpretations of Modalities

Unformatted text preview:

IntroductionStaged ComputationOperational SemanticsSource ExpressionsPossibilityVerifications and UsesProof TermsGeneralized Elimination RulesMonads and Computational EffectsRule SummaryLecture Notes onComputational Interpretations of Modalities15-816: Modal LogicFrank PfenningLecture 4January 21, 20101 IntroductionIn this lecture we present the first two of many possible computationalinterpretations of intuitionistic modal logic. The first interprets the type A as source code of type A and relates proof reduction to staged compu-tation [DP01]. For the second we analyze possibility, ♦A, and relate it tocomputational effects [PD01].2 Staged ComputationConsider for the moment the function exp : nat → nat → nat where exp n b =bn. We give two different definitions on unary natural numbers.exp (0) = λb. 1exp (s(n)) = λb. b ∗ exp n bexp0(0) = λb. 1exp0(s(n)) = let f = exp0n in λb. b ∗ f bThese are both correct implementations, but their operational behavior isvery different. The first one, when given the argument 2, performs just onestep of computation and returns a function. In an operational semanticsbased on closures, it would return a closure; here we just carry out thesubstitutions. We write M −→ M0for computational reduction which isbased on local reduction but extended by certain congruences, and M =⇒RM0for reductions which can be carried out on any subterm.LECTURE NOTES JANUARY 21, 2010L4.2 Computational Interpretations of Modalitiesexp (s(s(0))) −→∗λb2. b2∗ exp (s(0)) b2The second one actually recurses all the way to 0, returning a functionthat does not depend on the first argument any more.exp0(s(s(0))) −→∗λb2. b2∗ (λb1. b1∗ (λb0. 1) b1) b2=⇒∗Rλb2. b2∗ (b2∗ 1)We can see that the second version does a lot more computation thanthe first. However, if the resulting function is applied many times, to manydifferent bases, then the second can be more efficient, especially if the indi-cated optimization had been applied.The difference between the two programs is not the ultimately com-puted answer, but the way the computation is staged. In the second version,all computation depending on the first argument is carried out, while in thefirst version this is not the case.We would like to capture the difference between these two functions inthe type system. The goal is to devise a type system so that we can prescribea type under which the first program fails to type-check because it doesnot carry out all computation induced by its first argument, but which al-lows (essentially) the second version. The computational interpretation ofnecessity presented in the next section, achieves exactly that!3 Operational SemanticsIn order to show how necessity is related to staged computation, we willbe a bit more formal about the operational interpretation of proof terms.A simple definition is a so-called small-step semantics which applies localreductions according to a fixed evaluation discipline. We also need thenotion of a value. For concreteness, we work with a call-by-value functionallanguage although, as mentioned before, the logical underpinnings do notforce this.In the formal treatment we only consider A ∧ B, A ⊃ B, and >. This canbe extended to A ∨ B and ⊥ (see Exercise1). First, the definition of value,using a judgment M value.M value N valuehM, Ni value∧Vh i value>Vλx:A. M value⊃VLECTURE NOTES JANUARY 21, 2010Computational Interpretations of Modalities L4.3The notion of a value is related to the notion of a verification, as can beseen from the cases for conjunction and truth. However, we do not look in-side functions — they are treated entirely extensionally. We cannot analyzetheir structure, we can only apply them to arguments and observe their be-havior. Unlike verifications, this means that functional values of type A ⊃ Bmay refer to types much bigger than A or B. It is therefore a considerablechallenge to use an opaque notion of function as the foundation for logic ortype theory.The following reduction and congruence rules allow us to evaluate aclosed term to a value by repeated reduction, according to a call-by-valuediscipline. In the rule names, we use C to indicate a constructor for a typeand D a destructor.M value(λx:A. N) M −→ [M/x]N⊃DCM value N valueπ1hM, Ni −→ M∧DC1M value N valueπ2hM, Ni −→ N∧DC2M −→ M0hM, Ni −→ hM0, Ni∧C1M value N −→ N0hM, Ni −→ hM, N0i∧C2M −→ M0π1M −→ π1M0∧D1M −→ M0π2M −→ π2M0∧D2no ⊃C rule for λx. MM −→ M0M N −→ M0N⊃D1M value N −→ N0M N −→ M N0⊃D2Now we have preservation and progress property. The are formulatedonly on closed terms because, unlike the process of proof reduction, weonly evaluate expressions that are closed.Theorem 1 (Type Preservation) If • ` M : A and M −→ M0then • ` M0:A.Proof: By induction on the derivation of M −→ M0, using subject reduc-tion for the case of a redex. Theorem 2 (Progress) If • ` M : A then either(i) M value, orLECTURE NOTES JANUARY 21, 2010L4.4 Computational Interpretations of Modalities(ii) M −→ M0for some M0.Proof: By induction on the structure of M , applying inversion in each caseto obtain types for the subterms. We also have a termination property for the purely logical language,without recursion. We will not prove this property here.Theorem 3 (Termination) If • ` M : A then there exists a term V such thatV value and M −→∗V .4 Source ExpressionsNow we extend the computational interpretation sketched above to encom-pass the necessity modality A. The interpretation will go as follows:x:A true x stands for a value of type Au::A valid u stands for a source expression of type A[[M/u]]N substitute the source expression M for u in Nbox M M is a quoted source expressionlet box u = M in N evaluate M to a quoted source expression box M0and then evaluate [[M0/u]]N.We have one new kind of value: a quoted source expression.box M value VWe also have one new reduction and one congruence rule.M −→ M0let box u = M in N −→ let box u = M0in N Dlet box u = box M in N −→ [[M/u]]N DCThe crucial restriction of the typing rules ensures that in an expressionbox M, the term M does not reference any free variables x that stand forvalues. It can, however, mention variables u that stand for source expres-sions. So when we substitute [[N/u]]box M then we are building a largersource expression from two smaller ones, N and M. Conversely, whenLECTURE NOTES


View Full Document

CMU CS 15816 - Lecture Notes on Computational Interpretations of Modalities

Download Lecture Notes on Computational Interpretations of Modalities
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 Computational Interpretations of Modalities 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 Computational Interpretations of Modalities 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?