一句话：基于博弈语义为按值调用 λ-演算提出组合式时间代价模型，并在 RAM 上给出保常因子的完全惰性图归约实现。
本文为按值调用 λ-演算建立可组合的时间代价模型。作者基于博弈语义的自然表示，将项指称的有限逼近（求值树）的代价定义为该逼近在语义中最小推导的大小。该度量具有最优性，可组合地推理代价界：从 C[A] 计算 c 的代价不超过从 A 计算 a 再在 C[a] 中计算 c 的代价。尽管底层语义非确定，作者给出确定性算法识别求值树逼近，并在随机存取机上以常数因子开销满足该模型。为满足完全惰性，作者提出无名显式替换的新型图归约，并通过一系列线性代价归约编译 λv-演算。
We describe a (time) cost model for the (call-by-value) λ-calculus based on a natural presentation of its game semantics: the cost of computing a finite approximant to the denotation of a term (its evaluation tree) is the size of its smallest derivation in the semantics. This measure has an optimality property enabling compositional reasoning about cost bounds: for any term A, context C[_] and approximants a and c to the trees of A and C[A], the cost of computing c from C[A] is no more than the cost of computing a from A and c from C[a].Although the natural semantics on which it is based is nondeterministic, our cost model is reasonable: we describe a deterministic algorithm for recognizing evaluation tree approximants which satisfies it (up to a constant factor overhead) on a Random Access Machine. This requires an implementation of the λv-calculus on the RAM which is completely lazy: compositionality of costs entails that work done to evaluate any part of a term cannot be duplicated. This is achieved by a novel implementation of graph reduction for nameless explicit substitutions, to which we compile the λv-calculus via a series of linear cost reductions.