Higher order focusing for ordered logicRequest For Logic (RFL) #7Robert J. Simmons, Daniel Licata, and Jason ReedMarch 4, 2010In the previous note, we talked about coverage checking and case analysis with linear functions representing one-hole contexts. In this note, we push this further to do a version of higher-order focusing for ordered logic using the same notion of linear functions for one-hole contexts that reach into structures. Ordered logic occupies a unique position in this respect: because any one-hole context ƛx.Γ’(x) into an ordered structure is equivalent to ƛx.Γ,x,Δ, we can get away with explicitly representing the left and right hand sides. Experience seems to show that this is often quite a bit less satisfying than in linear logic where a one-hole context λx.Γ’(x) is equivalent to ƛx.Δ,x - the formulation we use here seems, in any case, no worse than the explicit left-hand-side-right-hand-side formulation..We only consider the Lambek calculus portion of ordered logic: that is, we don’t consider the validity or mobility modalities. Our proof appears to have the property that if we changed the properties of the context formation operator “,” we would still have a valid proof - in other words, this can be seen as a proof of rigid logic or a redundant proof of linear logic just by manipulating the algebraic properties of the comma.Higher order focusing for ordered logic Contexts are written as Γ or Δ. The context formation operator “,” is associative and commutative with unit “·”. Γ,Δ ::= hyp A⁻ | hyp Q⁺ | Γ,Δ | · We adopt the convention that a context with one hole is written as Γ’ or Δ’, a context with two holes is written as Γ’’ or Δ’’, and so on. However, these should really be understood as eta-contracted versions of the representational linear functions (ƛx.Γ’(x)), (ƛx.ƛy.Γ’’(x)(y)), and so on. The hole [] is similarly shorthand for (ƛx.x).The basic idea is that while we usually write the cut principle for ordered logic like this: If Ω ⊢ A and Ω₁,hyp A,Ω₂ ⊢ C, then Ω₁,Ω,Ω₂ ⊢ CHowever, we can talk about this cut principle more generally with one-hole contexts Ω’, where we write the cut principle like this: If Ω ⊢ A and Ω’(hyp A) ⊢ C, then Ω’(Ω) ⊢ CPatterns In higher-order focusing, propositions are handled by patterns, which are defined independently of the rules of the logic. Positive propositions are defined by constructor patterns, and negative propositions are defined by destructor patterns. A⁺ ::= Q⁺ | ↓A⁻ | A⁺ • B⁺ | 1 | A⁺ ⊕ B⁺ | 0 A⁻ ::= Q⁻ | ↑A⁺ | A⁺ ↠ B⁻ | A⁺ ↣ B⁻ | A⁻ & B⁻ | ⊤ γ ::= Q⁻ | A⁺Constructor patterns --------------- hyp Q⁺ ⊩ Q⁺ --------------- hyp A⁻ ⊩ ↓A⁻ Δ₁ ⊩ A₁ Δ₂ ⊩ A₂ ----------------- Δ₁,Δ₂ ⊩ A₁⁺ • A₂⁺ --------------- · ⊩ 1 Δ ⊩ A --------------- Δ ⊩ A ⊕ B Δ ⊩ B --------------- Δ ⊩ A ⊕ BDestructor patterns Destructor patterns are interesting because their type is ((ctx ⊸ ctx) → prop⁻ → gamma → type) - in other words, one of the outputs is not a context but rather a linear function from contexts to contexts (a context with a hole in it). When we write Δ’(Δ₁[]) we “really mean” the linear function ƛΔ₂.Δ’(Δ₁Δ₂). Δ₁ ⊩ A₁⁺ Δ₂’ ⊩ A₂⁻ > γ -------------------------- Δ₂’(Δ₁,[]) ⊩ A₁⁺ ↣ A₂⁻ > γ Δ₁ ⊩ A₁⁺ Δ₂’ ⊩ A₂⁻ > γ -------------------------- Δ₂’([],Δ₁) ⊩ A₁⁺ ↠ A₂⁻ > γ Δ’ ⊩ A > γ -------------------------- Δ’ ⊩ A & B > γ Δ’ ⊩ B > γ -------------------------- Δ’ ⊩ A & B > γ -------------------------- [] ⊩ ↓A⁺ > A⁺ -------------------------- [] ⊩ Q⁻ > Q⁻Properties of patterns In order for cut elimination to terminate, we depend on the subformula property of patterns. The introduction of, for instance, recursive types where this does not holdmay be reasonable programming languages, but can have nonterminating cut elimination procedures. (S⁺) If Δ ⊩ A⁺ then size(Δ) < size(A⁺) (S⁻) If Δ ⊩ A⁻ > γ, then size(Δ) < size(A⁻) and size(γ) < size(A⁻)Rules of the focused logic The only terribly curious part of the focused logic is our use of a representational linear function in the rule for having a one-hole context imply a one-hole context (the “holey alpha substitution” rule). Left focus Δ’ ⊩ A⁻ > γ₀ ⇐ Figure out the pattern of A⁻ Γ’ ≡ Γo’ ○ Γi’ ⇐ Γ’ is the composition of outside Γo’ and inside Γi’ Γi’ ⊢ Δ’ ⇐ Alpha substitution (= prove stuff, possibly after inverting) Γo’ ⊢ γ₀ > γ ⇐ Gamma substitution (= prove stuff, possibly after inverting) --------------- Perform Left Focus Γ’ ⊢ [A⁻] > γ Γ ≡ Γ’(hyp A⁻) Γ’ ⊢ [A⁻] > γ --------------- Enter Left Focus Γ ⊢ γ Right focus Δ ⊩ A⁺ ⇐ Figure out the pattern of A⁺ Γ ⊢ Δ ⇐ Alpha substitution (= prove stuff, possibly after inverting) --------------- Perform Right Focus Γ ⊢ [A⁺] Γ ⊢ [A⁺] --------------- Enter Right Focus Γ ⊢ A⁺Inversion Δ’ ⊩ A⁻ > γ ⇒ Δ’(Γ) ⊢ γ -------------------------- Right inversion Γ ⊢ A⁻ Δ ⊩ A⁺ ⇒ Γ’(Δ) ⊢ γ -------------------------- Left inversion Γ’ ⊢ A⁺ > γ Γ’ ≡ [] -------------------------- Atom Γ’ ⊢ Q⁻ > Q⁻Alpha substitution Γ₁ ⊢ Δ₁ Γ₂ ⊢ Δ₂ --------------- Split Γ₁,Γ₂ ⊢ Δ₁,Δ₂ --------------- Unit · ⊢ · --------------- Atomic hyp Q⁺ ⊢ hyp Q⁺ Γ ⊢ A⁻ --------------- Invert and prove Γ ⊢ hyp A⁻ Holey alpha substitution ΠΓ. ΠΔ. (Γ ⊢ Δ) -o Γ’(Γ) ⊢ Δ’(Δ) --------------------------------- Holey Γ’ ⊢ Δ’Identity This should be true and straightforward, but we don’t prove it here (Dan sketched it out on paper).Cut principles Cut is proved by a slew of mutually inductive statements, as usual. In all cases, the induction argument is either that the principal formula A⁺/A⁻/Δ/Δ’ gets smaller, or the principal formula stays the same and one of the input derivations gets smaller while the other stays the same. (+) If Γ ⊢ [A⁺] and Γ’ ⊢ A⁺ > γ then Γ’(Γ) ⊢ γ (-) If Γ ⊢ A⁻ and Γ’ ⊢ [A⁻] > γ then Γ’(Γ) ⊢ γ (R1) If Γ ⊢ Δ and