Abstract
We introduce a modular property of equational proofs, called modularity of normalization, for the union of term rewrite systems with shared symbols. The idea is, that every normalization with R=R 1+R 2 may be obtained by first normalizing with R 1 followed by an R 2 normalization.
We develop criteria for this that cover non-convergent TRS R, where, as the main restriction, R 1 is required to be left-linear and convergent. As interesting applications we consider solving equations modulo a theory given by a TRS. Here we present a modular narrowing strategy that can be combined with nearly all common narrowing strategies. Furthermore, we also prove some modularity results for decidability of unification and matching (via termination of narrowing).
Research supported by the DFG under grant Br 887/4-2, Deduktive Programmentwicklung and by ESPRIT WG 6028, CCL.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. Antoy, R. Echahed, and M. Hanus. A needed narrowing strategy. In Proc. 21st ACM Symposium on Principles of Programming Languages, pages 268–279, Portland, 1994.
L. Bachmair and N. Dershowitz. Commutation, transformation, and termination. In Joerg H. Siekmann, editor, Proc. 8th Int. Conf. Automated Deduction. LNCS 607, 1986.
A. Bockmayr. Narrowing with inductively defined functions. Technical report, Univ. Kaiserslautern, 1986. SEKI Memo 25/86.
Alexander Bockmayr, Stefan Krischer, and Andreas Werner. An optimal narrowing strategy for general canonical systems. In Michaël Rusinowitch and Jean-Luc Rémy, editors, Conditional Term Rewriting Systems, Third International Workshop, LNCS 656, pages 483–497, Pont-à-Mousson, France, July 8–10, 1992. Springer-Verlag.
P. G. Bosco, E. Giovanetti, and C. Moiso. Narrowing vs. SLD-resolution. Theoretical Computer Science, 59:3–23, 1988.
Jim Christian. Some termination criteria for narrowing and E-narrowing. In Kapur [14], pages 582–588.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Jan Van Leeuwen, editor, Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics, pages 243–320. Elsevier, 1990.
Nachum Dershowitz, Subrata Mitra, and G. Sivakumar. Decidable matching for convergent systems (preliminary version). In Kapur [14], pages 589–602.
A. Geser. Relative Termination. PhD thesis, Univ. Passau, 1990.
B. Gramlich. Generalized sufficient conditions for modular termination of rewriting. In H. Kirchner and G. Levi, editors, Algebraic and Logic Programming: Proc. of the Third International Conference, pages 53–68. Springer, Berlin, Heidelberg, 1992.
M. Hanus. The integration of functions into logic programming: A survey. 1994. To appear in Journal of Logic Programming.
M. Hanus. Lazy unification with simplification. In Proc. 5th European Symposium on Programming, pages 272–286. Springer LNCS 788, 1994.
Jean-Marie Hullot. Canonical forms and unification. In W. Bibel and R. Kowalski, editors, Proceedings of 5th Conference on Automated Deduction, pages 318–334. Springer Verlag, LNCS, 1980.
Deepak Kapur, editor. 11th International Conference on Automated Deduction, LNAI 607, Saratoga Springs, New York, USA, June 15–18, 1992. Springer-Verlag.
Aart Middeldorp. Modular aspects of properties of term rewriting systems related to normal forms. In Proc. 3rd Int. Conf. Rewriting Techniques and Applications, pages 263–277. LNCS 355, 1989.
Aart Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Free University Amsterdam, 1990.
Aart Middeldorp and Y. Toyama. Completeness of combinations of constructor systems. In Proc. 4th Int. Conf. Rewriting Techniques and Applications. LNCS 488, 1991.
T. Nipkow and G. Weikum. Operationelle Semantik axiomatisch spezifizierter Abstrakter Datentypen. Master's thesis, TH Darmstadt, 1982. In German.
W. Nutt and P. Réty and. Basic narrowing revisited. In C. Kirchner, editor, Unification. Academic Press, 1990.
M. R. K. Krisna Rao. Completeness of hierarchical combinations of term rewriting system. In R.K. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, pages 125–138. LNCS 761, 1993.
J. Raoult and J. Vuillemin. Operational and semantic equivalences between recursive Programms. J. of th ACM, 27:772–796, 1980.
U. S. Reddy. Narrowing as the operational semantics of functional languages. In Symposium on Logic Programming, pages 138–151. IEEE Computer Society, Technical Committee on Computer Languages, The Computer Society Press, July 1985.
K. Stroetmann. The union of rewrite systems. unpublished, 1992.
Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128–143, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Prehofer, C. (1994). On modularity in term rewriting and narrowing. In: Jouannaud, JP. (eds) Constraints in Computational Logics. CCL 1994. Lecture Notes in Computer Science, vol 845. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0016858
Download citation
DOI: https://doi.org/10.1007/BFb0016858
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58403-2
Online ISBN: 978-3-540-48699-2
eBook Packages: Springer Book Archive