tag:blogger.com,1999:blog-11295132.post1709827116482950347..comments2014-12-04T12:37:01.029-08:00Comments on A Neighborhood of Infinity: From Löb's Theorem to Spreadsheet EvaluationDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger25125tag:blogger.com,1999:blog-11295132.post-23088801051194867702014-09-20T03:14:27.576-07:002014-09-20T03:14:27.576-07:00After reading Ashley Yakeley's comments, I beg...After reading Ashley Yakeley's comments, I began to wonder what it would take to have a "proper" implementation that relied on the right assumptions. I ended up writing this post: <a href="http://lesswrong.com/r/discussion/lw/l0d/a_proof_of_l%C3%B6bs_theorem_in_haskell/" rel="nofollow">A proof of Löb's theorem in Haskell</a>.Vladimir Slepnevhttp://www.blogger.com/profile/17185829573201572625noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-81999877146839871102013-08-17T12:26:49.559-07:002013-08-17T12:26:49.559-07:00Noting for posterity, as this is where folks go wh...Noting for posterity, as this is where folks go when they seek the definition for this combinator:<br /><br />This version improves the sharing slightly.<br /><br /><br /> loeb x = xs where xs = fmap ($xs) xEdward Kmetthttp://www.blogger.com/profile/16144424873202502715noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-83706171128672223512012-05-24T02:31:56.292-07:002012-05-24T02:31:56.292-07:00I would like to know how should the diamond operat...I would like to know how should the diamond operator be represented in Haskell :)Hussain Sobhynoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-46411280161237644352012-05-22T12:56:33.495-07:002012-05-22T12:56:33.495-07:00If the box is represented in Haskell as a monad. W...If the box is represented in Haskell as a monad. What will be the representation of the diamond?s7shttp://www.blogger.com/profile/14600246493528044733noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-59232053331944599772012-05-22T12:54:52.597-07:002012-05-22T12:54:52.597-07:00This comment has been removed by the author.s7shttp://www.blogger.com/profile/14600246493528044733noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-85879268577270827712012-03-08T12:41:30.978-08:002012-03-08T12:41:30.978-08:00For the interested, Eliezer Yudkowski has a
...For the interested, Eliezer Yudkowski has a <br /><a href="http://yudkowsky.net/rational/lobs-theorem" rel="nofollow"> 'Cartoon Guide' to Löb's theorem</a>myzoskihttp://www.blogger.com/profile/02622704681931775367noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-48882005448451344582007-05-05T14:51:00.000-07:002007-05-05T14:51:00.000-07:00Henning,In both the 'humour' and 'proposal' catego...Henning,<BR/><BR/>In both the 'humour' and 'proposal' categories!sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-74149158695532795032007-05-05T14:03:00.000-07:002007-05-05T14:03:00.000-07:00Do you know my opinion of a Num instance for funct...Do you know <A HREF="http://www.haskell.org/haskellwiki/Num_instance_for_functions" REL="nofollow">my opinion</A> of a Num instance for functions?Henning Thielemannnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-40718747921965974552007-02-03T12:32:00.000-08:002007-02-03T12:32:00.000-08:00Nick,
If you're still reading, I just worked out ...Nick,<br /><br />If you're still reading, I just worked out a tiny bit more detail <a href="http://sigfpe.blogspot.com/2007/02/comonads-and-reading-from-future.html">here</a>.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-43918237129804703892007-01-31T15:08:00.000-08:002007-01-31T15:08:00.000-08:00Nick,
Well spotted! I looked hard on the web for ...Nick,<br /><br />Well spotted! I looked hard on the web for something with the same signature as loeb but couldn't find anything. I haven't yet fully proved to myself that loeb and cfix are the same thing. They look like they do the same thing but it seems curious that I'm able to define loeb for any Functor, not just for a Comonad. When I have some time I'll investigate further - comonads being a bit of a hobby of mine these days.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-46743940313358331602007-01-31T14:25:00.000-08:002007-01-31T14:25:00.000-08:00You have a neat derivation of "cfix" there!
I bum...You have a neat derivation of "cfix" there!<br /><br />I bumped into this once myself when attempting to improve on the Essence of Dataflow semantics. I eventually found this <a href="http://www.mail-archive.com/haskell@haskell.org/msg17244.html">post</a> by David Menendez. <br /><br />cfix :: Comonad d => d (d a -> a) -> a<br /><br />which is dual to <br /><br />mfix :: Monad t => (a -> t a) -> t a<br /><br />We know mfix needs a special Haskell definition for each monad, but cfix does not, it's applicable to all comonads.<br /><br />Usually, modal box matches a comonads an modal diamond matches a monad. S4's theorems support the functions:<br /><br />a -> Dia a<br />Dia (Dia a) -> Dia a<br />Box a -> a<br />Box a -> Box (Box a)<br /><br />which are (co)unit and (co)join of the (co)monad.<br /><br />Along the lines of your spreadsheet analogy, you're not alone! I've written up a "non-empty graph" data structure as a comonad with the intent of making a cool spreadsheet semantics in Haskell. I need to dust that off someday...<br /><br />In regards to fmap not being provable in modal logic, there might be a nuance here. In haskell, the type A matches Box A from a corresponding modal logic: values in Haskell are immutable and thus "necessary" (i.e. Haskell always assumes the trivial Identity comonad). So the type of fmap (for a monad) actually corresponds to:<br /><br />fmap :: Box (a -> b) -> Dia a -> Dia b<br /><br />which is a modal logic theorem (called Dia-K).<br /><br />Satoshi Kobayashi's "Monad as Modality" is good reference (but sometimes hard to obtain). In regards to Yakeley's Code modality, monads seem to play a role in staged-computing, don't remember a reference though. Template Haskell maybe?<br /><br />- Nick FrisbyAnonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-75212337099399271672007-01-28T10:39:00.000-08:002007-01-28T10:39:00.000-08:00Modal logics usually have these rules:
f (a -> ...<i>Modal logics usually have these rules:<br /><br /> f (a -> b) -> f a -> f b<br /><br />(This corresponds to the Applicative class, which may one day be made a superclass of Monad.)<br /><br /> f a -> a<br /><br />Monads do not in general satisfy this. Perhaps comonads or something?</i><br /><br />Yes, they are connected to <a href="http://www.eyrie.org/~zednenem/2004/hsce/Control.Comonad.html">comonads.</a><br /><br />Two functions<br />extract :: w a -> a<br />and<br />extend :: (w a -> b) -> w a -> w b<br />which follow these laws:<br /> extend extract == id<br /> extract . extend f == f<br /> extend f . extend g == extend (f . extend g)<br />define a comonad.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-83515115343409861642006-12-27T18:10:00.000-08:002006-12-27T18:10:00.000-08:00David,
Num's sneaky!David,<br /><br />Num's sneaky!sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-5769694882790266662006-12-27T15:28:00.000-08:002006-12-27T15:28:00.000-08:00Disregard my last comment. After loading up the po...Disregard my last comment. After loading up the post in GHCi, I see why it works. The Num definition for functions allows 3 and 17 to be functions which are basically const 3 and const 17.Davidhttp://www.blogger.com/profile/03396164169951516460noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-34475318717397161522006-12-27T15:25:00.000-08:002006-12-27T15:25:00.000-08:00I realise this is now something of an old post but...I realise this is now something of an old post but hopefully you're still picking up the comments. Just a quick question.<br /><br />Your test3 doesn't seem to be a monomorphic list (and therefore ill-typed in Haskell), is this deliberate? Or were the 3 and 17 meant to be const 3 and const 17 respectively?<br /><br />Great mind-boggling stuff, by the way :)Davidhttp://www.blogger.com/profile/03396164169951516460noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-25840936610728624712006-11-24T17:08:00.000-08:002006-11-24T17:08:00.000-08:00matthias,
Just had a look at that paper, which I ...matthias,<br /><br />Just had a look at that paper, which I didn't know. It looks like it addresses stuff I've been tossing about in my head for a little while. Not being in academia, I've no idea what are the good papers to read unless they get posted on Lambda the Ultimate. :-)sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-49690222750831934052006-11-24T16:39:00.000-08:002006-11-24T16:39:00.000-08:00Do you know Benton et al.'s paper?Do you know Benton et al.'s <a href="http://dx.doi.org/10.1017/S0956796898002998">paper</a>?Matthiashttp://www.blogger.com/profile/11645785715024119039noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-72013013946952356262006-11-24T14:03:00.000-08:002006-11-24T14:03:00.000-08:00Lennart,
In the special case where f is the ident...Lennart,<br /><br />In the special case where f is the identity functor, loeb is precisely the usual Y combinator, so it's about as circular as you can get. I just used the type corresponding to Löb's theorem as inspiration for a function definition of that type. However, I must read <a href="http://lambda-the-ultimate.org/node/1760">this</a> paper which makes proper use of a complete provability logic.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-25882807886793309332006-11-24T12:44:00.000-08:002006-11-24T12:44:00.000-08:00Is your way of proving Löb's theorem anything like...Is your way of proving Löb's theorem anything like the regular proof? Your code uses recursion in a way that looks dangerously like a circular proof.Lennarthttp://www.blogger.com/profile/07327620522294658036noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-82232046097300747092006-11-24T01:07:00.000-08:002006-11-24T01:07:00.000-08:00Interesting application for a compiler. The other ...Interesting application for a compiler. The other approach would be to type a constant t as "t" and code that calculates t as "Code t". Less like modal logic, though.Ashley Yakeleyhttp://www.blogger.com/profile/00449875179637133204noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-71295841789513842702006-11-24T00:23:00.000-08:002006-11-24T00:23:00.000-08:00I've been playing around with the axioms to see if...I've been playing around with the axioms to see if either □ or ◊ behave like some well-known Haskell class.<br /><br />Firstly, neither of them are Functors, since you cannot prove either of these even in S5:<br /><br /> (a→b)→(□a→□b)<br /> (a→b)→(◊a→◊b)<br /><br />The second is less obvious than the first, but consider temporal logic: just because 'a' implies 'b' now, and 'a' is sometimes true, it doesn't mean that 'b' is ever true.<br /><br />This is unfortunate, since axioms T and 4 are suggestive of Monads for ◊:<br /><br /> T: a → ◊a<br /> 4: ◊◊a → ◊a<br /><br />K on the other hand doesn't look like anything I've seen in Haskell:<br /><br /> K: (◊a → ◊b) → ◊(a → b)Ashley Yakeleyhttp://www.blogger.com/profile/00449875179637133204noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-7753948840584229222006-11-23T19:24:00.000-08:002006-11-23T19:24:00.000-08:00ashley,
OK, I have some spare moments now. I've s...ashley,<br /><br />OK, I have some spare moments now. I've spent quite a bit of time tinkering round with various axioms of modal logic but as you notice, things have a habit of not quite working out the way you want. There *is* a nice interpretation of □ as something like C/C++'s 'const'. There's a bunch of papers about it and I said something about it <a href="http://sigfpe.blogspot.com/search?q=modal+compile+time">here</a>. I've also seen some papers that uses the axiom GL (ie. Loeb's theorem) as a basis for describnig recursive types.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-443847467385626232006-11-23T15:44:00.000-08:002006-11-23T15:44:00.000-08:00ashley,
As I say, I'm not sure there's a deep con...ashley,<br /><br />As I say, I'm not sure there's a deep connection with Loeb's theorem! (But there is surely <em>some</em> link.)sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-55514367247573312172006-11-23T14:56:00.000-08:002006-11-23T14:56:00.000-08:00Eeep! The defining property of a functor is this:
...Eeep! The defining property of a functor is this:<br /><br /> fmap :: (a -> b) -> f a -> f b<br /><br />and not<br /><br /> ap :: f (a -> b) -> f a -> f b<br /><br />fmap is definitely not provable in any modal logic.Ashley Yakeleyhttp://www.blogger.com/profile/00449875179637133204noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-46748320746030468872006-11-23T14:34:00.000-08:002006-11-23T14:34:00.000-08:00Modal logics usually have these rules:
&nbs...Modal logics usually have these rules:<br /><br /> f (a -> b) -> f a -> f b<br /><br />(This corresponds to the Applicative class, which may one day be made a superclass of Monad.)<br /><br /> f a -> a<br /><br />Monads do not in general satisfy this. Perhaps comonads or something?Ashley Yakeleyhttp://www.blogger.com/profile/00449875179637133204noreply@blogger.com