Perpetual reductions in \(\lambda\)-calculus. (English) Zbl 0920.03024
Summary: This paper surveys a part of the theory of \(\beta\)-reduction in \(\lambda\)-calculus which might aptly be called perpetual reductions. The theory is concerned with perpetual reduction strategies, i.e., reduction strategies that compute infinite reduction paths from \(\lambda\)-terms (when possible), and with perpetual redexes, i.e., redexes whose contraction in \(\lambda\)-terms preserves the possibility (when present) of infinite reduction paths. The survey not only recasts classical theorems in a unified setting, but also offers new results, proofs, and techniques, as well as a number of applications to problems in \(\lambda\)-calculus and type theory. \(\copyright\) Academic Press.
MSC:
| 03B40 | Combinatory logic and lambda calculus |
Keywords:
\(\beta\)-reduction; \(\lambda\)-calculus; perpetual reductions; perpetual redexes; infinite reduction paths; survey; type theorySoftware:
AutomathReferences:
| [1] | Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science (1992), Oxford Univ. Press: Oxford Univ. Press London · Zbl 0777.68001 |
| [2] | Barendregt, H. P., The Lambda Calculus: Its Syntax and Semantics (1984), North-Holland: North-Holland Amsterdam · Zbl 0551.03007 |
| [3] | Barendregt, H. P.; Bergstra, J.; Klop, J. W.; Voken, H., Technical Report Preprint (1976) |
| [4] | Barendregt, H. P.; Kennaway, J. R.; Klop, J. W.; Sleep, M. R., Needed reduction and spine strategies for the lambda calculus, Inform. and Comput., 75, 191-231 (1987) · Zbl 0635.03009 |
| [5] | Bergstra, J. A.; Klop, J. W., Church-Rosser strategies in the lambda calculus, Theoret. Comput. Sci., 9, 27-38 (1979) · Zbl 0404.03015 |
| [6] | Bergstra, J. A.; Klop, W., Strong normalization and perpetual reductions in the lambda calculus, J. Inform. Process. Cybernet., 18, 403-417 (1982) · Zbl 0523.03009 |
| [7] | Bezem, M.; Groote, J. F., Typed Lambda Calculus and Applications. Typed Lambda Calculus and Applications, Lecture Notes in Computer Science, 664 (1993), Springer-Verlag: Springer-Verlag Berlin/New York |
| [8] | Böhm, C.; Coppo, M.; Dezani-Ciancaglini, M., Termination tests inside \(λ, λ. λ\), Lecture Notes in Computer Science, 37 (1975), Springer-Verlag: Springer-Verlag Berlin/New York, p. 95-110 · Zbl 0358.02025 |
| [9] | Böhm, C.; Dezani-Ciancaglini, M., \(λ\), (Böhm, C., \(λ. λ\), Lecture Notes in Computer Science (1975), Springer-Verlag: Springer-Verlag Berlin/New York), 96-121 · Zbl 0358.02025 |
| [10] | Capretta, V. Valentini, S. A general method to prove the normalization theorem for first and second order typed \(λ\); Capretta, V. Valentini, S. A general method to prove the normalization theorem for first and second order typed \(λ\) · Zbl 0942.03017 |
| [11] | Church, A., The Calculi of Lambda-Conversion (1941), Princeton Univ. Press: Princeton Univ. Press Princeton · JFM 67.0041.01 |
| [12] | Church, A.; Rosser, J. B., Some properties of conversion, Trans. Amer. Math. Soc., 39, 11-21 (1936) · Zbl 0014.38504 |
| [13] | Curien, P.-L., Algèbre universelle, introduction au \(λ\), Technical Report (1995) |
| [14] | Curry, H. B.; Feys, R., Combinatory Logic (1958), North-Holland: North-Holland Amsterdam · Zbl 0175.27601 |
| [15] | Ghilezan, S., Application of typed lambda calculi in the untyped lambda calculus, (Nerode, A.; Matiyasevich, Yu. V., Symposium on Logical Foundations of Computer Science. Symposium on Logical Foundations of Computer Science, Lecture Notes in Computer Science, 813 (1994), Springer-Verlag: Springer-Verlag Berlin/New York), 129-139 · Zbl 0947.03021 |
| [16] | Girard, J.-Y., Interprétation fonctionelle et élimination des coupures dans l’arithmétique d’ordre supérieur (1972), Université Paris VII |
| [17] | Gramlich, B., Termination and Confluence Properties of Structured Rewrite Systems (1996), Fachbereich Informatik der Universität Kaiserslautern · Zbl 0872.68081 |
| [18] | Hindley, J. R., Reductions of residuals are finite, Trans. Amer. Math. Soc., 240, 345-361 (1978) · Zbl 0387.03007 |
| [19] | Hindley, J. R., BCK-combinators and linear \(λ\), Theoret. Comput. Sci., 64, 97-105 (1989) · Zbl 0671.03010 |
| [20] | Hindley, J. R.; Seldin, J. P., Introduction to Combinators and \(λ (1986)\), Cambridge Univ. Press: Cambridge Univ. Press London · Zbl 0614.03014 |
| [21] | Honsell, F.; Lenisa, M., Some results on the full abstraction problem for restricted lambda calculi, (Borzyszkowski, A. M.; Sokolowski, S., Symposium on Mathematical Foundations of Computer Science. Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, 711 (1993), Springer-Verlag: Springer-Verlag Berlin/New York), 84-104 · Zbl 0925.03095 |
| [22] | Howard, W., Ordinal analysis of terms of finite type, J. Symbolic Logic, 45, 493-504 (1980) · Zbl 0444.03029 |
| [23] | Huet, G. Lévy, J.-J. 1979, Call by need computations in non-ambiguous linear term rewriting systems, INRIA; Huet, G. Lévy, J.-J. 1979, Call by need computations in non-ambiguous linear term rewriting systems, INRIA |
| [24] | Hyland, J. M. E. 1973, A simple proof of the Church-Rosser theorem, Oxford University; Hyland, J. M. E. 1973, A simple proof of the Church-Rosser theorem, Oxford University |
| [25] | Karr, M., “Delayability” in proofs of strong normalizability in the typed lambda calculus, (Ehrig, H.; Floyd, C.; Nivat, M.; Tatcher, J., Mathematical Foundations of Computer Software. Mathematical Foundations of Computer Software, Lecture Notes in Computer Science, 185 (1985), Springer-Verlag: Springer-Verlag Berlin/New York), 208-222 · Zbl 0583.03007 |
| [26] | Kfoury, A. J.; Wells, J., Technical Report (1995) |
| [27] | Khasidashvili, Z., \(ββ\), (Martin-Löf, P.; Mints, G., International Conference on Computer Logic. International Conference on Computer Logic, Lecture Notes in Computer Science, 417 (1988), Springer-Verlag: Springer-Verlag Berlin/New York), 105-111 |
| [28] | Khasidashvili, Z., Form Reduction Systems and Reductions of Contracted Forms and Lambda-Terms (1988), Tbilisi State University |
| [29] | Khasidashvili, Z., Optimal normalization in orthogonal term rewriting systems, (Kirchner, C., Rewriting Techniques and Applications. Rewriting Techniques and Applications, Lecture Notes in Computer Science, 690 (1993), Springer-Verlag: Springer-Verlag Berlin/New York), 243-258 · Zbl 1508.68162 |
| [30] | Khasidashvili, Z., The longest perpetual reductions in orthogonal expression reduction systems, (Nerode, A.; Matiyasevich, Yu. V., Symposium on Logical Foundations of Computer Science. Symposium on Logical Foundations of Computer Science, Lecture Notes in Computer Science, 813 (1994), Springer-Verlag: Springer-Verlag Berlin/New York), 191-203 · Zbl 0964.03528 |
| [31] | Khasidashvili, Z., On higher order recursive program schemes, Colloquium on Trees in Algebra and Programming. Colloquium on Trees in Algebra and Programming, Lecture Notes in Computer Science, 787 (1994), Springer-Verlag: Springer-Verlag Berlin/New York, p. 172-186 · Zbl 0938.68643 |
| [32] | Khasidashvili, Z.; Glauert, J., Discrete normalization and standardization in deterministic residual structures, (Tison, S., Algebraic and Logic Programming. Algebraic and Logic Programming, Lecture Notes in Computer Science, 1139 (1996), Springer-Verlag: Springer-Verlag Berlin/New York), 135-149 · Zbl 1355.68139 |
| [33] | Khasidashvili, Z.; Ogawa, M., Perpetuality and uniform normalization, (Hanus, M.; Heering, J., Algebraic and Logic Programming (1997), Springer-Verlag: Springer-Verlag Berlin/New York), 240-255 · Zbl 0884.03010 |
| [34] | Klop, J. W., Combinatory Reduction Systems (1980), Utrecht University · Zbl 0466.03006 |
| [35] | Komori, Y., BCK-algebras and lambda calculus, Proceedings, 10th Symposium on Semigroups (1987), Josai University: Josai University Sakado, p. 5-11 |
| [36] | Krivine, J.-L., Lambda-Calculus, Types and Models. Lambda-Calculus, Types and Models, Ellis Horwood Series in Computers and Their Applications (1993), Masson and Ellis Horwood: Masson and Ellis Horwood Chichester · Zbl 0779.03005 |
| [37] | Lercher, B., Lambda-calculus terms that reduce to themselves, Notre Dame J. Formal Logic, XVII, 291-292 (1976) · Zbl 0324.02016 |
| [38] | Lévy, J.-J., Réductions corrects et optimales dans le lambda-calcul (1978), Université de Paris VII |
| [39] | Melliès, P.-A., Description Abstraite des Systèmes de Réécriture (1996), Université Paris VII |
| [40] | Mitschke, G., The standardization theorem in \(λ\), Z. Math. Logik Grundlag. Math., 25, 29-31 (1979) · Zbl 0442.03013 |
| [41] | Nederpelt, R., Strong Normalization for a Typed Lambda Calculus with Lamda Structured Types (1973) |
| [42] | Nederpelt, R.; Geuvers, J. H.; de Vrijer, R. C., Selected Papers on Automath (1994), Elsevier Science B.V: Elsevier Science B.V Amsterdam · Zbl 0822.03009 |
| [43] | van Oostrom, V., Confluence for Abstract and Higher-Order Rewriting (1994), Vrije Universiteit Amsterdam |
| [44] | van Oostrom, V., IR (1996) |
| [45] | van Oostrom, V., Finite family developments, (Comon, H., Rewriting Techniques and Applications. Rewriting Techniques and Applications, Lecture Notes in Computer Science, 1232 (1997), Springer-Verlag: Springer-Verlag Berlin/New York), 308-322 · Zbl 1379.68208 |
| [46] | van Oostrom, V.; van Raamsdonk, F., Comparing combinatory reduction systems and higher-order rewrite systems, (Heering, J.; Meinke, K.; Möller, B.; Nipkow, T., Higher Order Algebra, Logic and Term Rewriting. Higher Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science, 816 (1994), Springer-Verlag: Springer-Verlag Berlin/New York) |
| [47] | Parigot, M., Internal labellings in lambda-calculus, (Rovan, B., Symposium on Mathematical Foundations of Computer Science. Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, 452 (1990), Springer-Verlag: Springer-Verlag Berlin/New York), 439-445 · Zbl 0748.03013 |
| [48] | Plaisted, D. A., Polynomial time termination and constraint satisfaction tests, (Kirchner, C., Rewriting Techniques and Applications. Rewriting Techniques and Applications, Lecture Notes in Computer Science, 690 (1993), Springer-Verlag: Springer-Verlag Berlin/New York), 405-420 · Zbl 1503.68147 |
| [49] | van de Pol, J., Termination proofs for higher-order rewrite systems, (Heering, J., Higher Order Algebra, Logic and Term Rewriting. Higher Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science, 816 (1994), Springer-Verlag: Springer-Verlag Berlin/New York), 305-325 |
| [50] | van de Pol, J., Termination of Higher-Order Rewrite Systems (1996), University of Utrecht · Zbl 0864.68053 |
| [51] | van de Pol, J.; Schwichtenberg, H., Strict functionals for termination proofs, (Dezani-Ciancaglini, M.; Plotkin, G., Typed Lambda Calculus and Applications. Typed Lambda Calculus and Applications, Lecture Notes in Computer Science, 902 (1995), Berlin/New York), 350-364 · Zbl 1063.03505 |
| [52] | van Raamsdonk, F., Confluence and Normalisation for Higher-Order Rewriting (1996), Vrije Universiteit Amsterdam |
| [53] | van Raamsdonk, F.; Severi, P., Technical Report (1995) |
| [54] | Regnier, L., Une équivalence sur les lambda-termes, Theoret. Comput. Sci., 126, 281-292 (1994) · Zbl 0801.03013 |
| [55] | Schroer, D. E., The Church-Rosser Theorem (1965), Cornell University |
| [56] | Schwichtenberg, H., Complexity of normalization in the pure typed lambda-calculus, (Troelstra, A. S.; van Dalen, D., The L.E.J. Brouwer Centenary Symposium (1982), North-Holland: North-Holland Amsterdam), 453-457 · Zbl 0537.03028 |
| [57] | Schwichtenberg, H., An upper bound for reduction sequences in the typed lambda-calculus, Arch. Math. Logic, 30, 405-408 (1991) · Zbl 0719.03007 |
| [58] | Seldin, J. P.; Hindley, J. R., To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (1980), Academic Press: Academic Press New York · Zbl 0469.03006 |
| [59] | Severi, P., Normalisation in Lambda Calculus and Its relation to Type Inference (1996), Eindhoven University of Technology · Zbl 0844.03004 |
| [60] | Sørensen, M. H., Effective longest and infinite reduction paths in untyped \(λ\), (Kirchner, H., Colloquium on Trees in Algebra and Programming. Colloquium on Trees in Algebra and Programming, Lecture Notes in Computer Science, 1059 (1996), Springer-Verlag: Springer-Verlag Berlin/New York), 287-301 · Zbl 1508.03049 |
| [61] | Sørensen, M. H., Properties of infinite reduction paths in untyped \(λ\), (Ginzburg, J.; Khasidashvili, Z.; Lévy, J. J.; Vogel, E.; Vallduvı́, E., Proceedings, Tbilisi Symposium on Language, Logic, and Computation. Proceedings, Tbilisi Symposium on Language, Logic, and Computation, CLSI Lecture Notes (1996)) · Zbl 0956.03011 |
| [62] | Sørensen, M. H., Normalization in \(λ (1997)\), Department of Computer Science: Department of Computer Science University of Copenhagen |
| [63] | Sørensen, M. H., Strong normalization from weak normalization in typed \(λ\), Inform. and Comput., 133, 35-71 (1997) · Zbl 0878.03010 |
| [64] | Sørensen, M. H. 1998, A note on shortest developments; Sørensen, M. H. 1998, A note on shortest developments · Zbl 1131.68039 |
| [65] | Statman, R., Research Report (1991) |
| [66] | Tait, W. W., Intensional interpretations of functionals of finite type I, J. Symbolic Logic, 32, 190-212 (1967) · Zbl 0174.01202 |
| [67] | Takahashi, M., Parallel reductions in \(λ\), Inform. and Comput., 118, 120-127 (1995) · Zbl 0827.68060 |
| [68] | Terlouw, J., Reduction of higher type levels by means of an ordinal analysis of finite terms, Ann. Pure Appl. Logic, 28, 73-102 (1985) · Zbl 0554.03024 |
| [69] | Terlouw, J., Strong normalization in type systems: A model theoretical approach, Ann. Pure Appl. Logic, 73, 53-78 (1995) · Zbl 0818.03006 |
| [70] | Terlouw, J. Feb. 1998, A proof of strong normalization for generalized labeled \(β\); Terlouw, J. Feb. 1998, A proof of strong normalization for generalized labeled \(β\) |
| [71] | de Vrijer, R. C., A direct proof of the finite developments theorem, J. Symbolic Logic, 50, 339-343 (1985) · Zbl 0601.03001 |
| [72] | de Vrijer, R. C., Exactly estimating functionals and strong normalization, Koninklijke Nederlandse Akademie van Wetenschappen, 90 (1987) · Zbl 0642.03008 |
| [73] | de Vrijer, R. C., Exactly estimating functionals and strong normalization, Indag. Math., 49, 479-493 (1987) · Zbl 0642.03008 |
| [74] | de Vrijer, R. C., Surjective Pairing and Strong Normalization: Two Themes in Lambda Calculus (1987), University of Amsterdam |
| [75] | Xi, H., Research Report (1996) |
| [76] | Xi, H., Research Report (1996) |
| [77] | Xi, H. 1996, Separating developments; Xi, H. 1996, Separating developments |
| [78] | Xi, H., Upper bounds for standardization and an application, J. Symbolic Logic (1997) |
| [79] | Xi, H., Weak and strong beta normalisations in typed \(λ\), (de Groote, P.; Hindley, J. R., Typed Lambda Calculus and Applications. Typed Lambda Calculus and Applications, Lecture Notes in Computer Science, 1210 (1997), Springer-Verlag: Springer-Verlag Berlin/New York) · Zbl 1063.03528 |
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.
