tag:blogger.com,1999:blog-827419514217130218.post2192156557514668949..comments2015-10-26T03:12:33.234-04:00Comments on Request for Logic: Differently-higher-order-focusingRobhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comBlogger4125tag:blogger.com,1999:blog-827419514217130218.post-43628360093462365992013-01-11T16:48:50.084-05:002013-01-11T16:48:50.084-05:00gasche: yes, I agree with all of this, including t...gasche: yes, I agree with all of this, including the fact that the straightforward proof obligation of my union means that you have to include two proofs instead of one for A+A. Of course, this is not a substructural logic, so you can always do that - the metatheory makes the difference between one and many copies of a proof irrelevant, I think. (Certainly this is true in the finitary case.)<br /><br />The set-like notation is the older one; in my thesis and some other places I use a function-ey notation for the left rule for equality; in a lot of Miller's work he does the exact same thing with a set-based notation. We ought to be able to move pretty seamlessly between these two views if I'm not mistaken.Robhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-35678393385355880802013-01-11T13:56:17.401-05:002013-01-11T13:56:17.401-05:00I'm coming back to this much later because I&#...I'm coming back to this much later because I'm now interested in term<br />search for other reasons<br />( http://gallium.inria.fr/blog/singleton-types-for-code-inference/ ). I think<br />it is possible to restore the order-independence of your formulation<br />by seeing I⁺{A}(P) and P(Δ) not as a judgment, but as a set of<br />judgment: I⁺{A} would have type<br />(Context → Set(Judgment)) → Set(Judgment); then you can define I{0}(P)<br />as the empty set, I{A*B} is still I{A}(ΔA.I{B}(ΔB.P(ΔA,ΔB))), and the<br />assumptions for (Δ,[A⁺] ⊢ C) are the I{A}(ΔA. {Δ,ΔA ⊢ C}). This<br />presentation corresponds to unfolding the patterns to full depth<br />(irrespectively of when 0 is encountered), keeping less structure on<br />the proof obligations to not distinguish anymore these different<br />trivial obligations.<br /><br />I think the full type for I,<br />(Context → Set(Judgment)) → (Positive → Set(Judgment)), corresponds to<br />doing some form of continuation-passing style. The structure could be<br />simplified with an operator I{A} returning directly a set of contexts,<br />that are exactly the set of realizing contexts Δ such that the pattern<br />judgment Δ ⊩ A holds. Noting contexts (A1,..,An) and sets {Δ₁,...Δn}:<br /><br />I{p+} := {(p+)}<br />I{A-} := {(A-)}<br />I{0} := {} (empty set)<br />I{1} = {()} (empty context singleton)<br />I{A+B} := I{A} U I(B) (union)<br />I{A*B} := { Δ₁,Δ₂ | Δ₁ ∈ I{A}, Δ₂ ∈ I{B} } (cartesian product + context concatenation)<br /><br />Remark the union in the I{A+B} rule; there is the question of whether<br />it is a disjoint sum or the usual set union, which makes a difference<br />in case some of the contexts on both sides happen to be the same<br />(eg. A+A or even (1*A)+(A+0)). The set union automatically recognizes<br />commons contexts and merge them, so they result, after the focusing<br />step, in one proof obligation instead of several identical<br />ones. I think that your formulation, when read naively, would tend to<br />use a disjoint sum, while Noam's quantification apparently suggests<br />a set union.<br />gaschehttp://www.blogger.com/profile/06100241581708586136noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-65363769578861578982012-04-03T07:49:24.348-04:002012-04-03T07:49:24.348-04:00I appreciate the irony. But working out structural...I appreciate the irony. But working out structural focalization took weeks and weeks (and the writing was longer than the proving); getting something out of my system so I can return to more pressing writing is a worthwhile use of two hours, I think. Also, trying to sketch a bit of what I'm thinking is the best way to make sure that I'll have some clue what *I* was thinking when I look back at this in the future (as opposed to writing a few sketchy comments in the version-controlled text file that passes as my research notebook), and that's the real reason this blog exists, anyway.<br /><br />Fixed the bugs you mention, I think. I explicitly intended to make this presentation shiftless, so I fixed the lurking shift by removing the one place a shift appeared in the pattern rule for Δ ⊩ A- > A-. (Focusing was developed without shifts, and the use of shifts remains a minority view in the focusing proof theory literature, it's just a minority view I favor.)<br /><br />You're absolutely right that I am ordering the inversions in a certain sense - the proof obligation for proving (Δ, [0⊗(1⊕1)] ⊢ C) is ⊤, and the proof obligation for proving (Δ, [(1⊕1)⊗0] ⊢ C) is ⊤ × ⊤. So the confluence proof in this setting would be to show that all these potential proof obligations are type isomorphisms. I think confluence is eventually a property we ought to grapple with, but it's nice to be able to prove cut, identity, and focalization without dealing with that question - especially, as you say, in a mechanized setting. I'll be interested to see if it continues to always be the case that this is doable.Robhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-41291942083064876912012-04-03T04:23:39.276-04:002012-04-03T04:23:39.276-04:00I found it nice to read about your musing, even as...I found it nice to read about your musing, even as an outsider to the field -- though I must say the idea of "I spent too much time on this, the best thing to do now is to write a blog post about it" looks quite ironic.<br /><br />A few typos:<br /><br />- in the rules for Δ ⊩ A⁺, there is a shift lurking, and you wrote the same A⊕B rule twice.<br /><br />- there is a closing parenthesis missing in the first occurence of I⁺{A⁺}(Δ.P(Δ)), first line of the "Alternate formulation" section<br /><br />- η-contract misses the '-' which would make it more readable (besides I think using the η-contracted form in the left-hand-side of the definitions of I⁺ and I⁻ would indeed be more readable, by allowing to concentrate visual weight on the parts that matter)<br /><br />- the rule for I⁻{A⊸B} should have I⁻{B} rather than I⁺{B}<br /><br /><br />Finally, I have a probably very naive question. As I'm not familiar with the litterature you're talking about, I'm not sure what those examples of "fixed order" vs. "confluent non-determinism" are (maybe an example would help), but I was wondering if you didn't understand a fixed order of some sort in you I⁺{A⊗B} and I⁻{A⊸B} definitions. For example you have:<br /><br /> I⁺{A⊗B}(P) := I⁺{A}(Δᴀ. I⁺{B}(Δʙ. P(Δᴀ,Δʙ))<br /><br />You could have evaluated B's judgement context first, then A's.<br /><br /> I⁺{A⊗B}(P) := I⁺{B}(Δʙ. I⁺{A}(Δᴀ. P(Δʙ,Δᴀ)))<br /><br />I think you could observe the difference on, for example, 0⊗(1⊕1). Is this the same kind of "fixed order" that you were talking about, or maybe a lesser issue?<br /><br />(For the record and as a general comment, I don't dislike the idea of having non-determinism and confluence to prove, because I suspect that in general such confluence result tells you nice things about the system, that you maybe wouldn't have listened about if you made the problem go away with a fixed order. At the same time I tend to find confluence questions boring – in the majority of case where they work out easily — so I understand the designer's choice to lessen the proof burden, especially in a mechanized setting.)gaschehttp://www.blogger.com/profile/06100241581708586136noreply@blogger.com