Abstract
In [PF-85] the concepts of fair derivations and fair-termination in term-rewriting systems were introduced and studied. In this paper, we define the notion of fairness in equational term-rewriting systems, where a derivation step is a composition of the equality generated by a (finite) set of equations with one step rewriting using a set of rules. A natural generalization of E-termination (termination of equational term-rewriting systems), namely E-fair-termination, is presented. We show that fair-termination and E-fair-termination are the same whenever the underlying rewriting relation is E-fully-commuting, a property inspired by Jouannaud and Munoz' E-commutation property. We obtain analogous results for combined term-rewriting systems.
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
L. Bachmair, N. Dershowitz: "Commutation, transformation and termination", 1985, (submitted).
L. Bachmair, D.A. Plaisted: "Associative path ordering", Proceedings of the First International Conference on Rewriting Techniques and Applications, Dijon, France, May 1985, (LNCS 202, J.P. Jouannaud-ed., Springer, Berlin).
G. Costa, C. Stirling: "Weak and strong fairness in CCS", Internal Report, CSR-167-85, University of Edinburgh, Jan. 1985.
N. Dershowitz: "Orderings for term rewriting systems", J. Theoretical Computer Science, Vol. 17, No. 3, March 1982, pp. 279–301 (previous version appeared in Proceedings of the Symposium on Foundations of Computer Science, San Juan, PR, pp. 123–131, Oct. 1979).
O. Grumberg, N. Francez, J.A. Makowsky, W.P. de Roever: "A proof rule for fair termination of guarded commands", Proceedings of the Int. Symp. on Algorithmic languages, Amsterdam, Oct. 1981, North-Holland.
J.P. Jouannaud, H. Kirchner: "Completion of a set of rules modulo a set of equations", 11th Ann. ACM Symp. on Principles of Programming Languages, Salt Lake City, Utah, January 1984, pp. 83–92.
J.P. Jouannaud, M. Munoz: "Termination of a set of rules modulo a set of equations", Proceedings of the 7th Intern. Conf. on Automated Deduction, Napa, CA. May 1984, pp. 175–193 (LNCS 170, R.E. Shostak-ed., Springer, Berlin).
D. Lehmann, A. Pnueli, J. Stavi: "Impartiality, justice and fairness: the ethics of concurrent termination", Proceedings 8th ICALP, Acre, Israel, LNCS 115 (O. Kariv, S. Even-eds.), Springer Verlag, 1981.
S. Porat: "Fairness in models for nondeterministic computations", Ph.D. Thesis, Computer Science Dept., Technion, Haifa, Israel, Jan. 1986.
S. Porat, N. Francez: "Fairness in term rewriting systems", Proceedings of the 1st Inter. Conf. on Rewriting Techniques and Applications, Dijon, France, May 1985 (LNCS 202, J.P. Jouannaud-ed., Springer, Berlin).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Porat, S., Francez, N. (1986). Full-commutation and fair-termination in equational (and combined) term-rewriting systems. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_77
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_77
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16780-8
Online ISBN: 978-3-540-39861-5
eBook Packages: Springer Book Archive