动态交互几何机：一种按需调用图重写器

Girard 的交互几何（GoI）是为线性逻辑证明设计的一种语义，也已成功应用于编程语言语义。一种方法是使用抽象机，在固定图上沿 GoI 指示的路径传递令牌（token）。这些传令牌抽象机是空间高效的，因为它们通过在固定图上重复令牌的相同移动来处理重复计算。尽管它们可以被调整以获得关于 λ 演算各种求值策略等式理论的可靠模型，但这可能以显著的时间代价为成本。在本文中，我们展示了一种传令牌抽象机，能够以经认证的时间效率实现 λ 演算的求值策略。我们的抽象机称为动态 GoI 机（DGoIM），重写图以避免复制计算，使用令牌来查找可约项（redexes）。交错令牌转移与图重写的灵活性使 DGoIM 能够平衡空间与时间代价的权衡。本文表明，DGoIM 可通过使用尽可能交错令牌传递与图重写的策略，实现 λ 演算的按需调用（call-by-need）求值。我们的定量分析确认，采用这种交错两类可能图操作策略的 DGoIM，按照 Accattoli 的抽象机分类法可被归类为“高效”。