Abstract:An important theorem of the $\lambda \beta K$-calculus which has not been fully appreciated up to now is D. E. Schroer’s finiteness theorem (1963), which states that all reductions of residuals are finite. The present paper gives a new proof of this theorem and extends it from $\lambda \beta$-reduction to $\lambda \beta \eta$-reduction and reductions with certain extra operators added, for example the pairing, iteration and recursion operators. Combinatory weak reduction, with or without extra operators, is also included.
- Henk Barendregt, The incompleteness theorems, Communications of the Mathematical Institute, Rijksuniversiteit Utrecht, Vol. 4, Rijksuniversiteit Utrecht, Mathematisch Instituut, Utrecht, 1976. With appendices “Eliminating exponentiation”, “A Post system for arithmetic”, “Metamathematical assumptions for the incompleteness theorems” and “The Löb conditions” by J. W. Klop and A. Visser. MR 0398760
- Alonzo Church and J. B. Rosser, Some properties of conversion, Trans. Amer. Math. Soc. 39 (1936), no. 3, 472–482. MR 1501858, DOI 10.1090/S0002-9947-1936-1501858-0
- Haskell B. Curry, A study of generalized standardization in combinatory logic, $\vDash$ISILC Proof Theory Symposium (Proc. Internat. Summer Inst. and Logic Colloq., Kiel, 1974) Lecture Notes in Math., Vol. 500, Springer, Berlin, 1975, pp. 44–55. MR 0409128
- Haskell B. Curry and Robert Feys, Combinatory logic. Vol. I, Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Co., Amsterdam, 1958. MR 0094298 H. B. Curry, R. Hindley and J. P. Seldin, Combinatory logic. II, North-Holland, Amsterdam, 1972.
- R. Hindley, An abstract form of the Church-Rosser theorem. I, J. Symbolic Logic 34 (1969), 545–560. MR 302434, DOI 10.2307/2270849
- R. Hindley, An abstract Church-Rosser theorem. II. Applications, J. Symbolic Logic 39 (1974), 1–21. MR 347558, DOI 10.2307/2272337
- R. Hindley, The equivalence of complete reductions, Trans. Amer. Math. Soc. 229 (1977), 227–248. MR 444445, DOI 10.1090/S0002-9947-1977-0444445-4
- R. Hindley, Standard and normal reductions, Trans. Amer. Math. Soc. 241 (1978), 253–271. MR 492300, DOI 10.1090/S0002-9947-1978-0492300-7
- J. R. Hindley, B. Lercher, and J. P. Seldin, Introduction to combinatory logic, London Mathematical Society Lecture Notes Series, vol. 7, Cambridge University Press, London-New York, 1972. MR 0335242 J. M. E. Hyland, A simple proof of the Church-Rosser theorem, unpublished manuscript available from J. Hyland, Math. Inst., 24-29 St. Giles, Oxford, England. D. E. Schroer, The Church-Rosser theorem, Doctoral thesis, Cornell University, Ithaca, N. Y., 1965.
- © Copyright 1978 American Mathematical Society
- Journal: Trans. Amer. Math. Soc. 240 (1978), 345-361
- MSC: Primary 03B40
- DOI: https://doi.org/10.1090/S0002-9947-1978-0489603-9
- MathSciNet review: 489603