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)



The equivalence of complete reductions

Author: R. Hindley
Journal: Trans. Amer. Math. Soc. 229 (1977), 227-248
MSC: Primary 02C20; Secondary 68A05
MathSciNet review: 0444445
Full-text PDF

Abstract | References | Similar Articles | Additional Information

Abstract: This paper is about two properties of the $ \lambda \beta $-calculus and combinatory reduction, namely (E): all complete reductions $ \rho $ and $ \sigma $ of the residuals of a set of redexes in a term X have the same end; and $ ({{\text{E}}^ + }):\rho $ and $ \sigma $ leave the same residuals of any other redex in X. Property (E) is deduced from abstract assumptions which do not imply $ ({{\text{E}}^ + })$. Also $ ({{\text{E}}^ + })$ is proved for the usual extensions of combinatory and $ \lambda \beta $-reduction, and a weak but natural form of $ ({{\text{E}}^ + })$ is proved for $ \lambda \beta \eta $-reduction.

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

  • [1] 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
  • [2] Alonzo Church, The Calculi of Lambda-Conversion, Annals of Mathematics Studies, no. 6, Princeton University Press, Princeton, N. J., 1941. MR 0005274
  • [3] R. Hindley, An abstract form of the Church-Rosser theorem. I, J. Symbolic Logic 34 (1969), 545–560. MR 0302434,
  • [4] R. Hindley, An abstract Church-Rosser theorem. II. Applications, J. Symbolic Logic 39 (1974), 1–21. MR 0347558,
  • [5] P. Martin-Löf, An intuitionistic theory of types, Univ. of Stockholm, 1972 (manuscript).
  • [6] P. Welch, Doctoral thesis, Univ. of Warwick, 1975.
  • [7] Barry K. Rosen, Tree-manipulating systems and Church-Rosser theorems, J. Assoc. Comput. Mach. 20 (1973), 160–187. MR 0331850,
  • [8] H. B. Curry, R. Hindley, J. P. Seldin, Combinatory logic, Vol. II, North-Holland, Amsterdam, 1972.
  • [9] J. H. Morris, Lambda-calculus models of programming languages, Ph. D. Thesis, Massachusetts Institute of Technology, Boston, 1968.
  • [10] H. P. Barendregt, J. Bergstra, J. W. Klop, H. Volken, Degrees, reductions, and representability in the lambda-calculus, Math. Inst., Univ. of Utrecht 22 (1976) (preprint).

Similar Articles

Retrieve articles in Transactions of the American Mathematical Society with MSC: 02C20, 68A05

Retrieve articles in all journals with MSC: 02C20, 68A05

Additional Information

Keywords: Reduction, residuals, relative reduction, development, lambda-calculus, combinators
Article copyright: © Copyright 1977 American Mathematical Society