Standard and normal reductions

Author:
R. Hindley

Journal:
Trans. Amer. Math. Soc. **241** (1978), 253-271

MSC:
Primary 03B40

DOI:
https://doi.org/10.1090/S0002-9947-1978-0492300-7

MathSciNet review:
492300

Full-text PDF

Abstract | References | Similar Articles | Additional Information

Abstract: Curry and Feys' original standardization proof for -reduction is analyzed and generalized to -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 -reduction, they become different for 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 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 -reductions extend to reductions with various extra operators.

**[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*-*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.

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

Retrieve articles in all journals with MSC: 03B40

Additional Information

DOI:
https://doi.org/10.1090/S0002-9947-1978-0492300-7

Keywords:
Reduction,
lambda-conversion,
combinator,
standard reduction,
normal reduction,
Gross reduction,
delta-conversion,
recursion combinator

Article copyright:
© Copyright 1978
American Mathematical Society