论文标题
相互作用的（IN）效率
The (In)Efficiency of Interaction
论文作者
论文摘要
已知通过相互作用的几何形状启发的抽象机器评估高阶功能程序，这诱发了$ \ textit {space} $效率，价格为$ \ textit {time} $表现通常比传统，基于环境的抽象机器可获得的价格差。尽管前者的lambda-terms家族的效率比后者的效率较低，但目前尚不清楚这种现象是如何\ emph {一般}，以及在最坏的情况下，效率低下的效率能走多远。我们回答了这些问题，在一个常见的定义性框架内提出了四台不同的众所周知的抽象机器，这样就可以对相对时间效率产生明显的结果。我们还证明，非数字相交类型的理论能够准确反映交互式抽象机器的时间性能，这种方式表明其时间友好率最终从高阶类型的存在中降下。
Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce $\textit{space}$ efficiencies, the price being $\textit{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 \emph{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.
