一句话：通过再函数化等语义变换，将小步抽象抽象机系统转化为大步抽象定义解释器，并揭示控制流分析中精确的调用/返回匹配。
抽象抽象机（AAM）是构造高阶语言可靠静态分析的系统方法，通过从具体求值的抽象机推导出执行抽象解释的小步 AAM；而单子抽象定义解释器（ADI）则在大步风格下做抽象解释。但小步 AAM 与大步 ADI 之间的关系尚不明确。本文解释两者的函数式对应，并展示如何系统地将小步 AAM 转换为大步 ADI。基于具体求值中已知的语义互推导技术，变换包括线性化、轻量融合、解缠、再函数化以及 CPS 变换的左逆。线性化用一阶数据类型表达非确定性选择，再函数化将表示续延的一阶数据类型变为高阶函数。再函数化后的 AAM 是一个带两层续延的 CPS 抽象解释器，可用定界控制算子转回直接风格；基于定界控制与单子的对应，表明 ADI 中显式使用单子是可选的。所有变换均正确处理收集语义和非确定性，并揭示通过带适当缓存的再函数化小步 AAM 可获得精确的调用/返回匹配。
Abstracting abstract machines is a systematic methodology for constructing sound static analyses for higher-order languages, by deriving small-step abstract abstract machines (AAMs) that perform abstract interpretation from abstract machines that perform concrete evaluation. Darais et al. apply the same underlying idea to monadic definitional interpreters, and obtain monadic abstract definitional interpreters (ADIs) that perform abstract interpretation in big-step style using monads. Yet, the relation between small-step abstract abstract machines and big-step abstract definitional interpreters is not well studied. In this paper, we explain their functional correspondence and demonstrate how to systematically transform small-step abstract abstract machines into big-step abstract definitional interpreters. Building on known semantic interderivation techniques from the concrete evaluation setting, the transformations include linearization, lightweight fusion, disentanglement, refunctionalization, and the left inverse of the CPS transform. Linearization expresses nondeterministic choice through first-order data types, after which refunctionalization transforms the first-order data types that represent continuations into higher-order functions. The refunctionalized AAM is an abstract interpreter written in continuation-passing style (CPS) with two layers of continuations, which can be converted back to direct style with delimited control operators. Based on the known correspondence between delimited control and monads, we demonstrate that the explicit use of monads in abstract definitional interpreters is optional. All transformations properly handle the collecting semantics and nondeterminism of abstract interpretation. Remarkably, we reveal how precise call/return matching in control-flow analysis can be obtained by refunctionalizing a small-step abstract abstract machine with proper caching.
@article{paperbot285,
title = {Refunctionalization of abstract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl)},
author = {Guannan Wei and James Decker and Tiark Rompf},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236800}
}