tag:blogger.com,1999:blog-8068466035875589791.post5751026312479366908..comments2019-05-17T16:06:44.731-07:00Comments on Semantic Domain: Löb's theorem is (almost) the Y combinatorNeel Krishnaswamihttp://www.blogger.com/profile/06853898957395028131noreply@blogger.comBlogger7125tag:blogger.com,1999:blog-8068466035875589791.post-68214532278930170662016-05-25T01:08:11.863-07:002016-05-25T01:08:11.863-07:00Not written up, no, aside from a rough piece of pa...Not written up, no, aside from a rough piece of paper and a comment on this blog post at this point, it may fail to be sensible on closer examination. The idea is add assumptions of the form "a=A : type" to the modal context at the fold rule, and have them out of scope at first, but flowing to the non-modal context along with the term variables. I can write up the rules if that's not clear.Rowan Davieshttps://www.blogger.com/profile/02888491281001274822noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-344646559723911722016-05-24T03:42:01.949-07:002016-05-24T03:42:01.949-07:00Hi Rowan, have you written up how to handle modal ...Hi Rowan, have you written up how to handle modal type variables anywhere? It's not obvious to me what the right rules are....Neelakantan Krishnaswamihttps://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-39940217693909002142016-05-22T18:43:10.239-07:002016-05-22T18:43:10.239-07:00Hmmm. induction |-> coinduction (?!)Hmmm. induction |-> coinduction (?!)Rowan Davieshttps://www.blogger.com/profile/02888491281001274822noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-54038427258754322782016-05-21T10:21:19.260-07:002016-05-21T10:21:19.260-07:00Actually, this isn't more general, the more ge...Actually, this isn't more general, the more general version is where you introduce the recursive type variable in the modal context, hence it only becomes available once you pass to a reachable world via the box rule. You can do this with the original syntax of types, but the well-formedness judgement for types should check that the modal scoping is correct, hence including modal type assumptions that are copied to ordinary assumptions when you pass through a ◻ type constructor. It seems pretty natural to have such "modal type variables" in the context of a modal type system, but in S4 I guess they would be equivalent to the ordinary type variables.Rowan Davieshttps://www.blogger.com/profile/02888491281001274822noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-50550572965547540792016-05-20T20:21:18.916-07:002016-05-20T20:21:18.916-07:00Very nice! I wonder though if you can remove the ...Very nice! I wonder though if you can remove the explicit occurrences of ◻ in the fold/unfold rules to get more orthogonal rules by restricting the grammar of types to:<br /><br /> A ::= A→B | μt.A(t) | ◻T<br /> T ::= A | t<br /><br />To me, at least, this also seems to more directly capture a modal restriction on recursion. I think it's also at least slightly more general. I'd guess consistency can be shown by induction on the modal nesting of types.<br /> Rowan Davieshttps://www.blogger.com/profile/02888491281001274822noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-58747832666905645592016-05-12T02:52:24.442-07:002016-05-12T02:52:24.442-07:00I like this take on Lob's theorem. There was a...I like this take on Lob's theorem. There was a nice related paper at the 2015 Haskell Symposium: http://dl.acm.org/citation.cfm?doid=2804302.2804310 Dominic Orchardhttps://www.blogger.com/profile/00356502943141121461noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-25661871593545751662016-05-11T18:25:46.785-07:002016-05-11T18:25:46.785-07:00Neat! Is there a simple way to see that the modal ...Neat! Is there a simple way to see that the modal mu *is* consistent?jcreedhttps://www.blogger.com/profile/06587572078416238811noreply@blogger.com