×

zbMATH — the first resource for mathematics

An axiomatic approach to the Korenjak-Hopcroft algorithms. (English) Zbl 0581.68032
Several equivalence decision algorithms for classes of grammars, program schemes, transducers follow the general pattern of the Korenjak-Hopcroft algorithm for deciding the equivalence of simple deterministic grammars. The author designs a unifying axiomatized framework for Korenjak-Hopcroft type algorithms. Applications are presented in which known algorithms are reformulated or proved in a different way. Also, a new result, the equivalence problem for \(\epsilon\)-limited deterministic top-down tree transductions of infinite trees, is given.
Reviewer: G.Slutzki

MSC:
68W99 Algorithms in computer science
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
68Q65 Abstract data types; algebraic specification
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] B. Courcelle. Une forme canonique pour les grammaires simples d√©terministes, RAIRO, R-1 (1974) pp. 19–36 · Zbl 0285.68033
[2] B. Courcelle. A representation of trees by languages.Theor. Computer Science 6 (1978) 225–279 and 7 (1978), 25–55 · Zbl 0377.68040
[3] B. Courcelle. Infinite trees in normal form and recursive equations having a unique solution.Math. Systems Theory 13 (1979), 131–180 · Zbl 0418.68013 · doi:10.1007/BF01744293
[4] B. Courcelle. Fundamental properties of infinite treesTheor. Computer Science 25 (1983) 95–169 · Zbl 0521.68013 · doi:10.1016/0304-3975(83)90059-2
[5] B. Courcelle, P. Franchi-Zannettacci. On the equivalence problem of attribute systems (To appear inInformation and Control) · Zbl 0529.68005
[6] B. Courcelle and J. Vuillemin. Completeness results for the equivalence of recursive schemas.J. Computer System Science 12 (1976), 179–197 · Zbl 0342.68008 · doi:10.1016/S0022-0000(76)80036-0
[7] K. Culik II and J. Pachl. Equivalence problem for mappings on infinite strings.Information and Control 49 (1981), 52–63 · Zbl 0472.68045 · doi:10.1016/S0019-9958(81)90444-7
[8] J. Darlington and R. Burstall. A system which automatically improves programs.Acta Informatica 6 (1976), 41–60 · Zbl 0323.68008 · doi:10.1007/BF00263742
[9] J. Engelfriet. Bottom-up and top-down tree transformations, a comparison.Math. Systems Theory 9 (1975), 198–231 · Zbl 0335.68061 · doi:10.1007/BF01704020
[10] J. Engelfriet. Top-down transducers with regular look-ahead.Math. Systems Theory 10 (1977) 289–303 · Zbl 0369.68048 · doi:10.1007/BF01683280
[11] Z. Ksik. On functional tree-transducers, Proceedings of 2nd Conference on Fundamentals of Computation Theory. L. Budach (ed.), East Berlin: Akademic-Verlag (1979) pp. 121–127
[12] E. Friedman. Equivalence problems for deterministic CFL and monadic recursion schemes.J. Computer System Science 14 (1977) 344–359 · Zbl 0358.68109 · doi:10.1016/S0022-0000(77)80019-6
[13] M. A. Harrison. Introduction to formal language theory. Addison-Wesley, 1978 · Zbl 0411.68058
[14] M. Harrison and I. Havel. Strict deterministic grammars.J. Computer System Science 7 (1973) 237–277 · Zbl 0261.68036 · doi:10.1016/S0022-0000(73)80008-X
[15] M. Harrison, I. Havel, and A. Yehudai. On equivalence of grammars through transformation trees,Theor. Computer Science 9 (1979) 173–205 · Zbl 0409.68041 · doi:10.1016/0304-3975(79)90024-0
[16] G. Huet, B. Lang. Proving and applying program transformations expressed with 2nd order patterns,Acta Informatica 11 (1978) 31–55 · Zbl 0389.68008 · doi:10.1007/BF00264598
[17] G. Huet. Confluent reductions: abstract properties and applications to term rewriting systems,J. Assoc. Comput. Mach. 27 (1980), 797–821. · Zbl 0458.68007
[18] A. Korenjak and J. Hopcroft. Simple deterministic languages. 7th IEEE Annual Symp. on Switching and Automata Theory, Berkeley, California (1966) 36–46 · Zbl 0313.68061
[19] M. Oyamaguchi, N. Honda, and Y. Inagaki. The equivalence problem for real-time strict deterministic languages,Information and Control 45 (1980) 90–115 · Zbl 0444.68038 · doi:10.1016/S0019-9958(80)90887-6
[20] Y. Olshansky and A. Pnueli. A direct algorithm for checking equivalence ofLL(k)-grammars,Theor. Computer Science 4 (1977) 321–349 · Zbl 0358.68118 · doi:10.1016/0304-3975(77)90016-0
[21] B. Rosen. Tree-manipulating systems and Church-Rosser theorems,J. Assoc. Comput. Mach. 20 (1973), 160–187 · Zbl 0267.68013
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.