Talk:Program synthesis

Please discuss the merge at Talk:Automatic programming ---- CharlesGillingham 05:53, 26 August 2007 (UTC)

Rewrote the article (July 2017)

I am a postdoc at UC Berkeley working on program synthesis User:MarkusRabe. I tried to address some of the problems with the previous version of this article (vagueness, poor writing, missing references, sometimes even wrong statements). I rewrote the introduction, origin, and current developments and I deleted "Problems and limitations" as it used too specific technical terms, such as 'factoring' and was very vague.

From here on, the article should be extended by more detailed discussions on modern algorithms for program synthesis, for example FlashFill by Sumit Gulwani, enumerative program synthesis, component-based synthesis, and so on. The current section on Manna and Waldinger's work is okay, but their approach does not play a big role today. - 4 July 2017‎ User:MarkusRabe

I agree that the Manna+Waldinger section currently has undue weight; it got even longer due to (apparently necessary) additional explanations. I hope this problem will vanish if some people add new sections on other, in particular, more common, approaches. Maybe, we will have to split the article eventually. - Jochen Burghardt (talk) 12:09, 11 February 2019 (UTC)

Copyright problem removed

Prior content in this article duplicated one or more previously published sources. Copied or closely paraphrased material has been rewritten or removed and must not be restored, unless it is duly released under a compatible license. (For more information, please see "using copyrighted works from others" if you are not the copyright holder of this material, or "donating copyrighted materials" if you are.) For legal reasons, we cannot accept copyrighted text or images borrowed from other web sites or published material; such additions will be deleted. Contributors may use copyrighted publications as a source of information, but not as a source of sentences or phrases. Accordingly, the material may be rewritten, but only if it does not infringe on the copyright of the original or plagiarize from that source. Please see our guideline on non-free text for how to properly implement limited quotations of copyrighted text. Wikipedia takes copyright violations very seriously, and persistent violators will be blocked from editing. While we appreciate contributions, we must require all contributors to understand and comply with these policies. Thank you. Osiris (talk) 13:04, 7 July 2012 (UTC)

This page needs a complete rewrite

The current contents of this page describe the state of program synthesis prior to 2000 (the only citation is from a 2004 review paper looking back at the eras from 1960-2000).

I am postdoc at UC Berkeley with primary research focus on Program Synthesis. My PhD was on Program Synthesis as well. I am starting on a project to revamp this page to make it current with the developments in the field, and I will ensure that the updated page contains contributions from faculty and researchers at all prominent establishments (including Berkeley, MIT, Microsoft, etc.) working in the area. The end result will bring the page up to par with, for example, the Software testing page.

If any of the current contributors have significant objections to a rewrite, please respond. — Preceding unsigned comment added by Saurabh.berkeley (talk • contribs) 19:28, 23 April 2013 (UTC)

Other aspects of program synthesis

This page only considers program synthesis from formal specification,e.g., LTL or CTL temporal logic. The important topic of program synthesis from input/output examples is omitted. Currently, the later is more actively pursued and has been already transferred to the industry, e.g, MS Excel's FlashFill feature. I refer here to the recent and remarkable works of Sumit Gulwani of MSR. — Preceding unsigned comment added by 131.246.78.12 (talk) 07:36, 14 July 2016 (UTC)

Confusing example

The "toy example" is very hard to read and understand for non-math people (including software engineers like me). Obvious questions to start:

• "The maximum is larger than any given number, and is one of the given numbers" sounds to me like an impossibility. Is that a mistake or poorly phrased or what?
• What does the axiom "A=A" mean in words and why is it required?

-- Beland (talk) 06:06, 28 May 2016 (UTC)

The informal specification of maximum was sloppy; I fixed this (not quite sure whether "larger or equal than" is ok or "... to").

"A=A" is the reflexivity property of equality; the remaining axioms aren't used in this example, so I omitted them. Reflexivity is used to obtain line 14 from line 12; informally, the (trivial) equation "x=M" (with x a constant and M a variable) is solved w.r.t. M by resolution with "A=A". - Jochen Burghardt (talk) 17:07, 28 May 2016 (UTC)

@Jochen Burghardt: Your rewrite clarified these questions, and I've removed the {{confusing}} tag. Thanks a bunch for your work on this article! -- Beland (talk) 17:43, 15 February 2019 (UTC)

The example at best produces only expressions that utilize only the ?: 3-place Boolean function. Even using this function more than once e.g. x?y:(z?w:v) would not be possible without a reference to how parentheses are generated. The work of Volkstorf cited describes the creation of complete PHP programs, which is vastly more complete than this example, but is given an only cursory mention. — Preceding unsigned comment added by 2601:184:4081:1CBE:BCCD:9145:66F5:A63E (talk) 04:46, 9 February 2019 (UTC)

In-text critics by anonymous user

I insert here paragraphs that were inserted into the article by an anonymous user. While they are valuable for the improvement of the article, they don't belong there. - Jochen Burghardt (talk) 09:01, 11 February 2019 (UTC)

• This gives the steps in a proof and then presents a programming language expression. However, there is no explanation as to how the expression was derived from the proof. The expression contains variables and symbols ? and : but there is no procedure given for constructing an expression consisting of these characters.

26 January 2019 - 2601:184:4081:1cbe:8c24:e846:2c8e:12f8

• However, there is no rule or procedure described that explains how or why the question mark and colon characters are introduced in line 58, in which the string p ? s : t appears. Furthermore, there is no explanation as to how programs which consist of commands such as assignment, if-else or loops are created.

9 February 2019 - 2601:184:4081:1cbe:bccd:9145:66f5:a63e:L

• However, the example does not follow the form of logic and resolution in particular. Wiki resolution states: “produces a new clause implied by two clauses containing complementary literals” e.g. “avb, ~avc => bvc”. 14 Resolve(12,1) uses 1 and 12 but they are not of the form avb and do not contain complementary literals. Likewise for 15, 17, 18. 16 is derived from 3 and 15, but if y=x then 15 is true but 16 is false. 16 contradicts 15. Lastly, 19 derives x<y ? y : x from contradictory statements x <= y and ~(x <= y). If this is Resolution then we would derive false. There is no explanation as to what in general is derived e.g. if we have x=y and ~(x=y) what expression do we derive? In general, from expressions P and ~P what do we derive?

10 February 2019 - 2601:184:4081:1cbe:980f:4a3c:27ed:8bf1

Correction: See Critiques of e.g. Law_of_excluded_middle, Falsifiability, Principia_Mathematica, Zermelo–Fraenkel_set_theory — Preceding unsigned comment added by 2601:184:4081:1CBE:80AC:29DF:4AA7:416D (talk) 17:56, 11 February 2019 (UTC)

Technical contributions need to be adjudicated or accepted without comment.

11 February 2019‎ 2601:184:4081:1cbe:80ac:29df:4aa7:416d

Ok, "critiques" (let alone "critics", I just found the subtle difference in my dictionary) wasn't the right word - sorry for that! What I meant was this:

Your phrase "there is no explanation of ..." refers to a drawback of the presentation, not necessarily of the contents itself. I am currently trying to improve the former. The talk page here is intended to discuss presentation issues. -

I think your issues of 26 Jan and 9 Feb are resolved in the current article version, aren't they? I guess your issue of 10 Feb is still unresolved; however, I have no idea how to explain it better than referring to the table showing the (non-clausal) resolution rules. - Jochen Burghardt (talk) 09:13, 12 February 2019 (UTC)

Another In-text critics by anonymous user

CRITIQUE: The Toy Example given produces only the one program given in the rules. Program Synthesis means creating a computer program from scratch, not plucking one from a list of one. Surely a system for creating computer programs that constantly is unable to produce anything until once in a blue moon someone asks for that one program, is not an example of how computer programs can be constructed automatically. It should either be removed or admit that it produces only one program and isn't really program synthesis.

A better way to produce that result is by having a program ask "Do you want a program to take the maximum of 2 numbers?" and if the answer is yes it outputs that program, and if the answer is no it says "Sorry, no can do."

— Preceding unsigned comment added by 2601:184:4081:1CBE:EC4B:754:77D:69F5 (talk) 21:20, 25 August 2019 (UTC)

The Manna-Waldinger approach is able to produce different algorithms even for the simple toy example "maximum of two numbers", if different logical derivations are used for synthesis. For example, int max(int x,int y) { return min(x,y)+abs(x-y); } may well be derived, given appropriate formal properties of min, abs, +, and -. In the Manna-Waldinger approach, there is no list to pluck programs from; I wonder where in the article you took that idea from. - Jochen Burghardt (talk) 08:41, 26 August 2019 (UTC)

Answer for Jochen Burghardt: The Toy Example uses rules that include the only program that can be "created". You are simply telling the system the program to output in the rules. True program synthesis has a mechanism for constructing programs. The example has only the single program that can be produced from the list of one program. - 6 Sep 2019‎ 2601:184:4081:1cbe:b170:ce3:5935:8557

Please: (1) don't change the old text of a discussion, in order to keep it transparent to all readers. (2) Sign your posts, for the very same reason.

The toy example shows only those axioms and rules that are needed to derive it. I guess, Zohar Manna and Richard Waldinger had in mind a large collection of axioms and rules to choose from. Also note that the system is far from being automatic; instead it provided rules to be applied by hand; it does guarantee, however, that the program finally obtained satisfies the specification you started from. Moreover, feel free to add text about other approaches to ("true") program synthesis. - Jochen Burghardt (talk) 15:36, 8 September 2019 (UTC)

Answer for Jochen Burghardt: The definition given for program synthesis is "the task to automatically construct a program". The program "synthesized" is input by a person in line 58. That is not automatic. Furthermore, as you say, "it does guarantee, however, that the program finally obtained satisfies the specification.". That is not program synthesis, that is program verification. Do you really believe this meets the definition for program synthesis given in the first sentence of this article? — Preceding unsigned comment added by 2601:184:4081:1CBE:6862:FA93:3A9:C677 (talk) 15:42, 9 September 2019 (UTC)

I see your point. However, I think that definition is too restrictive: the cited reference, Basin et al 2004, defines in the 1st sentence of the introduction "Program synthesis is concerned with the following question: Given a not necessarily executable specification, how can an executable program satisfying the specification be developed?" (no mention of automatization). On the next page, they say "The objective of program synthesis is to develop methods and tools to mechanize or automate (part of) this process"; "program synthesis" here apparently refers to the research field, not to a tool or method (the latter don't "develop methods and tools"). Indeed, it is the ultimate objective of this field to come up with automatic tools; however many early approaches' contributions were focussed on other subtopics (such as relating to predicate logic as a specification language). I checked one of the references Basin et al refer to for a description of major achievements, viz. [26] (Yves Deville and Kung-Kiu Lau (May–Jul 1994). "Logic program synthesis". Journal of Logic Programming. 19–20: 321–350.), it gives almost the same definition in its abstract (again no mention of automatization), and cites, on p.328, Manna.Waldinger.1980 (=[93]) as a "program synthesis system". This agrees with Manna's and Waldinger's own terminology (see their title).

The difference program synthesis vs. verification is not automatization vs. non-automatization, but whether the program is obtained as output of the method or has to be given as its input.

In any case, you should stop inserting discussion text into the article. - Jochen Burghardt (talk) 15:54, 16 September 2019 (UTC)

In the Toy Example, the program produced is entered by the user in line 58. This is not program synthesis, which is defined on this page as automatically constructing the program. The Toy Example needs to be moved to the Formal verification page listed below. If this is not corrected, this error will have to become a critique.

“It is the ultimate objective of this field to come up with automatic tools; however many early approaches' contributions were focussed on other subtopics (such as relating to predicate logic as a specification language).” The design of the specification language is necessary whether your methods are automated or not.

Critiques are common in Wikipedia.

“I think that definition is too restrictive”: Then it needs to be corrected to match the text of the page. - 17 September 2019‎ 2601:184:4081:1cbe:3d34:2e95:afb4:f746

The program is not entered by the user; line 58 is an instance of the rule in line 19; the "(?:)" operator originates from that rule.

"The design of the specification language is necessary whether your methods are automated or not." — That what I say; and for this reason, I (and, as far as I know, everyone in the community) consider Manna's and Waldinger's approach to belong to the research field of program synthesis, although their approach is not yet automatized.

Debates to settle different opions of editors are to be located at talk pages.

I agree the lead should be changed (as I said, you have a point there), but I wanted to wait for your response before. Would you be ok with the above-cited sentence from basin et al ("Program synthesis is concerned with the following question: Given a not necessarily executable specification, how can an executable program satisfying the specification be developed?"), or a slight rephrasing to avoid copyright problems?

By the way: undoubtedly, there are many more, and better, approaches to program synthesis than Manna's and Waldinger's (which is pretty old pioneering work). Currently, the latter has undue weight in this article. I still hope some other editors will contribute about other approaches in the future, in order to balance the weight. As a short-term measure, one might start an almost empty section for every major approach (found e.g. in the paper by Deville and Lau), and include a tag that it should be expanded. - Jochen Burghardt (talk) 09:42, 18 September 2019 (UTC)

PS: As an analogy in program verification, work has started there with the Hoare calculus, which was pioneering despite its complete lack of automatization; mordern approaches like e.g. Frama-C are fully automatic, and based on Hoare's work. - Jochen Burghardt (talk) 09:46, 18 September 2019 (UTC)

 Done I fixed the lead according to the above discussion. - Jochen Burghardt (talk) 15:48, 24 September 2019 (UTC)

Example Does Not Create an Entire Program

This only produces the one operator p ? s : t with substitution for p, s, t. It does not create any other aspects of a program, such other operators, complete expressions and commands such as assignment, conditional execution and loops. It is not a complete program. This can better be described as “creating a single operator” than creating a program. It is no more program synthesis that building a wheel is building a car. This fact is being suppressed by the author of this page without addressing it. — Preceding unsigned comment added by 2601:184:4081:1CBE:C193:3D85:27BF:92C2 (talk) 15:59, 4 November 2019 (UTC)

As noted in the article, the supported language is Turing-complete. This means that every possible program can be expressed in that language.

The example states "Since the goal formula true has been derived, the proof is done, and the program column of the "true" line contains the program." This is just an expression and programming languages require a lot more than single expressions to be Turing complete. At a minimum there needs to be some sort of looping mechanism e.g. FOR/WHILE/UNTIL. At best (if the proof were correct) you are verifying a single expression (that given in the rules) meets a given specification. It is not program synthesis and it is not even program verification. Perhaps you can call it expression verification. As such it does not belong on this page.

As noted in the footnote nearby, arbitrary new operators and relations can be added by providing their properties as axioms. To keep the toy example in toy size, only ≤ has been (incompletely) axiomatized there. (I now marked footnotes containing explanations, rather than just references, by "note".)

Adding more expressions does not change the fact that you are not synthesizing programs nor even verifying programs.

As noted under "structural induction", e.g. a algorithm to compute quotient and remainder of two given integers is synthesized in Manna, Waldinger (1980), p.108-111. More examples have been published in journal articles; as a reaction to your repeated criticism, I'll look them up and add their references. - However, this will still increase the undue weight of the Manna/Waldinger approach in this article. - Jochen Burghardt (talk) 09:05, 5 March 2020 (UTC)

Semi-protected edit request on 6 March 2020

In the example:

1. Step 16 is not true. x and y are free variables. x and y can be equal, so that both y <= x (15) and x <= y (the negation of 16) are actually true. This occurs when the two arguments to the program are equal. Axiom 3 is not an exclusive OR. (15) is not the negation of either disjunct of (3) and Resolution does not apply.

2. Step 19 is inconsistent with the other steps. The goal, true, in step 19 is the disjunction (OR) of the two arguments, x <= y (18) and ~(x <= y) (16). In the other steps, we are correctly assuming the conjunction (AND) of the two arguments, which would make Goal 19 false instead of true. For example, in 15 we are using the truth of A <= A (Axiom 2), substituting x for A to get x <= x and removing x <= x from x <=x ^ y <=x (14) to get y <= x (15). Certainly axioms are always true.

3. What happens if the input specification is not the maximum of two numbers? Does every program created have to be listed in the Program column of some rule? Wouldn’t that mean that every program that can be created must be supplied in the rules? If that is the case, then why not simply list the programs and their specifications, and compare the input specification to find its program? That would eliminate all of the effort required by the user to locate the correct program. In “A Survey and a Categorization Scheme of Automatic Programming Systems”, Generative and Component-Based Software Engineering, 1999, pp. 1-15, [e.g. https://link.springer.com/chapter/10.1007/3-540-40048-6_1] Wolfgang Goebl notes “All of the program code produced should be generated without the help of the user. All of these so called ‘Automatic Programming’ techniques are very different from the idealistic.” [pg. 2] Simply listing the programs and specifications to be looked up would meet this criteria. Mdaviscs (talk) 16:55, 6 March 2020 (UTC)

Reply:

The section in question presents one approach to program synthesis along published journal articles. I can't help if you don't like the approach. I'm tired of defending it. As for the challenged lines I'm sure they are OK:

1. Line 16 is obtained by resolving lines 15 and 3, according to the rule in line 57, using "y≤x" as p. Manna and Waldinger have proved the soundness of their calculus. Intuitively, the resolution argument at that point can be read: "To prove y≤x, when it is known that A≤B ∨ B≤A holds for all A,B, it is sufficient to prove ¬(x≤y).". (Also note that variables are denoted by capital letters here; x,y are both constants, obtained from reverse Skolemization. Maybe this should be elaborated in more detail in the article?)
2. Line 19 is obtained from 18 and 16 in a similar way by application of the non-clausal resolution rule from line 58, using "x≤y" as p.
3. See #Example Does Not Create an Entire Program. Make sure you understand what a functional programming language is, and what Turing complete means. - Jochen Burghardt (talk) 18:25, 6 March 2020 (UTC)