General Case and Theory
A rewriting system can be expressed as a directed graph in which nodes represent expressions and edges represent rewrites. So, for example, if the expression can be rewritten into, then we say that is a reduct of (alternatively, reduces to, or is an expansion of ). This is represented using arrow notation; indicates that reduces to . Intuitively, this means that the corresponding graph has a directed edge from to .
If there is a path between two graph nodes (let's call them and ), then the intermediate nodes form a reduction sequence. So, for instance, if, then we can write, indicating the existence of a reduction sequence from to .
With this established, confluence can be defined as follows. Let a, b, c ∈ S, with a →* b and a →* c. a is deemed confluent if there exists a d ∈ S with b →* d and c →* d. If every a ∈ S is confluent, we say that → is confluent, or has the Church-Rosser property. This property is also sometimes called the diamond property, after the shape of the diagram shown on the right. Caution: other presentations reserve the term diamond property for a variant of the diagram with single reductions everywhere; that is, whenever a → b and a → c, there must exist a d such that b → d and c → d. The single-reduction variant is strictly stronger than the multi-reduction one.
Read more about this topic: Confluence (abstract Rewriting)
Famous quotes containing the words general, case and/or theory:
“Why not draft executive and management brains to prepare and produce the equipment the $21-a-month draftee must use and forget this dollar-a-year tommyrot? Would we send an army into the field under a dollar-a-year General who had to be home Mondays, Wednesdays and Fridays?”
—Lyndon Baines Johnson (1908–1973)
“While the light burning within may have been divine, the outer case of the lamp was assuredly cheap enough. Whitman was, from first to last, a boorish, awkward poseur.”
—Rebecca Harding Davis (1831–1910)
“If my theory of relativity is proven correct, Germany will claim me as a German and France will declare that I am a citizen of the world. Should my theory prove untrue, France will say that I am a German and Germany will declare that I am a Jew.”
—Albert Einstein (1879–1955)