Combining algebraic rewriting, extensional lambda calculi, and fixpoints. (English) Zbl 0874.68158

Summary: It is well known that confluence and strong normalization are preserved when combining algebraic rewriting systems with the simply typed lambda calculus. It is equally well known that confluence fails when adding either the usual contraction rule for \(\eta\) , or recursion together with the usual contraction rule for surjective pairing. We show that confluence and strong normalization are modular properties for the combination of algebraic rewriting systems with typed lambda calculi enriched with expansive extensional rules for \(\eta\) and surjective pairing. We also show how to preserve confluence in a modular way when adding fixpoints to different rewriting systems. This result is also obtained by a simple translation technique allowing to simulate bounded recursion.


68Q42 Grammars and rewriting systems
Full Text: DOI


[1] Akama, Y, On mints’ reductions for ccc-calculus, (), 1-12 · Zbl 0786.03006
[2] Barendregt, H, The lambda calculus; its syntax and semantics, (1984), North-Holland Amsterdam · Zbl 0551.03007
[3] Breazu-Tannen, V, Combining algebra and higher order types, (), 82-90
[4] Breazu-Tannen, V; Gallier, J, Polymorphic rewriting preserves algebraic strong normalization, Theoret. comput. sci., 83, 3-28, (1991) · Zbl 0745.68065
[5] Breazu-Tannen, V; Gallier, J, Polymorphic rewriting preserves algebraic confluence, Inform. comput., 114, 1-24, (1994) · Zbl 0820.68059
[6] Curien, P.-L; Di Cosmo, R, A confluent reduction system for the λ-calculus with surjective pairing and terminal object, (), 291-302 · Zbl 0769.68056
[7] Cubric, D, On free CCC, distributed on the types mailing List, (1992)
[8] Dershowitz, Na; Jouannaud, J.-P, Rewrite systems, (), 243-320, Ch. 6 · Zbl 0900.68283
[9] Di Cosmo, R; Kesner, D, Combining first order algebraic rewriting systems, recursion and extensional lambda calculi, (), 462-472 · Zbl 1418.68112
[10] Di Cosmo, R; Kesner, D, Simulating expansions without expansions, Math. struct. comput. sci., 4, 1-48, (1994) · Zbl 0831.03004
[11] A preliminary version is available as Tech. Report LIENS-93-11/INRIA 1911.
[12] Dougherty, D.J, Some lambda calculi with categorical sums and products, ()
[13] Howard, B; Mitchell, J, Operational and axiomatic semantics of pcf, (), 298-306
[14] Jay, C.B; Ghani, N, The virtues of eta-expansion, (), preliminary version of [14]. · Zbl 0833.68072
[15] Jay, C.B; Ghani, N, The virtues of eta-expansion, J. functional programming, 5, 135-154, (1995) · Zbl 0833.68072
[16] Jouannaud, J.-P; Okada, M, A computation model for executable higher-order algebraic specification languages, (), 350-361
[17] Kamareddine, F; Ríos, Alejandro, The confluence of the λse-calculus via a generalized interpretation method, (1995), Draft.
[18] Kesner, D, La définition de fonctions par cas à l’aide de motifs dans des langages applicatifs, ()
[19] Kesner, D, Reasoning about layered, wildcard and product patterns, () · Zbl 0988.68531
[20] Klop, J.W, Combinatory reduction systems, Math. center tracts, 27, (1980) · Zbl 0466.03006
[21] Klop, J.W; van Oostrom, V; van Raamsdonk, F, Combinatory reduction systems: introduction and survey, Theoret. comput. sci., 121, 279-308, (1993), Bohm’s Festschrift. · Zbl 0796.03024
[22] Klop, J.W; van Oostrom, V; van Raamsdonk, F, Combinatory reduction systems: introduction and survey, () · Zbl 0796.03024
[23] Lévy, J.J, An algebraic interpretation of the λβκ-calculus and a labelled λ-calculus, Theoret. comput. sci., 2, 97-114, (1976) · Zbl 0335.02016
[24] Mints, G, Closed categories and the theory of proofs, (), 83-114
[25] Mints, G, Teorija categorii i teoria dokazatelstv. I, (), 252-278
[26] Necula, C, Algebraic rewriting preserves (β, η) confluence in the typed lambda calculus, ()
[27] Nesmith, D, An application of Klop’s counterexample to a higher-order rewrite system, ()
[28] Nipkow, T, Higher-order critical pairs, (), 342-349
[29] Okada, M, Strong normalizability for the combined system of the types lambda calculus and an arbitrary convergent term rewrite system, ()
[30] Poigné, A; Voss, J, On the implementation of abstract data types by programming language constructs, J. comput. system sci., 34, 340-376, (1987) · Zbl 0619.68025
[31] van Oostrom, V, Developing developments, (1994), Draft · Zbl 0903.68104
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.