5 ms·
This idea has a history! The reason most language research programs like this had limited success is as follows. There are precious few programs for which a|b
by thwayunion 4y ago
This idea has a history! The reason most language research programs like this had limited success is as follows.
There are precious few programs for which a|b ~ a;b is true for all atomic programs a,b where:
| is a parallel composition operator
; is the normal sequential composition operator (defined in the completely standard way in terms of updates to a global state or heap/stack-like structure if you want to be fancy)
~ is any sort of equivalence relation on reasonable and realistic semantics.
More-over, there are precious few programs that easily decompose into parts A,B,... such that A|B ~ A;B is true for each A and B in the set of parts. You can give theoretic characterizations of this fact, and many have, but the pragmatic point is more convincing.
Associativity and even reflexivity often fail as well.
The allure of this line of thought is promising, but alas... The "just make a simple algebra and arrange your programs to fit it" research program died early on for a reason. In the context of parallel and concurrent programs, it is hard/impossible to solve the decomposition problem at the language level of abstraction.
That pretty much summarizes outcome of a big chunk of program analysis research from the 70s to early 90s in a nutshell, unfortunately.
Let me briefly illustrate using OP's example:
`a' = b + 1; b' = a + 1`
from which I've deleted the errant training semicolon (it's `1+1` not `1+1+`!)
Suppose we instead have the program:
a' = a + b + 1; b' = a + b + 1
Now, the ordering does matter! No worries, so we order.
Additionally, suppose we put these programs into an outer while(true) loop and that's our whole program. Now what have we bought ourselves? Not much.
In this case we can solve that problem by... well, by solving some sort of integer recurrence equations that give us a program without loops which we can then think about algebraically. But of course this gets difficult or impossible very fast. (And, btw, the algebra part here did not buy us much. It was solving integer recurrence equations that saved the idea in this example). We haven't even added real data structures or external state yet.
Anyways, looks like OP is building something around this idea. Good luck! I'll be curious to see how you handle loops inside of blocks that contain @'d variables with recursively defined quantities :)
- oh_my_goodness 4y agoI don't think the ordering matters. In both a' = a + b + 1 and b' = a + b + 1 the new values are on the left and the old values are on the right.
- thwayunion 4y agoSorry, I edited a bunch and the point was that the ordering can matter due to references to the new value on the rhs or due to a loop. So a' = a + b + 1 and b' = a + b + 1 should be a' = a + b' + 1 and b' = a' + b + 1 Or alternatively they can have non-primed right hand sides but occur in a loop and you have the same problem even though the rhs's are at-free. A syntactic constraint won't work unless it includes "and also no loops in at-mentioning blocks" which... well, yeah, we know how to reason about NFAs :) Sorry again, trying to make too many points with a single example
- woutervdb 4y agoCould you not tackle this problem by not allowing this mingling of 'next' and 'current' variables? You would only allow a next variable to be a computation of current variables. Not sure to what extent this would limit the application of the paradigm, though.
- aappleby 4y agoAuthor here, you are both correct and not correct - in your example the two equations represent an impossible constraint (there's an evaluation loop), thus a program (or TLA proof) containing those two statements would be invalid.
- thwayunion 4y agoRight. That’s what I meant by imposing synaptic constraints getting you back to well trodden ground.
- aappleby 4y agoAuthor here. "Now what have we bought ourselves? Not much." Well of course I disagree with that statement. My work on Metron suggests that we've bought ourselves a way to write programs that can execute on both CPUs and FPGAs, which is a valuable thing. The ability to more directly translate the behavior of our programs into a proof framework like TLA is also quite useful, and I think folks who are deep into functional programming also like the lack of "side effects" since the process of computing x' is guaranteed not to change x (or any other observable property of the previous program state).