一句话：在统一框架中比较四种抽象机，并用非幂等交类型证明交互抽象机的时间低效源于高阶类型。
这篇论文研究基于交互几何的抽象机在求值高阶函数式程序时的时间效率问题。此类抽象机以空间高效著称，但时间性能常逊于传统的环境式抽象机；已有工作构造出使其指数级变慢的 λ 项族，然而这种低效的普遍性与最坏情况尚不清楚。作者将四种著名抽象机置于统一的定义框架中，精确比较它们的相对时间效率，并用非幂等交类型理论刻画交互抽象机的运行时间。结果表明非幂等交类型能够精确反映该抽象机的时间性能，从而说明其时间低效最终源于高阶类型的存在。
Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce space efficiencies, the price being time performances often poorer than those obtainable with traditional, environment-based, abstract machines. Although families of lambda-terms for which the former is exponentially less efficient than the latter do exist, it is currently unknown how general this phenomenon is, and how far the inefficiencies can go, in the worst case. We answer these questions formulating four different well-known abstract machines inside a common definitional framework, this way being able to give sharp results about the relative time efficiencies. We also prove that non-idempotent intersection type theories are able to precisely reflect the time performances of the interactive abstract machine, this way showing that its time-inefficiency ultimately descends from the presence of higher-order types.
@article{paperbot1167,
title = {The (In)Efficiency of interaction},
author = {Beniamino Accattoli and Ugo Dal Lago and Gabriele Vanoni},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434332}
}