Program synthesis
In
The primary application of program synthesis is to relieve the programmer of the burden of writing correct, efficient code that satisfies a specification. However, program synthesis also has applications to superoptimization and inference of loop invariants.[2]
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.[3] 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.[citation needed]
Since then, various research communities considered the problem of program synthesis. Notable works include the 1969 automata-theoretic approach by Büchi and Landweber,[4] 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
This section needs expansion with: a more detailed overview of contemporary approaches. You can help by adding to it. (December 2022) |
The early 21st century has seen a surge of practical interest in the idea of program synthesis in the
Syntax-guided synthesis
In 2013, a unified framework for program synthesis problems called Syntax-guided Synthesis (stylized SyGuS) was proposed by researchers at
(f(x,y) = x ∨ f(x,y) = y) ∧ f(x,y) ≥ x ∧ f(x,y) ≥ y
and the grammar might be:
<Exp> ::= x | y | 0 | 1 | <Exp> + <Exp> | ite(<Cond>, <Exp>, <Exp>)
<Cond> ::= <Exp> <= <Exp>
where "ite" stands for "if-then-else". The expression
ite(x <= y, y, x)
would be a valid solution, because it conforms to the grammar and the specification.
From 2014 through 2019, the yearly Syntax-Guided Synthesis Competition (or SyGuS-Comp) compared the different algorithms for program synthesis in a competitive event.
(set-logic LIA) (synth-fun f ((x Int) (y Int)) Int ((i Int) (c Int) (b Bool)) ((i Int (c x y (+ i i) (ite b i i))) (c Int (0 1)) (b Bool ((<= i i))))) (declare-var x Int) (declare-var y Int) (constraint (>= (f x y) x)) (constraint (>= (f x y) y)) (constraint (or (= (f x y) x) (= (f x y) y))) (check-synth)
A compliant solver might return the following output:
((define-fun f ((x Int) (y Int)) Int (ite (<= x y) y x)))
The framework of Manna and Waldinger
Nr | Assertions | Goals | Program | Origin |
---|---|---|---|---|
51 | ||||
52 | ||||
53 | s | |||
54 | t | |||
55 | Resolve(51,52) | |||
56 | s | Resolve(52,53) | ||
57 | s | Resolve(53,52) | ||
58 | p : t |
Resolve(53,54) |
The framework of
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"),[note 1]
- Terms denoting a valid output value ("Program")[note 2]
- 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
Proof rules
Proof rules include:
- Non-clausal resolution (see table).
- For example, line 55 is obtained by resolving Assertion formulas from 51 and from 52 which both share some common subformula . The resolvent is formed as the disjunction of , with replaced by , and , with replaced by . This resolvent logically follows from the conjunction of and . More generally, and need to have only two unifiable subformulas and , respectively; their resolvent is then formed from and as before, where is the most general unifierof and . This rule generalizes resolution of clauses.[19]
- Program terms of parent formulas are combined as shown in line 58 to form the output of the resolvent. In the general case, is applied to the latter also. Since the subformula appears in the output, care must be taken to resolve only on subformulas corresponding to computableproperties.
- Logical transformations.
- For example, can be transformed to ) 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.
- This rule allows for synthesis of recursive functions. For a given pre- and postcondition "Given such that , find such that ", and an appropriate user-givenwell-orderingof the domain of , it is always sound to add an Assertion "".[20] Resolving with this assertion can introduce a recursive call to 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 defined by (p.110).
Murray has shown these rules to be complete for first-order logic.[21] In 1986, Manna and Waldinger added generalized E-resolution and
Example
Nr | Assertions | Goals | Program | Origin |
---|---|---|---|---|
1 | Axiom | |||
2 | Axiom | |||
3 | Axiom | |||
10 | M | Specification | ||
11 | M | Distr(10) | ||
12 | M | Split(11) | ||
13 | M | Split(11) | ||
14 | x | Resolve(12,1) | ||
15 | x | Resolve(14,2) | ||
16 | x | Resolve(15,3) | ||
17 | y | Resolve(13,1) | ||
18 | y | Resolve(17,2) | ||
19 | x<y : x |
Resolve(18,16) |
As a toy example, a functional program to compute the maximum of two numbers and can be derived as follows.[citation needed]
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 is obtained as its formal translation. This formula is to be proved. By reverse
After applying a transformation rule for the
Turning to the first case, resolving line 12 with the axiom in line 1 leads to instantiation of the program variable in line 14. Intuitively, the last conjunct of line 12 prescribes the value that 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 true ∧ false) ∧ (x ≤ x ∧ y ≤ x ∧ true, which simplifies to .
In a similar way, line 14 yields line 15 and then line 16 by resolution. Also, the second case, 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 , the output is valid (with respect to the original specification), while line 15 says "in case , the output is valid; the step 15→16 established that both cases 16 and 18 are complementary.
See also
- Inductive programming
- Metaprogramming
- Program derivation
- Natural language programming
- Reactive synthesis
Notes
- ^ The distinction "Assertions" / "Goals" is for convenience only; following the paradigm of proof by contradiction, a Goal is equivalent to an assertion .
- ^ When and is the Goal formula and the Program term in a line, respectively, then in all cases where holds, is a valid output of the program to be synthesized. This invariantis maintained by all proof rules. An Assertion formula usually is not associated with a Program term.
- ?:) 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 and that are actually needed in the proof have been axiomatized, in line 1 to 3.
- ^ While ordinary Skolemization preserves satisfiability, reverse Skolemization, i.e. replacing universally quantified variables by functions, preserves validity.
- ^ Axiom 3 was needed for that; in fact, if wasn't a total order, no maximum could be computed for uncomparable inputs .
References
- CiteSeerX 10.1.1.62.4976.
- ^ (Alur, Singh & Fisman)
- ^ Alonzo Church (1957). "Applications of recursive arithmetic to the problem of circuit synthesis". Summaries of the Summer Institute of Symbolic Logic. 1: 3–50.
- JSTOR 1994916.
- ^ Solar-Lezama, Armando (2008). Program synthesis by sketching (PDF) (Ph.D.). University of California, Berkeley.
- ^ Alur, Rajeev; al., et (2013). "Syntax-guided Synthesis". Proceedings of Formal Methods in Computer-Aided Design. IEEE. p. 8.
- PMID 28871052.
- ^ SyGuS-Comp (Syntax-Guided Synthesis Competition)
- S2CID 14770735.
- ^ Zohar Manna and Richard Waldinger (Dec 1978). A Deductive Approach to Program Synthesis (PDF) (Technical Note). SRI International. Archived (PDF) from the original on January 27, 2021.
- ^ See Manna, Waldinger (1980), p.100 for correctness of the resolution rules.
- ^ Boyer, Robert S.; Moore, J. Strother (May 1983). A Mechanical Proof of the Turing Completeness of Pure Lisp (PDF) (Technical report). Institute for Computing Science, University of Texas at Austin. 37. Archived (PDF) from the original on 22 September 2017.
- ^ Manna, Waldinger (1980), p.108-111
- .
- .
- .
- LNCS. Vol. 230. Springer. pp. 641–660.
- .
- ^ Manna, Waldinger (1980), p.99
- ^ Manna, Waldinger (1980), p.104
- ^ Manna, Waldinger (1980), p.103, referring to: Neil V. Murray (Feb 1979). A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic (Technical report). Syracuse Univ. 2-79.
- S2CID 15140138.
- ^ Zohar Manna, Richard Waldinger (1992). "The Special-Relations Rules are Incomplete". Proc. CADE 11. LNCS. Vol. 607. Springer. pp. 492–506.
- Alur, Rajeev; Singh, Rishabh; Fisman, Dana; Solar-Lezama, Armando (2018-11-20). "Search-based program synthesis". Communications of the ACM. 61 (12): 84–93. ISSN 0001-0782.
- Zohar Manna, Richard Waldinger (1975). "Knowledge and Reasoning in Program Synthesis". Artificial Intelligence. 6 (2): 175–208. .