An Abstract form of the church-rosser theorem. I
Roger Hindley · Journal of Symbolic Logic · 1969
One of the basic results in the theory of λ-conversion is the Church-Rosser Theorem, which says that, using certain rules for conversion and reduction of λ-formulae, any two interconvertible formulae can both be reduced to one formula. (I will not explain this in detail, as λ-conversion is described fully in Church's [2], where the Church-Rosser Theorem is Theorem 7 XXVII; see also Chapter 4 of Curry and Feys' [3].) The first part of the present paper contains an abstract form of this theorem.