一句话：提出基于规范化等价的程序合成框架，将直接风格代码重构为使用库组合子的等价代码。
论文针对如何将不使用库组件的“直接风格”代码重构为使用库组件的“组合子风格”等价代码这一问题，提出基于组件的重构合成框架。其核心是“通过规范化实现等价”的判定技术：该技术可靠但不完备，不依赖输入输出示例或逻辑规约，并可复用已有编译器优化。作者在 Elm 的高阶函数组合子（如 map、filter）和 Python NumPy 的高性能数值组合子两个场景实例化框架，实现工具 Cobbler，并在数千个真实程序上评估执行时间与输出质量。结果表明，合成支持的重构可在不同领域应用，且除输入程序外无需额外规约。
We present an enumerative program synthesis framework called component-based refactoring that can refactor “direct” style code that does not use library components into equivalent “combinator” style code that does use library components. This framework introduces a sound but incomplete technique to check the equivalence of direct code and combinator code called equivalence by canonicalization that does not rely on input-output examples or logical specifications. Moreover, our approach can repurpose existing compiler optimizations, leveraging decades of research from the programming languages community. We instantiated our new synthesis framework in two contexts: (i) higher-order functional combinators such as map and filter in the staticallytyped functional programming language Elm and (ii) high-performance numerical computing combinators provided by the NumPy library for Python. We implemented both instantiations in a tool called Cobbler and evaluated it on thousands of real programs to test the performance of the component-based refactoring framework in terms of execution time and output quality. Our work offers evidence that synthesis-backed refactoring can apply across a range of domains without specification beyond the input program.
@article{paperbot2509,
title = {Equivalence by Canonicalization for Synthesis-Backed Refactoring},
author = {Justin Lubin and Jeremy Ferguson and Kevin Ye and Jacob Yim and Sarah E. Chasins},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656453}
}