一句话：提出 λRPCF 类型系统，通过动态分布类型与 Lyapunov 秩函数，对概率高阶函数式程序进行组合式平均情形复杂度分析。
本文研究如何以组合方式分析概率高阶函数式程序的复杂度。作者将精化类型扩展为 λRPCF：为处理概率效应引入动态分布类型，并采用基于耦合的子类型关系；递归定义的终止性由 Lyapunov 秩函数保证。作者证明该类型系统对平均情形复杂度分析是可靠的，并具有外延完备性：任何平均情形 nolytime 图灵机都可编码为 λRPCF 中可类型化的项。这一结果说明概率程序的复杂度可像普通程序一样通过类型系统进行组合推理，并为概率高阶程序的平均情形复杂度提供类型论刻画。
We show that complexity analysis of probabilistic higher-order functional programs can be carried out compositionally by way of a type system. The introduced type system is a significant extension of refinement types. On the one hand, the presence of probabilistic effects requires adopting a form of dynamic distribution type, subject to a coupling-based subtyping discipline. On the other hand, recursive definitions are proved terminating by way of Lyapunov ranking functions. We prove not only that the obtained type system, called l\pmbRPCF, provides a sound methodology for average case complexity analysis, but also that it is extensionally complete, in the sense that any average case nolytime Turing machines can be encoded as a term typable in l\pmbRPCF.