Polymorphic rewriting conserves algebraic strong normalization. (English) Zbl 0745.68065

Summary: We study combinations of many-sorted algebraic term rewriting systems and polymorphic lambda term rewriting. Algebraic and lambda terms are mixed by adding the symbols of the algebraic signature to the polymorphic lambda calculus, as higher-order constants. We show that if a many-sorted algebraic rewrite system \(R\) is strongly normalizing (terminating, Noetherian), then \(R+\beta+\eta+\text{type-}\beta+\text{type-}\eta\) rewriting of mixed terms is also strongly normalizing. The result is obtained using a technique which generalizes Girard’s “candidats de reductibilité”, introduced in the original proof of strong normalization for the polymorphic lambda calculus.


68Q42 Grammars and rewriting systems
Full Text: DOI Link


[1] Barendregt, H.P., The lambda calculus: its syntax and semantics, (1984), North-Holland Amsterdam, Studies in Logic and the Foundations of Mathematics · Zbl 0551.03007
[2] Barbanera, F., Combining term rewriting and type assignment systems, Proc. conf. Italian chapter of EATCS, (1989), to appear
[3] Breazu-Tannen, V.; Gallier, J., Polymorphic rewriting conserves algebraic confluence, (1989), manuscript, submitted for publication · Zbl 0686.68022
[4] Breazu-Tannen, V.; Meyer, A.R., Computable values can be classical, (), 238-245
[5] Breazu-Tannen, V., Combining algebra and higher-order types, (), 82-90
[6] Coquand, T.; Huet, G., The calculus of constructions, Inform. and control, 76, 95-120, (1988) · Zbl 0654.03045
[7] Dung, T.; Kfoury, A.J., Another view of combining β-reduction and algebraic rewriting, (1989), Boston University, manuscript
[8] Dougherty, D., Adding algebraic rewriting to the untyped lambda calculus, (March, 1989), Wesleyan University, manuscript
[9] Ehrig, H.; Mahr, B., Fundamentals of algebraic-specification 1: equations and initial semantics, (1985), Springer Berlin · Zbl 0557.68013
[10] Gallier, J., On Girard’s “candidats de reductibilité”, ()
[11] Girard, J.Y., Interprétation fonctionelle et élimination des coupures dans l’arithmétique d’ordre supérieure, Phd thesis, (1972), Université Paris VII
[12] Girard, J.Y.; Lafont, Y.; Taylor, P., Typed lambda calculus, (1989), Cambridge University Press
[13] Gallier, J.; Snyder, W., Complete sets of transformations for general E-unification, Theoret. comput. sci., 67, 203-260, (1989) · Zbl 0686.68024
[14] Gallier, J.; Snyder, W., Higher-order unification revisited: complete sets of transformations, J. symbolic comput., 8, 101-140, (1989) · Zbl 0682.03034
[15] Huet, G., A unification algorithm for typed λ-calculus, Theoret. comput. sci., 1, 27-57, (1975) · Zbl 0337.68027
[16] Klop, J.W., Term rewriting systems: a tutorial, Bull. EATCS, 32, 143-182, (1987) · Zbl 0666.68025
[17] Meseguer, J.; Goguen, J., Deduction with many-sorted rewrite, Technical report 42, (1985), CSLI Stanford · Zbl 0602.08004
[18] Mitchell, J.C., A type-inference approach to reduction properties and semantics of polymorphic expressions, (), 308-319
[19] Meyer, A.R.; Reinhold, M.B., ‘type’ is not a type: preliminary report, (), 287-295
[20] Okada, M., Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system, Proc. ISSAC, (1989), to appear
[21] Statman, R., Completeness, invariance and λ-definability, J. symbolic logic, 47, 17-26, (1982) · Zbl 0487.03006
[22] Statman, R., Logical relations and the typed λ-calculus, Inform. and control, 65, 85-97, (1985) · Zbl 0594.03006
[23] Tait, W.W., Intensional interpretations of functionals of finite type i, J. symbolic logic, 32, 198-212, (1967) · Zbl 0174.01202
[24] Tait, W.W., A realizability interpretation of the theory of species, (), 240-251, Lecture Notes in Mathematics
[25] Toyama, Y., On the church – rosser property for the direct sum of term rewriting systems, J. ACM, 34, 1, 128-143, (1987) · Zbl 1151.68453
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.