2024/05/27 by Jinwoo Kim, Kim, Jinwoo
Computer Science · Engineering · #Computational Complexity (cs.CC) #Experimental Learning in Engineering #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Numerical Methods and Algorithms #Programming Languages (cs.PL) #Teaching and Learning Programming
paper · pdf · doi:10.48550/arxiv.2405.16997
openalex publication_date 2024/05/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 Σ30-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 Σ30-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.