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.
翻译:在互动几何学的启发下,人们知道通过抽象机器对更高层次功能程序进行评估会引致 $\ textit{space}$效率,价格是 $\ textit{time}$(time}$) 的效益往往比传统、基于环境的、抽象的机器获得的效益要差。 虽然前者效率指数指数低于后者的羊排术语家庭目前还不清楚这一现象是如何发生的,在最坏的情况下,效率低下的程度有多大。我们回答这些问题时,在共同的定义框架内形成四台不同的知名的抽象机器,从而能够对相对的时间效率产生尖锐的结果。我们也证明非精英的交叉类型理论能够准确反映交互式抽象机器的时间表现,这说明它的时间效率最终会从更高等级类型的存在中下降。