Document Open Access Logo

Rational Lawvere Logic (Invited Paper)

Authors Giorgio Bacci , Radu Mardare, Prakash Panangaden, Gordon Plotkin

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.3.pdf
  • Filesize: 0.81 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Quantitative reasoning
  • complete deductive system
  • Lawvere’s quantale

Metrics

Abstract

We study Rational Lawvere logic (RL). This logic is defined over the extended positive reals with an algebraic structure combining the Lawvere quantale (with the reversed order on the extended reals and a sum as tensor) and a multiplicative quantale (with the usual order on the extended reals and a multiplication as tensor); together they provide a semiring structure. The logic is designed for complex quantitative reasoning, including sequents expressing inequalities between rational functions over the extended positive reals. We give a deduction system and demonstrate its expressiveness by deriving a classical result from probability theory relating the Kantorovich and total variation distances. Our deductive system is complete for finitely axiomatizable theories. The proof of completeness relies on the Krivine-Stengle Positivstellensatz.
We additionally provide complexity results for both RL and its affine fragment AL. We consider two decision problems: the satisfiability of a set of sequents and whether a sequent follows from a finite set of sequent. We show that both problems lie in PSPACE for RL, and we give sharper complexity bounds for AL: the first problem is NP-complete, while the second is co-NP-complete.

Cite As Get BibTex

Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Rational Lawvere Logic (Invited Paper). In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.3

Author Details

Giorgio Bacci
  • Department of Computer Science, Aalborg University, Denmark
Radu Mardare
  • School of Mathematical and Computer Sciences, Edinburgh, UK
Prakash Panangaden
  • School of Computer Science, McGill University, Montreal, Canada
  • School of Informatics, University of Edinburgh, UK
Gordon Plotkin
  • LFCS, School of Informatics, University of Edinburgh, UK

Funding

  • Mardare, Radu: EPSRC grant EP/Y000455/1, A correct-by-construction approach to approximate computation and ARIA TA1.1 project Predicate Logic as a Foundation for Verified ML.
  • Panangaden, Prakash: Natural Sciences and Engineering Research Council of Canada (NSERC).

References

  1. Jirí Adámek. Varieties of quantitative algebras and their monads. 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 9:1-9:10. ACM, 2022. URL: https://doi.org/10.1145/3531130.3532405.
  2. Jirí Adámek, Matej Dostál, and Jirí Velebil. Strongly finitary monads for varieties of quantitative algebras. In Paolo Baldan and Valeria de Paiva, editors, 10th Conference on Algebra and Coalgebra in Computer Science, CALCO 2023, June 19-21, 2023, Indiana University Bloomington, IN, USA, volume 270 of LIPIcs, pages 10:1-10:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CALCO.2023.10.
  3. André Arnold and Maurice Nivat. Metric interpretations of infinite trees and semantics of non deterministic recursive programs. Theor. Comput. Sci., 11:181-205, 1980. URL: https://doi.org/10.1016/0304-3975(80)90045-6.
  4. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. ACM SIGPLAN Notices, 52(1):545-556, 2017. Google Scholar
  5. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Converging from branching to linear metrics on Markov chains. Math. Struct. Comput. Sci., 29(1):3-37, 2019. URL: https://doi.org/10.1017/S0960129517000160.
  6. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel. Computing probabilistic bisimilarity distances for probabilistic automata. In Wan J. Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands, volume 140 of LIPIcs, pages 9:1-9:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.9.
  7. 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.
  8. Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Tensor of quantitative equational theories. In 9th Conference on Algebra and Coalgebra in Computer Science, 2021. Google Scholar
  9. Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Propositional logics for the lawvere quantale. In Proceedings of the39th Conference on Mathematical Foundations of Programming Semantics MFPS XXXIX (MFPS 2023). ENTICS, 2023. Google Scholar
  10. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Behavioral metrics via functor lifting. In Venkatesh Raman and S. P. Suresh, editors, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India, volume 29 of LIPIcs, pages 403-415. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2014.403.
  11. Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. Lower bounds on hilbert’s nullstellensatz and propositional proofs. Proceedings of the London Mathematical Society, 3(1):1-26, 1996. Google Scholar
  12. Radim Belohlavek. Fuzzy relational systems: foundations and principles, volume 20. Springer Science & Business Media, 2012. Google Scholar
  13. Jacek Bochnak, Michel Coste, and Marie-Françoise Roy. Real Algebraic Geometry, volume 36 of A Series of Modern Surveys in Mathematics. Springer Science & Business Media, 1998. Google Scholar
  14. John F. Canny. Some algebraic and geometric computations in PSPACE. In Janos Simon, editor, Proceedings of the 20th Annual ACM Symposium on Theory of Computing, (STOC), pages 460-467. ACM, 1988. URL: https://doi.org/10.1145/62212.62257.
  15. 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.
  16. Raphaëlle Crubillé and Ugo Dal Lago. Metric reasoning about λ-terms: The general case. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 341-367. Springer, 2017. Google Scholar
  17. Francesco Dagnino and Fabio Pasquali. Logical foundations of quantitative equality. 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 16:1-16:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533337.
  18. Ugo Dal Lago and Francesco Gavazzo. A relational theory of effects and coeffects. Proceedings of the ACM on Programming Languages, 6(POPL):1-28, 2022. URL: https://doi.org/10.1145/3498692.
  19. 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.
  20. J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Metrics for labeled Markov systems. In Proceedings of CONCUR99, number 1664 in Lecture Notes in Computer Science. Springer-Verlag, 1999. Google Scholar
  21. Josée Desharnais, Vineet Gupta, Radhakrishnan Jagadeesan, and Prakash Panangaden. A metric for labelled Markov processes. Theoretical Computer Science, 318(3):323-354, June 2004. Google Scholar
  22. Francesc Esteva, Lluís Godo, Petr Hájek, and Mirko Navara. Residuated fuzzy logics with an involutive negation. Archive for mathematical logic, 39(2):103-124, 2000. URL: https://doi.org/10.1007/S001530050006.
  23. Julius Farkas. Theorie der einfachen ungleichungen. Journal für die reine und angewandte Mathematik (Crelles Journal), 1902(124):1-27, 1902. Google Scholar
  24. Norm Ferns, Prakash Panangaden, and Doina Precup. Metrics for finite Markov decision precesses. In Proceedings of the 20th Conference on Uncertainty in Artificial Intelligence, pages 162-169, July 2004. URL: https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_id=1103&proceeding_id=20.
  25. Norm Ferns, Prakash Panangaden, and Doina Precup. Metrics for Markov decision processes with infinite state spaces. In Proceedings of the 21st Conference on Uncertainty in Artificial Intelligence, pages 201-208, July 2005. URL: https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_id=1175&proceeding_id=21.
  26. 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.
  27. Alison L. Gibbs and Francis Edward Su. On choosing and bounding probability metrics. International Statistical Review, 70(3):419-435, 2002. Google Scholar
  28. Marco Grandis. Categories, norms and weights. Journal of Homotopy and Related Structures, 2(2):171-186, 2007. Google Scholar
  29. Dima Grigoriev and Nicolai N. Vorobjov Jr. Complexity of null-and positivstellensatz proofs. Ann. Pure Appl. Log., 113(1-3):153-160, 2001. URL: https://doi.org/10.1016/S0168-0072(01)00055-0.
  30. Petr Hájek. What is mathematical fuzzy logic. Fuzzy sets and systems, 157(5):597-603, 2006. URL: https://doi.org/10.1016/J.FSS.2005.10.004.
  31. Petr Hájek. Metamathematics of fuzzy logic. Springer Science & Business Media, 2013. Google Scholar
  32. Petr Hájek, Lluís Godo, and Francesc Esteva. A complete many-valued logic with product-conjunction. Archive for mathematical logic, 35:191-208, 1996. URL: https://doi.org/10.1007/BF01268618.
  33. Shin-ya Katsumata. A double category theoretic analysis of graded linear exponential comonads. In Foundations of Software Science and Computation Structures: 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018. Proceedings 21, pages 110-127. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_6.
  34. L.G. Khachiyan. Polynomial algorithms in linear programming. USSR Computational Mathematics and Mathematical Physics, 20(1):53-72, 1980. URL: https://doi.org/10.1016/0041-5553(80)90061-0.
  35. Jean-Louis Krivine. Anneaux préordonnés. Journal d'analyse mathématique, 12:p-307, 1964. Google Scholar
  36. Ugo Dal Lago and Francesco Gavazzo. Differential logical relations, part II increments and derivatives. Theor. Comput. Sci., 895:34-47, 2021. URL: https://doi.org/10.1016/J.TCS.2021.09.027.
  37. Ugo Dal Lago and Francesco Gavazzo. Modal reasoning = metric reasoning, via lawvere. CoRR, abs/2103.03871, 2021. URL: https://arxiv.org/abs/2103.03871.
  38. Ugo Dal Lago and Francesco Gavazzo. A relational theory of effects and coeffects. Proc. ACM Program. Lang., 6(POPL):1-28, 2022. URL: https://doi.org/10.1145/3498692.
  39. Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential logical relations, part I: the simply-typed case. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, volume 132 of LIPIcs, pages 111:1-111:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.111.
  40. Francis William Lawvere. Metric spaces, generalized logic, and closed categories. Rendiconti del seminario matématico e fisico di Milano, 43(1):135-166, 1973. Google Scholar
  41. Francis William Lawvere. Metric spaces, generalized logic, and closed categories. Reprints in Theory and Applications of Categories, 1:1-37, 2002. Originally published in Rendiconti del Seminario Matematico e Fisico di Milano, XLIII (1973), 135-166. URL: http://www.tac.mta.ca/tac/reprints/articles/1/tr1.pdf.
  42. Jean-Simon Pacaud Lemay and Jean-Baptiste Vienney. Graded differential categories and graded differential linear logic. 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 EPTICS. EpiSciences, 2023. URL: https://doi.org/10.46298/ENTICS.12290.
  43. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, pages 700-709, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  44. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. On the axiomatizability of quantitative algebras. In Proceedings of the 32nd Annual ACM-IEEE Symposium on Logic in Computer Science, 2017. Google Scholar
  45. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Fixed-points for quantitative equational logics. In Proceedings of the ACM-IEEE Symposium on Logic in Computer Science, 2021. Google Scholar
  46. Jiří Matoušek and Bernd Gärtner. Understanding and using linear programming, volume 1. Springer, 2007. Google Scholar
  47. Matteo Mio. Compact quantitative theories of convex algebras. In Stefan Milius and Clemens Kupke, editors, MFPS'25: 41st Conference on Mathematical Foundations of Programming Semantics, Glasgow, Scotland, June 16-20, 2025, page ?? EPTS, 2025. to appear. Google Scholar
  48. Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. Combining nondeterminism, probability, and termination: Equational and metric reasoning. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470717.
  49. 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.
  50. Théodore Samuel Motzkin. Two consequences of the transposition theorem on linear inequalities. Econometrica (pre-1986), 19(2):184, 1951. Google Scholar
  51. Jan Pavelka. On fuzzy logic i, ii, iii. Zeit. Math. Logik u. Grundl. Math., 25:447-464, 1979. Google Scholar
  52. Toniann Pitassi and Iddo Tzameret. Algebraic proof complexity: Progress, frontiers and challenges. ACM SIGLOG News, 3(3):21-43, 2016. URL: https://doi.org/10.1145/2984450.2984455.
  53. Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Paul Hudak and Stephanie Weirich, editors, Proceeding 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.
  54. James Renegar. On the computational complexity and geometry of the first-order theory of the reals. Part I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals. Journal of Symbolic Computation, 13(3):255-299, 1992. URL: https://doi.org/10.1016/S0747-7171(10)80003-3.
  55. Kimmo I. Rosenthal. Quantales and their applications. Longman Scientific and Technical, 1990. Google Scholar
  56. Petr Savickỳ, Roberto Cignoli, Francesc Esteva, Lluís Godo, and Carles Noguera. On product logic with truth-constants. Journal of Logic and Computation, 16(2):205-225, 2006. URL: https://doi.org/10.1093/LOGCOM/EXI075.
  57. Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, 1998. Google Scholar
  58. G Stengle. A nullstellensatz and a positivstellensatz in semialgebraic geometry. Mathematische Annalen, 207(2):87-97, 1974. Google Scholar
  59. Marshall H. Stone. Postulates for the barycentric calculus. Annali di Matematica Pura ed Applicata, 29(1):25-30, December 1949. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact