chooseyourownlogic ([personal profile] chooseyourownlogic) wrote2012-11-04 09:44 am

Linear Permissions

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!

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

[personal profile] chrisamaphone 2012-11-05 05:39 pm (UTC)(link)
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.

[personal profile] chrisamaphone 2012-11-05 05:35 pm (UTC)(link)
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?

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

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

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