Partial Automata and Finitely Generated Congruences: An Extension of Nerode’s Theorem

  • D. Kozen
Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 12)


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.


Finite Index Finite Automaton Ground Term Tree Automaton Partial Algebra 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    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.MathSciNetCrossRefGoogle Scholar
  2. [2]
    Brainerd, W.S. [1967], Tree Generating Systems and Tree Automata. Ph.D. Thesis, Purdue University.Google Scholar
  3. [3]
    Brainerd, W.S. [1968], The minimalization of tree automata, Inf. and Control, 13, 484–491.MathSciNetzbMATHCrossRefGoogle Scholar
  4. [4]
    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.Google Scholar
  5. [5]
    Eilenberg, S. and J.B. Wright [1967], Automata in general algebra. Inf. and Control, 11, 452–470.MathSciNetzbMATHCrossRefGoogle Scholar
  6. [6]
    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.zbMATHGoogle Scholar
  7. [7]
    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.zbMATHGoogle Scholar
  8. [8]
    Grätzer, G. [1979], Universal Algebra. Springer-Verlag, second edition.Google Scholar
  9. [9]
    Hopcroft, J.E. and J.D. Ullman [1979], Introduction to Automata Theory, Languages, and Computation. Addison-Wesley.Google Scholar
  10. [10]
    Kozen, D. [1977], Complexity of finitely presented algebras. Ph.D. Thesis, Cornell University.Google Scholar
  11. [11]
    Kozen, D. [1977], Complexity of finitely presented algebras. Proc. 9th ACM Symp. Theory of Comput, 164–177.Google Scholar
  12. [12]
    Kozen, D. [1992], On the Myhill-Nerode Theorem for Trees. Bull. Amer. Theor. Comput. Sci, 47, 170–173.zbMATHGoogle Scholar
  13. [13]
    Myhill, J. [1957], Finite automata and the representation of events. WADC Tech. Rep. 57-264.Google Scholar
  14. [14]
    Nerode, A. [1958], Linear automata transformations. Proc. Amer. Math. Soc, 9, 541–544.MathSciNetzbMATHCrossRefGoogle Scholar
  15. [15]
    Nerode, A., A. Yakhnis and V. Yakhnis [1992], Concurrent programs as strategies in games. In Y. Moschovakis, editor, Logic from Computer Science. Springer-Verlag.Google Scholar
  16. [16]
    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.Google Scholar
  17. [17]
    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.MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media New York 1993

Authors and Affiliations

  • D. Kozen
    • 1
  1. 1.Computer Science DepartmentCornell UniversityIthacaUSA

Personalised recommendations