Tag Archives: Knuth-Bendix

Infinite lazy Knuth-Bendix completion for monoids in Haskell

The Knuth-Bendix completion procedure (when it succeeds) transforms a collection of equations into a confluent, terminating rewrite system. Sometimes the procedure fails, and sometimes does not terminate, but The Handbook of Computational Group Theory by D Holt remarked that even in this case it generates an infinite set of rewrite rules that are complete, and […]