提纯抽象机（长版）
编程语言
2014-06-11 v1
摘要
众所周知，许多基于环境的抽象机可以被视为带有显式替换（ES）的 lambda 演算中的策略。最近，图语法和线性逻辑引出了线性替换演算（LSC），这是一种介于大步演算和传统带 ES 演算之间的新 ES 方法。本文研究了 LSC 与基于环境的抽象机之间的关系。传统的带 ES 演算模拟抽象机，而 LSC 则是提纯它们：部分转换被模拟，而其他转换则消失，因为它们映射到结构同余的概念。提纯过程揭示了抽象机实际上实现了弱线性归约，这是一种在线性逻辑理论中占据核心地位的求值概念。我们表明这种模式统一适用于传名调用、传值调用和按需调用，涵盖了文献中的许多机器。我们首先提纯 KAM、CEK 和 ZINC，然后提供 SECD、惰性 KAM 和 Sestoft 机的简化版本。在此过程中，我们还引入了一些带有全局环境的新机器。此外，我们表明提纯保持了执行的时间复杂度，即 LSC 是抽象机的保复杂度抽象。
引用
@article{arxiv.1406.2370,
title = {Distilling Abstract Machines (Long Version)},
author = {Beniamino Accattoli and Pablo Barenbaum and Damiano Mazza},
journal= {arXiv preprint arXiv:1406.2370},
year = {2014}
}
备注
63 pages