×

A compact fixpoint semantics for term rewriting systems. (English) Zbl 1209.68285

Summary: This work is motivated by the fact that a “compact” semantics for term rewriting systems, which is essential for the development of effective semantics-based program manipulation tools (e.g. automatic program analyzers and debuggers), does not exist. The big-step rewriting semantics that is most commonly considered in functional programming is the set of values/normal forms that the program is able to compute for any input expression. Such a big-step semantics is unnecessarily oversized, as it contains many “semantically useless” elements that can be retrieved from a smaller set of terms. Therefore, in this article, we present a compressed, goal-independent collecting fixpoint semantics that contains the smallest set of terms that are sufficient to describe, by semantic closure, all possible rewritings. We prove soundness and completeness under ascertained conditions. The compactness of the semantics makes it suitable for applications. Actually, our semantics can be finite whereas the big-step semantics is generally not, and even when both semantics are infinite, the fixpoint computation of our semantics produces fewer elements at each step. To support this claim we report several experiments performed with a prototypical implementation.

MSC:

68Q42 Grammars and rewriting systems
68Q55 Semantics in the theory of computing

Software:

Maude; MTT; Haskell; TOY
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Alpuente, M.; Comini, M.; Escobar, S.; Falaschi, M.; Lucas, S., Abstract diagnosis of functional programs, (Leuschel, M., Logic Based Program Synthesis and Transformation — 12th International Workshop, LOPSTR 2002, Revised Selected Papers. Logic Based Program Synthesis and Transformation — 12th International Workshop, LOPSTR 2002, Revised Selected Papers, Lecture Notes in Computer Science, vol. 2664 (2003), Springer-Verlag: Springer-Verlag Berlin), 1-16 · Zbl 1278.68056
[2] Alpuente, M.; Correa, F. J.; Falaschi, M., A declarative debugging scheme for functional logic programs, (Hanus, M., Proceedings of 10th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2001). Proceedings of 10th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2001), Electronic Notes in Theoretical Computer Science, vol. 64 (2002), Elsevier Science Publishers: Elsevier Science Publishers North Holland) · Zbl 1268.68091
[3] Alpuente, M.; Escobar, S.; Iborra, J., Termination of narrowing revisited, Theoretical Computer Science, 410, 46, 4608-4625 (2009) · Zbl 1187.68271
[4] Alpuente, M.; Falaschi, M.; Ramis, M. J.; Vidal, G., A compositional semantics for conditional term rewriting systems, (Bal, H. E., Proc. of 6th IEEE Int’l Conf. on Computer Languages, ICCL’94 (1994), IEEE Computer Society Press: IEEE Computer Society Press Los Alamitos, CA, USA), 171-182
[5] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press: Cambridge University Press Cambridge, UK
[6] Barbuti, R.; Giacobazzi, R.; Levi, G., A general framework for semantics-based bottom-up abstract interpretation of logic programs, ACM Transactions on Programming Languages and Systems, 15, 1, 133-181 (1993)
[7] Bert, D.; Echahed, R.; Østvold, B. M., Abstract rewriting, (Proceedings of Third Int’l Workshop on Static Analysis (WSA’93). Proceedings of Third Int’l Workshop on Static Analysis (WSA’93), Lecture Notes in Computer Science, vol. 724 (1993), Springer-Verlag: Springer-Verlag Berlin), 178-192
[8] Bossi, A.; Gabbrielli, M.; Levi, G.; Martelli, M., The s-semantics approach: theory and applications, Journal of Logic Programming, 19-20, 149-197 (1994) · Zbl 0942.68527
[9] Christian, J., Some termination criteria for narrowing and E-narrowing, (Automated Deduction—CADE-11. Automated Deduction—CADE-11, Lecture Notes in Computer Science, vol. 607 (1992), Springer-Verlag: Springer-Verlag Berlin), 582-588
[10] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C., (All About Maude — A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic. All About Maude — A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol. 4350 (2007), Springer-Verlag: Springer-Verlag Berlin) · Zbl 1115.68046
[11] Comini, M.; Levi, G.; Meo, M. C.; Vitiello, G., Proving properties of logic programs by abstract diagnosis, (Dams, M., Proceedings of Analysis and Verification of Multiple-Agent Languages, 5th LOMAPS Workshop (LOMAPS’96). Proceedings of Analysis and Verification of Multiple-Agent Languages, 5th LOMAPS Workshop (LOMAPS’96), Lecture Notes in Computer Science, vol. 1192 (1996), Springer-Verlag: Springer-Verlag Berlin), 22-50
[12] Comini, M.; Levi, G.; Meo, M. C.; Vitiello, G., Abstract diagnosis, Journal of Logic Programming, 39, 1-3, 43-93 (1999) · Zbl 0947.68024
[13] Comon-Lundh, H., Intruder theories (ongoing work), (Proceedings FoSSaCS 2004. Proceedings FoSSaCS 2004, Lecture Notes in Computer Science, vol. 2987 (2004), Springer-Verlag), 1-4 · Zbl 1126.68390
[14] Cortier, V.; Delaune, S.; Lafourcade, P., A survey of algebraic properties used in cryptographic protocols, Journal of Computer Security, 14, 1, 1-43 (2006)
[15] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Los Angeles, California, January 17-19 (1977), ACM Press: ACM Press New York, NY, USA), 238-252
[16] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (van Leeuwen, J., Handbook of Theoretical Computer Science. Handbook of Theoretical Computer Science, Formal Methods and Semantics, vol. B (1990), Elsevier), 244-320, chapter 6 · Zbl 0900.68283
[17] Durán, F.; Lucas, S.; Meseguer, J., MTT: The Maude Termination Tool (System Description), (Armando, A.; Baumgartner, P.; Dowek, G., Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Proceedings. Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Proceedings, Lecture Notes in Computer Science, vol. 5195 (2008), Springer-Verlag), 313-319 · Zbl 1165.68360
[18] Falaschi, M.; Levi, G.; Martelli, M.; Palamidessi, C., A new declarative semantics for logic languages, (Kowalski, R. A.; Bowen, K. A., Proceedings of Fifth Int’l Conf. on Logic Programming (1988), The MIT Press: The MIT Press Cambridge, Mass), 993-1005
[19] Falaschi, M.; Levi, G.; Martelli, M.; Palamidessi, C., Declarative modeling of the operational behavior of logic languages, Theoretical Computer Science, 69, 3, 289-318 (1989) · Zbl 0699.68113
[20] M. Fay, First-order unification in an equational theory, in: Fourth Int’l Conf. on Automated Deduction, 1979, pp. 161-167.; M. Fay, First-order unification in an equational theory, in: Fourth Int’l Conf. on Automated Deduction, 1979, pp. 161-167.
[21] Giesl, J.; Swiderski, S.; Schneider-Kamp, P.; Thiemann, R., Automated termination analysis for haskell: from term rewriting to programming languages, (Pfenning, Frank, Term Rewriting and Applications, 17th International Conference, RTA 2006, Proceedings. Term Rewriting and Applications, 17th International Conference, RTA 2006, Proceedings, Lecture Notes in Computer Science, vol. 4098 (2006), Springer-Verlag), 297-312 · Zbl 1151.68444
[22] Hanus, M., The integration of functions into logic programming: from theory to practice, Journal of Logic Programming, 19&20, 583-628 (1994) · Zbl 0942.68526
[23] Hanus, M., Multi-paradigm declarative languages, (Dahl, V.; Niemelä, I., Logic Programming, 23rd International Conference, ICLP 2007, Proceedings. Logic Programming, 23rd International Conference, ICLP 2007, Proceedings, Lecture Notes in Computer Science, vol. 4670 (2007), Springer-Verlag), 45-75 · Zbl 1213.68162
[24] Hanus, M., Call pattern analysis for functional logic programs, (Proceedings 10th Int’l ACM SIGPLAN Conf. on Principle and Practice of Declarative Programming. Proceedings 10th Int’l ACM SIGPLAN Conf. on Principle and Practice of Declarative Programming, PPDP’08 (2008), ACM Press), 67-78
[25] Haskell Debugging Technologies. At http://www.haskell.org/debugging/; Haskell Debugging Technologies. At http://www.haskell.org/debugging/
[26] Hullot, J.-M., Canonical forms and unification, (Proceedings of the 5th International Conference on Automated Deduction. Proceedings of the 5th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 87 (1980), Springer-Verlag: Springer-Verlag Berlin), 318-334
[27] Klop, J. W., Term rewriting systems, (Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science, vol. I (1992), Oxford University Press), 1-112
[28] Knuth, D. E.; Bendix, P. B., Simple word problems in universal algebras, (Computational Problems in Abstract Algebra (1970)), 263-297 · Zbl 0188.04902
[29] López-Fraguas, F. J.; Sánchez-Hernández, J., TOY: a multiparadigm declarative system, (Proc. of 10th International Conference on Rewriting Techniques and Applications, RTA 1999. Proc. of 10th International Conference on Rewriting Techniques and Applications, RTA 1999, Lecture Notes in Computer Science, vol. 1631 (1999), Springer-Verlag), 244-247
[30] Marlow, S.; Iborra, J.; Pope, B.; Gill, A., A lightweight interactive debugger for haskell, (Keller, G., Proceedings of the ACM SIGPLAN Workshop on Haskell (Haskell 2007) (2007), ACM Press), 13-24
[31] Meseguer, J.; Rosu, G., The rewriting logic semantics project, Theoretical Computer Science, 373, 3, 213-237 (2007) · Zbl 1111.68068
[32] Meseguer, J.; Thati, P., Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, Higher-Order and Symbolic Computation, 20, 1-2, 123-160 (2007) · Zbl 1115.68079
[33] Middeldorp, A.; Hamoen, E., Completeness results for basic narrowing, Journal of Applicable Algebra in Engineering, Communication and Computing, 5, 313-353 (1994) · Zbl 0810.68088
[34] Mitchell, N.; Runciman, C., A static checker for safe pattern matching in haskell, (Van Eekelen, M., Trends in Functional Programming, vol. 6 (2007)), 15-30, Intellect
[35] Nielson, H. R.; Nielson, F., Infinitary control flow analysis: a collecting semantics for closure analysis, (Symposium on Principles of Programming Languages (1997)), 332-345
[36] Peyton Jones, S., Haskell 98 Language and Libraries: the Revised Report (2003), Cambridge University Press · Zbl 1067.68041
[37] Plasmeijer, R.; van Eekelen, M., Functional Programming and Parallel Graph Rewriting (1993), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0788.68023
[38] (TeReSe, Term Rewriting Systems (2003), Cambridge University Press: Cambridge University Press Cambridge, UK) · Zbl 1030.68053
[39] Wadler, P., An angry half-dozen, SIGPLAN Notices, 33, 2, 25-30 (1998)
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.