Hostname: page-component-78c5997874-s2hrs Total loading time: 0 Render date: 2024-11-12T22:29:35.732Z Has data issue: false hasContentIssue false
  • English
  • Français

An Abstract form of the church-rosser theorem. I

Published online by Cambridge University Press:  12 March 2014

R. Hindley
R. Hindley*
Affiliation:
University of Bristol
Rights & Permissions [Opens in a new window]

Extract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Abstracts
Information
The Journal of Symbolic Logic , Volume 34 , Issue 4 , February 1970 , pp. 545 - 560
Copyright
Copyright © Association for Symbolic Logic 1969

References

[1] Curry, H. B., A new proof of the Church-Rosser Theorem, Koninklijke Nederlandse Akademie van Wetenschappen. Proceedings. Series A, vol. 55 (1952), pp. 16–22.Google Scholar
[2] Church, A., The calculi of Lambda-conversion, Princeton Univ. Press, Princeton, N.J., 1941.Google Scholar
[3] Curry, H. B. and Feys, R., Combinatory logic, North-Holland, Amsterdam, 1958.Google Scholar
[4] Newman, M. H. A., On theories with a combinatorial definition of “equivalence”, Annals of mathematics, vol. 43 (1942), pp. 223–243.CrossRefGoogle Scholar
[5] Rosser, J. B., Review of “A new proof of the Church-Rosser theorem,” this Journal, vol. 21 (1956), p. 377.Google Scholar
[6] Schroer, D. E., The Church-Rosser theorem, Ph.D. thesis, University of Illinois, Urbana, Ill., 1965.Google Scholar