Abstract
A reachability problem is a problem used to decide whether s is reachable to t by R or not for a given two terms s, t and a term rewriting system R. Since it is known that this problem is undecidable, effort has been devoted to finding subclasses of term rewriting systems in which the reachability is decidable. However few works on decidability exist for innermost reduction strategy or context-sensitive rewriting.
In this paper, we show that innermost reachability and contextsensitive reachability are decidable for linear right-shallow term rewriting systems. Our approach is based on the tree automata technique that is commonly used for analysis of reachability and its related properties.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Caron, A.-C., Coquide, J.-L., Dauchet, M.: Encompassment Properties and Automata with Constraints. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 328–342. Springer, Heidelberg (1993)
Comon, H.: Sequentiality, second-order monadic logic and tree automata. In: 10th annual IEEE symposium on logic in computer science (LICS 1995), pp. 508–517 (1995)
Durand, I., Sénizergues, G.: Bottom-Up Rewriting Is Inverse Recognizability Preserving. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 107–121. Springer, Heidelberg (2007)
Gilleron, R., Tison, S.: Regular tree languages and rewrite systems. Fundamenta Informaticae 24, 157–176 (1995)
Godoy, G., Huntingford, E.: Innermost-reachability and innermost-joinability are decidable for shallow term rewrite systems. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 184–199. Springer, Heidelberg (2007)
Jacquemard, F.: Decidable approximations of term rewriting systems. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 362–376. Springer, Heidelberg (1996)
Jacquemard, F.: Reachability and confluence are undecidable for flat term rewriting systems. Information processing letters 87(5), 265–270 (2003)
Lucas, S.: Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming 1998(1), 1–61 (1998)
Mitsuhashi, I., Oyamaguchi, M., Jacquemard, F.: The Confluence Problem for Flat TRSs. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS (LNAI), vol. 4120, pp. 68–81. Springer, Heidelberg (2006)
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)
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kojima, Y., Sakai, M. (2008). Innermost Reachability and Context Sensitive Reachability Properties Are Decidable for Linear Right-Shallow Term Rewriting Systems. In: Voronkov, A. (eds) Rewriting Techniques and Applications. RTA 2008. Lecture Notes in Computer Science, vol 5117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70590-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-70590-1_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70588-8
Online ISBN: 978-3-540-70590-1
eBook Packages: Computer ScienceComputer Science (R0)