Reductions of residuals are finite

Hindley, R.

doi:10.1090/S0002-9947-1978-0489603-9

Reductions of residuals are finite
HTML articles powered by AMS MathViewer

by R. Hindley PDF

Trans. Amer. Math. Soc. 240 (1978), 345-361 Request permission

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.

References

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

Combinatory logic

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

A simple proof of the Church-Rosser theorem

The Church-Rosser theorem