1 patch for repository http://darcs.net/screened:patch 9dfd9ea8480ced1f5bf88491c51d31b622bd6a43
Author: Ben Franksen <firstname.lastname@example.org>
Date: Fri Feb 15 12:20:12 CET 2019
* revert partitionRL to its former state, remove partitionRL'
This rolls back parts of patch 47da99770d4be412f7d9baed75eb0573a5b18d54
* clean up partitioning functions and export primed versions
The idea was to reduce the number of commutations. I am not sure it does
so in every case, though. And the new implementation is less conservative,
i.e. he result contains more commutation that necessary.
> Fair enough. I guess ideally we'd have tests for the properties
> we actually want from this function so we can refactor with
These functions are underspecified but only with respect to (structural)
patch equality. Since we regard sequences that differ only in the order
of patches (via commutation) as equal, they are not /semantically/
underspecified (I think). We could add tests that the functions respect
the specification but that would be of no use in this particular case as
the two versions of partitionRL are (I think) semantically equivalent.
The problem is that some of our theories (V1 and V2) are incorrect in
that the order in which patches in a sequence are commuted may influence
whether later commutations in the same sequence succeed or fail, which
means commutation can distinguish between semantically equal sequences.
The properties we "want" (rather: are enforced to require due to bugs in
our previous theories) are, I think, pretty hard to specify abstractly.
It's basically "this version works (mostly)" vs. "this one more often
leads to failures". Sad but true.