arrow
Return

Synthesizing Accumulative Functions Via Program Transformation

delete2026-01-01
delete0
PRE
AI
L
Lin, Junyu *
A
Akimasa Morihata
DOI:10.1007/978-3-031-99751-8_15delete
deleteOriginal
deleteOriginal request for help
deleteShare
deleteSave
Abstract

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
TRENDS IN FUNCTIONAL PROGRAMMING, TFP 2025
IF:
0
Papers:
20
Citations:
0

Organization

U
university of tokyo
Scholars:
6.3K
Papers: 2.5K
Citations: 1