Recently, Miller and Wu introduced the positive $\lambda$-calculus, a call-by-value $\lambda$-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for minimal intuitionistic logic. The positive $\lambda$-calculus stands out among $\lambda$-calculi with sharing for a compactness property related to the sharing of variables. We show that -- thanks to compactness -- the positive calculus neatly captures the core of useful sharing, a technique for the study of reasonable time cost models.

翻译：最近，Miller和Wu提出了正向λ演算，这是一种通过为极小直觉主义逻辑的正向极化聚焦证明分配证明项而得到的具有共享特性的按值调用λ演算。正向λ演算在具有共享特性的λ演算中因其与变量共享相关的紧致性而显得尤为突出。我们证明——得益于紧致性——正向演算能够简洁地捕捉有用共享技术的核心，该技术是研究合理时间成本模型的重要方法。