||[Jan. 23rd, 2016|06:59 pm]
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])
◇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.