Strongly confluent rewriting system

Definition

Symbol-free definition

A rewriting system is said to be strongly confluent if it satisfies the following two conditions:

1. It is a locally strongly confluent rewriting system: Whenever $u\to v$ and $u\to w$ are (one-step) reductions, then there is a $z$ and one-step reductions $v\to z$ and $w\to z$.
2. It is a finitely terminating rewriting system: Any chain of reductions must terminate in finitely many steps.

An alternative way of saying that a rewriting system is strongly confluent is that it has the Church-Rosser property.

Relation with other properties

Weaker properties

• Confluent rewriting system is the corresponding property for multi-step reductions. The fact that any strongly confluent rewriting system is confluent has a neat diagrammatic proof which involves completion of squares.