@inproceedings{f5b42d10e79e4594a32fdf1918bc0cb2,
title = "Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs",
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{\textquoteright}s theory of generalized metric spaces.",
keywords = "Differential lambda-calculus, Lawvere quantale, Program metrics, Relational semantics, Tropical semiring",
author = "Davide Barbarossa and Paolo Pistone",
year = "2024",
month = feb,
day = "7",
doi = "10.4230/LIPICS.CSL.2024.14",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Murano, {Aniello } and Silva, {Alexandra }",
booktitle = "32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)",
address = "Germany",
}
