4 ms·
In some sense, whenever there's a choice (or a checkpoint) between two branches, each branch should morally get its own copy of the world; and effects should on
by Twisol 5y ago
In some sense, whenever there's a choice (or a checkpoint) between two branches, each branch should morally get its own copy of the world; and effects should only leak out when both branches incur the same observable effect. (This is motivated by the logical law `(A v B) ^ (A -> C) ^ (B -> C) -> C`.)
Of course, that's hard to do when interacting with external systems!
- maweki 5y agoDo you know of any work on this? I have a prototype implementation for a side-effects prolog library with a similar semantics and I'm working on the corresponding paper.
- Twisol 5y agoNot directly, no -- it's at least part of my own musings on logical systems. Probably the closest thing in my mind is Kuper et al.'s LVars, and I've long wanted to extend its join-semilattices to meets, but I left academia for a rather demanding day job ^_^; I do think consensus algorithms have something deeply in common here, as CALM (Consistency As Logical Monotonicity) seems to cover the space of join-semilattice structures pretty crisply, and CALM is all about when you don't need consensus. But again, just my own musings.