Editing Program synthesis (section)

== The framework of Manna and Waldinger ==
{| class="wikitable" style="float:right;"
|+ Non-clausal resolution rules (unifying substitutions not shown)
|-
! Nr !! Assertions !! Goals !! Program !! Origin
|-
| 51 || <math>E[p]</math> || ||  ||
|-
| 52 || <math>F[p]</math> || ||  ||
|-
| 53 || || <math>G[p]</math> || s ||
|-
| 54 || || <math>H[p]</math> || t ||
|-
| 55 || <math>E[\text{true}] \lor F[\text{false}]</math>||  ||  || Resolve(51,52)
|-
| 56 || || <math>\lnot F[\text{true}] \land G[\text{false}]</math> ||  s || Resolve(52,53)
|-
| 57 || || <math>\lnot F[\text{false}] \land G[\text{true}]</math> ||  s  || Resolve(53,52)
|-
| 58 || || <math>G[\text{true}] \land H[\text{false}]</math> || p [[?:|?]] s [[?:|:]] t || Resolve(53,54)
|}

The framework of [[Zohar Manna|Manna]] and [[Richard Waldinger|Waldinger]], published in 1980,<ref>{{cite journal| author=Zohar Manna, Richard Waldinger| title=A Deductive Approach to Program Synthesis| journal=ACM Transactions on Programming Languages and Systems|date=Jan 1980| volume=2| pages=90–121| doi=10.1145/357084.357090| s2cid=14770735}}</ref><ref>{{cite report | url=https://apps.dtic.mil/dtic/tr/fulltext/u2/a065558.pdf| archive-url=https://web.archive.org/web/20210127052044/https://apps.dtic.mil/dtic/tr/fulltext/u2/a065558.pdf| url-status=live| archive-date=January 27, 2021<!---http://www.sri.com/sites/default/files/uploads/publications/pdf/725.pdf---> | author=Zohar Manna and Richard Waldinger | title=A Deductive Approach to Program Synthesis | institution=SRI International | type=Technical Note | number=177 | date=Dec 1978 }}</ref> starts from a user-given [[first-order logic|first-order specification formula]]. For that formula, a proof is constructed, thereby also synthesizing a [[functional program]] from [[unification (computer science)#Syntactic unification of first-order terms|unifying]] substitutions.

The framework is presented in a table layout, the columns containing:
* A line number ("Nr") for reference purposes
* [[Well-formed formula#Predicate logic|Formulas]] that already have been established, including axioms and preconditions, ("Assertions")
* Formulas still to be proven, including postconditions, ("Goals"),<ref group=note>The distinction "Assertions" / "Goals" is for convenience only; following the paradigm of [[proof by contradiction]], a Goal <math>F</math> is equivalent to an assertion <math> \lnot F</math>.</ref>
* [[term (logic)|Terms]] denoting a valid output value ("Program")<ref group=note>When <math>F</math> and <math>s</math> is the Goal formula and the Program term in a line, respectively, then in all cases where <math>F</math> holds, <math>s</math> is a valid output of the program to be synthesized. This [[invariant (computer science)|invariant]] is maintained by all proof rules. An Assertion formula usually is not associated with a Program term.</ref>
* 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 [[resolution (logic)|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 <math>\it true</math> has been derived in the ''Goals'' column, or, equivalently, <math>\it false</math> 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''.<ref>See Manna, Waldinger (1980), p.100 for correctness of the resolution rules.</ref> Only a minimalist, yet [[Turing-complete]],<ref>{{cite tech report |last1=Boyer |first1=Robert S. |last2=Moore |first2=J. Strother |title=A Mechanical Proof of the Turing Completeness of Pure Lisp |number=37 |institution=Institute for Computing Science, University of Texas at Austin |date=May 1983 |url=http://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp37.pdf |format=PDF |url-status=live |archive-date=22 September 2017 |archive-url=https://web.archive.org/web/20170922044624/http://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp37.pdf |df=dmy-all }}</ref> [[purely functional programming language]], consisting of conditional, recursion, and arithmetic and other operators<ref group=note>Only the conditional operator ([[?:]]) is supported from the beginning. However, arbitrary new operators and relations can be added by providing their properties as axioms. In the toy example below, only the properties of <math>=</math> and <math>\leq</math> that are actually needed in the proof have been axiomatized, in line 1 to 3.</ref> is supported.
Case studies performed within this framework synthesized algorithms to compute e.g. [[division algorithm|division]], [[remainder]],<ref>Manna, Waldinger (1980), p.108-111</ref> [[square root]],<ref>{{cite journal | author=Zohar Manna and Richard Waldinger | title=The Origin of a Binary-Search Paradigm | journal=Science of Computer Programming | volume=9 | number=1 | pages=37&ndash;83 | date=Aug 1987 | doi=10.1016/0167-6423(87)90025-6 | doi-access= }}</ref> [[Unification (computer science)|term unification]],<ref>{{cite journal | author=Daniele Nardi | title=Formal Synthesis of a Unification Algorithm by the Deductive-Tableau Method | journal=[[Journal of Logic Programming]] | volume=7 | pages=1&ndash;43 | year=1989 | doi=10.1016/0743-1066(89)90008-3 | doi-access= }}</ref> answers to [[relational database]] queries<ref>{{cite book | author=Daniele Nardi and Riccardo Rosati | contribution=Deductive Synthesis of Programs for Query Answering | editor=Kung-Kiu Lau and Tim Clement | title=International Workshop on Logic Program Synthesis and Transformation (LOPSTR) | publisher=Springer | series=Workshops in Computing | pages=15&ndash;29 | year=1992 | doi=10.1007/978-1-4471-3560-9_2 | isbn=978-3-540-19806-2 }}</ref> and several [[sorting algorithm]]s.<ref>{{cite book | author=Jonathan Traugott | contribution=Deductive Synthesis of Sorting Programs | title=Proceedings of the International Conference on Automated Deduction | publisher=Springer | series=[[LNCS]] | volume=230 | pages=641&ndash;660 | year=1986 }}</ref><ref>{{cite journal | author=Jonathan Traugott | title=Deductive Synthesis of Sorting Programs | journal=[[Journal of Symbolic Computation]] | volume=7 | number=6 | pages=533&ndash;572 | date=Jun 1989 | doi=10.1016/S0747-7171(89)80040-9 | doi-access= }}</ref>

===Proof rules===
Proof rules include:
*Non-clausal [[Resolution (logic)|resolution]] (see table).
:For example, line 55 is obtained by resolving Assertion formulas <math>E</math> from 51 and <math>F</math> from 52 which both share some common subformula <math>p</math>. The resolvent is formed as the disjunction of <math>E</math>, with <math>p</math> replaced by <math>\it true</math>, and <math>F</math>, with <math>p</math> replaced by <math>\it false</math>. This resolvent logically follows from the conjunction of <math>E</math> and <math>F</math>. More generally, <math>E</math> and <math>F</math> need to have only two unifiable subformulas <math>p_1</math> and <math>p_2</math>, respectively; their resolvent is then formed from <math>E \theta</math> and <math>F \theta</math> as before, where <math>\theta</math> is the [[most general unifier]] of <math>p_1</math> and <math>p_2</math>. This rule generalizes [[Resolution (logic)#Resolution in first order logic|resolution of clauses]].<ref>Manna, Waldinger (1980), p.99</ref>
:Program terms of parent formulas are combined as shown in line 58 to form the output of the resolvent. In the general case, <math>\theta</math> is applied to the latter also. Since the subformula <math>p</math> appears in the output, care must be taken to resolve only on subformulas corresponding to [[computable]] properties.
*Logical transformations.
:For example, <math>E \land (F \lor G)</math> can be transformed to <math>(E \land F) \lor (E \land G)</math>) 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 function (programming)|recursive functions]]. For a given pre- and postcondition "Given <math>x</math> such that <math>\textit{pre}(x)</math>, find <math>f(x) = y</math> such that <math>\textit{post}(x,y)</math>", and an appropriate user-given [[well-ordering]] <math>\prec</math> of the domain of <math>x</math>, it is always sound to add an Assertion "<math>x' \prec x \land \textit{pre}(x') \implies \textit{post}(x',f(x'))</math>".<ref>Manna, Waldinger (1980), p.104</ref> Resolving with this assertion can introduce a recursive call to <math>f</math> 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 <math>(n',d') \prec (n,d)</math> defined by <math>0 \leq n' < n</math> (p.110).

Murray has shown these rules to be [[Completeness (logic)|complete]] for [[first-order logic]].<ref>Manna, Waldinger (1980), p.103, referring to: {{cite tech report| author=Neil V. Murray| title=A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic|date=Feb 1979| number=2-79| institution=Syracuse Univ.| url=http://surface.syr.edu/cgi/viewcontent.cgi?article=1005&context=eecs_techreports}}</ref>
In 1986, Manna and Waldinger added generalized E-resolution and [[paramodulation]] rules to handle also equality;<ref>{{cite journal| author=Zohar Manna, Richard Waldinger| title=Special Relations in Automated Deduction| journal=Journal of the ACM| volume=33|date=Jan 1986| pages=1–59|doi=10.1145/4904.4905 | s2cid=15140138| doi-access=free}}</ref> later, these rules turned out to be incomplete (but nevertheless [[soundness|sound]]).<ref>{{cite book| author=Zohar Manna, Richard Waldinger| chapter=The Special-Relations Rules are Incomplete| title=Proc. CADE 11| year=1992| volume=607| pages=492–506| publisher=Springer| series=LNCS}}</ref>

{{clear}}

===Example===
{| class="wikitable" style="float:right;"
|+ Example synthesis of maximum function
|-
! Nr !! Assertions !! Goals !! Program !! Origin
|-
| 1 || <math>A=A</math> || ||  || Axiom
|-
| 2 || <math>A \leq A</math>  ||  || || Axiom
|-
| 3 || <math>A \leq B \lor B \leq A</math>  || ||  || Axiom
|-
| 10 || || <math>x \leq M \land y \leq M \land (x = M \lor y = M)</math> || M || Specification
|-
| 11 || || <math>(x \leq M \land y \leq M \land x = M) \lor (x \leq M \land y \leq M \land y = M)</math> || M || Distr(10)
|-
| 12 || || <math>x \leq M \land y \leq M \land x = M</math> || M || Split(11)
|-
| 13 || || <math>x \leq M \land y \leq M \land y = M</math> || M || Split(11)
|-
| 14 || || <math>x \leq x \land y \leq x</math> || x || Resolve(12,1)
|-
| 15 || || <math>y \leq x</math> || x || Resolve(14,2)
|-
| 16 || || <math>\lnot (x \leq y)</math> || x || Resolve(15,3)
|-
| 17 || || <math>x \leq y \land y \leq y</math> || y || Resolve(13,1)
|-
| 18 || || <math>x \leq y</math> || y || Resolve(17,2)
|-
| 19 || || <math>\textit{true}</math> || x<y [[?:|?]] y [[?:|:]] x || Resolve(18,16)
|}
As a toy example, a functional program to compute the maximum <math>M</math> of two numbers <math>x</math> and <math>y</math> can be derived as follows.{{citation needed|date=May 2016}}

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 <math>\forall X \forall Y \exists M: X \leq M \land Y \leq M \land (X=M \lor Y=M)</math> is obtained as its formal translation. This formula is to be proved. By reverse [[Skolemization]],<ref group=note>While ordinary Skolemization preserves satisfiability, reverse Skolemization, i.e. replacing universally quantified variables by functions, preserves validity.</ref> 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 [[Substitution (logic)#First-order logic|instantiation]] of the program variable <math>M</math> in line 14. Intuitively, the last conjunct of line 12 prescribes the value that <math>M</math> must take in this case. Formally, the non-clausal resolution rule shown in line 57 above is applied to lines 12 and 1, with <!---Using {{math}} here to make the color template work--->
* {{color|#008000|{{math|p}}}} being the common instance {{color|#008000|{{math|1=x=x}}}} of {{color|#408000|{{math|1=A=A}}}} and {{color|#008040|{{math|1=x=M}}}}, obtained by syntactically [[unification (computer science)#Syntactic unification of first-order terms|unifying]] the latter formulas,
* {{color|#800000|{{math|F[}}}}{{color|#008000|{{math|p}}}}{{color|#800000|{{math|]}}}} being {{color|#800000|{{math|''true'' ∧ }}}}{{color|#008000|{{math|1=x=x}}}}, obtained from [[Substitution (logic)#First-order logic|instantiated]] line 1 (appropriately padded to make the context {{color|#800000|{{math|F[⋅]}}}} around {{color|#008000|{{math|p}}}} visible), and 
* {{color|#000080|{{math|G[}}}}{{color|#008000|{{math|p}}}}{{color|#000080|{{math|]}}}} being {{color|#000080|{{math|x ≤ x ∧ y ≤ x ∧ }}}}{{color|#008000|{{math|1=x = x}}}}, obtained from instantiated line 12,
yielding
<math>\lnot (</math>{{color|#800000|{{math|''true'' ∧ }}}}{{color|#008000|{{math|''false''}}}}{{math|) ∧ (}}{{color|#000080|{{math|x ≤ x ∧ y ≤ x ∧ }}}}{{color|#008000|{{math|''true''}}}}<math>)</math>,
which simplifies to <math>x \leq x \land y \leq x</math>.

In a similar way, line 14 yields line 15 and then line 16 by resolution. Also, the second case, <math>x \leq M \land y \leq M \land y = M</math> 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&rarr;16 was needed. Intuitively, line 18 could be read as "in case <math>x \leq y</math>, the output <math>y</math> is valid (with respect to the original specification), while line 15 says "in case <math>y \leq x</math>, the output <math>x</math> is valid; the step 15&rarr;16 established that both cases 16 and 18 are complementary.<ref group=note>Axiom 3 was needed for that; in fact, if <math>\leq</math> wasn't a [[total order]], no maximum could be computed for uncomparable inputs <math>x,y</math>.</ref> Since both line 16 and 18 comes with a program term, a [[?:|conditional expression]] results in the program column. Since the goal formula <math>\textit{true}</math> has been derived, the proof is done, and the program column of the "<math>\textit{true}</math>" line contains the program.