Remote Access Transactions of the American Mathematical Society
Green Open Access

Transactions of the American Mathematical Society

ISSN 1088-6850(online) ISSN 0002-9947(print)



Standard and normal reductions

Author: R. Hindley
Journal: Trans. Amer. Math. Soc. 241 (1978), 253-271
MSC: Primary 03B40
MathSciNet review: 492300
Full-text PDF

Abstract | References | Similar Articles | Additional Information

Abstract: Curry and Feys' original standardization proof for $ \lambda \beta $-reduction is analyzed and generalized to $ \lambda \beta \eta $-reductions with extra operators.

There seem to be two slightly different definitions of 'standard reduction' in current use, without any awareness that they are different; it is proved that although these definitions turn out to be equivalent for $ \lambda \beta $-reduction, they become different for $ \lambda \beta \eta $ and for reductions involving extra operators, for example the recursion operator.

Normal reductions are also studied, and it is shown that the basic normal-reduction theorem stays true when fairly simple operators like Church's $ \delta $ and Curry's iterator Z are added, but fails for more complicated ones like the recursion operator R.

Finally, a table is given summarizing the results, and showing how far the main theorems on $ \lambda \beta $-reductions extend to reductions with various extra operators.

References [Enhancements On Off] (What's this?)

  • [1] H. P. Barendregt, J. Bargstra, J. W. Klop and H. Volken, Degrees, reductions and representability in the lambda calculus, Math. Instituut, Budapestlaan 6, Utrecht, preprint 22, 1976. MR 0398760 (53:2611)
  • [2] A. Church and J. B. Rosser, Some properties of conversion, Trans. Amer. Math. Soc. 39 (1936), 472-482. MR 1501858
  • [3] H. B. Curry, A study of generalized standardization in combinatory logic, Lecture Notes in Math., vol. 500, Springer-Verlag, Berlin and New York, 1974, pp. 45-55. MR 0409128 (53:12890)
  • [4] H. B. Curry and R. Feys, Combinatory logic. I, North-Holland, Amsterdam, 1958. MR 20 #817. MR 0094298 (20:817)
  • [5] H. B. Curry, R. Hindley and J. P. Seldin, Combinatory logic. II, North-Holland, Amsterdam, 1972.
  • [6] R. Hindley, An abstract form of the Church-Rosser theorem. I, J. Symbolic Logic 34 (1969), 545-560. MR 0302434 (46:1578)
  • [7] -, An abstract Church-Rosser theorem. II, J. Symbolic Logic 39 (1974), 1-21. MR 0347558 (50:61)
  • [8] -, The equivalence of complete reductions, Trans. Amer. Math. Soc. 229 (1977), 227-248. MR 0444445 (56:2798)
  • [9] -, Reductions of residuals are finite, Trans. Amer. Math. Soc. 240 (1978), 345-361. MR 489603 (80a:03017)
  • [10] R. Hindley, B. Lercher and J. P. Seldin, Introduction to combinatory logic, Cambridge Univ. Press, London and New York, 1972. MR 49 #25. MR 0335242 (49:25)
  • [11] 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.
  • [12] G. Mitschke, The standardization theorem for the $ \lambda $-calculus, 1975, unpublished manuscript available from G. Mitschke, Fachbereich Mathematik, Technische Hochschule, Darmstadt, Federal Republic of Germany.
  • [13] R. P. Nederpelt, Strong normalization in a typed lambda-calculus with lambda-structured types, Doctoral thesis, 1973, Tech. Hogeschool, Eindhoven, The Netherlands.
  • [14] J. B. Rosser, A mathematical logic without variables, Ann. of Math. 36 (1935), 127-150. MR 1503213
  • [15] D. E. Schroer, The Church-Rosser theorem, Doctoral thesis, Cornell Univeristy, Ithaca, N. Y., 1965.

Similar Articles

Retrieve articles in Transactions of the American Mathematical Society with MSC: 03B40

Retrieve articles in all journals with MSC: 03B40

Additional Information

Keywords: Reduction, lambda-conversion, combinator, standard reduction, normal reduction, Gross reduction, delta-conversion, recursion combinator
Article copyright: © Copyright 1978 American Mathematical Society

American Mathematical Society