January 23rd, 2016

beartato phd

(no subject)

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.