swift
2fc6ec55 - RequirementMachine: Use trie for left hand side simplification

Commit
4 years ago
RequirementMachine: Use trie for left hand side simplification In a confluent rewrite system, if the left hand side of a rule X => Y can be reduced by some other rule X' => Y', then it is permissible to delete the original rule X => Y altogether. Confluence means that rewrite rules can be applied in any order, so it is always valid to apply X' => Y' first, thus X => Y is obsolete. This was previously done in the completion procedure via a quadratic algorithm that attempted to reduce each existing rule via the newly-added rule obtained by resolving a critical pair. Instead, we can do this in the post-processing pass where we reduce right hand sides using a trie to speed up the lookup. This increases the amount of work performed by the completion procedure, but eliminates the quadratic algorithm, saving time overall.
Author
Committer
Parents
Loading