一句话：综述λ演算的定量语义，证明关系语义、HO/N博弈语义与Taylor展开语义等价，并讨论两类关系模型推广。
本文综述λ演算定量语义的近期进展，核心问题是刻画带计量的高阶程序语义，并统一不同语义模型。作者以线性逻辑的退化关系模型 MRel 为起点，说明简单类型λ演算的三种定量语义——关系语义、HO/N 博弈语义与 Taylor 展开语义——彼此等价。随后介绍关系模型的两种推广：Laird 等人研究的以完备交换半环 R 为权重的 R-加权关系模型，以及 Fiore 等人提出的广义结构 species。文中还简要讨论这些模型在高层程序定量分析中的应用。
We present an overview of some recent work on the quantitative semantics of the λ-calculus. Our starting point is the fundamental degenerate model of linear logic, the relational model MRel. We show that three quantitative semantics of the simply-typed λ-calculus are equivalent: the relational semantics, HO/N game semantics, and the Taylor expansion semantics. We then consider two recent generalisations of the relational model: first, R-weighted relational models where R is a complete commutative semiring, as studied by Laird et al.; secondly, generalised species of structures, as introduced by Fiore et al. In each case, we briefly discuss some applications to quantitative analysis of higher-order programs.