一句话：将记忆化算法合成分解为局部目标函数与记忆化划分函数两个子任务，并联合演绎与归纳方法实现高效合成。
论文研究如何从声明式规约自动合成正确且高效的记忆化算法。该问题有两个挑战：记忆化算法规模过大，传统合成器难以处理；同时必须保证效率。作者将合成过程结构化，引入局部目标函数与记忆化划分函数，把任务归约为两个较小且独立的程序合成任务，并将效率目标转化为最小化第二个任务所合成函数的不同输出值数量。针对归约后仍复杂的问题，提出结合演绎与归纳的新合成算法。作者从 LeetCode、全国信息学奥林匹克省级联赛（Junior）及已有方法中收集 42 个真实基准，在合理时间内成功合成 39/42 个问题，优于基线。
In this paper, we propose an automated approach to finding correct and efficient memoization algorithms from a given declarative specification. This problem has two major challenges: (i) a memoization algorithm is too large to be handled by conventional program synthesizers; (ii) we need to guarantee the efficiency of the memoization algorithm. To address this challenge, we structure the synthesis of memoization algorithms by introducing the local objective function and the memoization partition function and reduce the synthesis task to two smaller independent program synthesis tasks. Moreover, the number of distinct outputs of the function synthesized in the second synthesis task also decides the efficiency of the synthesized memoization algorithm, and we only need to minimize the number of different output values of the synthesized function. However, the generated synthesis task is still too complex for existing synthesizers. Thus, we propose a novel synthesis algorithm that combines the deductive and inductive methods to solve these tasks. To evaluate our algorithm, we collect 42 real-world benchmarks from Leetcode, the National Olympiad in Informatics in Provinces-Junior (a national-wide algorithmic programming contest in China), and previous approaches. Our approach successfully synhesizes 39/42 problems in a reasonable time, outperforming the baselines.
@article{paperbot1887,
title = {Synthesizing Efficient Memoization Algorithms},
author = {Yican Sun and Xuanyu Peng and Yingfei Xiong},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622800}
}