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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Synthesizing Accumulative Functions Via Program Transformation

  • Junyu Lin,
  • Akimasa Morihata

摘要

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.