Program Synthesis is $\Sigma_3^0$-Complete

TL;DR

This paper proves that determining the existence of solutions in program synthesis for a Turing-complete language is highly computationally complex, specifically $\, ext{Sigma}_3^0$-complete, and provides a first-order logical characterization of this complexity.

Contribution

It establishes the $\, ext{Sigma}_3^0$-completeness of program synthesis and introduces a first-order formula encoding for synthesis problems, including variants with finite examples.

Findings

Program synthesis for IMP is $\, ext{Sigma}_3^0$-complete.

Constructive encoding of synthesis as a first-order formula in arithmetic.

First-order characterization of synthesis problems and variants.

Abstract

This paper considers program synthesis in the context of computational hardness, asking the question: How hard is it to determine whether a given synthesis problem has a solution or not? To answer this question, this paper studies program synthesis for a basic imperative, Turing-complete language IMP, for which this paper proves that program synthesis is $\Sigma_3^0$-\emph{complete} in the arithmetical hierarchy. The proof of this fact relies on a fully constructive encoding of program synthesis (which is typically formulated as a second-order query) as a first-order formula in the standard model of arithmetic (i.e., Peano arithmetic). Constructing such a formula then allows us to reduce the decision problem for COF (the set of functions which diverge only on a finite set of inputs), which is well-known to be a $\Sigma_3^0$-complete problem, into the constructed first-order representation of synthesis. In addition to this main result, we also consider the hardness of variants of synthesis problems, such as those introduced in previous work to make program synthesis more tractable (e.g., synthesis over finite examples). To the best of our knowledge, this paper is the first to give a first-order characterization of program synthesis in general, and precisely define the computability of synthesis problems and their variants.