[personal profile] chooseyourownlogic
I wrote an unfortunately long pdf about linear logic and comonads. It might be interesting? It might solve a long-standing problem? Or it might just be a good way for me to procrastinate on my homework---only one way to find out!

Date: 2012-11-05 05:32 pm (UTC)
From: [personal profile] chrisamaphone
i'm not able to prove cobind (as stated) with any of the box/! connectives you mentioned. what am i missing?

Date: 2012-11-05 05:39 pm (UTC)
From: [personal profile] chrisamaphone
yep - certainly if you make the ([]A -> B) argument be []'ed, it works, but i was curious why that doesn't correspond with the literature on comonads.

Date: 2012-11-05 05:35 pm (UTC)
From: [personal profile] chrisamaphone
i like the idea of having the "valid" and "true" judgments be represented by a 2-element preorder. it feels familiar, like something i've seen from jcreed.

i'm still not clear on how this constitutes a solution to permissions, though. what's your imagined encoding of "with permission p, a -o b"? does the permission become a worldy-resource?

Date: 2012-11-05 06:00 pm (UTC)
From: [personal profile] chrisamaphone
i don't see anything in your pdf with that ([p]) syntax?

Date: 2012-11-05 06:01 pm (UTC)
From: [personal profile] chrisamaphone
well, they're modal operators in the kripke semantics sense, not in the resource semantics sense -- they form a preorder, not a monoid :)

Date: 2012-11-05 06:02 pm (UTC)
From: [personal profile] chrisamaphone
"worldy", not "worldly" :) i just meant "resource semantics resource" as opposed to "linear logic resource".



April 2013

14151617 181920

Style Credit

Expand Cut Tags

No cut tags
Page generated Oct. 21st, 2017 03:09 am
Powered by Dreamwidth Studios