On the Church-Rosser property and reducibility of natural derivations

Abstract

The paper contains a treatment of the Church-Rosser property with regard to several kinds of reductions. We give an example that the reducibility relation defined in [1] does not possess the property, although it is used to verify the uniqueness of the normal form and for stating the identity between proofs; we show a derivation that reduces to different normal ones. The property for this relation appears if we deny the restriction over commutative reductions to be applied only for maximal segments. The Church--Rosser property is a well-known fact for reducibility of derivations, and it might be expected that enlarging reducibility with commutative reductions will save the property. Here we illustrate that in that case the property is lost.