×

A \(\rho\)-calculus of explicit constraint application. (English) Zbl 1115.68094

Summary: Theoretical presentations of the rewriting or \(\rho\)-calculus often treat the matching constraint computations as an atomic operation although matching constraints are explicitly expressed. Actual implementations have to take a more realistic view: computations needed in order to find the solutions of a matching equation can have an important impact on the (efficiency of the) calculus for some matching theories and the substitution application usually involves a term traversal.
Following the works on explicit substitutions in the \(\lambda\)-calculus, we present two versions of the \(\rho\)-calculus, one with explicit matching and one with explicit substitutions, together with a version that combines the two and considers efficiency issues and more precisely the composition of substitutions. The approach is general, allowing for potential extensions to various matching theories. We establish the confluence of the calculus and the termination of the explicit constraint handling and application sub-calculus.

MSC:

68Q42 Grammars and rewriting systems

Software:

ATERM; Maude; LCF; ELAN
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. J. Func. Progr. 1(4), 375–416 (1991) · Zbl 0941.68542 · doi:10.1017/S0956796800000186
[2] Barendregt, H.: The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics. 2nd edn. Elsevier Science Publishers B.V. (North-Holland), Amsterdam (1984) · Zbl 0551.03007
[3] Barthe, G., Cirstea, H., Kirchner, C., Liquori, L.: Pure patterns type systems. In: Principles of Programming Languages–POPL2003, New Orleans, USA. ACM (2003) · Zbl 1321.68137
[4] Berkling, K., Fehr, E.: A consistent extension of the lambda-calculus as a base for functional programming languages. Inform. Contr. 55(1–3), 89–101 (1982) · Zbl 0553.68025 · doi:10.1016/S0019-9958(82)90458-2
[5] Bloo, R., Rose, K.H.: Combinatory reduction systems with explicit substitution that preserve strong nomalisation. In: Proceedings of the Fifth International Conference on Rewriting Techniques and Application (RTA ’96), pp. 169–183 (1996)
[6] Borovanský, P.: Controlling rewriting: study and implementation of a strategy formalism. Elect. Notes Theor. Comp. Sci. 15 (1998) · Zbl 0917.68102
[7] Borovanský, P., Kirchner, C., Kirchner, H.: A functional view of rewriting and strategies for a semantics of ELAN. In: Sato, M., Toyama, Y. (eds.) The Third Fuji International Symposium on Functional and Logic Programming, pp. 143–167. Kyoto (1998). World Scientific. Also report LORIA 98-R-165
[8] Borovanský, P., Kirchner, C., Kirchner H., Moreau, P.-E., Ringeissen, C.: An overview of ELAN. In: Proceedings of Workshop on Rewriting Techniques and Application–WRLA’1998, vol. 15. Electronic Notes in Theoretical Computer Science (1998) Report LORIA 98-R-316 · Zbl 0917.68022
[9] van den Brand, M., de Jong, H., Klint, P., Olivier, P.: Efficient annotated terms. Softw. Prac. Exp. 30, 259–291 (2000) · doi:10.1002/(SICI)1097-024X(200003)30:3<259::AID-SPE298>3.0.CO;2-Y
[10] Chailloux, E., Manoury. P., Pagano, B.: Développement d’applications avec Objective CAML. O’REILLY (2000)
[11] Cirstea, H.: Calcul de réécriture: fondements et applications. PhD thesis, Université Henri Poincaré–Nancy I (2000)
[12] Cirstea, H., Faure, G., Kirchner, C.: A rho-calculus of explicit constraint application. In: Workshop on Rewriting Logic and Applications, Barcelona (Spain) (2004). Electronic Notes in Theoretical Computer Science · Zbl 1115.68094
[13] Cirstea, H., Kirchner, C.: The rewriting calculus–Part I and II. Logic J. Interest Group in Pure and Appl. Logics 9(3), 427–498 (2001) · Zbl 0986.03027
[14] Cirstea, H., Kirchner, C., Liquori, L.: Matching Power. In: Proceedings of Rewriting Techniques and Applications RTA’2001, http://www.springer.de/comp/lncs/index.html Lecture Notes in Computer Science, Utrecht (The Netherlands). Springer-Verlag (2001) · Zbl 0981.68065
[15] Cirstea, H., Kirchner, C., Liquori, L.: Rewriting calculus with(out) types. In: Fabio Gadducci, Ugo Montanari (eds.) Proceedings of the Fourth Workshop on Rewriting Logic and Applications, Pisa (Italy) (2002). Electronic Notes in Theoretical Computer Science · Zbl 1272.68173
[16] Cirstea, H., Kirchner, C., Liquori, L., Wack, B.: Rewrite strategies in the rewriting calculus. In: Proceedings of the Third International Workshop on Reduction Strategies in Rewriting and Programming, Valencia, Spain (2003). Electronic Notes in Theoretical Computer Science · Zbl 1270.68122
[17] Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude. In: José Meseguer (ed.) Proceedings of the First International Workshop on Rewriting Logic, vol. 4. Asilomar (California) (1996). Electronic Notes in Theoretical Computer Science · Zbl 0912.68095
[18] Curien, P.-L., Hardin, T., Lévy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. J. ACM (JACM) 43(2), 362–397 (1996) · Zbl 0885.03014 · doi:10.1145/226643.226675
[19] David, R., Guillaume, B.: A {\(\lambda\)}-calculus with explicit weakening and explicit substitution. Math. Struct. Comp. Sci. 11, 169–206 (2001) · Zbl 0972.68028 · doi:10.1017/S0960129500003224
[20] de Bruijn, N.: Lambda calculus with namefree formulas involving symbols that represent reference transforming mappings. Indagationes Mathematicae 40, 348–356 (1978) · Zbl 0393.03009
[21] de Bruijn, N.G.: A lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae 34, 381–392 (1972) · Zbl 0253.68007
[22] Dowek, G., Hardin, T., Kirchner, C.: Higher order unification via explicit substitutions. Inform. Comp. 157(1/2), 183–235 (2000) · Zbl 1005.03016 · doi:10.1006/inco.1999.2837
[23] Eker, S.: Associative-commutative matching via bipartite graph matching. Comp. J. 38(5), 381–399 (1995) · Zbl 05478894 · doi:10.1093/comjnl/38.5.381
[24] Faure, G., Kirchner, C.: Exceptions in the rewriting calculus. In: Proceedings of Rewriting Techniques and Applications–RTA’2002, vol. 2378 of LNCS, pp. 66–82, Copenhagen, Springer-Verlag (2002) · Zbl 1045.68069
[25] Gordon, M.J., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanized Logic of Computation, vol. 78 of Lecture Notes in Computer Science. Springer-Verlag, New York (NY, USA) (1979) · Zbl 0421.68039
[26] Hendriks, D., van Oostrom, V.: The {\(\lambda\)} calculus. In: Proceedings of Conference on Automated Deduction–CADE’2003, vol. 2741 of Lecture Notes in Artificial Intelligence, pp. 136–150 (2003)
[27] Hudak, P., Fasel, J.H.: A gentle introduction to Haskell. ACM SIGPLAN Notices 27(5), T-1–T-53 (1992)
[28] Huet, G.: Resolution d’Equations dans les Languages d’Ordre 1,2,...,{\(\omega\)}. These de Doctorat D’Etat, Universite Paris VII (1976)
[29] Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980) · Zbl 0458.68007 · doi:10.1145/322217.322230
[30] Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comp. 15(4), 1155–1194 (1986) · Zbl 0665.03005 · doi:10.1137/0215084
[31] Kesner, D., Lengrand, S.: Extending the explicit substitution paradigm. In: Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA ’05), LNCS 256 (2005) · Zbl 1078.03027
[32] Kirchner, C., Kirchner, H.: Rewriting, solving, proving. A preliminary version of a book available at | www.loria.fr/\(\sim\)ckirchne/rsp.ps.gz | (1999) · Zbl 0955.74027
[33] Kirchner, C., Kirchner, H.: Rule-based programming and proving : the ELAN experience outcomes. In: Ninth Asian Computing Science Conference–ASIAN’04, Chiang Mai, Thailand (2004) · Zbl 1115.68367
[34] Kirchner, C., Moreau, P.-E., Reilles, A.: Formal validation of pattern matching code. In: PPDP ’05: Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 187–197, ACM Press, New York, NY, USA (2005) · Zbl 1247.68056
[35] Klop, J.W.: Combinatory Reduction Systems. Ph.D. thesis, Mathematisch Centrum, Amsterdam (1980) · Zbl 0466.03006
[36] Leroy, X.: Compiling functional languages. Summer school on Semantics of programming languages (2002)
[37] Lescanne, P.: From {\(\lambda\)}{\(\sigma\)} to {\(\lambda\)}v a journey through calculi of explicit substitutions. In: Conference Record of POPL ’94, pp. 60–69. ACM (1994)
[38] Liang, C., Nadathur, G.: Choices in representation and reduction strategies for lambda terms in intensional contexts. J. Auto. Reasoning 33(2), 89–132 (2004) · Zbl 1102.68019 · doi:10.1007/s10817-004-6885-1
[39] Liquori, L., Serpette, B.: irho: an imperative rewriting calculus. In: Proceedings of te International Conference on Principles and Practice of Declarative Programming (PPDP’04), pp. 167–178 (2004) · Zbl 1153.68026
[40] Moreau, P.-E., Ringeissen, C., Vittek, M.: A Pattern Matching Compiler for Multiple Target Languages. In: Hedin G. (ed.) 12th Conference on Compiler Construction, Warsaw (Poland), vol. 2622 of LNCS, pp. 61–76. Springer-Verlag (2003) · Zbl 1032.68920
[41] Muñoz, C.: Un calcul de substitutions pour la représentation de preuves partielles en théorie de types. Thése de doctorat, Université Paris 7 (1997). English version available as INRIA research report RR-3309
[42] Nadathur, G.: The suspension notation for lambda terms and its use in metalanguage implementations. In: Ninth Workshop on Logic, Language, Information and Computation (WoLLIC’02) Electronic Notes in Theoretical Computer Science, vol. 67 (2002) · Zbl 1261.68043
[43] Nguyen, Q.-H., Kirchner, C., Kirchner, H.: External rewriting for skeptical proof assistants. J. Auto. Reasoning 29(3–4), 309–336 (2002) · Zbl 1064.68048 · doi:10.1023/A:1021975117537
[44] Ohlebusch, E.: Church-rosser theorems for abstract reduction modulo an equivalence relation. In: Proceedings of Rewriting Techniques and Applications (RTA-98), vol. 1379 of LNCS, pp. 17–31. Springer (1998)
[45] Pagano, B.: X.R.S: Explicit reduction systems–A first-order calculus for higher-order calculi. In: Proceedings of the International Conference on Automated Deduction (CADE ’98), pp. 72–87 (1998) · Zbl 0924.03047
[46] Rose, K.H.: Operational Reduction Models for Functional Programming Languages. Ph.D. Thesis, DIKU, University of Copenhagen, Denmark (1996) · Zbl 0891.68011
[47] Sinot, F.-R.: Director strings revisited: A generic approach to the efficient representation of free variables in higher-order rewriting. J. Log. Comput. 15(2), 201–218 (2005) · Zbl 1101.68639 · doi:10.1093/logcom/exi010
[48] Stehr, M.-O.: CINNI–A generic calculus of explicit substitutions and its application to lambda-, varsigma- and pi-calculi. Elect. Notes Theor. Comp. Sci. 36 (2000) · Zbl 0966.68147
[49] Stump, A., Deivanayagam, A., Kathol, S., Lingelbach, D., Schobel, D.: Rogue decision procedures. In: 1st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning–PDPAR (2003)
[50] Wack, B.: Aspects logique du calcul de réécriture. Ph.D. Thesis, Université Henri Poincaré–Nancy I (2005)
[51] Yokouchi, H., Hikita, T.: A rewriting system for categorical combinators with multiple arguments. SIAM J. Comput. 19(1), 78–97 (1990) · Zbl 0696.68041 · doi:10.1137/0219005
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.