11institutetext: Utrecht University, The Netherlands, 11email:
<EMAIL_ADDRESS>22institutetext: Open University of The
Netherlands, The Netherlands, 22email<EMAIL_ADDRESS>
# Program Synthesis Using Example Propagation

Niek Mulleners 11 0000-0002-7934-6834 Johan Jeuring 11 0000-0001-5645-7681
Bastiaan Heeren 22 0000-0001-6647-6130

###### Abstract

We present Scrybe, an example-based synthesis tool for a statically-typed
functional programming language, which combines top-down deductive reasoning
in the style of $\lambda^{2}$ with Smyth-style live bidirectional evaluation.
During synthesis, example constraints are propagated through sketches to prune
and guide the search. This enables Scrybe to make more effective use of
functions provided in the context. To evaluate our tool, it is run on the
combined, largely disjoint, benchmarks of $\lambda^{2}$ and Myth. Scrybe is
able to synthesize most of the combined benchmark tasks.

###### Keywords:

Program Synthesis Constraint Propagation Input-Output Examples Functional
Programming

##  1 Introduction

Type-and-example driven program synthesis is the process of automatically
generating a program that adheres to a type and a set of input-output
examples. The general idea is that the space of type-correct programs is
enumerated, evaluating each program against the input-output examples, until a
program is found that does not result in a counterexample. Recent work in this
field has aimed to make the enumeration of programs more efficient, using
various pruning techniques and other optimizations. Hoogle+ [4] and Hectare
[6] explore efficient data structures to represent the search space. Smith and
Albarghouthi [12] describe how synthesis procedures can be adapted to only
consider programs in normal form. MagicHaskeller [5] and RESL [11] filter out
programs that evaluate to the same result. Instead of only using input-output
examples for the verification of generated programs, Myth [10, 9], Smyth [7],
and $\lambda^{2}$ [3] use input-output examples during pruning, by eagerly
checking incomplete programs for counterexamples using constraint propagation.

####  1.0.1 Constraint Propagation

Top-down synthesis incrementally builds up a sketch, a program which may
contain holes (denoted by $\CIRCLE$). Holes may be annotated with constraints,
e.g. type constraints. During synthesis, holes are filled with new sketches
(possibly containing more holes) until no holes are left. For example, for
type-directed synthesis, let us start from a single hole $\CIRCLE_{0}$
annotated with a type constraint:

$\CIRCLE_{0}::\textit{List}~{}\textit{Nat}\rightarrow\textit{List}~{}\textit{Nat}$

We may fill $\CIRCLE_{0}$ using the function $\textsf{map}::(a\rightarrow
b)\rightarrow\textit{List}~{}a\rightarrow\textit{List}~{}b$, which applies a
function to the elements of a list. This introduces a new hole $\CIRCLE_{1}$,
with a new type constraint:

$\CIRCLE_{0}::\textit{List}~{}\textit{Nat}\rightarrow\textit{List}~{}\textit{Nat}\quad\xrightarrow{\textsf{map}}\quad\textsf{map}~{}(\CIRCLE_{1}::\textit{Nat}\rightarrow\textit{Nat})$

We say that the constraint on $\CIRCLE_{0}$ is propagated through map to the
hole $\CIRCLE_{1}$. Note that type information is preserved: the type
constraint on $\CIRCLE_{0}$ is satisfied exactly if the type constraint on
$\CIRCLE_{1}$ is satisfied. We say that the hole filling
$\CIRCLE_{0}\mapsto\textsf{map}~{}\CIRCLE_{1}$ refines the sketch with regards
to its type constraint.

A similar approach is possible for example constraints, which partially
specify the behavior of a function using input-output pairs. For example, we
may further specify hole $\CIRCLE_{0}$, to try and synthesize a program that
doubles each value in a list:111In this example, as well as in the rest of
this paper, we will leave type constraints implicit.

$\CIRCLE_{0}\vDash\left\\{\begin{array}[]{c}[0,1,2]\mapsto[0,2,4]\end{array}\right\\}$

Now, when introducing map, we expect its argument $\CIRCLE_{1}$ to have three
example constraints, representing the doubling of a natural number:

$\CIRCLE_{0}\vDash\left\\{\begin{array}[]{c}[0,1,2]\mapsto[0,2,4]\end{array}\right\\}\quad\xrightarrow{\textsf{map}}\quad\textsf{map}~{}(\CIRCLE_{1}\vDash\left\\{\begin{array}[]{c}0\mapsto
0\\\ 1\mapsto 2\\\ 2\mapsto 4\end{array}\right\\})$

Similar to type constraints, we want example constraints to be correctly
propagated through each hole filling, such that example information is
preserved. Unlike with type constraints, which are propagated through hole
fillings using type checking/inference, it is not obvious how to propagate
example constraints through arbitrary functions. Typically, synthesizers
define propagation of example constraints for a hand-picked set of functions
and language constructs. Feser et al. [3] define example propagation for a set
of combinators, including map and foldr, for their synthesizer $\lambda^{2}$.
Limited to this set of combinators, $\lambda^{2}$ excels at composition, but
lacks in generality. Myth [10, 9], and by extension Smyth [7], take a more
general approach, in exchange for compositionality, defining example
propagation for basic language constructs, including constructors and pattern
matches.

$\begin{array}[]{c}\boxed{\begin{array}[]{ll}\\{-\\#~{}\text{USE}~{}\dots~{}\\#-\\}&\textbf{assert}~{}\textsf{dupli}~{}[\>]\vDash[\>]\\\
\textsf{dupli}::\textit{List}~{}a\rightarrow\textit{List}~{}a&\textbf{assert}~{}\textsf{dupli}~{}[0]\vDash[0,0]\\\
\textsf{dupli}~{}xs=\CIRCLE&\textbf{assert}~{}\textsf{dupli}~{}[0,1]\vDash[0,0,1,1]\\\
\end{array}}\\\ \\\
\begin{array}[]{l|l}\begin{array}[]{l}\\{-\\#~{}\text{USE}~{}\textsf{foldr}~{}\\#-\\}\\\\[2.0pt]
\boxed{\CIRCLE\mapsto\textsf{foldr}~{}(\lambda
x~{}r.~{}x:x:r)~{}[\>]~{}xs}\end{array}&\begin{array}[]{l}\\{-\\#~{}\text{USE}~{}\textsf{concat},\textsf{map}~{}\\#-\\}\\\\[2.0pt]
\boxed{\CIRCLE\mapsto\textsf{concat}~{}(\textsf{map}~{}(\lambda
x.~{}[x,x])~{}xs)}\end{array}\\\ \\\ \hline\cr\\\
\begin{array}[]{l}\\{-\\#~{}\text{USE}~{}\textsf{foldl},\textsf{($\mathbin{+\mkern-10.0mu+}$)}~{}\\#-\\}\\\\[2.0pt]
\boxed{\CIRCLE\mapsto\textsf{foldl}~{}(\lambda
r~{}x.~{}r\mathbin{+\mkern-10.0mu+}[x,x])~{}[\>]~{}xs}\end{array}&\begin{array}[]{l}\\{-\\#~{}\text{USE}~{}\textsf{interleave}~{}\\#-\\}\\\\[2.0pt]
\boxed{\CIRCLE\mapsto\textsf{interleave}~{}xs~{}xs}\end{array}\end{array}\end{array}$
Figure 1: (Top) A program sketch in Scrybe, for synthesizing the function
dupli, which duplicates each value in a list. (Bottom) Different synthesis
results returned by Scrybe, for different sets of included functions.

#### Presenting Scrybe

In this paper, we explore how the techniques of $\lambda^{2}$ and Smyth can be
combined to create a general-purpose, compositional example driven
synthesizer, which we will call Scrybe. Figure 1 shows four different
interactions with Scrybe, where the function dupli is synthesized with
different sets of functions. Scrybe is able to propagate examples through all
of the provided functions using live bidirectional evaluation as introduced by
Lubin et al. [7] for their synthesizer Smyth, originally intended to support
sketching [13, 14]. By choosing the right set of functions (for example, the
set of combinators used in $\lambda^{2}$), Scrybe is able to cover different
synthesis domains. Additionally, allowing the programmer to choose this set of
functions opens up a new way for them to express their intent to the
synthesizer, without going out of their way to provide an exact specification.

#### Main Contributions

The contributions of this paper are as follows:

  * •

We give an overview of example propagation and how it can be used to perform
program synthesis (Section 2).

  * •

We show how live bidirectional evaluation as introduced by Lubin et al. [7]
allows arbitrary sets of functions to be used as refinements during program
synthesis (Section 3).

  * •

We present Scrybe, an extension of Smyth [7] and evaluate it against existing
benchmarks from different synthesis domains (Section 4).

##  2 Example Propagation

Example constraints give a specification of a function in terms of input-
output pairs. For example, the following constraint represents the function
mult that multiplies two numbers.

$\left\\{\begin{array}[]{c}0\ \ 1\mapsto 0\\\ 1\ \ 1\mapsto 1\\\ 2\ \ 3\mapsto
6\end{array}\right\\}$

The constraint consists of three input-output examples. Each arrow ($\mapsto$)
maps the inputs on its left to the output on its right. A function can be
checked against an example constraint by evaluating it on the inputs and
matching the results against the corresponding outputs. During synthesis, we
want to check that generated expressions adhere to these constraints. For
example, to synthesize mult, we may generate a range of expressions of type
$\textit{Nat}\rightarrow\textit{Nat}\rightarrow\textit{Nat}$ and then check
each against the example constraint. The expression $\lambda
x~{}y.~{}\textsf{double}~{}(\textsf{plus}~{}x~{}y)$ will be discarded, as it
maps the inputs to $2$, $4$ and $10$, respectively. It would be more
efficient, however, to recognize that any expression of the form $\lambda
x~{}y.~{}\textsf{double}~{}e$, for some expression $e$, can be discarded,
since there is no natural number whose double is $1$.

To discard incorrect expressions as early as possible, we incrementally
construct a sketch, where each hole (denoted by $\CIRCLE$) is annotated with
an example constraint. Each time a hole is filled, the example constraints are
propagated to the new holes and checked for contradictions. Let us start from
a single hole $\CIRCLE_{0}$. We refine the sketch by eta-expansion, binding
the inputs to the variables $x$ and $y$.

$\CIRCLE_{0}\vDash\left\\{\begin{array}[]{c}0\ \ 1\mapsto 0\\\ 1\ \ 1\mapsto
1\\\ 2\ \ 3\mapsto 6\end{array}\right\\}\quad\xrightarrow{\textbf{eta-
expand}}\quad\lambda
x~{}y.~{}(\CIRCLE_{1}\vDash\left\\{\begin{array}[]{cc|c}x&y\\\ 0&1&0\\\
1&1&1\\\ 2&3&6\end{array}\right\\})$

A new hole $\CIRCLE_{1}$ is introduced, annotated with a constraint that
captures the values of $x$ and $y$. Example propagation through double should
be able to recognize that the value $1$ is not in the codomain of double, so
that the hole filling
$\boxed{\CIRCLE_{1}\mapsto\textsf{double}~{}\CIRCLE_{2}}$ can be discarded.

###  2.1 Program Synthesis Using Example Propagation

Program synthesizers based on example propagation iteratively build a program
by filling holes. At each iteration, the synthesizer may choose to fill a hole
using either a refinement or a guess. A refinement is an expression for which
example propagation is defined. For example, eta-expansion is a refinement, as
shown in the previous example. To propagate an example constraint through a
lambda abstraction, we simply bind the inputs to the newly introduced
variables. A guess is an expression for which example propagation is _not_
defined. The new holes introduced by a guess will not have example
constraints. Once you start guessing, you have to keep guessing! Only when all
holes introduced by guessing are filled can the expression be checked against
the example constraint. In a sense, guessing comes down to brute-force
enumerative search.

Refinements are preferred over guesses, since they preserve constraint
information, which is needed to prune the search space. It is, however, not
feasible to define example propagation for every possible expression. Instead,
previous synthesizers define only a hand-picked set of refinements. In the
rest of this section, we show how the synthesizers $\lambda^{2}$, Myth and
Smyth implement and use example propagation.

###  2.2 Example Propagation in $\lambda^{2}$

For the tool $\lambda^{2}$, Feser et al. [3] define deduction rules for a set
of combinators, including map, foldr, and filter. In essence, these deduction
rules propagate examples through the respective combinators. For example,
consider map, which maps a function over a list. Refinement using map replaces
a constraint on a list with constraints on its elements, while checking that
the input and output lists have equal length, and that no value in the input
list is mapped to different values in the output list.

$\begin{array}[]{rccc}&\textsf{inc}&\textsf{compress}&\textsf{reverse}\\\\[2.0pt]
\CIRCLE_{0}\vDash&\left\\{\begin{array}[]{c}[0,1,2]\mapsto[1,2,3]\end{array}\right\\}&\left\\{\begin{array}[]{c}[0,0]\mapsto[0]\end{array}\right\\}&\left\\{\begin{array}[]{c}[0,0,1]\mapsto[1,0,0]\end{array}\right\\}\\\\[3.0pt]
\CIRCLE_{1}\vDash&\left\\{\begin{array}[]{c}0\mapsto 1\\\ 1\mapsto 2\\\
2\mapsto 3\end{array}\right\\}&\left\\{\begin{array}[]{c}0\mapsto 0\\\
0\mapsto\phantom{0}\\\ \end{array}\right\\}&\left\\{\begin{array}[]{c}0\mapsto
1\\\ 0\mapsto 0\\\ 1\mapsto 0\end{array}\right\\}\\\ &&=\bot&=\bot\end{array}$
Figure 2: The inputs and outputs for example propagation through the hole
filling $\CIRCLE_{0}~{}\mapsto~{}\textsf{map}~{}\CIRCLE_{1}$, for example
constraints taken from the functions inc, compress and reverse. The latter two
cannot be implemented using map, which is reflected in the contradictory
constraints: for compress there is a length mismatch, and for reverse the same
input is mapped to different outputs.

See Figure 2 for examples of example propagation through map, for various
example constraints based on common functions on lists. The function inc,
which increments each number in a list by one, can be implemented using map.
As such, example propagation succeeds, resulting in a constraint which
represents incrementing a number by one. The function compress, which removes
consecutive duplicates from a list, cannot be implemented using map, since the
input and output lists can have different lengths. As such, example
propagation fails, as seen in Figure 2. The function reverse, which reverses a
list, has input and output lists of the same length. It can, however, not be
implemented using map, as map cannot take the positions of elements in a list
into account. This is reflected in the example in Figure 2, where the
resulting constraint is inconsistent, mapping $0$ to two different values.

For each combinator in $\lambda^{2}$, a deduction rule is defined that
captures the various properties relevant for example propagation. This allows
$\lambda^{2}$ to efficiently synthesize complex functions in terms of these
combinators. For example, $\lambda^{2}$ is able to synthesize a function
computing the Cartesian product in terms of foldr, believed to be the first
functional pearl [2].

$\lambda^{2}$ shows that synthesis using example propagation is feasible, but
it is not general purpose. Many synthesis problems require other recursion
schemes or are defined over different types. Example propagation can be added
for other functions in a similar fashion by adding new deduction rules, but
this is very laborious work.

###  2.3 Example Propagation in Myth

Osera and Zdancewic [10, 9] take a more general approach in their synthesizer
Myth, compared to $\lambda^{2}$, by focusing on structural recursion, rather
than a specific recursion scheme such as foldr. To do so, they describe how
example constraints can be propagated through constructors and pattern
matches. Note that their language does not contain primitive integers. Rather,
literals $0$, $1$, $2$, etc. are syntactic sugar for Peano-style natural
numbers.

$\textbf{data}~{}\textit{Nat}=\textsc{\small Zero}~{}|~{}\textsc{\small
Succ}~{}\textit{Nat}$

####  2.3.1 Constructors

To propagate a constraint through a constructor, we have to check that all
possible outputs agree with this constructor. For example, the constraint
$\left\\{\begin{array}[]{c}\textsc{\small Zero}\end{array}\right\\}$ can be
refined by the constructor Zero. No constraints need to be propagated, since
Zero has no arguments. In the next example, there are multiple possible
outputs, depending on the value of the variable $x$.

$\CIRCLE_{0}\vDash\left\\{\begin{array}[]{c|l}x\\\ \dots&\textsc{\small
Succ}~{}\textsc{\small Zero}\\\ \dots&\textsc{\small Succ}~{}(\textsc{\small
Succ}~{}\textsc{\small
Zero})\end{array}\right\\}\quad\xrightarrow{\textsc{\small
Succ}}\quad\textsc{\small
Succ}~{}(\CIRCLE_{1}\vDash\left\\{\begin{array}[]{c|l}x\\\
\dots&\textsc{\small Zero}\\\ \dots&\textsc{\small Succ}~{}\textsc{\small
Zero}\end{array}\right\\})$

Since every possible output is a successor, the constraint can be propagated
through Succ by removing one Succ constructor from each output, i.e.
decreasing each output by one. The resulting constraint on $\CIRCLE_{1}$
cannot be refined by a constructor, since the outputs do not all agree.

####  2.3.2 Pattern Matching

The elimination of constructors (i.e. pattern matching) is a bit more
complicated. Myth describes example propagation through non-nested pattern
matches, as long as the scrutinee has no holes. Consider the following
example, wherein the sketch $\textsf{double}=\lambda n.~{}\CIRCLE_{0}$ is
refined by propagating the constraint on $\CIRCLE_{0}$ through a pattern match
on the local variable $n$.

$\CIRCLE_{0}\vDash\left\\{\begin{array}[]{c|c}n\\\ 0&0\\\ 1&2\\\
2&4\end{array}\right\\}\quad\xrightarrow{\textbf{pattern
match}}\quad\begin{array}[]{l}\textbf{case}~{}n~{}\textbf{of}\\\
\quad\begin{array}[]{ll}\textsc{\small
Zero}&\rightarrow\CIRCLE_{1}\vDash\left\\{\begin{array}[]{c}0\end{array}\right\\}\\\\[1.42262pt]
\textsc{\small
Succ}~{}m&\rightarrow\CIRCLE_{2}\vDash\left\\{\begin{array}[]{c|c}m\\\ 0&2\\\
1&4\end{array}\right\\}\end{array}\end{array}$

Pattern matching on $n$ creates two branches, one for each constructor of Nat,
with holes on the right-hand side. The constraint on $\CIRCLE_{0}$ is
propagated to each branch by splitting up the constraint based on the value of
$n$. For brevity, we leave $n$ out of the new constraints. The newly
introduced variable $m$ is exactly one less than $n$, i.e. one Succ
constructor is stripped away.

####  2.3.3 Structural Recursion

With support for structural recursion, Myth is able to perform general-
purpose, propagation-based synthesis. To illustrate this, we show how Myth
synthesizes the function double, starting from the previous sketches. Hole
$\CIRCLE_{1}$ is easily refined with Zero. Hole $\CIRCLE_{2}$ can be refined
with Succ twice, since every output is at least 2:

$\CIRCLE_{2}\vDash\left\\{\begin{array}[]{c|c}m\\\ 0&2\\\
1&4\end{array}\right\\}\quad\xrightarrow{\textsc{\small
Succ}}\dots\xrightarrow{\textsc{\small Succ}}\quad\textsc{\small
Succ}~{}(\textsc{\small
Succ}~{}(\CIRCLE_{3}\vDash\left\\{\begin{array}[]{c|c}m\\\ 0&0\\\
1&2\end{array}\right\\}))$

At this point, to tie the knot, Myth should introduce the recursive call
$\textsf{double}~{}m$. Note, however, that double is not yet implemented, so
we cannot directly test the correctness of this guess. We can, however, use
the original constraint (on $\CIRCLE_{0}$) as a partial implementation of
double. The example constraint on $\CIRCLE_{3}$ is a subset of this original
constraint, with $m$ substituted for $n$. This implies that
$\textsf{double}~{}m$ is a valid refinement. This property of example
constraints, i.e. that the specification for recursive calls is a subset of
the original constraint, is known as trace completeness [9], and is a
prerequisite for synthesizing recursive functions in Myth.

###  2.4 Example Propagation in Smyth

In their synthesizer Smyth, Lubin et al. [7] extend Myth with sketching, i.e.
program synthesis starting from a sketch, a program containing holes. A global
example constraint is propagated through the sketch using example propagation,
after which Myth-style synthesis takes over using the local example
constraints.

Take for example the constraint
$\left\\{\begin{array}[]{c}[0,1,2]\mapsto[0,2,4]\end{array}\right\\}$, which
represents doubling each number in a list. The programmer may provide the
sketch $\textsf{map}~{}\CIRCLE$ as a starting point for the synthesis
procedure. In order to perform Myth-style synthesis, the constraint has to be
propagated through map, but unlike $\lambda^{2}$, Smyth does not provide a
handcrafted rule for map. Instead, Smyth determines how examples are
propagated through functions based on their implementation.

The crucial idea is that the sketch is first evaluated, essentially inlining
all function calls222Note that function calls within the branches of a stuck
pattern match are not inlined. until only simple language constructs remain,
each of which supports example propagation. Omar et al. [8] describe how to
evaluate an expression containing holes using live evaluation. The sketch is
applied to the provided input, after which map is inlined and evaluated as far
as possible:

$\textsf{map}~{}\CIRCLE~{}[0,1,2]\hfill\leadsto\hfill[\CIRCLE~{}0,~{}\CIRCLE~{}1,~{}\CIRCLE~{}2]$

At this point, the constraint can be propagated through the resulting
expression. Lubin et al. [7] extend Myth-style example propagation to work for
the primitives returned by live evaluation. The constraint is propagated
through the result of live evaluation.

$\begin{array}[]{l}[\CIRCLE~{}0,~{}\CIRCLE~{}1,~{}\CIRCLE~{}2]\vDash\left\\{\begin{array}[]{c}[0,2,4]\end{array}\right\\}\quad\longrightarrow^{*}\quad\begin{array}[]{rl}[&(\CIRCLE\vDash\left\\{\begin{array}[]{c}0\mapsto
0\end{array}\right\\})~{}0\\\
,&(\CIRCLE\vDash\left\\{\begin{array}[]{c}1\mapsto
2\end{array}\right\\})~{}1\\\
,&(\CIRCLE\vDash\left\\{\begin{array}[]{c}2\mapsto
4\end{array}\right\\})~{}2~{}]\end{array}\end{array}$

The constraints propagated to the different occurrences of $\CIRCLE$ in the
evaluated expression can then be collected and combined to compute a
constraint for $\CIRCLE$ in the input sketch.

$\textsf{map}~{}(\CIRCLE\vDash\left\\{\begin{array}[]{l}0\mapsto 0\\\ 1\mapsto
2\\\ 2\mapsto 4\end{array}\right\\})$

This kind of example propagation based on evaluation is called live
bidirectional evaluation. For a full description, see Lubin et al. [7]. Smyth
uses live bidirectional evaluation to extend Myth with sketching. Note,
however, that Smyth does not use live bidirectional evaluation to introduce
refinements during synthesis.

##  3 Program Synthesis Using Example Propagation

We define our synthesis problem as finding an expression of type $\tau$ in the
environment $\Gamma$ that adheres to example constraint $\varphi$. Inspired by
Smith and Albarghouthi [12], we give a high-level overview of the synthesis
procedure as a set of guarded rules that can be applied non-deterministically,
shown in Figure 4. We keep track of a set of candidate expressions
$\mathcal{E}$, which is initialized by the rule init and then expanded by the
rule expand until the rule final applies, returning a solution.

The rule init initializes $\mathcal{E}$ with a single hole $\CIRCLE_{0}$,
constrained by the synthesis parameters. Each invocation of the rule expand
non-deterministically picks an expression $e$ from $\mathcal{E}$ and a hole
$\CIRCLE_{i}$ in $e$ to fill, by generating a hole filling hf using the
context and type of $\CIRCLE_{i}$. If the resulting expression $e^{\prime}$
does not conflict with $\varphi$, it is considered a valid candidate and added
to $\mathcal{E}$. As an invariant, $\mathcal{E}$ only contains expressions
that do not conflict with $\varphi$. As such, a solution to the synthesis
problem is simply any expression that has no holes.

To implement a synthesizer according to these rules, we have to make the non-
deterministic choices explicit: we have to decide in which order expressions
are expanded ($e\in\mathcal{E}$); which holes are selected for expansion
($\CIRCLE\in\textit{holes}(e)$); and how hole fillings are generated based on
the hole’s type and environment ($\Gamma\vdash\textit{hf}:\tau$).
Additionally, we describe how expressions containing holes are checked against
the constraint $\varphi$.

$\inference{\Gamma\vdash\CIRCLE_{0}:\tau\vDash\varphi}{\mathcal{E}\leftarrow\\{\CIRCLE_{0}\\}}[\textsc{init}]$

$\inference{e\in\mathcal{E}&\CIRCLE_{i}\in\textit{holes}(e)\Gamma_{i}\vdash\textit{hf}:\tau_{i}\\\
e^{\prime}=[\CIRCLE_{i}\mapsto\textit{hf}\;]e\quad\quad
e^{\prime}\vDash\varphi}{\mathcal{E}\leftarrow\mathcal{E}\cup\\{e^{\prime}\\}}[\textsc{expand}]$

$\inference{e\in\mathcal{E}&\textit{holes}(e)=\emptyset}{e~{}\text{is a
solution}}[\textsc{final}]$

Figure 3: Program synthesis using example propagation as a set of guarded
rules that can be applied non-deterministically.

$\boxed{\begin{array}[]{l}\CIRCLE_{0}\mapsto\textsf{map}~{}(\lambda
x.~{}\CIRCLE_{1})~{}\CIRCLE_{2}\\\ \CIRCLE_{1}\mapsto\textsc{\small
Succ}~{}\CIRCLE_{3}\\\ \CIRCLE_{2}\mapsto xs\\\ \CIRCLE_{3}\mapsto
x\end{array}}$ Figure 4: A set of hole fillings synthesizing an expression
that increments each value in a list, starting from the sketch $\lambda
xs.~{}\CIRCLE_{0}$.

###  3.1 Expression Order

To decide in which order candidate expressions are selected for expansion, we
define an order on expressions by assigning a weight to each expression. We
keep track of all expressions in a priority queue and expand expressions in
increasing order of their weight. The weight of an expression is computed as
follows: we assign a weight of 1 to each application, as well as to each
pattern match and each call to a recursion scheme. Additionally, the weight of
scrutinees is doubled, to disincentivize pattern matching on large scrutinees.

###  3.2 Hole Order

Choosing in which order holes are filled during synthesis is a bit more
involved. Consider, for example, the hole fillings in Figure 4, synthesizing
the expression $\lambda xs.~{}\textsf{map}~{}(\lambda x.~{}\textsc{\small
Succ}~{}x)~{}xs$ starting from $\lambda xs.~{}\CIRCLE_{0}$. There are three
different synthesis paths that lead to this result, depending on which holes
are filled first. More specifically, $\CIRCLE_{2}$ can be filled independently
of $\CIRCLE_{1}$ and $\CIRCLE_{3}$, so it could be filled before, between, or
after them. To avoid generating the same expression three times, we should fix
the order in which holes are filled, so that there is a unique path to every
possible expression.

Because our techniques rely heavily on evaluation, we let evaluation guide the
hole order. After filling hole $\CIRCLE_{0}$, we live evaluate.

$\textsf{map}~{}(\lambda
x.~{}\CIRCLE_{1})~{}\CIRCLE_{2}\leadsto\textbf{case}~{}\CIRCLE_{2}~{}\textbf{of}~{}\dots$

At this point, evaluation cannot continue, because we do not know which
pattern $\CIRCLE_{2}$ will be matched on. We say that $\CIRCLE_{2}$ blocks the
evaluation. By filling $\CIRCLE_{2}$, the pattern match may resolve and
generate new example constraints for $\CIRCLE_{1}$. Conversely, filling
$\CIRCLE_{1}$ does not introduce any new constraints. Hence, we always fill
blocking holes first. Blocking holes are easily computed by live evaluating
the expression against the example constraints.

###  3.3 Generating Hole Fillings

Hole fillings depend on the local context and the type of a hole and may
consist of constructors, pattern matches, variables and function calls. To
avoid synthesizing multiple equivalent expressions, we will only generate
expressions in $\beta$-normal, $\eta$-long form. An expression is in
$\beta$-normal, $\eta$-long form exactly if no $\eta$-expansions or
$\beta$-reductions are possible. During synthesis, we guarantee
$\beta$-normal, $\eta$-long form by greedily $\eta$-expanding newly introduced
holes and always fully applying functions, variables and constructors.
Consider, for example, the function map. To use map as a refinement, it is
applied to two holes, the first of which is $\eta$-expanded:

$\textsf{map}~{}(\lambda x.~{}\CIRCLE_{0})~{}\CIRCLE_{1}$

Pattern matches can be handled in the same way by interpreting them as
eliminator functions, which are equivalent in expressiveness.

Furthermore, we add some syntactic restrictions to the generated expressions:
we only allow the recursive argument of recursion schemes such as foldr to be
variables. This is similar to the restriction on structural recursion in Myth
[10, 9] and Smyth [7]. Additionally, we disallow expressions that are not in
normal form, somewhat similar to equivalence reduction as described by Smith
and Albarghouthi [12]. Currently, our tool provides a handcrafted set of
expressions that are not in normal form, which are prohibited during
synthesis. Ideally, these sets of disallowed expressions would be taken from
an existing data set (such as HLint333https://github.com/ndmitchell/hlint), or
approximated using evaluation-based techniques such as QuickSpec [1].

###  3.4 Pruning Expressions

For an expression $e\in\mathcal{E}$ and a hole
$\CIRCLE_{i}\in\textit{holes}(e)$, we generate a set of possible hole fillings
based on the hole context $\Gamma_{i}$ and the hole type $\tau_{i}$. For each
of these hole fillings, we try to apply the expand rule. To do so, we must
check that the resulting expression $e^{\prime}$ does not conflict with the
example constraint $\varphi$. We use Smyth-style example propagation to
compute hole constraints for $e^{\prime}$. If example propagation fails, we do
not add $e^{\prime}$ to $\mathcal{E}$, essentially pruning the search space.

####  3.4.1 Diverging Constraints

Unfortunately, example propagation is not feasible for all possible
expressions. Consider, for instance, the function sum. If we try to propagate
a constraint through $\textsf{sum}~{}\CIRCLE$, we first use live evaluation,
resulting in the following partially evaluated result, with $\CIRCLE$ in a
scrutinized position:

$\begin{array}[]{l}\textbf{case}~{}\CIRCLE~{}\textbf{of}\\\
\quad\begin{array}[]{ll}[\>]&\rightarrow 0\\\
x:xs&\rightarrow\textsf{plus}~{}x~{}(\textsf{sum}~{}xs)\end{array}\end{array}$

Unlike Myth, Smyth allows examples to be propagated through pattern matches
whose scrutinee may contain holes, considering each branch separately under
the assumption that the scrutinee evaluates to the corresponding pattern. This
introduces disjunctions in the example constraint. Propagating
$\left\\{\begin{array}[]{c}\textsc{\small Zero}\end{array}\right\\}$ through
the previous expression results in a constraint that cannot be finitely
captured in our constraint language:

$(\CIRCLE\vDash\left\\{\begin{array}[]{c}[\>]\end{array}\right\\})\lor(\CIRCLE\vDash\left\\{\begin{array}[]{c}[\textsc{\small
Zero}]\end{array}\right\\})\lor(\CIRCLE\vDash\left\\{\begin{array}[]{c}[\textsc{\small
Zero},\textsc{\small Zero}]\end{array}\right\\})\lor\dots$

Without extending the constraint language it is impossible to compute such a
constraint. Instead, we try to recognize that example propagation diverges, by
setting a maximum to the amount of recursive calls allowed during example
propagation. If the maximum recursion depth is reached, we cancel example
propagation.

Since example propagation through $\textsf{sum}~{}\CIRCLE$ always diverges, we
could decide to disallow it as a hole filling. This is, however, too
restrictive, as example propagation becomes feasible again when the length of
the argument to sum is no longer unrestricted. Take, for example, the
following constraint, representing counting the number of Trues in a list, and
a possible series of hole fillings:

$\CIRCLE_{0}\vDash\left\\{\begin{array}[]{c|c}xs\\\\[0.0pt] [\textsc{\small
False}]&0\\\\[0.0pt] [\textsc{\small False},\textsc{\small True}]&1\\\\[0.0pt]
[\textsc{\small True},\textsc{\small
True}]&2\end{array}\right\\}\quad\quad\quad\quad\boxed{\begin{array}[]{l}\CIRCLE_{0}\mapsto\textsf{sum}~{}\CIRCLE_{1}\\\
\CIRCLE_{1}\mapsto\textsf{map}~{}(\lambda x.~{}\CIRCLE_{2})~{}\CIRCLE_{3}\\\
\CIRCLE_{3}\mapsto xs\\\ \end{array}}$

Trying to propagate through
$\boxed{\CIRCLE_{0}\mapsto\textsf{sum}~{}\CIRCLE_{1}}$ diverges, since
$\CIRCLE_{1}$ could be a list of any length. At this point, we could decide to
disregard this hole filling, but this would incorrectly prune away a valid
solution. Instead, we allow synthesis to continue guessing hole fillings,
until we get back on the right track: after guessing
$\boxed{\CIRCLE_{1}\mapsto\textsf{map}~{}(\lambda
x.~{}\CIRCLE_{2})~{}\CIRCLE_{3}}$ and $\boxed{\CIRCLE_{3}\mapsto xs}$, the
length of the argument to sum becomes restricted and example propagation no
longer diverges:

$\textsf{sum}~{}(\textsf{map}~{}(\lambda
x.~{}\CIRCLE_{2}\vDash\left\\{\begin{array}[]{c|c}x\\\ \textsc{\small
False}&0\\\ \textsc{\small True}&1\end{array}\right\\})~{}xs)$

At this point, synthesis easily finishes by pattern matching on $x$. Note
that, unlike $\lambda^{2}$, Myth and Smyth, Scrybe is able to interleave
refinements and guesses.

####  3.4.2 Exponential Constraints

Even if example propagation does not diverge, it still might take too long to
compute or generate a disproportionally large constraint, slowing down the
synthesis procedure. Lubin et al. [7] compute the falsifiability of an example
constraint by first transforming it to disjunctive normal form (DNF), which
may lead to exponential growth of the constraint size. For example, consider
the function or, defined as follows:

$\begin{array}[]{l}\textsf{or}=\lambda
a~{}b.~{}\textbf{case}~{}a~{}\textbf{of}\\\
\quad\begin{array}[]{ll}\textsc{\small False}&\rightarrow b\\\ \textsc{\small
True}&\rightarrow\textsc{\small True}\end{array}\end{array}$

Propagating the example constraint $\left\\{\begin{array}[]{c}\textsc{\small
True}\end{array}\right\\}$ through the expression
$\textsf{or}~{}\CIRCLE_{0}~{}\CIRCLE_{1}$ puts the hole $\CIRCLE_{0}$ in a
scrutinized position, resulting in the following constraint:

$(\CIRCLE_{0}\vDash\left\\{\begin{array}[]{c}\textsc{\small
False}\end{array}\right\\}\land\CIRCLE_{1}\vDash\left\\{\begin{array}[]{c}\textsc{\small
True}\end{array}\right\\})\lor\CIRCLE_{0}\vDash\left\\{\begin{array}[]{c}\textsc{\small
True}\end{array}\right\\}$

This constraint has size three (the number of hole occurrences). We can extend
this example by mapping it over a list of length $n$ as follows:

$\textsf{map}~{}(\lambda
x.~{}\textsf{or}~{}\CIRCLE_{0}~{}\CIRCLE_{1})~{}[0,1,2,\dots]\vDash\left\\{\begin{array}[]{c}[\textsc{\small
True},\textsc{\small True},\textsc{\small True},\dots]\end{array}\right\\}$

Propagation generates a conjunction of $n$ constraints that are all exactly
the same apart from their local context, which differs in the value of $x$.
This constraint, unsurprisingly, has size $3n$. Computing the disjunctive
normal form of this constraint, however, results in a constraint of size of
$2^{n}\times\frac{3}{2}n$, which is exponential.

In some cases, generating such a large constraint may cause example
propagation to reach the maximum recursion depth. In other cases, example
propagation succeeds, but returns such a large constraint that subsequent
refinements will take too long to compute. In both cases, we treat it the same
as diverging example propagation.

##  4 Evaluation

To evaluate Scrybe, we combine the benchmarks of Myth [10] and $\lambda^{2}$
[3]. This evaluation is not intended to compare our technique directly with
previous techniques in terms of efficiency, but rather to show the wide range
of synthesis problems that Scrybe can handle. Additionally, we get some
insight in the effectiveness of example propagation as a pruning technique.

For ease of readability, the benchmark suite is split up into a set of
functions operating on lists (Table 1, Appendix 0.A) and a set of functions
operating on binary trees (Table 2, Appendix 0.A). We have excluded functions
operating on just booleans or natural numbers, as these are all trivial and
synthesize in a few milliseconds. For consistency, and to avoid naming
conflicts, the names of some of the benchmarks are changed to reflect the
corresponding functions in the Haskell prelude. To avoid confusion, each
benchmark function comes with a short description.

Each row describes a single synthesis problem in terms of a function that
needs to be synthesized. The first two columns give the name and a short
description of this function. The third and fourth columns show, in
milliseconds, the average time our synthesizer takes to correctly synthesize
the function with example propagation (EP) and without example propagation
(NoEP), respectively. Some functions may fail to synthesize ($\bot$) within 5
seconds and some cannot straightforwardly be represented in our language (-).
The last three columns show, for Myth, Smyth, and $\lambda^{2}$, respectively,
whether the function synthesizes (), fails to synthesize (), or is not
included in their benchmark (-).

The benchmarks list_head, list_tail, list_init and list_last are all partial
functions (marked $\dagger$). We do not support partial functions, and
therefore these functions are replaced by their total equivalents, by wrapping
their return type in Maybe. For example, list_last is defined as follows,
where the outlined hole filling is the result returned by Scrybe (input-output
constraints are omitted for brevity):

$\begin{array}[]{l}\\{-\\#~{}\text{USE}~{}\textsf{foldr}~{}\\#-\\}\\\\[2.0pt]
\textsf{list\\_last}::\textit{List}~{}a\rightarrow\textit{Maybe}~{}a\\\
\textsf{list\\_last}~{}\textit{xs}=\CIRCLE\\\\[3.0pt]
\boxed{\CIRCLE\mapsto\textsf{foldr}~{}(\lambda
x~{}r.~{}\textbf{case}~{}r~{}\textbf{of}\;\begin{array}[]{ll}\textsc{\small
Nothing}&\rightarrow\textsc{\small Just}~{}x\\\\[-1.0pt] \textsc{\small
Just}~{}y&\rightarrow r\end{array})~{}\textsc{\small
Nothing}~{}\textit{xs}}\end{array}$

The benchmarks list_drop, list_index, list_take and tree_level (marked
$\ddagger$) all recurse over two datatypes at the same time. As such, they
cannot be implemented using foldr as it is used in Section 3.3. Instead, we
provide a specialized version of foldr that takes an extra argument:

$\begin{array}[]{l}\\{-\\#~{}\text{USE}~{}\textsf{foldr}::(a\rightarrow(c\rightarrow
b)\rightarrow(c\rightarrow b))\rightarrow(c\rightarrow
b)\rightarrow\textit{List}~{}a\rightarrow c\rightarrow b~{}\\#-\\}\\\\[2.0pt]
\textsf{list\\_take}::\textit{Nat}\rightarrow\textit{List}~{}a\rightarrow\textit{List}~{}a\\\
\textsf{list\\_take}~{}n~{}\textit{xs}=\CIRCLE\\\\[3.0pt]
\boxed{\CIRCLE\mapsto\textsf{foldr}~{}(\lambda
x~{}r~{}m.~{}\textbf{case}~{}m~{}\textbf{of}\;\begin{array}[]{ll}\textsc{\small
Zero}&\rightarrow[\>]\\\\[-1.0pt] \textsc{\small
Succ}~{}o&\rightarrow(x:r~{}o)\end{array})~{}(\lambda\\_.~{}[\>])~{}\textit{xs}~{}n}\end{array}$

A few functions (marked *) could not straightforwardly be translated to our
approach:

  * •

Function list_delete_mins requires a total function in scope that returns the
minimum number in a list. This is not possible for natural numbers, as there
is no obvious number to return for empty lists.

  * •

Function list_swap uses nested pattern matching on the input list, which is
not possible to mimic using a fold.

  * •

Function list_reverse combines a set of benchmarks from Myth that synthesize
reverse using different techniques, which are not easily translated to our
language.

###  4.1 Results

Scrybe is able to synthesize most of the combined benchmarks of Myth and
$\lambda^{2}$, with a median runtime of 15.95 milliseconds. Furthermore,
synthesis with example propagation is on average 5.22 times as fast as without
example propagation, disregarding the benchmarks where synthesis without
example propagation failed. $\lambda^{2}$ noticed a similar improvement (6
times as fast) for example propagation based on automated deduction, which
indicates that example propagation using live-bidirectional evaluation is
similar in strength, while being more general.

Some functions benefit especially from example propagation, in particular
problems that are composed of multiple synthesis problems. Take, for example,
tree_snoc, which effectively synthesizes mapTree and snoc from foldTree and
foldr respectively. Without example propagation, it is not tractable to
automatically decompose this synthesis problem into these two parts.

$\begin{array}[]{l}\\{-\\#~{}\text{USE}~{}\textsf{foldTree},\textsf{foldr}~{}\\#-\\}\\\\[2.0pt]
\textsf{tree\\_snoc}::a\rightarrow\textit{Tree}~{}(\textit{List}~{}a)\rightarrow\textit{Tree}~{}(\textit{List}~{}a)\\\
\textsf{tree\\_snoc}~{}x~{}t=\CIRCLE\\\\[3.0pt]
\boxed{\CIRCLE\mapsto\textsf{foldTree}~{}(\lambda
l~{}\textit{xs}~{}r.~{}\textsc{\small Node}~{}l~{}(\textsf{foldr}~{}(\lambda
x~{}q.~{}x:q)~{}[x]~{}\textit{xs})~{}r)~{}\textsc{\small
Leaf}~{}t}\end{array}$

On the other hand, for some functions, such as tree_search, synthesis is
noticeably faster without example propagation, showing that the overhead of
example propagation sometimes outweighs the benefits. This indicates that it
might be helpful to use some heuristics to decide when example propagation is
beneficial. A few functions that fail to synthesize, such as list_compress, do
synthesize when a simple sketch is provided:

$\begin{array}[]{ll}\begin{array}[]{l}\\{-\\#~{}\text{USE}~{}\textsf{foldr},(\equiv)~{}\\#-\\}\\\\[2.0pt]
\textsf{compress}::\textit{List}~{}\textit{Nat}\rightarrow\textit{List}~{}\textit{Nat}\\\
\textsf{compress}~{}xs=\textsf{foldr}~{}(\lambda
x~{}r.~{}\CIRCLE_{0})~{}\CIRCLE_{1}\end{array}&\boxed{\begin{array}[]{l}\CIRCLE_{0}\mapsto[\>]\\\
\CIRCLE_{1}\mapsto x:\textbf{case}~{}r~{}\textbf{of}\\\
\quad\begin{array}[]{ll}[\>]&\rightarrow r\\\\[-1.0pt]
y:ys&\rightarrow\textbf{if}~{}x\equiv
y~{}\textbf{then}~{}ys~{}\textbf{else}~{}r\end{array}\end{array}}\end{array}$

Since our evaluation was not aimed at sketching, we still consider
list_compress to fail ($\bot$).

##  5 Conclusion

We presented an approach to program synthesis using example propagation that
specializes in compositionality, by allowing arbitrary functions to be used as
refinement steps. One of the key ideas is holding on to constraint information
as long as possible, rather than resorting to brute-force, enumerative search.
Our experiments show that we are able to synthesize a wide range of synthesis
problems from different synthesis domains.

There are many avenues for future research. One direction we wish to explore
is to replace the currently ad hoc constraint solver with a more general
purpose SMT solver. Our hope is that this paves the way for the addition of
primitive data types such as integers and floating point numbers.

#### Acknowledgements

We would like to thank Alex Gerdes, Koen Claessen, and the anonymous reviewers
of HATRA 2022 for their supportive comments and constructive feedback.

## References

  * [1] Claessen, K., Smallbone, N., Hughes, J.: Quickspec: Guessing formal specifications using testing. In: Fraser, G., Gargantini, A. (eds.) Tests and Proofs. pp. 6–21. Springer Berlin Heidelberg (2010)
  * [2] Danvy, O., Spivey, M.: On Barron and Strachey’s cartesian product function. In: Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming. p. 41–46. ICFP ’07, Association for Computing Machinery, New York, NY, USA (2007), https://doi.org/10.1145/1291151.1291161
  * [3] Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. ACM SIGPLAN Notices 50(6), 229–239 (Aug 2015), https://dl.acm.org/doi/10.1145/2813885.2737977
  * [4] Guo, Z., James, M., Justo, D., Zhou, J., Wang, Z., Jhala, R., Polikarpova, N.: Program synthesis by type-guided abstraction refinement. Proc. ACM Program. Lang. 4(POPL) (Dec 2019), https://doi.org/10.1145/3371080
  * [5] Katayama, S.: Efficient exhaustive generation of functional programs using monte-carlo search with iterative deepening. In: Ho, T.B., Zhou, Z.H. (eds.) PRICAI 2008: Trends in Artificial Intelligence. pp. 199–210. Springer Berlin Heidelberg (2008)
  * [6] Koppel, J., Guo, Z., de Vries, E., Solar-Lezama, A., Polikarpova, N.: Searching entangled program spaces. Proc. ACM Program. Lang. 6(ICFP) (aug 2022), https://doi.org/10.1145/3547622
  * [7] Lubin, J., Collins, N., Omar, C., Chugh, R.: Program sketching with live bidirectional evaluation. Proc. ACM Program. Lang. 4(ICFP) (Aug 2020), https://doi.org/10.1145/3408991
  * [8] Omar, C., Voysey, I., Chugh, R., Hammer, M.A.: Live functional programming with typed holes. Proc. ACM Program. Lang. 3(POPL) (Jan 2019), https://doi.org/10.1145/3290327
  * [9] Osera, P.M.: Programming assistance for type-directed programming (extended abstract). In: Proceedings of the 1st International Workshop on Type-Driven Development - TyDe 2016. pp. 56–57. ACM Press, Nara, Japan (2016), http://dl.acm.org/citation.cfm?doid=2976022.2976027
  * [10] Osera, P.M., Zdancewic, S.: Type-and-example-directed program synthesis. ACM SIGPLAN Notices 50(6), 619–630 (Aug 2015), https://dl.acm.org/doi/10.1145/2813885.2738007
  * [11] Peleg, H., Gabay, R., Itzhaky, S., Yahav, E.: Programming with a read-eval-synth loop. Proc. ACM Program. Lang. 4(OOPSLA) (nov 2020), https://doi.org/10.1145/3428227
  * [12] Smith, C., Albarghouthi, A.: Program synthesis with equivalence reduction. In: Enea, C., Piskac, R. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 24–47. Springer International Publishing, Cham (2019)
  * [13] Solar-Lezama, A.: Program Synthesis by Sketching. Ph.D. thesis, Berkeley (2008)
  * [14] Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) Programming Languages and Systems. pp. 4–13. Springer Berlin Heidelberg (2009)

##  Appendix 0.A Appendix

Function | Description | EP (ms) | NoEP (ms) | Myth | Smyth | $\lambda^{2}$
---|---|---|---|---|---|---
list_add | Increment each value in a list by $n$ | 4.96 | 11.60 | - | - |
list_append | Append two lists | 4.90 | 18.30 |  |  |
list_cartesian | The cartesian product | 449.00 | $\bot$ | - | - |
list_compress | Remove consecutive duplicates from a list | $\bot$ | $\bot$ |  |  | -
list_flatten | Flatten a list of lists | 3.53 | 3.00 |  |  |
list_copy_first | Replace each element in a list with the first | 40.10 | 82.90 | - | - |
list_copy_last | Replace each element in a list with the last | 38.20 | 106.00 | - | - |
list_delete_max | Remove the largest numbers from a list | 38.60 | 127.00 | - | - |
list_delete_mins* | Remove the smallest numbers from a list of lists | - | - | - | - |
list_drop‡ | All but the first $n$ elements of a list | 192.00 | 473.00 |  |  | -
list_even_parity | Whether a list has an odd number of $True$s | 15.30 | 99.90 |  |  | -
list_evens | Remove the odd numbers from a list | 2.00 | 4.60 | - | - |
list_filter | The elements in a list that satisfy $p$ | 8.88 | 46.30 |  |  | -
list_fold | A catamorphism over a list | 8.40 | 5.55 |  |  | -
list_head† | The first element of a list | 0.65 | 0.70 |  |  | -
list_inc | Increment each value in a list by one | 3.30 | 221.00 |  |  | -
list_incs | Increment each value in a list of lists by one | 9.16 | 23.40 | - | - |
list_index‡ | Index a list starting at 0 | 51.80 | 167.00 |  |  | -
list_init† | All but the last element of a list | 869.00 | $\bot$ | - | - |
list_last† | The last element of a list | 167.00 | 123.00 |  |  |
list_length | The number of elements in a list | 0.62 | 2.86 |  |  |
list_map | Map a function over a list | 1.38 | 2.03 |  |  | -
list_maximum | The largest number in a list | 26.20 | 303.00 | - | - |
list_member | Whether a number occurs in a list | 873.00 | 4090.00 | - | - |
list_nub | Remove duplicates from a list | $\bot$ | $\bot$ | - | - |
list_swap* | Swap the elements in a list pairwise | - | - |  |  | -
list_reverse* | Reverse a list | 1.67 | 2.57 |  |  | -
list_shiftl | Shift all elements in a list to the left | 69.00 | 366.00 | - | - |
list_shiftr | Shift all elements in a list to the right | 89.20 | 708.00 | - | - |
list_snoc | Add an element to the end of a list | 69.00 | 366.00 |  |  |
list_set_insert | Insert an element in a set | $\bot$ | $\bot$ |  |  | -
list_dupli | Duplicate each element in a list | 2.44 | 3.33 |  |  |
list_sum | The sum of all numbers in a list | 3.59 | 19.20 |  |  |
list_sums | The sum of each nested list in a list of lists | 607.00 | $\bot$ | - | - |
list_tail† | All but the first element of a list | 0.85 | 1.33 |  |  | -
list_take‡ | The first $n$ elements of a list | 182.00 | 3690.00 |  |  | -
list_to_set | Sort a list, removing duplicates | 458.00 | $\bot$ |  |  | -

Table 1: Benchmark for functions acting on lists. Each row describes a single benchmark task and the time it takes for each function to synthesize with example propagation (EP) and without (NoEP) respectively. Some tasks cannot be synthesized within 5 seconds ($\bot$) and others are omitted, since they cannot straightforwardly be translated to our language (-). Function | Description | EP (ms) | NoEP (ms) | Myth | Smyth | $\lambda^{2}$
---|---|---|---|---|---|---
tree_cons | Add an element to the front of each node in a tree of lists | 6.92 | $\bot$ | - | - |
tree_flatten | Flatten a tree of lists into a list | 20.80 | 25.20 | - | - |
tree_height | The height of a tree | 7.71 | 27.00 | - | - |
tree_inc | Increment each element in a tree by one | 6.14 | $\bot$ | - | - |
tree_inorder | Inorder traversal of a tree | 11.50 | 9.17 |  |  |
tree_insert | Insert an element in a binary tree | $\bot$ | $\bot$ |  |  | -
tree_leaves | The number of leaves in a tree | 24.50 | 40.00 |  |  |
tree_maximum | The largest number in a tree | 31.90 | 157.00 | - | - |
tree_map | Map a function over a tree | 2.61 | 6.84 |  |  | -
tree_member | Whether a number occurs in a tree | 597.00 | $\bot$ | - | - |
tree_level‡ | The number of nodes at depth $n$ | $\bot$ | $\bot$ |  |  | -
tree_postorder | Postorder traversal of a tree | 19.60 | 24.40 |  |  | -
tree_preorder | Preorder traversal of a tree | 7.49 | 15.40 |  |  | -
tree_search | Whether a number occurs in a tree of lists | 964.00 | 307.00 | - | - |
tree_select | All nodes in a tree that satisfy $p$ | 773.00 | 3170.00 | - | - |
tree_size | The number of nodes in a tree | 16.60 | 39.50 |  |  |
tree_snoc | Add an element to the end of each node in a tree of lists | 81.60 | $\bot$ | - | - |
tree_sum | The sum of all nodes in a tree | 16.70 | 104.00 | - | - |
tree_sum_lists | The sum of each list in a tree of lists | 7.13 | $\bot$ | - | - |
tree_sum_trees | The sum of each tree in a list of trees | 28.40 | $\bot$ | - | - |

Table 2: Benchmark for functions acting on binary trees. Each row describes a
single benchmark task and the time it takes for each function to synthesize
with example propagation (EP) and without (NoEP) respectively. Some tasks
cannot be synthesized within 5 seconds ($\bot$) and others are omitted, since
they cannot straightforwardly be translated to our language (-).