Hostname: page-component-745bb68f8f-5r2nc Total loading time: 0 Render date: 2025-02-11T15:41:22.729Z Has data issue: false hasContentIssue false
  • English
  • Français

Remarks on the Church-Rosser Property

Published online by Cambridge University Press:  12 March 2014

E. G. K. López-Escobar
E. G. K. López-Escobar*
Affiliation:
Department of Mathematics and Institute for Advanced Computer Studies, University of Maryland, College Park, Maryland 20742
Get access Rights & Permissions [Opens in a new window]

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
The Journal of Symbolic Logic , Volume 55 , Issue 1 , March 1990 , pp. 106 - 112
Copyright
Copyright © Association for Symbolic Logic 1990

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Barendregt, Hendrik, The lambda calculus. Its syntax and semantics, North-Holland, Amsterdam, 1984.Google Scholar
[2]de Bruijn, N. G., Lambda calculus notation with nameless dummies: a tool for automatic formula manipulation, with applications to the Church-Rosser theorem, Indagationes Mathematica, vol. 34 (1972), pp. 381–392.CrossRefGoogle Scholar
[3]Church, Alonzo and Rosser, Barkley, Some properties of conversion, Transactions of the American Mathematical Society, vol. 39 (1936), pp. 472–482.CrossRefGoogle Scholar
[4]Girard, J. Y., Une extension de I 'interpretation de Gödel à I 'analyse, et son application à l'èlimination de coupures dans l'analyse et la thèorie des types, Proceedings of the Second Scandinavian Logic Symposium, North-Holland, Amsterdam, 1971, pp. 63–92.CrossRefGoogle Scholar
[5]Prawitz, Dag, Natural deduction. A proof theoretical study, Almqvist and Wiksell, Uppsala, 1965.Google Scholar
[6]Prawitz, Dag, Ideas and results in proof theory, Proceedings of the Second Scandinavian Logic Symposium, North-Holland, Amsterdam, 1971, pp. 235–307.CrossRefGoogle Scholar
[7]Troelstra, A. S., Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin, 1973.CrossRefGoogle Scholar