darcs

Patch 1810 revert partitionRL to its former state, remove partiti...

Title revert partitionRL to its former state, remove partiti...
Superseder Nosy List bf
Related Issues
Status accepted Assigned To
Milestone

Created on 2019-06-11.22:41:07 by bf, last changed 2019-06-14.17:40:30 by bf.

Files
File name Status Uploaded Type Edit Remove
patch-preview.txt bf, 2019-06-11.22:41:07 text/x-darcs-patch
revert-partitionrl-to-its-former-state_-remove-partitionrl_.dpatch bf, 2019-06-11.22:41:07 application/x-darcs-patch
unnamed bf, 2019-06-11.22:41:07 text/plain
See mailing list archives for discussion on individual patches.
Messages
msg20735 (view) Author: bf Date: 2019-06-11.22:41:07
1 patch for repository http://darcs.net/screened:

patch 9dfd9ea8480ced1f5bf88491c51d31b622bd6a43
Author: Ben Franksen <ben.franksen@online.de>
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.
Attachments
msg20782 (view) Author: ganesh Date: 2019-06-14.11:28:48
Fair enough. I guess ideally we'd have tests for the properties
we actually want from this function so we can refactor with
confidence.
msg20804 (view) Author: bf Date: 2019-06-14.17:40:30
> Fair enough. I guess ideally we'd have tests for the properties
> we actually want from this function so we can refactor with
> confidence.

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.
History
Date User Action Args
2019-06-11 22:41:07bfcreate
2019-06-12 12:35:06bfsetstatus: needs-screening -> needs-review
2019-06-14 11:28:48ganeshsetstatus: needs-review -> accepted-pending-tests
messages: + msg20782
2019-06-14 12:09:45ganeshsetstatus: accepted-pending-tests -> accepted
2019-06-14 17:40:30bfsetmessages: + msg20804