Abstract
We provide a confluent and strongly normalizing rewriting system, based on expansion rules, for the extensional second order typed lambda calculus with product and unit types: this system corresponds to the Intuitionistic Positive Calculus with implication, conjunction, quantification over proposition and the constant True. This result is an important step towards a new theory of reduction based on expansion rules, and gives a natural interpretation to the notion of second order η-long normal forms used in higher order resolution and unification, that are here just the normal forms of our reduction system.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Yohji Akama. On Mints' reductions for ccc-Calculus. In Typed Lambda Calculus and Applications, number 664 in LNCS, pages 1–12. Springer Verlag, 1993.
Henk Barendregt. The Lambda Calculus; Its syntax and Semantics (revised edition). North Holland, 1984.
Val Breazu-Tannen, Combining algebra and higher-order types. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 82–90, Edinburgh, Scotland, July 5–8 1988. IEEE Computer Society.
Val Breazu-Tannen and Jean Gallier. Polymorphic rewiting preserves algebraic confluence. Information and Computation, 114:1–29, 1994.
Val Breazu-Tannen and Albert R. Meyer. Polymorphism is conservative over simple types (preliminary report). In Proceedings, Symposium on Logic in Computer Science, pages 7–17, Cambridge, Massachusetts, June 16–18 1986. IEEE Computer Society.
Pierre-Louis Curien and Roberto Di Cosmo. A confluent reduction system for the λ-calculus with surjective pairing and terminal object. In Leach, Monien, and Artalejo, editors, Intern. Conf. on Automata, Languages and Programming (ICALP), volume 510 of Lecture Notes in Computer Science, pages 291–302. Springer-Verlag, July 1991.
Djordje Cubric. On free CCC. Distributed on the types mailing list, 1992.
Roberto Di Cosmo and Delia Kesner. Combining first order algebraic rewriting systems, recursion and extensional lambda calculi. In Serge Abite-boul and Eli Shamir, editors, Intern. Conf. on Automata, Languages and Programming (ICALP), volume 820 of Lecture Notes in Computer Science, pages 462–472. Springer-Verlag, July 1994.
Roberto Di Cosmo and Delia Kesner. Simulating expansions without expansions. Mathematical Structures in Computer Science, 4:1–48, 1994. A preliminary version is available as Technical Report LIENS-93-11/INRIA 1911.
Roberto Di Cosmo and Adolfo Piperno. Expanding extensional polymorphism. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Typed Lambda Calculus and Applications, volume 902 of Lecture Notes in Computer Science, pages 139–153, April 1995.
Daniel J. Dougherty. Some lambda calculi with categorical sums and products. In Proc, of the Fifth International Conference on Rewriting Techniques and Applications (RTA), 1993.
Alfons Geser. Relative termination. Dissertation, Fakultät für Mathematik und Informatik, Universität Passau, Germany, 1990. Also available as: Report 91-03, Ulmer Informatik-Berichte, Universität Ulm, 1991.
Herman Geuvers. The church-rosser property for βη-reduction in typed λ-calculi. In 7th Proceedings of the Symposium on Logic in Computer Science (LICS), pages 453–460, 1992.
Neil Ghani. Extensionality and polymorphism. University of Edimburgh, Submitted, 1995.
Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1990.
Colin Barry Jay. Long βη normal forms and confluence (revised). Technical Report 44, LFCS — University of Edinburgh, August 1992.
Colin Barry Jay and Neil Ghani. The Virtues of Eta-expansion. Technical Report ECS-LFCS-92-243, LFCS, 1992. University of Edimburgh, preliminary version of [JG95].
Colin Barry Jay and Neil Ghani. The Virtues of Eta-expansion. Journal of Functional Programming, 5(2):135–154, April 1995.
Jean-Pierre Jouannaud and Mitsuhiro Okada. A computation model for executable higher-order algebraic specification languages. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pages 350–361, Amsterdam, The Netherlands, July 15–18 1991. IEEE Computer Society Press.
Jan Willem Klop. Combinatory reduction systems. Mathematical Center Tracts, 27, 1980.
Tobias Nipkow. A critical pair lemma for higher-order rewrite systems and its application to λ*. First Annual Workshop on Logical Frameworks, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Di Cosmo, R., Kesner, D. (1996). Rewriting with extensional polymorphic λ-calculus. In: Kleine Büning, H. (eds) Computer Science Logic. CSL 1995. Lecture Notes in Computer Science, vol 1092. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61377-3_40
Download citation
DOI: https://doi.org/10.1007/3-540-61377-3_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61377-0
Online ISBN: 978-3-540-68507-4
eBook Packages: Springer Book Archive