Remarks on the Church-Rosser Property
Lopez-Escobar, E. G. K.
J. Symbolic Logic, Tome 55 (1990) no. 1, p. 106-112 / Harvested from Project Euclid
A reduction algebra is defined as a set with a collection of partial unary functions (called reduction operators). Motivated by the lambda calculus, the Church-Rosser property is defined for a reduction algebra and a characterization is given for those reduction algebras satisfying CRP and having a measure respecting the reductions. The characterization is used to give (with 20/20 hindsight) a more direct proof of the strong normalization theorem for the impredicative second order intuitionistic propositional calculus.
Publié le : 1990-03-14
Classification: 
@article{1183743188,
     author = {Lopez-Escobar, E. G. K.},
     title = {Remarks on the Church-Rosser Property},
     journal = {J. Symbolic Logic},
     volume = {55},
     number = {1},
     year = {1990},
     pages = { 106-112},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183743188}
}
Lopez-Escobar, E. G. K. Remarks on the Church-Rosser Property. J. Symbolic Logic, Tome 55 (1990) no. 1, pp.  106-112. http://gdmltest.u-ga.fr/item/1183743188/