We propose $$SE^2GIS$$, a novel inductive recursion synthesis approach with the ability to both synthesize code and declare the problem unsolvable. $$SE^2GIS$$ combines a symbolic variant of counterexample-guided inductive synthesis (CEGIS) with a new dual inductive procedure, which focuses on proving a synthesis problem unsolvable rather than finding a solution for it. A vital component of this procedure is a new algorithm with the capability of producing a witness, a set of concrete assignments to relevant variables, as a proof that the synthesis instance is not solvable. Witnesses in the dual inductive procedure play the same role that solutions do in classic CEGIS; that is, they ensure progress. Given a reference function, invariants on the input recursive data types and a target family of recursive functions, $$SE^2GIS$$ synthesizes an implementation in this family that is equivalent to the reference implementation, or declares the problem unsolvable and produces a witness for it. We demonstrate that $$SE^2GIS$$ is effective in both cases; that is, for interesting data types with complex invariants, it can synthesize non-trivial recursive functions or output witnesses that contain useful feedback for the user.

The Appendix referred to in the submission has been submitted as anonymized Supplemental Text.