Abstract
Huet and Lévy [6] showed that for the class of orthogonal term rewriting systems (TRSs) every term not in normal form contains a needed redex (i.e., a redex contracted in every normalizing rewrite sequence) and that repeated contraction of needed redexes results in a normal form if it exists. However, neededness is in general undecidable. In order to obtain a decidable approximation to neededness Huet and Lévy introduced the subclass of strongly sequential TRSs and showed that strong sequentiality is a decidable property of orthogonal TRSs.
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
H. Comon. Sequentiality, second-order monadic logic and tree automata. In Proc. 10 th LICS, pages 508–517, 1995.
H. Comon. Sequentiality, monadic second-order logic and tree automata. Information and Computation, 1999. Full version of [1].
I. Durand and A. Middeldorp. Decidable call by need computations in term rewriting (extended abstract). In Proc. 14th CADE, volume 1249 of LNAI, pages 4–18, 1997.
Irène Durand and Aart Middeldorp. On the complexity of deciding call-by-need. Technical Report 1196-98, LaBRI, 1998.
Iréne Durand and Aart Middeldorp. On the modularity of deciding call-by-need. In Foundations of Software Science and Computation Structures, volume 2030 of Lecture Notes in Computer Science, pages 199–213, Genova, 2001. Springer-Verlag.
G. Huet and J.-J. Lévy. Computations in orthogonal rewriting systems, i and ii. In Computational Logic, Essays in Honor of Alan Robinson, pages 396–443. The MIT Press, 1991. Original version: Report 359, Inria, 1979.
F. Jacquemard. Decidable approximations of term rewriting systems. In Proc. 7th RTA, volume 1103 of LNCS, pages 362–376, 1996.
J.W. Klop. Term rewriting systems. In Handbook of Logic in Computer Science, Vol. 2, pages 1–116. Oxford University Press, 1992.
J.W. Klop and A. Middeldorp. Sequentiality in orthogonal term rewriting systems. Journal of Symbolic Computation, 12:161–195, 1991.
Takashi Nagaya and Yoshihito Toyama. Decidability for left-linear growing term rewriting systems. In Proc. 10th RTA, volume 1631 of LNCS, 1999.
M. Oyamaguchi. NV-sequentiality: A decidable condition for call-by-need computations in term rewriting systems. SI AM Journal on Computation, 22:114–135, 1993.
Y. Toyama. Strong sequentiality of left-linear overlapping term rewriting systems. In Proc. 7th LICS, pages 274–284, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Durand, I. (2002). Autowrite: A Tool for Checking Properties of Term Rewriting Systems. In: Tison, S. (eds) Rewriting Techniques and Applications. RTA 2002. Lecture Notes in Computer Science, vol 2378. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45610-4_27
Download citation
DOI: https://doi.org/10.1007/3-540-45610-4_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43916-5
Online ISBN: 978-3-540-45610-0
eBook Packages: Springer Book Archive