Slava Pestov fee97ea96a RequirementMachine: Fix the most embarassing bug of all time ...

The implementation of Knuth-Bendix completion has had a subtle
bookkeeping bug since I first wrote the code in 2021.

It is possible for two rules to overlap in more than one position,
but the ResolvedOverlaps set was a set of pairs (i, j), where
i and j are the index of the two rules. So overlaps other than
the first were not considered. Fix this by changing ResolvedOverlaps
to a set of triples (i, j, k), where k is the position in the
left-hand side of the first rule.

The end result is that we would incorrectly accept the protocol M3
shown in the test case. I'm pretty sure the monoid that M3 encodes
does not have a complete presentation over any alphabet, so of
course it should not be accepted here.

2025-06-17 17:51:26 -04:00

15 KiB

Raw Permalink Blame History

View Raw