An Abstract form of the church-rosser theorem. I
- 17 November 1969
- journal article
- abstracts
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 34 (4) , 545-560
- https://doi.org/10.1017/s0022481200128439
Abstract
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.Keywords
This publication has 1 reference indexed in Scilit:
- On Theories with a Combinatorial Definition of "Equivalence"Annals of Mathematics, 1942