Abstract
Different pattern calculi integrate the functional mechanisms from the λ-calculus and the matching capabilities from rewriting. Several approaches are used to obtain the confluence but in practice the proof methods share the same structure and each variation on the way pattern-abstractions are applied needs another proof of confluence.
We propose here a generic confluence proof where the way pattern-abstractions are applied is axiomatized. Intuitively, the conditions guarantee that the matching is stable by substitution and by reduction.
We show that our approach directly applies to different pattern calculi, namely the lambda calculus with patterns, the pure pattern calculus and the rewriting calculus. We also characterize a class of matching algorithms and consequently of pattern-calculi that are not confluent.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ait-Kaci, H., Podelski, A., Smolka, G.: A feature constraint system for logic programming with entailment. Theoretical Computer Science 122(1-2), 263–283 (1994)
Arbiser, A., Miquel, A., Ríos, A.: A lambda-calculus with constructors. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 181–196. Springer, Heidelberg (2006)
Barendregt, H.: The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics. North Holland, 2nd edn. (1984)
Barthe, G., Cirstea, H., Kirchner, C., Liquori, L.: Pure Patterns Type Systems. In: 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL 2003, New Orleans, USA, pp. 250–261. ACM, New York (2003)
Bertolissi, C., Kirchner, C.: The rewriting calculus as a combinatory reduction system. In: Siedl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, Springer, Heidelberg (2007)
Cirstea, H., Kirchner, C.: The rewriting calculus — Part I and II. Logic Journal of the Interest Group in Pure and Applied Logics 9, 427–498 (2001)
Cirstea, H., Liquori, L., Wack, B.: Rewriting calculus with fixpoints: Untyped and first-order systems. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 147–161. Springer, Heidelberg (2004)
Curien, P.-L., Hardin, T., Lévy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM (JACM) 43(2), 362–397 (1996)
Hoffmann, C.M., O’Donnell, M.J.: Pattern matching in trees. Journal of the ACM 29(1), 68–95 (1982)
Jay, B., Kesner, D.: Pure pattern calculus. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, pp. 100–114. Springer, Heidelberg (2006)
Kesner, D.: Confluence of extensional and non-extensional lambda-calculi with explicit substitutions. Theoritical Computer Science 238(1-2), 183–220 (2000)
Kirchner, C., Kopetz, R., Moreau, P.-E.: Anti-pattern matching. In: European Symposium on Programming – ESOP 2007, Braga, Portugal. LNCS, Springer, Heidelberg (2007)
Klop, J.W.: Combinatory Reduction Systems. Ph.D. thesis, Mathematisch Centrum, Amsterdam (1980)
Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: Introduction and survey. Theoretical Computer Science 121, 279–308 (1993)
Knuth, D.E., Morris, J., Pratt, V.: Fast pattern matching in strings. SIAM Journal of Computing 6(2), 323–350 (1977)
Liquori, L., Honsell, F., Lenisa, M.: A framework for defining logical frameworks (2007) (submitted)
Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Comput. Sci. 192, 3–29 (1998)
Melliès, P.-A.: Axiomatic rewriting theory VI residual theory revisited. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 24–50. Springer, Heidelberg (2002)
Peyton-Jones, S.: The implementation of functional programming languages. Prentice Hall, Inc., Englewood Cliffs (1987)
Takahashi, M.: Parallel reductions in λ-calculus. Information and Compututation 118, 120–127 (1995)
Terese: Term Rewriting Systems. Cambridge University Press, Cambridge (2002)
The Maude Team. The Maude Home Page, http://maude.cs.uiuc.edu/
The Tom Team. The Tom language, http://tom.loria.fr/
van Oostrom, V.: Lambda calculus with patterns. Technical report, Vrije Universiteit, Amsterdam (November 1990)
Yokouchi, H., Hikita, T.: A rewriting system for categorical combinators with multiple arguments. SIAM Journal on Computing 19(1), 78–97 (1990)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cirstea, H., Faure, G. (2007). Confluence of Pattern-Based Calculi. In: Baader, F. (eds) Term Rewriting and Applications. RTA 2007. Lecture Notes in Computer Science, vol 4533. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73449-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-73449-9_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73447-5
Online ISBN: 978-3-540-73449-9
eBook Packages: Computer ScienceComputer Science (R0)