Distilling abstract machines
Distilling abstract machines
复制标题
提炼抽象机器
DOI：
10.1145/2692915.2628154
复制
发表时间：
2014
影响因子：
--
通讯作者：
Damiano Mazza
中科院分区：
文献类型：
--
作者：
Beniamino Accattoli;Pablo Barenbaum;Damiano Mazza
众所周知，许多基于环境的抽象机器可以被视为具有显式替换（ES）的lambda演算中的策略。最近，图形语法和线性逻辑导致了线性替换演算（LSC），这是一种新的ES方法，介于小步演算和传统演算之间。本文研究了LSC与基于环境的抽象机之间的关系。虽然传统的演算与ES模拟抽象的机器，而LSC提炼它们：一些转换被模拟，而其他消失，因为它们映射到一个概念的结构一致性。蒸馏过程揭示了抽象机器实际上实现了弱线性头归约，这是一个在线性逻辑理论中起核心作用的评估概念。我们表明，这样的模式适用于统一的名称调用，调用的值，和调用的需要，在文献中捕获许多机器。我们首先提取KAM、CEK和ZINC的草图，然后提供简化版本的SECD、懒惰的KAM和Sestoft的机器。沿着的方式，我们还介绍了一些新的机器与全球环境。此外，我们表明，蒸馏保留的时间复杂度的执行，即LSC是一个复杂性保持抽象机的抽象。
It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ES that is halfway between small-step calculi and traditional calculi with ES. This paper studies the relationship between the LSC and environment-based abstract machines. While traditional calculi with ES simulate abstract machines, the LSC rather distills them: some transitions are simulated while others vanish, as they map to a notion of structural congruence. The distillation process unveils that abstract machines in fact implement weak linear head reduction, a notion of evaluation having a central role in the theory of linear logic. We show that such a pattern applies uniformly in call-by-name, call-by-value, and call-by-need, catching many machines in the literature. We start by distilling the KAM, the CEK, and a sketch of the ZINC, and then provide simplified versions of the SECD, the lazy KAM, and Sestoft's machine. Along the way we also introduce some new machines with global environments. Moreover, we show that distillation preserves the time complexity of the executions, i.e. the LSC is a complexity-preserving abstraction of abstract machines.