Program synthesis

In computer science, program synthesis is the task to construct a program that provably satisfies a given high-level formal specification. In contrast to program verification, the program is to be constructed rather than given; however, both fields make use of formal proof techniques, and both comprise approaches of different degrees of automatization. In contrast to automatic programming techniques, specifications in program synthesis are usually non-algorithmic statements in an appropriate logical calculus.

Origin

During the Summer Institute of Symbolic Logic at Cornell University in 1957, Alonzo Church defined the problem to synthesize a circuit from mathematical requirements. Even though the work only refers to circuits and not programs, the work is considered to be one of the earliest descriptions of program synthesis and some researchers refer to program synthesis as "Church's Problem". In the 1960s, a similar idea for an "automatic programmer" was explored by researchers in artificial intelligence.

Since then, various research communities considered the problem of program synthesis. Notable works include the 1969 automata-theoretic approach by Büchi and Landweber, and the works by Manna and Waldinger (c. 1980). The development of modern high-level programming languages can also be understood as a form of program synthesis.

21st century developments

The early 21st century has seen a surge of practical interest in the idea of program synthesis in the formal verification community and related fields. Armando Solar-Lezama showed that it is possible to encode program synthesis problems in Boolean logic and use algorithms for the Boolean satisfiability problem to automatically find programs. In 2013, a unified framework for program synthesis problems was proposed by researchers at UPenn, UC Berkeley, and MIT. Since 2014 there has been a yearly program synthesis competition comparing the different algorithms for program synthesis in a competitive event, the Syntax-Guided Synthesis Competition or SyGuS-Comp. Still, the available algorithms are only able to synthesize small programs.

The framework of Manna and Waldinger

Non-clausal resolution rules (unifying substitutions not shown)

Nr	Assertions	Goals	Program	Origin
51	$E[p]$
52	$F[p]$
53		$G[p]$	s
54		$H[p]$	t
55	$E[{\text{true}}]\lor F[{\text{false}}]$			Resolve(51,52)
56		$\lnot F[{\text{true}}]\land G[{\text{false}}]$	s	Resolve(52,53)
57		$\lnot F[{\text{false}}]\land G[{\text{true}}]$	s	Resolve(53,52)
58		$G[{\text{true}}]\land H[{\text{false}}]$	p ? s : t	Resolve(53,54)

The framework of Manna and Waldinger, published in 1980, starts from a user-given first-order specification formula. For that formula, a proof is constructed, thereby also synthesizing a functional program from unifying substitutions.

The framework is presented in a table layout, the columns containing:

• A line number ("Nr") for reference purposes
• Formulas that already have been established, including axioms and preconditions, ("Assertions")
• Formulas still to be proven, including postconditions, ("Goals"),
• Terms denoting a valid output value ("Program")
• A justification for the current line ("Origin")

Initially, background knowledge, pre-conditions, and post-conditions are entered into the table. After that, appropriate proof rules are applied manually. The framework has been designed to enhance human readability of intermediate formulas: contrary to classical resolution, it does not require clausal normal form, but allows one to reason with formulas of arbitrary structure and containing any junctors ("non-clausal resolution"). The proof is complete when ${\it {true}}$ has been derived in the Goals column, or, equivalently, ${\it {false}}$ in the Assertions column. Programs obtained by this approach are guaranteed to satisfy the specification formula started from; in this sense they are correct by construction. Only a minimalist, yet Turing-complete, functional programming language, consisting of conditional, recursion, and arithmetic and other operators is supported. Case studies performed within this framework synthesized algorithms to compute e.g. division, remainder, square root, term unification, answers to relational database queries and several sorting algorithms.

Proof rules

Proof rules include:

• Non-clausal resolution (see table).

For example, line 55 is obtained by resolving Assertion formulas $E$ from 51 and $F$ from 52 which both share some common subformula $p$. The resolvent is formed as the disjunction of $E$, with $p$ replaced by ${\it {true}}$, and $F$, with $p$ replaced by ${\it {false}}$. This resolvent logically follows from the conjunction of $E$ and $F$. More generally, $E$ and $F$ need to have only two unifiable subformulas $p_{1}$ and $p_{2}$, respectively; their resolvent is then formed from $E\theta$ and $F\theta$ as before, where $\theta$ is the most general unifier of $p_{1}$ and $p_{2}$. This rule generalizes resolution of clauses.

Program terms of parent formulas are combined as shown in line 58 to form the output of the resolvent. In the general case, $\theta$ is applied to the latter also. Since the subformula $p$ appears in the output, care must be taken to resolve only on subformulas corresponding to computable properties.

• Logical transformations.

For example, $E\land (F\lor G)$ can be transformed to $(E\land F)\lor (E\land G)$) in Assertions as well as in Goals, since both are equivalent.

• Splitting of conjunctive assertions and of disjunctive goals.

An example is shown in lines 11 to 13 of the toy example below.

• Structural induction.

This rule allows for synthesis of recursive functions. For a given pre- and postcondition "Given $x$ such that ${\textit {pre}}(x)$, find $f(x)=y$ such that ${\textit {post}}(x,y)$", and an appropriate user-given well-ordering $\prec$ of the domain of $x$, it is always sound to add an Assertion "$x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))$". Resolving with this assertion can introduce a recursive call to $f$ in the Program term.

An example is given in Manna, Waldinger (1980), p.108-111, where an algorithm to compute quotient and remainder of two given integers is synthesized, using the well-order $(n',d')\prec (n,d)$ defined by $0\leq n'<n$ (p.110).

Murray has shown these rules to be complete for first-order logic. In 1986, Manna and Waldinger added generalized E-resolution and paramodulation rules to handle also equality; later, these rules turned out to be incomplete (but nevertheless sound).

See also

• Inductive programming
• Metaprogramming
• Program derivation
• Natural language programming
• Reactive synthesis

References

• Zohar Manna, Richard Waldinger (1975). "Knowledge and Reasoning in Program Synthesis". Artificial Intelligence. 6 (2): 175–208. doi:10.1016/0004-3702(75)90008-9.