一句话：提出结合令牌传递与图重写的动态 GoI 抽象机，统一实现并分析多种 lambda 求值策略的时空效率。
实现 lambda 演算求值策略时，正确性与效率（尤其空间与时间的权衡）都需考虑。本文受 Girard 的交互几何（GoI）启发，提出一种结合令牌传递与图重写的抽象机——动态 GoI 机（DGoIM），为研究该权衡提供统一框架。作者证明 DGoIM 相对于 call-by-need、从左到右 call-by-value 和从右到左 call-by-value 三种求值策略具有可靠性与完备性，并分析其执行时间成本，按 Accattoli 的抽象机分类将其归为“高效”机器。
In implementing evaluation strategies of the lambda-calculus, both correctness and efficiency of implementation are valid concerns. While the notion of correctness is determined by the evaluation strategy, regarding efficiency there is a larger design space that can be explored, in particular the trade-off between space versus time efficiency. Aiming at a unified framework that would enable the study of this trade-off, we introduce an abstract machine, inspired by Girard's Geometry of Interaction (GoI), a machine combining token passing and graph rewriting. We show soundness and completeness of our abstract machine, called the \emph{Dynamic GoI Machine} (DGoIM), with respect to three evaluations: call-by-need, left-to-right call-by-value, and right-to-left call-by-value. Analysing time cost of its execution classifies the machine as ``efficient'' in Accattoli's taxonomy of abstract machines.Comment: arXiv admin note: text overlap with arXiv:1802.06495
@article{paperbot745,
title = {The Dynamic Geometry of Interaction Machine: A Token-Guided Graph Rewriter},
author = {Koko Muroya and Dan R. Ghica},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 4},
year = {2019},
doi = {10.23638/lmcs-15(4:7)2019}
}