| Linear Temporal Logic: https://www.cs.colostate.edu/~france/CS614/Slides/Ch5-Summar... (for Xφ, I prefer to define it as relative to a given frame: φ holds the next time any of the frame variables change, which allows both continuous<->discrete translation and for Lamport's stuttering [to allow abstraction!]) Next up: GC via creation and annihilation operators? (in my algebraic view of informatics, one is often either structuring by cleaving two parts to make a whole, or destructuring by cleaving a whole into two parts) EDIT: and by past-oriented I mean using "was ever" for "eventually" and in the past for "globally", as well as "since" for "until". rotate t by i^2. Eg dirty := F{edit} U ({save} ∨ {load})
says the local buffer differs from the cloud if there was ever an edit since a save or load.EDIT 2: ...and I'm pretty sure I can autogenerate code that turns these kinds of def'ns into an imperative event-driven state machine; one can of course come up in theory with formulae that require an arbitrarily complex implementation, but I think in practice most def'ns (especially if we provide backpressure by signalling the complexity of the resulting imp) would be satisfied with simple ones. |
Not sure when i’ll get there praying for a serendipitous intersection of cargoculting nonsssociativity and diagram spelunking (aided by your hints, half-remember’d)
Although… i confess to doing the trivial thing of drawing the “cayley graph” of {rock,paper,scissors} and observing that it looks like a loopfree 3-vertex term (1 outgoing)
https://en.wikipedia.com/wiki/Commutative_magma