Jason (jcreed) wrote,
Jason
jcreed

Further grinding away on a token-passing definition of linear-time possibility, think I got it to a nice state. I appended my thoughts to http://jcreed.org/papers/buysell.pdf together with some discussion of what led me to need it in the first place. The tl;dr is that a definition as simple as
◇A = ∃x.[x] ⊗ □ (∀y ≥ x.[y] ⊸ A ∨ [○y])
indeed has
◇A, ◇B ⊢ ◇((A∧◇B)∨(◇A∧B))
except just saying that leaves out the meaning of most of the junk in the definition, so go read the pdf anyway.

I'm actually quite pleased at the near-systematicness of this conversion of corecursion into linear token passing, I'll have to think more about that.

At various times during this stretch of thinking I thought I had a use for the "fermionically true" modality that I mentioned on twitter a while back, but sadly it doesn't appear to be necessary after all.
Tags: math
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments