Abstract
General computational models obtained by integrating different specific models have recently become a stimulating and promising research subject for the computer science community. In particular, combinations of algebraic term rewriting systems and various λ-calculi, either typed or untyped, have been deeply investigated. In the present paper this subject is addressed from the point of view of type assignment. A powerful type assignment system, the one based on intersection types, is combined with term rewriting systems, first and higher order, and relevant properties of the resulting system, like strong normalization and confluence, are proved.
To Roberta Gottardi
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
S. van Bakel, S. Smetsers, and S. Brock. Type assignment in left linear applicative term rewriting systems. In Proc. of CAAP'92. Colloquium on Trees in Algebra and Programming, Rennes, France, 1992, 1992.
F. Barbanera. Adding algebraic rewriting to the calculus of constructions: Strong normalization preserved. In Proc. of the 2nd Int. Workshop on Conditional and Typed Rewriting, 1990.
F. Barbanera. Combining term rewriting and type assignment systems. International Journal of Foundations of Computer Science, 1:165–184, 1990.
H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter λ-model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940, 1983.
H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North Holland, Amsterdam, 2nd ed., 1984.
Val Breazu-Tannen. Combining algebra and higher-order types. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, July 1988.
Val Breazu-Tannen and Jean Gallier. Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science, 1990. to appear.
F. Cardone and M. Coppo. Two extensions of Curry's type inference system. In P. Odifreddi, editor, Logic and Computer Sciennce. Academic Press, 1990.
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–309. North-Holland, 1990.
Daniel J. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. In Proc. 4th Rewriting Techniques and Applications, Como, LNCS 488, 1991.
J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.
M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF. Lecture Notes in Computer Science, 78, 1979.
R. Hindley. Types with intersection, an introduction. Formal aspects of Computing, 1990.
R. Hindley and J. Seldin. Introduction to Combinators and λ-calculus. Cambridge University Press, 1986.
Jean-Pierre Jouannaud and Mitsuhiro Okada. Executable higher-order algebraic specification languages. In Proc. 6th IEEE Symp. Logic in Computer Science, Amsterdam, pages 350–361, 1991.
J. W. Klop. Term rewriting systems: a tutorial. EATCS Bulletin, 32:143–182, June 1987.
D. Leivant. Typing and computational properties of lambda expressions. Theoretical Computer Science, 44:51–68, 1986.
M. H. A. Newman. On theories with a combinatorial definition of ‘equivalence'. Ann. Math., 43(2):223–243,1942.
T. Nipkow. Higher order critical pairs. In Proc. IEEE Symp. on Logic in Comp. Science, Amsterdam, 1991.
Mitsuhiro Okada. Strong normalizability for the combined system of the types lambda calculus and an arbitrary convergent term rewrite system. In Proc. ISSAC 89, Portland, Oregon, 1989.
G. Pottinger. A type assignment for the strongly normalizable λ-terms. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 561–578. Academic Press, 1980.
Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25:141–143, April 1987.
D. A. Turner. Miranda: A non-strict functional language with polymorphic types. In Functional Programming Languages and Computer Architecture, Nancy, LNCS 201. Springer-Verlag, September 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barbanera, F., Fernández, M. (1993). Combining first and higher order rewrite systems with type assignment systems. In: Bezem, M., Groote, J.F. (eds) Typed Lambda Calculi and Applications. TLCA 1993. Lecture Notes in Computer Science, vol 664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0037098
Download citation
DOI: https://doi.org/10.1007/BFb0037098
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56517-8
Online ISBN: 978-3-540-47586-6
eBook Packages: Springer Book Archive