Locally confluent rewriting system

From Groupprops
Jump to: navigation, search

Template:Rewriting system property


A rewriting system is said to be confluent if it satisfies the following condition: whenever u \longrightarrow v and u \longrightarrow w are one-step reductions in the rewriting system, then there exists a word z such that there exist multi-step reductions v \longrightarrow z and w \longrightarrow z.

In other words, any two things obtained by single-step reductions from the same source finally get together again.

Relation with other properties

Stronger properties