Partial Automata and Finitely Generated Congruences: An Extension of Nerode’s Theorem
Dexter C. Kozen · Birkhäuser Boston eBooks · 1993
Let T Σ , be the set of ground terms over a finite ranked alphabet Σ. We define partial automata on T Σ and prove that the finitely generated congruences on T Σ are in one-to-one correspondence (up to isomorphism) with the finite partial automata on T Σ with no inaccessible and no inessential states. We give an application in term rewriting: every ground term rewrite system has a canonical equivalent system that can be constructed in polynomial time. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.