Confluence (abstract Rewriting) - General Case and Theory

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, cS, with a →* b and a →* c. a is deemed confluent if there exists a dS with b →* d and c →* d. If every aS 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 ab and ac, there must exist a d such that bd and cd. 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:

    All the critics who could not make their reputations by discovering you are hoping to make them by predicting hopefully your approaching impotence, failure and general drying up of natural juices. Not a one will wish you luck or hope that you will keep on writing unless you have political affiliations in which case these will rally around and speak of you and Homer, Balzac, Zola and Link Steffens.
    Ernest Hemingway (1899–1961)

    We all know the Navy is never wrong, but in this case it was a little weak on being right.
    Wendell Mayes, U.S. screenwriter. Otto Preminger. CINCPAC II (Henry Fonda)

    Lucretius
    Sings his great theory of natural origins and of wise conduct; Plato
    smiling carves dreams, bright cells
    Of incorruptible wax to hive the Greek honey.
    Robinson Jeffers (1887–1962)