Unformatted text preview:

Derived Rules via FocusingFocusing on QuantifiersDerived Rules from QuantifiersForward ChainingUsing CelfExercisesReferencesLecture Notes onForward Chaining15-816: Linear LogicFrank PfenningLecture 13February 29, 2012In this lecture we start discussing proof search as a basic computationalmechanism; so far, it has only been proof reduction. Computation via proofsearch is the technique underlying logic programming. It provides a fun-damentally different way of combining programming with reasoning, byusing reasoning itself as the source of computation.The particular instance of this idea we introduce in this lecture is linearforward chaining, also called linear bottom-up logic programming. Linear for-ward chaining is supported in the Celf implementation [SNS08]1of the CLFlogical framework [WCPW02, CPWW02], and also in LolliMon [LPPW05].Our goal for this lecture is to provide enough intuition regarding for-ward chaining and its implementation that we can write Celf code im-plementing substructural operational semantics. Some of this will remainmysterious since CLF provides a dependent type theory that we haven’tcovered yet in this course.1 Derived Rules via FocusingWe previously discussed that we can go from certain propositions back toderived rules via the process of focusing. Let’s reconsider this and then addquantifiers.Assume we have an inference ruleqd d n1More information on the Software page for this courseLECTURE NOTES FEBRUARY 29, 2012Forward Chaining L13.2When we explained linear inference we used this rule for the purpose ofeffecting a state transition. For example,q, n −→ d, d, n, nIn general, applying linear rules of inference allowed transitions∆ −→ ∆0to be described by inference rules. We allowed the state to contain persis-tent as well as ephemeral propositions, so with our new notation we mightrewrite this as(Γ ; ∆) −→ (Γ0; ∆0)where Γ ⊆ Γ0.When we switched from linear inference to a sequent calculus (since wewere unable to represent nested hypothetical judgments in a satisfactoryway), we turned our sample rule from above into a persistent propositionq ( d ⊗ d ⊗ nIn which way does this now represent a possible state transition? Assumewe have the proposition above as part of Γ and a stable sequentΓ ; ∆ → CRecall that a sequent if stable if all propositions in ∆ are negative or positiveatoms, and C is either positive or a negative atom.At this point we can potentially focus on any proposition in Γ or ∆(except for positive atoms), or on C (unless it is a negative atom). Considerthe derivation if we focus on q ( d ⊗ d ⊗ n ∈ Γ:...Γ ; ∆1→ [q]...Γ ; ∆2, d ⊗ d ⊗ n → CΓ ; ∆2, [d ⊗ d ⊗ n] → CblurLΓ ; ∆, [q ( d ⊗ d ⊗ n] → C(LΓ ; ∆ → CfocusL!where ∆ = (∆1, ∆2). Note that after the first focusing step, all the rules areforced.Let’s now fix the polarity of all atoms to be positive. In that case, the firstremaining subgoal can only succeed if Γ contains q or ∆1= q. Let’s assumeLECTURE NOTES FEBRUARY 29, 2012Forward Chaining L13.3we are in a situation where we know that q cannot be in Γ, so ∆1= q isforced. Completing the first subproof and substituting in our knowledgeon the form of ∆, we obtain:Γ ; q → [q]idq+...Γ ; ∆2, d ⊗ d ⊗ n → CΓ ; ∆2, [d ⊗ d ⊗ n] → CblurLΓ ; ∆2, q, [q ( d ⊗ d ⊗ n] → C(LΓ ; ∆2, q → Cfocus!Multiplicative conjunction is invertible on the left. So in a full focusingsystem, the inversion on d ⊗ d ⊗ n is also forced. We arrive at:Γ ; q → [q]idq+Γ ; ∆2, d, d, n → CΓ ; ∆2, d ⊗ d ⊗ n → C⊗L × 2Γ ; ∆2, [d ⊗ d ⊗ n] → CblurLΓ ; ∆2, q, [q ( d ⊗ d ⊗ n] → C(LΓ ; ∆2, q → Cfocus!At this point we again have a stable sequent, since we assumed the originalgoal sequent was stable. Writing it out explicitly, we obtain the followingderived rule:Γ ; ∆, d, d, n → CΓ ; ∆, q → CA remarkable observation is that in a system of focusing, this representsthe only way we can use the persistent assumption q ( d ⊗ d ⊗ n. In otherwords, we could throw away this assumption and just agree to use theabove derived rule instead.Looking at the derived rule we can now see how state change is repre-sented in the sequent calculus. If, under linear inference, we had a transi-tion∆ −→ ∆0then using focusing on the corresponding proposition in Γ we obtain thetransitionΓ ; ∆0→ CΓ ; ∆ → CLECTURE NOTES FEBRUARY 29, 2012Forward Chaining L13.4More generally, if we allow persistent propositions as well, then the contextΓ plays two roles: one for the propositions representing rules Γr, the otherfor persistent atomic propositions. Then a transition (Γ ; ∆) −→ (Γ0; ∆0)becomesΓr, Γ0; ∆0→ CΓr, Γ ; ∆ → CNote that the right-hand side C plays no significant role here.In summary, we can model linear inference using persistent proposi-tions and focusing by assigning all atoms a positive polarity.2 Focusing on QuantifiersOur goal for this lecture is to implement substructural operational seman-tics as an executable forward-chaining logic program. Our discussion ofchaining and focusing so far lacks quantifiers, which are necessary for manyprograms.The universal quantifier is invertible on the right, so we focus on theleft and invert on the right.Ψ, n:τ ; Γ ; ∆ → A{n/x}Ψ ; Γ ; ∆ → ∀x:τ.A∀RΨ ` M : τ Ψ ; Γ ; ∆, [A{M/x}] → CΨ ; Γ ; ∆, [∀x:τ.A] → C∀LThe right rule introduces a new parameter n into the term context Ψ; theleft rule instantiates the quantifier with a term of the correct type.Conversely, the existential quantifier is invertible on the left, so we focuson the right and invert on the left.Ψ ` M : τ Ψ ; Γ ; ∆ → [A{M/x}]Ψ ; Γ ; ∆ → [∃x:τ.A]∃RΨ, n:τ ; Γ ; ∆, A{n/x} → CΨ ; Γ ; ∆, ∃x:τ.A → C∃LIt is straightforward to extend the theorems regarding the soundness andcompleteness of chaining and focusing to the quantifiers. Crucial is theobservation that we can consider A{M/x} to be strictly smaller than ∃x:τ.Aand ∀x:τ.A, because A{M/x} has fewer quantifiers and connectives.3 Derived Rules from QuantifiersOnce we add quantifiers, our state transitions have to account for the pos-sibility that new term parameters are introduced, either by the ∃L rule orLECTURE NOTES FEBRUARY 29, 2012Forward Chaining L13.5the ∀R rule. Then a state transition(Ψ ; Γ ; ∆) −→ (Ψ0; Γ0; ∆0)with Ψ ⊆ Ψ0and Γ ⊆


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?