Abstract
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.
Research supported in part by the Danish Research Academy, the National Science Foundation, the John Simon Guggenheim Foundation, and the U.S. Army Research Office through the ACSyAM branch of the Mathematical Sciences Institute of Cornell University, contract DAAL03-91-C-0027.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Arbib, M.A. and Y. Give’on [1968], Algebra automata I: parallel programming as a prolegomena to the categorical approach. Inf. and Control, 12, 331–345.
Brainerd, W.S. [1967], Tree Generating Systems and Tree Automata. Ph.D. Thesis, Purdue University.
Brainerd, W.S. [1968], The minimalization of tree automata, Inf. and Control, 13, 484–491.
Dershowitz, N. and J.-P. Jouannaud [1990], Rewrite Systems. In: J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, vol. B, 243–320. North-Holland, Amsterdam.
Eilenberg, S. and J.B. Wright [1967], Automata in general algebra. Inf. and Control, 11, 452–470.
Fülöp, Z. and S. Vágvölgyi [1989], Congruential tree languages are the same as recognizable tree languages — a proof for a theorem of D. Kozen. Bull. Eur. Assoc. Theor. Comput. Sci, 39, 175–184.
Fülöp, Z. and S. Vágvölgyi [1991], Ground term rewriting rules for the word problem of ground term equations. Bull. Europ. Assoc. Theor. Comput. Sci, 45, 186–201.
Grätzer, G. [1979], Universal Algebra. Springer-Verlag, second edition.
Hopcroft, J.E. and J.D. Ullman [1979], Introduction to Automata Theory, Languages, and Computation. Addison-Wesley.
Kozen, D. [1977], Complexity of finitely presented algebras. Ph.D. Thesis, Cornell University.
Kozen, D. [1977], Complexity of finitely presented algebras. Proc. 9th ACM Symp. Theory of Comput, 164–177.
Kozen, D. [1992], On the Myhill-Nerode Theorem for Trees. Bull. Amer. Theor. Comput. Sci, 47, 170–173.
Myhill, J. [1957], Finite automata and the representation of events. WADC Tech. Rep. 57-264.
Nerode, A. [1958], Linear automata transformations. Proc. Amer. Math. Soc, 9, 541–544.
Nerode, A., A. Yakhnis and V. Yakhnis [1992], Concurrent programs as strategies in games. In Y. Moschovakis, editor, Logic from Computer Science. Springer-Verlag.
Snyder, W. [1989], 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.
Thatcher, J.W. and J.B. Wright [1968], Generalized finite automata theory with an application to a decision problem of second order logic. Math. Syst. Theory, 2, 57–81.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer Science+Business Media New York
About this chapter
Cite this chapter
Kozen, D. (1993). Partial Automata and Finitely Generated Congruences: An Extension of Nerode’s Theorem. In: Crossley, J.N., Remmel, J.B., Shore, R.A., Sweedler, M.E. (eds) Logical Methods. Progress in Computer Science and Applied Logic, vol 12. Birkhäuser, Boston, MA. https://doi.org/10.1007/978-1-4612-0325-4_16
Download citation
DOI: https://doi.org/10.1007/978-1-4612-0325-4_16
Publisher Name: Birkhäuser, Boston, MA
Print ISBN: 978-1-4612-6708-9
Online ISBN: 978-1-4612-0325-4
eBook Packages: Springer Book Archive