Abstract
A new proof of strong normalization of Parigot’s (second order) λμ-calculus is given by a reduction-preserving embedding into system F (second order polymorphic λ-calculus). The main idea is to use the least stable supertype for any type. These non-strictly positive inductive types and their associated iteration principle are available in system F, and allow to give a translation vaguely related to CPS translations (corresponding to the Kolmogorov embedding of classical logic into intuitionistic logic). However, they simulate Parigot’s μ-reductions whereas CPS translations hide them.
As a major advantage, this embedding does not use the idea of reducing stability (¬¬¬ ¬ ¬) to that for atomic formulae. Therefore, it even extends to non-interleaving positive fixed-point types. As a non-trivial application, strong normalization of λμ-calculus, extended by primitive recursion on monotone inductive types, is established.
I am grateful for an invitation to present a preliminary version of the present results at the “Séminaire Preuves, Programmes et Systèmes” at Paris VII in October 2000.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, second revised edition, 1984.
Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Proceedings of the fifth ACM SIGPLAN International Conference on Functional Programming (ICFP’ 00), Montréal, pages 233–243. ACM Press, 2000.
Philippe de Groote. A CPS-translation of the λμ-calculus. In Sophie Tison, editor, Trees in Algebra and Programming — CAAP’94, 19th International Colloquium, volume 787 of Lecture Notes in Computer Science, pages 85–99, Edinburgh, 1994. Springer Verlag.
Herman Geuvers. Inductive and coinductive types with iteration and recursion. In Bengt Nordström, Kent Pettersson, and Gordon Plotkin, editors, Proceedings of the 1992 Workshop on Types for Proofs and Programs, Bästad, Sweden, June 1992, pages 193–217, 1992. Only published electronically: ftp://ftp.cs.chalmers.se/pub/cs-reports/baastad.92/proc.dvi.Z
Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.
Thierry Joly. Un plongement de la logique classique du 2nd ordre dans AF2. Unpublished manuscript. In French, 5 pp., January 1996.
Ralph Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Doktorarbeit (PhD thesis), University of Munich, 1998. Available via http://www.tcs.informatik.uni-muenchen.de/~matthes/.
Ralph Matthes. Monotone (co)inductive types and positive fixed-point types. The-oretical Informatics and Applications, 33(4/5):309–328, 1999.
Ralph Matthes. Monotone fixed-point types and strong normalization. In Georg Gottlob, Etienne Grandjean, and Katrin Seyr, editors, Computer Science Logic, 12th International Workshop, Brno, Czech Republic, August 24–28, 1998, Proceedings, volume 1584 of Lecture Notes in Computer Science, pages 298–312. Springer-Verlag, 1999.
Nax P. Mendler. Recursive types and type constraints in second-order lambda calculus. In Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, Ithaca, N.Y., pages 30–36. IEEE Computer Society Press, 1987. Forms a part of [11].
Paul F. Mendler. Inductive definition in type theory. Technical Report 87-870, Cornell University, Ithaca, N.Y., September 1987. Ph.D. Thesis (Paul F. Mendler = Nax P. Mendler).
Michel Parigot. λμ-calculus: an algorithmic interpretation of classical natural deduction. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning, International Conference LPAR’92, St. Petersburg, Russia, volume 624 of Lecture Notes in Computer Science, pages 190–201. Springer Verlag, 1992.
Michel Parigot. Strong normalization for second order classical natural deduction. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 39–46, Montreal, Canada, 1993. IEEE Computer Society Press.
Michel Parigot. Proofs of strong normalisation for second order classical natural deduction. The Journal of Symbolic Logic, 62(4):1461–1479, 1997.
Christine Paulin-Mohring. Définitions Inductives en Théorie des Types d’Ordre Supérieur. Habilitation á diriger les recherches, ENS Lyon, 1996.
Dag Prawitz. Natural Deduction. A Proof-Theoretical Study. Almquist and Wiksell, 1965.
Zdzisław Spławski and Paweł Urzyczyn. Type Fixpoints: Iteration vs. Recursion. SIGPLAN Notices, 34(9):102–113, 1999. Proceedings of the 1999 International Conference on Functional Programming (ICFP), Paris, France.
Thomas Streicher and Bernhard Reus. Classical logic, continuation semantics and abstract machines. Journal of Functional Programming, 8(6):543–572, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Matthes, R. (2001). Parigot’s Second Order λμ-Calculus and Inductive Types. In: Abramsky, S. (eds) Typed Lambda Calculi and Applications. TLCA 2001. Lecture Notes in Computer Science, vol 2044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45413-6_26
Download citation
DOI: https://doi.org/10.1007/3-540-45413-6_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41960-0
Online ISBN: 978-3-540-45413-7
eBook Packages: Springer Book Archive