一句话：研究给 Gödel T 加入不同概率选择算子后的表达力，证明它们均几乎必然终止但可生成不同的分布类。
本文研究子递归高阶概率演算的表达能力。作者在 Gödel T 这类极具表达力的确定型演算上加入多种概率选择算子，考察所得演算能否生成相同的分布类；结果显示，尽管所有演算都保证几乎必然终止，不同选择算子所定义的分布类并不等价。方法上，作者引入经典可归约性（reducibility）技术的概率变体，并用它证明最简单的概率选择并不改变 T 的本质表达力。最后，在标准观察下，这些演算在函数表达力上仍都对应 T 所表示的函数。
We study the expressive power of subrecursive probabilistic higher-order calculi. More specifically, we show that endowing a very expressive deterministic calculus like G\"odel's $\mathbb{T}$ with various forms of probabilistic choice operators may result in calculi which are not equivalent as for the class of distributions they give rise to, although they all guarantee almost-sure termination. Along the way, we introduce a probabilistic variation of the classic reducibility technique, and we prove that the simplest form of probabilistic choice leaves the expressive power of $\mathbb{T}$ essentially unaltered. The paper ends with some observations about the functional expressive power: expectedly, all the considered calculi capture the functions which $\mathbb{T}$ itself represents, at least when standard notions of observations are considered.
@article{paperbot1251,
title = {On Higher-Order Probabilistic Subrecursion},
author = {Flavien Breuvart and Ugo Dal Lago and Agathe Herrou},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 4},
year = {2021},
doi = {10.46298/lmcs-17(4:25)2021}
}