Synthesizing Accumulative Functions Via Program Transformation
摘要
Accumulative functions, such as tail-recursive functions, employ accumulation parameters to carry and update the intermediate results. Despite their ubiquity and importance for efficient implementations, the automatic synthesis of accumulative functions remains challenging. The presence of accumulative parameters not only expands the search space but also unfastens the input-output examples from the traces of recursive calls, leading existing program synthesis methods to either fail in generating nontrivial accumulative functions or rely on pre-provided skeletons of recursive calls with accumulations. In this paper, we investigate an alternative approach to synthesizing accumulative functions. Our strategy integrates an off-the-shelf synthesizer, which may not inherently produce accumulative functions, and a program transformation that derives accumulative functions from non-accumulative ones. We specifically focus on the transformation introduced by Kühnemann et al. (RTA 2001), which effectively derives accumulative functions if the non-accumulative ones consist of substitution operators. By guiding the synthesizer to use substitution operators, we aim to obtain functions suitable for the transformation. We demonstrate the ability of our approach with examples from existing benchmarks.