Church-Rosser property

Let be a reductionPlanetmathPlanetmath (a binary relationMathworldPlanetmath) on a set S, and let * be the reflexiveMathworldPlanetmathPlanetmath transitiveMathworldPlanetmathPlanetmathPlanetmath symmetric closure of . The reduction is said to have the Church-Rosser propertyMathworldPlanetmath provided that a*b implies that a and b are joinable, for any a,bS.

In terms of diagrams, the Church-Rosser property means the following, for any a,bS, if


where uv means uv or uv (:=vu), then there is some xS such that


Remark. It can be shown that has the Church-Rosser property iff it is confluent.


  • 1 F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press (1998).
Title Church-Rosser property
Canonical name ChurchRosserProperty
Date of creation 2013-03-22 17:47:28
Last modified on 2013-03-22 17:47:28
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 9
Author CWoo (3771)
Entry type Definition
Classification msc 68Q42
Related topic Confluence