Confluence (abstract rewriting)

In computer science, confluence is a property of rewriting systems, describing which terms in such a system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system. The usual rules of elementary arithmetic form an abstract rewriting system. For example, the expression (11 + 9) × (2 + 4) can be evaluated starting either at the left or at the right parentheses; however, in both cases the same result is eventually obtained. If every arithmetic expression evaluates to the same result regardless of reduction strategy, the arithmetic rewriting system is said to be ground-confluent. Arithmetic rewriting systems may be confluent or only ground-confluent depending on details of the rewriting system. A second, more abstract example is obtained from the following proof of each group element equalling the inverse of its inverse: This proof starts from the given group axioms A1–A3, and establishes five propositions R4, R6, R10, R11, and R12, each of them using some earlier ones, and R12 being the main theorem. Some of the proofs require non-obvious, or even creative, steps, like applying axiom A2 in reverse, thereby rewriting "1" to "a−1 ⋅ a" in the first step of R6's proof. One of the historical motivations to develop the theory of term rewriting was to avoid the need for such steps, which are difficult to find by an inexperienced human, let alone by a computer program . If a term rewriting system is confluent and terminating, a straightforward method exists to prove equality between two expressions (also known as terms) s and t: Starting with s, apply equalities from left to right as long as possible, eventually obtaining a term s′. Obtain from t a term t′ in a similar way. If both terms s′ and t′ literally agree, then s and t are (not surprisingly) proven equal. More importantly, if they disagree, then s and t cannot be equal. That is, any two terms s and t that can be proven equal at all can be done so by that method.