Abstract
Reachability and joinability are central properties of term rewriting. Unfortunately they are undecidable in general, and even for some restricted classes of term rewrite systems, like shallow term rewrite systems (where variables are only allowed to occur at depth 0 or 1 in the terms of the rules).
Innermost rewriting is one of the most studied and used strategies for rewriting, since it corresponds to the ”call by value” computation of programming languages. Henceforth, it is meaningful to study whether reachability and joinability are indeed decidable for a significant class of term rewrite systems with the use of the innermost strategy.
In this paper we show that reachability and joinability are decidable for shallow term rewrite systems assuming that the innermost strategy is used. All of these results are obtained via the definition of the concept of weak normal form, and a construction of a finite representation of all weak normal forms reachable from every constant. For the particular left-linear shallow case and assuming that the maximum arity of the signature is a constant, these results are obtained with polynomial time complexity.
The both authors were supported by Spanish Min. of Educ. and Science by the LogicTools project (TIN2004-03382). The second author was also supported by Spanish Min. of Educ. and Science by the GRAMMARS project (TIN2004-07925-C03-01).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (1997), Available on http://www.grappa.univ-lille3.fr/tata
Coquidé, J.L., Dauchet, M., Gilleron, R., Vágvölgyi, S.: Bottom-up tree pushdown automata: classification and connection with rewrite systems. Theoretical Computer Science 127, 69–98 (1994)
Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J.(ed.) Handbook of Theoretical Computer Science (Vol. B: Formal Models and Semantics), pp. 243–320, Amsterdam, North-Holland (1990)
Ganzinger, H., Jacquemard, F., Veanes, M.: Rigid reachability: The non-symmetric form of rigid E-unification. Intl. Journal of Foundations of Computer Science 11(1), 3–27 (2000)
Godoy, G., Tiwari, A.: Deciding fundamental properties of right-(ground or variable) rewrite systems by rewrite closure. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 91–106. Springer, Heidelberg (2004)
Godoy, G., Tiwari, A.: Termination of rewrite systems with shallow right-linear, collapsing, and right-ground rules. In: Nieuwenhuis, R. (ed.) Automated Deduction – CADE-20. LNCS (LNAI), vol. 3632, pp. 164–176. Springer, Heidelberg (2005)
Godoy, G., Tiwari, A., Verma, R.: On the confluence of linear shallow term rewrite systems. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 85–96. Springer, Heidelberg (2003)
Gyenizse, P., Vgvlgyi, S.: Linear generalized semi-monadic rewrite systems effectively preserve recognizability. Theoretical Computer Science 194, 87–122 (1998)
Jacquemard, F.: Reachability and confluence are undecidable for flat term rewriting systems. Inf. Process. Lett. 87(5), 265–270 (2003)
Nagaya, T., Toyama, Y.: Decidability for left-linear growing term rewriting systems. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 256–270. Springer, Heidelberg (1999)
Salomaa, K.: Deterministic tree pushdown automata and monadic tree rewriting systems. J. Comput. Syst. Sci. 37, 367–394 (1998)
Takai, T., Kaji, Y., Seki, H.: Right-linear finite path overlapping term rewriting systems effectively preserve recognizability. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 246–260. Springer, Heidelberg (2000)
Takai, T., Seki, H., Fujinaka, Y., Kaji, Y.: Layered transducing term rewriting system and its recognizability preserving property. IEICE Transactions on Information and Systems E86-D(2), 285–295 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Godoy, G., Huntingford, E. (2007). Innermost-Reachability and Innermost-Joinability Are Decidable for Shallow Term Rewrite Systems . In: Baader, F. (eds) Term Rewriting and Applications. RTA 2007. Lecture Notes in Computer Science, vol 4533. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73449-9_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-73449-9_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73447-5
Online ISBN: 978-3-540-73449-9
eBook Packages: Computer ScienceComputer Science (R0)