No CrossRef data available.
Article contents
Remarks on the Church-Rosser Property
Published online by Cambridge University Press: 12 March 2014
Abstract
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.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 1990