Lambda-calculus goes to the tropics


Davide Barbarossa, LIPN. 14 mars 2023 14:00 limd
Abstract:

Among the approaches directed towards the analysis of quantitative properties of programs, one can certainly mention the metric approaches and the differential/resource-aware ones. In both, the notion of (non-)linearity in the sense of linear logic plays a central role: the first ones aim at treating program distances, and duplication leads to interpret bounded programs as Lipschitz maps; the second ones aim at directly handling duplication in the syntax, and duplication leads to interpret programs as power series. A natural question is thus whether these two apparently unrelated ways of handling (non-)linearity can be somehow connected. At a first glance, there seems to be a “logarithmic” gap between the two: in metric models n duplications result in a Lipschitz function nx, while in differential models this results in a polynomial x^n, not Lipschitz. The central insight of my talk is that a natural way to overcome this obstacle and bridge these two viewpoints is to consider differential semantics in the framework of tropical mathematics, which is a rich combinatorial counterpart of usual algebraic geometry in tight relation with optimization and computational problems.