Partial Automata and Finitely Generated Congruences: An Extension of Nerode’s Theorem
- 157 Downloads
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.
KeywordsFinite Index Finite Automaton Ground Term Tree Automaton Partial Algebra
Unable to display preview. Download preview PDF.
- Brainerd, W.S. , Tree Generating Systems and Tree Automata. Ph.D. Thesis, Purdue University.Google Scholar
- Dershowitz, N. and J.-P. Jouannaud , Rewrite Systems. In: J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, vol. B, 243–320. North-Holland, Amsterdam.Google Scholar
- Grätzer, G. , Universal Algebra. Springer-Verlag, second edition.Google Scholar
- Hopcroft, J.E. and J.D. Ullman , Introduction to Automata Theory, Languages, and Computation. Addison-Wesley.Google Scholar
- Kozen, D. , Complexity of finitely presented algebras. Ph.D. Thesis, Cornell University.Google Scholar
- Kozen, D. , Complexity of finitely presented algebras. Proc. 9th ACM Symp. Theory of Comput, 164–177.Google Scholar
- Myhill, J. , Finite automata and the representation of events. WADC Tech. Rep. 57-264.Google Scholar
- Nerode, A., A. Yakhnis and V. Yakhnis , Concurrent programs as strategies in games. In Y. Moschovakis, editor, Logic from Computer Science. Springer-Verlag.Google Scholar
- Snyder, W. , Fast ground completion: an O(n log n) algorithm for generating reduced sets of ground rewrite rules equivalent to a set of ground equations. In Nacham Dershowitz, editor, Proc. Third Int. Conf. Rewriting Techniques and Applications. Springer-Verlag Lect. Notes in Comput. Sci. 355, 419–433.Google Scholar