1

Synthesis of Data Completion Scripts using Finite Tree Automata

arXiv:1707.01469v1 [] 5 Jul 2017

XINYU WANG, UT Austin
ISIL DILLIG, UT Austin
RISHABH SINGH, Microsoft Research
In application domains that store data in a tabular format, a common task is to fill the values of some cells using values stored
in other cells. For instance, such data completion tasks arise in the context of missing value imputation in data science and
derived data computation in spreadsheets and relational databases. Unfortunately, end-users and data scientists typically
struggle with many data completion tasks that require non-trivial programming expertise. This paper presents a synthesis
technique for automating data completion tasks using programming-by-example (PBE) and a very lightweight sketching
approach. Given a formula sketch (e.g., AVG(?1 , ?2 )) and a few input-output examples for each hole, our technique synthesizes
a program to automate the desired data completion task. Towards this goal, we propose a domain-specific language (DSL) that
combines spatial and relational reasoning over tabular data and a novel synthesis algorithm that can generate DSL programs
that are consistent with the input-output examples. The key technical novelty of our approach is a new version space learning
algorithm that is based on finite tree automata (FTA). The use of FTAs in the learning algorithm leads to a more compact
representation that allows more sharing between programs that are consistent with the examples. We have implemented the
proposed approach in a tool called DACE and evaluate it on 84 benchmarks taken from online help forums. We also illustrate
the advantages of our approach by comparing our technique against two existing synthesizers, namely PROSE and SKETCH.
ACM Reference format:
Xinyu Wang, Isil Dillig, and Rishabh Singh. 2017. Synthesis of Data Completion Scripts using Finite Tree Automata. PACM
Progr. Lang. 1, 1, Article 1 (January 2017), 24 pages.
DOI: 10.1145/nnnnnnn.nnnnnnn

1

INTRODUCTION

Many application domains store data in a tabular form arranged using rows and columns. For example, Excel
spreadsheets, R dataframes, and relational databases all view the underlying data as a 2-dimensional table
consisting of cells. In this context, a common scenario is to fill the values of some cells using values stored in
other cells. For instance, consider the following common data completion tasks:
• Data imputation: In statistics, imputation means replacing missing data with substituted values. Since
missing values can hinder data analytics tasks, users often need to fill missing values using other related
entries in the table. For instance, data imputation arises frequently in statistical computing frameworks,
such as R and pandas.
• Spreadsheet computation: In many applications involving spreadsheets, users need to calculate the
value of a cell based on values from other cells. For instance, a common task is to introduce new columns,
where each value in the new column is derived from values in existing columns.
• Virtual columns in databases: In relational databases, users sometimes create views that store the
result of some database query. In this context, a common task is to add virtual columns whose values are
computed using existing entries in the view.
As illustrated by these examples, users often need to complete missing values in tabular data. While some of
these data completion tasks are fairly straightforward, many others require non-trivial programming knowledge
that is beyond the expertise of end-users and data scientists.
2017. 2475-1421/2017/1-ART1 $15.00
DOI: 10.1145/nnnnnnn.nnnnnnn
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

1:2

• Xinyu Wang, Isil Dillig, and Rishabh Singh

5
-1
5
4

Fig. 1. A data completion task taken from StackOverflow.

To illustrate a typical data completion task, consider the tabular data shown in Fig. 1. Here, the table stores
measurements for different people during a certain time period, where each row represents a person and each
column corresponds to a day. As explained in a StackOverflow post 1 , a data scientist analyzing this data wants
to compute the difference of the measurements between the first and last days for each person and record this
information in the Delta column. Since the table contains a large number of rows (of which only a small subset is
shown in Fig. 1), manually computing this data is prohibitively cumbersome. Furthermore, since each person’s
start and end date is different, automating this data completion requires non-trivial programming logic.
In this paper, we present a novel program synthesis technique for automating data completion tasks in tabular
data sources, such as dataframes, spreadsheets, and relational databases. Our synthesis methodology is based on
two key insights that we gained by analyzing dozens of posts on online forums: First, it is often easy for end-users
to specify which operators should be used in the data completion task and provide a specific instantiation of
the operands for a few example cells. However, it is typically very difficult for end-users to express the general
operand extraction logic. For instance, for the example from Fig. 1, the user knows that the missing value can be
computed as C 1 − C 2 , but he is not sure how to implement the logic for extracting C 1 , C 2 in the general case.
Based on this observation, our synthesis methodology for data completion combines program sketching and
programming-by-example (PBE). Specifically, given a formula sketch (e.g., SUM(?1 ,AVG(?2 ,?3 ))) as well as a few
input-output examples for each hole, our technique automatically synthesizes a program that can be used to fill
all missing values in the table. For instance, in our running example, the user provides the sketch MINUS(?1 ,?2 )
as well as the following input-output examples for the two holes:
?1
(A, Delta) 7→ (A, Day 6)
(B, Delta) 7→ (B, Day 4)

?2
(A, Delta) 7→ (A, Day 3)
(B, Delta) 7→ (B, Day 1)

Given these examples, our technique automatically synthesizes a program that can be used to fill all values in the
Delta column in Fig. 1.
One of the key pillars underlying our synthesis algorithm is the design of a new domain-specific language
(DSL) that is expressive enough to capture most data completion tasks we have encountered, yet lightweight
enough to facilitate automation. The programs in our DSL take as input a table and a cell with missing value,
and return a list of cells that are used for computing the missing value. Our main insight in designing this DSL
is to use abstractions that combine spatial reasoning in the tabular structure with relational reasoning. Spatial
reasoning allows the DSL programs to follow structured paths in the 2-dimensional table whereas relational
reasoning allows them to constrain those paths with predicates over cell values.
As shown schematically in Fig. 2, the high-level structure of our synthesis algorithm is similar to prior
techniques that combine partitioning with unification (Alur et al. 2015; Gulwani 2011; Yaghmazadeh et al. 2016) .
Specifically, partitioning is used to classify the input-output examples into a small number of groups, each of
which can be represented using a conditional-free program in the DSL. In contrast, the goal of unification is
1 http://stackoverflow.com/questions/30952426/substract-last-cell-in-row-from-first-cell-with-number

PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

Synthesis of Data Completion Scripts using Finite Tree Automata

SUM(?, ?)

•

1:3

Uniﬁcation

Partitioning

Sketch
Code
Enumerative
Search

Finite Tree
Automata

Examples

Fig. 2. High-level overview of our synthesis approach.

to find a conditional-free program that is consistent with each example in the group. The key novelty of our
synthesis algorithm is a new unification algorithm based on finite tree automata (FTA).
Our unification procedure can be viewed as a new version space learning algorithm (Mitchell 1982) that
succinctly represents a large number of programs. Specifically, a version space represents all viable hypotheses
that are consistent with a given set of examples, and prior work on programming-by-example have used so-called
version space algebras (VSA) to combine simpler version spaces into more complex ones (Gulwani 2011; Lau et al.
2003; Polozov and Gulwani 2015). Our use of FTAs for version space learning offers several advantages compared
to prior VSA-based techniques such as PROSE: First, FTAs represent version spaces more succinctly, without
explicitly constructing individual sub-spaces representing sub-expressions. Hence, our approach avoids the need
for finite unrolling of recursive expressions in the DSL. Second, our finite-tree automata are constructed in a
forward manner using the DSL semantics. In constrast to VSA-based approaches such as PROSE that construct
VSAs in a backward fashion starting from the outputs, our approach therefore obviates the need to manually
define complex inverse semantics for each DSL construct. As we demonstrate experimentally, our version space
learning algorithm using FTAs significantly outperforms the VSA-based learning algorithm used in PROSE.
We have implemented our synthesis algorithm in a tool called DACE 2 and evaluated it on 84 real-world data
completion tasks collected from online help forums. Our evaluation shows that DACE can successfully synthesize
over 92% of the data completion tasks in an average of 0.7 seconds. We also empirically compare our approach
against PROSE and SKETCH and show that our new synthesis technique outperforms these baseline algorithms
by orders of magnitude in the data completion domain.
To summarize, this paper makes the following key contributions:
• We propose a new program synthesis methodology that combines program sketching and programmingby-example techniques to automate a large class of data completion tasks involving tabular data.
• We describe a DSL that can concisely express a large class of data completion tasks and that is amenable
to an efficient synthesis algorithm.
• We propose a new unification algorithm that uses finite tree automata to construct version spaces that
succinctly represent DSL programs that are consistent with a set of input-output examples.
• We evaluate our approach on real-world data completion tasks involving dataframes, spreadsheets, and
relational databases. Our experiments show that the proposed learning algorithm is effective in practice.

2

MOTIVATING EXAMPLES

In this section, we present some representative data completion tasks collected from online help forums. Our
main goal here is to demonstrate the diversity of data completion tasks and motivate various design choices for
the DSL of cell extraction programs.

2 DACE

stands for DAta Completion Engine.
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

1:4

1:
2:
3:
4:
5:
6:
7:
8:

• Xinyu Wang, Isil Dillig, and Rishabh Singh
1
id
1
1
2
2
1
2
1
··

2
x
10
? 10
100
200
? 10
? 200
300
··
(a)

1:
2:
3:
4:
5:
6:
7:
(b)

(c)

1
2016-11-01
2016-11-02
2016-11-03
2016-11-04
2016-11-05
2016-11-06
2016-11-07
··

2
A
B
A
C
B
B
C
··

3
?
12
?
18
10
?
?
··

12
12
10
10

4
? 200
? 200
200
400
? 400
800
1000
··

(d)

Fig. 3. (a) Replace missing entry by previous non-missing value with same id. (b) Fill cells in column D by copying values
in column C. (c) Calculate total count for each group. (d) Replace missing value by previous non-missing value (if exists),
otherwise use next non-missing one.

Example 2.1. A numerical ecologist needs to perform data imputation in R using the last observation carried
forward (LOCF) method 3 . Specifically, he would like to replace each missing entry with the previous nonmissing entry incremented by 1. For instance, if the original row contains [2, 2, ?, ?, 8, ?], the new row should be
[2, 2, 3, 3, 8, 9].
Here, the desired imputation task can be expressed using the simple formula sketch SUM(?1 , 1). The synthesis
task is to find an expression that retrieves the previous non-missing value for each missing entry.
Example 2.2. An astronomer needs to perform data imputation using Python’s pandas data analysis library 4 .
Specifically, the astronomer wants to replace each missing value with the previous non-missing value with the
same id. The desired data imputation task is illustrated in Fig. 3(a).
As this example illustrates, some data completion tasks require finding a cell that satisfies a relational predicate.
In this case, the desired cell with non-missing value must have the same id as the id of the cell with missing value.
Example 2.3. A businessman using Excel wants to add a new column to his spreadsheet 5 . As shown in Fig. 3
(b), the entries in the new column D are obtained from column C. Specifically, the data completion logic is as
follows: First, find the previous row that has value 1 in column B. Then, go down from that row and find the first
non-zero value in column C and use that value to populate the cell in column D. Fig. 3 (b) shows the desired
values for column D.
As this example illustrates, the cell extraction logic in some tasks can be quite involved. In this example, we
first need to find an intermediate cell satisfying a certain property (namely, it must be upwards from the missing
cell and have value 1 in column B). Then, once we find this intermediate cell, we need to find the target cell
satisfying a different property (namely, it must be downwards from the intermediate cell and store a non-zero
value in column C).
This example illustrates two important points: First, the data extraction logic can combine both geometric
(upward and downward search) and relational properties. Second, the data extraction logic can require “making
turns” — in this example, we first go up to an intermediate cell and then change direction by going down to find
the target cell using a different logic.
3 http://stackoverflow.com/questions/38100208/fill-missing-value-based-on-previous-values

4 http://stackoverflow.com/questions/16345583/fill-in-missing-pandas-data-with-previous-non-missing-value-grouped-by-key
5 http://stackoverflow.com/questions/29606616/find-values-between-range-fill-in-next-cells

PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

Synthesis of Data Completion Scripts using Finite Tree Automata
Task
Example 2.1
Example 2.2
Example 2.3
Example 2.4
Example 2.5

Sketch
SUM(?1 , 1)
?1
?1
COUNT(?1 )
?1

•

1:5

Input-output examples

?
,→
{(1,
3)
→
7
[(1, 2)], (1, 4) 7→ [(1, 2)], (1, 6) 7→ [(1, 5)]}
 1
?
,→
{(3,
2)
→
7
[(2, 2)], (6, 2) 7→ [(2, 2)], (7, 2) 7→ [(5, 2)]}
1

?
,→
{(1,
D)
→
7
[(1,
C)], (3, D) 7→ [(4, C)], (8, D) 7→ [(6, C)]}
1

?1 ,→ {(5, B) 7→ [(3, B), (4, B)], (10, B) 7→ [(7, B), (8, B), (9, B)]}
?1 ,→ {(3, 3) 7→ [(2, 3)], (7, 3) 7→ [(5, 3)], (1, 4) 7→ [(3, 4)]}

Fig. 4. Specifications for examples from Section 2.

Example 2.4. A statistician working on spreadsheet data needs to complete the “Group Total” rows from Fig. 3
(c) using the count of entries in that group 6 . For instance, the GroupA Total entry should be filled with 2.
This example illustrates the need for allowing holes of type list in the sketches. Since each missing value
is obtained by counting a variable number of entries, the user instead provides a sketch COUNT(?1 ), where ?1
represents a list of cells. Furthermore, this example also illustrates the need for a language construct that can
extract a range of values satisfying a certain property. For instance, in this example, we need to extract all cells
between the cell c to be completed and the first empty entry that is upwards from c.
Example 2.5. An R user wants to perform imputation on the dataframe shown in Fig. 3 (d) using the LOCF
method. Specifically, she wants to impute the missing value by substituting it with the first previous non-missing
value in the same column. However, if no such entry exists, she wants to fill the missing entry by using the first
following non-missing value in the same column instead.
This example illustrates the need for allowing a conditional construct in our DSL: Here, we first try some
extraction logic, and, if it fails, we then resort to a back-up strategy. Many of the data completion tasks that
we have encountered follow this pattern – i.e., they try different extraction logics depending on whether the
previous logic succeeds. Based on this observation, our DSL introduces a restricted form of switch statement,
where the conditional implicitly checks if the current branch fails.

3

SPECIFICATIONS

A specification in our synthesis methodology is a pair (S, E), where S is a formula sketch and E is a set of
input-output examples. Specifically, formula sketches are defined by the following grammar:
Sketch S
Term t

:= t | F (S1 , ··, Sn ), F ∈ Λ
:= const | ?id

Here, Λ denotes a family of pre-defined functions, such as AVG, SUM, MAX, etc. Holes in the sketch represent
unknown cell extraction programs to be synthesized. Observe that formula sketches can contain multiple functions.
For instance, SUM(MAX(?1 , ?2 ), 1) is a valid sketch and indicates that a missing value in the table should be filled
by adding one to the maximum of two unknown cells.
In many cases, the data completion task involves copying values from an existing cell. In this case, the user
can express her intent using the identity sketch ID(?1 ). Since this sketch is quite common, we abbreviate it using
the notation ?1 .
In addition to the sketch, users of DACE are also expected to provide one or more input-output examples E for
each hole. Specifically, examples E map each hole ?id in the sketch to a set of pairs of the form i 7→ [o 1 , ··, on ],
where i is an input cell and [o 1 , ··, on ] is the desired list of output cells. Hence, examples in DACE have the
6 http://stackoverflow.com/questions/13998218/count-values-in-groups/13999520

PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

1:6

• Xinyu Wang, Isil Dillig, and Rishabh Singh
Extractor π
Simple prog. ρ
Cell prog. τ
Predicate ϕ
Cell mapper χ
Direction dir

:=
:=
:=
:=
:=
:=

λT.λx .ρ | λT.λx .Seq(ρ, π )
List(τ1 , ··, τn ) | Filter(τ1 , τ2 , τ3 , λy.λz.ϕ)
x | GetCell(τ , dir, k, λy.λz.ϕ)
True | Val(χ (z)) = s | Val(χ (z)) , s | Val(χ (y)) = Val(χ (z)) | ϕ 1 ∧ ϕ 2
λc.c | λc.(k, col(c)) | λc.(row(c), k)
u|d|l|r

Fig. 5. Syntax of the DSL. Here, T is a table, x is a cell, and y and z are bound to cells in table T. Also, k denotes an integer
constant, and s denotes a string constant. Val(·) returns the value in a given cell.

following shape:
n
o
Example E := ?id ,→ {i 7→ [o 1 , ··, on ]}
Each cell in the table is represented as a pair (x, y), where x and y denote the row and column of the cell
respectively. Fig. 4 provides the complete specifications for the examples described in Section 2.
Given a specification (S, E), the key learning task is to synthesize a program Pid for each hole ?id such that
Pid satisfies all examples E[?id ]. For a list of programs P = [P 1 , ··, Pn ], we write S[P] to denote the resulting
program that is obtained by filling hole ?id in S with program Pid . Once DACE learns a cell extraction program
Pid for each hole, it computes missing values in the table T using S[P](T, c) where c denotes a cell to be completed
in table T. In the rest of the paper, we assume that missing values in the table are identified using the special
symbol ?. For instance, the analog of ? is the symbol NA in R and blank cell in Excel.

4

DOMAIN-SPECIFIC LANGUAGE

In this section, we present our domain-specific language (DSL) for cell extraction programs. The syntax of the
DSL is shown in Fig. 5, and its denotational semantics is presented in Fig. 6. We now review the key constructs in
the DSL together with their semantics.
A cell extraction program π takes as input a table T and a cell x, and returns a list of cells [c 1 , ··, c n ] or the
special value ⊥. Here, ⊥ can be thought of as an “exception” and indicates that π fails to extract any cells on its
input cell x. A cell extraction program π is either a simple program ρ without branches or a conditional of the
form Seq(ρ, π ). As shown in Fig. 6, the semantics of Seq(ρ, π ) is that the second argument π is only evaluated if
ρ fails (i.e., returns ⊥).
Let us now consider the syntax and semantics of simple programs ρ. A simple program is either a list of
individual cell extraction programs (List(τ1 , ··, τn )), or a filter construct of the form Filter(τ1 , τ2 , τ3 , λy.λz.ϕ). Here,
τ denotes a so-called cell program for extracting a single cell. The semantics of the Filter construct is that it returns
all cells between τ2 and τ3 that satisfy the predicate ϕ. Note that the predicate ϕ takes two arguments y and z,
where y is bound to the result of τ1 and z is bound to each of the cells between τ2 and τ3 .
The key building block of cell extraction programs is the GetCell construct. In the simplest case, a GetCell
construct has the form GetCell(x, dir, k, λy.λz.ϕ) where x is a cell, dir is a direction (up u, down d, left l, right
r), k is an integer constant drawn from the set {−3, −2, −1, 1, 2, 3}, and ϕ is a predicate. The semantics of this
construct is that it finds the k’th cell satisfying predicate ϕ in direction dir from the starting cell x. For instance, the
expression GetCell(x, r, 1, λy.λz.True) refers to x itself, while GetCell(x, r, 2, λy.λz.True) extracts the neighboring
cell to the right of cell x. An interesting point about the GetCell construct is that it is recursive: For instance, if x
is bound to cell (r , c), then the expression
GetCell(GetCell(x, u, 2, λy.λz.True), r, 2, λy.λz.True)
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

Synthesis of Data Completion Scripts using Finite Tree Automata
JVal(χ (z)) = sKT,c 1,c 2 = Eval(T(χ (c 2 )), =, s)

JVal(χ (z)) , sKT,c 1,c 2 = Eval(T(χ (c 2 )), ,, s)

JVal(χ (y)) = Val(χ (z))KT,c 1,c 2 = Eval(T(χ (c 1 )), =, T(χ (c 2 )))

Eval(s 1 , /, s 2 ) =

Jϕ 1 ∧ ϕ 2 KT,c 1,c 2 = Jϕ 1 KT,c 1,c 2 ∧ Jϕ 2 KT,c 1,c 2
JxKT,c = c

c=



false

1:7

if s 1 = ? or s 2 = ?

s1 / s2


•

otherwise

⊥

if c =⊥

[c]

otherwise


⊥ if Jτ KT,c =⊥ or |k | > len(L)

(




⊥
JGetCell(τ , dir, k, λy.λz.ϕ)KT,c = L.get k if k > 0
c1 ] c2 =



c 1 :: c 2
 L.get len(L) + 1 − |k | if k < 0


where L = filter range(Jτ KT,c , dir), (λy.λz. ϕ)Jτ KT,c

if c 1 =⊥ or c 2 =⊥
otherwise

JList(τ1 , ··, τn )KT,c = Jτ1 KT,c ] · · ]Jτn KT,c
(
⊥ if Jτ1 KT,c =⊥ or Jτ2 KT,c =⊥ or Jτ3 KT,c =⊥

JFilter(τ1 , τ2 , τ3 , λy.λz.ϕ)KT,c =
filter range(Jτ2 KT,c , Jτ3 KT,c ), (λyλz. ϕ)Jτ1 KT,c otherwise
(
JρKT,c if JρKT,c ,⊥
JSeq(ρ, π )KT,c =
Jπ KT,c otherwise

Fig. 6. Semantics of the DSL. T(·) gives the value of the given cell in table T. Function range(c, dir) returns all cells in the
direction dir from c (including c). Function range(c 1 , c 2 ) returns all cells between c 1 and c 2 (including c 1 and c 2 ) if c 1 and c 2
are in the same row/column, otherwise it gets stuck. Function filter(L, p) is the standard combinator that returns a list of
elements satisfying p in L.

retrieves the cell at row r − 1 and column c + 1. Effectively, the recursive GetCell construct allows the program
to “make turns” when searching for the target cell. As we observed in Example 2.3 from Section 2, the ability to
“make turns” is necessary for expressing many real-world data extraction tasks.
Another important point about the GetCell construct is that it returns ⊥ if the k’th entry from the starting cell
falls outside the range of the table. For instance, if the input table has 3 rows, then GetCell((3, 1), d, 2, λy.λz.True)
yields ⊥. Finally, another subtlety about GetCell is that the k value can be negative. For instance, GetCell(x, u, −1,
λy.λz.True) returns the uppermost cell in x’s column.
So far, we have seen how the GetCell construct allows us to express spatial (geometrical) relationships by
specifying a direction and a distance. However, as illustrated through the examples in Section 2, many real-world
data extraction tasks require combining geometrical and relational reasoning. For this purpose, predicates in our
DSL can be constructed using conjunctions of an expressive family of relations. Specifically, unary predicates
Val(χ (z)) = s and Val(χ (z)) , s in our DSL check whether or not the value of a cell χ (z) is equal to a string
constant s. Similarly, binary predicates Val(χ (y)) = Val(χ (z)) check whether two cells contain the same value.
Observe that the mapper function χ used in the predicate yields a new cell that shares some property with its
input cell z. For instance, the cell mapper λc.(row(c), 1) yields a cell that has the same row as c but whose column
is 1. The use of mapper functions in predicates allows us to further combine geometric and relational reasoning.
Example 4.1. Fig. 7 gives the desired cell extraction program for each hole from Fig. 4. For instance, the
program λT.λx . GetCell(x, l, 1, λy.λz.Val(z) , ?) yields the first non-missing value to the left of x. Similarly, the
cell extraction program for Example 2 yields the first cell c such that (1) c does not have a missing value, (2) c has
the same entry as x at column 1, and (3) c is obtained by going up from x.

PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

1:8

• Xinyu Wang, Isil Dillig, and Rishabh Singh

Task
Example 2.1
Example 2.2

Sketch
SUM(?1 , 1)
?1

Example 2.3

?1

Example 2.4
Example 2.5

COUNT(?1 )
?1

Implementation in our DSL
?1 ,→ λT.λx . GetCell(x, l, 1, λy.λz.Val(z) , ?)

?1 ,→ λT.λx . GetCell x, u, 1, λy.λz.Val(z) , ? ∧ Val((row(y), 1)) = Val((row(z), 1))
?1 ,→ λT.λx . GetCell GetCell(GetCell(x,
l, 2, λy.λz.True), u, 1, λy.λz.Val((row(z), 2)) =

“1”), d, 1, λy.λz.Val(z) , “0”
?1 ,→ λT.λx . Filter(x, GetCell(x, u, 1, Val(z) = “ ”), x, λy.λz.Val(z) , “ ”)

?1 ,→ λT.λx . Seq GetCell(x, u, 1, λy.λz.Val(z) , ?), GetCell(x, d, 1, λy.λz.Val(z) , ?)

Fig. 7. Code in the DSL for examples. The List keyword is omitted if it has only one cell program as the argument.
1:

procedure Learn(table T, set E)

2:
3:

input: Table T, and input-output examples E of the form {i 1 7→ L 1 , ··, i n 7→ Ln }
output: A Seq program satisfying all examples in E

4:
5:
6:
7:
8:

π := null;
for k := 1, ··, |E | do
π := LearnExtractor(T, k, E);
if π , null then return π ;
return null;

. Enumerate # branches

Fig. 8. Algorithm for Learn(T, E).

5

TOP-LEVEL SYNTHESIS ALGORITHM

We now present the synthesis algorithm for learning cell extraction programs from input-output examples. Recall
that the formula sketches provided by the user can contain multiple holes; hence, the synthesis algorithm is
invoked once per hole in the input sketch, given input-output examples for each hole.
Fig. 8 shows the high-level structure of our synthesis algorithm. The algorithm Learn takes as input a table T
and a set of examples E of the form {i 1 7→ L 1 , ··, i n 7→ Ln } and returns a Seq program π such that π is consistent
with all examples E. Essentially, the Learn algorithm enumerates the number of branches k in the Seq program
π . In each iteration of the loop (lines 5–7), it calls the LearnExtractor function to find the “best” program
that contains exactly k branches and satisfies all the input-output examples, and returns the program with the
minimum number of branches. If no such program is found after the loop exits, it returns null, meaning there is
no program in the DSL satisfying all examples in E. 7
Let us now consider the LearnExtractor procedure in Fig. 9 for learning a program with exactly k branches.
At a high level, LearnExtractor partitions the inputs E into k disjoint subsets S1 , ··, Sk and checks whether
each Si can be “unified”, meaning that all examples in Si can be represented using the same conditional-free
program. Our algorithm performs unification using the LearnSimpProg function, which we will explain later.
Let us now consider the recursive LearnExtractor procedure in a bit more detail. The base case of this
procedure corresponds to learning a simple (i.e., conditional-free) program. Since the synthesized program should
not introduce any branches, it simply calls the LearnSimpProg function to find a unifier ρ for examples E. Note
that the conditional-free program ρ here could be null.
The recursive case of LearnExtractor enumerates all subsets of all the input cells dom(E) that are to be
handled by the first simple program in the Seq construct (line 8). Here the notation dom(E) is defined as follows:
dom(E) = {i | (i 7→ L) ∈ E}
7A

discussion of the complexity of the algorithm can be found in the Appendix.

PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

Synthesis of Data Completion Scripts using Finite Tree Automata

1:

procedure LearnExtractor(table T, int k, set E)

2:

input: Table T, number of partitions k, and examples E of the form {i 1 7→ L 1 , ··, i n 7→ Ln }
output: A Seq program with k branches satisfying E

3:
4:
5:
6:

if k = 1 then
ρ := LearnSimpProg(T, E, ∅);
return ρ;

7:
8:
9:

π 0 := null;
for all P ∈ 2dom(E) do
ρ := LearnSimpProg(T, E ↓ P, P);
if ρ = null then continue;
π := LearnExtractor(T, k − 1, E ↓ P);
if π = null then continue;
π 00 := Seq(ρ, π );
if θ (π 00) > θ (π 0) then π 0 := π 00;
return π 0;

10:
11:
12:
13:
14:
15:

•

1:9

. Base case

. Recursive case

Fig. 9. Algorithm for LearnExtractor(T, k, E).

Given a subset P of all the input cells, we first try to unify the examples whose inputs belong to P. In particular,
the notation E ↓ P used at line 9 is defined as follows:
E ↓ P = {i 7→ L | i ∈ P ∧ (i 7→ L) ∈ E}
Hence, if the call to LearnSimpProg at line 9 returns non-null, this means there is a conditional-free program ρ
satisfying all examples in E ↓ P and returning failure (⊥) on all input cells P = dom(E)\P. Note that it is crucial
that ρ yields ⊥ on inputs P, because the second statement of the Seq construct is only evaluated when the first
program returns ⊥. For this reason, the unification algorithm LearnSimpleProg takes as input a set of negative
examples E − as well as positive examples E + . Observe that a “negative example” in our case corresponds to a
cell on which the learned program should yield ⊥.
Now, if unification of examples E ↓ P returns null, we know that P is not a valid subset and we move on to the
next subset. On the other hand, if E ↓ P is unifiable, we try to construct a program that contains k − 1 branches
and that is consistent with the remaining examples E ↓ P. If such a program exists (i.e, the recursive call to
LearnExtractor at line 11 returns non-null), we have found a program Seq(ρ, π ) that has exactly k branches and
that satisfies all input-output examples E. However, our algorithm does not return the first consistent program it
finds: In general, our goal is to find the “best” program, according to some heuristic cost metric θ (described in
the Appendix), that is consistent with the examples and that minimizes the number of branches. For this reason,
the algorithm only returns π 0 after it has explored all possible partitions (line 15).
Finally, let us turn our attention to the unification algorithm LearnSimpProg from Fig. 10 for finding a simple
(conditional-free) program ρ such that ρ(T, i) = L for all (i 7→ L) ∈ E + and ρ(T, i) = ⊥ for every i ∈ E − . The key
idea underlying LearnSimpProg is to construct a finite tree automaton A for each example i 7→ L such that
A accepts exactly those simple programs that produce L on input i. 8 Since constructing the FTA for a given
example is non-trivial, we will explain it in detail in the next section. Once we construct an FTA for each example,
8 Note

that here L can be either a list of cells or ⊥.
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

1:10

• Xinyu Wang, Isil Dillig, and Rishabh Singh

1:

procedure LearnSimpProg(table T, set E + , set E − )

input: E + is positive examples {i 1 7→ L 1 , ··, i n 7→ Ln }, and E − : {j 1 , ··, jm } is set of negative examples
3: output: A simple program satisfying both E + and E −
2:

4:
5:
6:
7:
8:

if ∃i, i 0 ∈ dom(E + ). len(E + [i]) , len(E + [i 0])
then t := −1;
else t := len(E + [i 1 ]);
A := FTA(T, i 1 , E + [i 1 ], t);

9:
10:

for i ∈ dom(E + ) \ {i 1 } do
A := A ∩ FTA(T, i, E + [i], t);

11:
12:

for j ∈ E − do
A := A ∩ FTA(T, j, ⊥, t);
if JAK = ∅ then return null;
ρ := Rank(A);
return ρ;

13:
14:
15:

. Initialization

. Positive examples
. Negative examples

. Rank programs

Fig. 10. Algorithm for LearnSimpProg(T, E + , E − ).

the final program is obtained by taking the intersection of the tree automata for each individual example (lines
8-12) and then extracting the best program accepted by the automaton (line 14).
Example 5.1. Consider a row vector [?, 1, ?, 2, ?]. The user wants to fill each missing value by the previous
non-missing value, if one exists, and by the next non-missing value otherwise. Here, the formula sketch is ?1 ,
and suppose that the user gives two examples for ?1 :
(1, 1) 7→ (1, 2) and (1, 3) 7→ (1, 2)
Given this input, DACE first tries to learn a Seq program with one branch by unifying two examples. Since there
is no such program in the DSL, the algorithm then tries to learn a program π = Seq(ρ 1 , ρ 2 ) by partitioning the
examples into two disjoint sets. There are two ways of partitioning the examples:
(1) The first partition is {(1, 1)}, meaning that ρ 1 should return (1, 2) on (1, 1) and ⊥ on (1, 3), and ρ 2 should
return (1, 2) on (1, 3). In this case, DACE learns the following two programs ρ 1 , ρ 2 :
ρ1 :
ρ2 :

GetCell(x, r, −2, λy.λz.Val(z) , ?)
GetCell(x, l, 1, λy.λz.Val(z) , ?)

(2) The second partition is {(1, 3)}, meaning that ρ 1 should return (1, 2) on (1, 3) and ⊥ on (1, 1), and ρ 2
should return (1, 2) on (1, 1). In this case, DACE learns the following two programs ρ 1 , ρ 2 :
ρ1 :
ρ2 :

GetCell(x, l, 1, λy.λz.Val(z) , ?)
GetCell(x, r, 1, λy.λz.Val(z) , ?)

After learning these two programs, DACE compares them according to a scoring function θ . In this case, the
second program has a higher score (because the scoring function prefers k values in GetCell with smaller absolute
value), hence we select the Seq program learned in the second case.
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

Synthesis of Data Completion Scripts using Finite Tree Automata

6

•

1:11

UNIFICATION USING TREE AUTOMATA

In this section, we describe how to represent conditional-free programs using finite tree automata (FTA). Since the
LearnSimpProg algorithm from Section 5 performs unification using standard FTA intersection (Comon et al.
2007), the key problem is how to construct a tree automaton representing all programs that are consistent with a
given input-output example. As mentioned in Section 1, our FTA-based formulation leads to a new version space
learning algorithm that offers several advantages over prior VSA-based techniques. We discuss the relationship
between our learning algorithm and VSA-based techniques in Section 9.

6.1

Preliminaries

Since the remainder of this section relies on basic knowledge about finite tree automata, we first provide some
background on this topic. At a high level, tree automata generalize standard automata by accepting trees rather
than words (i.e., chains).
Definition 6.1 (FTA). A (bottom-up) finite tree automaton (FTA) over alphabet F is a tuple A = (Q, F , Q f , ∆)
where Q is a set of states, Q f ⊆ Q is a set of final states, and ∆ is a set of transition (rewrite) rules of the form
f (q 1 , ··, qn ) → q where q, q 1 , ··, qn ∈ Q, and f ∈ F has arity n.
Here, the alphabet is ranked in that every symbol f in F has an
arity (rank) associated with it. The set of function symbols of arity k
is denoted Fk . In the context of tree automata, we view ground terms
over alphabet F as trees. Intuitively, an FTA accepts a ground term t
if we can rewrite t to some q ∈ Q f using rules in ∆. The language of
an FTA A, written L(A), is the set of all ground terms accepted by A.
Example 6.2. Consider the tree automaton defined by states Q = Fig. 11. Tree for ¬(1 ∧ ¬0) where each subterm is annotated with its state.
{q 0 , q 1 }, F0 = {0, 1}, F1 = {¬} F2 = {∧}, final state q 1 , and the following transitions ∆:
1 → q1
0 → q0
∧(q 0 , q 0 ) → q 0 ∧(q 0 , q 1 ) → q 0
¬(q 1 ) → q 0 ¬(q 0 ) → q 1 ∧(q 1 , q 0 ) → q 0 ∧(q 1 , q 1 ) → q 1
This tree automaton accepts exactly those propositional logic formulas (without variables) that evaluate to true.
As an example, Fig. 11 shows the tree for the formula ¬(1 ∧ ¬0) where each sub-term is annotated with its state.
Since q 0 is not a final state, this formula is rejected by the tree automaton.

6.2

Simple programs as tree automata

Suppose we are given a single input-output example i 7→ L where we have i ∈ Cells(T) and L is either ⊥ or a
list of cells [o 1 , ··, ot ] in table T. Our key idea is to construct a (deterministic) bottom-up FTA A such that L(A)
represents exactly those simple programs (i.e., abstract syntax trees) that produce output L on input cell i.
Before presenting the full FTA construction procedure, we first explain the intuition underlying our automata.
At a high level, the alphabet of the FTA corresponds to our DSL constructs, and the states in the FTA represent
cells in table T. The constructed FTA contains a transition f (c 1 , ··, c n ) → c if it is possible to get to cell c from
cells c 1 , · · c n via the DSL construct f . Hence, given an input cell c and output cell c 0, the trees accepted by our
FTA correspond to simple programs that produce output cell c 0 from input cell c.
With this intuition in mind, let us now consider the FTA construction procedure in more detail. Given a table
T, an input cell i, a list of output cells L (or ⊥ in the case of negative examples), and an integer t denoting the
number of output cells, we construct a tree automaton A = (Q, F , Q f , ∆) in the following way:
• The states Q include all cells in table T as well as two special symbols q ⊥ and q? :
Q = {qc | c ∈ Cells(T)} ∪ {q ⊥ , q? }
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

1:12

• Xinyu Wang, Isil Dillig, and Rishabh Singh

λc.c ∈ Mappers(T)

1 ≤ k ≤ NumCols(T)

1 ≤ k ≤ NumRows(T)

λc.(k, col(c)) ∈ Mappers(T)

λc.(row(c), k) ∈ Mappers(T)

χ ∈ Mappers(T), / ∈ {=, ,}
∃c ∈ Cells(T). s = Val(c)

χ ∈ Mappers(T)

(Val(χ (z)) / s) ∈ Preds(T)

Val(χ (y)) = Val(χ (z)) ∈ Preds(T)

True ∈ Preds(T)

ϕ 1 ∈ Preds(T), ϕ 2 ∈ Preds(T)
ϕ 1 ∧ ϕ 2 ∈ Preds(T)

Fig. 12. Rules for constructing the universe of predicates.

(Init)

T, i, L ` x → qi ∈ ∆
c ∈ Cells(T) ∪ {⊥}
JGetCell(c, dir, k, λy.λz.ϕ)KT = c 0

T, i, L ` GetCelldir,k,ϕ (qc ) → qc 0 ∈ ∆
L = [o 1 , ··, on ]
c 1 ∈ Cells(T), c 2 ∈ Cells(T), c 3 ∈ Cells(T)
JFilter(c 1 , c 2 , c 3 , λy.λz.ϕ)KT = L
T, i, L ` Filterϕ (qc 1 , qc 2 , qc 3 ) → q? ∈ ∆

(GetCell)

(Filter 1)

L = [o 1 , ··, on ]
T, i, L ` List(qo1 , ··, qon ) → q? ∈ ∆

(List 1)

L=⊥
∃k ∈ [1, n]. q jk = q ⊥
∀k ∈ [1, n]. q jk , q?

(List 2)

T, i, L ` List(q j1 , ··, q jn ) → q? ∈ ∆
L=⊥
∃k ∈ [1, 3]. q jk = q ⊥
∀k ∈ [1, 3]. q jk , q?
T, i, L ` Filterϕ (q j1 , q j2 , q j3 ) → q? ∈ ∆

(Filter 2)

Fig. 13. Rules for constructing transition rules ∆ for table T and example i 7→ L.

Here, q ⊥ denotes any cell that is outside the range of the input table, and q? indicates we have reached
all desired output cells.
• The final states Q f only include the special symbol q? (i.e., Q f = {q? }).
• The alphabet F is F0 ∪ F1 ∪ F3 ∪ Ft where F0 = {x }, Ft = {List} 9 , and
F3 = {Filterϕ | ϕ ∈ Preds(T)}
n

F1 = GetCelldir,k,ϕ

dir ∈ {u, d, l, r} ∧ k ∈ [1, 3] ∪ [−3, −1] ∧ ϕ ∈ Preds(T)

o

In other words, the alphabet of A consists of the DSL constructs for simple programs. Since Filter and
GetCell statements also use predicates, we construct the universe of predicates Preds(T) as shown in
Fig. 12 and generate a different symbol for each different predicate. Furthermore, since GetCell also takes
a direction and position as input, we also instantiate those arguments with concrete values.
• The transitions ∆ of A are constructed using the inference rules in Fig. 13. The Init rule says that argument
x is bound to input cell i. The GetCell rule states that GetCelldir,k,ϕ (qc ) can be rewritten to qc 0 if we can
get to cell c 0 from c using the GetCell construct in the DSL. The List 1 rule says that we can reach the final
state q? if the arguments of List correspond to cells in the output L. Finally, the Filter 1 rule states that
we can reach the final state q? from states qc 1 , qc 2 , qc 3 via Filterϕ if Filter(c 1 , c 2 , c 3 , ϕ) yields the output
L on input table T. The second variants of the rules (labeled 2) deal with the special case where L = ⊥
(negative example). For instance, according to the List 2 rule, we can reach the final state q? if the desired
output is ⊥ and any of the arguments of List is ⊥.
9 If

t is −1, then we have F = F0 ∪ F1 ∪ F3 . Recall from Fig. 10 that t = −1 indicates that the positive examples differ in the number of
output cells; hence, there can be no simple program constructed using List that is consistent with all input-output examples.
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

•

1:13

Desc. Prog.

Tree

Synthesis of Data Completion Scripts using Finite Tree Automata

List(GetCell(x, u, 2, λy .λz .True)) List(GetCell(x, u, 1, λy .λz .Val(z) , ?))
The previous cell upwards

The previous non-missing cell upwards

Filter x, GetCell(x, u, −1, λy .λz .True),
 GetCell(x,
d, −1, λy .λz .True), λy .λz .Val(z) , ?
All non-missing cells in the same column

Fig. 14. Three terms (programs) accepted by the tree automaton in Example 6.4.

Theorem 6.3. (Soundness and Completeness) Let A be the finite tree automaton constructed by our technique
for example i 7→ L and table T. Then, A accepts the tree that represents a simple program ρ iff JρKT,i = L.
Proof. Provided in the appendix.

Example 6.4. Consider a small table with two rows, where the first row is [4, 5] and the second row is [6, ?].
Furthermore, suppose the user provides the sketch ?1 and the example {(2, 2) 7→ [(1, 2)]} (i.e., ? should be 5).
Let us consider the FTA construction for this example. The states in the FTA are {q (1,1) , q (1,2) , q (2,1) , q (2,2) , q ⊥ , q ∗ },
and the final state is q ∗ . The transition rules ∆ of the FTA are constructed according to Fig. 13. For example, ∆
includes x → q (2,2) because cell (2, 2) is the input cell in the example (Init). It also includes GetCellu,2,True (q (2,2) ) →
q (1,2) because, using GetCell, we have
JGetCell((2, 2), u, 2, λy.λz.True)KT = (1, 2)

Using List 1, the transition rules ∆ also include the transition List(q (1,2) ) → q ∗ and, using Filter 1, it contains:
FilterVal(z),? (q (2,2) , q (1,2) , q (2,2) ) → q ∗

6.3

Ranking programs accepted by tree automaton

Recall from Section 5 that the LearnSimpProg algorithm requires finding the “best” program accepted by A
according to a Rank function. In this section, we briefly discuss how we rank programs accepted by a tree
automaton. In the rest of this section, we use the term “program” and its corresponding AST interchangably.
Definition 6.5. The size of a tree (term) t, denoted by ||t ||, is inductively defined by:
- ||t || = 1 if t ∈ F0 ,
- ||t || = 1 + Σi ∈ {1, ··,n } ||ti || if Root(t) ∈ Fn , where ti is the i-th argument of t.
The ranking function Rank(A) selects the best program by finding a tree t in L(A) such that ||t || is minimized.
If there are multiple trees with the same size, it selects the one with the highest score according to a heuristic
scoring function θ . Intuitively, θ assigns a positive score to each language construct in our DSL so that a more
“general” construct has a higher score. For example, the identity mapper λc.c is assigned a higher score than the
other cell mappers, and predicate True has a higher score than other predicates. More details about the heuristic
scoring function θ are provided in the appendix.
Example 6.6. Fig. 14 shows a subset of the programs accepted by the tree automaton A from Example 6.4. The
first program, List(x, u, 2, λy.λz.True), is selected as the best program, because it is of the minimum size (3), and
it only uses the most general predicate True.
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

1:14

7

• Xinyu Wang, Isil Dillig, and Rishabh Singh

IMPLEMENTATION

We have implemented the synthesis algorithm proposed in this paper in a tool called DACE, written in Java.
While our implementation mostly follows our technical presentation, it performs several additional optimizations.
First, our presentation of LearnSimpProg algorithm constructs a separate tree automaton for each example.
However, observe that the tree automata for different examples actually have the same set of cells and share a
large subset of the transitions. Based on this observation, our implementation constructs a base (incomplete)
tree automaton A B that is shared by all examples and then adds additional transitions to A B for each individual
example. Second, our implementation memoizes results of automaton intersection. Since the top-level synthesis
algorithm ends up intersecting the same pair of automata many times, this kind of memoization is useful for
improving the efficiency of our synthesis procedure. In addition to these optimizations, our implementation also
limits the number of nested GetCell constructs to be at most 4. We have found this restriction to improve the
scalability of automaton intersection without affecting expressiveness in practice.

8

EVALUATION

In this section, we present the results of our evaluation on 84 data completion benchmarks collected from online
forums. All experiments are conducted on an Intel Xeon(R) machine with an E5-2630 CPU and 64G of memory.
Benchmarks. To evaluate the proposed synthesis technique , we collected a total of 84 data completion benchmarks from StackOverflow by searching for posts containing relevant keywords such as “data imputation”,
“missing value”, “missing data”, “spreadsheet formula”, and so on. We then manually inspected each post and
only retained those benchmarks that are indeed relevant to data completion and that contain at least one example. Among these 84 benchmarks, 46 involve data imputation in languages such as R and Python, 32 perform
spreadsheet computation in Excel and Google Sheets, and 6 involve data completion in relational databases.
Recall that an input to DACE consists of (a) a small example table, (b) a sketch formula, and (c) a mapping
from each hole in the sketch to a set of examples of the form i 7→ [o 1 , ··, on ]. As it turns out, most posts contain
exactly the type of information that DACE requires: Most questions related to data completion already come
with a small example table, a simple formula (or a short description in natural language), and a few examples that
show how to instantiate the formula for concrete cells in the table.
We categorize our benchmarks in 21 groups according to their shared functionality. Specifically, as shown
in Fig. 15, benchmarks in the same category typically require the same sketch. For instance, all benchmarks
in the first category in Fig. 15 share the sketch ?1 and require filling the missing value with the previous/next
non-missing value (with or without the same key). The column labeled “Formula sketch” shows the concrete
sketch for each benchmark category. Observe that most of these sketches are extremely simple to write. In fact,
for over 50% of the benchmarks, the user only needs to specify the sketch ?1 , which is equivalent to having no
sketch at all. The next column labeled Count indicates the number of benchmarks that belong to the corresponding
category, and the column called “Avg. table size” shows the average number of cells in the tables for each category.
Finally, the last column labeled “Avg. # examples per hole” shows the average number of examples that the user
provides in the original StackOverflow post. Observe that this is not the number of examples that DACE actually
requires to successfully perform synthesis, but rather the number of all available examples in the forum post.
Experimental Setup. Since DACE is meant to be used in an interactive mode where the user iteratively provides
more examples, we simulated a realistic usage scenario in the following way: First, for each benchmark, we
collected the set S of all examples provided by the user in the original Stackoverflow post. We then randomly
picked a single example e from S and used DACE to synthesize a program P satisfying e. If P failed any of the
examples in S, we then randomly sampled a failing test case e 0 from S and used DACE to synthesize a program
that satisfies both e and e 0. We repeated this process of randomly sampling examples from S until either (a) the
synthesized program P satisfies all examples in S, or (b) we exhaust all examples in S, or (c) we reach a time-out
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

Fill missing value by previous/next non-missing value with/without same keys.
Fill missing value by previous (next) non-missing value with/without same keys
if one exists, otherwise use next (previous) non-missing value
Replace missing value by the average of previous and next non-missing values.
Fill missing value by the average of previous and next non-missing values, but
if either one does not exist, fill by the other one.
Replace missing value by the sum of previous non-missing value (with or without
the same key) and a constant.
Replace missing value by the average of all non-missing values in the same
row/column (with or without same keys).
Replace missing value by the max/min of all non-missing values in the column
with the same key.
Fill missing value by linear interpolation of previous/next non-missing values.
Fill cells by copying values from other cells in various non-trivial ways, such as
by copying the first/last entered entry in the same/previous/next row, and etc.
Fill value by the sum of a range of cells in various ways, such as by summing all
values to the left with the same keys.
Fill cells with the count of non-empty cells in a range.
Fill cells in a column by the sum of values from two other cells.
Fill each value in a column by the difference of values in two other cells in
different columns found in various ways.
Replace missing value by the average of two non-missing values to the left.
Complete a column so that each value is the difference of the sum of a range of
cells and another fixed cell.
Fill each value in a column by the difference of a cell and sum of a range of cells.
Create column where each value is the max of previous five cells in sibling
column.
Fill blank cell in a column by concatenating two values to its right.
Fill missing value by the linear extrapolation of the next two non-missing values
to the right, but if there is only one or zero such entries, fill by the linear
extrapolation of the previous two non-missing values to the left.
Replace missing values by applying an equation (provided by the user) to the
previous and next non-missing values.
Fill missing value using the highest value or linear interpolation of two values
before and after it, based on two different criteria.
Summary

Formula sketch

Avg. # examples
per hole

1

1:15

Avg. table size

Benchmark category description

•

Count

Synthesis of Data Completion Scripts using Finite Tree Automata

?1

24

24.4

5.3

?1

9

25.6

5.7

AVG(?1, ?2 )

3

12.7

2.3

AVG(?1 )

2

21.5

4

SUM(?1, c)

3

31.3

5.7

AVG(?1 )

7

21.7

3.1

MAX(?1 ), MIN(?1 )

2

28.0

3

INTERPOLATE(?1, ?2 )

2

28.0

7.5

?1

13

44.5

10.2

SUM(?1 )

4

47.8

10.3

COUNT(?1 )
SUM(?1, ?2 )

1
2

32.0
38.3

3
6.5

MINUS(?1, ?2 )

4

39.0

3.5

AVG(?1, ?2 )

1

32.0

5

MINUS(SUM(?1 ), ?2 )

1

27.0

8

MINUS(?1, SUM(?2 ))

1

10.0

3

MAX(?1 )

1

60.0

15

CONCAT(?1, ?2 )

1

12.0

2

EXTRAPOLATE(?1 )

1

121.0

16

1

60.0

9

1

60.0

10

84

32.0

6.3

SUM(?1,

MINUS(?1 , ?2 )
ROW(?2 )−ROW(?1 ) )

—

Fig. 15. Benchmark statistics.

of 30 seconds per synthesis task. At the end of this process, we manually inspected the program P synthesized by
DACE and checked whether P conforms to the natural language description provided by the user.
Results. We present the main results of our evaluation of DACE in Fig. 16. The column “# Solved” shows the
number of benchmarks that can be successfully solved by DACE for each benchmark category. Overall, DACE
can successfully synthesize over 92% of the benchmarks. Among the six benchmarks that cannot be synthesized
by DACE, one benchmark (Category 21) cannot be expressed using our specification language. For the remaining
5 benchmarks, DACE fails to synthesize the correct program due to limitations of our DSL, mainly caused by the
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

• Xinyu Wang, Isil Dillig, and Rishabh Singh

Med.

Avg.

Med.

Avg.

Med.

24
7
3
1
3
5
1
1
5
1
0
1
2
0
1
0
1
1
0
0
0

1.32
4.88
5.16
2.11
0.90
15.86
296.17
19.72
6.02
2.27
—
66.95
1.52
—
148.95
—
183.19
1.44
—
—
—

0.73
1.13
5.89
2.11
0.99
8.31
296.17
19.72
1.52
2.27
—
66.95
1.52
—
148.95
—
183.19
1.44
—
—
—

1.1
2.4
1.0
2.0
1.7
1.8
3.0
1.0
1.4
2.0
—
2.0
2.0
—
3.0
—
2.0
1.0
—
—
—

1.0
2.0
1.0
2.0
1.0
2.0
3.0
1.0
1.0
2.0
—
2.0
2.0
—
3.0
—
2.0
1.0
—
—
—

6
2
0
0
0
5
0
1
2
0
3
0
0
0
0
0
1
0
0
0
0

230
182
—
—
—
353
—
501
507
—
223
—
—
—
—
—
78
—
—
—
—

224
182
—
—
—
352
—
501
507
—
182
—
—
—
—
—
78
—
—
—
—

6
0
0
0
0
4
0
0
0
0
3
0
0
0
0
0
1
0
0
0
0

314
—
—
—
—
399
—
—
—
—
353
—
—
—
—
—
81
—
—
—
—

281
—
—
—
—
400
—
—
—
—
298
—
—
—
—
—
81
—
—
—
—

All

84

78

0.70

0.19

1.8

2.0

57

16.09

1.18

1.5

1.0

20

289

226

14

330

314

Run
per ning
ben time
ch
(sec mark
)

Avg.

1.0
3.0
1.0
2.0
1.0
2.0
2.0
1.0
2.0
2.0
1.0
1.0
2.0
3.0
2.0
2.0
4.0
1.0
5.0
1.0
—

# Solved (3 exs)

Med.

1.1
2.7
1.0
2.0
1.3
1.8
2.0
1.0
2.8
1.7
1.0
1.0
2.0
3.0
2.0
2.0
4.0
1.0
5.0
1.0
—

Run
per ning
ben time
ch
(sec mark
)

Avg.

0.04
0.13
0.04
0.19
0.14
0.07
0.66
0.15
0.31
0.30
0.59
0.51
0.46
0.16
0.11
0.03
1.96
0.01
13.66
1.92
—

# Solved (2 exs)

Med.

0.41
0.50
0.05
0.19
0.18
0.09
0.66
0.15
1.55
0.42
0.59
0.51
0.51
0.16
0.11
0.03
1.96
0.01
13.66
1.92
—

# Solved

Avg.

24
9
3
2
3
6
2
2
10
3
1
2
4
1
1
1
1
1
1
1
0

#E
use xamp
l
dp
er h es
ole

Med.

24
9
3
2
3
7
2
2
13
4
1
2
4
1
1
1
1
1
1
1
1

Run
per ning
ben time
ch
(sec mark
)

Avg.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

# Solved

#E
use xamp
l
dp
er h es
ole

SKETCH

Run
per ning
ben time
ch
(sec mark
)

PROSE

Count

DACE

Benchmark category

1:16

Fig. 16. Evaluation results of DACE, as well as PROSE and SKETCH as two baselines. The time-out for DACE is set to be 30
seconds, whereas the time-out for baselines is set to be 10 minutes.

restricted vocabulary of predicates. For instance, two benchmarks require capturing the concept “nearest”, which
is not expressible by our current predicate language.
Next, let us consider the running time of DACE, which is shown in the column labeled “Running time per
benchmark”. We see that DACE is quite fast in general and takes an average of 0.7 seconds to solve a benchmark.
The median time to solve these benchmarks is 0.19 seconds. In cases where the sketch contains multiple holes,
the reported running times include the time to synthesize all holes in the sketch. In more detail, DACE can
synthesize 75% of the benchmarks in under one second and 87% of the benchmarks in under three seconds. There
is one benchmark (Category 19) where DACE’s running time exceeds 10 seconds. This is because (a) the size of
the example table provided by the user is large in comparison to other example tables, and (b) the table contains
over 100 irrelevant strings that form the universe of constants used in predicates. These irrelevant entries cause
DACE to consider over 30, 000 predicates to be used in the GetCell and Filter programs.
Finally, let us look at the number of examples used by DACE, as shown in the column labeled “# Examples
used per hole”. As we can see, the number of examples used by DACE is much smaller than the total number of
examples provided in the benchmark (as shown in Fig. 15). Specifically, while StackOverflow users provide about
6 examples on average, DACE requires only about 2 examples to synthesize the correct program. This statistic
highlights that DACE can effectively learn general programs from very few input-output examples.
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

Synthesis of Data Completion Scripts using Finite Tree Automata

•

1:17

Comparison with PROSE. In this paper, we argued that our proposed FTA-based technique can be viewed as a
new version space learning algorithm; hence, we also empirically compare our approach again PROSE (Polozov and
Gulwani 2015), which is the state-of-the-art version space learning framework that has been deployed in Microsoft
products. To provide some background, PROSE propagates example-based constraints on subexpressions using
the inverse semantics of DSL operators and then represents all programs that are consistent with the examples
using a version space algebra (VSA) data structure (Lau et al. 2003).
To allow a fair comparison between PROSE and DACE, we use the same algorithm presented in Section 5 to
learn the Seq construct (i.e., branches), but we encode simple programs in the DSL using the PROSE format. 10
Since PROSE’s learning algorithm requires so-called witness functions, which describe the inverse semantics of
each DSL construct, we also manually wrote precise witness functions for all constructs in our DSL. Finally, we
use the same scoring function θ described in the Appendix to rank different programs in the version space.
The results of our evaluation are presented under the PROSE column in Fig. 16. Overall, PROSE can successfully
solve 68% of the benchmarks in an average of 15 seconds, whereas DACE can solve 92% of the benchmarks in an
average of 0.7 seconds. These results indicate that DACE is superior to PROSE, both in terms of its running time
and the number of benchmarks that it can solve. Upon further inspection of the PROSE results, we found that the
tasks that can be automated using PROSE tend to be relatively simple ones, where the input table size is very
small or the desired program is relatively simple. For benchmarks that have larger tables or involve more complex
synthesis tasks (e.g., require the use of Filter operator), PROSE does not scale well – i.e., it might take much longer
time than DACE, time out in 10 minutes, or run out of memory. We provide more details and intuition regarding
why our FTA-based learning algorithm performs better than PROSE’s VSA-based algorithm in Section 9.
The careful reader may have observed in Fig. 16 that PROSE requires fewer examples on average than DACE
(1.5 vs. 1.8). However, this number is quite misleading, as the benchmarks that can be solved using PROSE are
relatively simple and therefore require fewer examples on average.
Comparison with SKETCH. Since our synthesis methodology involves a sketching component in addition to
examples, we also compare DACE against SKETCH, which is the state-of-the-art tool for program sketching. To
compare DACE against SKETCH, we define the DSL operators using nested and recursive structures in SKETCH.
For each struct, we define two corresponding functions, namely RunOp and LearnOp. The RunOp function
defines the semantics of the operator whereas LearnOp encodes a SKETCH generator that defines the bounded
space of all possible expressions in the DSL. The specification is encoded as a sequence of assert statements of
the form assert RunExtractor(LearnExtractor(), i k ) == Lk , where (i k , Lk ) denotes the input-output examples. To
optimize the sketch encoding further, we use the input-output examples inside the LearnOp functions, and we
also manually unroll and limit the recursion in predicates and cell programs to 3 and 4 respectively.
When we use the complete DSL encoding, SKETCH was able to solve only 1 benchmark out of 84 within a
time limit of 10 minutes per benchmark. We then simplified the SKETCH encoding by removing the Seq operator,
which allows us to synthesize only conditional-free programs. As shown in Fig. 16, SKETCH terminated on 20
benchmarks within 10 minutes using 2 input-output examples. The average time to solve each benchmark was
289 seconds. However, on manual inspection, we found that most of the synthesized programs were not the
desired ones. When we increase the number of input-output examples to 3, 14 benchmarks terminated with an
average of 330 seconds, but only 5 of these 14 programs were the desired ones. We believe that SKETCH performs
poorly due to two reasons: First, the constraint-based encoding in SKETCH does not scale for complex synthesis
tasks that arise in the data completion domain. Second, since it is difficult to encode our domain-specific ranking
heuristics using primitive cost operations supported by SKETCH, it often generates undesired programs. In
summary, this experiment confirms that a general-purpose program sketching tool is not adequate for automating
the kinds of data completion tasks that arise in practice.
10

PROSE performs significantly worse (i.e., terminates on only three benchmarks) if we use PROSE’s built-in technique for learning Seq.
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

1:18

9

• Xinyu Wang, Isil Dillig, and Rishabh Singh

VERSION SPACE LEARNING USING FINITE TREE AUTOMATA

So far in this paper, we focused on our algorithm for synthesizing data completion tasks in our domain-specific
language. However, as argued in Section 1, our FTA-based formulation of unification can be seen as a new
version-space learning algorithm. In this section, we outline how our FTA-based learning algorithm could
be applied to other settings, and we also discuss the advantages of our learning algorithm compared to prior
VSA-based techniques (Gulwani 2011; Lau et al. 2003; Polozov and Gulwani 2015).

9.1

The general idea

To see how our FTA-based unification procedure can be used as a general version space learning algorithm, let us
consider a domain-specific language specified by a context-free grammar G = (T , N , P, S), where T is a finite set
of terminals (i.e., variables and constants), N is the set of non-terminal symbols, P is a set of productions of the
form e → F (e 1 , ··, en ) where F is a built-in DSL function (i.e., “component”), and S is the start symbol representing
a complete program. To simplify the presentation, let us assume that the components used in each production
are first-order; if they are higher-order, we can combine our proposed methodology with enumerative search (as
we did in this paper for dealing with predicates inside the Filter and GetCell constructs).
Now, our general version space learning algorithm works as follows. For each input-output example σ → o,
where σ is a valuation and o is the output value, we construct an FTA A = (Q, F , Q f , ∆) that represents exactly
the set of programs that are consistent with the examples. Here, the alphabet F of the FTA consists of the built-in
components provided by the DSL.
To construct the states Q of the FTA, let us assume that every non-terminal symbol n ∈ N has a pre-defined
universe Un = {v 1 , ··, vk } of values that it can take. Then, we introduce a state qvni for every n ∈ N and vi ∈ Un ; let
us refer to the set of states for all non-terminals in N as Q N . We also construct a set of states QT by introducing
a state qt for each terminal t ∈ T . Then, the set of states in the FTA is given by Q N ∪ QT .
Next, we construct the transition rules ∆ using the productions P in the grammar. To define the transitions, let
us define a function dom(s) that gives the domain of s for every symbol s:

if s is constant

 s

dom(s) = σ (s) if s is a variable

 Us
if s is a non-terminal, and Us is its corresponding universe


Now, consider a production of the form n → F (s 1 , ··, sk ) in the grammar where n is a non-terminal and each si is
either a terminal or non-terminal. For every vi ∈ dom(si ), we add a transition F (qvs11 , ··, qvskk ) → qvn iff we have
v = JF (v 1 , ··, vk )K. In addition, for every variable x, we add a transition x → q x . Finally, the final state Q f is a
singleton containing the state qoS , where S is the start symbol of the grammar and o is the output in the example.
Given this general methodology for FTA construction, the learning algorithm works by constructing the
FTA for each individual example and then intersecting them. The final FTA represents the version space of all
programs that are consistent with the examples.

9.2

Comparison with prior version space learning techniques

As mentioned briefly in Section 1, we believe that our FTA-based learning algorithm has two important advantages
compared to the VSA-based approach in PROSE. First, FTAs yield a more succinct representation of the version
space compared to VSAs in PROSE. To see why, recall that VSA-based approaches construct more complex
version spaces by combining smaller version spaces using algebraic operators, such as Join and Union. In essence,
PROSE constructs a hierarchy of version spaces where the version spaces at lower levels can be shared by version
spaces at higher levels, but cyclic dependencies between version spaces are not allowed. As a result, PROSE must
unroll recursive language constructs to introduce new version spaces, but this unrolling leads to a less compact
representation with less sharing between version spaces at different layers. The second advantage of our learning
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

Synthesis of Data Completion Scripts using Finite Tree Automata

•

1:19

algorithm using FTAs is that it does not require complex witness functions that encode inverse semantics of DSL
constructs. Specifically, since PROSE propagates examples backwards starting from the output, the developer of
the synthesizer must manually specify witness functions. In contrast, the methodology we outlined in Section 9.1
does not require any additional information beyond the grammar and semantics of the DSL.
We refer the interested reader to the Appendix for an example illustrating the differences between PROSE’s
VSA-based learning algorithm and our FTA-based technique.

10

RELATED WORK

In this section, we compare and contrast our approach with prior work on program synthesis.
Programming-by-example. In recent years, there has been significant interest in programming by example
(PBE) (Bornholt et al. 2016; Feser et al. 2015; Gulwani 2011; Osera and Zdancewic 2015; Polikarpova et al. 2016;
Polozov and Gulwani 2015; Smith and Albarghouthi 2016; Udupa et al. 2013; Wang et al. 2016; Yaghmazadeh
et al. 2016). Existing PBE techniques can be roughly categorized into two classes, namely enumerative search
techniques (Feser et al. 2015; Osera and Zdancewic 2015; Udupa et al. 2013), and those based on version space
learning (Gulwani 2011; Polozov and Gulwani 2015; Singh and Gulwani 2012).
The enumerative techniques search a space of programs to find a single program that is consistent with the
examples. Specifically, they enumerate all programs in the language in a certain order and terminate when they
find a program that satisfies all examples. Recent techniques in this category employ various pruning methods
and heuristics, for instance by using type information (Osera and Zdancewic 2015; Polikarpova et al. 2016),
checking partial program equivalence (Albarghouthi et al. 2013; Udupa et al. 2013), employing deduction (Feser
et al. 2015), or performing stochastic search (Schkufza et al. 2013).
In contrast, PBE techniques based on version space learning construct a compact data structure representing
all possible programs that are consistent with the examples. The notion of version space was originally introduced
by Mitchell (Mitchell 1982) as a general search technique for learning boolean functions from samples. Lau et
al. later extended this concept to version space algebra for learning more complex functions (Lau et al. 2003).
The basic idea is to build up a complex version space by composing together version spaces containing simpler
functions, thereby representing hypotheses hierarchically (Pardowitz et al. 2007).
The synthesis algorithm proposed in this paper is another technique for performing version space learning –
i.e., we build a data structure (namely, finite tree automaton) that represents all consistent hypotheses. However,
our approach differs from previous work using version space learning in several key aspects: First, unlike VSAbased techniques that decompose the version space of complex programs into smaller version spaces of simpler
programs, we directly construct a tree automaton whose language accepts all consistent programs. Second, our
FTA construction is done in a forward manner, rather than by back-propagation as in previous work (Polozov
and Gulwani 2015). Consequently, we believe that our technique results in a more compact representation and
enables better automation.
Program sketching. In sketch-based synthesis (Lezama 2008; Solar-Lezama et al. 2007, 2005, 2006), the programmer provides a skeleton of the program with missing expressions (holes). Our approach is similar to program
sketching in that we require the user to provide a formula sketch, such as SUM(?1 , ?2 ). However, holes in our
formula sketches are programs rather than constants. Furthermore, while SKETCH uses a constraint-based
counter-example guided inductive synthesis algorithm, DACE uses a combination of finite tree automata and
enumerative search. As we show in our experimental evaluation, DACE is significantly more efficient at learning
data completion programs compared to SKETCH.
Tree automata. Tree automata were introduced in the late sixties as a generalization of finite word automata (Thatcher and Wright 1968). Originally, ranked tree automata were used to prove the existence of
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

1:20

• Xinyu Wang, Isil Dillig, and Rishabh Singh

a decision procedure for weak monadic second-order logic with multiple successors (Thatcher and Wright 1968).
In the early 2000s, unranked tree automata have also gained popularity as a tool for analyzing XML documents
where the number of children of a node are not known a priori (Cristau et al. 2005; Martens and Niehren 2005).
More recently, tree automata have found numerous applications in the context of software verification (Abdulla
et al. 2008; Kafle and Gallagher 2015), analysis of XML documents (Cristau et al. 2005; Hosoya and Pierce 2003;
Martens and Niehren 2005), and natural language processing (Knight and May 2009; May and Knight 2008).
Most related to our technique is the work of Parthasarathy in which they advocate the use of tree automata
as a theoretical basis for synthesizing reactive programs (Madhusudan 2011). In that work, the user provides a
regular ω-specification describing the desired reactive system, and the proposed synthesis methodology constructs a non-deterministic tree automaton representing programs (over a simple imperative language) that meet
the user-provided specification. The technique first constructs an automaton that accepts reactive programs
corresponding to the negation of the regular ω-specification, and then complements it to obtain the automaton
for representing the desired set of programs. In contrast to the purely theoretical work of Parthasarathy in the
context of synthesizing reactive programs from regular ω-specifications, we show how finite tree automata can
be used in the context of program synthesis from examples. Moreover, we combine this FTA-based approach with
enumerative search to automatically synthesize programs for real-world data completion tasks in a functional
DSL with higher-order combinators.

11

CONCLUSIONS AND FUTURE WORK

In this paper, we presented a new approach for automating data completion tasks using a combination of program
sketching and programming-by-example. Given a formula sketch where holes represent programs and a set of
input-output examples for each hole, our technique generates a script that can be used to automate the target data
completion task. To solve this problem, we introduced a new domain-specific language that combines relational
and spatial reasoning for tabular data and a new synthesis algorithm for generating programs over this DSL. Our
synthesis procedure combines enumerative search (for learning conditionals) with a new version-space learning
algorithm that uses finite tree automata. We also showed the generality of our FTA-based learning algorithm
by explaining how it can be used synthesize programs over any arbitrary DSL specified using a context-free
grammar.
We evaluated our proposed synthesis algorithm on 84 data completion tasks collected from StackOverflow and
compared our approach with two existing state-of-the-art synthesis tools, namely PROSE and SKETCH. Our
experiments demonstrate that DACE is practical enough to automate a large class of data completion tasks and
that it significantly outperforms both PROSE and SKETCH in terms of both running time and the number of
benchmarks that can be solved.
We are interested in two main directions for future work. First, as discussed in Section 8, there are a few
benchmarks for which DACE’s DSL (specifically, predicate language) is not sufficiently expressive. While such
benchmarks seem to be relatively rare, we would like to investigate how to enrich the DSL so that all of these
tasks can be automated. Second, we would like to apply our new version-learning algorithm using FTAs to other
domains beyond data completion. We believe that our new VS-learning algorithm can be quite effective in other
domains, such as automating table transformation tasks.

PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

Synthesis of Data Completion Scripts using Finite Tree Automata

•

1:21

REFERENCES
Parosh A Abdulla, Ahmed Bouajjani, Lukáš Holı́k, Lisa Kaati, and Tomáš Vojnar. 2008. Composed bisimulation for tree automata. In
International Conference on Implementation and Application of Automata. Springer, 212–222.
Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. 2013. Recursive Program Synthesis (CAV). Springer-Verlag, 934–950.
Rajeev Alur, Pavol Černỳ, and Arjun Radhakrishna. 2015. Synthesis through unification. In International Conference on Computer Aided
Verification. Springer, 163–179.
James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. 2016. Optimizing Synthesis with Metasketches (POPL). ACM, 775–788.
H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. 2007. Tree Automata Techniques and
Applications. Available on: http://www.grappa.univ-lille3.fr/tata. (2007). release October, 12th 2007.
Julien Cristau, Christof Löding, and Wolfgang Thomas. 2005. Deterministic Automata on Unranked Trees (FCT’05). Springer-Verlag, 68–79.
John K. Feser, Swarat Chaudhuri, and Isil Dillig. 2015. Synthesizing Data Structure Transformations from Input-output Examples (PLDI).
ACM, 229–239.
Sumit Gulwani. 2011. Automating String Processing in Spreadsheets Using Input-output Examples (POPL). ACM, 317–330.
Haruo Hosoya and Benjamin C. Pierce. 2003. XDuce: A Statically Typed XML Processing Language. ACM Trans. Internet Technol. 3, 2 (2003),
117–148.
Bishoksan Kafle and John P. Gallagher. 2015. Tree Automata-Based Refinement with Application to Horn Clause Verification (VMCAI 2015).
Springer-Verlag New York, Inc., 209–226.
Kevin Knight and Jonathan May. 2009. Applications of weighted automata in natural language processing. In Handbook of Weighted Automata.
Springer, 571–596.
Tessa Lau, Steven A. Wolfman, Pedro Domingos, and Daniel S. Weld. 2003. Programming by Demonstration Using Version Space Algebra.
Mach. Learn. 53, 1-2 (2003), 111–156.
A Solar Lezama. 2008. Program synthesis by sketching. Ph.D. Dissertation.
Parthasarathy Madhusudan. 2011. Synthesizing Reactive Programs. In Computer Science Logic. 428–442.
Wim Martens and Joachim Niehren. 2005. Minimizing Tree Automata for Unranked Trees. Springer Berlin Heidelberg, 232–246.
Jonathan May and Kevin Knight. 2008. A Primer on Tree Automata Software for Natural Language Processing. (2008).
Tom M Mitchell. 1982. Generalization as search. Artificial intelligence 18, 2 (1982), 203–226.
Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed Program Synthesis (PLDI). ACM, 619–630.
Michael Pardowitz, Bernhard Glaser, and Rüdiger Dillmann. 2007. Learning Repetitive Robot Programs from Demonstrations Using Version
Space Algebra. In Proceedings of the 13th IASTED International Conference on Robotics and Applications (RA). ACTA Press, 394–399.
Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types (PLDI). ACM,
522–538.
Oleksandr Polozov and Sumit Gulwani. 2015. FlashMeta: A Framework for Inductive Program Synthesis (OOPSLA). ACM, 107–126.
Eric Schkufza, Rahul Sharma, and Alex Aiken. 2013. Stochastic Superoptimization (ASPLOS ’13). 305–316.
Rishabh Singh and Sumit Gulwani. 2012. Synthesizing number transformations from input-output examples (CAV). Springer, 634–651.
Calvin Smith and Aws Albarghouthi. 2016. MapReduce Program Synthesis (PLDI). ACM, 326–340.
Armando Solar-Lezama, Gilad Arnold, Liviu Tancau, Rastislav Bodik, Vijay Saraswat, and Sanjit Seshia. 2007. Sketching Stencils (PLDI). ACM,
167–178.
Armando Solar-Lezama, Rodric Rabbah, Rastislav Bodı́k, and Kemal Ebcioğlu. 2005. Programming by Sketching for Bit-streaming Programs
(PLDI). ACM, 281–294.
Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs
(ASPLOS). ACM, 404–415.
James W Thatcher and Jesse B Wright. 1968. Generalized finite automata theory with an application to a decision problem of second-order
logic. Theory of Computing Systems 2, 1 (1968), 57–81.
Abhishek Udupa, Arun Raghavan, Jyotirmoy V. Deshmukh, Sela Mador-Haim, Milo M. K. Martin, and Rajeev Alur. 2013. TRANSIT: specifying
protocols with concolic snippets (PLDI). 287–296.
Xinyu Wang, Sumit Gulwani, and Rishabh Singh. 2016. FIDEX: Filtering Spreadsheet Data using Examples (OOPSLA). ACM, 195–213.
Navid Yaghmazadeh, Christian Klinger, Isil Dillig, and Swarat Chaudhuri. 2016. Synthesizing Transformations on Hierarchically Structured
Data (PLDI). ACM, 508–521.

PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

1:22

• Xinyu Wang, Isil Dillig, and Rishabh Singh

APPENDIX A: HEURISTIC SCORING FUNCTION
Recall that our synthesis algorithm uses a scoring function θ to choose between multiple programs that satisfy
the input-output examples. The design of the scoring fuction follows the Occam’s razor principle and tries to
favor simpler, more general programs over complex ones.
In more detail, our scoring function assign scores to constants, cell mappers, and predicates in our DSL in a
way that satisfies the following properties:
• A predicate with mapper λc.c has a higher score than the same predicate with other mappers.
• For predicates containing the same mapper χ , we require that the scoring function satisfies the following
constraint:
θ (True) > θ (Val(χ (z)) = ?) > θ (Val(χ (y)) = Val(χ (z))) > θ (Val(χ (z)) = s) = θ (Val(χ (z)) , s)
• θ (ϕ 1 , ··, ϕ n ) takes into account both the scores of each conjunct as well as the number of conjuncts. That
is, θ assigns a higher score to predicates that have conjuncts with higher scores, and assigns lower scores
to predicates with more conjuncts. One design choice satisfying this criterion is to take the average of
scores of all the terms in the conjunct.
• For scores of integer k we have θ (1) > θ (2) > θ (−1) > θ (3) > θ (−2) > θ (−3).
Using the scores assigned to predicates, mappers, and constants, we then assign scores to more complex
programs in the DSL in the following way. The score of a GetCell program is defined by taking into account both
the scores of its arguments and the recursion depth (number of nested GetCell constructs). One possible way to
assign scores to GetCell programs is therefore the following:
θ (GetCell(x, dir, k, λyλz.ϕ)) := θ (k) · θ (ϕ)
θ (τ ) + θ (k) · θ (ϕ)
depth(τ )
depth(x) := 0

θ (GetCell(τ , dir, k, λyλz.ϕ)) :=

depth(GetCell(τ , dir, k, λyλz.ϕ)) := depth(τ ) + 1
The score of a simple program, i.e., List(τ1 , ··, τn ) or Filter(τ1 , τ2 , τ3 , λyλz.ϕ), takes into account of the scores of
its arguments and the number of the arguments. Specifically, it assigns scores in the following way:
θ (τ1 ) + · · +θ (τn )
n
θ (τ1 ) + θ (τ2 ) + θ (τ3 )
θ (Filter(τ1 , τ2 , τ3 , λyλz.ϕ)) :=
3
θ (List(τ1 , ··, τn )) :=

APPENDIX B: PROOF OF SOUNDNESS AND COMPLETENESS
Theorem 11.1. (Soundness and Completeness) Let A be the finite tree automaton constructed by our technique
for example i 7→ L and table T. Then, A accepts the tree that represents a simple program ρ iff JρKT,i = L.

Proof. We first prove soundness – i.e., if A accepts the tree t that represents a simple program ρ, then we
have JρKT,i = L. We show this by inductively proving (call it P) that for any program p whose program tree is a
sub-tree t 0 of t and whose height is at most h, we have
(
L if Root(t 0) = q ∗
JpKT,i =
o if Root(t 0) = qo
The base case for h = 1 trivially holds, since we have p = x, t = qi , t 0 = qi , and JpKT,i = i. For the inductive case,
0 ) and consider t 0 ’s
we want to prove that P holds for any sub-tree t 0 of height h + 1. Suppose t 0 = f ω® (t 10 , ··, tm
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

Synthesis of Data Completion Scripts using Finite Tree Automata

•

1:23

0 . Because a child-tree t 0 is of height at most h, P holds for t 0 according to the inductive
m child-trees t 10 , ··, tm
j
j
hypothesis. Furthermore, we have
(
L if Root(t 0) = q ∗
Jf (o 1 , ··, om , ω)K
® =
o if Root(t 0) = qo

according to the rules in Fig. 13. Therefore, P also holds for any sub-tree t 0 of height h + 1, and for any sub-tree
of height at most h + 1 as well due to the inductive hypothesis.
Now we turn to the proof of completeness – i.e., if there is a simple program ρ that JρKT,i = L, then A accepts
ρ’s program tree t. Consider the evaluation of ρ given input cell i. In each step in which it evaluates a function of
the form f (o 1 , ··, om , ω)
® where we have o j ∈ Cells(T) ∪ {⊥}, there exists a transition in A that goes from states
qo1 , ··, qom to a state that represents the evaluation result with an m-ary function f ω® (according to the rules in
Fig. 13). Therefore, there exists a tree that is accepted by A (according to our construction) and represents simple
program ρ.


APPENDIX C: COMPLEXITY
The complexity of our synthesis algorithm depends on the number of examples n, the number of branches k in
the target program, and the size of the input table (number of cells), m. Specifically, the running time complexity
of the algorithm is O(k n · (m2 )n ). To see where this result comes from, observe that the worst-case complexity
of our FTA construction is O(|∆|), where ∆ is the set of transitions. In our case, |∆| is bound by m 2 because
we can have a transition for each pair of cells. Since the number of examples is n and FTA intersection takes
quadratic time in the size of each FTA, the time to unify n examples is bound by O((m2 )n ). Finally, if the learned
program has k branches, our algorithm searches for k n possible partitions. Thus, an upper bound on the run-time
complexity is O(k n · (m2 )n ). However, in practice, since the constructed FTAs are quite sparse, FTA intersection
does not result in a quadratic blow-up and remains roughly linear. Hence, in practice, the complexity is closer to
O(k n · m2 ). Furthermore, in PBE systems, the user is expected to provide a small number of examples; otherwise,
the technique would be too cumbersome for the user. Therefore, in practice, n is expected to be a small number (at
most 5 in our experiments). Finally, since the target programs typically do not have a large number of branches,
k is also expected to be quite small in practice (at most 3 in our experiments).

APPENDIX D: IN-DEPTH COMPARISON BETWEEN VERSION SPACE ALGEBRAS AND FINITE TREE
AUTOMATA
Let us consider how PROSE would solve the simple synthesis problem from Example 6.4. For simplicity, let us
only consider the DSL shown in Fig. 17. Here, the top-level construct is a cell program τ , which is either the input
cell x, or a GetCell program whose arguments are chosen from a restricted space. Note that GetCell is recursive,
and we assume PROSE allows at most 3 GetCell programs to be nested together.
Fig. 19 shows how PROSE constructs the VSA. Conceptually, PROSE first performs backpropagation of examples
in the unrolled grammar (shown in Fig. 18).11 In particular, given examples of an expression e it deduces examples
of each argument in e using witness functions. In our case, if τ is chosen to be a GetCell program, the example
{(2, 2) 7→ [(1, 2)]} is translated into the example for the first argument τ1 , which is {(2, 2) 7→ [(1, 1)]} ∨ {(2, 2) 7→
Ð
[(1, 2)] ∨ {(2, 2) 7→ [(2, 2)]}, since we have dir,k GetCell−1 ((1, 2), dir, k, λy.λz.True) = {(1, 1), (1, 2), (2, 2)}. This
is shown in Fig. 19 as the three edges from the first level τ to the second level τ1 , where nodes represent the
specifications. PROSE does backpropagation until it reaches the bottom terminals, i.e., x in our case, and constructs
the atomic version spaces for terminal symbols. Then it goes upwards to compose existing version spaces using
VSA operations. For instance, node (2, 2) ⇒ (2, 1) for τ2 represents a version space that composes smaller spaces
11 PROSE

does the unrolling implicitly in its synthesis algorithm.
PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

1:24

• Xinyu Wang, Isil Dillig, and Rishabh Singh

Cell prog. τ
Direction dir
int k

:=
:=
:=

x | GetCell(τ , dir, k, λy.λz.True) ;
u|d|l|r;
−1 | 1 ;

(2,2) => (1,2)

(2,2) => (1,1)

(2,2) => (2,2)

(2,2) => (1,2)

Fig. 17. A simple DSL.
Cell prog. τ
Cell prog. τ1
Cell prog. τ2
Direction dir
int k

:=
:=
:=
:=
:=

x | GetCell(τ1 , dir, k, λy.λz.True) ;
x | GetCell(τ2 , dir, k, λy.λz.True) ;
x | GetCell(x, dir, k, λy.λz.True) ;
u|d|l|r;
−1 | 1 ;

Fig. 18. The unrolled grammar in PROSE.

(2,2) => (1,1)

(2,2) => (1,1)

(2,2) => (1,2)

(2,2) => (1,2)

(2,2) => (2,1)

(2,2) => (2,1)

(2,2) => (2,2)

Fig. 19. Part of the VSA in PROSE.

using Union operation. As we can see, nodes that represent examples for τ , τ1 and τ2 are duplicated, even though
they are unrolled from the same symbol τ in the original grammar.
In contrast, our FTA technique does not require unrolling, and thus
(1,1)
(1,2)
(2,1)
(2,2)
has the potential to create fewer states and lead to a more compact
representation. Fig. 20 shows conceptually how the FTA technique
works for the same example. In Fig. 20, nodes represent states in the
(2,1)
(2,2)
(1,1)
(1,2)
FTA and edges represent transitions. Our technique starts from the
input example, i.e., (2, 2), computes the reachable values using the
Fig. 20. Part of the FTA in DACE.
GetCell construct, and creates transitions from the input value to the
output values. It does so until all possible transitions are added. As we
can see, our technique performs FTA construction in a forward manner, and hence it does not require inverse
semantics. Furthermore, it does not require unrolling and results in a more compact FTA representation in this
example.

PACM Progr. Lang., Vol. 1, No. 1, Article 1. Publication date: January 2017.

