Program Synthesis

I will compare and contrast two approaches to the problem of program synthesis, one by Osera and Zdancewic [10] and one by Hong and Aiken [3]. I will consider how techniques from programming languages, machine learning, and human-computer interaction can be used to tackle the synthesis problem.

The synthesis problem must be seen through the eyes of a pragmatist. A solution to the synthesis problem is not difficult to find: enumerate through the countably infinite Gödel-encoded programs, decoding and testing each in turn. If the specification is satisfiable, then this technique is guaranteed to find it. The problem is a practical one. Not only is blind enumeration incredibly inefficient, but if a solution does not exist, it will not terminate. We must thus attempt to make the problem tractable.

Judgement Day

Osera and Zdancewic illustrate how techniques from programming language theory can be used to make the problem tractable. Assume the user provides a specification in the form of a type, and a set of examples (constraints).

let rec stutter l : list nat -> list nat |>
    { [] => []
    | [0] => [0;0]
    | [0;1] => [0;0;1;1]
    } = ?

We first reach for the low hanging fruit: without having to guess a term, we know that we must synthesise a well-typed list, and further, that it cannot be a constant list. Any further inference requires guesswork. Osera and Zdancewic guess in order of increasing term size.

Blind enumeration in this fashion would be far too expensive. Two techniques are employed here: one based on normal forms, and another based on typing judgements.

First, Osera and Zdancewic only generate terms in \(\beta\)-normal, \(\eta\)-long form. For example, the synthesiser is allowed to generate x, but not \((\lambda \texttt{y}. \texttt{y}) \texttt{x}\). This decreases the search space. It uses \(\beta\eta\)-equivalence (the reflexive, symmetric, transitive closure of \(\beta\)-reduction and \(\eta\)-expansion) to partition the search space, considering only one representative from each partition.

Second, Osera and Zdancewic only generate well-typed terms. Thus, the generated term must have an associated typing judgement. The typing derivation decomposes the type inference problem into sub-goals. This compositional structure can be leveraged to decompose the synthesis problem into sub-goals. For example, assume that the synthesiser is guessing a term of the form

\[ \texttt{match l with [] -> }e_1\texttt{ | x::xs -> }e_2\texttt{::}e_3 \]

where \(e_1\), \(e_2\), and \(e_3\) are to be guessed. This has typing derivation

This typing derivation decomposes the problem into the synthesis of \(e_1\) (list nat), \(e_2\) (nat), and \(e_3\) (list nat). This limits complexity in two ways. First, each of the sub-goals can be solved independently. Hence, if there are \(N_i\) possible candidates for \(e_i\), we only need to consider \(\Sigma_i N_i\) candidates, rather than \(\Pi_i N_i\).

Second, checking solutions to the sub-goals can be made easier by using the derivation to distribute constraints. In this particular example, we know \(e_1\) necessarily satisfies the constraint

[]  =>  []

\(e_2\) the constraints

0::[]   =>  0
0::[1]  =>  0

and \(e_3\) the constraints

0::[]   =>  [0]
0::[1]  =>  [0;1;1]

While Osera and Zdancewic build a strong theoretical foundation, in my opinion, their approach would benefit from a more rigorous empirical treatment. In describing their implementation, Osera and Zdancewic appeal to weak empirical arguments. For example, they assume that the same terms will be repeatedly synthesised, and design data structures that maximise cache hit rate under this assumption. While seemingly reasonable, the assumption is asserted without evidence. Additionally, the search procedure relies on parameters that switch between guessing and refinement. These parameters are chosen by a “simple strategy” that works on their test cases, but this assumes their test cases are representative. Once again, it is made without justification.

Similarly, their “evaluation” could go further. Osera and Zdancewic report runtimes in the order of \(10^{-2}\) and \(10^1\) seconds, but do not indicate if this is suitable for their imagined use-cases, for example, by considering interactivity thresholds [9]. They point out that the synthesiser occasionally synthesises sound but surprising programs, but do not indicate their frequency, nor the effect on understandability or maintainability.

In summary, one sees a foundation on which to build, rather than a complete solution.

Rise of the Machines

Hong and Aiken recognise the importance of empiricism in solving the synthesis problem, supplementing a theoretical framework with empirical techniques. As such, in my opinion, their solution is more complete.

At first glance, the structure of Hong and Aiken’s [3] approach mirrors Osera and Zdancewic’s [10]. In both, users specify the type and a set of examples. Where Osera and Zdancewic are able to generate any well-typed structurally recursive term, Hong and Aiken only consider a smaller class of (nested) paramorphisms. A paramorphism is a primitive recursive function that tracks its input. The primitive recursion scheme over lists, parameterised on \(g_\texttt{Nil}\) and \(g_\texttt{Cons}\), looks like

\[ \begin{array}{llllll} \texttt{primrec} & \texttt{[]} & g_\texttt{Nil} & g_\texttt{Cons} & = & g_\texttt{Nil} \\ \texttt{primrec} & \texttt{x::xs} & g_\texttt{Nil} & g_\texttt{Cons} & = & g_\texttt{Cons}\,\texttt{(x, primrec xs }g_\texttt{Nil}\;g_\texttt{Cons}\texttt{)} \end{array} \]

The equivalent paramorphism scheme is

\[ \begin{array}{llllll} \texttt{para} & \texttt{[]} & g_\texttt{Nil} & g_\texttt{Cons} & = & g_\texttt{Nil} \\ \texttt{para} & \texttt{x::xs} & g_\texttt{Nil} & g_\texttt{Cons} & = & g_\texttt{Cons}\,\texttt{(x, (xs, para xs }g_\texttt{Nil}\;g_\texttt{Cons}\texttt{))} \end{array} \]

Paramorphisms are thus a mode-of-use of primitive recursion. Hence, in particular, the Ackermann function is not synthesisable by Hong and Aiken. It is, however, structurally recursive, and thus synthesisable, in theory, by Osera and Zdancewic.

Just as Osera and Zdancewic use a typing derivation to decompose the problem into sub-goals (whose solutions may contain recursive calls), Hong and Aiken first generate a recursion template, with a hole for each sub-goal. Specifically, they consider “proper recursion nests”: recursive templates created by nesting paramorphisms such that all branches have equal nesting depth. For example,

para [-]Boolean gTrue gFalse where
  gTrue  = para [-]TreeNat gLeaf gNode where
    gLeaf  = [-]ListNat
    gNode n (l, s1) (r, s2) = [-]ListNat
  gFalse = para [-]TreeNat gLeaf gNode where
    gLeaf  = [-]ListNat
    gNode n (l, s1) (r, s2) = [-]ListNat

The functions on which a paramorphism is parameterised (\(g_\texttt{True}\) and \(g_\texttt{False}\) in the example above) may themselves be paramorphisms (in this case, on TreeNat). This creates a tree of nested paramorphisms (different levels have been colour coded):

para [-]Boolean gTrue gFalse where
  gTrue  = para [-]TreeNat gLeaf gNode where
    gLeaf  = [-]ListNat
    gNode n (l, s1) (r, s2) = [-]ListNat
  gFalse = para [-]TreeNat gLeaf gNode where
    gLeaf  = [-]ListNat
    gNode n (l, s1) (r, s2) = [-]ListNat

All branches must nest to the same depth: if \(g_\texttt{True}\) is a paramorphism, then so must \(g_\texttt{False}\) be. Nodes in the tree are holes, representing non-recursive terms that must be synthesised to instantiate the template. As in Osera and Zdancewic, holes are filled by search.

While the scaffolding appears similar, look more closely at the details, however, and a pattern emerges: Hong and Aiken rely on empirical arguments to justify trading generality for guarantees.

Rather than lamenting their inability to handle general recursion [10], Hong and Aiken are content to only search for paramorphisms, as they are still “quite expressive”.

Similarly, proper recursion nests place far more syntactic constraints on synthesised expressions than typing derivations (typing derivations do not fix the recursive structure). This restriction limits expressiveness, but is still able to generate “most programs of interest”. Not only is the argument empirical, so too is the justification – their tool is able to solve tasks not explicitly designed to be primitive recursive.

The search procedure is clearly empirical. Assume we wish to generate a term of type list. Hong and Aiken initialise this term to a default element, Nil, to which we apply one or more re-write rules. To determine which re-write rule to choose, a stochastic approach is used. First, define a cost function that penalises candidate terms for size and incorrectness (with respect to the constraints). Each re-write rule introduces a change in the cost. Treating these changes as weights, we obtain a probability distribution over re-write rules. In the case of the paper, the weighting is such that proposals which introduce a decrease in the cost are always accepted. The fundamental advantage of this technique is that the search is guided by approximating the semantic proximity to a correct solution, rather than a syntactic policy.

While an improvement, I argue more can be done. The techniques here are borrowed from the field of machine learning. In machine learning, it is conventional to justify the choice of initialisation [6], and to weigh the trade-offs between exploring more of the search space, and exploiting improvements [5]. The latter might involve trying different weighting strategies that do not so eagerly pursue local improvements to the cost function.

Cancellation and Reboot

Neither Hong and Aiken nor Osera and Zdancewic consider the importance of human-centric techniques. As with any practical problem, discussion of program synthesis must be grounded in a context of use. Implicitly, both Osera and Zdancewic and Hong and Aiken assume that different flavours of synthesis (synthesis of Excel formulae, or paramorphisms) have similar cognitive effects on the user. This assumption underlies, for instance, motivating general program synthesis by appealing to the usability benefits of synthesis in domain-specific programming (like Flash Fill for Excel formulae) [3, 10].

This assumption is unrealistic. In particular, synthesis in the context of end-user programming [8] – for example, Excel manipulation – is not the same as synthesis in the context of professional programming – for example, building a parser generator.

Cognitively, end-user and professional programming are very different tasks [11]. The theory of Attention-Investment considers programming through the lens of cognitive psychology: by investing attention to write a program in the present, we save on attentional costs in the long run. Indeed, the more attention invested in the present, the less attention one has to invest in the future, because the solution was sufficiently abstract, sufficiently maintainable, or because the programmer has developed a better understanding of the problem [1].

Consider end-user programming in Attention-Investment terms, through the example of Excel spreadsheets. In many cases, users do not need to write an abstract solution, but simply solve a concrete problem. They thus can choose not to invest attention towards writing spreadsheet formulae, but rather manually modify the spreadsheet [11, 13]. Hence, synthesis of Excel formulae can encourage users to generate more abstract solutions. In professional programming, however, the problem itself demands that attention be invested in writing code. The incentive structure is thus reversed. If the programmer can synthesise portions of the program, they may reduce the attention invested in the present. Code becomes harder to debug, maintain, and extend in future.

Program synthesis may also have an undesirable effect on intention [12]. Program synthesis tools are often viewed as mixed-initiative systems [4]: helping the user achieve their desired intention more efficiently [2]. This is true if the user has an extremely precise specification, which can occur in one-off end-user programming tasks, but not in the case of an incomplete specification [7]. Even the slightest under-specification can create choices for the synthesiser. For example, should a list reversal function be recursive or tail-recursive? In making these choices, the synthesiser can shape the user’s intention [12]. In professional programming, the specification is often imprecise, and the programmer iteratively refines their understanding of the specification by surfacing design decisions made during the process of writing code [7]. Being able to generate code that satisfies their first draft of a specification bypasses this process, making implementation less intentional.

In my opinion, we should ask not only if synthesis is doable, but also if it is desirable, by considering how programmers interact with the synthesiser. A clearer understanding of these contexts of use would provide mechanisms for justifying empirical assertions. For example, end-user programmers might expect interactivity, but not require full Turing-completeness.

References

1. [1] A. Blackwell and M. Burnett. Applying attention investment to end-user programming. In Proceedings IEEE 2002 Symposia on Human Centric Computing Languages and Environments, pages 28–30. 2002. doi.org/10.1109/HCC.2002.1046337
2. [2] A. Head, E. Glassman, G. Soares, R. Suzuki, L. Figueredo, L. D'Antoni, and B. Hartmann. Writing Reusable Code Feedback at Scale with Mixed-Initiative Program Synthesis. In Learning at Scale (L@S), pages 89–98. 2017.
3. [3] Q. Hong and A. Aiken. Recursive Program Synthesis using Paramorphisms. Proc. ACM Program. Lang., 8(PLDI). 2024. doi.org/10.1145/3656381
4. [4] E. Horvitz. Mixed-Initiative Interaction. IEEE Intelligent Systems, pages 14–24. 1999.
5. [5] L. P. Kaelbling, M. L. Littman, and A. W. Moore. Reinforcement learning: A survey. Journal of artificial intelligence research, 4, pages 237–285. 1996.
6. [6] P. Krähenbühl, C. Doersch, J. Donahue, and T. Darrell. Data-dependent Initializations of Convolutional Neural Networks. arXiv:1511.06856. 2016. arxiv.org/abs/1511.06856
7. [7] M. J. L. Lee, A. Sarkar, and A. F. Blackwell. Predictability of identifier naming with Copilot: A case study for mixed-initiative programming tools. In Proceedings of the 35th Annual Conference of the Psychology of Programming Interest Group (PPIG 2024). 2024.
8. [8] B. A. Myers, A. J. Ko, and M. M. Burnett. Invited research overview: end-user programming. In CHI '06 Extended Abstracts on Human Factors in Computing Systems, pages 75–80. 2006. doi.org/10.1145/1125451.1125472
9. [9] J. Nielsen. Usability Engineering. 1993. dl.acm.org/citation.cfm?id=2821575
10. [10] P.-M. Osera and S. Zdancewic. Type-and-example-directed program synthesis. SIGPLAN Not., 50(6), pages 619–630. 2015. doi.org/10.1145/2813885.2738007
11. [11] S. Peyton Jones, A. Blackwell, and M. Burnett. A user-centred approach to functions in Excel. SIGPLAN Not., 38(9), pages 165–176. 2003. doi.org/10.1145/944746.944721
12. [12] A. Sarkar. Intention Is All You Need. In Proceedings of the 35th Annual Conference of the Psychology of Programming Interest Group (PPIG 2024). 2024.
13. [13] A. Sarkar and A. Gordon. How do people learn to use spreadsheets? (Work in progress). In Psychology of Programming Interest Group (PPIG), pages 28–35. 2018.