一句话：将热带几何用于高阶概率程序的统计推断，并设计交集类型系统组合式估计最可能运行。
本文研究如何对高阶概率程序进行统计推断。作者结合热带几何（min-plus 半环上的代数簇）与近期用线性逻辑语义中的代数、范畴工具解释概率程序的思路，提出：每个高阶概率程序都可关联一个次数和一个 n 维多面体，用以编码其最可能的运行。基于此，作者设计了一种交集类型系统，以组合且高效的方式估计这些最可能运行。该工作把热带几何、λ演算与概率编程语言语义联系起来，为高阶概率程序的推断提供了类型论方法。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2501-15637,
title = {Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages},
author = {Davide Barbarossa and Paolo Pistone},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776675}
}