Confluent rewriting system: Difference between revisions
No edit summary |
No edit summary |
||
| (5 intermediate revisions by the same user not shown) | |||
| 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 condition: 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>. | ||
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. | ||
| Line 13: | Line 13: | ||
===Stronger properties=== | ===Stronger properties=== | ||
* [[Strongly confluent rewriting system]] | * [[Weaker than::Strongly confluent rewriting system]] | ||
* [[Complete rewriting system]] | * [[Weaker than::Complete rewriting system]] | ||
===Weaker properties=== | ===Weaker properties=== | ||
* [[Locally confluent rewriting system]] | * [[Stronger than::Locally confluent rewriting system]] | ||
==Metaproperties== | ==Metaproperties== | ||
{{reduction graph-based rsp}} | |||
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-closed rsp}} | {{free product-closed rsp}} | ||
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. | 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. | ||
Latest revision as of 22:06, 31 January 2012
Template:Rewriting system property
Definition
A rewriting system is said to be confluent if it satisfies the following condition: whenever and are multi-step reductions in the rewriting system, then there exists a word such that there exist multi-step reductions and .
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.