Abstract
This chapter explains how to check whether a terminating specification is confluent, which ensures that the result of evaluating an expression is independent of the choice of which equation is applied to a term, and where the selected equation is applied.
This is a preview of subscription content, log in via an institution to check access.
Notes
- 1.
Formally, a renaming is a bijective substitution.
- 2.
The symbol \(\uplus \) denotes disjoint union, which means that \(f(t_1, \ldots , t_n){\mathop {=}\limits ^{?}} f(u_1, \ldots , u_n)\) does not appear in \( UP '\).
- 3.
Instead of checking joinability directly, one can find some normal forms of the two terms. If they have the same normal forms, they are obviously joinable; if not, the specification is obviously not confluent, since the “overlap term” \(l_i\rho \) has two different normal forms.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2017 Springer-Verlag London
About this chapter
Cite this chapter
Ölveczky, P.C. (2017). Confluence. In: Designing Reliable Distributed Systems. Undergraduate Topics in Computer Science. Springer, London. https://doi.org/10.1007/978-1-4471-6687-0_5
Download citation
DOI: https://doi.org/10.1007/978-1-4471-6687-0_5
Published:
Publisher Name: Springer, London
Print ISBN: 978-1-4471-6686-3
Online ISBN: 978-1-4471-6687-0
eBook Packages: Computer ScienceComputer Science (R0)