一句话：提出 superfusion，用归纳程序合成消除函数式程序中的中间数据结构，并以 ghost 函数分解草图填充问题。
中间数据结构是函数式程序低效的常见原因，传统 fusion 依赖预定义重写规则，表达力受限。本文探索基于归纳程序合成的新途径——superfusion：从标注了待消除数据结构的参考程序出发，先生成把操作这些结构的片段替换为洞的 sketch，再用常数时间表达式填充洞，使结果程序与参考程序等价。核心技术挑战是可扩展性：优化后的程序往往复杂，朴素枚举的搜索空间过大。作者的关键洞见是先合成一个 ghost 函数，刻画原中间数据结构与其压缩版本之间的关系；该函数虽不出现在最终程序中，却能把联合的草图填充问题分解为每个洞各自独立的简单子问题。作者实现工具 SuFu，并在源自演绎融合与程序重构先前工作的 290 个任务上评估，结果显示 SuFu 解决了其中 264 个任务，超越了基于重写的 fusion 系统，并在各自领域达到与专用程序重构方法相当的性能。
Intermediate data structures are a common cause of inefficiency in functional programming. Fusion attempts to eliminate intermediate data structures by combining adjacent data traversals into one; existing fusion techniques, however, are based on predefined rewrite rules and hence are limited in expressiveness. In this work we explore a different approach to eliminating intermediate data structures, based on inductive program synthesis. We dub this approach superfusion (by analogy with superoptimization , which uses inductive synthesis for program optimization). Starting from a reference program annotated with data structures to be eliminated, superfusion first generates a sketch where program fragments operating on those data structures are replaced with holes; it then fills the holes with constant-time expressions such that the resulting program is equivalent to the reference. The main technical challenge here is scalability because optimized programs are often complex, making the search space intractably large for naive enumeration. To address this challenge, our key insight is to first synthesize a ghost function that describes the relationship between the original intermediate data structure and its compressed version; this function, although not used in the final program, serves to decompose the joint sketch filling problem into independent simpler problems for each hole. We implement superfusion in a tool called SuFu and evaluate it on a dataset of 290 tasks collected from prior work on deductive fusion and program restructuring. The results show that SuFu solves 264 out of 290 tasks, exceeding the capabilities of rewriting-based fusion systems and achieving comparable performance with specialized approaches to program restructuring on their respective domains.
@article{JiZPXH24,
title = {Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis},
author = {Ruyi Ji and Yuwei Zhao and Nadia Polikarpova and Yingfei Xiong and Zhenjiang Hu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656415}
}