Abstract
The different reachability problems for ground rewrite systems are decidable[OY86], [DEGI89]. We prove these results using ground tree transducers of [DATI85] and wellknown algorithms on recognizable tree languages in order to obtain efficient algorithms. We introduce and study derivation proofs to describe the sequences of rules used to reduce a term t in a term t' for a given ground rewrite system S and sketch how compute a derivation proof in linear time. Moreover, we study the same problem for recognizable tree languages.
This work was in part supported by the “PRC Mathématiques et Informatique” et ESPRIT2 Working Group ASMICS.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Bibliography
Brainerd, W.S, Tree generating regular systems, Inf. and control, 14 (1969), pp217–231.
Coquidé, J.L., Ph.D, Lille, to appear. (1990).
Courcelle, B.,On recognizable sets and tree automata, Resolution of Equations in Algebraic Structures, Academic Press, M.Nivat & H. Ait-Kaci edts, (1989).
Dauchet, M., Deruyver, A., "VALERIANN":Compilation of Ground Term Rewriting Systems and Applications, Rewriting Technics and Applications, (1989), Lec. Notes Comp. Sci., 355(Dershowitz ed.).
Dauchet, M., Heuillard, P., Lescanne, P., Tison, S., Decidability of the Confluence of Ground Term Rewriting Systems, 2nd Symposium on Logic in Computer Science, New-York, IEEE Computer Society Press (1987)
Dauchet, M., Tison, S., Decidability of Confluence in Ground Term Rewriting Systems, Fondations of Computation Theory, Cottbus, Lec. Notes Comp. Sci., 199, (1985)
Dauchet, M., Tison, S., The theory of Ground Rewrite System is Decidable, IEEE Symposium on Logic in Computer Science, to appear, (1990)
Deruyver, A., Gilleron, R., Compilation of Term Rewriting Systems, CAAP 89, Lec. Notes. Comp. Sci., (Diaz ed), 354, (1989)
Dershowitz, N., Jouannaud, J.P., Rewrite systems, Handbook of Theoretical Computer Science, J.V.Leeuwen editor, North-Holland, to appear.(1989).
Engelfriet, J., Bottom-up and Top-down Tree Transformations, a Comparison, Math. Systems Theory, 9, (1975)
Fülöp, Z., Vàgvölgyi, S., Ground Term Rewriting rules for the Word Problem of Ground Term Equations, submitted paper, (1989).
Gecseg, F., Steinby, M., Tree automata, Akademiai Kiado, (1984).
Gilleron, R., Ph.D, Lille, to appear (1990).
Huet, G., Oppen, D.C., Equations and Rewrite Rules: A survey, in R.V. Book, ed., New York, Academic Press, Formal Language Theory: Perspectives and Open Problems, (1980).
Nelson, G., Oppen, D.C., Fast Decision Procedures Based on Congruence Closure, JACM, 27, (1980).
Oyamaguchi, M., The reachability Problem for Quasi-ground Term Rewriting Systems, Journal of Information Processing, 9-4, (1986).
Tison, S., The Fair Termination is decidable for Ground Systems, Rewriting Technics and Applications, Chapel Hill, Lec. Notes Comp. Sci., 355 (Dershowitz ed.), (1989).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coquidé, J.L., Gilleron, R. (1990). Proofs and reachability problem for ground rewrite systems. In: Dassow, J., Kelemen, J. (eds) Aspects and Prospects of Theoretical Computer Science. IMYCS 1990. Lecture Notes in Computer Science, vol 464. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53414-8_34
Download citation
DOI: https://doi.org/10.1007/3-540-53414-8_34
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53414-3
Online ISBN: 978-3-540-46869-1
eBook Packages: Springer Book Archive