Relating confluence, innermost-confluence and outermost-confluence properties of term rewriting systems
Tóm tắt
Innermost-confluence is important in giving call-by-value and denotational semantics and outermost-confluence is important in giving call-by-need and lazy semantics of programs. In this paper, we give a few sets of sufficient conditions under which the properties of confluence, innermost-confluence and outermost-confluence coincide. Confluence and innermost-confluence coincide for weakly innermost normalizing overlay systems and confluence and outermost-confluence coincide for outermost normalizing left-linear overlay systems. In general, every weakly innermost (outermost) normalizingconfluent system isinnermost (outermost) confluent but the converse is not true.
Tài liệu tham khảo
N. Dershowitz, J.-P. Jouannaud (1990): Rewrite systems. In: J. van Leeuwen (ed.) Handbook of Theoretical Computer Science, Vol. B, pp. 243–320, North-Holland
B. Gramlich (1992): Relating innermost, weak, uniform and modular termination of term rewrite systems. Proc. of Logic Prog. and Automated Reasoning. LPAR’92 (Lecture Notes in Computer Science 624, pp. 285–296) Springer-Verlag. Revised version to appear in a special issue of Fundamenta Informaticae on term rewrite systems
J.W. Klop (1992): Term rewriting systems. In: S. Abramsky, D. Gabbay, T. Maibaum (eds.) Handbook of Logic in Computer Science, Vol. 2. Oxford University Press
M.J. O’Donnell (1977): Computing in systems described by equations. Lecture Notes in computer Science, Vol. 58. Springer-Verlag
D.A. Plaisted (1993): Equational reasoning and term rewriting systems. In: S. Abramsky, D. Gabbay, T. Maibaum (eds.) Handbook of logic in artificial intelligence and logic programming, Vol. 1. Oxford University Press
J. Staples (1975): Church-Rosser Theorems for Replacement Systems. In: J. Crosley (ed.) Algebra and Logic. (Lecture Notes in Mathematics, Vol 450, pp. 291–307) Springer-Verlag