程序综合概述
Definition
Program Synthesis is the task of automatically finding programs from the underlying programming language that satisfy user intent expressed in some form of constraints.
Challenge
- Program Space : program synthesis is a second order search problem. In its most general formulation (for a Turing-complete programming language and an arbitrary constraint) program synthesis is undecidable. Even though modern-day synthesis techniques produce sizable real-life code snippets, they are still rarely applicable to industrial-size projects. See 程序综合的一般原则 for common techniques to reduce the space.
- User Intent : It’s hard to accurately expressing and interpreting user intent (without making the specification complicated)
Three Dimensions of a Synthesizer
User Intent
The user intent can be expressed in various forms:
- logical specification : It can act as a precise and succinct form of functional specification of the desired program. However, complete logical specifications are often quite tricky to write.
- Example-based specifications : ambiguity is often resolved in an interactive loop with the user, where the user may iteratively provide more examples dependant on the behavior of the program synthesized in the last step. see programming by example
- trace : A trace is a detailed step-by-step description of how the program should behave on a given input. Traces are an appropriate model for programming by demonstration systems.
- program : for certain applications such as superoptimization, deobfuscation and synthesis of program inverses, the program to be optimized, deobfuscated, or inverted respectively forms the specification.
Search Space
The search space can be over imperative or functional GPL or DSL programs, or restricted models of computations like CFG and regular expression.
Search Technique
- enumerative search based synthesis
- constraint solving based synthesis
- stochastic search
- deductive search, which is documented in programming by example
Application
- data wrangling
- Graphics Manipulation
- Code Repair
- code suggestion
- probabilistic modeling
- superoptimization
- concurrent programming