
Commutative Gröbner Bases 231
Definition 7.3.4.2 (Church–Rosser property). An ARS (A, →) is said to
have the Church–Rosser property if
∗
↔-equivalence implies joinability. That
is, the relation is Church–Rosser if for all f, g ∈ A we have
f
∗
↔ g =⇒ f ↓ g.
(The converse is trivial by definition of the relations.) In other words, if f and
g can be connected by a sequence of left-right arrows as in (7.3), then they
have a common successor h.
The importance of this property was first pointed out in the work of Church
and Rosser [59] on mathematical logic.
Definition 7.3.4.3 (Third definition of a Gröbner basis). Suppose that the
ideal I ⊆ F[X] is generated by the ...