Abstract
We introduce the notion of abstract term rewriting system, R a, corresponding to a constructor-based term rewriting system R. R a is aimed to determine the set of possible constructors of a given term, using abstract rules in R a. A characterization of an abstract term rewriting system as a fixed point is given. Among the possible applications of the introduced concepts, we quote: E-unification, proofs by consistency, type checking etc.
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
Didier Bert and Rachid Echahed. Design and implementation of a generic, logic and functional programming language. Number 213 in Lecture Notes in Computer Science, pages 119–132. Springer-Verlag, 1986.
P.G. Bosco, E. Giovannetti, G. Levi, and C. Moiso, C.and Palamidessi. A complete semantic characterization of K-LEAF, a logic language with partial functions. In Proceedings of the 4th IEEE International Symposium on Logic Programming, pages 318–327, San Francisco, 1987.
Patrick Cousot and Radhia Cousot. Abstract interpretation and application to logic programs. Journal of Logic. Programming, 13(1, 2, 3 and 4):103–179, 1992. Also appeared as Technical Report LIENS-92-12, école normale supérieure, Paris.
Patrick Cousot and Radhia Cousot. Abstract interpretation frameworks. Technical Report LIX-RR-92-05, école polytecnique, 1992.
N. Dershowitz and J. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pages 243–320. North Holland, Amsterdam, 1990.
Nachum Dershowitz and 6. Sivakumar. Solving goals in equational languages. Number 308 in Lecture Notes in Computer Science, pages 45–55. Springer-Verlag, July 1987.
Harmut Ehrig and Bernd Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.
L. Fribourg. Slog: A logic programming language interpreter based on clausal superposition and rewriting. In Proc. IEEE International Symposium on Logic Programming, pages 172–184, Boston, 1985.
M. Hanus. Compiling logic programs with equality. In Proceedings of the 2nd International Workshop on Programming Language Implementation and Logic Programming, number 456 in Lecture Notes in Computer Science, pages 387–401. Springer-Verlag, 1990.
J.-M. Hullot. Canonical forms and unification. In Proc. 5th Conference on Automated Deduction, number 87 in Lecture Notes in Computer Science, pages 318–334. Springer-Verlag, 1980.
J. W. Klop. Term Rewriting Systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, Vol. II, pages 1–112. Oxford University Press, 1992. Previous version: Term rewriting systems, Technical Report CS-R9073, Stichting Mathematisch Centrum, Amsterdam, 1990.
J. J. Moreno-Navarro and M. Rodríguez-Artalejo. Logic programming with functions and predicates: The language BABEL. Journal of Logic Programming, 12:191–223, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bert, D., Echahed, R., Østvold, B.M. (1993). Abstract rewriting. In: Cousot, P., Falaschi, M., Filé, G., Rauzy, A. (eds) Static Analysis. WSA 1993. Lecture Notes in Computer Science, vol 724. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57264-3_39
Download citation
DOI: https://doi.org/10.1007/3-540-57264-3_39
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57264-0
Online ISBN: 978-3-540-48027-3
eBook Packages: Springer Book Archive