Program synthesis

Proof rules include:

• Non-clausal resolution (see table).

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

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

• Logical transformations.

For example, ${\displaystyle E\land (F\lor G)}$ can be transformed to ${\displaystyle (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 ${\displaystyle x}$ such that ${\displaystyle {\textit {pre}}(x)}$, find ${\displaystyle f(x)=y}$ such that ${\displaystyle {\textit {post}}(x,y)}$", and an appropriate user-given well-ordering ${\displaystyle \prec }$ of the domain of ${\displaystyle x}$, it is always sound to add an Assertion "${\displaystyle x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))}$".[18] Resolving with this assertion can introduce a recursive call to ${\displaystyle 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 ${\displaystyle (n',d')\prec (n,d)}$ defined by ${\displaystyle 0\leq n'<n}$ (p.110).

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

Example synthesis of maximum function

Nr	Assertions	Goals	Program	Origin
1	${\displaystyle A=A}$			Axiom
2	${\displaystyle A\leq A}$			Axiom
3	${\displaystyle A\leq B\lor B\leq A}$			Axiom
10		${\displaystyle x\leq M\land y\leq M\land (x=M\lor y=M)}$	M	Specification
11		${\displaystyle (x\leq M\land y\leq M\land x=M)\lor (x\leq M\land y\leq M\land y=M)}$	M	Distr(10)
12		${\displaystyle x\leq M\land y\leq M\land x=M}$	M	Split(11)
13		${\displaystyle x\leq M\land y\leq M\land y=M}$	M	Split(11)
14		${\displaystyle x\leq x\land y\leq x}$	x	Resolve(12,1)
15		${\displaystyle y\leq x}$	x	Resolve(14,2)
16		${\displaystyle \lnot (x\leq y)}$	x	Resolve(15,3)
17		${\displaystyle x\leq y\land y\leq y}$	y	Resolve(13,1)
18		${\displaystyle x\leq y}$	y	Resolve(17,2)
19		${\displaystyle {\textit {true}}}$	x<y ? y : x	Resolve(18,16)

As a toy example, a functional program to compute the maximum ${\displaystyle M}$ of two numbers ${\displaystyle x}$ and ${\displaystyle y}$ can be derived as follows.

Starting from the requirement description "The maximum is larger than or equal to any given number, and is one of the given numbers", the first-order formula ${\displaystyle \forall X\forall Y\exists M:X\leq M\land Y\leq M\land (X=M\lor Y=M)}$ is obtained as its formal translation. This formula is to be proved. By reverse Skolemization,[note 4] the specification in line 10 is obtained, an upper- and lower-case letter denoting a variable and a Skolem constant, respectively.

After applying a transformation rule for the distributive law in line 11, the proof goal is a disjunction, and hence can be split into two cases, viz. lines 12 and 13.

Turning to the first case, resolving line 12 with the axiom in line 1 leads to instantiation of the program variable ${\displaystyle M}$ in line 14. Intuitively, the last conjunct of line 12 prescribes the value that ${\displaystyle M}$ must take in this case. Formally, the non-clausal resolution rule shown in line 57 above is applied to lines 12 and 1, with

• p being the common instance x=x of A=A and x=M, obtained by syntactically unifying the latter formulas,
• F[p] being true ∧ x=x, obtained from instantiated line 1 (appropriately padded to make the context F[⋅] around p visible), and
• G[p] being x ≤ x ∧ y ≤ x ∧ x = x, obtained from instantiated line 12,

yielding ${\displaystyle \lnot (}$true ∧ false) ∧ (x ≤ x ∧ y ≤ x ∧ true${\displaystyle )}$, which simplifies to ${\displaystyle x\leq x\land y\leq x}$.

In a similar way, line 14 yields line 15 and then line 16 by resolution. Also, the second case, ${\displaystyle x\leq M\land y\leq M\land y=M}$ in line 13, is handled similarly, yielding eventually line 18.

In a last step, both cases (i.e. lines 16 and 18) are joined, using the resolution rule from line 58; to make that rule applicable, the preparatory step 15→16 was needed. Intuitively, line 18 could be read as "in case ${\displaystyle x\leq y}$, the output ${\displaystyle y}$ is valid (with respect to the original specification), while line 15 says "in case ${\displaystyle y\leq x}$, the output ${\displaystyle x}$ is valid; the step 15→16 established that both cases 16 and 18 are complementary.[note 5] Since both line 16 and 18 comes with a program term, a conditional expression results in the program column. Since the goal formula ${\displaystyle {\textit {true}}}$ has been derived, the proof is done, and the program column of the "${\displaystyle {\textit {true}}}$" line contains the program.