tag:blogger.com,1999:blog-827419514217130218.comments2015-10-26T03:12:33.234-04:00Request for LogicRobhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comBlogger111125tag: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-88338101351741380502012-10-17T08:55:06.931-04:002012-10-17T08:55:06.931-04:00Just for reference, CiteSeerX has a non-paywalled ...Just for reference, CiteSeerX has a non-paywalled copy of the F-Pop paper here: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.183.9267david.givenhttp://www.blogger.com/profile/09478403138062371685noreply@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.comtag:blogger.com,1999:blog-827419514217130218.post-51831291398558200702012-03-06T10:59:56.913-05:002012-03-06T10:59:56.913-05:00Thank you for the discussion and the summary. I di...Thank you for the discussion and the summary. I didn't mean to be tricky, but I now understand the issue better. Thanks for clarifying, giving pointers to relevant topics, and also suggesting a few significant topics for future research. This is what makes academic discussion fun and productive.William Cookhttp://www.blogger.com/profile/13627036863243572742noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-58216690559217605182012-03-06T08:06:21.693-05:002012-03-06T08:06:21.693-05:00Excellent, thanks.
My summary, then is that both...Excellent, thanks. <br /><br />My summary, then is that both Cook's set object and my set negative-recursive-type are based on the same functor F that is not positive-in-the-sense-of-stuff-occurring-to-the-left-of-an-arrow (hence not covariant). However, the interpretation of that functor as a negative recursive type is, in fact, different than Cook's interpretation into System F. Precisely characterizing this difference is maybe not straightforward for the set example, but for other examples this can be described as a difference in termination behavior.Robhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-10725946432634308502012-03-06T07:38:27.427-05:002012-03-06T07:38:27.427-05:00This is pretty close to what I mean. One correctio...This is pretty close to what I mean. One correction is that algebras are not inductive types, only *intitial* algebras are, and dually, for coinductive types, only *final* coalgebras are coinductive types. This is basically because you need initiality/finality for the induction/coinduction principle.<br /><br />However, being the initial algebra (or final coalgebra) of a functor forbids negative occurences in the type scheme, because satisfying functoriality basically requires that a covariant map functional exist. The ADJ group looked at arbitrary algebras and coalgebras, because they wanted to consider non-free datatypes (eg., lists up to associativity). But IMO, it was the ban on negative occurences that was the big roadblock to their project. <br /><br />If you look at pg. 565 of the Cook paper you link to, you'll see he does something very sneaky. He gives an encoding of set objects into System F. That is, he gives a type operator F(a), which includes negative occurences, and then uses the traditional encoding of coinductive types into F, as Obj(F) = exists r. r * (r -> F(r)). <br /><br />However, we only know that exists r. r * (r -> F(r)) is a coninductive type for positive F. Its behavior for mixed-variance F is not well-understood, and so Cook's proposed interpretation of the recursive type constructor is *not* the recursive type you're used to from ML or Haskell. This is because F is total, and fully general mu-types let you code up infinite loops. (So it is not the one that CPBV would give you if you allowed negative occurences.) <br /><br />The mu he is using is different, and not very well-understood. I call it the Mendler-style mu -- there was a paper at ICFP last year about this last year, and Bob Atkey, Sam Lindley, and Jeremy Yallop had a paper ("Unembedding DSLs") about its connections to PHOAS.Neel Krishnaswamihttp://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-51155012344473060752012-03-06T06:57:02.029-05:002012-03-06T06:57:02.029-05:00Neel - I think you're making some good points,...Neel - I think you're making some good points, but you're introducing a bunch of terms that weren't present in this discussion before, so help me catch up a bit :-). In particular, when you say "abstract type," are you talking about "positive recursive type" as Levy defines them, or are you talking about abstract data types as Cook describes them? I was trying to be pretty careful about *not* making any statements or claims about the relationship between positive recursive types and what Cook called ADTs, as I'm not 100% certain whether the relationship between those two ideas exists or is precise. <br /><br />Is your point in the first paragraph possible to re-state as follows? "Algebras = inductive types, but (datatypes in ML/positive recursive types in CPBV) aren't inductive types because of occurrences of the recursive type variable to the left of an arrow. Coalgebras = coinductive types, but negative recursive types in CPBV aren't coinductive types because of occurrences of the recursive type variable to the left of an arrow; this happens in the 'union' method for set objects." <br /><br />I'm putting words in your mouth here, so I apologize if this is not what you were trying to say. This was something that I was thinking as I was writing the post but lacked the evidence to say, and it seems to be implicit in what you're saying in the first paragraph.Robhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-85860339134011780832012-03-06T04:38:58.980-05:002012-03-06T04:38:58.980-05:00Abstract types are not algebras, and objects are n...Abstract types are not algebras, and objects are not coalgebras. The ADJ group (Thatcher, Wright, and co) advanced this view back in the 70s, and they ran into the insurmountable problem that (co)algebras are functorial: i.e., it's most natural to view signatures as functors and then the functoriality requirement prevents negative occurrences of the carrier in arguments to the generators. This rules out a lot of signatures that (a) work, and (b) are useful (eg, binary methods in OO languages). <br /><br />We need to strengthen our understanding of uniformity from functoriality to relational parametricity before we can say the right things about these programs. However, this reveals the problem that focusing is not powerful enough to tell us what "purely functional" means. That is, equivalence of normal forms in a focused calculus is finer than the equivalence of purely functional programs. Consequently, some of System F's more astonishing isomorphisms -- e.g., that A is isomorphic to all a. (A -> a) -> a -- don't have a good proof-theoretic explanation, since such isos can cross polarity boundaries (eg, if A is positive).Neel Krishnaswamihttp://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-90512043930386788832012-03-05T23:52:02.315-05:002012-03-05T23:52:02.315-05:00Bob, why don't you point out that Simula preda...Bob, why don't you point out that Simula predates all these references? You have a very selective memory. But anyway, who *cares* that it was discovered many times. This doesn't invalidate the use of the term Object or the amazing things that people have done with the idea.William Cookhttp://www.blogger.com/profile/13627036863243572742noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-86785586152541453912012-03-05T23:19:41.206-05:002012-03-05T23:19:41.206-05:00MacQueen wrote an excellent retrospective for the ...MacQueen wrote an excellent retrospective for the Gilles Kahn volume.Existential Typehttp://www.blogger.com/profile/05595505123938492280noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-26240178842521908532012-03-05T17:32:55.085-05:002012-03-05T17:32:55.085-05:00This was my intended point in Footnote 3; I was at...This was my intended point in Footnote 3; I was attempting (struggling, even) to remain agnostic on what the name for anything is or should be. What's a good reference for Kahn-MacQueen networks?Robhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-50350332260152183182012-03-05T17:24:43.634-05:002012-03-05T17:24:43.634-05:00I'm not sure why a recursive record of functio...I'm not sure why a recursive record of functions type is being renamed, but it's an idea that's as old as the hills, and is a quite fine using functions to abstract behavior, exploiting the fact that functions are "black boxes" (i.e., of negative type). One of the earliest uses of this idea is in Kahn-MacQueen networks, which date back to the 1970's, but I am sure there are older versions than that. One may call these things "objects", but (a) its a retronym for a pre-existing condition, and (b) the term "object" is so vague that it's a good name for just about anything.Existential Typehttp://www.blogger.com/profile/05595505123938492280noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-26461110824305291552012-03-05T10:14:50.726-05:002012-03-05T10:14:50.726-05:00gasche: Thanks! I believe that the lazy_t encoding...gasche: Thanks! I believe that the lazy_t encoding is just as (if not more) faithful to the CPBV code - you'll notice in the revision history that I only made the records correctly lazy (adding the thunk) a few hours ago, it was an oversight originally. <br /><br />I think you may be right about ν versus μ, but because I wasn't certain (read: was lazy) I avoided any discussion of least and greatest fixed-points and just followed Levy's lead - he uses μ for both fixedpoints in his book.Robhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-37186233862348433892012-03-05T10:03:17.924-05:002012-03-05T10:03:17.924-05:00Thanks for this blog post! I'm quite intereste...Thanks for this blog post! I'm quite interested in the interaction of<br />focusing and evaluation-order or pattern-matching, and I've had<br />"getting sense of the various works on the topic" on my hobby<br />TODO-list for quite a while, but those CBPV posts make for a great<br />introduction, that is not as exhausting as reading a full paper on the<br />topic.<br /><br />I have done an OCaml porting of your SML code. This lifts the<br />restriction that a constructor is need: in OCaml, record types are not<br />anonymous but generative, so a iso-recursive type definition need to<br />go through either a sum or a record type.<br /><br />I have done one version with your (unit -> foo) wrapping for value<br />recursion, and one using lazyness instead:<br /> - https://gitorious.org/gasche-snippets/object-encoding-example/blobs/master/iset.ml<br /> - https://gitorious.org/gasche-snippets/object-encoding-example/blobs/master/iset_lazy.ml<br /><br />There is one point of the port that I'm not sure is an exact<br />translation; I have combined the negative layer (unit -> ...) or<br />(... lazy_t) in the definition of the iset type with the restriction<br />on which sort of values can be defined recursively. In your code,<br />there is a (fun () => ...) for negativity, and one other for<br />recursivity. I'm under the impression that it is meaningful to confuse<br />the two aspects, but I may be wrong, and maybe the translation has<br />a different behavior for this reason.<br /><br /><br />Finally, a small remark: in the negative case, does μ denote<br />a "smallest" or "largest" fixpoint? I'm used to think of coinductive<br />types such as streams in terms of largest fixpoint, but maybe the<br />distinction doesn't need to be done with the polarity information. In<br />any case, the suggestion: it seems the custom to use ν, rather than μ,<br />for coinduction; maybe you could use ν as well in your<br />presentation. The clever color scheme is already good enough to make<br />the distinction, but a different syntax would make it even clearer.gaschehttp://www.blogger.com/profile/06100241581708586136noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-54562409775394304562012-03-05T09:51:53.947-05:002012-03-05T09:51:53.947-05:00Good question, let me see if I can answer it. A qu...Good question, let me see if I can answer it. A quick analogue: the type of map over my lists would be "U(int -> F int) -> list -> F list" - we wrap the function (computation) type in a U so it can be passed to a function. <br /><br />More detail: one thing I didn't mention here, but has been mentioned elsewhere, is that implication is a negative (computation) type with the structure (PosType -> NegType). In other words, CPBV is very "call by value" in the sense that the *only* thing you can pass to a function is a value - value code with value (positive) type. All variables in CPBV have positive (value) type, by the way. (This can trip people up because it's often different between the CPBV-based systems and the focusing-based systems, but if you're not familiar with the latter you shouldn't have to worry.)<br /><br />So, we can only pass values as arguments to functions, but functions and (Cook) objects aren't values (positive/blue), they're computations (negative/red). The reason this isn't totally horrible is that we can make any computation type (like "iset" or "int -> F int") into a value type by wrapping it in the "U" - "U (int -> F int)" is the value type of (thunked, that is, suspended, not-running) functions from ints to ints, and "U iset" is the value type of a a thunked (Cook) object. When we write ((force x).union y), both x and y have type "U iset." Then (force x) is computation code of type "iset," ((force x).union) is computation code of type "U iset -> iset" - that is, a computation waiting on a thunked, not-running, set object.Robhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-10833046292131435382012-03-05T09:08:21.829-05:002012-03-05T09:08:21.829-05:00Why are you making the type of union: U iset ->...Why are you making the type of union: U iset -> iset ?Manuel Simonihttp://www.blogger.com/profile/07840673741485280526noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-49926993531410450922012-01-17T05:46:39.656-05:002012-01-17T05:46:39.656-05:00Let's try this again, shall we.
"In rela...Let's try this again, shall we.<br /><br />"In relation to argument from Russell O'Connor, I reject the plausibility or even the possibility that the ACM might "go evil" for the reasons I've outlined above. Since ACM ultimately carries out the well thought out wishes of the community itself since the decision makers are the very members of the community who are impacted by those decisions, it is just not possible for such a scenario to occur."<br /><br />The fact that an individual is part of a group which will become negatively influenced by certain actions does not mean this individual will not have an incentive to do so; it just means that such an incentive would come from someone for whom the interests of said group does not matter. This is the definition of corruption and only the most naiive would not realize that a position that enables this -- even inadvertently -- is very vulnerable. It's not like companies are forever; if someone in the ACM enronizes it (by accepting outside incentives which ultimately work against the ACM's users', and therefore the ACM's, interest) he can just go on with his life; in fact the quicker he can do it the shorter the agony, so that's an extra incentive to burn the grassfields and get out.<br /><br />Saying "I'm one of you" is the first thing the wolf in sheep's skins does.cheaterhttp://www.blogger.com/profile/17582891779655886034noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-20938876715922534262012-01-15T07:41:08.420-05:002012-01-15T07:41:08.420-05:00This comment has been removed by a blog administrator.cheaterhttp://www.blogger.com/profile/17582891779655886034noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-5190741008740494962012-01-15T07:36:34.189-05:002012-01-15T07:36:34.189-05:00This comment has been removed by the author.cheaterhttp://www.blogger.com/profile/17582891779655886034noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-91954031556768660702012-01-15T07:33:50.768-05:002012-01-15T07:33:50.768-05:00This comment has been removed by the author.cheaterhttp://www.blogger.com/profile/17582891779655886034noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-53195816467990451252012-01-09T20:22:38.625-05:002012-01-09T20:22:38.625-05:00Rich: I can respect this point, but this is one pl...Rich: I can respect this point, but this is one place where I agree with Scott Delman - there's a lot of gray area.<br /><br />I think there is definitely an ethical dimension to open access, but in my area of computer science, I happen to think that the any "green" SHERPA/RoMEO policy meets a reasonable ethical standard of allowing ideas to be accessed and disseminated. I understand how it might be quite different for someone doing medical/science research or research in an area with a stronger ethical considerations against publishing preprints ArXiV-style.Robhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-13446891300872075762012-01-09T16:22:52.869-05:002012-01-09T16:22:52.869-05:00The answer is simply to publish in an OA journal. ...The answer is simply to publish in an OA journal. Don't publish in journals that support RWA. It is unethical to do so when we know they will restrict the research to an unreasonable degree. My blog post on this: Ethical responsibilities of scientists: re proposed US federal legislation on open science. ibiosphere.blogspot.comRich Jorgensenhttp://www.blogger.com/profile/08713562874646987566noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-29286944278696884702012-01-09T12:53:51.120-05:002012-01-09T12:53:51.120-05:00How are different fields navigating the new landsc...How are different fields navigating the new landscape? I know that the NIH policy requiring placement in a repository is being accommodated (though the for profit publishers don't like it); it is having an unintended consequence, the devaluation of research that isn't NIH funded (in, say, psychology) because that work doesn't end up in the database. The devaluation isn't huge, because university based researchers still have plentiful access (right now, though I see these budgets being cut as public universities, in particular, face challenges). But, it's there. <br /><br />Is the model in computing different enough that ACM can maintain paywall access and still be relevant? <br /><br />How are physics and chemistry navigating the new publishing landscape?zbhttp://www.blogger.com/profile/13205346985598789513noreply@blogger.com