Confluent rewriting system: Difference between revisions
m (6 revisions) |
No edit summary |
||
| Line 3: | Line 3: | ||
==Definition== | ==Definition== | ||
A [[rewriting system]] is said to be '''confluent''' if whenever <math>u \longrightarrow v</math> and <math>u \longrightarrow w</math> are multi-step reductions in the rewriting system, then there exists a word <math>z</math> such that there exist multi-step reductions <math>v \longrightarrow z</math> and <math>w \longrightarrow z</math>. | A [[rewriting system]] is said to be '''confluent''' if it satisfies the following two conditions: | ||
# '''Local confluence''' (see [[locally confluent rewriting system]]): whenever <math>u \longrightarrow v</math> and <math>u \longrightarrow w</math> are multi-step reductions in the rewriting system, then there exists a word <math>z</math> such that there exist multi-step reductions <math>v \longrightarrow z</math> and <math>w \longrightarrow z</math>. | |||
# '''Finite termination''' (see [[finitely terminating rewriting system]]): there is no infinite chain of rewrites that can be applied starting from any word, i.e., any chain of rewrites must terminate in finitely many steps. | |||
In other words, any two things from the same source finally get together again. | In other words, any two things from the same source finally get together again. | ||
Revision as of 21:55, 31 January 2012
Template:Rewriting system property
Definition
A rewriting system is said to be confluent if it satisfies the following two conditions:
- Local confluence (see locally confluent rewriting system): whenever and are multi-step reductions in the rewriting system, then there exists a word such that there exist multi-step reductions and .
- Finite termination (see finitely terminating rewriting system): there is no infinite chain of rewrites that can be applied starting from any word, i.e., any chain of rewrites must terminate in finitely many steps.
In other words, any two things from the same source finally get together again.
The term confluent rewriting system can also be used for a rewriting system for a group. Note that the free group rewriting system is confluent. A group that possesses a confluent rewriting system is termed a confluent group.
Relation with other properties
Stronger properties
Weaker properties
Metaproperties
Dependence only on reduction graph
This property of a rewriting system depends only on the reduction graph associated with the rewriting system, viz it can be reduces to testing the reduction graph for a directed graph property
Whether a rewriting system is confluent or not, can be reduced to checking a property of the associated reduction graph )assuming we remove the identity rewrite.
Free product-closedness
This property of a rewriting system is free product-closed. In other words, if we have two rewriting systems satisfying the property, the natural free product of these rewriting systems also satisfies the property
A free product of confluent rewriting systems is confluent. This is essentially because reductions in the various free factors do not interfere with one another, and hence commute.