论文标题
按价值划分的抽象机器用于强烈呼叫
An Abstract Machine for Strong Call by Value
论文作者
论文摘要
我们提出了一台抽象机器，该机器实现了纯$λ$ -calculus的全面还原（又称强）呼叫策略。它是使用Danvy等人的功能对应来得出的：（1）将KN解析为类似于Filinski和Rohde's的呼叫呼叫归一化功能，（2）修改所得的归一化器，以使其实现合理的呼叫式呼叫效果，以使其实现型逐渐构造的操作和（3）机器。 这台新机器实现了一种还原策略，该策略涵盖了Accattoli等人研究的值的火球校准变体。我们用基于Biernacka等人的广义重新聚焦的方法来描述机器的强大策略，并使用一种方法证明了机器的正确性。作为副产品，我们通过根据其部分归一化的形式来区分机器来检查计算机的示例应用程序。
We present an abstract machine that implements a full-reducing (a.k.a. strong) call-by-value strategy for pure $λ$-calculus. It is derived using Danvy et al.'s functional correspondence from Crégut's KN by: (1) deconstructing KN to a call-by-name normalization-by-evaluation function akin to Filinski and Rohde's, (2) modifying the resulting normalizer so that it implements the right-to-left call-by-value function application, and (3) constructing the functionally corresponding abstract machine. This new machine implements a reduction strategy that subsumes the fireball-calculus variant of call by value studied by Accattoli et al. We describe the strong strategy of the machine in terms of a reduction semantics and prove the correctness of the machine using a method based on Biernacka et al.'s generalized refocusing. As a byproduct, we present an example application of the machine to checking term convertibility by discriminating on the basis of their partially normalized forms.
