Document Open Access Logo

Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs

Authors Davide Barbarossa , Paolo Pistone

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.14.pdf
  • Filesize: 0.95 MB
  • 23 pages

Document Identifiers

Author Details

Davide Barbarossa
  • Università di Bologna, Italy
Paolo Pistone
  • Università di Bologna, Italy

Funding

This work has been supported by the European Research Council through the project ERC CoG 818616 DIAPASoN.

Cite AsGet BibTex

Davide Barbarossa and Paolo Pistone. Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.14

Abstract

We study the interpretation of the lambda-calculus in a framework based on tropical mathematics, and we show that it provides a unifying framework for two well-developed quantitative approaches to program semantics: on the one hand program metrics, based on the analysis of program sensitivity via Lipschitz conditions, on the other hand resource analysis, based on linear logic and higher-order program differentiation. To do that, we focus on the semantics arising from the relational model weighted over the tropical semiring, and we discuss its application to the study of "best case" program behavior for languages with probabilistic and non-deterministic effects. Finally, we show that a general foundation for this approach is provided by an abstract correspondence between tropical algebra and Lawvere’s theory of generalized metric spaces.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Categorical semantics
  • Theory of computation → Linear logic
Keywords
  • Relational semantics
  • Differential lambda-calculus
  • Tropical semiring
  • Program metrics
  • Lawvere quantale

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Samson Abramsky and Steven Vickers. Quantales, observational logic and process semantics. Mathematical Structures in Computer Science, 3(2):161-227, 1993. URL: https://doi.org/10.1017/S0960129500000189.
  2. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The (in)efficiency of interaction. In Proceedings POPL 2021, volume 5, New York, NY, USA, 2021. Association for Computing Machinery. Google Scholar
  3. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. Multi types and reasonable space. Proceedings ICFP 2022, 6, 2022. Google Scholar
  4. Marianne Akian, Stéphane Gaubert, and Alexander Guterman. Tropical polyhedra are equivalent to mean payoff games. International Journal of Algebra and Computation, 22(01):1250001, 2023/01/16 2012. URL: https://doi.org/10.1142/S0218196711006674.
  5. Marianne Akian, Stéphane Gaubert, Viorel Niţică, and Ivan Singer. Best approximation in max-plus semimodules. Linear Algebra and its Applications, 435(12):3261-3296, 2011. URL: https://doi.org/10.1016/j.laa.2011.06.009.
  6. Mario Alvarez-Picallo and Jean-Simon Pacaud Lemay. Cartesian difference categories. In Jean Goubault-Larrecq and Barbara König, editors, Proceedings FoSSaCS 2020, pages 57-76, Cham, 2020. Springer International Publishing. Google Scholar
  7. Mario Alvarez-Picallo and C.-H. Luke Ong. Change actions: Models of generalised differentiation. In Mikołaj Bojańczyk and Alex Simpson, editors, Proceedings FoSSaCS 2019, pages 45-61, Cham, 2019. Springer International Publishing. Google Scholar
  8. Mário S. Alvim, Miguel E. Andrés, Konstantinos Chatzikokolakis, Pierpaolo Degano, and Catuscia Palamidessi. Differential privacy: On the trade-off between utility and information leakage. In Proceedings FAST 2011, FAST-11, pages 39-54, Berlin, Heidelberg, 2011. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-29420-4_3.
  9. Melissa Antonelli, Ugo Dal Lago, and Paolo Pistone. Curry and Howard Meet Borel. In Proceedings LICS 2022, pages 1-13,. IEEE Computer Society, 2022. Google Scholar
  10. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. In Proceedings POPL 2017, pages 545-556, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3009837.3009890.
  11. Marco Azevedo de Amorim, Gaboardi, Arthur, Justin Hsu, and Shin-ya Katsumata. Probabilistic relational reasoning via metrics. In Proceedings LICS 2019. IEEE Computer Society, 2019. Google Scholar
  12. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Logical Methods in Computer Science, 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:20)2018.
  13. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. Probabilistic relational reasoning for differential privacy. In Proceedings POPL 2012. ACM Press, 2012. URL: https://doi.org/10.1145/2103656.2103670.
  14. Leonard E. Baum and Ted Petrie. Statistical inference for probabilistic functions of finite state markov chains. The Annals of Mathematical Statistics, 37(6):1554-1563, 2023/01/17/ 1966. URL: http://www.jstor.org/stable/2238772.
  15. Richard Blute, Thomas Ehrhard, and Christine Tasson. A convenient differential category. Cahiers de Topologie et Géométrie DIfférentielle Catégorique, LIII:211-232, 2012. URL: https://arxiv.org/abs/1006.3140.
  16. Richard F. Blute, Robin Cockett, J.S.P. Lemay, and R.A.G. Seely. Differential categories revisited. Applied Categorical Structures, 28:171-235, 2020. Google Scholar
  17. Richard F. Blute, Robin Cockett, and R.A.G. Seely. Cartesian Differential Categories. Theory and Applications of Categories, 22(23):622-672, 2009. Google Scholar
  18. Gérard Boudol. The lambda-calculus with multiplicities. In Eike Best, editor, Proceedings CONCUR'93, pages 1-6, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg. Google Scholar
  19. Flavien Breuvart and Ugo Dal Lago. On intersection types and probabilistic lambda calculi. In Proceedings PPDP 2018, PPDP '18, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3236950.3236968.
  20. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Categorical models for simply typed resource calculi. In Proceedings MFPS 2010, volume 265 of Electronic Notes in Theoretical Computer Science, pages 213-230, 2010. URL: https://doi.org/10.1016/j.entcs.2010.08.013.
  21. Maria Manuel Clementino and Dirk Hofmann. Exponentiation in V-categories. Topology and its Applications, 153(16):3113-3128, 2006. URL: https://doi.org/10.1016/j.topol.2005.01.038.
  22. Stefan Cobzaş. Lipschitz properties of convex functions. Advances in Operator Theory, 2(1):21-49, 2017. URL: https://doi.org/10.22034/aot.1610.1022.
  23. Raphaëlle Crubillé. Probabilistic stable functions on discrete cones are power series. In Proceedings LICS 2018, pages 275-284. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209198.
  24. Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential logical relations, part I: the simply-typed case. In Proceedings ICALP 2019, pages 111:1-111:14, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.111.
  25. Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On quantitative algebraic higher-order theories. In Proceedings FSCD 2022, volume 228 of LIPIcs, pages 4:1-4:18, 2022. Google Scholar
  26. Ugo Dal Lago and Ulrich Schöpp. Computation by interaction for space-bounded functional programming. Information and Computation, 248:150-194, June 2016. URL: https://doi.org/10.1016/j.ic.2015.04.006.
  27. Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation, 209(6):966-991, 2011. URL: https://doi.org/10.1016/j.ic.2011.02.001.
  28. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science, 28(7):1169-1203, 2018. Google Scholar
  29. Thomas Ehrhard. Finiteness spaces. Mathematical Structures in Computer Science, 15(4):615-646, 2005. URL: https://www.cambridge.org/core/article/finiteness-spaces/E5E9CE1FA4050A56EF25CFB6F6A5754F.
  30. Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science, pages 1-66, February 2017. URL: https://doi.org/10.1017/S0960129516000372.
  31. Thomas Ehrhard. Cones as a model of intuitionistic linear logic. In Proceedings LICS 2020, pages 370-383. IEEE Computer Society, 2020. URL: https://doi.org/10.1145/3373718.3394758.
  32. Thomas Ehrhard. Differentials and distances in probabilistic coherence spaces. Logical Methods in Computer Science, 18(3):2:1-2:33, 2022. Google Scholar
  33. Thomas Ehrhard, Michele Pagani, and Christine Tasson. The computational meaning of probabilistic coherence spaces. In Proceedings LICS 2011, pages 87-96. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.29.
  34. Thomas Ehrhard, Michele Pagani, and Christine Tasson. Full Abstraction for Probabilistic PCF. Journal of the ACM, 65(4), 2018. Google Scholar
  35. Thomas Ehrhard, Michele Pagani, and Christine Tasson. Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. In Proceedings POPL 2018, volume 2, pages 59:1-59:28, 2018. URL: https://doi.org/10.1145/3158147.
  36. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1):1-41, December 2003. URL: https://doi.org/10.1016/S0304-3975(03)00392-X.
  37. Martín Hötzen Escardó. A metric model of PCF, 1999. Unpublished note presented at the Workshop on Realizability Semantics and Applications, June 1999. Available at the author’s webpage. Google Scholar
  38. Soichiro Fuji. Enriched categories and tropical mathematics, 2019. URL: https://arxiv.org/abs/1909.07620.
  39. Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear dependent types for differential privacy. SIGPLAN Not., 48(1):357-370, January 2013. URL: https://doi.org/10.1145/2480359.2429113.
  40. Zeinab Galal. A bicategorical model for finite nondeterminism. In Proceedings FSCD 2021, volume 195 of LIPIcs, pages 10:1-10:17, 2021. Google Scholar
  41. D. Gebler and S. Tini. SOS specifications for uniformly continuous operators. Journal of Computer and System Science, 92:113-151, 2018. Google Scholar
  42. Guillaume Geoffroy and Paolo Pistone. A partial metric semantics of higher-order types and approximate program transformations. In Proceedings CSL 2021, volume 183 of LIPIcs, pages 35:1-35:18, 2021. Google Scholar
  43. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  44. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: A modular approach to polynomial time computability. Theoretical Computer Science, 97:1-66, 1992. Extended abstract in Feasible Mathematics, S. R. Buss and P. J. Scott editors, Proceedings of the MCI Workshop, Ithaca, NY, June 1989, Birkhauser, Boston, pp. 195-209. Google Scholar
  45. Dima Grigoriev. Tropical differential equations. Advances in Applied Mathematics, 82:120-128, 2017. URL: https://doi.org/10.1016/j.aam.2016.08.002.
  46. Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. In Proceedings LICS 2017. IEEE Computer Society, 2017. Google Scholar
  47. Dirk Hofmann, Gavin J Seal, and W Tholen. Monoidal Topology: a Categorical Approach to Order, Metric and Topology. Cambridge University Press, New York, 2014. Google Scholar
  48. C. Kahlert and L.O. Chua. The complete canonical piecewise-linear representation. I. the geometry of the domain space. IEEE Transactions on Circuits and Systems I: Fundamental Theory and Applications, 39(3):222-236, 1992. URL: https://doi.org/10.1109/81.128016.
  49. Shin-ya Katsumata. A double category-theoretic analysis of graded linear exponential comonads. In Proceedings FoSSaCS 2018, pages 110-127. Springer International Publishing, 2018. Google Scholar
  50. Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In Proceedings LICS 2013, pages 301-310. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.36.
  51. F. William Lawvere. Metric spaces, generalized logic, and closed categories. Rendiconti del Seminario Matematico e Fisico di Milano, 43(1):135-166, December 1973. URL: https://doi.org/10.1007/BF02924844.
  52. Jean-Simon Pacaud Lemay. Convenient antiderivatives for differential linear categories. Mathematical Structures in Computer Science, 30(5):545-569, 2020. Google Scholar
  53. Jean-Simon Pacaud Lemay. Coderelictions for Free Exponential Modalities. In Proceedings CALCO 2021, volume 211 of Leibniz International Proceedings in Informatics (LIPIcs), pages 19:1-19:21, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CALCO.2021.19.
  54. Yves Lucet. What shape is your conjugate? a survey of computational convex analysis and its applications. SIAM Journal on Optimization, 20(1):216-250, 2009. URL: https://doi.org/10.1137/080719613.
  55. Diane Maclagan and Bernd Sturmfels. Introduction to tropical geometry, volume 161 of Graduate Studies in Mathematics. American Mathematical Society, 2015. Google Scholar
  56. Giulio Manzonetto. What is a categorical model of the differential and the resource λ-calculi? Mathematical Structures in Computer Science, 22(3):451-520, 2012. URL: https://doi.org/10.1017/S0960129511000594.
  57. Petros Maragos, Vasileios Charisopoulos, and Emmanouil Theodosis. Tropical geometry and machine learning. Proceedings of the IEEE, 109(5):728-755, 2021. URL: https://doi.org/10.1109/JPROC.2021.3065238.
  58. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proceedings LICS 2016. IEEE Computer Society, 2016. Google Scholar
  59. Damiano Mazza, Luc Pellissier, and Pierre Vial. Polyadic approximations, fibrations and intersection types. In Proceedings POPL 2018. ACM, 2018. Google Scholar
  60. Paul-André Melliès, Nicolas Tabareau, and Christine Tasson. An explicit formula for the free exponential modality of linear logic. Mathematical Structures in Computer Science, 28(7):1253-1286, 2018. URL: https://doi.org/10.1017/S0960129516000426.
  61. Gian Maria Negri Porzio, Vanni Noferini, and Leonardo Robol. Tropical Laurent series, their tropical roots, and localization results for the eigenvalues of nonlinear matrix functions, 2021. URL: https://arxiv.org/abs/2107.07982.
  62. Vanni Noferini, Meisam Sharify, and Françoise Tisseur. Tropical roots as approximations to eigenvalues of matrix polynomials. SIAM J. Matrix Anal. Appl., 36(1):138-157, January 2015. URL: https://doi.org/10.1137/14096637X.
  63. Federico Olimpieri. Intersection type distributors. In Proceedings LICS 2021. IEEE Computer Society, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470617.
  64. Lior Pachter and Bernd Sturmfels. Tropical geometry of statistical models. Proceedings of the National Academy of Sciences, 101(46):16132-16137, 2023/01/16 2004. URL: https://doi.org/10.1073/pnas.0406010101.
  65. Michele Pagani and Paolo Tranquilli. Parallel reduction in resource λ-calculus. In Proceedings APLAS 2009, pages 226-242, 2009. Google Scholar
  66. Paolo Pistone. On generalized metric spaces for the simply typed λ-calculus. In Proceedings LICS 2021, pages 1-14. IEEE Computer Society, 2021. Google Scholar
  67. Gordon Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223-255, 1977. Google Scholar
  68. Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger. Proceedings ICFP 2010, pages 157-168, 2010. Google Scholar
  69. Ciro Russo. Quantale Modules, with Applications to Logic and Image Processing. PhD thesis, Università degli Studi di Salerno, available at https://arxiv.org/abs/0909.4493, 2007.
  70. Ulrich Schöpp. Stratified Bounded Affine Logic for Logarithmic Space. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 411-420, July 2007. URL: https://doi.org/10.1109/LICS.2007.45.
  71. Peter Selinger. Towards a semantics for higher-order quantum computation. In Proceedings QPL 2004, TUCS General Publication No 33, pages 127-143, 2004. Google Scholar
  72. Imre Simon. On semigroups of matrices over the tropical semiring. Informatique Théorique et Applications, 28:277-294, 1994. Google Scholar
  73. Isar Stubbe. Categorical structures enriched in a quantaloid: Tensored and cotensored categories. Theory and Applications of Categories, 16(14):283-306, 2006. Google Scholar
  74. Isar Stubbe. An introduction to quantaloid-enriched categories. Fuzzy Sets and Systems, 256:95-116, 2014. Special Issue on Enriched Category Theory and Related Topics (Selected papers from the 33rd Linz Seminar on Fuzzy Set Theory, 2012). URL: https://doi.org/10.1016/j.fss.2013.08.009.
  75. Franck van Breugel. An introduction to metric semantics: operational and denotational models for programming and specification languages. Theoretical Computer Science, 258(1):1-98, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00403-5.
  76. Simon Willerton. Tight spans, Isbell completions and semi-tropical modules. Theory and Applications of Categories, 28(22):696-732, 2013. Google Scholar
  77. Liwen Zhang, Gregory Naitzat, and Lek-Heng Lim. Tropical geometry of deep neural networks. In Proceedings ICML 2018, volume 80 of Proceedings of Machine Learning Research, pages 5819-5827. PMLR, 2018. URL: http://proceedings.mlr.press/v80/zhang18i.html.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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