Abstract
We study the extensional version of the simply typed λ-calculus with product types and fixpoints enriched with layered, wildcard and product patterns. Extensionality is expressed by the surjective pairing axiom and a generalization of the η- conversion to patterns. We obtain a confluent reduction system by turning the extensional axioms as expansion rules, and then adding some restrictions to these expansions in order to avoid reduction loops. Confluence is proved by composition of modular properties of the extensional and non-extensional subsystems of the reduction calculus.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Yohji Akama. On mints' reductions for ccc-calculus. In Typed Lambda Calculus and Applications, number 664 in LNCS. Springer Verlag, 1993.
Val Breazu-Tannen, Delia Kesner, and Laurence Puel. A typed pattern calculus. In Proceedings of the Symposium on Logic in Computer Science (LICS), Montreal, Canada, June 1993.
Guy Cousineau, Pierre-Louis Curien, Michel Mauny, and Ascánder Suárez. Combinateurs catégoriques et implémentation des langages fonctionnels. Technical Report LIENS-86-3, Laboratoire d'Informatique du Département de Mathématiques et d'Informatique de l'École Normale Supérieur, 1986.
Djordje Cubric. On free ccc. Distributed on the types mailing list, 1992.
Roberto Di Cosmo and Delia Kesner. A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object. In Andrzej Lingas, editor, Intern. Conf. on Automata, Languages and Programming (ICALP), number 700 in LNCS. Springer-Verlag, 1993.
Roberto Di Cosmo and Delia Kesner. Simulating expansions without expansions. Mathematical Structures in Computer Science, 1993. To appear. Available also as INRIA Technical Report 1911.
Roberto Di Cosmo and Delia Kesner. Combining first order algebraic rewriting systems, recursion and extensional typed lambda calculi. In Intern. Conf. on Automata, Languages and Programming (ICALP), LNCS. Springer-Verlag, 1994. To appear.
Daniel Dougherty. Some lambda calculi with categorical sums and products. In Proc. of the Fifth International Conference on Rewriting Techniques and Applications (RTA), 1993.
Xavier Leroy et al. The Caml Light system, release 0.6. Software and documentation distributed by anonymous FTP on ftp.inria.fr, 1993.
Jean Gallier. Constructive logics part i: A tutorial on proof systems and typed λ-calculi. Theoretical Computer Science, 110:249–339, 1993.
Thérèse Hardin. Résultats de confluence pour les règles fortes de la logique combinatoire catégorique et liens avec les lambda-calculs. Thèse de doctorat, Université de Paris VII, 1987.
Brian Howard. Fixed Points and Extensionality in Typed Functional Programming Languages. PhD thesis, Stanford University, August 1992.
Gérad Huet. Résolution d'équations dans les langages d'ordre 1,2, ...,ω. Thèse de doctorat d'état, Université Paris VII, 1976.
Colin Barry Jay. Long βη normal forms and confluence (and its revised version). Technical Report ECS-LFCS-91-183, LFCS, University of Edimburgh, 1992.
Colin Barry Jay and Neil Ghani. The virtues of eta-expansion. Technical Report ECS-LFCS-92-243, LFCS, University of Edimburgh, 1992.
Simon Peyton Jones. The implementation of functional programming languages. Prentice-Hall, 1987.
Delia Kesner. La définition de fonctions par cas à l'aide de motifs dans des langages applicatifs. Thèse de doctorat, Université de Paris XI, Orsay, december 1993.
Grigori Mints. Teorija categorii i teoria dokazatelstv.I. Aktualnye problemy logiki i metodologii nauky, pages 252–278, 1979.
Dan Nesmith. An application of Klop's counterexample to a higher-order rewrite system. Seki-Report SR-94-06, Department of Computer Science, University of the Saarland, 1989.
Garrel Pottinger. The Church Rosser Theorem for the Typed lambda-calculus with Surjective Pairing. Notre Dame Journal of. Formal Logic, 22(3):264–268, 1981.
Dag Prawitz. Ideas and results in proof theory. Proceedings of the 2nd Scandinavian Logic Symposium, pages 235–307, 1971.
Vincent van Oostrom. Lambda calculus with patterns. Technical Report IR 228, Vrije Universiteit, Amsterdam, November 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag
About this paper
Cite this paper
Kesner, D. (1994). Reasoning about layered, wildcard and product patterns. In: Levi, G., Rodríguez-Artalejo, M. (eds) Algebraic and Logic Programming. ALP 1994. Lecture Notes in Computer Science, vol 850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58431-5_18
Download citation
DOI: https://doi.org/10.1007/3-540-58431-5_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58431-5
Online ISBN: 978-3-540-48791-3
eBook Packages: Springer Book Archive