Standard and normal reductions
Author:
R. Hindley
Journal:
Trans. Amer. Math. Soc. 241 (1978), 253271
MSC:
Primary 03B40
MathSciNet review:
492300
Fulltext PDF Free Access
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 normalreduction 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]
Henk
Barendregt, The incompleteness theorems, Mathematisch
Instituut, Rijksuniversiteit Utrecht, 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; Communications of the Mathematical Institute,
Vol. 4. MR
0398760 (53 #2611)
 [2]
Alonzo
Church and J.
B. Rosser, Some properties of
conversion, Trans. Amer. Math. Soc.
39 (1936), no. 3,
472–482. MR
1501858, http://dx.doi.org/10.1090/S00029947193615018580
 [3]
Haskell
B. Curry, A study of generalized standardization in combinatory
logic, ⊨ISILC Proof Theory Symposion (Proc. Internat. Summer
Inst. and Logic Colloq., Kiel, 1974) Springer, Berlin, 1975,
pp. 44–55. Lecture Notes in Math., Vol. 500. MR 0409128
(53 #12890)
 [4]
Haskell
B. Curry and Robert
Feys, Combinatory logic. Vol. I, Studies in logic and the
foundations of mathematics, NorthHolland Publishing Co., Amsterdam, 1958.
MR
0094298 (20 #817)
 [5]
H. B. Curry, R. Hindley and J. P. Seldin, Combinatory logic. II, NorthHolland, Amsterdam, 1972.
 [6]
R.
Hindley, An abstract form of the ChurchRosser theorem. I, J.
Symbolic Logic 34 (1969), 545–560. MR 0302434
(46 #1578)
 [7]
R.
Hindley, An abstract ChurchRosser theorem. II. Applications,
J. Symbolic Logic 39 (1974), 1–21. MR 0347558
(50 #61)
 [8]
R.
Hindley, The equivalence of complete
reductions, Trans. Amer. Math. Soc. 229 (1977), 227–248. MR 0444445
(56 #2798), http://dx.doi.org/10.1090/S00029947197704444454
 [9]
R.
Hindley, Reductions of residuals are
finite, Trans. Amer. Math. Soc. 240 (1978), 345–361. MR 489603
(80a:03017), http://dx.doi.org/10.1090/S00029947197804896039
 [10]
J.
R. Hindley, B.
Lercher, and J.
P. Seldin, Introduction to combinatory logic, Cambridge
University Press, LondonNew York, 1972. London Mathematical Society
Lecture Notes, 7. MR 0335242
(49 #25)
 [11]
J. M. E. Hyland, A simple proof of the ChurchRosser theorem, unpublished manuscript available from J. Hyland, Math. Inst., 2429 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 lambdacalculus with lambdastructured types, Doctoral thesis, 1973, Tech. Hogeschool, Eindhoven, The Netherlands.
 [14]
J.
B. Rosser, A mathematical logic without variables. I, Ann. of
Math. (2) 36 (1935), no. 1, 127–150. MR
1503213, http://dx.doi.org/10.2307/1968669
 [15]
D. E. Schroer, The ChurchRosser theorem, Doctoral thesis, Cornell Univeristy, Ithaca, N. Y., 1965.
 [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), 472482. MR 1501858
 [3]
 H. B. Curry, A study of generalized standardization in combinatory logic, Lecture Notes in Math., vol. 500, SpringerVerlag, Berlin and New York, 1974, pp. 4555. MR 0409128 (53:12890)
 [4]
 H. B. Curry and R. Feys, Combinatory logic. I, NorthHolland, Amsterdam, 1958. MR 20 #817. MR 0094298 (20:817)
 [5]
 H. B. Curry, R. Hindley and J. P. Seldin, Combinatory logic. II, NorthHolland, Amsterdam, 1972.
 [6]
 R. Hindley, An abstract form of the ChurchRosser theorem. I, J. Symbolic Logic 34 (1969), 545560. MR 0302434 (46:1578)
 [7]
 , An abstract ChurchRosser theorem. II, J. Symbolic Logic 39 (1974), 121. MR 0347558 (50:61)
 [8]
 , The equivalence of complete reductions, Trans. Amer. Math. Soc. 229 (1977), 227248. MR 0444445 (56:2798)
 [9]
 , Reductions of residuals are finite, Trans. Amer. Math. Soc. 240 (1978), 345361. 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 ChurchRosser theorem, unpublished manuscript available from J. Hyland, Math. Inst., 2429 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 lambdacalculus with lambdastructured types, Doctoral thesis, 1973, Tech. Hogeschool, Eindhoven, The Netherlands.
 [14]
 J. B. Rosser, A mathematical logic without variables, Ann. of Math. 36 (1935), 127150. MR 1503213
 [15]
 D. E. Schroer, The ChurchRosser 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
DOI:
http://dx.doi.org/10.1090/S00029947197804923007
PII:
S 00029947(1978)04923007
Keywords:
Reduction,
lambdaconversion,
combinator,
standard reduction,
normal reduction,
Gross reduction,
deltaconversion,
recursion combinator
Article copyright:
© Copyright 1978
American Mathematical Society
