Logical Methods pp 490-511 | Cite as

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

Chapter

- 2 Citations
- 157 Downloads

## 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.

## Keywords

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.

## Preview

Unable to display preview. Download preview PDF.

## References

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