Document Open Access Logo

Quantitative Equational Rewriting

Authors Besik Dundua , Georg Ehling , Santiago Escobar , Maribel Fernández , Temur Kutsia

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2026.76.pdf
  • Filesize: 1 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Quantitative rewriting
  • quantitative equational reasoning

Metrics

Abstract

Rewriting logic is a logical framework for expressing both concurrent computation and logical deduction using equations and rewrite rules. Quantitative equational reasoning enriches equations with quantitative measures, expressing concepts such as similarity or proximity rather than mere equality of terms. In this article, we bring these two approaches together and propose a quantitative extension of rewriting logic as a flexible formalism for quantitative deduction and computation.

Cite As Get BibTex

Besik Dundua, Georg Ehling, Santiago Escobar, Maribel Fernández, and Temur Kutsia. Quantitative Equational Rewriting. In 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 386, pp. 76:1-76:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.MFCS.2026.76

Author Details

Besik Dundua
  • Giorgi Nikoladze Scientific-Research Center, Kutaisi International University, Georgia
  • Vekua Institute of Applied Mathematics, Tbilisi State University, Georgia
Georg Ehling
  • RISC, Johannes Kepler University Linz, Austria
Santiago Escobar
  • VRAIN, Universitat Politècnica de València, Spain
Maribel Fernández
  • Department of Informatics, King’s College London, UK
Temur Kutsia
  • RISC, Johannes Kepler University Linz, Austria

Funding

Partially supported by the Austrian Science Fund (FWF) project P 35530; Rustaveli National Science Foundation of Georgia project FR-25-5957; grant CIPROM/2022/6 funded by Generalitat Valenciana; grant PID2024-162030OB-100 funded by MCIN/AEI/10.13039/501100011033 and ERDF A way of making Europe; The NATO Science for Peace and Security Programme project SymSafe (grant number G6133).

References

  1. Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl, and Joost-Pieter Katoen. Weighted rewriting: Semiring semantics for abstract reduction systems. In Maribel Fernández, editor, 10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025, July 14-20, 2025, Birmingham, UK, volume 337 of LIPIcs, pages 6:1-6:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.FSCD.2025.6.
  2. Martin Avanzini and Akihisa Yamada. Weighted rewriting. In René Thiemann and Christoph Weidenbach, editors, Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings, volume 15979 of Lecture Notes in Computer Science, pages 191-208. Springer, 2025. URL: https://doi.org/10.1007/978-3-032-04167-8_11.
  3. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google Scholar
  4. Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. An algebraic theory of Markov processes. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 679-688. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209177.
  5. Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative equational reasoning. In Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva, editors, Foundations of Probabilistic Programming, pages 333-360. Cambridge University Press, 2020. URL: https://doi.org/10.1017/9781108770750.011.
  6. Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Tensor of quantitative equational theories. In Fabio Gadducci and Alexandra Silva, editors, 9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021, Salzburg, Austria, August 31 - September 3, 2021, volume 211 of LIPIcs, pages 7:1-7:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CALCO.2021.7.
  7. Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Propositional logics for the Lawvere quantale. In Marie Kerjean and Paul Blain Levy, editors, Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics, MFPS XXXIX, Indiana University, Bloomington, IN, USA, June 21-23, 2023, volume 3 of Electronic Notes in Theoretical Informatics and Computer Science. EpiSciences, 2023. URL: https://doi.org/10.46298/ENTICS.12292.
  8. Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Rational Lawvere logic (invited paper). In Stefano Guerrini and Barbara König, editors, 34th EACSL Annual Conference on Computer Science Logic, CSL 2026, Paris, France, February 23-28, 2026, volume 363 of LIPIcs, pages 3:1-3:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. URL: https://doi.org/10.4230/LIPIcs.CSL.2026.3.
  9. Leo Bachmair, Nachum Dershowitz, and David A. Plaisted. Completion without failure. In Resolution of Equations in Algebraic Structures, Volume 2: Rewriting Techniques. Academic Press, 1989. Google Scholar
  10. Roberto Bruni and José Meseguer. Semantic foundations for generalized rewrite theories. Theoretical Computer Science, 360(1–3):386-414, 2006. URL: https://doi.org/10.1016/J.TCS.2006.04.012.
  11. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM Trans. Comput. Log., 11(4):23:1-23:38, 2010. URL: https://doi.org/10.1145/1805950.1805953.
  12. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative automata under probabilistic semantics. Log. Methods Comput. Sci., 15(3), 2019. URL: https://doi.org/10.23638/LMCS-15(3:16)2019.
  13. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott, editors. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71999-1.
  14. Raphaëlle Crubillé and Ugo Dal Lago. Metric reasoning about λ-terms: The affine case. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 633-644. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.64.
  15. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 545-556. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009890.
  16. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theor. Comput. Sci., 318(3):323-354, 2004. URL: https://doi.org/10.1016/J.TCS.2003.09.013.
  17. Manfred Droste and Dietrich Kuske. Weighted automata. In Jean-Éric Pin, editor, Handbook of Automata Theory, pages 113-150. European Mathematical Society Publishing House, Zürich, Switzerland, 2021. URL: https://doi.org/10.4171/AUTOMATA-1/4.
  18. Manfred Droste, Temur Kutsia, George Rahonis, and Wolfgang Schreiner. McCarthy-Kleene fuzzy automata and MSO logics. Inf. Comput., 272:104499, 2020. URL: https://doi.org/10.1016/J.IC.2019.104499.
  19. Besik Dundua, Georg Ehling, Santiago Escobar, Maribel Fernández, and Temur Kutsia. Quantitative equational rewriting. RISC Report Series 26-09, Research Institute for Symbolic Computation, Johannes Kepler University Linz, Altenberger Straße 69, 4040 Linz, Austria, June 2026. URL: https://doi.org/10.35011/risc.26-09.
  20. Besik Dundua, Temur Kutsia, Mircea Marin, and Cleo Pau. Extending the ρLog calculus with proximity relations. In George Jaiani and David Natroshvili, editors, Applications of Mathematics and Informatics in Natural Sciences and Engineering, volume 334 of Springer Proceedings in Mathematics & Statistics, pages 83-100. Springer International Publishing, Cham, 2020. URL: https://doi.org/10.1007/978-3-030-56356-1_6.
  21. Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, and Carolyn L. Talcott. Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program., 110, 2020. URL: https://doi.org/10.1016/J.JLAMP.2019.100497.
  22. Georg Ehling and Temur Kutsia. Solving quantitative equations. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II, volume 14740 of Lecture Notes in Computer Science, pages 381-400. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63501-4_20.
  23. Norm Ferns, Prakash Panangaden, and Doina Precup. Metrics for finite Markov decision processes. In David Maxwell Chickering and Joseph Y. Halpern, editors, UAI '04, Proceedings of the 20th Conference in Uncertainty in Artificial Intelligence, Banff, Canada, July 7-11, 2004, pages 162-169. AUAI Press, 2004. URL: https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_id=1103&proceeding_id=20.
  24. Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 452-461. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209149.
  25. Francesco Gavazzo. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. (Equivalences coinductives et métriques pour les langages d'ordre supérieur avec des effets algébriques). PhD thesis, University of Bologna, Italy, 2019. URL: https://doi.org/10.6092/unibo/amsdottorato/9075.
  26. Francesco Gavazzo and Cecilia Di Florio. Quantitative and metric rewriting: Abstract, non-expansive, and graded systems. CoRR, abs/2206.13610, 2022. URL: https://doi.org/10.48550/arXiv.2206.13610.
  27. Francesco Gavazzo and Cecilia Di Florio. Elements of quantitative rewriting. Proc. ACM Program. Lang., 7(POPL):1832-1863, 2023. URL: https://doi.org/10.1145/3571256.
  28. Daniel Gebler, Kim G. Larsen, and Simone Tini. Compositional bisimulation metric reasoning with probabilistic process calculi. Log. Methods Comput. Sci., 12(4), 2016. URL: https://doi.org/10.2168/LMCS-12(4:12)2016.
  29. Jürgen Giesl and Deepak Kapur. Dependency pairs for equational rewriting. In Aart Middeldorp, editor, Rewriting Techniques and Applications, 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001, Proceedings, volume 2051 of Lecture Notes in Computer Science, pages 93-108. Springer, 2001. URL: https://doi.org/10.1007/3-540-45127-7_9.
  30. Joseph A. Goguen and José Meseguer. Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci., 105(2):217-273, 1992. URL: https://doi.org/10.1016/0304-3975(92)90302-V.
  31. Thomas A. Henzinger. From boolean to quantitative notions of correctness. In Manuel V. Hermenegildo and Jens Palsberg, editors, Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pages 157-158. ACM, 2010. URL: https://doi.org/10.1145/1706299.1706319.
  32. Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4):1155-1194, 1986. URL: https://doi.org/10.1137/0215084.
  33. Gunther Jäger and T. M. G. Ahsanullah. Characterization of quantale-valued metric spaces and quantale-valued partial metric spaces by convergence. Applied General Topology, 19(1):129-144, 2018. URL: https://doi.org/10.4995/agt.2018.7849.
  34. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585-591. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_47.
  35. Churn Jung Liau and Bertrand I-peng Lin. Fuzzy term-rewriting system. Fuzzy Sets and Systems, 44(1):1-15, 1991. URL: https://doi.org/10.1016/0165-0114(91)90028-O.
  36. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative algebraic reasoning. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 700-709. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  37. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. On the axiomatizability of quantitative algebras. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005102.
  38. Catherine Meadows, Radha Poovendran, Dusko Pavlovic, LiWu Chang, and Paul F. Syverson. Distance bounding protocols: Authentication logic analysis and collusion attacks. In Radha Poovendran, Sumit Roy, and Cliff Wang, editors, Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks, Advances in Information Security, pages 279-298. Springer, 2007. URL: https://doi.org/10.1007/978-0-387-46276-9_12.
  39. José Meseguer. Conditional rewriting logic as a united model of concurrency. Theor. Comput. Sci., 96(1):73-155, 1992. URL: https://doi.org/10.1016/0304-3975(92)90182-F.
  40. José Meseguer. Twenty years of rewriting logic. J. Log. Algebraic Methods Program., 81(7-8):721-781, 2012. URL: https://doi.org/10.1016/J.JLAP.2012.06.003.
  41. José Meseguer. Strict coherence of conditional rewriting modulo axioms. Theoretical Computer Science, 672:1-35, 2017. URL: https://doi.org/10.1016/J.TCS.2016.12.026.
  42. José Meseguer. Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebraic Methods Program., 110, 2020. URL: https://doi.org/10.1016/J.JLAMP.2019.100483.
  43. Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. Beyond nonexpansive operations in quantitative algebraic reasoning. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 52:1-52:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533366.
  44. Peter Csaba Ölveczky and José Meseguer. Specification of real-time and hybrid systems in rewriting logic. Theor. Comput. Sci., 285(2):359-405, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00363-2.
  45. Peter Csaba Ölveczky and José Meseguer. Semantics and pragmatics of Real-Time Maude. High. Order Symb. Comput., 20(1-2):161-196, 2007. URL: https://doi.org/10.1007/S10990-007-9001-5.
  46. Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28(2):233-264, 1981. URL: https://doi.org/10.1145/322248.322251.
  47. Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Paul Hudak and Stephanie Weirich, editors, Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 157-168. ACM, 2010. URL: https://doi.org/10.1145/1863543.1863568.
  48. Lennert De Smet, Pedro Zuidberg Dos Martires, Robin Manhaeve, Giuseppe Marra, Angelika Kimmig, and Luc De Raedt. Neural probabilistic logic programming in discrete-continuous domains. In Robin J. Evans and Ilya Shpitser, editors, Uncertainty in Artificial Intelligence, UAI 2023, July 31 - 4 August 2023, Pittsburgh, PA, USA, volume 216 of Proceedings of Machine Learning Research, pages 529-538. PMLR, 2023. URL: https://proceedings.mlr.press/v216/de-smet23a.html.
  49. Leon Weber, Pasquale Minervini, Jannes Münchmeyer, Ulf Leser, and Tim Rocktäschel. NLProlog: Reasoning with weak unification for question answering in natural language. In Anna Korhonen, David R. Traum, and Lluís Màrquez, editors, Proceedings of the 57th Conference of the Association for Computational Linguistics, ACL 2019, Florence, Italy, July 28 - August 2, 2019, Volume 1: Long Papers, pages 6151-6161. Association for Computational Linguistics, 2019. URL: https://doi.org/10.18653/V1/P19-1618.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact