Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages

In the last few years there has been a growing interest towards methods for statistical inference and learning based on computational geometry and, notably, tropical geometry, that is, the study of algebraic varieties over the min-plus semiring. At the same time, recent work has demonstrated the possibility of interpreting higher-order probabilistic programming languages in the framework of tropical mathematics, by exploiting algebraic and categorical tools coming from the semantics of linear logic. In this work we combine these two worlds, showing that tools and ideas from tropical geometry can be used to perform statistical inference over higher-order probabilistic programs. Notably, we first show that each such program can be associated with a degree and a n-dimensional polyhedron that encode its most likely runs. Then, we use these tools in order to design an intersection type system that estimates most likely runs in a compositional and efficient way.