Synthesizing Recursive Functional Programs via Structure-Element Separation

Abstract

Synthesizing recursive functional programs over algebraic data types from input-output examples remains challenging, largely due to the explosion of structurally distinct candidates during search. We present a synthesis approach for structurally recursive list/tree transformations based on a structure-element separation viewpoint: a structure transformation that determines output shape, and element computations that determine the values placed into that shape. Our method first infers structural relationships from examples that describe per-step output-size evolution along recursive calls and uses them to prune partial programs during top-down enumeration. For candidates that are structurally feasible, we apply a diamond function that converts the remaining element-level holes into small local program-by-example subproblems, which are then solved using symbolic execution and output alignment, enabling early acceptance or rejection without expanding unrelated global constructs. We implement the approach in an OCaml prototype synthesizer and evaluate it on a suite of list and tree benchmarks drawn from prior work. The results show that our method substantially reduces expensive example checking and improves synthesis performance on recursive list/tree transformation programs.