Return
Synthesizing Accumulative Functions Via Program Transformation
DOI:10.1007/978-3-031-99751-8_15.png)
Abstract
En 中文
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 preprovided 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 Kuhnemann 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.
Keywords:
Program synthesis
Accumulative function
Program transformation
Journal
T
IF:
0
Papers:
20
Citations:
0

