Bottom-up Synthesis of Recursive Functional Programs using Angelic Execution

We present a novel bottom-up method for the synthesis of functional recursive programs.

While bottom-up synthesis techniques

can work better than top-down methods in certain settings,
there is no prior  technique for synthesizing recursive programs from logical specifications in a purely bottom-up fashion. The main challenge is that effective bottom-up methods need to execute sub-expressions of the code being synthesized, but it is impossible to execute a recursive subexpression of a program that has not been fully constructed yet.  In this paper, we address this challenge using the concept of angelic semantics.

Specifically, our method finds a program that satisfies the specification under angelic semantics (we refer to this as angelic synthesis), analyzes the assumptions made during its angelic execution, uses this analysis to strengthen the specification, and finally reattempts synthesis with the strengthened specification. Our proposed angelic synthesis algorithm is based on version space learning and therefore deals effectively with many incremental synthesis calls made during the overall algorithm.
We have implemented this approach in a prototype called and evaluate it on synthesis problems from prior work.
Our experiments show that is able to synthesize a solution to 95% of the benchmarks in our benchmark suite, outperforming prior work.

Anders Miltner

UT Austin

Adrian Trejo Nuñez

UT Austin

Ana Brendel

UT Austin

Swarat Chaudhuri

UT Austin

Isil Dillig

UT Austin

§ INTRODUCTION

Methods for program synthesis from formal specifications typically come in two flavors: top-down and bottom-up. Top-down methods <cit.> iterate through a sequence of partial programs, starting with an “empty” program and progressively refining them through the addition of new code. In contrast, bottom-up methods <cit.> maintain a pool of complete programs and  progressively generate new programs by composing existing ones.

Top-down and bottom-up approaches  have complementary strengths. For example, top-down methods work well when the specification  can be naturally decomposed into subgoals through an analysis of partial programs.

However, they can run into imprecision or computational complexity issues when the specification or the language semantics are complicated. In contrast, a bottom-up approach only needs to evaluate complete sub-expressions of a program, which is generally a much easier task than that of reasoning about partial programs.

Unfortunately, it is difficult to apply bottom-up synthesis  to programming languages that permit recursion.
This is because effective bottom-up  approaches need to  execute all sub-expressions of the target program; however, for recursive programs, sub-expressions can call the function being synthesized, whose semantics are still unknown.

One way to overcome this issue is to assume that the specification is trace-complete, i.e., that the result of each such evaluation is part of the specification. (Indeed, such a strategy is followed in the Escher <cit.> system for the bottom-up synthesis of recursive programs.) However, trace-completeness is a restrictive assumption, and writing trace-complete specifications can be cumbersome and unintuitive.

In this paper, we propose a new approach to bottom-up program synthesis that addresses this difficulty.
The key insight behind our solution

is to use angelic execution <cit.> to evaluate recursive sub-expressions of the program being synthesized. Specifically, our method first performs angelic synthesis to find a program $P$ that satisfies the specification under the assumption that recursive calls can return any value that is consistent with the specification. For example, if the specification is $0 \leq f(x) \leq x$, the angelic synthesizer assumes that a recursive call $f(2)$ can return any of the integers $0, 1, $ or $2$, although in reality it can only return one of these. Thus, when performing angelic synthesis of a function $f$, we only need access to $f$'s specification rather than its full implementation.

One complication with this approach is that a program $P$ that angelically satisfies its specification $\varphi$ may not actually satisfy $\varphi$. To deal with this  difficulty, our method combines angelic synthesis with specification strengthening and back-tracking search. In more detail, given an angelic synthesis result $P$, our synthesis technique first checks if $P$ satisfies $\varphi$ under the standard semantics. If so, then $P$ is returned as a solution. Otherwise, our method analyzes the assumptions made in angelic executions of $P$, uses this information to strengthen the specification, and re-attempts synthesis with the strengthened specification. If synthesis is unsuccessful with the strengthened specification, it backtracks and tries a different strengthening, continuing this process until it either finds the right program or exhausts the search space.

As illustrated by the above discussion, our end-to-end approach requires gradually strengthening the specification and making many calls to an angelic synthesizer. Thus, for our approach to be practical, it is important to have an  angelic synthesis technique that can reuse partial synthesis results. Additionally, it must be possible to easily analyze assumptions made in angelic executions in order determine how to  strengthen the specification. Motivated by these considerations, we propose an angelic synthesis technique based on  finite tree automata <cit.>. Our proposed angelic synthesizer handles incremental specifications by taking the intersection of previously constructed tree automata (for weaker specifications) with new automata constructed from the additional specifications. This incremental nature of the angelic synthesizer allows our approach to efficiently handle a series of increasingly more complex specifications. Furthermore, by inspecting runs of the tree automaton, we can easily and efficiently analyze the assumptions made by the angelic synthesizer.

A key characteristic of our method is that it stores sets of generated programs in a compact version space representation —

finite tree automata  <cit.>.

Traditionally, a version space in program synthesis exactly represents the set of programs that satisfies a specification. However,
because our algorithm uses the angelic semantics of recursive calls, the automata that it constructs are
over-approximations of
actual version spaces.
Our algorithm iteratively refines these overapproximate version spaces by analyzing angelic program traces and using the results of this analysis to gradually strengthen the specification.

The use of version spaces makes our method especially well-suited to incremental program synthesis settings <cit.>. Given a new constraint on the specification, we start by constructing an version space for this constraint. This version space is then intersected with the version space for the older specification using an efficient version space intersection operation.

We have implemented our technique in a tool called [Bottom-Up Recursive SynThesizer] and evaluate it on 45 benchmarks from prior work <cit.> using three types of specifications, namely (1) input-output examples, (2) reference implementations, and (3) logical formulas.

Our evaluation shows that can synthesize more functions than prior work on all three types of specifications. In particular, our tool is able to synthesize 96% (43) of the functions from input/output examples, 96% (43) of the functions from reference implementations, and 93% (41) of the functions from logical specifications. We also compare against a simpler variant that does not perform specification strengthening, and we show that our proposed backtracking  search technique is useful in practice.

In summary, this paper makes the following contributions:

* We present the first bottom-up synthesis procedure that can handle general recursion and general logical specifications, and does not require the restrictive trace-completeness assumption.

* We introduce a new form of angelic program synthesis that combines the use of angelic program semantics and specification strengthening and can make use of efficient version space representations. Some of the insights in our algorithm may be applicable outside the immediate setting that we target.

* Our artifactual contribution is an implementation of our approach, called . We have conducted an extensive experimental evaluation on synthesis benchmarks from prior work.

Our experiments show that significantly outperforms the state-of-the-art in the synthesis of recursive programs on several counts.

§ OVERVIEW

figureFirst example $T_1$

figureSecond example $T_2$

Example trees $T_1$ and $T_1^R$. The right spine of $T_1$ is the list [1;0], and the right spine of $T_1^R$ is the list [0].

Example trees $T_2$ and $T_2^R$. The right spine of $T_1$ is the list [2], and the right spine of $T_2^R$ is the list [].

In this section, we give an overview of our method with the aid of a motivating example. Our goal in this example is to synthesize a recursive implementation of the right_spine procedure, which takes as input a tree and produces a list that is obtained by traversing the rightmost children of a node, starting from the root  and  continuing until a leaf node is reached.   As an example, Figures <ref> and <ref> show two trees $T_1$ and $T_2$, and a partial input-output specification for right_spine is given as follows:

\begin{equation}
\label{eq:init-spec}
\begin{split}
\mlstinline{right_spine}(T_1) & = [1;0] \\
\mlstinline{right_spine}(T_2) & = [2]
\end{split}
\end{equation}

Note that our method can work with specifications that are not input-output examples (see Section <ref>); here, we simply choose it for simplicity of presentation. We now explain how our technique synthesizes this right_spine procedure in a bottom-up fashion.

§.§ High Level Algorithm

Our algorithm works in a refinement loop that performs two major steps: (1) it synthesizes a program that angelically satisfies the specification, and (2) strengthens the specification based on the assumptions made in the angelic execution. In this subsection, we illustrate the high-level approach on right_spine, leaving the details of angelic synthesis to Section <ref>.

*Iteration 1 The algorithm starts by invoking the angelic synthesizer to find a program that angelically satisfies the specification shown in Equation <ref>. As we will discuss later, the angelic synthesizer outputs the following program in this iteration:

let rec P1(x) =
match x with
| Nil -> []
| Node(l,v,r) -> P1(r)

Clearly, this program does not actually satisfy the specification, but it does satisfy the specification under the angelic semantics: Since the specification from Eq. <ref> does not constrain the output of the recursive call on $T_1^R$, the angelic synthesizer assumes that  the recursive call to P1 can return anything, including [1;0], for the right subtree of $T_1$. Thus, program P1 satisfies the specification under the angelic semantics of recursion.

Next, our algorithm checks whether the candidate program satisfies the specification under the actual semantics. Since
P1($T_1$) = P1($T_2$) = [],
it clearly does not, and our algorithm analyzes the assumptions made in the angelic execution to determine how to strengthen the specification. In this case, the angelic execution assumes that the recursive call on the right-subtrees $T_{1}^R$ and $T_2^R$ return $[1; 0]$ and $[2]$ respectively. Thus, our algorithm re-attempts synthesis using the following strengthened specification:

\begin{equation}
\label{eq:spec2a}
\begin{array}{rlrl}
\mlstinline{right_spine}(T_1) & = [1;0] & \hspace*{2em}
\mlstinline{right_spine}(T_2) & = [2] \\[4pt]
\mlstinline{right_spine}(T_1^R) & = [1;0] & \hspace*{2em}
\mlstinline{right_spine}(T_2^R) & = [2]
\end{array}
\end{equation}

*Iteration 2a In the next recursive call, our algorithm invokes the angelic synthesizer to find a program consistent with the specification shown in  Eq. <ref> but it fails.

*Iteration 2b Since synthesis was unsuccessful for Eq. <ref>, our algorithm backtracks and tries a different strengthening. Specifically, since we could not find a program where the recursive calls on $T_1^R$ and $T_2^R$ return $[1;0]$ and $[2]$ respectively, we now strengthen the specification using the negation of these assumptions. This yields the following specification for the next recursive call to the synthesizer:

\begin{equation}
\label{eq:spec2b}
\begin{array}{rcl}
\mlstinline{right_spine}(T_1) = [1;0] & &
\mlstinline{right_spine}(T_2) = [2] \\[4pt]
\neg(\mlstinline{right_spine}(T_1^R) = [1;0] & \wedge &
\mlstinline{right_spine}(T_2^R) = [2])
\end{array}
\end{equation}

In this case, the angelic synthesizer returns the following program:

let rec P2(x) =
match x with
| Nil -> [0]
| Node(l,v,r) -> v::P2(r)

This program is again incorrect but it does satisfy Eq. <ref> under the angelic semantics. Indeed, a “witness" to angelic satisfaction is:

P2($T_1^R$) = [0] $\land$ P2($T_2^R$) = []

Note that this assumption is allowed under the angelic semantics since these return values on $T_1^R$ and $T_2^R$ are both consistent with Eq. <ref>. Thus, using the witness to angelic satisfaction, we now strengthen the specification as follows:

\begin{equation}
\label{eq:spec3b}
\begin{array}{rcl}
\mlstinline{right_spine}(T_1) = [1;0] & &
\mlstinline{right_spine}(T_2) = [2] \\[4pt]
\neg(\mlstinline{right_spine}(T_1^R) = [1;0] & \wedge &
\mlstinline{right_spine}(T_2^R) = [2])\\[4pt]
\mlstinline{right_spine}(T_1^R) = [0] & &
\mlstinline{right_spine}(T_2^R) = [] \\
\end{array}
\end{equation}

*Iteration 3b In the next (and last) iteration, when we invoke the angelic synthesizer on Eq. <ref>, it outputs the following program:

let rec P3(x) =
match x with
| Nil -> []
| Node(l,v,r) -> v::P3(r)

This program satisfies the specification under the actual semantics; thus, the algorithm terminates with P3 as the (correct) solution.

§.§ Angelic Synthesis using FTAs

An example FTA that accepts a program that brings the input $T_1$ to the valid output of [1;0].

As illustrated by the above discussion, a key piece of our technique is the angelic synthesizer for finding a program that satisfies the specification under the angelic semantics. Inspired by prior work on bottom-up synthesis <cit.>, our angelic synthesizer constructs a finite tree automaton (FTA) that compactly represents a set of programs. In a nutshell, FTAs generalize standard automata by accepting trees instead of words. In our setting, the states in the automata correspond to concrete program values (e.g., lists like [1;0] or []), and the trees accepted by the automaton correspond to programs (i.e., abstract syntax trees).

In order to explain our angelic synthesis approach, we first briefly review the construction from prior work <cit.>. The idea is to construct a separate automaton for each input (e.g., $T_1$ from Fig <ref>) and then take the intersection of all of these automata. To construct each automaton, we start with the given input and obtain new states by applying language constructs to the existing states. For example, given states $q_2$ and $q_3$ representing integers $2$ and $3$ and the operator $+$, we generate a new state $q_5$ (for integer 5) by applying the transition $+(q_2, q_3) \rightarrow q_5$. Since the accepting states of the FTA are those that satisfy the specification, the language of the constructed automaton includes exactly those programs that are consistent with the specification.

As illustrated by the above discussion, such an FTA-based synthesis method is bottom-up in that it evaluates complete sub-expressions on the input and combines the values of these sub-expressions to generate new values. However, prior work cannot deal with recursive functions because it is not possible to evaluate a function that has not yet been synthesized. For example, consider the recursive call to right_spine(r) where $r$ has value $T_1^R$ in our running example. Since right_spine has not yet been synthesized, we simply do not know what right_spine will return on $T_1^R$.

To deal with this challenge, our angelic synthesizer assumes that the result of the recursive call could be any value that is consistent with the specification. In particular, given a specification $\varphi$ and  FTA states $q_1, \ldots, q_n$, we assume that a recursive  invocation expression f($\overline{q}$) could evaluate to any $q_i$ as long as $q_i$ is consistent with $\varphi$. For instance, Figure <ref> shows an FTA with states $\set{T_1,T_1^R,1,[0],[1;0]}$ for the angelic synthesis problem for Eq. <ref>. Here, there is a transition right_spine$(T_1^R) \rightarrow [0]$ since the call right_spine$(T_1^R) = [0]$ is consistent with Eq. <ref>. Note that edges in Figure <ref> correspond to program syntax and [1,0] is an accepting state, so the program right_spine(x) = val(x)::right_spine(right_child(x))) is accepted by this FTA.

As illustrated by this discussion, the use of angelic semantics allows us to construct a bottom-up tree automaton despite not knowing what the recursive invocation will return on a given input. However, an obvious ramification of this is that programs accepted by the automaton may not satisfy the specification under the true semantics, which is why our method combines angelic synthesis with specification strengthening and backtracking search, as described in Section <ref>.

So, the key question becomes, how do we synthesize programs that angelically satisfy the specification? We leverage existing work on bottom-up synthesis of nonrecursive functions. In particular, we use FTA-based synthesis to generate these functions. An FTA is an automaton that describes sets of trees (eager readers can skip to our formalization in Section <ref>). In FTA-based synthesis, the core idea is that one can build up the automaton in such a way that accepted trees correspond to programs that satisfy the specification.

From a high-level, this construction is performed by maintaining a set of “reachable” values.  Programs operations are then iteratively applied to these reachable values, expanding the reachable set. For example, before applying any operations, the example $x_1$ can only reach the value $x_1$. After applying one operation (for example: “introduce constant empty list” or “extract left subtree” or “extract right subtree” or “extract node value”) the set of reachable values expands from $\set{x_1}$ to $\set{x_1,\mlstinline{L},\mlstinline{N(L,0,L)},1,\mlstinline{[]}}$.

Eventually, this process will reach a value $v$ such that $\groundSpec(x_1,v)$, like $l_1$ for $t_1$. This value corresponds to an accepting state. Any run (informally, a path from the input to a valid output) to that node will correspond to an accepting program. We show an example run in Figure <ref>.

This approach gets trickier when applying to programs with recursion. We enumerate programs by repeatedly applying transformations corresponding to partial programs to the state space. Recursive calls are also partial programs, so can we also apply them? In our example,
when we make a recursive call on N(L,0,L), what value should be returned?

Prior approaches <cit.> made use of the specification to see what value should be returned. If the specification stated that right_spine(N(L,0,L)) = [0] then when making a recursive call on right_spine(N(L,0,L)) the return would simply be [0]. Eventually, when a run is found that works on all the examples, recursive calls would perform as expected. Because right_spine(N(L,0,L)) = [0] was part of the specification, and the identified run satisfies the complete specification, the recursive call will perform as expected. This approach worked because the specifications were trace-complete. Namely, if an input-output example $v_1 \mapsto v_2$ were given, then for each subvalue $v_1'$, an input-output example $v_1' \mapsto v_2'$ would also have to part the specification.

Possible outputs from a recursive call to N(L,0,L). same as above, let me know if this is helpful.

In our example, the provided input-output specifications are unfortunately not trace complete. We extend this approach to work on our (more general) specifications. At the start, we know that any call to N(L,0,L) can return a value $v$ such that $\groundSpec_1(\mlstinline{N(L,0,L)},v)$. Thus, when iteratively applying program operations, when applying a recursive right_spine to N(L,0,L), we can return any arbitrary value $v$. Of course, we cannot interact with an FTA with infinitary fanout, so f can only transform N(L,0,L) to output values that are reachable in a fixed number of operations. A few examples of such transformations is shown in Figure <ref>

Runs in these programs no longer correspond to programs that are guaranteed to be fully correct. Programs accepted by this automaton are exactly those that are angelically correct. If a program is accepted by this nondeterministic FTA, then that program angelically evaluates to an accepting value. We then use this run to extract the witness, and refine the specification.

§.§ Incremental Synthesis

As we saw from Equations <ref>, <ref>,  and <ref>  from Section <ref>, successive calls to the synthesis algorithm involve increasingly strong specifications. In particular, if the synthesis algorithm is invoked on specification $\varphi$ in the $i$'th iteration, then the specification in the $i+1$'th iteration is of the form $\varphi \land \psi$. We exploit this incremental nature of the algorithm to make angelic synthesis more efficient.

In particular, recall that our angelic synthesizer based on FTAs constructs a different FTA for each input and then takes their intersection. Thus, given a specification $\varphi \land \psi$ where $\varphi$ is the old specification, we can simply construct a new FTA for $\psi$ and then take its intersection with the old FTA for $\varphi$. Hence, performing angelic synthesis using FTAs allows us to reuse all the work from prior iterations.

Note that the specification $\groundSpec_1$ was used multiple times in our extended example. When synthesizing a program that satisfied both $\groundSpec_{2a}$ and $\groundSpec_{2b}$, the programs had to also satisfy $\groundSpec_{1}$. When synthesizing a program that satisfied $\groundSpec_{3b}$, the program also had to satisfy $\groundSpec_{2b}$. By using FTAs, has a representation of all programs up to a given size that satisfy $\groundSpec_1$. To refine this to those that satisfy $\groundSpec_{2a}$, merely has to intersect the programs that satisfy the new constraints with those that satisfied the old ones.

While incremental synthesis is helpful within a given synthesis, it can also be helpful when is used interactively. Say, when using a user gave the specification $\groundSpec_1$, but they actually wanted to synthesize an inorder traversal of the tree. After realizing they had underspecified inorder they refine the specification to $\groundSpec_1' = \groundSpec_1 \wedge f(\mlstinline{N(N(L,3,L),1,L)}) = [3;1]$.

At it's simplest, we can simply reuse the specification $\groundSpec$ like we did within the program. But we can also memoize knowledge that $\groundSpec_{2a}$ was not satisfiable, and skip any specification that is stronger than it. In effect, we can restart the synthesis at the same place in the call stack as $\groundSpec_{3b}$, updated to be $\groundSpec_{3b}' = \groundSpec_{eb} \wedge f(\mlstinline{N(N(L,3,L),1,L)}) = [3;1]$.

§.§ Generalization to Arbitrary Logical Specs

In our example so far, we illustrated the synthesis algorithm on the simple input-output examples from Eq. <ref>. However, our method can be generalized to more complicated logical specifications using the standard counterexample-guided inductive synthesis (CEGIS) paradigm. In particular, since our core synthesis algorithm takes as input ground formulas as opposed to input-output examples, it can be easily incorporated within the CEGIS loop to handle more general logical specifications. For instance, our method can produce the correct implementation of right_spine given the following logical specification:

\[
\phi(in,out) := \mlstinline{no_left_subchildren}(in) \Rightarrow (\mlstinline{tree_size}(in) == \mlstinline{list_size}(out))
\]

where tree_size  and list_size return the number of elements in a tree and list respectively,  and no_left_subchildren returns true if the left child of every node in the tree is a leaf.

§ PROBLEM STATEMENT

$P$                    |rec f($x$) = $\ e$|

$e$                    $x$

|     |$e_1\ e_2$|     |     |unit|

|     |inl $\ e$|     |     |inr $\ e$|

|     |unl $\ e$|     |     |unr $\ e$|

|     |fst $\ e$|     |     |snd $\ e$|

|     |($e_1,\ e_2$)|     |     |switch $\ e_3$ on inl _| $\rightarrow e_1$ | inr _ $\rightarrow e_2$

$v$                    |unit|     |     |($v_1,\ v_2$)|

|     |inl $\ v$|     |     |inr $\ v$|

A functional ML-like language with explicit recursion in which we synthesize programs. The nonterminal $P$ denotes programs in this language, and the nonterminal $v$ denotes values in this language.

In this section, we present our problem statement, which  is synthesizing recursive programs in a simple ML-like language  with products and sums (see Figure <ref>). Without loss of generality, we assume that programs take a single input, as we can represent multiple inputs using tuples (i.e., pairs with nested pairs). Given a program $P$ and a concrete input $v$, we use the notation $\SemanticsOf{P}(v)$ to denote the result of executing $P$ on input $v$ according to the semantics presented in Figure <ref>.

e_2 ⇓v_2

e_1[!rec f!$(x)=e_1$/!f!,v_2/x] ⇓v_3

(!rec f!$(x)=e_1$) e_2 ⇓v_3

!unit! ⇓!unit!

e_1 ⇓v_1

e_2 ⇓v_2

(e_1,e_2) ⇓(v_1,v_2)

e ⇓(v_1,v_2)

!fst $\;e \Downarrow v_1$!

e ⇓(v_1,v_2)

!snd $\;e \Downarrow v_2$!

e ⇓v

!inl! $e \Downarrow$ !inl! $v$

e ⇓v

!inr! $e \Downarrow$ !inr! $v$

e ⇓!inl! v

!unl! e ⇓v

e ⇓!inr! v

!unr! e ⇓v

e_3 ⇓!inl! v_3

e_1 ⇓v_1

!switch! $e_3$ !on inl! $\_ \to e_1$ !inr! $\_ \to e_2$

e_3 ⇓!inr! v_3

e_2 ⇓v_2

!switch! $e_3$ !on inl! $x_1 \to e_1$ !inr! $x_2 \to e_2$

Program Semantics. The symbols $e$ range over expressions and $v$ range over values. Both $f$ and $x$ denote arbitrary free variables.
If $P=\mlstinline{rec f}(x)=e$
and $P\ v \Downarrow v'$
then $\SemanticsOf{P}(v) = v'$.

Our goal in this paper is to synthesize a single recursive procedure f from a given specification, which is represented as a ground formula $\Spec$. We assume that $\Spec$ always contains a special uninterpreted function symbol $f$ which refers to the function to be synthesized. More formally, we define ground specifications as follows:

(Ground specification)
A ground specification is a boolean combination of atomic formulas of the form $f(i) \opr c$ where $f$ denotes the function to be synthesized, $i$ and $c$ are constants (with $i$ being the input), and $\opr$ is a binary relation.

(Satisfaction of ground spec)
Given a program $P$ defining function $f$, we say that $P$ satisfies a ground specification $\Spec$, denoted $P \models \Spec$, iff the following condition holds:

\[
P \models \Spec \ \ \Longleftrightarrow \ \  \models \Spec\big [\SemanticsOf{P}(x) / f(x) \big ]
\]

where the notation  $\Spec[\SemanticsOf{P}(x) / f(x)]$ denotes the formula  with every ground term  $f(v_i)$ is replaced by $\SemanticsOf{P}(v_i)$.

Problem Statement: Given a ground specification $\Spec$, find program $P$ such that $P \models \Spec$.

Note that ground specifications are quite powerful: synthesizers that can generate programs from ground specifications can also perform synthesis from a number of specification classes.
For example we can always encode I/O examples as ground formulas. but not vice versa.

Consider the set of input-output examples $\{1 \mapsto 2, 2 \mapsto 3 \}$. We can encode this specification in our format using the ground formula $f(1)= 2 \land f(2) = 3$. In general, I/O examples correspond to specifications of the form:

\[
\bigwedge_k f(i_k) = o_k
\]

where $(i_k, o_k)$ are input-output pairs.

Furthermore, we can also lift  synthesis from ground specifications to an even more general class of specifications  using the well-known CEGIS paradigm (see Figure <ref>). Given a fixed set of inputs $I$ and a general predicate $\varphi$ with variables (representing inputs), one can convert this into a ground formula of the form $\bigwedge_{i \in I}\varphi(i)$ where each $i$ a counterexample returned by the verifier. Since the CEGIS paradigm invokes the verifier to add new counterexamples if the synthesized program is not correct,

synthesis from ground formulas immediately provides a way to perform synthesis from more general logical specifications.

Consider the problem of synthesizing a function that returns a value greater than its input for all positive inputs. The specification for such a function is of the form $x>0 \Rightarrow f(x) > x$. While this specification is not a ground formula, we can embed our synthesis technique into the CEGIS paradigm and reduce it to inductively synthesizing programs from ground specifications of the form:

\[
\bigwedge_k f(i_k) > i_k
\]

where each $i_j$ is a positive integer returned as a counterexample by a verifier.

Counterexample-guided inductive synthesis. Since the input to the inductive synthesizer is a ground formula, our approach can be lifted to a general class of specifications using the CEGIS paradigm.

Given a program $P$ defining function $f$ and a specification $\Spec$, we use the notation $P \models \Spec$ to indicate that $P$ satisfies specification $\Spec$, i.e.,

\[
\forall (v, v'). \  \SemanticsOf{P}(v) = v'  \Rightarrow {\textsc{Valid}}(\Spec[v/x, v'/y])
\]

where Valid indicates logical validity. In other words, a program $P$ satisfies a given specification $\Spec$ iff all input-output pairs of $P$ are models of formula $\Spec$.

§.§ Background on CEGIS

§.§ Preliminaries

Given a program $P$ and a concrete input $v$, we use the notation $\SemanticsOf{P}(v)$ to denote the result of executing $P$ on input $v$ according to the semantics presented in Figure <ref>. We also use the notation $P \models \Spec$ to indicate that $P$ satisfies specification $\Spec$, i.e.,

\[
\forall (v, v'). \  \SemanticsOf{P}(v) = v'  \Rightarrow {\textsc{Valid}}(\Spec[v/x, v'/y])
\]

where Valid indicates logical validity. In other words, a program $P$ satisfies a given specification $\Spec$ iff all input-output pairs of $P$ are models of formula $\Spec$.

(Ground specification) A ground specification $\groundSpec$ is a set of pairs  $(v, \phi(y))$   where $v$ is a concrete input (i.e., constant) and $\phi(y)$ is a logical formula over output variable $y$.

In other words, a ground specification constrains how the function should behave on specific concrete inputs. In the remainder of this paper, we assume that each specific input $v$ occurs only once in the ground specification. In other words, there is at most one element of the form $(v,\_) \in \groundSpec$.

The ground specification $\set{(0, y > 0), (1, y > 1)}$ indicates that the synthesized function  should return a value greater than  $0$ on input $0$ and that it should return a value greater than $1$ on input $1$.

Note that input-output examples are a special case of ground specifications of the form $\set{(v_1, y=v_1'), \ldots, (v_n, y = v_n')}$.

Given a ground specification , the domain of the ground specification, denoted $\domain(\groundSpec)$, is defined as $ \set{v \ | \ (v,\Spec(y)) \in \groundSpec}$. Also,
we use the notation $\groundSpec(v)$ to denote the specification for a specific input $v$. More formally,

\[
\groundSpec(v) = \left \{
\begin{array}{ll}
\phi &  (v, \phi) \in \groundSpec \\
\true & \emph{otherwise}
\end{array}
\right .
\]

(Conjunction of ground specs) Given two ground specifications $\groundSpec_1$ and $\groundSpec_2$, we define their conjunction, denoted $\groundSpec_1 \sqcap \groundSpec_2$, as follows:

\[
\groundSpec_1 \sqcap \groundSpec_2 = \{ (v, \groundSpec_1(v) \land \groundSpec_2(v)) \ | \ v \in \domain(\groundSpec_1) \lor v \in \domain(\groundSpec_2) \}
\]

The result of conjoining the ground specification  $\set{(0, y \geq 0), (1, y > 1)}$ with $\set{(0, y \leq 0), (2, y = 2)}$ is:

\[
\set{(0, y \geq 0 \land y \leq 0), (1, y>1), (2, y = 2)}
\]

(Satisfaction of ground specification) We say that a program $P$ satisfies a ground specification $\set{(v_1, \phi_1(y)), \ldots, (v_n, \phi_n(y))}$ iff:

\[
P \models \bigwedge_{i=1}^n (x = v_i) \rightarrow \phi_i(y)
\]

§.§ CEGIS and Revised Problem Statement

Our high-level approach is to solve the synthesis problem using a standard counterexample-guided inductive synthesis (CEGIS) loop  wherein an inductive synthesizer proposes candidate programs to a verifier (see Figure <ref>). Specifically, the inductive synthesizer in the CEGIS paradigm takes as input  a ground specification $\groundSpec$ and returns a candidate program $P$ such that $P \models \groundSpec$. However, the program returned by the inductive synthesizer may or may not satisfy the actual specification $\Spec$. Thus, in the CEGIS paradigm, a verifier is invoked to check whether $P \models \Spec$. If this is not the case,  the verifier returns a new counterexample of the form $\chi' = \set{(v, \phi(y))}$, where $v$ is the input $P$ fails on, and $\phi(y) = \Spec[v/x]$. Then, the inductive synthesizer is re-invoked with the stronger ground specification $\groundSpec \sqcap \groundSpec'$, and this process continues until the program returned by the inductive synthesizer is verified.

Since our high-level approach is to use the CEGIS paradigm, the rest of this paper focuses on the inductive synthesis problem defined as follows:

(Inductive synthesis problem)
Given a ground specification $\groundSpec$, the inductive synthesis problem is to find a program $P$ in the language of Figure <ref> such that $P \models \groundSpec$.

In the remainder of this paper, we use the term synthesis to mean inductive synthesis from ground specifications.

Remark. Note that a programming-by-example (PBE) technique is, in general, not sufficient to
implement the inductive synthesizer in the CEGIS paradigm because input-output examples are a very restricted form of ground specification. For example, consider a specification of the form $y > x$, meaning that the synthesized function's output should be greater than the input. In this case, the counterexamples returned by the verifier will be a specific input $c$ that violates the specification; however, the specification does not state what exact output the function should return on $c$. Thus, a PBE technique cannot be embedded in the CEGIS paradigm to handle arbitrary logical specifications of the form $\Spec(x, y)$.

§ ANGELIC RECURSION

As mentioned earlier, our method is based on bottom-up synthesis, which requires the ability to execute sub-expressions of the program being synthesized. Since this is not feasible for recursive procedures, we introduce the notion of angelic recursion and angelic satisfaction.

(Angelic recursion) Given a recursive procedure $P$, the angelic semantics of $P$ with respect to specification $\Spec$, denoted $\SemanticsOf{P}^\Spec$, is defined in Figure <ref>. These semantics are very similar to the semantics in Figure <ref>; the key difference lies in how recursion is performed. When performing a recursive call f($v$), the result can be any $v'$ where $f(v) = v'$ is consistent with the specification. Thus, $\SemanticsOf{P}^\Spec(v)$ yields a set of values $\Values$.

e ⇓^φv

𝖲𝖠𝖳(f(v) = v' ∧φ)

!f! e ⇓^φv'

!unit! ⇓^φ!unit!

e_1 ⇓^φv_1

e_2 ⇓^φv_2

(e_1,e_2) ⇓^φ(v_1,v_2)

e ⇓^φ(v_1,v_2)

!fst $\;e \Downarrow^\varphi v_1$!

e ⇓^φ(v_1,v_2)

!snd $\;e \Downarrow^\varphi v_2$!

e ⇓^φv

!inl! $e\Downarrow^\varphi$ !inl! $v$

e ⇓^φv

!inr! $e \Downarrow^\varphi$ !inr! $v$

e ⇓^φ!inl! v

!unl! e ⇓^φv

e ⇓^φ!inr! v

!unr! e ⇓^φv

e_3 ⇓^φ!inl! v_3

e_1 ⇓^φv_1

!switch! $e_3$ !on inl! $x_1 \to e_1$ !inr! $x_2 \to e_2$

e_3 ⇓^φ!inr! v_3

e_2 ⇓^φv_2

!switch! $e_3$ !on inl! $x_1 \to e_1$ !inr! $x_2 \to e_2$

P = |rec f|(x) = e

e[v/x] ⇓^φv'

v' ∈P^(v)

Angelic Semantics. The key difference between angelic semantics and standard semantics lies in the first rule, for recursive calls.

e ⇓^(v,τ)

!f! e ⇓^v' τ[(v,v')]

!unit! ⇓^(!unit!,[])

e_1 ⇓^(v_1,τ_1)

e_2 ⇓^(v_2,τ_2)

(e_1,e_2) ⇓^((v_1,v_2),τ_1τ_2)

(e ⇓^(v_1,v_2),τ)

(!fst $\;e \Downarrow^\Spec v_1$!,τ)

(e ⇓^(v_1,v_2),τ)

(!snd $\;e \Downarrow^\Spec v_2$!,

(e ⇓^v,τ)

(!inl! $e \Downarrow^\Spec$ !inl! $v$,τ)

(e ⇓^v,τ)

(!inr! $e \Downarrow^\Spec$ !inr! $v$,τ)

(e ⇓^!inl! v,τ)

(!unl! e ⇓^v,τ)

(e ⇓^!inr! v,τ)

(!unr! e ⇓^v,τ)

(e_3 ⇓^!inl! v_3,τ_3)

(e_1 ⇓^v_1,τ_1)

(!switch! $e_3$ !on inl! $x_1 \to e_1$ !inr! $x_2 \to e_2$

(e_3 ⇓^!inr! v_3,τ_3)

(e_2 ⇓^v_2,τ_2)

(!switch! $e_3$ !on inl! $x_1 \to e_1$ !inr! $x_2 \to e_2$

Angelic Semantics. If $P = \mlstinline{let rec f}(x) = e$, then
$\SemanticsOf{P}^\varphi(v) = \set{v' \SuchThat \exists \tau. e[v/x] \Downarrow^\phi (v',\tau)}$.

Intuitively, angelic recursion is useful in our setting because it allows us to “execute" a recursive program without knowing the exact behavior of recursive calls.

Let $P$ be the program rec f(x) = if x=0 then 1 else f(x-1) and suppose that $\Spec = f(0) > 0$. Then, $\SemanticsOf{P}^\Spec(0) = \set{1}$, and $\SemanticsOf{P}^\Spec(1) = \set{y \mid y > 0}$. In particular, for input $1$, $f$ contains a recursive invocation on input $0$, and the angelic semantics allows the recursive call to return any value greater than $0$. Thus, $\SemanticsOf{P}^\Spec(1)$ is exactly the set of positive integers.

Next, we define a notion of angelic satisfaction:

(Angelic satisfaction on input)
Given a program $P$ defining function $f$, we say that $P$ angelically satisfies specification $\Spec$ on input $v$, denoted $P \angelicmodels_v \Spec$, iff the following condition holds:

\[
P \angelicmodels_v \Spec \ \Longleftrightarrow \  \exists v'. \ v' \in \SemanticsOf{P}^\Spec(v) \land \mathsf{SAT}(f(v) = v' \wedge \varphi)
\]

Next, we generalize this notion of angelic satisfaction from a single input to all inputs:

(Angelic satisfaction)
A program $P$ angelically satisfies specification $\Spec$, denoted $P \angelicmodels \Spec$,  iff for all possible inputs $v$, we have  $P \angelicmodels_v \Spec$.

Note that angelic satisfaction ($P \angelicmodels \Spec$) is a much weaker notion than standard satisfaction ($P \models \Spec$).
This is illustrated by the following example:

Let $P$ be the program rec f(x) = if x=0 then 1 else f(x-1) and suppose that $\Spec = f(0) > 0 \land f(1) > 1$. Then, $P \angelicmodels \Spec$, as $\forall x. \  x+1 \in \SemanticsOf{P}^\Spec(x)$. However, clearly, this program does not satisfy $\Spec$ with respect to the standard semantics because we have $\SemanticsOf{P}(1) = 1$.

If a program $P$ angelically satisfies a specification $\Spec$, we can define a witness to angelic satisfaction as follows:

(Witness to angelic satisfaction)
Let  $P$ be a program  such that $P \angelicmodels \Spec$. Then, a witness $\witness$  to angelic satisfaction of $P$ is a formula $\bigwedge_i f(c_i) = c_i'$ such that, if $P \models \witness$, then $P \models \Spec$.

Intuitively, a witness to angelic satisfaction specifies what the recursive calls in $P$ must return in order for $P$ to actually satisfy the specification. We discuss how to find these witnesses in Section <ref>.

Consider the program rec f(x) = if x=0 then 1 else f(x-1)+1 and  the ground specification  $f(1) > 1 \land f(2) > 2$. This program angelically satisfies the specification in an execution where the recursive call returns $f(0) = 1$ and $f(1) = 2$. Thus, $f(0) = 1 \land f(1) = 2$ is a witness to angelic satisfaction. Of course, note that angelic witnesses are not unique. For example, $f(0) = 2 \land f(1) = 3$ is also a witness to angelic satisfaction.

Next, we introduce the concept of an angelic recursion trace (or angelic trace) for short.

(Angelic trace) An angelic trace $\tau$ for a recursive procedure $P$ with angelic semantics $\Spec$ is a sequence $[(i_1, o_i), \ldots, (i_n, o_n)]$ where $i_k$ is the input on the $k$'th recursive call to $P$ and $o_k$ is the output.  More formally, Figure <ref> defines the set of all angelic traces of a program $P$ in the form of a predicate $\mathsf{Trace}(P \Downarrow^\Spec v, \tau)$ — i.e., if $\mathsf{Trace}(P \Downarrow^\Spec v, \tau)$ for some $\tau$, then $\tau$ is an angelic trace of $P$.

We illustrate the concept of angelic trace with an example:

Consider again the program rec f(x) = if x=0 then 1 else f(x-1) and suppose that $\Spec(x,y) = y > x$. Here, $[(1,2)]$ and $[(0,1), (1,3)]$ are both possible angelic traces of this program. However, $[(1,0)]$ is not since the inout-output pair $(1,0)$ violates the specification. Similarly,  $[(0,1), (2,3)]$ is also not a valid angelic trace because if there is a recursive call on inputs $0$ and $2$, there must also be

A key component of our algorithm is an iterative refinement loop, where the specification is refined to include the assumptions made in the angelic semantics. These assumptions take the form of angelic traces. An angelic trace $\tau$ is a sequence $(i_1, o_1), \ldots,
(i_n, o_n)$ where the $j$’th recursive call to f has input
$i_j$ and output $o_j$. The relation $\Trace(v' \in \SemanticsOf{P}^\Spec,\tau)$ means that $v' \in \SemanticsOf{P}^\Spec$ and $\tau$ serves as a trace for that evaluation. We give the deduction rules for  in Figure <ref>.

(e ⇓^v,τ)

(!f! e ⇓^v',τ[(v,v')])

(!unit! ⇓^!unit!,[])

(e_1 ⇓^v_1,τ_1)

(e_2 ⇓^v_2,τ_2)

((e_1,e_2) ⇓^(v_1,v_2),τ_1τ_2)

(e ⇓^(v_1,v_2),τ)

(!fst $\;e \Downarrow^\Spec v_1$!,τ)

(e ⇓^(v_1,v_2),τ)

(!snd $\;e \Downarrow^\Spec v_2$!,

(e ⇓^v,τ)

(!inl! $e \Downarrow^\Spec$ !inl! $v$,τ)

(e ⇓^v,τ)

(!inr! $e \Downarrow^\Spec$ !inr! $v$,τ)

(e ⇓^!inl! v,τ)

(!unl! e ⇓^v,τ)

(e ⇓^!inr! v,τ)

(!unr! e ⇓^v,τ)

(e_3 ⇓^!inl! v_3,τ_3)

(e_1 ⇓^v_1,τ_1)

(!switch! $e_3$ !on inl! $x_1 \to e_1$ !inr! $x_2 \to e_2$

(e_3 ⇓^!inr! v_3,τ_3)

(e_2 ⇓^v_2,τ_2)

(!switch! $e_3$ !on inl! $x_1 \to e_1$ !inr! $x_2 \to e_2$

Definition of angelic recursion trace. If $P = \mlstinline{let rec f}(x) = e$, then
$\Trace(v' \in \SemanticsOf{P}^\varphi(v),\tau)$ if $\Trace(e[v/x] \Downarrow^\varphi v',\tau)$.

We can lift a trace $\tau = (i_1,o_1),\ldots,(i_n,o_n)$ to a ground specification:

\[
\groundSpec(\tau) = \bigsqcap_j \set{(i_j,y = o_j) }
\]

§  SYNTHESIS ALGORITHM USING ANGELIC EXECUTION

[1]
input: Ground specification output: A program $P$ or $\bot$
global: $\Omega$ is a learned anti-specification, initially $\emptyset$
$\text{result} \gets \Call{SynthesizeAngelic}{\groundSpec \land \bigwedge_{\phi_i \in \Omega} \neg\phi_i }$
$\Omega \gets \Omega \cup \kappa$
$P \models \groundSpec$ $P$
$\mathit{P} \gets \Call{Synthesize}{\groundSpec \land \witness}$
$\mathit{P} = \bot$
Synthesize$\groundSpec \land \neg \witness$

Core Recursive Synthesis Algorithm

In this section, we describe our top-level synthesis algorithm based on angelic recursion. While this synthesis algorithm does not specify whether to construct programs in a top-down or bottom-up fashion, we emphasize that it is the use of angelic recursion that makes it possible to implement its key components using a bottom-up approach (as we discuss in the next section).

<ref> shows the high-level structure of our synthesis algorithm. The procedure Synthesize takes as input a ground specification $\groundSpec$  and returns either a program $P$ or $\bot$ to indicate that synthesis is unsuccessful. Internally, the algorithm also maintains a global variable, namely set $\Omega$, that we refer to as an anti-specification which is used for pruning the search space. In particular, $\Omega$ is constructed in such a way that any program that satisfies $\phi \in \Omega$ is guaranteed to not satisfy the desired specification $\chi$, i.e.:

\begin{equation}\label{eq:anti-spec}
\forall P. \ \forall \phi \in \Omega. \ P \models \phi \Rightarrow P \not \models \chi
\end{equation}

Since the contrapositive of <ref> is

$$\forall P. \ \forall \phi \in \Omega. \ P \models \chi \Rightarrow P \not\models \phi$$

which implies that $P$ must satisfy
$\bigwedge_{\phi_i \in \Omega} \neg \phi_i$ in order to also satisfy $\chi$, we can use $\Omega$ to construct a stronger specification and thereby reduce  the search space.

Our synthesis procedure starts by invoking a procedure call SynthesizeAngelic (line <ref>) which takes as input a specification that the returned program must satisfy under the angelic semantics. In particular, given a (ground) specification $\varphi$, SynthesizeAngelic either returns failure or a program $P$ that angelically satisfies $\varphi$ (i.e., $P \angelicmodels \varphi$). If the output is failure (meaning that there is no program in the search space that satisfies $\varphi$), SynthesizeAngelic also returns an anti-specification (i.e., set of formulas) $\kappa$ that serves as an “explanation" of why angelic synthesis failed. In particular, $\kappa$ has the property, for every $\psi \in \kappa$, there is no program in the search space that satisfies $\psi$. Thus, if SynthesizeAngelic returns  $\mathsf{Failure}(\kappa)$, we  add $\kappa$ to  $\Omega$ (line <ref>).

On the other hand, if SynthesizeAngelic returns a program $P$, our synthesis procedure checks whether $P$ satisfies the specification $\groundSpec$ under the true semantics (line <ref>). If so, then it  returns $P$ as a valid solution to the synthesis problem. Otherwise, it uses the witness $\witness$ to angelic satisfaction returned by SynthesizeAngelic to construct a stronger specification. In particular, recall that such a witness $\witness$ encodes assumptions that an angelic execution makes in order to satisfy the specification. Thus, we strengthen the specification as $\chi \land \witness$ and  re-attempt synthesis by recursively invoking Synthesize on this stronger specification (line <ref>). If synthesis is successful, we return the resulting program as a solution (line <ref>); otherwise, we backtrack and recursively invoke Synthesize with the alternative specification $\chi \land \neg \witness $ (line <ref>), which ends up ruling out $\witness$ from the search space.  Observe that  the anti-specification $\Omega$ also grows during the recursive calls; thus, the second recursive call at line <ref> actually prunes more programs than just those satisfying $\witness$.

The following theorems state the soundness and completeness of our synthesis algorithm.

If Synthesize($\chi$) returns a program $P$, then we have $P \models \chi$.

Follows directly from line <ref> of Algorithm <ref>.

If $\Synthesize(\chi)$ returns $\bot$, then there is no program that satisfies $\chi$ under the assumption that (1) is complete, and (2) if   returns $\mathsf{Failure}(\kappa)$, then $\kappa$ satisfies the assumption from <ref>.

The proof is in
Section <ref>.
the full version of the paper.

Remark. A simpler alternative to the specification strengthening approach in Algorithm <ref> would be to perform enumerative search over the angelic synthesis results as opposed to strengthening the specification. However, as we show empirically in Section <ref>, this simpler alternative is not  as effective. In particular,  many programs that angelically satisfy the specification are wrong due to shared incorrect assumptions about recursive calls; thus, our proposed algorithm allows ruling out many incorrect programs at the same time.

In this section, we describe the algorithm in the context of a generic version space. We describe our FTA instantiation of the algorithm in <ref>. We assume the following 3 functions on version spaces in this section, and describe our implementations of them in the next section.

* . Calling $\CreateVersionSpace(\groundSpec)$ returns a set of programs $P$ such that $P \models^\groundSpec \groundSpec$.

* . Calling $\GetAcceptingTraces(\vs,\groundSpec)$ returns a program $P$ and a set of traces $T$ such that for all $(i,\phi(i)) \in \groundSpec$ there exists $\tau_i \in T$ and output $o$, such that $\Trace(o \in \SemanticsOf{P}^\groundSpec,\tau_i)$.

* . Calling $\Conflict(\vs,\groundSpec)$ will return a ground formula $\kappa$ such that $\groundSpec \Rightarrow \kappa$ and $\Synthesize(\kappa) = (\bot,\kappa)$. In other words, identifies unsatisfiable core of the ground specification.

* . Calling $\Prohibit(\vs,\kappa)$ will return an updated version space $\vs'$, such if $(P,T) = \GetAcceptingTraces(\vs')$, then $\bigsqcap_{\tau \in T} \groundSpec(\tau) \not\Rightarrow \kappa$.

Given ground specification $\groundSpec$ our algorithm calls () to generate an initial set of candidate programs. These programs satisfy the specification with angelic semantics, but do not necessarily satisfy the specification with standard semantics.

Running Example.
If the ground specification $\groundSpec$ was

then the program rec f(x).if x==[] then [] else f(tl x) would be accepted by $\CreateVersionSpace(\groundSpec)$.

Our algorithm first pops a candidate program $P$ and a set of traces $T$ from the automaton. If there is no accepting program, then no program satisfies the spec, and we can return $\bot$, as well as the unsatisfiable core $\kappa$.

If there is a program $P$ with accepting traces $T$, we first check whether $P$ satisfies with standard semantics – if it does, we simply return $P$. If it does not, we recursively call with an updated ground specification $\groundSpec\ \sqcap\ \bigsqcap_{\tau \in T} \groundSpec(\tau)$. This refined specification ensures that accepted programs transforms the inputs in the same way traces in $T$ assumes they were transformed.

If $\textsc{SynthesizeAngelic}$ identified the candidate program $P$ and witness :

\begin{align*}
P & = \mlstinline{rec f(x).if x==Nil then [] else f(rightsub x)} \\
\witness & = f(\mlstinline{N(L,0,L)}) = [0;1] \wedge f(\mlstinline{L}) = [2]\\
\end{align*}

for the ground specification $\groundSpec$ of:

\[
\groundSpec = \Spec(x_1,f(x_1)) \wedge \Spec(x_2,f(x_2))
\]

where $x_1 = \mlstinline{N(L,1,N(L,0,L))}$ and $x_2 = \mlstinline{N(L,2,L)}$.

Next, our algorithm will make a recursive call to $\textsc{SynthesizeAngelic}(\groundSpec \wedge \omega)$. Once this call results in a failure, we know that the refined constraint $\groundSpec \wedge \omega$ is unrealizeable. So we add the additional constraint: $\groundSpec \wedge \neg\omega$, to prevent any runs with witness $\omega$ from being found again, and recurse on this updated constraint. If both $\groundSpec \wedge \omega$ and $\groundSpec \wedge \neg\omega$ are unrealizeable, the original spec is unrealizeable, and we return $\bot$.

§ BOTTOM-UP ANGELIC SYNTHESIS USING TREE AUTOMATA

Recall that our top-level synthesis procedure (Algorithm <ref>) uses a key procedure called SynthesizeAngelic to find a program that satisfies the specification under the angelic semantics. In this section, we describe a realization of the angelic synthesis algorithm using bottom-up finite tree automata. Towards this goal, we first review tree automata basics and then describe the angelic synthesis algorithm.

§.§ Angelic Synthesis Algorithm

[1]
input: A ground specification $\groundSpec$
output: $\mathsf{Success}(P,\witness)$ for program $P$ and angelic witness $\witness$; $\mathsf{Failure}(\kappa)$ for anti-specification $\kappa$
$\kappa \gets \emptyset$
$\varphi \in \mathsf{DNFClauses}(\groundSpec)$

$\text{first} \gets \mlstinline{true}$
$\psi \gets \mlstinline{true}$
$f(v) \  \emph{op} \ v' \in \varphi$
$\psi \gets \psi \wedge f(v) \  \emph{op} \ v'$
$\fta \gets \BuildAngelicFTA(v,\varphi)$
$\text{first}$ $\fta^* \gets \fta$
$\fta^* \gets \Intersect(\fta^*, \fta)$
$\text{first} \gets \mlstinline{false}$
$\LanguageOf{\fta^*} = \emptyset$ break

$\LanguageOf{\fta^*} \neq \emptyset$
$(P,L) \gets \GetAcceptingRun(\fta^*)$
$\witness \gets \GetWitness(P,L)$
$\kappa \gets \kappa \cup \set{\psi}$

Angelic synthesis procecdure based on tree automata

In this section, we describe an FTA-based implementation of the SynthesizeAngelic procedure that is invoked at line 2 of Algorithm <ref>. This procedure, which is summarized  in Algorithm <ref>, takes as input a ground specification $\chi$ and returns one of two things: If angelic synthesis is successful, the output is a program $P$ that angelically satisfies $\chi$, together with a witness $\witness$ to angelic satisfaction. On the other hand, if there is no program that angelically satisfies $\chi$, SynthesizeAngelic returns a set of ground formulas $\kappa$ that serve as an anti-specification satisfying Equation <ref>.

The algorithm starts by converting the specification $\chi$ to disjunctive normal form (DNF) at line 3 and iterates over each of the DNF clauses (line 3–17). If there is a program $P$ that angelically satisfies  any clause $\varphi$, then it returns $P$ (and its corresponding witness $\witness$) as a solution (line 16). On the other hand, if it exhausts all clauses without successfully finding a program, the algorithm returns $\mathsf{Failure}$ at line 18.

In more detail, each clause $\varphi$ is a conjunction of atomic predicates of the form $f(v) \opr v'$ where $v$ and $v'$ are constants (since $\chi$ is a ground specification). The nested loop at lines 6–12 iterates over all of these predicates, builds an FTA $\fta$ for each of them (line 8), and constructs a version space $\fta^*$ satisfying all of them by taking the intersection of all FTAs (line 10).  If the language of the resulting automaton $\fta^*$ becomes empty (line 12), then this means there is no program satisfying the current clause so the algorithm moves on to the next clause.

On the other hand, if the final version space $\fta^*$ is non-empty after processing an entire clause (line 13), then we know that there exists a program that satisfies this clause under the angelic semantics. In this case, the algorithm finds an accepting run of this FTA, extracts a witness $\witness$ to angelic satisfaction by calling the GetWitness procedure at line 15, and returns “success" at line 16.

Finally, if the algorithm exhausts all DNF clauses without finding a program, it returns $\mathsf{Failure}$ at line 18. In particular, the anti-specification $\kappa$ at line 18 consists of a set of unsynthesizable cores (UC), where each UC $\psi$ is a conjunction of predicates such that there is no program $P$ that angelically satisfies $\psi$. Thus, it is always safe to strengthen the specification using the negation of an unsynthesizable core.

In the remainder of this subsection, we discuss the BuildAngelicFTA and GetWitness  procedures in more detail.

*Recursive Calls

When performing a recursive call, we must mirror the angelic semantics of the language. For each value $v$, if $\varphi(v,v')$, then rec_call(v) $\rightarrow$ v' is a valid transition. By using the angelic semantics in our FTA constructions, recursive calls are immediately addressed.

When creating a switch, we would like to be able to permit “garbage” syntax on the side of the branch that is not taken. For example, consider the following expression:

rec f(x) =
switch x on
| inl -> unl x
| inr -> unr x

If we attempted to generate programs without special rules for switches, this program could never get generated. The Prod rule takes existing states (in other words, explored values) and merges them with one piece of syntax. It then evaluates the newly generated expression, and finds the result. However, if $i = \mlstinline{inl unit}$, then the subexpression unr x could never be generated, as that does not evaluate to any value. In the same way, if $i = \mlstinline{inr unit}$, then the subexpression unl x could never be generated.

There are two solutions to this: one can add a sentinel “accept everything” state, and leave the branch not taken unconstrained, or one could add an “error” value, and have previously stuck expressions evaluate to “error”s.

We went with the first approach, though the second approach would also have worked. In this approach, we added the wildcard state , and have that state always be a valid transition to itself. Notably, this wildcard state is not final, if it were the automata would accept every tree!

*Finitization The above procedure describes rules for constructing an FTA that accepts all programs that transforms the input values to the output values. However, the rules in Figure <ref> permit trees with an arbitrarily large number of states. To address this, we synthesize programs where only a fixed number of Prod rules are permitted. If no programs satisfy the specification with a given number of applications, we increase that number, and resynthesize I don't want to pipe this number throughout all our formalisms, as its standard and would just serve to distract. Is it ok to just mention it here, or should I do that piping? Maybe mention it earlier on in the algorithm? Any thoughts would be appreciated.. When we call $\BuildAngelicFTA$, it will derive an FTA using the inference rules of Figure <ref>, but only with a fixed number of applications of Prod.

Furthermore, these trees can have infinite fanout when making a recursive call on an value that has an infinite number of valid outputs (for example, this occurs when the input is unconstrained by the specification). To address this, we synthesize the FTAs from the smallest input to the largest. Then, recursive transitions are not transitions to all valid output values, but rather to reachable output values. This full process is formalized in Algorithm <ref>.

Retrieving an accepting program, and trace for that program, is relatively simple, as runs through an FTA correspond closely to program traces. The general algorithm is to first extract an accepting run, then process that run and extract a witness. Intuitively, we extract the witness by inspecting all recursive calls in the run, and updating the trace for each input according to that call. This process is described in Algorithm <ref>.
[1]

A FTA run $L$, a candidate tree node $n$, and a ground specification $\groundSpec$.
A list of traces $T$ corresponding to the run.

$T \gets \List{[]_i \SuchThat i \in \domain(\groundSpec)}$
$n' \in \children(n)$
$T \gets \List{ \tau_i \Append \tau_i' \SuchThat \tau_i \in T \wedge \tau_i' \in \ExtractAngelicTraces(r,n',\groundSpec)}$
$\Label{}(n) = \mlstinline{f}$
$[n'] \gets \children(n)$
$T \gets \List{ \tau_i \Append (r(n')_i,r(n)_i) \SuchThat \tau_i \in T \wedge r(n)_i \neq \wildcard \wedge r(n')_i \neq \wildcard}$

A FTA $\vs$ and a ground specification $\groundSpec$.
A list of traces $T$ corresponding to the run.

$(r,P) \gets \GetAcceptingRun(\vs)$
$n \gets P.\rootnode$

Retrieving Accepting Traces

§.§ GetWitness

!rec f($x$).$e$! ⇓!rec f($x$).$e$!

e_1 ⇓!rec f($x$).$e$!

e_2 ⇓v_2

e[!rec f($x$).$e$!/𝑓,v_2/x] ⇓v

e_1 e_2 ⇓v

!unit! ⇓!unit!

e_1 ⇓v_1

e_2 ⇓v_2

(e_1,e_2) ⇓(v_1,v_2)

e ⇓(v_1,v_2)

!fst $\;e \Downarrow v_1$!

e ⇓(v_1,v_2)

!snd $\;e \Downarrow v_2$!

e ⇓v

!inl! $e \Downarrow$ !inl! $v$

e ⇓v

!inr! $e \Downarrow$ !inr! $v$

e ⇓!inl! v

!unl! e ⇓v

e ⇓!inr! v

!unr! e ⇓v

e_3 ⇓!inl! v_3

e_1 ⇓v_1

!switch! $e_3$ !on inl! $x_1 \to e_1$ !inr! $x_2 \to e_2$

e_3 ⇓!inr! v_3

e_2 ⇓v_2

!switch! $e_3$ !on inl! $x_1 \to e_1$ !inr! $x_2 \to e_2$

Program Semantics. The symbols $e$ range over expressions and $v$ range over values. Both $f$ and $x$ denote arbitrary free variables.
If $P=\mlstinline{rec f(}x\mlstinline{)}.e$
and $P\ v \Downarrow v'$
then $\SemanticsOf{P}(v) = v'$.

§.§ Prohibiting Runs

In our core algorithm, we ensure termination by prohibiting traces that have
already been processed. In particular, each run encodes a trace for each of the inputs. By prohibiting the runs corresponding to those traces, programs with the same traces are no longer accepted.
This process is
done by creating a new automaton, which is the union of $\fta_1\ldots\fta_n$,
where $\fta_i$ is $\fta$, with the transition corresponding to the $i$th
recursive call in $T$ is removed. This process is formalized in Algorithm <ref>.
[1]
ProhibitTraces(,,,), P, r

An FTA $(\ftastates,\alphabet,\finalstates,\transitions)$, a candidate program $P$, and a run $L$ of $P$ over the FTA.
An FTA that does not permit any runs that correspond to the same trace set as $L$.

$\fta \gets \bot$
$n \in P.\nodes$
$\Label(n) = \mlstinline{f} \wedge \children(n) = [n']$
$\transitions_i \gets \transitions \setminus \set{\mlstinline{f}(r(n')) \to r(n)}$
$\fta_i \gets (\ftastates,\alphabet,\finalstates,\transitions_i)$
$\fta \gets \mathsf{union}(\fta,\fta_i)$

Prohibit Traces

§.§ Optimality
As described, Algorithm <ref> does not guarantee an optimal program. However, with some tweaks, we can recover optimality.

* If $(P,T) = \GetAcceptingTraces(\vs)$, then forall $P' \in \vs$, $cost(P) \leq cost(P')$

* The current algorithm performs a backtracking search algorithm, where we refine, and if that refinement fails, we try with new refinements. In this way, the current algorithm can be thought of as a depth-first-search. To recover optimality, we update the algorithm to be analogous to Dijkstra's algorithm, where we continually inspect the lowest-cost program.

§.§ Incrementality
After a valid program is found, the partial computation can still be used for future synthesis calls. If a conflict was identified, additionally constraining the program will not invalidate that conflict. Similarly, when a version space has been created, we can easily update that version space with additional constraints. To incrementalize Algorithm <ref>, we merely must store the partial computation. When resuming computation, we update the version spaces to satisfy the new constraints in addition to the old ones. We can then resume the partial computation with the updated specification.

§ IMPLEMENTATION

We have implemented our proposed technique in a tool called that is implement in OCaml.
In this section, we discuss some important implementation details and optimizations omitted from the technical development.

§.§ Finitization of FTA States

Recall that our angelic synthesis technique uses finite tree automata to find a program that satisfies the specification under the angelic semantics. Further, recall that states in the tree automaton correspond to concrete values, of which there may be infinitely many. Similar to prior work <cit.>,  our implementation bounds the number of automaton states  using a parameter $k$ that controls the number of applications of the inference rules from Figure <ref>. By default, this parameter is set to 4.

Another complication in our setting is due to the use of angelic recursion in the inference rules in Figure <ref>. In particular, recall that, under the angelic semantics, a recursive call can return any value that satisfies the specification; so, for example, if the specification is true, there are infinitely many concrete values that satisfy it. In our implementation, we get around this issue by constructing FTAs for all inputs in increasing size up to $N$ where $N$ is the size of the largest input [If there is no ground specification for some of these inputs, we mark all states as accepting]. Then, for any recursive call $f$ on input $c$, we assume that the return value of $f(c)$ can be anything that both satisfies the specification and that is marked as accepting in the FTA for input $c$. Since each FTA has finitely many states, this allows us to implement the Angelic Recursion rule from Figure <ref> without introducing infinitely many states.

Our approach relies on processing finite tree automata to find programs. We perform a standard approach to finitization: we parameterize our core algorithm by an additional integer $i$ that corresponds to maximal depth of any deduction made by the inference rules in Figure <ref>. In other words, given $i=2$, one could not deduce $\mlstinline{inl (inl unit)} \in \ftastates$ with just the Inl and Unit rules, as it requires a minimum inference depth of 3.

Our technique has an additional source of trickiness – how do we finitize our
possible recursive calls? If there is no constraint on the argument to the
recursive function, the recursive call could return anything! Whenever we reach
a possible recursive call f($v$), we simply lookup the FTA associated with input $v$. The possible results are the final values of that FTA.

§.§ Program Selection

In general, there may be many programs that satisfy the given specification, and most synthesis algorithms use heuristics to choose which program to return to the user. One of these heuristics is to prefer smaller programs, and, inspired by the effectiveness of this heuristic in prior work <cit.>, also returns the smallest program in terms of AST size. However, to provide such a minimality guarantee, our implementation slightly deviates from the core synthesis procedure shown in Algorithm <ref>. In particular,  our actual implementation  maintains a priority queue over specifications sorted according to the size of the minimal solution for the corresponding angelic synthesis problem and explores these programs in increasing order or size. Thus, our implementation guarantees that the program returned to the user is the smallest one among those that satisfy the specification. The interested reader can see the pseudo-code in Algorithm <ref> in Section <ref> of the appendixthe full version of the paper.

The algorithm that ensures that $\mathsf{GetAcceptingRun}$ returns optimal results is the same as is used in Blaze, it is an adopted version of the minimal weight B-path algorithm introduced in <cit.>. Being expressed as a minimal weight B-path is also the primary limiter for what metrics can be used – if we can express our metric as a minimal weight B-path, it is a valid metric.

For our overall algorithm to return the optimal program, we update our program to use Dijkstra's Algorithm for search, where it is currently using a Depth-First Search. In particular, given a specification $\groundSpec$ and a witness $\witness$, we first try to see if there are any programs that satisfy $\groundSpec \wedge \witness$. Only after this fails do we try to find a program that satisfies $\groundSpec \wedge \neg\witness$. To return an optimal program, we must search through these updated specifications concurrently. Each specification is given a priority according to the cost of the minimal program that angelically satisfies it. These specifications are put in a priority queue, and processed according to their priority. When a minimal priority specification is found where the associated program satisfies the specification with standard semantics, that program is returned.

§.§ Improving the CEGIS Loop

Recall that our technique can perform synthesis from logical specifications by integrating our proposed approach within a CEGIS loop. While the standard CEGIS paradigm only uses ground formulas for inductive synthesis, our approach can actually utilize the original logical specification when performing angelic synthesis. In particular, when deciding which values can be returned by a recursive call, our implementation utilizes the original logical specification as opposed to the weaker ground specifications. For example, suppose that the original specification is $f(x) < x$ and our current counterexamples include $3$ and $4$ (i.e., ground specification is $f(3) < 3 \land f(4) < 4$). While the ground specification does not constrain the output of recursive call $f(2)$, we can use the original specification to constrain the return value of $f(2)$ to be either $0$ or $1$ (assuming that $x$ is a natural number).

§.§ Termination of Synthesized Programs

To ensure that our synthesized programs terminate, our implementation utilizes  a well-founded default ordering  on our values. In particular, ensures that it generates terminating programs by only permitting recursive calls on values that are strictly smaller than the input. If $v_\emph{in}$ is provided as an input, recursive calls to f can only be applied to values $v$ when $v \prec v_\emph{in}$. This prevents generating infinite loops like let rec f(x) = f(x+1).

§.§ Optimizations

Our implementation also utilizes a few standard optimizations described in prior synthesis literature. Since it is common to perform type-directed pruning in synthesis <cit.>,  we construct  our FTAs to only accept well-typed programs. Inspired by prior work that utilizes eta-long beta-normal form <cit.>, we also modify our FTA construction rules to only accept such normalized programs.

§.§ Optimizations

We identified 4 key optimizations in our implementation that are not captured in
our core algorithm. (1) bounds the size of the value space, (2)
distinguishes between introduction and elimination forms, (3)
performs incremental memoization, and (4) utilizes logical

*Value Space Bounding A common problem in version-space synthesis is
the state-space explosion problem. As more operations are applied and as
the FTAs are intersected, the number of FTA states exponentially increases. To
tame this explosion, we bound the size of the explored values to be 3 nodes
larger than the original value. We dynamically increase this bound whenever the
number of nodes not added at a given depth due to the bound is larger
than the number of nodes that are added at a given depth.

Let $[0]$ be a state in $\ftastates$ in our extended example of
right_spine and imagine append is in our context.
With no applications of append, the only reachable list has length
1. With 1 application of append, a lists of length one and two
reachable (append [0] [0] = [0;0]). With 2 applications of
append lists of length 1-4 are reachable. With 3 applications,
lists of length 1-8 is reachable. If the input tree is N(L,2,L)
(size 3),
then the lists of size over 6 get pruned from the state space.

*Distinguishing Between Introduction and Elimination Forms
Distinguishing between introduction and elimination forms is a technique in the
automated theorem proving literature that reduces the number of ways to prove a
given theorem, reducing the search space. This type of approach can be applied
to synthesis to reduce the number of semantically equivalent, but syntactically
distinct, programs. It also reduces the number of states in our state space.

Consider the input-output example $T_2 \mapsto
\mlstinline[2]$. Using introduction and elimination forms prohibits expressions like

switch (inl 7) on | inl -> [2] | inr -> [5;6;7]

This program is accepting, but the value (inl $7$)
is not used for anything besides the useless switch, it is the exact same
program as just one that returns singleton [2].

If this expression were allowed in the search space, the states corresponding
to the values inl 7 and 7 would be part of an
accepting run. Values that are not a part of accepting runs can safely be
pruned, which makes future intersections much easier.

By not permitting these types of programs, values like inl 7 and
7 are not errantly included in the search space.

*Incremental Memoization As previously mentioned, our algorithm
memoizes FTA creations and intersections. We've mentioned this like
everywhere in the paper, is it necessary to add here too?

*Logical Specification Utilization Recall that, when given a logical
specification, we can perform a CEGIS loop to get increasingly strong ground
specifications. For example, consider the logical specification for
right_spine given earlier:

\[
\phi(in,out) := \mlstinline{no_left_subchildren}(in) \Rightarrow (\mlstinline{tree_size}(in) == \mlstinline{list_size}(out))
\]

After instantiating it to input $T_1$, we get the ground

\[
\groundSpec := \mlstinline{no_left_subchildren}(T_1) \Rightarrow
(\mlstinline{tree_size}(T_1) == \mlstinline{list_size}(f (T_1)))
\]

According to our formalization, the program

$P_1$ := let rec right_spine(x) =
match x with
| L -> []
| N(l,v,r) -> right_spine(r)

angelically satisfies the specification (with witness $\witness = f (T_1^R) =
[1;0]$). We know this witness is incompatible with the original logical spec.
Any program found that uses this witness would be destined to require another
CEGIS iteration. To remove these unnecessary iterations, when used as part of a
CEGIS loop, we only permit recursive calls that return values compatible with
the original spec.

§ EVALUATION

In this section, we describe a series of experimental evaluations that are designed to answer the following research questions:

RQ1. Is able to effectively synthesize programs from a variety of different specifications?

RQ2. How does compare against prior work in terms of synthesis efficiency and correctness of synthesized programs?

RQ3. How important is it to combine angelic synthesis with specification strengthening?

All experiments described in this section are performed on a 2.5 GHz Intel Core i7 processor with 16 GB of 1600 MHz DDR3 running macOS Big Sur with a time limit of 120 seconds.

§.§ Benchmarks and Baselines

To answer the  research questions listed above, we use to synthesize 45 recursive functional programs from prior work <cit.> and compare it against the following baselines:

* SMyth <cit.>, which is a top-down type-directed programming-by-example tool. In particular, generalizes  <cit.> to handle input-output examples that are not trace-complete.

* Synquid <cit.>, which performs synthesis from liquid types.

* Leon <cit.>, which is a synthesizer that performs synthesis from logical specifications.

§.§ Specifications

To evaluate whether can handle a variety of different specifications and to compare it against different tools, we consider three classes of specifications for each of our 45 benchmarks:

* IO: These are input-output examples written by developers of   <cit.>.

* Ref: These are reference implementations written by us.

* Logical: These are logical specifications that specify pre- and post-conditions (or, in the case of , refinement types) on the function to be synthesized.

While can perform synthesis from all three classes of specifications listed above, not all baselines can effectively handle these different specifcations. Thus, we only compare against on the IO and Ref specifications and against and for the Logical specifications. Note that  can be adapted to perform synthesis from a reference implementation by integrating it inside a CEGIS loop and obtaining input-output examples from the reference implementation. Furthermore, while and can, in principle, handle IO specifications, prior work has shown that they are not effective when used for this purpose <cit.>. Thus, we only compare against and on the Logical specifications.

created a benchmark suite consisting of IO tasks, Reimpl tasks, and Logical tasks. These synthesis tasks are those in the and benchmark suites, with different specifications depending on whether the task is an IO task, a Reimpl task, or a Logical task.

An IO task uses exactly those from . On benchmarks where did not provide a benchmark (namely, those it failed on), we pulled the IO examples from .

The Reimpl benchmark suite consists of a set of benchmarks where the postcondition is of the form:

\[
\varphi(in,out) = out == \mlstinline{desired_f}(in)
\]

In other words, for each function desired_f in the benchmark suite, we attempt to synthesize an equivalent function. We use these specifications in a CEGIS loop to simulate user behavior. When a user engages with an IO synthesizer, they have a desired function in their head (here, desired_f). Whenever the synthesizer does not generate the correct function, the user provides a new IO example. This is exactly the same thing our CEGIS algorithm does on this type of specification. To simulate this user behavior, we did not enable the Logical Specification Utilization optimization, when running on these benchmarks.

For the Logical benchmark suite, for each of the benchmarks in the benchmark suite, we came up with a logical specification for that benchmark. We then wrote this logical specification as both a predicate (for and ) and as a measure (for ). For , we also provided refinement types for functions in the context, to help with 's internal verification.

A few of the logical specifications we had to refine after realizing the desired function would not satisfy the written specification. We did not edit any logical specifications besides those that did not accept the desired program. A full description of our logical specifications is available in Section <ref>. the full verison of our paper.

§.§ Synthesis from Input/Output Specifications

Test     2c     2c

Time (s)     Correct?     Time (s)     Correct?
[head to column names]examples.csv

The results of running and on the IO benchmark suite. A cross mark under the Time column indicates failure (i.e., either timeout or terminating without finding a solution). Under the “Correct?” column  “” indicates that the synthesized program is the desired one, and “" indicates that the synthesized program matches the IO examples but not the user intent.

Figure <ref> presents the results of our comparison against on synthesis tasks from IO specifications. Here, the column labeled “Time” shows the synthesis time in seconds, and a cross mark () indicates failure (e.g., time-out). The column labeled “Correct?” shows whether the synthesized program is the one intended by the user. In particular, when synthesis is successful, the returned program always satisfies the provided IO examples, however, it may or may not be the program by the user. Thus, this additional column allows us to evaluate how generalizable the synthesis results of these tools are.

As we can see from Figure <ref>, is able to synthesize a program consistent with the IO examples in all but 2 cases, whereas fails on 4 benchmarks.
For the benchmarks that can be solved by both tools, the  running time of both tools is quite fast (a few seconds or less) with the exception of a few outliers.

Finally, the programs synthesized by and are roughly equal in terms of generalization power: for , there are 5 cases where the synthesized program is not the intended one, and for , there are 4 such cases.

*Failure Analysis Next, we analyze the two benchmarks that fails on and provide some intuition about why it is unable to solve them. For the benchmarks called list-take and list-sorted-insert, times out because the specification does not in any way constrain the outputs of the many possible recursive calls. This both makes FTA creation quite slow and also causes the algorithm to explore many different strengthenings of the specification.

We find that has issues when the function is highly underspecified. Our algorithm has two primary components (1) FTA construction, and (2) the backtracking search. When general postconditions are given, both components are hurt. FTA construction is made slower because the fanout on recursive calls is made larger – intersecting two highly nondeterministic FTAs is very slow. With more choices to make, the backtracking search is also made slower, as there are more possible routes to take. This is why performs badly on list-sorted-insert and list-drop. The specifications for both of these are highly unconstrained, and permit a number of possible recursive calls, resulting in an explosion in a state space explosion.

Result #1: When synthesizing programs from IO specifications, is competitive with , a state-of-the-art  tool for synthesizing recursive programs from input-output examples. In particular, can solve two more benchmarks despite not specializing in IO specifications.

§.§ Synthesis from Reference Implementation

Test     2c     2c

Time (s)     # Iters     Time (s)     # Iters
[head to column names]equiv.csv

The results of running and on the Ref benchmark suite. A cross mark under the Time column indicates failure (i.e., either timeout or terminating without finding a solution). The column labeled “# Iters" shows the number of iterations within the CEGIS loop.

In this section, we use to synthesize programs from reference implementations and compare against . We incorporate both tools into a CEGIS loop and, for each candidate program, check whether it is equivalent to our reference implementation. If not, we ask the verifier for a concrete counterexample $I$ and obtain its corresponding output $O$ by running the reference implementation on $I$. We then add $(I, O)$ as a new input-output example and continue this process until the synthesizer program is indeed equivalent to the reference implementation.[We actually use bounded testing instead of verification; however, we manually confirmed that the generated programs are indeed equivalent to the reference implementation.]

The results of this evaluation are shown in Figure <ref>. In particular, the column labeled “Time" indicates synthesis time in seconds, with  indicating failure as before. The second column labeled “# iters" shows the number of iterations of the CEGIS loop for those benchmarks that can be synthesized. As we can see from this figure, successfully solves all but two of the benchmarks with an average synthesis time of 4.49 seconds and 4.37 CEGIS iterations on average. In contrast, fails to solve 12 of these benchmarks, and it takes an average of 3.07 seconds and 4.52 CEGIS iterations. Overall, we believe these results indicate that  is able to deal better with the random examples generated by the verifier compared to .[Recall that the IO examples used in the previous experiment are written by the developers.]

*Failure Analysis The reason that fails on  tree-nodes-at-level  is similar to that for pure IO examples: the verifier returns IO pairs for which the results of the many possible recursive calls are highly under-constrained, resulting in slow FTA construction as well as many strengthening steps.
fails on list-rev-tailcall due to our requirement for ensuring termination of synthesized programs (see Section <ref>). Concretely, list-rev-tailcall needs to make a recursive call on ([2],[1]) for input ([1;2],[]), but our default ordering does not consider ([2],[1]) to be strictly less than ([1;2],[]).

Result #2: is able to synthesize 96% of the programs from a reference implementation. In contrast, is only able to synthesize 73%.

§.§ Synthesis from Logical Specifications

Figure <ref> shows the results of our evaluation on logical specifications for each  of , , and . As before, the column labeled “Time” shows the synthesis time for each tool, and the column labeled “Correct?” shows whether the tools were able to generate the intended program from the given specification. As we can see in this table, solves more benchmarks than and significantly more compared to .
In what follows, we explain the failure cases of each tool and contrast them with each other.

Test     2c     2c     2c

Time (s)     Correct?     Time (s)     Correct?     Time (s)     Correct?
[head to column names]postconditional.csv

The results of running , , and on the Logical benchmark suite. The result “” under “Time” indicates failure (in this case, timeout). Under the “Correct?” column,“” (resp. “”) indicates that the synthesized program was (resp. not) the intended one.

*Failure Analysis for . The two unique failure cases for are nat-add and nat-max. For the first one, given the unary encoding of two natural numbers, the goal is to add them, and for the second one, the goal is to return the maximum. While these benchmarks look very easy at first glance, fails on them because the specification is very under-constrained. For example, the specification of nat-max only states that the output should be greater than or equal to both inputs, but under the angelic semantics of recursion, this results in many possible outputs of the recursive calls and causes a blow-up. This is a common theme for across all types of specifications: Since it constructs a version space based on angelic semantics, synthesis becomes more difficult when the specification is “loose" for arguments used in recursive calls.

These postconditions are particularly nefarious as they encourage a state space explosion. On input $(0,0)$, any natural number can be returned (due to finitization, perhaps just 4). On input $(0,1)$, any natural number greater than 1 can be returned. On a recursive call to $(0,0)$, the result can be any number up to 4 – then additional transitions can increase the size of that number to 8. This effect compounds, where larger examples can return more and more possible results. This increases the nondeterminism in two ways: it adds extra final states and it adds more nondeterministic transitions on each recursive call. This makes the FTA intersection quite slow – the majority of the time is spent in a single intersection that does not terminate by the timeout.

The tree-binsert benchmark is interesting because it is a relatively constrained postcondition, but the synthesis task is hard enough that it does not terminate within 120 seconds. The postcondition states that if the input tree is a BST, then the output is too, and the elements of the output are exactly the elements of the input tree and the inserted value:

\[
\varphi((in_t,in_x),out) := \mlstinline{is_bst}(in_t) \Rightarrow (\mlstinline{is_bst}(out) \wedge \mlstinline{elements}(in_t) \cup \set{in_x} == \mlstinline{elements}(out))
\]

However, despite this having a relatively constrained postcondition, it still fails. Despite neither having much backtracking in the search, nor having much nondeterminism in the FTA, the required size of this benchmark, and relative complexity of the synthesized function, makes FTA intersection still take too long.

Behavior of . At first glance, seems to perform surprisingly poorly on these benchmarks.  Upon further investigation, we found that is only able to successfully synthesize programs from highly stylized specifications. For example, consider our specification for the list-compress benchmark shown in Figure <ref>. While is unable to synthesize a program from this specification within the given time limit, it can synthesize the desired program from the specification shown in Figure <ref>. These specifications are semantically equivalent; however, 's behavior on them is very different. Thus, while it may be possible to re-engineer our specifications so that performs successful synthesis, coming up with specifications that are -friendly is a highly non-trivial task.

data List where
Nil :: List
Cons :: Nat -> List -> List

measure heads :: List -> Set Nat where
Nil -> []
Cons x xs -> [x]

measure no_adjacent_dupes :: List -> Bool where
Nil -> True
Cons x xs -> !(x in heads xs)        no_adjacent_dupes xs

compress :: xs: List a -> List | elems xs == elems _v        no_adjacent_dupes _v
compress = ??
Our list-compress benchmark specification for .

data PList a <p :: a -> PList a -> Bool> where
Nil :: PList a <p>
Cons :: x: a -> xs: PList a <p> | p x _v -> PList a <p>

measure heads :: PList a -> Set a where
Nil -> []
Cons x xs -> [x]

type List a = PList a <True>
type CList a = PList a <!(_0 in heads _1)>

compress :: xs:List a -> CList a | elems xs == elems _v
compress = ??
Alternative list-compress benchmark specification for .

*Comparisons to Leon performs better than for our specifications; however, it solves 34 benchmarks compared to the 41 of . Overall, tends to perform relatively poorly on benchmarks with nontrivial branching (e.g., list-compress and tree-binsert). This behavior is likely due to their condition abduction procedure  failing to infer the correct branch conditions when they are deeply nested. On the higher-order benchmarks (list-filter, list-map), either reports an error or returns a wrong solution that does not satisfy the provided logical specification.

Result #3: is able to synthesize  93% of the benchmarks from logical specifications and solves more benchmarks than both (76%) and (49%).

§.§ Ablation Study for Specification Strengthening

Our proposed synthesis algorithm combines angelic synthesis with specification strengthening. However, an alternative approach is to perform enumerative search over all programs that angelically satisfy the specification. That is, one could repeatedly sample solutions to the angelic synthesis problem and test whether they satisfy the specification until we exhaust the search space or find the correct program. In this section, we perform an ablation study to evaluate the benefit of specification  strengthening compared to a simpler enumerative search baseline.

The results of this ablation study are presented in Figure <ref>, where Burst$^\dagger$  is a variant of that performs basic enumerative search instead of backtracking search with specification strengthening. As we can see from this table, with specification strengthening solves more benchmarks within the given time limit, and this difference is particularly pronounced for the IO and Ref specifications. For Logical specifications, the difference between and Burst$^\dagger$ is less stark due to the optimization described in Section <ref>.

IO     Ref     Logical

Number of benchmarks that can be solved within the time limit for each of the three specifications.

Result #4: The variant of that performs enumerative search over angelic synthesis results solves fewer benchmarks than (with specification strengthening) for all three specification types.

§ RELATED WORK

The prior work most related to this paper can be divided into four overlapping categories: (i)
bottom-up synthesis,

(ii) version-space-based synthesis, (iii) synthesis of functional recursive programs, and (iv) synthesis based on angelic semantics.

Now we elaborate on these categories of work.
For a broader survey of program synthesis, see <cit.>.

*Bottom-up Synthesis Bottom-up enumeration is a classic approach to program synthesis. A canonical example is Transit <cit.>. Transit grows a pool of programs of increasing complexity, ensuring that no program in the pool is observationally equivalent to another program in the pool.
The Stun <cit.> approach generalizes this method by decomposing the input-output specification into multiple parts, synthesizing programs that work for these sub-specifications in a bottom-up way, then combining these programs using a form of anti-unification. Bustle <cit.> offers another generalization, using a learning algorithm to guide bottom-up exploration. However, none of these methods handle programs with general recursion.

Escher <cit.> is a bottom-up inductive synthesis approach that handles recursion. The algorithm here combines a forward search, in which terms are generated bottom-up, with a procedure for inferring conditional statements. However, a key limitation of this approach is that it requires a trace-complete specification to handle recursive calls.

*Version-Space-Based Synthesis Version space approaches to synthesis use an efficient data structure to represent the set of all programs that satisfy a specification.
Early techniques <cit.> proved hard to scale.
FlashFill <cit.>, which represented version spaces using a form of e-graphs <cit.>, was a major leap forward.

FlashFill's success led to followup methods, for example, FlashExtract <cit.>, FlashRelate <cit.>, and Refazer <cit.>.
This line of work culminated in FlashMeta <cit.>, a framework for version-space-based synthesis that supports the above methods as instantiations.
Unlike , these methods all construct versions spaces top-down. They work backward from the desired output for a specific input, iteratively producing subgoals describing the unknown parts of the target program, and then construct version spaces for these subgoals.

The use of tree automata (FTAs) as a version space representation was first explored by <cit.> in the setting of reactive synthesis. Subsequently, the Dace <cit.>, Relish <cit.>, and Blaze <cit.> systems used tree automata to represent version spaces in the synthesis of functional programs.
Like , these three approaches proceed bottom-up:

rather than starting from the desired outputs and producing subgoals for incomplete programs, they start from the input values and propagate these inputs through a space of programs.
However, for reasons explained earlier, these methods cannot handle general recursion.

*Synthesis of Recursive Programs The synthesis of (functional) recursive programs has a long history.
Most methods in this area consider synthesis from examples, but synthesis from richer specifications, such as refinement types, has also been considered.
The Thesys <cit.> and  Igor2 <cit.> systems are two early examples of work of this sort.
Given a a set of examples, these methods first synthesize straight-line programs in a top-down manner, then identify patterns within a given program, then generalize these patterns into a recursive program.

More recently, the Myth <cit.> and $\lambda^2$ <cit.> systems introduced types as a means of directing an inductive synthesis process.
Myth2 <cit.> extended with more complex types of refinement types, including negative examples, intersection, and union types.

All these approaches are top-down; also, all of them, except for $\lambda^2$, rely on trace-completeness to handle recursive calls. While $\lambda^2$ does not assume trace-completeness, it only applies deductive reasoning to limited forms of recursion assuming trace-completeness, and defaults to brute-force enumeration when handling general recursion or on non-trace-complete examples.

<cit.> is a generalization of that also performs top-down deduction-aided search, but does not have the trace-completeness requirement.

To handle non-trace-complete specifications, generates partial programs, then propagates constraints from partial programs to the remaining holes. This propagation is both complex and domain-specific, and incomplete. By contrast, relies on a single generalizable principle of angelic recursion, and is complete.

Leon <cit.> performs synthesis modulo recursive functions. Leon takes a pre-/post-condition specification and searches for a recursive function that can satisfy it. Leon solves this task using a term generation engine that produces candidate programs, a condition abduction engine that synthesizes branches, and a verification engine that evaluates candidate solutions.
's term generation runs similarly (though not exactly, due to the lack of angelic execution) to our $^\dagger$ ablation; it does not search through programs based on recursive results but simply based on increasing cost. Its condition abduction engine is top-down and quite distinct from ours.

Synquid <cit.> synthesizes programs from polymorphic refinement types. Such types are expressive and allow the specification of desired functions in a way that is both compositional and tight.
However, while can synthesize nearly any function from a carefully crafted refinement type, there are many kinds of
realizable specifications on which it simply gives up.

In particular, cannot synthesize from specifications that are non-inductive, including many of the specifications in our benchmark suite.

More generally, and address different problems: focuses on always being able to synthesize from a well-written refinement type, while focuses on best-effort synthesis from arbitrary

logical specifications.

The recent Cypress <cit.> system targets synthesis of recursive programs from separation logic specifications.
Cypress generates a satisfying straight-line program, then “folds” that program into a generalized recursive procedure.
We attempted a similar strategy in our setting but found the space of possible foldings to be prohibitively large.

In contrast, our synthesis algorithm follows a lazier strategy: instead of synthesizing the full search space, then finding ways to fold it together, we overapproximate the search space and then discover ways to refine it.

*Angelic Synthesis
While angelic non-determinism has been used to expose synthesizers to programmers, there is almost no work on the use of angelic semantics as a core part of a synthesis algorithm. The one approach that we know of is FrAngel <cit.>, which adds control structures to the well-studied problem of component-based synthesis. FrAngel first identifies candidate partial programs by synthesizing programs with no control structures, but instead with angelic placeholders, then attempts to place appropriate control structures in place of the angelic placeholders.

In contrast, does not have angelic placeholders but instead  updates the generated code itself to fulfill the requirements put in place by  angelic recursion.

§ CONCLUSION

In this paper, we presented a new technique for synthesizing recursive functional programs. Our approach differs from prior work in this space as it performs synthesis in a bottom-up fashion. Our algorithm first performs angelic synthesis wherein recursive calls may return any value consistent with the specification. This result may be spurious, so our method analyzes the assumptions made in angelic executions and gradually strengthens the specification to find the correct program.

We have implemented the proposed algorithm in a tool called and showed that it can synthesize programs from a variety of specifications, including examples, reference implementations, and logical formulas. Our comparison against three synthesizers (, , and ) shows that advances the state-of-the-art in synthesizing recursive functional programs.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Albarghouthi, Gulwani, and
KincaidAlbarghouthi et al2013]
authorpersonAws Albarghouthi, personSumit
Gulwani, and personZachary Kincaid.
Recursive Program Synthesis. In
booktitleComputer Aided Verification,
editorpersonNatasha Sharygina and
personHelmut Veith (Eds.). publisherSpringer Berlin
Heidelberg, addressBerlin, Heidelberg,

[Alur, Černỳ, and RadhakrishnaAlur
et al2015a]
authorpersonRajeev Alur, personPavol
Černỳ, and personArjun Radhakrishna.
Synthesis through unification. In
booktitleInternational Conference on Computer Aided
Verification. Springer, publisherSpringer International
Publishing, pages163–179.

[Alur, Černỳ, and RadhakrishnaAlur
et al2015b]
authorpersonRajeev Alur, personPavol
Černỳ, and personArjun Radhakrishna.
Synthesis through unification. In
booktitleInternational Conference on Computer Aided
Verification. Springer, pages163–179.

[Barowy, Gulwani, Hart, and ZornBarowy
et al2015]
authorpersonDaniel W Barowy, personSumit
Gulwani, personTed Hart, and personBenjamin Zorn.
FlashRelate: extracting relational data from
semi-structured spreadsheets using examples.
journalACM SIGPLAN Notices volume50,
number6 (year2015), pages218–228.

[Broy and WirsingBroy and Wirsing1981]
authorpersonM. Broy and personM.
Wirsing. year1981.
On the algebraic specification of nondeterministic
programming languages. In booktitleCAAP '81,
editorpersonEgidio Astesiano and
personCorrado Böhm (Eds.). publisherSpringer
Berlin Heidelberg, addressBerlin, Heidelberg,

[Comon, Dauchet, Gilleron, Löding,
Jacquemard, Lugiez, Tison, and TommasiComon et al2007]
authorpersonH. Comon, personM. Dauchet,
personR. Gilleron, personC. Löding,
personF. Jacquemard, personD. Lugiez,
personS. Tison, and personM. Tommasi.
titleTree Automata Techniques and Applications.
howpublishedAvailable on:
release October, 12th 2007.

[Downey, Sethi, and TarjanDowney
et al1980]
authorpersonPeter J. Downey, personRavi
Sethi, and personRobert Endre Tarjan.
Variations on the Common Subexpression Problem.
journalJ. ACM volume27,
number4 (dateOct. year1980),

[Feser, Chaudhuri, and DilligFeser
et al2015]
authorpersonJohn K. Feser, personSwarat
Chaudhuri, and personIsil Dillig.
Synthesizing Data Structure Transformations from
Input-Output Examples.
journalSIGPLAN Not. volume50,
number6 (dateJune year2015),

[Frankle, Osera, Walker, and ZdancewicFrankle
et al2016]
authorpersonJonathan Frankle,
personPeter-Michael Osera, personDavid Walker, and
personSteve Zdancewic. year2016.
Example-Directed Synthesis: A Type-Theoretic
journalSIGPLAN Not. volume51,
number1 (dateJan. year2016),

authorpersonSumit Gulwani.
Automating string processing in spreadsheets using
input-output examples. In booktitleProceedings of the 38th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL 2011, Austin, TX, USA, January 26-28, 2011,
editorpersonThomas Ball and personMooly
Sagiv (Eds.). publisherACM, pages317–330.

[Gulwani, Polozov, and SinghGulwani
et al2017]
authorpersonSumit Gulwani, personOleksandr
Polozov, and personRishabh Singh.
Program Synthesis.
journalFoundations and TrendsÂ® in Programming
Languages volume4, number1-2
(year2017), pages1–119.

[Itzhaky, Peleg, Polikarpova, Rowe, and
SergeyItzhaky et al2021]
authorpersonShachar Itzhaky, personHila
Peleg, personNadia Polikarpova, personReuben NS
Rowe, and personIlya Sergey. year2021.
Cyclic program synthesis. In
booktitleProceedings of the 42nd ACM SIGPLAN International
Conference on Programming Language Design and Implementation.

[Kitzelmann, Schmid, Olsson, and
KaelblingKitzelmann et al2006]
authorpersonEmanuel Kitzelmann, personUte
Schmid, personRoland Olsson, and personLeslie Pack
Kaelbling. year2006.
Inductive synthesis of functional programs: An
explanation based generalization approach.
journalJournal of Machine Learning Research
volume7, number2 (year2006).

[Kneuss, Kuraj, Kuncak, and SuterKneuss
et al2013]
authorpersonEtienne Kneuss, personIvan
Kuraj, personViktor Kuncak, and personPhilippe
Suter. year2013.
Synthesis modulo Recursive Functions. In
booktitleProceedings of the 2013 ACM SIGPLAN International
Conference on Object Oriented Programming Systems Languages & Applications
(Indianapolis, Indiana, USA) (seriesOOPSLA '13).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages407–426.

[Lau, Domingos, and WeldLau
et al2003]
authorpersonTessa Lau, personPedro
Domingos, and personDaniel S Weld.
Learning programs from traces using version space
algebra. In booktitleProceedings of the 2nd international
conference on Knowledge capture. pages36–43.

[Le and GulwaniLe and Gulwani2014]
authorpersonVu Le and personSumit
Gulwani. year2014.
Flashextract: A framework for data extraction by
examples. In booktitleProceedings of the 35th ACM SIGPLAN
Conference on Programming Language Design and Implementation.

[Lubin, Collins, Omar, and ChughLubin
et al2020]
authorpersonJustin Lubin, personNick
Collins, personCyrus Omar, and personRavi Chugh.
Program Sketching with Live Bidirectional
journalProc. ACM Program. Lang.
volume4, numberICFP, Article articleno109
(dateAug. year2020), numpages29 pages.

authorpersonParthasarathy Madhusudan.
Synthesizing reactive programs. In
booktitleComputer Science Logic (CSL'11)-25th International
Workshop/20th Annual Conference of the EACSL. Schloss
Dagstuhl-Leibniz-Zentrum fuer Informatik.

[Odena, Shi, Bieber, Singh, and SuttonOdena
et al2020]
authorpersonAugustus Odena, personKensen
Shi, personDavid Bieber, personRishabh Singh, and
personCharles Sutton. year2020.
BUSTLE: Bottom-up program-Synthesis Through
Learning-guided Exploration.
journalarXiv preprint arXiv:2007.14381

[Osera and ZdancewicOsera and
authorpersonPeter-Michael Osera and
personSteve Zdancewic. year2015.
Type-and-example-directed program synthesis. In
booktitleProceedings of the 36th ACM SIGPLAN Conference
on Programming Language Design and Implementation, Portland, OR, USA, June
15-17, 2015, editorpersonDavid Grove and
personStephen M. Blackburn (Eds.). publisherACM,

[Polikarpova, Kuraj, and
Solar-LezamaPolikarpova et al2016]
authorpersonNadia Polikarpova, personIvan
Kuraj, and personArmando Solar-Lezama.
Program synthesis from polymorphic refinement
types. In booktitleProceedings of the 37th ACM SIGPLAN
Conference on Programming Language Design and Implementation, PLDI 2016,
Santa Barbara, CA, USA, June 13-17, 2016,
editorpersonChandra Krintz and
personEmery Berger (Eds.). publisherACM,

[Polozov and GulwaniPolozov and
authorpersonOleksandr Polozov and
personSumit Gulwani. year2015.
Flashmeta: A framework for inductive program
synthesis. In booktitleProceedings of the 2015 ACM SIGPLAN
International Conference on Object-Oriented Programming, Systems, Languages,
and Applications. pages107–126.

[Rolim, Soares, D'Antoni, Polozov, Gulwani,
Gheyi, Suzuki, and HartmannRolim et al2017]
authorpersonReudismam Rolim, personGustavo
Soares, personLoris D'Antoni, personOleksandr
Polozov, personSumit Gulwani, personRohit Gheyi,
personRyo Suzuki, and personBjörn Hartmann.
Learning syntactic program transformations from
examples. In booktitle2017 IEEE/ACM 39th International
Conference on Software Engineering (ICSE). IEEE, pages404–415.

[Shi, Steinhardt, and LiangShi
et al2019]
authorpersonKensen Shi, personJacob
Steinhardt, and personPercy Liang.
Frangel: component-based synthesis with control
journalProceedings of the ACM on Programming
Languages volume3, numberPOPL
(year2019), pages1–29.

authorpersonPhillip D Summers.
A methodology for LISP program construction from
journalJournal of the ACM (JACM)
volume24, number1 (year1977),

[Udupa, Raghavan, Deshmukh, Mador-Haim, Martin,
and AlurUdupa et al2013]
authorpersonAbhishek Udupa, personArun
Raghavan, personJyotirmoy V Deshmukh, personSela
Mador-Haim, personMilo MK Martin, and personRajeev
Alur. year2013.
TRANSIT: specifying protocols with concolic
journalACM SIGPLAN Notices volume48,
number6 (year2013), pages287–296.

[Wang, Dillig, and SinghWang
et al2017a]
authorpersonXinyu Wang, personIsil Dillig,
and personRishabh Singh. year2017a.
Program Synthesis Using Abstraction Refinement.
journalProc. ACM Program. Lang.
volume2, numberPOPL, Article articleno63
(dateDec. year2017), numpages30 pages.

[Wang, Dillig, and SinghWang
et al2017b]
authorpersonXinyu Wang, personIsil Dillig,
and personRishabh Singh. year2017b.
Synthesis of Data Completion Scripts Using Finite
Tree Automata.
journalProc. ACM Program. Lang.
volume1, numberOOPSLA, Article
articleno62 (dateOct. year2017),
numpages26 pages.

[Wang, Wang, and DilligWang
et al2018]
authorpersonYuepeng Wang, personXinyu Wang,
and personIsil Dillig. year2018.
Relational Program Synthesis.
journalProc. ACM Program. Lang.
volume2, numberOOPSLA, Article
articleno155 (dateOct. year2018),
numpages27 pages.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Albarghouthi, Gulwani, and
KincaidAlbarghouthi et al2013]
authorpersonAws Albarghouthi, personSumit
Gulwani, and personZachary Kincaid.
Recursive Program Synthesis. In
booktitleComputer Aided Verification,
editorpersonNatasha Sharygina and
personHelmut Veith (Eds.). publisherSpringer Berlin
Heidelberg, addressBerlin, Heidelberg,

[Alur, Černỳ, and RadhakrishnaAlur
et al2015a]
authorpersonRajeev Alur, personPavol
Černỳ, and personArjun Radhakrishna.
Synthesis through unification. In
booktitleInternational Conference on Computer Aided
Verification. Springer, publisherSpringer International
Publishing, pages163–179.

[Alur, Černỳ, and RadhakrishnaAlur
et al2015b]
authorpersonRajeev Alur, personPavol
Černỳ, and personArjun Radhakrishna.
Synthesis through unification. In
booktitleInternational Conference on Computer Aided
Verification. Springer, pages163–179.

[Barowy, Gulwani, Hart, and ZornBarowy
et al2015]
authorpersonDaniel W Barowy, personSumit
Gulwani, personTed Hart, and personBenjamin Zorn.
FlashRelate: extracting relational data from
semi-structured spreadsheets using examples.
journalACM SIGPLAN Notices volume50,
number6 (year2015), pages218–228.

[Broy and WirsingBroy and Wirsing1981]
authorpersonM. Broy and personM.
Wirsing. year1981.
On the algebraic specification of nondeterministic
programming languages. In booktitleCAAP '81,
editorpersonEgidio Astesiano and
personCorrado Böhm (Eds.). publisherSpringer
Berlin Heidelberg, addressBerlin, Heidelberg,

[Comon, Dauchet, Gilleron, Löding,
Jacquemard, Lugiez, Tison, and TommasiComon et al2007]
authorpersonH. Comon, personM. Dauchet,
personR. Gilleron, personC. Löding,
personF. Jacquemard, personD. Lugiez,
personS. Tison, and personM. Tommasi.
titleTree Automata Techniques and Applications.
howpublishedAvailable on:
release October, 12th 2007.

[Downey, Sethi, and TarjanDowney
et al1980]
authorpersonPeter J. Downey, personRavi
Sethi, and personRobert Endre Tarjan.
Variations on the Common Subexpression Problem.
journalJ. ACM volume27,
number4 (dateOct. year1980),

[Feser, Chaudhuri, and DilligFeser
et al2015]
authorpersonJohn K. Feser, personSwarat
Chaudhuri, and personIsil Dillig.
Synthesizing Data Structure Transformations from
Input-Output Examples.
journalSIGPLAN Not. volume50,
number6 (dateJune year2015),

[Frankle, Osera, Walker, and ZdancewicFrankle
et al2016]
authorpersonJonathan Frankle,
personPeter-Michael Osera, personDavid Walker, and
personSteve Zdancewic. year2016.
Example-Directed Synthesis: A Type-Theoretic
journalSIGPLAN Not. volume51,
number1 (dateJan. year2016),

authorpersonSumit Gulwani.
Automating string processing in spreadsheets using
input-output examples. In booktitleProceedings of the 38th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL 2011, Austin, TX, USA, January 26-28, 2011,
editorpersonThomas Ball and personMooly
Sagiv (Eds.). publisherACM, pages317–330.

[Gulwani, Polozov, and SinghGulwani
et al2017]
authorpersonSumit Gulwani, personOleksandr
Polozov, and personRishabh Singh.
Program Synthesis.
journalFoundations and TrendsÂ® in Programming
Languages volume4, number1-2
(year2017), pages1–119.

[Itzhaky, Peleg, Polikarpova, Rowe, and
SergeyItzhaky et al2021]
authorpersonShachar Itzhaky, personHila
Peleg, personNadia Polikarpova, personReuben NS
Rowe, and personIlya Sergey. year2021.
Cyclic program synthesis. In
booktitleProceedings of the 42nd ACM SIGPLAN International
Conference on Programming Language Design and Implementation.

[Kitzelmann, Schmid, Olsson, and
KaelblingKitzelmann et al2006]
authorpersonEmanuel Kitzelmann, personUte
Schmid, personRoland Olsson, and personLeslie Pack
Kaelbling. year2006.
Inductive synthesis of functional programs: An
explanation based generalization approach.
journalJournal of Machine Learning Research
volume7, number2 (year2006).

[Kneuss, Kuraj, Kuncak, and SuterKneuss
et al2013]
authorpersonEtienne Kneuss, personIvan
Kuraj, personViktor Kuncak, and personPhilippe
Suter. year2013.
Synthesis modulo Recursive Functions. In
booktitleProceedings of the 2013 ACM SIGPLAN International
Conference on Object Oriented Programming Systems Languages & Applications
(Indianapolis, Indiana, USA) (seriesOOPSLA '13).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages407–426.

[Lau, Domingos, and WeldLau
et al2003]
authorpersonTessa Lau, personPedro
Domingos, and personDaniel S Weld.
Learning programs from traces using version space
algebra. In booktitleProceedings of the 2nd international
conference on Knowledge capture. pages36–43.

[Le and GulwaniLe and Gulwani2014]
authorpersonVu Le and personSumit
Gulwani. year2014.
Flashextract: A framework for data extraction by
examples. In booktitleProceedings of the 35th ACM SIGPLAN
Conference on Programming Language Design and Implementation.

[Lubin, Collins, Omar, and ChughLubin
et al2020]
authorpersonJustin Lubin, personNick
Collins, personCyrus Omar, and personRavi Chugh.
Program Sketching with Live Bidirectional
journalProc. ACM Program. Lang.
volume4, numberICFP, Article articleno109
(dateAug. year2020), numpages29 pages.

authorpersonParthasarathy Madhusudan.
Synthesizing reactive programs. In
booktitleComputer Science Logic (CSL'11)-25th International
Workshop/20th Annual Conference of the EACSL. Schloss
Dagstuhl-Leibniz-Zentrum fuer Informatik.

[Odena, Shi, Bieber, Singh, and SuttonOdena
et al2020]
authorpersonAugustus Odena, personKensen
Shi, personDavid Bieber, personRishabh Singh, and
personCharles Sutton. year2020.
BUSTLE: Bottom-up program-Synthesis Through
Learning-guided Exploration.
journalarXiv preprint arXiv:2007.14381

[Osera and ZdancewicOsera and
authorpersonPeter-Michael Osera and
personSteve Zdancewic. year2015.
Type-and-example-directed program synthesis. In
booktitleProceedings of the 36th ACM SIGPLAN Conference
on Programming Language Design and Implementation, Portland, OR, USA, June
15-17, 2015, editorpersonDavid Grove and
personStephen M. Blackburn (Eds.). publisherACM,

[Polikarpova, Kuraj, and
Solar-LezamaPolikarpova et al2016]
authorpersonNadia Polikarpova, personIvan
Kuraj, and personArmando Solar-Lezama.
Program synthesis from polymorphic refinement
types. In booktitleProceedings of the 37th ACM SIGPLAN
Conference on Programming Language Design and Implementation, PLDI 2016,
Santa Barbara, CA, USA, June 13-17, 2016,
editorpersonChandra Krintz and
personEmery Berger (Eds.). publisherACM,

[Polozov and GulwaniPolozov and
authorpersonOleksandr Polozov and
personSumit Gulwani. year2015.
Flashmeta: A framework for inductive program
synthesis. In booktitleProceedings of the 2015 ACM SIGPLAN
International Conference on Object-Oriented Programming, Systems, Languages,
and Applications. pages107–126.

[Rolim, Soares, D'Antoni, Polozov, Gulwani,
Gheyi, Suzuki, and HartmannRolim et al2017]
authorpersonReudismam Rolim, personGustavo
Soares, personLoris D'Antoni, personOleksandr
Polozov, personSumit Gulwani, personRohit Gheyi,
personRyo Suzuki, and personBjörn Hartmann.
Learning syntactic program transformations from
examples. In booktitle2017 IEEE/ACM 39th International
Conference on Software Engineering (ICSE). IEEE, pages404–415.

[Shi, Steinhardt, and LiangShi
et al2019]
authorpersonKensen Shi, personJacob
Steinhardt, and personPercy Liang.
Frangel: component-based synthesis with control
journalProceedings of the ACM on Programming
Languages volume3, numberPOPL
(year2019), pages1–29.

authorpersonPhillip D Summers.
A methodology for LISP program construction from
journalJournal of the ACM (JACM)
volume24, number1 (year1977),

[Udupa, Raghavan, Deshmukh, Mador-Haim, Martin,
and AlurUdupa et al2013]
authorpersonAbhishek Udupa, personArun
Raghavan, personJyotirmoy V Deshmukh, personSela
Mador-Haim, personMilo MK Martin, and personRajeev
Alur. year2013.
TRANSIT: specifying protocols with concolic
journalACM SIGPLAN Notices volume48,
number6 (year2013), pages287–296.

[Wang, Dillig, and SinghWang
et al2017a]
authorpersonXinyu Wang, personIsil Dillig,
and personRishabh Singh. year2017a.
Program Synthesis Using Abstraction Refinement.
journalProc. ACM Program. Lang.
volume2, numberPOPL, Article articleno63
(dateDec. year2017), numpages30 pages.

[Wang, Dillig, and SinghWang
et al2017b]
authorpersonXinyu Wang, personIsil Dillig,
and personRishabh Singh. year2017b.
Synthesis of Data Completion Scripts Using Finite
Tree Automata.
journalProc. ACM Program. Lang.
volume1, numberOOPSLA, Article
articleno62 (dateOct. year2017),
numpages26 pages.

[Wang, Wang, and DilligWang
et al2018]
authorpersonYuepeng Wang, personXinyu Wang,
and personIsil Dillig. year2018.
Relational Program Synthesis.
journalProc. ACM Program. Lang.
volume2, numberOOPSLA, Article
articleno155 (dateOct. year2018),
numpages27 pages.

§ ADDITIONAL ALGORITHMS

Ground specification
A queue element $(pri,P,\witness,\groundSpec)$, or $\bot$.
$res \gets \Call{SynthesizeAngelic}{\groundSpec}$
$pri \gets |P|$

Ground specification
A program $P$, or $\bot$.
$PQ \gets$ Empty
PQ $\neq$ Empty
$(\_,P,\witness,\groundSpec) \gets PQ.\textsc{Pop}()$
$P \models \groundSpec$ $P$
$PQ.\textsc{Push}(\Call{MakeQE}{\groundSpec \wedge \witness})$
$PQ.\textsc{Push}(\Call{MakeQE}{\groundSpec \wedge \neg\witness})$

Recursive Synthesis Algorithm Guaranteeing Optimality

§ PROOFS

§.§ Completeness of

We prove the completeness of by introducing the following definition and using it to prove the claim.

We define $\Respects(e \Downarrow v,\varphi)$ as the following.

(e_2 ⇓v_2, φ)

(e_1 [v_2/x] ⇓v_3, φ)

SAT(φ∧f(v_2) = v_3)

(( f(x)=e_1) e_2 ⇓v_3, φ)

( ⇓, φ)

(e_1 ⇓v_1,φ)

(e_2 ⇓v_2,φ)

((e_1,e_2) ⇓(v_1,v_2),φ)

(e ⇓(v_1,v_2), φ)

( e ⇓v_1, φ)

(e ⇓(v_1,v_2), φ)

( e ⇓v_2, φ)

(e ⇓v, φ)

( e ⇓ v, φ)

(e ⇓v, φ)

( e ⇓ v, φ)

(e ⇓ v, φ)

( e ⇓v, φ)

(e ⇓ v, φ)

( e ⇓v, φ)

(e_3 ⇓ v_3, φ)

(e_1 ⇓v_1, φ)

( e_3  x_1 →e_1  x_2 →e_2
⇓v_1, φ)

(e_3 ⇓ v_3, φ)

(e_2 ⇓v_2, φ)

( e_3  x_1 →e_1  x_2 →e_2
⇓v_2, φ)

The following lemma relates the semantics in <ref> and the relation.

$\Respects(e \Downarrow v,\varphi) \implies e \Downarrow^\varphi v$

We proceed by structural induction on the evaluation of .

Case Unit:

By the angelic semantics it always holds that $\texttt{unit} \Downarrow^\varphi \texttt{unit}$.

Case Tuple Construction:

Suppose the last rule applied was

\[
\inferrule
\Respects(e_1 \Downarrow v_1,\varphi)\\
\Respects(e_2 \Downarrow v_2,\varphi)
\Respects((e_1,e_2) \Downarrow (v_1,v_2),\varphi)
\]

By IH, $e_1 \Downarrow^\varphi v_1$ and $e_2 \Downarrow^\varphi v_2$.

By the angelic semantics, we have the following derivation:

\[
\inferrule
e_1 \Downarrow^\varphi v_1\\
e_2 \Downarrow^\varphi v_2
(e_1,e_2) \Downarrow^\varphi (v_1,v_2)
\]

Therefore, $(e_1,e_2) \Downarrow^\varphi (v_1,v_2)$.

Case Function Application:

Suppose the last rule applied was:

\[
\inferrule
\Respects(e_2 \Downarrow v_2,\varphi)\\
\Respects(e_1[\texttt{rec}\ f(x)=e_1/f,v_2/x] \Downarrow v_3,\varphi)\\
\mathsf{SAT}(\varphi\wedge f(v_2) = v_3)
\Respects((\texttt{rec}\ f(x)=e_1)\ e_2 \Downarrow v_3,\varphi)
\]

By IH, $e_2 \Downarrow^\varphi v_2$.
It also holds that $\mathsf{SAT}(\varphi \wedge f(v_2) = v_3)$.

By the angelic semantics, we have the following derivation:

\[
\inferrule
e_2 \Downarrow^\varphi v_2\\
\mathsf{SAT}(\varphi\wedge f(v_2) = v_3)
f(e_2) \Downarrow^\varphi v_3
\]

Therefore, $f(e_2) \Downarrow^\varphi v_3$.

The rest of the rules follow similarly.

Case $e = \mlstinline{fst}\ e'$.
Assume that $e' \Downarrow^\varphi (v_1, v_2)$ by induction.

Only one rule matches and thus $e \Downarrow^\varphi v_1$.

Case $e = \mlstinline{snd}\ e'$.
Assume that $e' \Downarrow^\varphi (v_1, v_2)$ by induction.

Only one rule matches and thus $e \Downarrow^\varphi v_2$.

Case $e = \mlstinline{inl}\ e'$.
Assume that $e' \Downarrow^\varphi v$ by induction.

Only one rule matches and thus $e \Downarrow^\varphi \mlstinline{inl}\ v$.

Case $e = \mlstinline{inr}\ e'$.
Assume that $e' \Downarrow^\varphi v$ by induction.

Only one rule matches and thus $e \Downarrow^\varphi \mlstinline{inr}\ v$.

Case $e = \mlstinline{unl}\ e'$.
Assume that $e' \Downarrow^\varphi \mlstinline{inl}\ v$ by induction.
Only one rule matches and thus $e \Downarrow v$.

Case $e = \mlstinline{unr}\ e'$.
Assume that $e' \Downarrow^\varphi \mlstinline{inr}\ v$ by induction.
Only one rule matches and thus $e \Downarrow v$.

Case $e = \mlstinline{f}\ e'$.
Assume that $e' \Downarrow^\varphi v'$ and $\mathsf{SAT}((f(v') = v) \wedge \varphi)$ by induction.
Only one rule matches and thus $e \Downarrow^\varphi v$.

case $e = P = \mlstinline{rec f}(x) = e\\
e[v/x] \Downarrow^\varphi v'
v' \in \SemanticsOf{P}^\Spec(v)

Case $e = e_1 e_2$.
Assume that $e_1 ⇓^φlet rec f(x) = e'$, $e_2 ⇓^φv_2$, and $e'[rec f(x)=e'/f,v_2/x] ⇓^φv$ by induction.
Only one rule matches and thus $e ⇓^φv$.
$inr x_2 →e_2 ⇓v_1$
Case $e = switch e_3 on inl x_1 →e_1 |inr x_2 →e_2$.
\begin{itemize}
\item
Assume that $e_3 \Downarrow^\varphi \mlstinline{inl}\ v_3$ and $e_1 \Downarrow^\varphi v_1$ by induction.
Only one rule matches and thus $e \Downarrow^\varphi v_1$.
\item
Assume that $e_3 \Downarrow^\varphi \mlstinline{inr}\ v_3$ and $e_2 \Downarrow^\varphi v_2$ by induction.
Only one rule matches and thus $e \Downarrow^\varphi v_2$.
\end{itemize}
\fi
\end{proof}

\begin{lemma}\label{lemma:rec}
If $P \models \varphi$ and $P \gets \texttt{rec }f(x) = e$, then for all $v, v'$ where $v' \in \SemanticsOf{P}(v)$, it holds that $\Respects(P(v) \Downarrow v',\varphi)$.
\end{lemma}
\begin{proof}
%By induction on the derivation of $v' \in $ \SemanticsOf{P}($v$).
By induction on the derivation of $P(v) \Downarrow v'$.

Case {\sc Unit}: If $P(v) = \mlstinline{unit}$, then $\mlstinline{unit} \Downarrow \mlstinline{unit}$. It follows that $\Respects(\mlstinline{unit} \Downarrow \mlstinline{unit}, \varphi)$.

Case {\sc Tuple Construction}:
Suppose the last rule applied was
\[
\inferrule
e_1 \Downarrow v_1\\
e_2 \Downarrow v_2\\
(e_1,e_2) \Downarrow (v_1,v_2)
\]

By IH, $\Respects(e_1 \Downarrow v_1, \varphi)$ and $\Respects(e_2 \Downarrow v_2, \varphi)$.

By the semantics of \Respects, we have the following derivation:
\[
\inferrule
\Respects(e_1 \Downarrow v_1, \varphi)\\
\Respects(e_2 \Downarrow v_2, \varphi)
\Respects((e_1,e_2) \Downarrow (v_1,v_2), \varphi)
\]
Therefore, $\Respects((e_1,e_2) \Downarrow (v_1,v_2), \varphi)$.

Case {\sc Function Application}:
Suppose the last rule applied was:
\[
\inferrule
e_2 \Downarrow v_2\\
e_1[\texttt{rec f}(x)=e_1/f,v_2/x],v_2/x] \Downarrow v_3\\
(\texttt{rec f}(x)=e_1)\ e_2 \Downarrow v_3
\]
By IH, $\Respects(e_2 \Downarrow v_2, \varphi)$ and $\Respects(e_1[\texttt{rec f}(x)=e_1/f,v_2/x] \Downarrow v_3, \varphi)$.
It also holds that $\mathsf{SAT}(\varphi \wedge f(v_2) = v_3)$ which follows from the fact that $P \models \varphi$.

By the semantics of \Respects, we have the following derivation:
\[
\inferrule
\Respects(e_2 \Downarrow v_2,\varphi)\\
\Respects(e_1[\texttt{rec}\ f(x)=e_1/f,v_2/x] \Downarrow v_3,\varphi)\\
\mathsf{SAT}(\varphi\wedge f(v_2) = v_3)
\Respects((\texttt{rec}\ f(x)=e_1)\ e_2 \Downarrow v_3,\varphi)
\]
Therefore, $\Respects(f(e_2) \Downarrow v_3, \varphi)$.

The rest of the rules follow similarly.

\iffalse
Suppose that $P \models \varphi$ and $P \gets \texttt{rec }f(x) = e$. Let $v, v'$ be values such that $v' \in \SemanticsOf{P}(v)$.

By the angelic semantics, $v' \in \SemanticsOf{P(v)}$ and $P \gets \texttt{rec } f(x) = e$ implies that $e[v/x] \Downarrow^\varphi v'$ by inversion of the last rule in \autoref{fig:angelic-semantics}.
Therefore, it holds that $\Respects(e[v/x] \Downarrow v',\varphi)$.
\fi
\end{proof}

\begin{lemma}\label{lemma:semantics}
If $P \models \varphi$ then then $P \angelicmodels \varphi$
\end{lemma}
\begin{proof}
By the previous two lemmas, the conclusion follows.

Let $v$ be a value. We want to show there exists a value $v'$ such that $v' \in [[P]](v)$.

By Lemma \ref{lemma:rec}, $\Respects(e[v/x] \Downarrow v',\varphi)$.

By Lemma \ref{lemma:respects}, $e[v/x] \Downarrow^\varphi v'$, thus $v' \in [[P]](v)$.
\end{proof}

% \autoref{alg:core-recursive-synthesis}
% \autoref{alg:angelic-synthesis}
\begin{theorem}{\bf (Completeness)}
Suppose that (1) \SynthesizeAngelic \ is complete,
and (2) if \SynthesizeAngelic \ returns $\mathsf{Failure}(\kappa)$, then $\kappa$ satisfies the assumption from \autoref{eq:anti-spec}.
If $\Synthesize(\chi)$ returns $\bot$, then there is no program that satisfies $\chi$.
\end{theorem}
\begin{proof}[Proof of \autoref{thm:completeness}]
The statement of the completeness of \SynthesizeAngelic is as follows: If \SynthesizeAngelic$(\chi)$ returns $\mathsf{Failure}(\kappa)$, then there is no program $P$ such that $P \angelicmodels \chi$.

Assume that there is a program $S$ such that $S \models \chi$.
Suppose that \SynthesizeAngelic$(\groundSpec \land \bigwedge_{\phi_i \in \Omega} \neg\phi_i)$ returns $\mathsf{Failure}(\kappa)$.
By assumption (1), there is no program $P$ such that $P \angelicmodels \chi$. By \autoref{lemma:semantics}, there is no program $P$ such that $P \models \chi$.
Thus, $S \not\models \groundSpec$ which contradicts our assumption.
\iffalse
By assumption (2),
\forall P. \ \forall \phi \in \kappa. \ P \models \phi \Rightarrow P \not \models \groundSpec
By assumption (1), $\kappa$ is non-empty, which means that $S \not\models \groundSpec$ which contradicts our assumption.
\fi

Thus, \SynthesizeAngelic$(\groundSpec \land \bigwedge_{\phi_i \in \Omega} \neg\phi_i)$ always returns $\mathsf{Success}(P,\witness)$.
If $P \models \groundSpec$ then the algorithm returns $P \neq \bot$ and the conclusion holds.

Suppose that $P \not\models \groundSpec$.
Then it must be the case that either $\Synthesize(\chi \land \witness) \neq \bot$ or $\Synthesize(\chi \land \neg\witness) \neq \bot$, otherwise it would contradict assumption (1) and the assumption that there is some program $S$ such that $S \models \groundSpec$.
Furthermore, recursive calls do not destroy the invariant that $\Omega$ is an anti-specification due to assumption (2).
Thus, the algorithm returns some program $P \neq \bot$ and the conclusion holds.

Therefore, the theorem holds in all cases.

\iffalse
Suppose that \SynthesizeAngelic$(\groundSpec \land \bigwedge_{\phi_i \in \Omega} \neg\phi_i)$ returns $\mathsf{Failure}(\kappa)$.
Assuming $P$

Suppose $\Synthesize(\chi)$ returns $\bot$.
If \SynthesizeAngelic$(\groundSpec \land \bigwedge_{\phi_i \in \Omega} \neg\phi_i)$ returns $\mathsf{Failure}(\kappa)$, then by assumption (2),
\forall P. \ \forall \phi \in \kappa. \ P \models \phi \Rightarrow P \not \models \groundSpec
By assumption (1), $\kappa$ is non-empty in this case, therefore the conclusion holds.

If \SynthesizeAngelic$(\groundSpec \land \bigwedge_{\phi_i \in \Omega} \neg\phi_i)$ returns $\mathsf{Success}(P,\witness)$.
Suppose that $P \models \groundSpec$, then the algorithm would return $P$ which would contradict our conclusion.
However, by assumption (1), since the algorithm returns $P$, it must hold that $P \angelicmodels \groundSpec$,
\forall P. \ \forall \phi \in \kappa. \ P \models \groundSpec \land \bigwedge_{\phi_i \in \Omega} \neg\phi_i \Rightarrow P \not\models \phi
\fi
\end{proof}
\iffalse
If \SynthesizeAngelic is complete

Show angelic satisfaction is weaker than the larger one

Suppose $(χ)$ returns $$ but there is a program $P$ that satisfies $χ$ under the assumptions above.

Suppose $P$ is $unit$.
\fi

\subsection{Completeness of {\sc BuildAngelicFTA}}
\begin{lemma}
If {\sc BuildAngelicFTA}$(v_{in},\varphi)$ returns $\fta$ and $(T,L)$ is an run on $\fta$ where $L(\mathsf{root}(T)) \neq \bot$, then $T \Downarrow^\varphi v$ where
$L(\mathsf{root}(T)) = q_v$
\end{lemma}
\begin{proof}
By induction on the tree $T$.
Assume the root is a node $n$ with children $\set{n_1,\dots,n_k}$.
Proceed by cases on $\textsf{Label}(T)$.

Case {$\textsf{Label}(n) = \mlstinline{x}$}:
By inversion, then $L(n) = q_{v_{in}}$. $x[v_{in}] \Downarrow^\varphi v_{in}$, as desired.

Case {$\textsf{Label}(n) = \mlstinline{unit}$}:
By inversion, then $L(n) = q_{\texttt{unit}}$. $unit[v_{in}] \Downarrow^\varphi \texttt{unit}$, as desired.

Case {$\textsf{Label}(n) = \mlstinline{switch on inl/inr}$}:
By inversion, then either it comes from a left or a right $\bot$ rule. Without loss of generality, assume it's a right $\bot$ rule, since the left side follows a symmetric argument.
Then, $L(n) = q_{v_1}$ and $\mathsf{children}(n) = [n_1,n_2,n_3]$ where $L(n_1) = q_{\mlstinline{inl}\ v_3}$, $L(n_2) = q_{v_1}$, and $L(n_3) = \bot$.

By IH, $n_1[v/x] \Downarrow^\varphi \mlstinline{inl}\ v_3$ and $n_2[v/x] \Downarrow^\varphi v_1$.
Thus, we have the following deduction:
\[
\inferrule*
n_1[v/x] \Downarrow^\varphi \mlstinline{inl}\ v_3\\
n_2[v/x] \Downarrow^\varphi v_1
\mlstinline{switch}\ n_1[v/x]\ \mlstinline{on inl _}\ \rightarrow n_2[v/x] \mid \mlstinline{inr _}\ \rightarrow n_3[v/x]  \Downarrow^\varphi (v_1,v_2)
\]

Since we can rewrite $\mlstinline{switch}\ n_1[v/x]\ \mlstinline{on inl _}\ \rightarrow n_2[v/x]\mid \mlstinline{inr _}\ \rightarrow n_3[v/x]$ as $(\mlstinline{switch}\ n_1\ \mlstinline{on inl _} \rightarrow n_2 \mid \mlstinline{inr _} \rightarrow n_3)[v/x]$,