The equivalence of complete reductions
HTML articles powered by AMS MathViewer
- by R. Hindley PDF
- Trans. Amer. Math. Soc. 229 (1977), 227-248 Request permission
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
- 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
- Alonzo Church, The Calculi of Lambda-Conversion, Annals of Mathematics Studies, No. 6, Princeton University Press, Princeton, N. J., 1941. MR 0005274
- 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 P. Martin-Löf, An intuitionistic theory of types, Univ. of Stockholm, 1972 (manuscript). P. Welch, Doctoral thesis, Univ. of Warwick, 1975.
- Barry K. Rosen, Tree-manipulating systems and Church-Rosser theorems, J. Assoc. Comput. Mach. 20 (1973), 160–187. MR 331850, DOI 10.1145/321738.321750 H. B. Curry, R. Hindley, J. P. Seldin, Combinatory logic, Vol. II, North-Holland, Amsterdam, 1972. J. H. Morris, Lambda-calculus models of programming languages, Ph. D. Thesis, Massachusetts Institute of Technology, Boston, 1968. 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).
Additional Information
- © Copyright 1977 American Mathematical Society
- Journal: Trans. Amer. Math. Soc. 229 (1977), 227-248
- MSC: Primary 02C20; Secondary 68A05
- DOI: https://doi.org/10.1090/S0002-9947-1977-0444445-4
- MathSciNet review: 0444445