Combinatory weak reduction in lambda calculus. (English) Zbl 0902.68116
Summary: Combinatory logic claims to do the same work as \(\lambda\)-calculus but with a simpler language and a simpler reduction process. In a sense this claim is true: the classical reduction process in \(\lambda\)-calculus is indeed more complex than that in combinatory logic. But by changing its definition only slightly one can define in \(\lambda\)-calculus a perfect analogue of combinatory reduction. This analogue was first formulated 30 years ago but it is still not as well known as it deserves, so in the present purely expository paper we shall try to make it more accessible. We discuss its definition, motivation and its neat relation to substitution.
References:
| [1] | Akama, Y., A λ-to-CL translation for strong normalization, (de Groote, Ph.; Hindley, J. R., Typed Lambda Calculi and Applications, TLCA’97. Typed Lambda Calculi and Applications, TLCA’97, Lecture Notes in Computer Science, vol. 1210 (1997), Springer: Springer Berlin), 1-10 · Zbl 1063.03506 |
| [2] | Barendregt, H. P., The Lambda Calculus (1984), North-Holland: North-Holland Amsterdam · Zbl 0549.03012 |
| [3] | Çağman, N., Weak reduction in lambda calculus, (Dissertation (1996), Math. Department, University of Wales Swansea: Math. Department, University of Wales Swansea Swansea SA2 8PP, UK) · Zbl 0902.68116 |
| [4] | Hankin, C., Lambda Calculi, a Guide for Computer Scientists (1994), Oxford Univ. Press: Oxford Univ. Press Oxford · Zbl 0833.68070 |
| [5] | Hindley, J. R., Combinatory reductions and lambda reductions compared, Zeit. Math. Logik, 23, 169-180 (1977) · Zbl 0361.02035 |
| [6] | Hindley, J. R.; Seldin, J. P., Introduction to Combinators and λ-calculus (1986), Cambridge Univ. Press: Cambridge Univ. Press Cambridge · Zbl 0614.03014 |
| [7] | Howard, W. A., (Proc. confer.. Proc. confer., Buffalo, USA (1968)) · Zbl 0206.28202 |
| [8] | Hyland, J. M.E.; Ong, C.-H. L., Modified realizability toposes and strong normalization proofs, (Bezem, M.; Groote, J. F., Typed Lambda Calculi and Applications, TLCA’93. Typed Lambda Calculi and Applications, TLCA’93, Lecture Notes in Computer Science, vol. 664 (1993), Springer: Springer Berlin), 179-194 · Zbl 0793.03079 |
| [9] | Rosser, J. B., Duke Math. J., 1, 328-355 (1935), Part 2 · Zbl 0012.38601 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
