Abstract
In a recent paper we introduced a new framework for the study of call by need computations. Using elementary tree automata techniques and ground tree transducers we obtained simple decidability proofs for a hierarchy of classes of rewrite systems that are much larger than earlier classes defined using the complicated sequentiality concept. In this paper we study the modularity of membership in the new hierarchy. Surprisingly, it turns out that none of the classes in the hierarchy is preserved under signature extension. By imposing various conditions we recover the preservation under signature extension. By imposing some more conditions we are able to strengthen the signature extension results to modularity for disjoint and constructor-sharing combinations.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
H. Comon. Sequentiality, monadic second-order logic and tree automata. Information and Computation, 157:25–51, 2000.
N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279–301, 1982.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, volume B, pages 243–320. Elsevier, 1990.
I. Durand. Bounded, strongly sequential and forward-branching term rewriting systems. Journal of Symbolic Computation, 18:319–352, 1994.
I. Durand and A. Middeldorp. Decidable decidable call by need computations in term rewriting (extended abstract). In Proceedings of the 14th International Conference on Automated Deduction, volume 1249 of LNAI, pages 4–18, 1997.
I. Durand and A. Middeldorp. On the complexity of deciding call-by-need. Technical Report 1194-98, LaBRI, Université de Bordeaux I, 1998.
B. Gramlich. Termination and Confluence Properties of Structured Rewrite Systems. PhD thesis, Universität Kaiserslautern, 1996.
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 Proceedings of the 7th International Conference on Rewriting Techniques and Applications, volume 1103 of LNCS, pages 362–376, 1996.
R. Kennaway, J.W. Klop, R. Sleep, and F.-J. de Vries. Comparing curried and uncurried rewriting. Journal of Symbolic Computation, 21(1):15–39, 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.
A. Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Vrije Universiteit, Amsterdam, 1990.
T. Nagaya and Y. Toyama. Decidability for left-linear growing term rewriting systems. In Proceedings of the 10th International Conference on Rewriting Techniques and Applications, volume 1631 of LNCS, pages 256–270, 1999.
E. Ohlebusch. Modular Properties of Composable Term Rewriting Systems. PhD thesis, Universitat Bielefeld, 1994.
M. Oyamaguchi. NV-sequentiality: A decidable condition for call-by-need computations in term rewriting systems. SIAM Journal on Computation, 22:114–135, 1993.
R. Strandh. Classes of equational programs that compile into efficient machine code. In Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, volume 355 of LNCS, pages 449–461, 1989.
T. Takai, Y. Kaji, and H. Seki. Right-linear finite path overlapping term rewriting systems effectively preserve recognizability. In Proceedings of the 11th International Conference on Rewriting Techniques and Applications, volume 1833 of LNCS, pages 246–260, 2000.
Y. Toyama. Strong sequentiality of left-linear overlapping term rewriting systems. In Proceedings of the 7th IEEE Annual Symposium on Logic in Computer Science, pages 274–284, 1992.
Y. Toyama, S. Smetsers, M. van Eekelen, and R. Plasmeijer. The functional strategy and transitive term rewriting systems. In Term Graph Rewriting: Theory and Practice, pages 61–75. Wiley, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Durand, I., Middeldorp, A. (2001). On the Modularity of Deciding Call-by-Need. In: Honsell, F., Miculan, M. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2001. Lecture Notes in Computer Science, vol 2030. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45315-6_13
Download citation
DOI: https://doi.org/10.1007/3-540-45315-6_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41864-1
Online ISBN: 978-3-540-45315-4
eBook Packages: Springer Book Archive