# Searching Entangled Program Spaces

James Koppel  MITCambridgeMAUSA<EMAIL_ADDRESS>,  Zheng Guo  UC San DiegoLa
JollaCAUSA<EMAIL_ADDRESS>,  Edsko de Vries  Well-Typed LLPUnited Kingdom
<EMAIL_ADDRESS>,  Armando Solar-Lezama  MITCambridgeMAUSA
<EMAIL_ADDRESS>and  Nadia Polikarpova  UC San DiegoLa JollaCAUSA
<EMAIL_ADDRESS>
###### Abstract.

Many problem domains, including program synthesis and rewrite-based
optimization, require searching astronomically large spaces of programs.
Existing approaches often rely on building specialized data
structures—version-space algebras, finite tree automata, or e-graphs—to
compactly represent such spaces. At their core, all these data structures
exploit independence of subterms; as a result, they cannot efficiently
represent more complex program spaces, where the choices of subterms are
entangled.

We introduce _equality-constrained tree automata_ (ECTAs), a new data
structure, designed to compactly represent large spaces of programs with
entangled subterms. We present efficient algorithms for extracting programs
from ECTAs, implemented in a performant Haskell library, ecta. Using the ecta
library, we construct Hectare, a type-driven program synthesizer for Haskell.
Hectare significantly outperforms a state-of-the-art synthesizer
Hoogle+—providing an average speedup of $8\times$—despite its implementation
being an order of magnitude smaller.

††journal: PACMPL††journalnumber: ICFP††journalyear: 2022††copyright:
rightsretained

##  1\. Introduction

From program synthesis to theorem proving and compiler optimizations, a range
of problem domains make use of data structures that compactly represent large
spaces of terms. In program synthesis, the most well-known example is _version
space algebras_ (VSAs) (Lau et al., 2003; Polozov and Gulwani, 2015), the data
structure behind the successful spreadsheet-by-example tool FlashFill
(Gulwani, 2011). Although there may be over $10^{100}$ programs matching an
input/output example, FlashFill is able to represent all of them as a tiny
VSA, efficiently run functions over every program in the space, and then
extract the best concrete solution.

To illustrate the idea behind VSAs, consider the space of nine terms
$\mathcal{T}=\\{\mathsf{f}(t_{1})+\mathsf{f}(t_{2})\\}$ where
$t_{1},t_{2}\in\\{\mathsf{a},\mathsf{b},\mathsf{c}\\}$. 1(a) shows a VSA that
represents this space. In a VSA a _union node_ , marked with $\cup$,
represents a union of all its children, while a _join node_ , marked with
$\bowtie$, applies a function symbol to every combination of terms represented
by its children. You can see how, by exploiting the shared top-level structure
of the terms in $\mathcal{T}$, this VSA is able to compactly represent nine
terms, each of size five, using only six nodes.

Another data structure that exploits sharing in a similar way is _e-graphs_ ,
which enjoy a wide range of applications, including theorem proving (de Moura
and Bjørner, 2007), rewrite-based optimization (Tate et al., 2009), domain-
specific synthesis (Nandi et al., 2020, 2021), and semantic code search
(Premtoon et al., 2020). Both VSAs and e-graphs are now known (Pollock and
Haan, 2021; Koppel, 2021) to be equivalent to special cases of _finite tree
automata_ (FTAs), which have independently experienced a surge of interest in
recent years (Adams and Might, 2017; Wang et al., 2017, 2018). 1(b) shows an
FTA that represents the same term space as the VSA in 1(a). An FTA consists of
_states_ (circles) and _transitions_ (rectangles), with each transition
connecting zero or more states to a single state. Intuitively, FTA transitions
correspond to VSA’s join nodes, and FTA states correspond to VSA’s union nodes
(although in a VSA, union nodes with a single child are omitted). Importantly,
all three data structures111We omit e-graphs from Fig. 1 for space reasons,
but also because e-graphs are typically used to represent congruence relations
rather than arbitrary sets of terms, which makes them less relevant to our
setting, as we discuss in §8. thrive on spaces where terms share some top-
level structure, while their divergent sub-terms can be chosen _independently_
of each other.

(a) VSA for $\mathcal{T}$

(b) FTA for $\mathcal{T}$

(c) VSA for $\mathcal{U}$

(d) ECTA for $\mathcal{U}$

Figure 1. Representations of
$\mathcal{T}=\\{\mathsf{f}(t_{1})+\mathsf{f}(t_{2})\\}$ and
$\mathcal{U}=\\{\mathsf{f}(t)+\mathsf{f}(t)\\}$, where
$t,t_{1},t_{2}\in\\{\mathsf{a},\mathsf{b},\mathsf{c}\\}$.

_Challenge: Dependent Joins._ Consider now the term space
$\mathcal{U}=\\{\mathsf{f}(t)+\mathsf{f}(t)\\}$, where
$t\in\\{\mathsf{a},\mathsf{b},\mathsf{c}\\}$, that is, a sub-space of
$\mathcal{T}$ where both arguments to $\mathsf{f}$ _must be the same term_.
Such “entangled” term spaces arise naturally in many domains. For example, in
term rewriting or logic programming, we might want to represent the subset of
$\mathcal{T}$ that matches the non-linear pattern $X+X$. Similarly, in type-
driven API search (Mitchell, 2004; Gissurarson, 2018), we might want to
represent the space of all _types_ of library functions that unify with a
given query type, such as
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{List}}}}}}\
\alpha\to\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{List}}}}}}\
\alpha$.

Existing data structures are incapable of fully exploiting shared structure in
such entangled spaces. 1(c) shows a VSA representing $\mathcal{U}$: here, the
node $+_{\bowtie}$ cannot be reused because VSA joins are _independent_ ,
whereas our example requires a dependency between the two children of $+$.
This limitation is well-known: for example, the seminal work on VSAs (Lau et
al., 2003) notes that “efficient representation of non-independent joins
remains an item for future work.”

_Solution: ECTA._ To address this limitation, we propose a new data structure
we dub _equality-constrained tree automata_ (ECTAs). ECTAs are tree automata
whose transitions can be annotated with _equality constraints_.222This might
remind some readers of Dauchet’s _reduction automata_ ; we postpone a detailed
comparison to related work (§8). For example, 1(d) shows an ECTA that
represents the term space $\mathcal{U}$. It is identical to the FTA in 1(b)
save for the constraint $0.0=1.0$ on its $+$ transition. This constraint
restricts the set of terms accepted by the automaton to those where the sub-
term at path $0.0$ (the first child of the first child of $+$) equals the sub-
term at path $1.0$ (the first child of the second child of $+$). The
constraint enables this ECTA to represent a dependent join while still fully
exploiting shared structure, unlike the VSA in 1(c).

_Challenge: Enumeration._ Being able to represent a term space is not
particularly useful unless we also can efficiently _extract_ a concrete
inhabitant of this space—or, more generally, _enumerate_ some number of its
inhabitants. Unsurprisingly, equality constraints make enumeration harder,
since the terms must now comply with those constraints (in fact, as we
demonstrate in §6.1, extracting a term for an ECTA is at least as hard as SAT
solving). A naïve fix is to filter out spurious (constraint-violating) terms
after the fact, but such “rejection sampling” can be extremely inefficient.

_Solution: Dynamic and Static Reduction._ Our first insight for how to speed
up enumeration is inspired by constraint-based type inference. Instead of
making an _eager_ choice at a constrained state, such as $q_{1}$ in 1(d), our
enumeration technique _postpones_ this choice, instead introducing a
“unification variable” $V_{1}$ to stand for the chosen term. This variable
gets reused the second time $q_{1}$ is visited. At the end, $V_{1}$ is reified
into a concrete term, thereby making a simultaneous choice at the two
constrained states, which is guaranteed by construction to satisfy all
equality constraints. We dub this mechanism _dynamic reduction_ , where
“dynamic” refers to operating during the enumeration process. As we illustrate
in §2, dynamic reduction becomes more involved when equality constraints
relate different states: in that case the term space associated with a
unification variable gets refined during enumeration.

Our second insight is that enumeration can often be made even more efficient
by transforming the ECTA _statically_ —that is, before the enumeration
starts—so that some of its constraints are “folded” into the structure of the
underlying FTA. We will present examples in §2 of using static reduction to
“prune” away states that cannot be part of any term that satisfies the
constraints.

_Contributions._ In summary, this paper makes the following contributions:

  1. (1)

We introduce the _ECTA data structure_ (§3), which supports compact
representation of program spaces with dependent joins, as well as efficient
enumeration (§4) via _static_ and _dynamic reduction_. We first formalize the
simpler acyclic ECTAs, and then show how to add cycles in order to support
infinite term spaces (§5).

  2. (2)

We develop _ECTA encodings_ for two diverse domains: Boolean satisfiability
and type-driven program synthesis (§6). These encodings illustrate that ECTAs
are expressive and versatile, and that ECTA enumeration can effectively be
used as a general-purpose constraint solver.

  3. (3)

We implement the data structure and its operations in a performant Haskell
library, ecta.

We evaluate the ecta library on the domain of type-driven program synthesis
(§7). The experiments show that our ECTA-based synthesizer Hectare
significantly outperforms its state-of-the-art competitor Hoogle+ (Guo et al.,
2020), despite our implementation being _only a tenth of the size_.
Specifically, Hectare is able to solve 88% of synthesis problems in the
combined benchmark suite compared to only 64% by Hoogle+, and on commonly
solved benchmarks Hectare is _$8\times$ faster_ on average. Further, our
evaluation demonstrates that static and dynamic reduction are critical for
performance: ablating either of those mechanisms reduces the number of
benchmarks solved, while a naïve baseline that uses “rejection sampling”
enumeration is unable to solve _any_ benchmarks.

##  2\. ECTA by Example

In this section we illustrate the ECTA data structure and its two major
features—static and dynamic reduction—using the problem of type-driven program
synthesis as a motivating example. We give a simple encoding of the space of
well-typed small programs into ECTAs, and then show how the _general-purpose
ECTA operations_ are used to efficiently enumerate the well-typed terms. We
will present the full encoding, which also handles arbitrary polymorphism and
higher-order functions, in §6, along an with ECTA encoding of another problem
domain.

###  2.1. Representing Spaces of Well-typed Terms

(a) Initial ECTA.

(b) Reduced ECTA.

Figure 2. ECTAs representing all well-typed size-two terms in the environment
$\Gamma_{1}$.

Consider a typing environment
${{{{{{{{\Gamma_{1}=\\{x:\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}},y:\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Char}}}}}},f:\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Bool}}}}}}\to\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Bool}}}}}},g:\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}}\to\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Bool}}}}}},h:\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Char}}}}}}\to\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}}\\}$.
Suppose we are interested in enumerating all application terms that are well-
typed in $\Gamma_{1}$; for now let us restrict our attention to terms of size
two—that is, applications of variables to variables. The space of all such
terms can be compactly represented with an ECTA, as shown in 2(a).

This ECTA has a _transition_ for each variable in $\Gamma_{1}$; scalar
variables ($x$ and $y$) are annotated with their type, while functions ($f$,
$g$, and $h$) are annotated with an argument type targ and a return type tret.
The _node_ (state) unary represents the space of all unary variables, while
the node scalar represents the space of all scalars. The accepting node has a
single incoming transition app, which represents an application of a unary fun
to a scalar arg, fulfilling the restriction to size-two terms.333In our full
encoding in §6 we remove the distinction between the terms of different arity
in order to support higher-order and partial applications.

While the underlying tree automaton of this ECTA (its _skeleton_) accepts all
terms of the form $A\ B$ where $A\in\\{f,g,h\\}$ and $B\in\\{x,y\\}$; most of
these terms, such as $f\ x$ are ill-typed. In order to restrict the set of
represented terms to only well-typed ones, there is an _equality constraint_
fun.targ = arg.type attached to the app transition, which demands that the
types of the formal and the actual arguments coincide. Thanks to this
constraint, the full ECTA accepts only the two well-typed terms, $g\ x$ and
$h\ y$. (Note that in this presentation, we give names to the incoming edges
of each transition to make the constraints more readable; in the
formalization, we instead use indices to refer to the edges.)

###  2.2. Static Reduction

How would one go about enumerating the terms represented by the ECTA in 2(a)?
A naïve approach is to  (1) enumerate all terms represented by its skeleton
and  (2) filter out those terms that violate the constraint.  Step 1 is easily
accomplished via depth-first search, starting from the root (the accepting
node) and picking a single incoming transition for every node. This approach
is, however, inefficient: it ends up constructing six terms, only to filter
out four of them. In ECTA terminology, the skeleton admits six _runs_ , four
of which are _spurious_ (violate the constraints).

Our first key insight is that enumeration can often be made more efficient by
transforming the ECTA’s skeleton so as to reduce the number of spurious runs.
We refer to this transformation as _static reduction_ (because it happens
once, _before_ the enumeration starts). The reduced ECTA for our example is
given in 2(b). Intuitively, we were able to eliminate the $f$ transition
entirely because there are no scalar variables that match its formal argument
type Bool; as a result the reduced ECTA contains only two spurious runs
instead of four.

More formally, static reduction works via automata _intersection_. For the
ECTA in 2(a), reducing the constraint fun.targ = arg.type involves
constructing an automaton that accepts all terms reachable via the path
arg.type—namely Int and Char—and intersecting it with each node at the path
fun.targ. Since the child node of f labeled targ represents only Bool, the
intersection for that child is empty, meaning the f transition can never be
used to satisfy the constraint, and hence can be eliminated. The reduction
algorithm performs a similar intersection for g and h, as well as (in the
other direction) x and y, but finds that each of these other choices could be
part of a satisfying run, and eliminates no further transitions.

###  2.3. Type-Driven Program Synthesis with ECTAs

Figure 3. ECTAs representing size-two terms of type Bool. The diagram on the
right shows how a sequence of static reductions on the constraints
\raisebox{-.9pt} {1}⃝, \raisebox{-.9pt} {2}⃝, and \raisebox{-.9pt} {3}⃝
eliminates the grayed-out transitions and nodes.

In type-driven program synthesis, we are typically not interested in all well-
typed terms, but rather terms of a given _query_ type. The ECTA in Fig. 3
(left) represents a type-driven synthesis problem with the same environment
$\Gamma_{1}$ as before and query type Bool. The main difference between this
automaton and the one in 2(b) is the new transition query, whose type edge
encodes the given query type and whose term edge connects to the node
representing all well-typed terms in the search space. To filter out the terms
of undesired types, constraint \raisebox{-.9pt} {1}⃝ prescribes that the
term’s type be equal to the query type. In order for this constraint to make
sense, we also add a type annotation to the app transition; the type of an
application is initially undetermined (can be any base type), but is
restricted by a new constraint \raisebox{-.9pt} {2}⃝ to coincide with the
return type of the function.

Fig. 3 (right) demonstrates a sequence of static reductions that happens to
eliminate _all_ spurious run of this ECTA, until its skeleton represents the
sole solution to the synthesis problem: the term $g\ x$. First, reducing
constraint \raisebox{-.9pt} {1}⃝ eliminates all possible types of the
application except Bool; next, reducing \raisebox{-.9pt} {2}⃝ eliminates the
function $h$ as it has a wrong return type; finally, reducing \raisebox{-.9pt}
{3}⃝ eliminates the argument $y$, since it is incompatible with the only
remaining function $g$.

###  2.4. Dynamic Reduction

In the previous example, static reduction was able to eliminate all spurious
runs of the ECTA before enumeration. so that no spurious runs remained. This
is not always possible. Consider a slightly more involved version of type-
driven synthesis where functions can be polymorphic. Specifically let
${{{{\Gamma_{2}=\\{x:\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}},y:\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Char}}}}}},g:\forall\alpha.\alpha\to\alpha,h:\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Char}}}}}}\to\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Bool}}}}}}\\}$,
and suppose we are interested in all size-two terms of types Int or Bool. This
problem can be represented by the ECTA in Fig. 4, which is similar to the one
in Fig. 3. The only interesting difference is how the polymorphic type of $g$
is represented: the type variable $\alpha$ is encoded as a _union_ of all
types it can unify with—here Bool, Char, and Int.444Here we consider a limited
form of polymorphism, where type variables can be instantiated only with base
types; this restriction is relaxed in §6. Crucially, the constraint
\raisebox{-.9pt} {4}⃝ on $g$ guarantees that _the same_ type is used to
instantiate both occurrences of $\alpha$.

Figure 4. Type-driven synthesis with polymorphic functions. Left: ECTA
representing all terms of types Bool or Int in $\Gamma_{2}$. Grayed-out
transitions are eliminated by static reduction. Right: Intermediate state
during enumeration. The choice of the query type has been suspended into an
auxiliary automaton $V_{1}$.

Although static reduction can eliminate some of the transitions in this ECTA
(shown in gray), a fair number of spurious runs remain. For example, a naïve
left-to-right enumeration would first pick Bool as the query type and $g$ as
the function (forcing the selection of
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Bool}}}}}}\to\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Bool}}}}}}$
as the type of $g$), only to discover later that there is no argument of type
Bool. More generally, in the presence of constraints, the choices made for
constrained nodes are not independent, and making a wrong combination of
choices early on (such as Bool and $g$ in our example) may lead to expensive
backtracking further down the line.

Our second key insight is that such backtracking can be avoided by _deferring_
the enumeration of constrained nodes until more information is available. Fig.
4 (right) illustrates this idea. It depicts a _partially enumerated_ term from
the ECTA on the left. You can think of a partially enumerated term as a tree
fragment at the top with yet-to-be-enumerated ECTAs among the branches.
Importantly, because the node qtype is constrained (by \raisebox{-.9pt} {1}⃝),
it is not enumerated eagerly, but instead _suspended_ into a named sub-
automaton $V_{1}$. As the enumeration encounters each other node $N$
constrained to be equal to qtype (via \raisebox{-.9pt} {1}⃝, \raisebox{-.9pt}
{2}⃝, and \raisebox{-.9pt} {4}⃝), $n$ is replaced by a reference to $V_{1}$,
while $V_{1}$ is updated to $V_{1}\sqcap N$. Thus, to arrive at Fig. 4
(right), the enumeration has made a single decision—picking $g$ over
$h$—whereas all the other choices have been deferred.

Finally, the enumeration picks $x$ among the two scalars. The type state of
$x$—let’s call it $N_{x}$—represent a singleton
${\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}}\\}$
_and_ is constrained to equal $V_{1}$ (by \raisebox{-.9pt} {3}⃝). As a result,
$V_{1}$ gets intersected with $N_{x}$, eliminating its Bool alternative. Now
when it comes time to “unsuspend” $V_{1}$, it only contains a single
alternative, Int, which is already guaranteed to be consistent with all
constraints. In other words, we have found the solution $g\ x$555The only
other solution to this synthesis problem is $h\ y$, which is discovered after
backtracking and picking $h$ over $g$. without having to explicitly search
over all possible query types, result types of the application, or
instantiations of $g$; instead all these three choices were made
simultaneously and consistency. We refer to this mechanism as _dynamic
reduction_ because it reduces the number of explored spurious runs _during_
enumeration.

##  3\. Acyclic ECTA

This section formalizes the ECTA data structure and its core algorithms. We
begin by presenting the special case of ECTAs without cycles, which simplifies
both the theory and implementation. Proofs of all theorems omitted from this
and the following sections can be found in App. A.

###  3.1. Preliminaries

We first present standard definitions of terms, paths, and the prefix-free
property from the term-rewriting literature.

_Terms._ A _signature_ $\Sigma$ is a set of function symbols, each associated
with a natural number by the $\mathsf{arity}$ function. $\mathcal{T}(\Sigma)$
denotes the set of _terms_ over $\Sigma$, defined as the smallest set
containing all $s(t_{0},\dots,t_{k-1})$ where $s\in\Sigma$,
$k=\mathsf{arity}(s)$, and $t_{0},\dots,t_{k-1}\in\mathcal{T}(\Sigma)$. We
abbreviate nullary terms of the form $s()$ as $s$.

_Paths._ Paths are used to denote locations inside terms. Formally, a _path_
$p$ is a list of natural numbers $i_{1}.i_{2}.\dots.i_{k}\in\mathbb{N}^{*}$.
The empty path is denoted $\epsilon$, and $p_{1}.p_{2}$ denotes the
concatenation of paths $p_{1}$ and $p_{2}$. We write $p_{1}\sqsubseteq p_{2}$
if $p_{1}$ is a prefix of $p_{2}$ (and $p_{1}\sqsubset p_{2}$ if it is a
proper prefix). A set $P$ of paths is _prefix-free_ if there are no
$p_{1},p_{2}\in P$ such that $p_{1}\sqsubset p_{2}$.

Given a term $t\in\mathcal{T}(\Sigma)$, a _subterm of $t$ at path $p$_,
written $t|_{p}$, is inductively defined as follows:  (i) $t|_{\epsilon}=t$
(ii) $s(t_{0},\dots,t_{k-1})|_{i.p}=t_{i}|_{p}$if $i<k$ and $\bot$ otherwise.
For example, for $t=+(f(a),f(b))$: $t|_{0.0}=a$, $t|_{1.0}=b$ and
$t|_{2.0}=\bot$.

###  3.2. Path Constraints and Consistency

The difference between ECTAs and conventional tree automata is the presence of
path equalities, such as $0.0=1.0$ in 1(d). We now formalize the semantics of
these path equalities over terms, before using them to define the ECTA data
structure. In the following, we are interested in equalities between an
arbitrary number $n>0$ of paths rather than just two paths; we refer to such
$n$-ary constraints as _path equivalences classes_ (PECs).

###### Definition 3.1 (Path Equivalence Classes).

A _path equivalence class_ (PEC) $c$, is a set of paths. We write a PEC
$\\{p_{1},p_{2},\dots,p_{n}\\}$ as $\\{p_{1}=p_{2}=\dots=p_{n}\\}$.

Intuitively, the constraint $0.0=1.0$ is satisfied on a term $t$ if
$t|_{0.0}=t|_{1.0}$; this notion generalizes straightforwardly to non-binary
PECs:

###### Definition 3.2 (Satisfaction of a PEC, Value at a PEC).

A path equivalence class $c=\\{p_{1}=\dots=p_{n}\\}$ is _satisfied_ on a term
$t$ if there is some $t^{\prime}$ such that, $\forall p_{i}\in
c,t|_{p_{i}}=t^{\prime}$. We write $t\models c$ if this condition holds, and
$t|_{c}$ to denote this unique $t^{\prime}$.

Finally, we discuss sets of PECs, called path constraint sets (PCSs):

###### Definition 3.3 (Path Constraint Sets, Satisfaction, Consistency).

A _path constraint set_ $C=\\{c_{1},\dots,c_{m}\\}$ is a set of disjoint path
equivalence classes.666Any set of PECs can be _normalized_ into a PCS by
merging non-disjoint PECs; for example, the set $\\{\\{0=1\\},\\{1=2\\}\\}$
can be normalized into $\\{\\{0=1=2\\}\\}$. In the following, we assume that
the results of all PCS operations (_e.g._ $C_{1}\cup C_{2}$) are always
implicitly normalized. A term $t$ satisfies $C$, written $t\models C$, if
$\forall c\in C,t\models c$. If there exists a $t$ such that $t\models C$,
then $C$ is _consistent_ ; otherwise, it is _inconsistent_.

We are interested in detecting inconsistent PCSs because ECTA operations can
use this property to prune empty subautomata. For a single PEC $c$,
consistency is rather straightforward: $c$ is consistent iff it is prefix-
free.777Technically, we must also ensure that $\forall i\in
c.i<\max_{s\in\Sigma}\mathsf{arity}(s)$, but this is trivially maintained by
all ECTA operations. A non-prefix-free PEC, such as $1.0.0=1$, requires a term
to be equal to its subterm, which is impossible since terms are finite trees.
For a PCS, however, the story is more complicated: in particular, it is not
sufficient that each of its member PECs is prefix-free, because two PECs may
reference subterms of each other. For example, consider the PCS
$C=\\{c_{1},c_{2}\\}=\\{\\{0=1.0\\},\\{0.0=1\\}\\}$. Although $c_{1}$ and
$c_{2}$ are prefix-free, together they imply an inconsistent constraint
$1.0.0=1$, which can be obtained by substituting $1.0$ for $0$ in $c_{2}$, as
justified by $c_{1}$.

For more intuition, consider two patterns $f(A,g(A))$ and $f(g(B),B)$; it is
easy to see that the terms matching these patterns satisfy the PECs $c_{1}$
and $c_{2}$, respectively. The conjunction of the two PECs corresponds to the
unification of the two patterns, which produces unification constraints
$A=g(B)$ and $g(A)=B$, and eventually the contradictory constraint
$B=g(g(B))$—which corresponds exactly to the $1=1.0.0$ PEC above. In
unification parlance, we say that this constraint fails an _occurs check_.
Checking consistency of a PCS is the name-free analogue of the occurs check.

_Checking Consistency via Congruence Closure._ These observations suggest an
algorithm for checking PCS consistency:  (1) saturate the PCS with all implied
equalities (such as $1.0.0=1$ above), and  (2) check if any of them is non-
prefix-free.  To formalize the former step, we first declaratively define the
_closure_ operation on PCSs, and then discuss how to implement it efficiently.

###### Definition 3.4 (Closure).

A PCS $C$ is _closed_ if the following holds for any $c_{1},c_{2}\in C$: for
any paths $p,p^{\prime},p^{\prime\prime}$, if $p^{\prime},p^{\prime\prime}\in
c_{1}$ and $p^{\prime}.p\in c_{2}$, then $p^{\prime\prime}.p\in c_{2}$. In
other words, whenever $c_{2}$ contains an extension of a path in $c_{1}$, it
also contains the same extension of _all_ paths in $c_{1}$. The _closure_ of
$C$, denoted $\mathsf{cl}(C)$, is the smallest closed PCS that contains $C$.

For example, the PCS $C=\\{c_{1},c_{2}\\}=\\{\\{0=1.0\\},\\{0.0=1\\}\\}$ is
not closed: if we set $p^{\prime}=0,p^{\prime\prime}=1.0$, and $p=0$, then
$0\in c_{1}$, $1.0\in c_{1}$, and $0.0\in c_{2}$, but $1.0.0\notin c_{2}$. The
closure of this PCS $\mathsf{cl}(C)=\\{c^{\prime}_{1},c^{\prime}_{2}\\}$,
where $c^{\prime}_{1}$ and $c^{\prime}_{2}$ are infinite PECs of the form
$c^{\prime}_{1}=\\{0=1.0=0.0.0=1.0.0.0=\ldots\\}$ and
$c^{\prime}_{2}=\\{1=0.0=1.0.0=0.0.0.0=\ldots\\}$.

###### Theorem 3.5 (Correctness of Closure).

For any term $t\in\mathcal{T}(\Sigma)$, $t\models C\Leftrightarrow
t\models\mathsf{cl}(C)$.

###### Theorem 3.6 (Consistency of a Closed PCS).

Let $C$ be a closed PCS. Then $C$ is inconsistent iff one of the $c_{i}\in C$
is not prefix-free.

Together Theorem 3.5 and Theorem 3.6 ensure the correctness of our consistency
checking procedure; what is left is to implement the closure computation
efficiently. It turns out this can be done using the well-known congruence
closure algorithm for the first-order theory of equality and uninterpreted
functions (Nelson and Oppen, 1980). This algorithm finitely represents a
possibly infinite set of equalities using an e-graph. Hence, to check
consistency of a PCS $C$, we can simply  (1) add each path of $C$ into an
e-graph, interpreting path prefixes as subterms (_i.e._ $1.0$ is $.0$ applied
to $1$);  (2) merge all paths from the same PEC into one e-class and run
congruence closure on the e-graph;  (3) check if the resulting e-graph has
cycles; if so, then $C$ is inconsistent.  The figure on the right shows the
(cyclic) e-graph obtained by running this algorithm on our example
$\\{\\{0=1.0\\},\\{0.0=1\\}\\}$.

###  3.3. Acyclic ECTAs: Core Definition

Syntax

$\begin{array}[]{rll}c\mathrel{\mathord{:}\mathord{:=}}&\\{p_{1}=\dots=p_{n}\\}&\text{path
equivalence classes}\\\
C\mathrel{\mathord{:}\mathord{:=}}&\\{c_{1},\dots,c_{m}\\}&\text{path
constraint sets}\\\
n\mathrel{\mathord{:}\mathord{:=}}&\bm{\mathtt{U}}(\overline{e})&\text{nodes
(states)}\\\
e\mathrel{\mathord{:}\mathord{:=}}&\bm{\Pi}(s,\overline{n},C)\mid\bm{\Pi}_{\bot}&\text{transitions}\\\
\end{array}$

Denotation

$\begin{array}[]{rl}\\\ \\\
\llbracket\bm{\mathtt{U}}(\overline{e})\rrbracket^{N}&=\bigcup_{i}\llbracket
e^{i}\rrbracket^{E}\\\
\llbracket\bm{\Pi}(s,\overline{n},C)\rrbracket^{E}&=\left\\{s(\overline{t})\mathrel{\Big{|}}t^{i}\in\llbracket
n^{i}\rrbracket^{N},s(\overline{t})\models C\right\\}\end{array}$

Figure 5. Acyclic ECTAs: syntax and semantics. Here $s\in\Sigma$ and $p$ is a
path.

Like string automata, tree automata are usually formalized as graphs, defined
by a set of states and a transition function. For our purposes, it is more
convenient to formalize ECTAs using a recursive grammar, in the same style
VSAs are typically presented (Polozov and Gulwani, 2015).

_Syntax._ Fig. 5 (left) shows the grammar for acyclic ECTAs, consisting of
mutually recursive definitions for nodes (states) $n\in N$ and transitions
$e\in E$; an ECTA then is identified with its root node, which represents the
final state.888Although this representation is restricted to ECTAs with a
single final state (the root node), this is not an important restriction: any
acyclic tree automaton is equivalent to the same automaton with all its final
states merged into one. In a transition
$\bm{\Pi}(s,\overline{n},C)$,999Hereafter we write $\overline{x}$ to denote a
sequence of $x$s, with $x^{i}$ referring to the $i$-th element of that
sequence. the number of child nodes $|\overline{n}|$ must equal
$\mathsf{arity}(s)$; both $\overline{n}$ and $C$ can be omitted when empty. As
is common for VSAs, we assume implicit sharing of sub-trees: that is, an
acyclic ECTA is a DAG with no duplicate sub-graphs.

The special symbol $\bm{\Pi}_{\bot}$denotes an “empty transition”, which is
used in intermediate results of ECTA operations. For symmetry, we also
abbreviate the empty node, $\bm{\mathtt{U}}()$, as $\bm{\mathtt{U}}_{\bot}$. A
_normalized_ ECTA contains no occurrences of $\bm{\Pi}_{\bot}$or
$\bm{\mathtt{U}}_{\bot}$, unless the root is itself $\bm{\mathtt{U}}_{\bot}$.
Any ECTA can be normalized by iteratively replacing any transition containing
a $\bm{\mathtt{U}}_{\bot}$child with $\bm{\Pi}_{\bot}$, and removing all
instances of $\bm{\Pi}_{\bot}$from the children of each node. For instance,
$\bm{\mathtt{U}}(\bm{\Pi}(\mathsf{a}),\bm{\Pi}(+,[\bm{\mathtt{U}}(\bm{\Pi}(\mathsf{b})),\bm{\mathtt{U}}_{\bot}]))$
normalizes to $\bm{\mathtt{U}}(\bm{\Pi}(\mathsf{a})))$. We assume henceforth
that all ECTAs are implicitly normalized after every operation.

_Semantics and Spurious Runs._ The _denotation_ of an acyclic ECTA, _i.e._ the
set of terms it accepts, is defined in Fig. 5 (right) as a pair of mutually-
recursive functions: $\llbracket\cdot\rrbracket^{N}\colon
N\to\mathbb{P}(\mathcal{T}(\Sigma))$ and $\llbracket\cdot\rrbracket^{E}\colon
E\to\mathbb{P}(\mathcal{T}(\Sigma))$. We define a partial order $\prec$ on
ECTAs as the subset order on their denotations: $n_{1}\prec n_{2}$ iff
$\llbracket n_{1}\rrbracket^{N}\subseteq\llbracket n_{2}\rrbracket^{N}$. The
_skeleton_ of an ECTA, $\mathsf{sk}(n)$, is obtained by recursively removing
all path constraints from its transitions. A _spurious run_ of $n$ is a term
$t$, that is rejected by $n$ but accepted by its skeleton: $t\notin\llbracket
n\rrbracket^{N}\wedge t\in\llbracket\mathsf{sk}(n)\rrbracket^{N}$.

###  3.4. Basic Operation: Union and Intersection

We now present algorithms for two basic operations on ECTAs, union and
intersection. They serve as building blocks for our two core contributions:
static and dynamic reduction.

_Union._ The union of two ECTAs, $n_{1}\sqcup n_{2}$, simply merges the
transition of their root nodes:

###### Definition 3.7 (Union).

Let
$n_{1}=\bm{\mathtt{U}}(\overline{e_{1}}),n_{2}=\bm{\mathtt{U}}(\overline{e_{2}})$
be two nodes. Then $n_{1}\sqcup
n_{2}=\bm{\mathtt{U}}(\overline{e_{1}}\cup\overline{e_{2}})$.

Fig. 6 gives an example of ECTA union $n_{u}=n_{1}\sqcup n_{2}$.

###### Theorem 3.8 (Correctness of ECTA Union).

$\llbracket n_{1}\sqcup n_{2}\rrbracket^{N}=\llbracket
n_{1}\rrbracket^{N}\cup\llbracket n_{2}\rrbracket^{N}$.

_Intersection._ The intersection of two ECTAs is more involved. Intersecting
two nodes, $n_{1}\sqcap n_{2}$, involves intersecting all pairs of their
transitions; intersecting two transitions, $e_{1}\sqcap e_{2}$, in turn,
involves intersecting their child nodes point-wise, and is only well-defined
if the symbols and PCSs of $e_{1}$ and $e_{2}$ are compatible:

###### Definition 3.9 (Intersection).

Let
$n_{1}=\bm{\mathtt{U}}(\overline{e_{1}}),n_{2}=\bm{\mathtt{U}}(\overline{e_{2}})$
be two nodes, then:

$n_{1}\sqcap n_{2}=\bm{\mathtt{U}}\left(\left\\{e_{1}^{i}\sqcap
e_{2}^{j}\mathrel{\Big{|}}e_{1}^{i}\in\overline{e_{1}},e_{2}^{j}\in\overline{e_{2}}\right\\}\right)$

Let $e_{1}=\bm{\Pi}(s_{1},[n_{1}^{0}\dots n_{1}^{k-1}],C_{1})$,
$e_{2}=\bm{\Pi}(s_{2},[n_{2}^{0}\dots n_{2}^{l-1}],C_{2})$ be two transitions,
then:

$e_{1}\sqcap e_{2}=\begin{cases}\bm{\Pi}(s_{1},[n_{1}^{0}\sqcap
n_{2}^{0},\dots,n_{1}^{k-1}\sqcap n_{2}^{k-1}],C_{1}\cup C_{2})&\text{if}\
s_{1}=s_{2}\ \text{and}\ C_{1}\cup C_{2}\ \text{is consistent}\\\
\bm{\Pi}_{\bot}&\text{otherwise}\end{cases}$

Consider the example of ECTA intersection $n_{i}=n_{1}\sqcap n_{2}$ in Fig. 6.
To compute the intersection at the top level, we intersect all pairs of
transitions—$(f,g)$, $(f,h)$, $(g,g)$, and $(g,h)$—but the three pairs with
incompatible function symbols simpy yield $\bm{\Pi}_{\bot}$ and are discarded.
To intersect the two $g$-transitions, we recursively intersect their targ and
tret nodes; the resulting $g$-transition also inherits its constraint from
$n_{2}$.

###### Theorem 3.10 (Correctness of ECTA Intersection).

$\llbracket n_{1}\sqcap n_{2}\rrbracket^{N}=\llbracket
n_{1}\rrbracket^{N}\cap\llbracket n_{2}\rrbracket^{N}$.

###### Proposition 3.11.

$\bm{\mathtt{U}}_{\bot}\sqcap
n=n\sqcap\bm{\mathtt{U}}_{\bot}=\bm{\mathtt{U}}_{\bot}$

###### Corollary 3.12.

Define $n_{1}\cong n_{2}$ if $\llbracket n_{1}\rrbracket^{N}=\llbracket
n_{2}\rrbracket^{N}$. Then, with respect to $(\cong)$, the $(\sqcap)$ and
$(\sqcup)$ operations form a distributive lattice, with
$\bm{\mathtt{U}}_{\bot}$ as the bottom element, and $(\prec)$ as the order.

Figure 6. Two ECTAs $n_{1}$ and $n_{2}$, their union $n_{u}$ and intersection
$n_{i}$.

###  3.5. Static Reduction

We are now ready to present static reduction, the first of the two core
algorithms that enable efficient extraction of terms satisfying ECTA
constraints. Consider the example in Fig. 2. Intuitively, the constraint
fun.targ = arg.type has been _reduced_ in 2(b), because with $f$ elimitated,
_every_ possible formal parameter type at path fun.targ matches _some_ actual
parameter type at path arg.type. More generally, a binary constraint
$p_{1}=p_{2}$ is reduced if everything at path $p_{1}$ matches something at
path $p_{2}$; this definition extends naturally to non-binary constraints. We
now define the machinery to state this formally, and then provide a simple
algorithm for reducing a constraint, which builds upon ECTA intersection.

_Subautomaton at a Path._ First, we generalize the definition of a subterm at
a path, $t|_{p}$, to ECTAs:

###### Definition 3.13 (Nodes at path, Subautomaton at a path).

The set $\mathsf{nodes}(n,p)$ of nodes reachable from
$n=\bm{\mathtt{U}}(\overline{e})$ via path $p$ is defined as:

$\mathsf{nodes}(n,\epsilon)=\\{n\\}\quad\quad\quad\mathsf{nodes}(n,j.p)=\bigcup_{i}\mathsf{nodes}(e^{i},j.p)$

The set $\mathsf{nodes}(e,p)$ of nodes reachable from a transition
$e=\bm{\Pi}(s,\overline{n},C)$ is defined as:

$\mathsf{nodes}(e,j.p)=\begin{cases}\mathsf{nodes}(n^{j},p)&j<\mathsf{arity}(s)\\\
\emptyset&\text{otherwise}\end{cases}$

Finally, the _subautomaton_ of $n$ at path $p$ is defined as
$n|_{p}=\bigsqcup\mathsf{nodes}(n,p)$; similarly, the subautomaton of $e$ is
defined as $e|_{p}=\bigsqcup\mathsf{nodes}(e,p)$.

In 2(a), if $n$ is the root node, then
${{{\mathsf{nodes}(n,\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{arg}}.{\@listingGroup{ltx_lst_identifier}{type}}}}}})=\\{\bm{\mathtt{U}}(\bm{\Pi}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}})),\bm{\mathtt{U}}(\bm{\Pi}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Char}}}}}}))\\}$
and
${{n|_{\texttt{arg.type}}=\bm{\mathtt{U}}([\bm{\Pi}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}}),\bm{\Pi}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Char}}}}}})])$.
The reader might be wondering why define $\mathsf{nodes}(e,j.p)=\emptyset$ for
an out-of-bounds index $j$ instead of restricting these and following
definitions to “well-formed” paths. The rationale is to enable ECTAs to have
“cousin” transitions with different arities, and be able to navigate to nodes
and subautomata at higher arities, by simply discarding branches with lower
arities; this flexibility is required, for instance, in our full encoding of
type-driven synthesis in §6.2.

Without equality constraints, the denotation of $n|_{p}$ would simply be the
set of subterms $t|_{p}$ of all terms $t$ represented by $n$. With equality
constraints, $n|_{p}$ is an overapproximation of that set, since the equality
constraints on the topmost layers get ignored:

###### Theorem 3.14 (Correctness of subautomaton at a path).

$\llbracket
n|_{p}\rrbracket^{\text{N}}\supseteq\left\\{t|_{p}\mathrel{\Big{|}}t\in\llbracket
n\rrbracket^{\text{N}}\right\\}$

_Reduction Criterion._ We can now formally state what it means for a
constraint to be reduced:

###### Definition 3.15 (Reduction Criterion).

Let $e=\bm{\Pi}(s,\overline{n},C)$ be a transition and let
$c=\\{p_{1}=\dots=p_{k}\\}\in C$. We say that $e$ satisfies the _reduction
criterion_ for $c$ (alternatively, $c$ is _reduced_ at $e$) if, for each
$p_{i},p_{j}\in c$ and each $n\in\mathsf{nodes}(e,p_{i})$, $n\sqcap
e|_{p_{j}}\neq\bm{\mathtt{U}}_{\bot}$.

The reduction criterion suggests an algorithm for reducing a path constraint:
given a constraint $p_{1}=p_{2}$ on transition $e$, replace every node $n$
reachable via $p_{1}$ with $n\sqcap e|_{p_{2}}$. As a result, every node in
$\mathsf{nodes}(e,p_{1})$ will match some node in $\mathsf{nodes}(e,p_{2})$.
For example, to reduce the constraint fun.targ = arg.type at the transition
app in Fig. 2, the algorithm first computes
${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set<EMAIL_ADDRESS>the automaton representing all possible actual parameter types; the result is
${{n_{a}=\bm{\mathtt{U}}(\bm{\Pi}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}}),\bm{\Pi}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Char}}}}}}))$.
Next, it intersects $n_{a}$ it with each of the three nodes reachable via
fun.targ, that is, Int, Char, and Bool. This has no effect on the targ
children of $g$ and $h$, but the targ child of $f$ becomes
$\bm{\mathtt{U}}_{\bot}$, leading to the removal of the $f$ transition upon
normalizatoin and resulting in 2(b).

_Intersection at a Path._ In order to formalize the reduction algorithm
outlined above, we introduce the notion of _intersection at a path_.

###### Definition 3.16 (Intersection at a Path).

Intersecting node $n$ with node $n^{\prime}$ at path $p$, denoted
$n|_{p}^{\sqcap n^{\prime}}$, replaces all nodes reachable from $n$ via $p$
with their intersection with $n^{\prime}$. More formally, if
$n=\bm{\mathtt{U}}(\overline{e})$:

$n|_{\epsilon}^{\sqcap n^{\prime}}=n\sqcap n^{\prime}\quad\quad\quad
n|_{j.p}^{\sqcap n^{\prime}}=\bm{\mathtt{U}}(e^{i}|_{j.p}^{\sqcap
n^{\prime}})$

where intersecting a transition $e=\bm{\Pi}(s,[n^{0},\dots,n^{k-1}],C)$ at a
non-empty path $p$ is defined as:

$e|_{j.p}^{\sqcap
n^{\prime}}=\begin{cases}\bm{\Pi}(s,[n^{0},\dots,n^{j}|_{p}^{\sqcap
n^{\prime}},\dots,n^{k-1}],C)&j<\mathsf{arity}(s)\\\
\bm{\Pi}_{\bot}&\text{otherwise}\end{cases}$

For example, in 2(a), intersecting the root node $n$ at path fun.targ with the
node $n_{a}$ from our previous example
(${{n_{a}=\bm{\mathtt{U}}(\bm{\Pi}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}}),\bm{\Pi}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Char}}}}}}))$)
yields the ECTA in 2(b).

###### Lemma 3.17.

If $t\in\llbracket n|_{p}\rrbracket^{N}$ and $t\in\llbracket
n^{\prime}\rrbracket^{N}$, then $t\in\llbracket\left(n|_{p}^{\sqcap
n^{\prime}}\right)|_{p}\rrbracket^{N}$.

_Reduction Algorithm._ With this new terminology, we can recast our previous
explanation of how the constraint fun.targ = arg.type in Fig. 2 gets reduced:
once we have obtained the “actual parameter automaton”
${n_{a}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set<EMAIL_ADDRESS>we can simply return $n|_{\texttt{fun.targ}}^{\sqcap n_{a}}$ (where $n$ is the
root node). This explanation needs one final tweak: in this example, the
information only propagates in one direction—from arg.type to fun.targ—because
the types of the actuals happen to be a subset of the types of the formals; in
general, though, reduction needs to propagate information both ways. Hence a
more accurate recipe for how to perform the reduction in Fig. 2 is:  (1)
compute the automaton
$n^{*}=\left(n|_{\texttt{fun.targ}}\right)\sqcap\left(n|_{\texttt{arg.type}}\right)$,
capturing all _shared_ formal and actual parameter types;  (2) intersects the
root with $n^{*}$ at _both_ paths involved in the constraint:
$\left(n|_{\texttt{fun.targ}}^{\sqcap
n^{*}}\right)|_{\texttt{arg.type}}^{\sqcap n^{*}}$.  We extrapolate this
description into a general algorithm for static reduction:

###### Definition 3.18 (Static Reduction).

Let $c=\\{p_{1}=\dots=p_{k}\\}$ be a prefix-free PEC; then

$\mathsf{reduce}(e,c)=e|_{p_{1}}^{\sqcap n^{*}}\dots|_{p_{k}}^{\sqcap
n^{*}}\quad\quad\text{where}\quad n^{*}=\bigsqcap_{p_{i}\in c}e|_{p_{i}}$

###### Theorem 3.19 (Completeness of Reduction).

$\mathsf{reduce}(e,c)$ satisfies the reduction criterion for $c$.

###### Theorem 3.20 (Soundness of Reduction).

Let $e=\bm{\Pi}(s,\overline{n},C)$ be a transition and $c\in C$; then:

$\llbracket\mathsf{reduce}(e,c)\rrbracket^{E}=\llbracket e\rrbracket^{E}$

##  4\. Fast Enumeration with Dynamic Reduction

We now turn to our second core contribution: the algorithm for efficiently
extracting (or enumerating) terms represented by an ECTA. As we have outlined
in §2.4, the main idea behind the algorithm is to avoid eager enumeration of
constrained nodes, instead replacing them with “unification” variables—the
mechanism we dub _dynamic reduction_.

Inspired by presentations of DPLL(T) and Knuth-Bendix completion (Bachmair and
Dershowitz, 1994; Nieuwenhuis et al., 2006), we formalize the enumeration
algorithm as a non-deterministic transition system. Configurations of this
system are called _enumeration states_ and steps are governed by two rules,
Choose and Suspend. Intuitively, Choose handles unconstrained ECTA nodes,
making a non-deterministic choice between their incoming transitions; Suspend
handles constrained nodes, suspending them into variables. Fig. 7, which
serves as the running example for this section, shows an example sequence of
Choose and Suspend steps applied to a simplified version of the ECTA from Fig.
4 (the simplified ECTA encodes all well-typed size-two terms in the
environment
${{{{\Gamma=\\{x\colon\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}},y\colon\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Char}}}}}},g\colon\alpha\to\alpha,h\colon\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Char}}}}}}\to\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Bool}}}}}}\\}$).

Figure 7. An example sequence of steps through enumeration states. The focus
node of each step is highlighted in blue and constraint fragments are
highlighted in green. The final state is fully enumerated.

###  4.1. Enumeration State

The syntax of enumeration states is shown in subsection 4.1 (left). Var is a
countably infinite set of variables, with a dedicated “root” variable
$v_{\top}\in\textsf{Var}$. An _enumeration state_ $\sigma$ is a mapping from
variables to _partially-enumerated terms_ (or _p-terms_ for short). With the
exception of $v_{\top}$, which stores the top-level enumeration result, each
variable captures a set of ECTA nodes that are constrained to be equal. For
example, in Fig. 7 (g), the variable $v_{1}$ captures the nodes g.targ and
x.type, which are equated by the constraint on app, and also g.tret, equated
to the former by the constraint on g.

A p-term $\tau$ is a term that might contain variables and _unenumerated
nodes_ (_u-nodes_ for short). A u-node $\square(n,\Phi)$ is an ECTA node $n$
annotated with zero or more _constraint fragments_ $\phi$, each consisting of
a PEC and a variable. Intuitively, a constraint fragment is a constraint
propagated downward from an ECTA transition. For example, in Fig. 7 (b), when
the original constraint fun.targ = arg.type on app is propagated down to unary
and scalar, it is split into two fragments:
${\langle\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{targ}}}}}}=v_{1}\rangle$
and
${\langle\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{type}}}}}}=v_{1}\rangle$.
The splitting is necessary because for each of the child u-nodes one of the
sides of this constraint is “out of scope”; hence a fresh variable $v_{1}$ is
introduced to refer to the common value at both sides. A variable $v$ is
_solved_ in $\sigma$ iff it is not mentioned in any of the constraint
fragments; for example, $v_{1}$ is unsolved in Fig. 7 (b)–(f) and solved in
Fig. 7 (g).

A u-node is _restricted_ iff its $\Phi$ is non-empty; an unrestricted u-node
is written $\square(n)$. An enumeration state $\sigma$ is called _fully
enumerated_ if there are no restricted u-nodes anywhere inside $\sigma$. The
reader might be surprised that a fully enumerated state is allowed to have
u-nodes at all; as we explain in §4.4, this enables compact representation of
enumeration results with “trivial differences.”

Enumeration States

$s\in\Sigma,v\in\textsf{Var},c\in\textsf{PEC}$
$\begin{array}[]{rll}\phi\mathrel{\mathord{:}\mathord{:=}}&\langle
c=v\rangle&\text{\emph{Constraint fragments}}\\\
\Phi\mathrel{\mathord{:}\mathord{:=}}&\overline{\phi}&\text{\emph{Cons.
fragment sets}}\\\
\tau\mathrel{\mathord{:}\mathord{:=}}&&\text{\emph{P-terms}}\\\ &\mid v\mid
s(\overline{\tau})&\text{variable, application}\\\
&\mid\square(n,\Phi)&\text{unenumerated node}\\\
\sigma\mathrel{\mathord{:}\mathord{:=}}&[\overline{v\mapsto\tau}]&\text{\emph{Enumeration
states}}\\\
\mathcal{C}[\cdot]\mathrel{\mathord{:}\mathord{:=}}&&\text{\emph{Contexts}}\\\
&\mid\cdot&\\\ &\mid
s(\overline{\tau},\mathcal{C}[\cdot],\overline{\tau})&\end{array}$

Enumeration step
$\boxed{\tau\longrightarrow\tau^{\prime},\sigma\longrightarrow\sigma^{\prime}}$

$\square(\bm{\mathtt{U}}(\overline{e}),\Phi)\longrightarrow
s(\tau^{0},\dots,\tau^{k-1})$ [Choose] σ[v] = C[τ]
$\tau\longrightarrow\tau^{\prime}$ v is solved
$\sigma\longrightarrow\sigma[v\mapsto\mathcal{C}[\tau^{\prime}]]$ [Suspend-1]
σ[v] = C[$\square(n,\langle\epsilon=v^{\prime}\rangle\cup\Phi)$] v’
∉$\mathsf{dom}$(σ)
$\sigma\longrightarrow\sigma[v\mapsto\mathcal{C}[v^{\prime}],v^{\prime}\mapsto\square(n,\Phi)]$
[Suspend-2] σ[v] = C[$\square(n,\langle\epsilon=v^{\prime}\rangle\cup\Phi)$]
σ[v’] = $\square(n^{\prime},\Phi^{\prime})$
$\sigma\longrightarrow\sigma[v\mapsto\mathcal{C}[v^{\prime}],v^{\prime}\mapsto\square(n\sqcap
n^{\prime},\Phi\cup\Phi^{\prime})]$

Figure 8. Enumeration states and rules.

_Denotation._ The denotation of an enumeration state
$\llbracket\sigma\rrbracket^{S}$ is a set of substitutions
$\rho\colon\textsf{Var}\rightharpoonup\mathcal{T}(\Sigma)$, which is
compatible with the constraint fragments and subterm relations imposed by
variables inside p-terms. Because of the circular dependencies between a
p-term and its enclosing $\sigma$, the formal definition is somewhat technical
and therefore relegated to App. A.2.

###  4.2. Enumeration Rules

subsection 4.1 (right) formalizes the above-mentioned Choose and Suspend rules
as a step relation $\sigma\longrightarrow\sigma$ over enumeration states and
an auxiliary step relation $\tau\longrightarrow\tau^{\prime}$ over p-terms.

_Choose._ We first formalize the auxiliary rule Choose-$\square$ for p-terms.
This rule takes a u-node, non-deterministically selects one of its transitions
$e$, and steps to a p-term that has $e$’s function symbol at the root and new
u-nodes as children. Step \raisebox{-.9pt} {5}⃝ in Fig. 7 is an example
application of this rule: here the original u-node scalar turns into one of
its two incoming transitions, x; step \raisebox{-.9pt} {1}⃝ is also an
instance of this rule, albeit with no alternatives.

The tricky aspect of Choose-$\square$ is propagating constraints—either from
the transition $e$ or from the original u-node—to the newly minted u-nodes.
The former scenario is illustrated in step \raisebox{-.9pt} {1}⃝: here the PEC
${{c=\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{fun}}.{\@listingGroup{ltx_lst_identifier}{targ}}}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{arg}}.{\@listingGroup{ltx_lst_identifier}{type}}}}}}\\}$
on the app transition is split into two fragments,
${\langle\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{targ}}}}}}=v_{1}\rangle$
and
${\langle\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{type}}}}}}=v_{1}\rangle$,
attached to the new u-nodes unary and scalar, respectively. To this end,
Choose-$\square$ first creates a fresh variable $v_{1}$ and forms a constraint
fragment $\langle c=v_{1}\rangle$ using the original PEC $c$; next it
_projects_ this fragment down to each $i$-th child, retaining only those paths
of $c$ that start with $i$ and chopping off their heads. The
$\mathsf{project}$ function is defined formally in Fig. 10. Note how the two
new fragments together completely capture the semantics of the original
constraint.

The latter scenario—propagating existing constraint fragments—is illustrated
in step \raisebox{-.9pt} {5}⃝. Here the u-node scalar is restricted by the
fragment
${\langle\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{type}}}}}}=v_{1}\rangle$;
in this case, there is no need to create new variables: the existing fragment
is simply projected down to the child tx and becomes
$\langle\epsilon=v_{1}\rangle$. In the general case, both new and existing
constraint fragments should be combined; this is the case in step
\raisebox{-.9pt} {2}⃝, where the u-node targ inherits the fragment
$\langle\epsilon=v_{1}\rangle$ from unary, and also acquires a new fragment
$\langle\epsilon=v_{2}\rangle$ by splitting the constraint on g.

Finally, consider the rule Choose, which lifts Choose-$\square$ to whole
enumeration states. This rule allows making a step inside any component of
$\sigma$, as long as its variable is solved. For example, in Fig. 7 (e) we are
not allowed to make a step inside $v_{1}$ (say, choosing Bool among the three
types), because $v_{1}$ still appears in the constraint fragment
${\langle\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{type}}}}}}=v_{1}\rangle$
inside $v_{\top}$. The rationale for this restriction is to avoid making
premature choices for constrained nodes: in our example, picking Bool would be
a mistake, which is entirely avoidable by simply waiting until all constraints
are resolved (such as the state in Fig. 7 (g)).

_Suspend._ The Suspend rules handle u-nodes with _$\epsilon$ -fragments_,
_i.e._ constraint fragments of the form
$\langle\epsilon=v\rangle$.101010Choose-$\square$ does not apply to these
nodes thanks to its last premise. Note also that because all PECs in the
original ECTA are prefix-free and this property is maintained by
$\mathsf{project}$, any fragment that contains $\epsilon$, must _only_ contain
$\epsilon$. Intuitively, an $\epsilon$-fragment indicates that this node is
the target of a constraint captured by $v$. In response, the Suspend rules
simply “move” the target u-node to the $v$-component of the state, replacing
it with $v$ in the original p-term.

The two Suspend rules differ in whether the current state $\sigma$ already has
a mapping for $v$: if it does not, Suspend-1 initializes this mapping with its
target u-node $\square(n,\Phi)$; if it does, Suspend-2 updates this mapping,
combining the old u-node $\square(n^{\prime},\Phi^{\prime})$ and the new one
$\square(n,\Phi)$ by intersecting their ECTAs and merging their constraint
fragments. Note that the old value of $v$ must necessarily be a u-node,
because Choose is not allowed to operate under unsolved variables.

An example application of Suspend-1 is step \raisebox{-.9pt} {3}⃝ of Fig. 7.
The target node tret has an $\epsilon$-fragment
$\langle\epsilon=v_{2}\rangle$; since $v_{2}$ is uninitialized, Suspend-1
creates a new mapping $[v_{2}\mapsto\text{{tret}}]$. Step \raisebox{-.9pt}
{6}⃝, on the other hand, is an example of Suspend-2: the target node tx is
restricted by $\langle\epsilon=v_{1}\rangle$; since $v_{1}$ already maps to
tg, Suspend-2 updates it with $\text{{tx}}\sqcap\text{{tg}}$. As a result of
this intersection, $v_{1}$ now contains only those types (in this case, the
sole type Int) that make the term represented by $v_{\top}$ well-typed.

_Eliminating Redundant Variables._ Finally, let us demystify the
transformation \raisebox{-.9pt} {4}⃝ in Fig. 7, which consists of three atomic
steps. The first step suspends targ, which has _not one but two_
$\epsilon$-fragments—$\langle\epsilon=v_{1}\rangle$ and
$\langle\epsilon=v_{2}\rangle$—either of which can be targeted by a Suspend.
Suppose that the second one is chosen (both choices lead to equivalent
results, up to variable renaming). Since $v_{2}$ is already initialized,
Suspend-2 fires, merging tret and targ into a single u-node tg’ under $v_{2}$;
importantly, tg’ inherits the other constraint fragment from targ, namely
$\langle\epsilon=v_{1}\rangle$. Because of that, Suspend-1 can now fire on
tg’, creating the state $[v_{\top}\mapsto\dots,v_{2}\mapsto
v_{1},v_{1}\mapsto\text{{tg}}]$, where tg is tg’ stripped of its constraint
fragment. This new state is a bit awkward, since it contains a “redundant”
variable $v_{2}$, which simply stores another variable, $v_{1}$. To get rid of
such redundant variables, we introduce an auxiliary rule Subst, which simply
replaces all occurrences of $v_{2}$ with $v_{1}$ and removes the unused
mapping from $\sigma$ (see Fig. 10). After applying Subst, we arrive at the
state in Fig. 7 (e).

###  4.3. Enumeration Algorithm

We are now ready to describe the top-level algorithm Enumerate. The algorithm
takes as input an ECTA $n$ and produces a stream of fully-enumerated states.
To this end, it first creates an initial state
$\sigma_{0}=[v_{\top}\mapsto\square(n)]$, and then enumerates derivations of
$\sigma_{0}\longrightarrow^{*}\sigma_{\bullet}$ where $\sigma_{\bullet}$ is
fully enumerated and $\longrightarrow^{*}$ is the reflexive-transitive closure
of $\longrightarrow$. In each step, the algorithm has the freedom to select
(i) which u-node to target, and  (ii) in the case of Choose, which transition
to choose.  The enumeration rules are designed in such a way that the former
selection constitutes “don’t care non-determinism” (_i.e._ any target node can
be selected without loss of completeness); this is in contrast to the latter
selection, which constitutes “don’t know non-determinism” and must be
backtracked. At the same time, different schedules of rule applications might
lead to significantly different performance. The ecta library provides a
default schedule—depth-first, left to right—but enables the user to specify a
domain-specific schedule in order to optimize performance.

###### Theorem 4.1 (Termination of Enumeration).

There is no infinite sequence
$\sigma_{0}\longrightarrow\sigma_{1}\longrightarrow\dots$.

###### Theorem 4.2 (Correctness of Enumeration).

Let $n$ be an ECTA, $\sigma_{0}$ be the initial enumeration state, and
consider all finite sequences $\sigma_{0}\longrightarrow^{*}\sigma_{\bullet}$,
such that $\sigma_{\bullet}$ is fully enumerated; then:

$\llbracket
n\rrbracket^{N}=\left\\{\rho(v_{\top})\mathrel{\Big{|}}\sigma_{0}\longrightarrow^{*}\sigma_{\bullet},\rho\in\llbracket\sigma_{\bullet}\rrbracket^{S}\right\\}$

###  4.4. Compact Fully Enumerated States

Projecting constraint fragments

$\begin{array}[]{rl}\mathsf{project}(\Phi,i)&=\bigcup_{\phi\in\Phi}\mathsf{project}(\phi,i)\\\
\\\ \mathsf{project}(\langle c=v\rangle,i)&=\begin{cases}\\{\langle
c^{\prime}=v\rangle\\}&\text{if}\ c^{\prime}\neq\emptyset\\\
\emptyset&\text{otherwise}\end{cases}\\\ \text{where}\
c^{\prime}&=\bigcup_{p\in c}\mathsf{project}(p,i)\\\ \\\
\mathsf{project}(p,i)&=\begin{cases}\bot&\text{if}\ p=\epsilon\\\
\\{p^{\prime}\\}&\text{if}\ p=i.p^{\prime}\\\
\emptyset&\text{otherwise}\end{cases}\end{array}$

Enumeration step (cont.) $\boxed{\sigma\longrightarrow\sigma^{\prime}}$

$\inference[\textsc{Subst}]{\sigma[v_{2}]=v_{1}}{\sigma\longrightarrow[v_{1}/v_{2}]\left(\sigma\setminus[v_{2}\mapsto
v_{1}]\right)}$

Figure 9. Auxiliary definitions

(a)

(b)

Figure 10. (a) An ECTA representing all perfect trees of depth three, whose
leaves are either all x or all y (b) The ECTA fully enumerated, in logarithmic
space

We now return to the design decision to allow (unrestricted) u-nodes in fully
enumerated states. Our running example in Fig. 7 does not motivate this
decision very well: the fully enumerated state in Fig. 7 (g) encodes a single
term anyway, so it seems only natural to let Choose loose on the last
remaining u-node. For other ECTAs, however, a single fully-enumerated state
might represent exponentially many111111Or, with the cyclic ECTAs of §5,
infinitely many. terms, or the terms might be exponentially larger, or both.
For an example, consider 10(a). This ECTA represents the set of all perfect
binary trees of depth three, whose leaves are either all x or all y. A
moment’s thought reveals that this set contains two trees, each of size $15$.
Instead of returning these two large trees explicitly, the fully-enumerated
state $\sigma_{\bullet}$ in 10(b) represents them as a _hierarchy of
unconstrained tree automata_ , from which the concrete trees may be trivially
generated. It is straightforward to see that the sizes of the two perfect
trees grow exponentially with their depth, while the size of
$\sigma_{\bullet}$ grows only linearly.

The main benefit of this design, however, is that, depending on the problem
domain, some nodes _need not be enumerated at all_ , as long as we know their
denotation is non-empty. For example, to determine whether a propositional
formula is satisfiable (§6.1), it is often enough to provide a _partial
satisfying assignment_ , because the values of the unassigned variables are
irrelevant; such a partial assignment can be represented by a
$\sigma_{\bullet}$, where irrelevant variables are left unenumerated.
Similarly, in type-driven synthesis, the polymorphic type of a component need
not always be fully instantiated, as long we know that a compatible
instantiation exists. In fact, as we explain in §6.2, cyclic ECTAs can encode
infinitely many possible polymorphic instantiations, and enumerating them all
would be simply impossible.

##  5\. Cyclic ECTA

Syntax

$\begin{array}[]{rll}n\mathrel{\mathord{:}\mathord{:=}}&\bm{\mathtt{U}}(\overline{e})\mid\mu
x.\bm{\mathtt{U}}(\overline{e})\mid x&\text{nodes (states)}\\\
e\mathrel{\mathord{:}\mathord{:=}}&\bm{\Pi}(s,\overline{n},C)\mid\bm{\Pi}_{\bot}&\text{transitions}\\\
\end{array}$

Unfolding Recursive Nodes

$\begin{array}[]{rl}\mathsf{unfold}(\mu x.n)&=\left[\mu
x.n\middle/x\right]n\\\
\mathsf{unfold}(\bm{\mathtt{U}}(\overline{e}))&=\bm{\mathtt{U}}(\overline{e})\end{array}$

Denotation

$\begin{array}[]{rl}\llbracket\bm{\mathtt{U}}(\overline{e})\rrbracket^{N}&=\bigcup_{i}\llbracket
e^{i}\rrbracket^{E}\\\ \llbracket\mu
x.n\rrbracket^{N}&=\llbracket\mathsf{unfold}(\mu x.n)\rrbracket^{N}\\\
\llbracket\bm{\Pi}(s,\overline{n},C)\rrbracket^{E}&=\left\\{s(\overline{t})\mathrel{\Big{|}}t^{i}\in\llbracket
n^{i}\rrbracket^{N},s(\overline{t})\models C\right\\}\end{array}$

Figure 11. Cyclic ECTAs: syntax and semantics. Here $s\in\Sigma$, $C$ is a
PCS, and $x$ is a bound variable.

We now present the formalism for fully general ECTAs, which may contain
cycles. With cycles, an ECTA node can now represent an infinite space of
terms, such as an arbitrary term in some context-free language, including (as
in §6.2) the language of arbitrary Haskell types. While this requires an
extension to the syntax of ECTAs to allow recursion, shockingly, none of the
algorithms require substantial modification.

###  5.1. Cyclic ECTAs: Core Definition

We extend acyclic ECTAs to cyclic by adding “recursive nodes” $\mu
x.\bm{\mathtt{U}}(\overline{e})$. Within this node, $x$ is a variable bound to
$\bm{\mathtt{U}}(\overline{e})$. In diagrams, we depict any use of $x$ as a
back-edge to $\bm{\mathtt{U}}(\overline{e})$ and keep the $\mu$ binding itself
implicit. Semantically, $x$ can be replaced with a copy of the node it is
bound to, so that an ECTA $n$ is equivalent to
$[\bm{\mathtt{U}}(\overline{e})/x]n$—or rather, to $[\mu
x.\bm{\mathtt{U}}(\overline{e})/x]n$, since $\bm{\mathtt{U}}(\overline{e})$
contains further uses of $x$. 12(a) shows an example ECTA, with a recursive
node Nat representing arbitrary natural numbers defined by the grammar
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Nat}}}}}}\mathrel{\mathord{:}\mathord{:=}}S(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Nat}}}}}})\mid
Z$. Fig. 11 gives the syntax and semantics of cyclic ECTAs. The recursive
definition of $\llbracket n\rrbracket^{N}$ should be interpreted with least-
fixed-point semantics (as it may unfold arbitrarily many times). Note that
this grammar excludes nodes like $\mu x.x$ or $\mu x.\mu y.x$, which would be
meaningless. We again assume implicit sharing of sub-trees.121212However, this
pseudo-tree representation precludes sharing of some nodes which would be
shared in a true graph representation.

(a)

(b)

Figure 12. (a) ECTA representing an environment with two arbitrary natural
numbers $x$ and $y$, where $y=x+2$. The Nat node is represented $\mu
x.\bm{\mathtt{U}}(\bm{\Pi}(S,x),\bm{\Pi}(Z))$. (b) The ECTA unfolded into
lasso form. The grayed-out transitions will be removed by static reduction.

Cyclic ECTAs become unwieldy when constraints are allowed inside cycles. As a
recursive node $\mu x.n$ is repeatedly unfolded and its constraints
duplicated, it can yield an arbitrarily large constraint system whose smallest
solution may be arbitrarily large. In fact, in this general case, ECTA
emptiness is undecidable:

###### Theorem 5.1 (Undecidability of Emptiness).

Determining whether $\llbracket n\rrbracket^{N}=\emptyset$ is undecidable.

###### Proof.

By reduction from the Post Correspondence Problem. More explanation in App.
A.1. ∎

This motivates a restriction barring constraints on cycles, which guarantees
that the constraint system remains finite and efficient algorithms remain
possible. More formally:

###### Definition 5.2 (Finitely-constrained ECTA).

An ECTA $n$ is _finitely-constrained_ if, for all recursive nodes $\mu x.m$
reachable from $n$, $m=\mathsf{sk}(m)$.

We assume henceforth that all ECTAs are finitely-constrained. What makes such
ECTAs tractable is that, after sufficient unfolding, they enter what we call
_lasso form_ :

###### Definition 5.3 (Lasso form).

An ECTA $n$ is in _lasso form_ if it contains no constrained recursive nodes
(_i.e._ , no path constraint references a recursive node).

An ECTA in lasso form is split into a top portion, which contains constraints
but no cycles, and a bottom portion, which contains cycles but no constraints.
The top portion permits only finitely many choices, while the bottom portion
can be enumerated and intersected as in classic tree automata theory. While
they may perform intersection on entire subautomata, neither static nor
dynamic reduction directly inspect nodes beneath the deepest constraint.
Hence, with the updated definition of intersection, our definitions for both
static and dynamic reduction work unmodified on ECTAs in lasso form. An
example ECTA in lasso form is in 12(b).

###  5.2. Algorithms for Cyclic ECTAs

Reachable Nodes

$\mathsf{nodes}(\mu x.n,p)=\mathsf{nodes}(\mathsf{unfold}(\mu x.n),p)$

Intersection at a Path

$(\mu x.n)|_{n^{\prime}}^{\sqcap p}=\mathsf{unfold}(\mu
x.n)|_{n^{\prime}}^{\sqcap p}$

Enumeration step $\boxed{\tau\longrightarrow\tau^{\prime}}$

$\displaystyle\inference[\textsc{Choose-$\mu$}]{\Phi\neq\emptyset}{\square(\mu
x.n,\Phi)\longrightarrow\square(\mathsf{unfold}(\mu x.n),\Phi)}$

Figure 13. Extensions to prior algorithms to account for recursive nodes

_Intersection._ One formulation of intersection for classic string automata is
a depth-first search that begins from a pair of initial or final states and
finds all reachable pairs of states. We use this idea to extend our previous
definition of intersection to cyclic ECTAs: the algorithm tracks all previous
visited pairs of nodes, and creates a recursive reference upon seeing the same
pair twice.

More formally, we define $n_{1}\sqcap n_{2}$ in terms of a helper operation,
$n_{1}\mathrel{\underset{S}{\sqcap}}n_{2}$ (intersection tracking the set of
previously-visited pairs); which in turn invokes the helper
$n_{1}\mathrel{\underset{S}{\tilde{\sqcap}}}n_{2}$. We assume a function
$\mathsf{var}(\\{n_{1},n_{2}\\})$ mapping an unordered pair of nodes to a
unique named variable for that pair. We use the notation $n_{1}\in n_{2}$ to
mean that some descendant of $n_{1}$ is equal to $n_{2}$.

Let $n_{1},n_{2}\in N$ be two ECTAs, $S\subseteq\binom{N}{2}$ be a set of
unordered pairs of ECTAs, and define
$S^{\prime}=S\cup\\{\\{n_{1},n_{2}\\}\\}$. Then define:

$n_{1}\mathrel{\underset{S}{\sqcap}}n_{2}=\begin{cases}\mathsf{var}(n_{1},n_{2})&\\{n_{1},n_{2}\\}\in
S\\\ \mu
z.n_{1}\mathrel{\underset{S^{\prime}}{\tilde{\sqcap}}}n_{2}&z=\mathsf{var}(\\{n_{1},n_{2}\\})\wedge
z\in(n_{1}\mathrel{\underset{S^{\prime}}{\tilde{\sqcap}}}n_{2})\\\
n_{1}\mathrel{\underset{S^{\prime}}{\tilde{\sqcap}}}n_{2}&\text{otherwise}\end{cases}$

The remainder of the definition is almost identical to the definition for
acyclic ECTAs, except that recursive nodes are first unfolded. Let
$\mathsf{unfold}(n_{1})=\bm{\mathtt{U}}(\overline{e_{1}})$ and
$\mathsf{unfold}(n_{2})=\bm{\mathtt{U}}(\overline{e_{2}})$. Then:

$n_{1}\mathrel{\underset{S}{\tilde{\sqcap}}}n_{2}=\bm{\mathtt{U}}\left(\left\\{e_{1}^{i}\mathrel{\underset{S}{\sqcap}}e_{2}^{j}\mathrel{\Big{|}}e_{1}^{i}\in\overline{e_{1}},e_{2}^{j}\in\overline{e_{2}}\right\\}\right)$

Let $e_{1}=\bm{\Pi}(s_{1},[n_{1}^{0}\dots n_{1}^{k-1}],C_{1})$,
$e_{2}=\bm{\Pi}(s_{2},[n_{2}^{0}\dots n_{2}^{l-1}],C_{2})$ be two transitions,
then:

$e_{1}\mathrel{\underset{S}{\sqcap}}e_{2}=\begin{cases}\bm{\Pi}(s_{1},[n_{1}^{0}\mathrel{\underset{S}{\sqcap}}n_{2}^{0},\dots,n_{1}^{k-1}\mathrel{\underset{S}{\sqcap}}n_{2}^{k-1},C_{1}\cup
C_{2})&\text{if}\ s_{1}=s_{2}\ \text{and}\ C_{1}\cup C_{2}\ \text{is
consistent}\\\ \bm{\Pi}_{\bot}&\text{otherwise}\end{cases}$

Now, define $n_{1}\sqcap
n_{2}=n_{1}\mathrel{\underset{\emptyset}{\sqcap}}n_{2}$.

_Static Reduction._ Recall from §3.5 that static reduction is defined in terms
intersection at a path, which in turn relies on the definition of reachable
nodes. Fig. 13 extends these operations to unfold recursive nodes until the
ECTA enters lasso form, at least with regards to the PEC under consideration.
Then the rest of the static reduction algorithm remains unchanged.

_Enumeration._ Adapting enumeration to cyclic ECTAs requires a single change:
the new Choose-$\mu$ rule in Fig. 13 unfolds recursive nodes referenced by
some ancestor’s constraint. This rule continues unfolding such nodes so long
as they are referenced by a parent’s constraint, at which point it is a fully
enumerated node. Note that a fully-enumerated state will necessarily be in
lasso form.

##  6\. Applications

This section gives two examples of problem domains that can be reduced to ECTA
enumeration: boolean satisfiability (SAT; §6.1) and type-driven program
synthesis (§6.2). The second domain has already been introduced informally in
§2; here we present its encoding in full generality, and in §7 we evaluate our
encoding against a state-of-the-art synthesizer Hoogle+. The purpose of
presenting the first domain is to demonstrate the versatility of ECTAs, not to
compete with highly-engineered industrial SAT solvers; hence we leave the SAT
domain out of empirical evaluation.

###  6.1. Boolean Satisfiability

(a) Variable assignment

(b) CNF formula

Figure 14. ECTA encoding of a CNF formula $(a\vee b)\wedge(\neg a\vee\neg b)$

_Problem Statement._ Given a propositional formula in _conjunctive normal
form_ (CNF), the SAT problem is to find a satisfying assignment to its
variables. A CNF formula is a conjunction of _clauses_ , where each clause is
a disjunction of _literals_ , and each literal is either a variable or its
negation. For example, the CNF formula $(a\vee b)\wedge(\neg a\vee\neg b)$ has
two satisfying assignments: $\\{a,\neg b\\}$ and $\\{\neg a,b\\}$.

_Encoding._ Fig. 14 illustrates our ECTA encoding for the above formula. The
sub-automaton assn in 14(a) represents the set of all possible variable
assignments. The assignment transition has one child per variable, and each
variable node has two alternatives: true and false; hence, to extract a term
from assn one must pick a value for each variable.

The ECTA for the entire CNF formula is shown in 14(b); this ECTA has a single
top-level conjunction transition $\wedge$, with one child per clause. Each
clause node has one alternative per literal in that clause: the choice between
these alternatives corresponds to picking which literal is responsible for
making the clause true. Each literal transition—such as a or
${\neg\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{a}}}}}}$—has
two children: assn is its local copy of the assignment sub-automaton and val
is the Boolean value that this literal assigns to its variable. The constraint
on the literal—such as assn.a = val—restricts its local assignment in such a
way that the literal evaluates to true. Finally, the constraints on the
$\wedge$ transition force all local assignments to coincide; note that, while
the various assn nodes are shared in memory, each occurrence of this node is
an independent choice unless so constrained. The reader might be wondering why
we chose to split these constraints per-variable instead of simply writing
cl1.assn = cl2.assn; as we explain next, this helps enumeration discover
inconsistent assignments quickly.

_SAT Solving as ECTA Enumeration._ With this encoding, the general-purpose
ECTA enumeration algorithm from §4 turns into a SAT solver.131313A curious
reader might be wondering why don’t we go the other direction: encode an ECTA
into a SAT formula and use a SAT solver for ECTA enumeration; this is not
possible in general, as we discuss in more detail in §9.  Specifically, once
Enumerate has found a fully enumerated state, the satisfying assignment can be
read off the children of any assignment symbol in that state; note that if we
let Enumerate run past the first result, it will enumerate all satisfying
assignments, modulo irrelevant variables (see §4.4).

The overall solving procedure amounts to choosing a literal from each clause
and backtracking whenever the assignment becomes inconsistent. For example,
suppose Enumerate has chosen a from cl1; the enumeration state $\sigma$ now
contains variables $v_{a}$ and $v_{b}$, which store assignments for $a$ and
$b$ consistent with the current choices (that is, $v_{a}$ is restricted to
true, while $v_{b}$ still allows both choices). If the algorithm now attempts
to make an inconsistent choice of
${\neg\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{a}}}}}}$
from cl2, this inconsistency is discovered immediately when
${{\neg\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{a}}}}}}.\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{val}}}}}}$
is suspended and intersected with $v_{a}$.

###  6.2. Type-Driven Program Synthesis

_Problem Statement._ We are interested in the following _type-driven program
synthesis_ problem:141414This problem is also known as _type inhabitation_
(Urzyczyn, 1997) and _composition synthesis_ (Heineman et al., 2016). given a
type $T$, called the query type, and a components library $\Lambda$, which
maps component names to their types, enumerate terms of type $T$ built out of
compositions of components from $\Lambda$. For example, a Haskell programmer
might be interested in a code snippet that, given a list of optional values,
finds the first element that is not Nothing (and returns a default value if
such an element does not exist). The programmer might pose this as a type-
driven synthesis problem, where $\Lambda$ is the Haskell standard library, and
the query $T$ is
${{{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{a}}}}}}\to\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language[{\@listingGroup{ltx_lst_identifier}{Maybe}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{a}}]}}}}\to\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{a}}}}}}$.
Given this problem, the state-of-the-art type-driven synthesizer Hoogle+ (Guo
et al., 2020; James et al., 2020) returns a list of candidate programs that
includes the desired solution:
${{{\lambda\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{def}}}}}}\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{mbs}}}}}}\to\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{fromMaybe}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{def}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{listToMaybe}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{catMaybes}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{mbs}}))}}}}$.

In this section we adopt the setting of Hoogle+, where components can be both
_polymorphic_ and _higher-order_ , both of which make the synthesis problem
significantly harder. On the other hand, also following Hoogle+, we do not
consider synthesis of inner lambda abstractions: that is, arguments to higher-
order functions can be partial applications but not lambdas.

_Hoogle+ Limitations._ Hoogle+ works by encoding a synthesis problem into a
data structure called _type-transition net_ : a Petri net, where places
(nodes) correspond to types, and transitions correspond to components; the
synthesis problem then reduces to finding a path from the input types to the
output type of the query. This encoding has two major limitations:

  1. (1)

_No native support for polymorphic components._ In the presence of
polymorphism, the space of types that can appear in a well-typed program
becomes infinite. Because types are encoded as places, a finite Petri net
cannot represent all candidate programs. Instead, Hoogle+ employs a
sophisticated abstraction-refinement loop to build a series of Petri nets that
encode increasingly precise approximations of the set of types of interest.

  2. (2)

_No native support for higher-order components._ Because components are
encoded as transitions with a fixed arity—they transform a fixed number of
types into a single type—all components must always be fully applied. This
precludes the use of higher-order components: for example, in foldr (+) 0 xs,
the binary component (+) is not fully applied. To circumvent this limitation,
Hoogle+ must add a separate _nullary copy_ of the (+) component to the
library. Since these duplicate components bloat the library and slow down
synthesis, in practice only a few popular components are duplicated, thereby
limiting the practicality of the synthesizer.

In this section we present Hectare (Hoogle+: ECTA REvision), our encoding of
type-driven synthesis as ECTA enumeration. This encoding has native support
for both polymorphic and higher-order components, without the need for an
expensive refinement loop or duplicate components.

(a) Variables (library components)

(b) Types (c) Size-two terms

Figure 15. Encoding of variables, types, and fixed-size terms in Hectare.

_Encoding Types._ Recall that §2 (Fig. 4) introduced an encoding for a limited
form of polymorphism, where the type variable $\alpha$ in a type like
$\alpha\to\alpha$ could be instantiated only with base types. We now
generalize this encoding so that $\alpha$ can be instantiated with _any type_
, with arbitrarily nested applications of type constructors. The infinite
space of all types can be finitely encoded as a recursive node any, as shown
in Fig. 15(b). The any node has one child per type constructor in $\Lambda$,
with non-nullary type constructors looping back to any. Now the type
$\alpha\to\alpha$ can be represented as a $\to$ transition, whose children are
both any (and are constrained to equal each other).

_Encoding Components._ The simplified encoding in §2 splits components into
different nodes by their arity (_e.g._ the nodes scalar and unary in Fig. 2);
this was necessary given our simplified encoding of function types, but as we
mentioned above, such arity-specific encoding precludes partial applications.
15(a) illustrates the generalized encoding of components in Hectare. Here all
components, regardless of arity, are gathered in single node
$\text{{term}}_{1}$. Each component is annotated with its type; function types
are represented using the $\to$ transition with two child types, in and out
(for now, ignore the grayed out edges labeled tag, we explain those below).
15(a) showcases the type encoding for two polymorphic components:
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{listToMaybe}}}}}}::[\alpha]\to\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Maybe}}}}}}\
\alpha$ and
${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{map}}}}}}::(\alpha\to\beta)\to[\alpha]\to[\beta]$;
as before, all occurrences of the same type variable are related by equality
constraints, shown in green.

_Encoding Applications._ 15(c) illustrates the Hectare encoding of size-two
terms. As before, the application transition app has two children fun and arg,
but now they are both represented by the same node $\text{{term}}_{1}$; hence
this encoding supports partial applications, such as map listToMaybe.

We now explain the purpose of the grayed-out parts of Fig. 15. The app node
must ensure that its fun child has an arrow type. The mere presence of
fun.type.in and fun.type.out in its first two constraints does not suffice:
recall that the actual ecta library refers to children by index instead of by
name, and hence any other binary type constructor (such as Either) could
satisfy those two constraints. This would lead to accepting ill-typed
programs, such as
${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Left}}}}}}\
x\ y$. To circumvent this issue, we introduce a special tag transition
$(\to)$, which occurs nowhere else but as a first child of every $\to$
transition; by constraining the first child of fun to be $(\to)$, app
effectively ensures that it is indeed a function (see the last constraint on
app).

This encoding of application terms generalizes from size-two terms to terms of
arbitrary fixed size $n$ as follows: the node $\text{{term}}_{n}$ has $n-1$
incoming app transitions, where the $i$-th transition ($i\in
1\mathinner{\ldotp\ldotp}n-1$) has children $\text{{term}}_{i}$ and
$\text{{term}}_{n-i}$.

_Synthesis Algorithm._ So far we have discussed how to encode the space of all
well-typed terms of size $n$. Let us now proceed to the top-level synthesis
algorithm of Hectare. Given a query type, such as
${{{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{a}}}}}}\to[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Maybe}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{a}}}}}}]\to\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{a}}}}}}$,
Hectare first adds the inputs of the query (here
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{def}}}}}}::\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{a}}}}}}$
and
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{mbs}}}}}}::[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Maybe}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{a}}}}}}]$) to the node
$\text{{term}}_{1}$, as if they were components. The algorithm then iterates
over program sizes $n\geq 1$; for each size $n$, it constructs the ECTA
$\text{{term}}_{n}$ and restricts its top-level type to the return type of the
query (here a), following the recipe illustrated in Fig. 3. The algorithm then
statically reduces all constraints in the restricted ECTA and enumerates all
terms accepted by the resulting reduced ECTA, before moving on to the next
size $n$. Note that the type variables _of the query_ (here a) are represented
as type constructors and not as the any node, since those type variables are
universally quantified.

_Enforcing Relevancy._ Existing type-driven synthesizers (Feng et al., 2017;
Guo et al., 2020) restrict synthesis results to _relevantly typed_ terms—that
is, terms that use all the inputs of the query. Without such relevancy
restriction, any synthesis algorithm gets bogged down by short but meaningless
programs. Hectare enforces relevancy via a slight modification to the simple
synthesis algorithm outlined above: it splits every $\text{{term}}_{n}$ node
into $2^{k}$ nodes, where $k$ is the number of inputs in the query. In our
example, there are four nodes at each term size:
$\text{{term}}_{n}^{\\{\texttt{def},\texttt{mbs}\\}},\text{{term}}_{n}^{\\{\texttt{def}\\}},\text{{term}}_{n}^{\\{\texttt{mbs}\\}},\text{{term}}_{n}^{\emptyset}$,
each representing terms that must mention the corresponding set of inputs.
When constructing a new term node, say
$\text{{term}}_{2}^{\\{\texttt{def}\\}}$, Hectare considers all applications
of $\text{{term}}_{1}^{P}$ to $\text{{term}}_{1}^{Q}$ such that ${P\cup
Q=\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{def}}}}}}\\}$.
At the top level, only $\text{{term}}_{n}^{\\{\texttt{def},\texttt{mbs}\\}}$
is connected to the accepting node. Although the number of term-nodes in this
encoding grows exponentially with the number of inputs, this is not a problem
in practice, since the number of inputs is typically small; note also that due
to hash consing in ecta, the overlapping component sets are not actually
duplicated.

##  7\. Evaluation

As we explained in §6.2, we used the ecta library to implement Hectare, a
type-driven component-based synthesizer for Haskell. In this section, we
evaluate the performance of Hectare and compare it with the state-of-the-art
synthesizer Hoogle+, based on an SMT encoding of Petri-net reachability (Guo
et al., 2020). Both tools are written in Haskell, but the Hoogle+
implementation (excluding tests and parsing) contains a whopping 4000 LOC,
while Hectare only contains 400. Although code size is an imperfect measure of
development effort, these numbers suggest that the ecta library has the
potential to significantly simplify the development of program synthesizers.

We designed our evaluation to answer the following research questions:

  1. bx(RQ0)

How does Hectare compare against Hoogle+ on existing and new benchmarks?

  2. bx(RQ0)

How significant are the benefits of static and dynamic reduction in program
synthesis?

All experiments were conducted on an Intel Core i9-10850K CPU with 32 GB
memory.

Table 1. Three sample queries and corresponding solutions from two benchmark suites. Suite | Name | Query | Expected solution
---|---|---|---
Hoogle+ | mergeEither | Either a (Either a b) $\rightarrow$ Either a b | \e $\rightarrow$ either Left id e
headLast | [a] $\rightarrow$ (a, a) | \xs $\rightarrow$ (head xs, last xs)
both | (a $\rightarrow$ b) $\rightarrow$ (a, a) $\rightarrow$ (b, b) | \f p $\rightarrow$ (f (fst p), f (snd p))
Stack-
Overflow | multiIndex | [a] $\rightarrow$ [Int] $\rightarrow$ [a] | \xs is $\rightarrow$ map ((!!) xs) is
splitOn | Eq a $\Rightarrow$ a $\rightarrow$ [a] $\rightarrow$ [[a]] | \x xs $\rightarrow$ groupBy (on (lx@column@trimrighthfillx@intercol@column@after&&) (/= x)) xs
matchedKeys | (b $\rightarrow$ Bool) $\rightarrow$ [(a, b)] $\rightarrow$ [a] | \p xs $\rightarrow$ map fst (filter (p . snd) xs)

###  7.1. Comparison on Hoogle+ Benchmarks

_Experiment Setup._ For our main experiment, we compare the two synthesizers
on the benchmark suite from the latest Hoogle+ publication (James et al.,
2020). This suite includes 45 synthesis queries, and a library of 291
components from 12 popular Haskell modules. These benchmarks are non-trivial:
the expected solutions range in size from 3 to 9, with the average size of
4.7; 40% of the components are polymorphic, and 44% of the queries require
using a higher-order component. Three samples queries from this suite are
listed at the top of Tab. 1. These queries have sizes 4, 5, and 7
respectively, and mergeEither uses a higher-order component either.

Both Hoogle+ and Hectare yield candidate programs one at a time, gradually
increasing the size of the programs they consider. For both tools, our test
harness terminates the search once the expected solution has been found (or
the timeout of 300 seconds has been reached). We report the average time to
expected solution over three runs. We configured Hectare to perform static
reduction on all constructs prior to running the fast enumeration procedure of
§4.3, repeating this operation up to 30 rounds or until the automaton
converges.

Figure 16. Benchmarks solved vs time for Hectare and Hoogle+ on Hoogle+
benchmarks.

Figure 17. Synthesis times of Hectare against Hoogle+ on Hoogle+ benchmarks.

_Results._ Fig. 17 plots the number of benchmarks solved _vs._ time for both
synthesizers. Within the timeout, Hectare solves 43 out of 45 benchmarks,
whereas Hoogle+ only solves 39. Importantly, as we show in Fig. 17, on
commonly solved benchmarks Hectare is significantly faster: it achieves an
average speedup (geometric mean) of $7\times$ on this suite, solving all but
two tasks faster than Hoogle+. Fast synthesis times are especially important
if a synthesizer is to be used interactively. As shown in the zoomed-in
scatter plot in Fig. 17 (right), Hectare also vastly outperforms Hoogle+ if we
consider a shorter timeout of seven seconds, commonly used for interactive
synthesizers (Ferdowsifard et al., 2021); in fact, Hectare solves 84% of the
benchmarks within seven seconds.

The poor performance of Hoogle+ can be mainly attributed to the brittleness of
the abstraction-refinement loop it uses to support polymorphic components
(§6.2). For example, the headLast benchmark from Tab. 1 is one of the queries
where Hoogle+ times out, while Hectare only takes 2.5 seconds. Upon closer
inspection, Hoogle+ is unable to create an accurate type abstraction for this
query and ends up wasting a lot of time enumerating ill-typed terms. Hectare,
in contrast, natively supports polymorphic components via recursive nodes,
which leads to more predictable performance. On the other hand, the two
benchmarks where Hectare is slower than Hoogle+ both involve deconstructing a
Pair and using both of its fields (both from Tab. 1 is one of these
benchmarks). Hoogle+ solves these queries using a special treatment of Pairs:
it introduces a single component that projects both fields of a pair
simultaneously, which makes the solutions to these queries much shorter; in
Hectare, we did not find a straightforward way to add this trick.

In general, we conclude that _Hectare is effective in solving type-driven
synthesis tasks and outperforms a state-of-the-art tool on 89% of their
benchmarks with $7\times$ speedup on average_.

###  7.2. Comparison on StackOverflow Benchmarks

_Benchmark Selection._ Recall that another limitation of Hoogle+ we discussed
in §6.2 is its restricted support for higher-order functions. In fact, the
original Hoogle+ configuration contains only _nine_ components whose nullary
versions are added to the Petri net (and which consequently can appear in
arguments to higher-order functions). In order to push the limits of both
tools and demonstrate the benefits of Hectare’s native encoding, we assembled
an additional benchmark suite focusing on higher-order functions. To this end,
we searched StackOverflow for Haskell programming questions; for each
question, we attempted to construct an expected solution using only
applications of library components; we excluded tasks that can be solved
without higher-order functions or require unsupported features (such as
higher-kinded type variables and inner lambda abstractions). This left us with
19 synthesis queries. The new benchmark suite is generally more complex than
the original Hoogle+ suite: expected solutions range in size from 4 to 9, with
the average of 6.2; all of these programs include partial applications as
arguments to higher-order components. Three sample queries are shown at the
bottom of Tab. 1.

_Experiment Setup._ To run the newly collected benchmarks, we augmented the
original component set from Hoogle+ with seven components required in these
benchmarks. We also created a variant of Hoogle+ called HplusAll, in which we
added nullary copies of all components into the Petri net (HplusAll thus has
the same expressiveness as Hectare). As before, we record the time to expected
solution, repeat the measurement three times, and report the average time; to
accommodate the increased benchmark complexity, we use a longer timeout of 600
seconds.

Figure 18. Comparison of synthesis time on higher-order benchmarks between
Hectare and HplusAll.

Figure 19. Comparison of synthesis performance between Hectare and its two
variants.

_Results._ Unsurprisingly, the original Hoogle+ cannot solve any of the new
benchmarks: most of them require using new components in higher-order
arguments (and the rest are simply too large). The results for HplusAll and
Hectare are shown in Fig. 19. Although the search space of HplusAll does
include all the new benchmarks, it still fares poorly, solving only 3 out of
19. The reason is that adding nullary versions of all components blows up the
Petri net and makes the reachability problem intractable. In contrast,
Hectare’s native support for partial applications enables it to solve 13 out
of 19 tasks in this challenging suite, achieving $40\times$ speedup on the
three commonly solved benchmarks. We therefore conclude that _the benefits of
ecta-based synthesis are even more pronounced on larger benchmarks focused on
higher-order functions_.

###  7.3. Benefits of Static and Dynamic Reduction

_Experiment Setup._ To isolate the contributions of static and dynamic
reduction, we compare Hectare with its three variants: Hectare-StaticOnly,
Hectare-DynamicOnly, and Hectare-Naïve, which forgo one or both kinds of
reduction, respectively. Specifically, both Hectare-StaticOnly and Hectare-
Naïve, use a naïve “rejection-sampling” enumeration. Note that in the presence
of recursive nodes, such as the any type, the naïve enumeration tends to get
“stuck”, constructing infinitely many spurious terms and never finding one
that satisfies the constraints. To prevent this behavior, we limit the
unfolding depth of recursive nodes to three, which is sufficient to solve all
the benchmarks. We run the three variants on the Hoogle+ benchmarks with a
timeout of 300 seconds and report the average time to expected solution over
three runs.

_Results._ Fig. 19 plots the number of benchmarks solved _vs._ time for
Hectare and its variants. Hectare-Naïve is omitted from the plot because it
cannot solve _any benchmarks_ : it spends most of its time unfolding the
recursive any node, or in other words, blindly going through all possible
instantiations of every polymorphic component. The other two variants fare
significantly better: Hectare-StaticOnly and Hectare-DynamicOnly are able to
solve 34 and 36 tasks, respectively. That said, as the tasks get harder,
Hectare still outperforms these variants drastically: in particular, the
variants cannot solve any benchmarks of size six or larger.

A closer look at Fig. 19 reveals a curious difference: Hectare-StaticOnly is
“all-or-nothing”: it performs as well as Hectare on easy benchmarks, but then
completely falls flat; Hectare-DynamicOnly, in contrast, demonstrates a more
gradual degradation of performance. To understand why, recall that the biggest
time sink during enumeration is blindly unfolding the recursive any nodes.
Static reduction can sometimes get rid of any nodes entirely, making the
resulting ECTA small enough that any enumeration algorithm would do; when it
fails to do so, however, naïve enumeration spends all its time in any nodes.
Dynamic reduction, on the other hand, provides a more gradual yet robust
approach to dealing with any nodes, via Suspend. In summary, we find that
_both static and dynamic reduction individually are critical to the
performance of ECTA-based programs synthesis, and moreover, they complement
each other’s strengths._

##  8\. Related Work

_Constrained Tree Automata._ Tree automata have long been used to represent
sets of terms in term rewriting (Dauchet, 1993; Feuillade et al., 2004; Geser
et al., 2007), and we are not the first to consider adding equality
constraints to handle nonlinear rewrites. In fact, in 1995, Dauchet introduced
a data structure very similar to our ECTAs, called _reduction automata_
(Dauchet et al., 1995). In fact, reduction automata are more expressive than
ECTAs, as they also allow _disequality constraints_ , including disequalities
(but not equalities) on cycles. Unfortunately, allowing disequalities—or other
classes of constraints for that matter—precludes efficient static and dynamic
reduction based on automata intersection. For that reason, we consider ECTAs
to be a sweet spot: expressive enough to encode a variety of interesting
problems, yet restricted enough to enable fast enumeration.

Other prior work on constrained tree automata (Bogaert et al., 1999; Bogaert
and Tison, 1992; Barguñó et al., 2010, 2013; Reuß and Seidl, 2010) similarly
focuses on theoretical aspects, such as worst-case complexity and decidability
results, and we have found no reference to these data structures being used in
a practical system in the $30$ years since their introduction.

Attribute grammars (Knuth, 1968; Paakki, 1995; Van Wyk et al., 2010) augment
context-free grammars with a number of equations of the form
$\left<\text{attribute}\right>=\left<\text{expression}\right>$. This notation
resembles a constraint system over trees, but those equations are actually
unidirectional assignments; attribute grammars compute values over trues, but
do not constrain them.

_Unconstrainted FTAs, VSAs, and E-Graphs._ In contrast to the purely
theoretical work on constrained tree automata, their unconstrained
counterparts, as well as VSAs and e-graphs, have enjoyed practical
applications in program synthesis (Wang et al., 2017, 2018; Gulwani, 2011;
Polozov and Gulwani, 2015; Nandi et al., 2020, 2021; Willsey et al., 2020) and
related areas, such as theorem proving (Detlefs et al., 2005),
superoptimization (Yang et al., 2021), and semantic code search (Premtoon et
al., 2020). One important feature of these data structures, which ECTAs
currently lack, is the ability extract an optimal term according to a user-
defined cost function. It is not surprising that ECTAs have a slightly
different focus, since in the presence of constraints extracting or
enumerating terms regardless of cost becomes nontrivial—at least as hard as
SAT solving. Consequently, extracting optimal terms would be akin to MaxSAT
solving (Krentel, 1986); we leave this non-trivial extension to future work.

Finally note that unlike FTAs and VSAs, e-graphs are used to represent a
_congruence relation_ over terms, as opposed to an arbitrary term space; hence
adding equality constraints to an e-graph is less meaningful. Returning to our
introductory example in Fig. 1, an e-graph equivalent to the FTA in 1(b) would
actually encode that $\mathsf{a}$, $\mathsf{b}$, and $\mathsf{c}$, are all
_equivalent_ to each other; hence it is hard to imagine why one would want to
represent only the terms of the form $+(f(X),f(X))$ but not $+(f(X),f(Y))$,
because all these terms are equivalent.

##  9\. Conclusions and Future Work

This paper has introduced _equality-constrained tree automata_ (ECTAs) and
contributed an efficient implementation of this new data structure in the ecta
library. We think of ECTAs as a general-purpose language for expressing
constraints over terms, and the ecta library as a solver for these
constraints. Although in this paper we only discussed two concrete examples of
properties that can be encoded with ECTAs—boolean satisfiability and well-
typing—in the future we hope to see many fruitful applications in a wide range
of domains.

_ECTA _vs._ SMT._ Instead of developing a custom solver for ECTAs, wouldn’t it
be better to simply translate ECTAs into SAT or SMT constraints, and use
existing, well-engineered solvers? A natural idea is to introduce a variable
per ECTA node, whose value represents the choice of incoming transition, and
to translate ECTA constraints into equalities between these variables. This
simple idea, however, does not work: because the choice is made independently
every time a node is visited, this encoding would require unfolding the ECTA
_into a tree_. This is a complete non-starter for cyclic ECTAs (like the
Hectare encoding of §6.2), since the corresponding tree is infinite. For
acyclic ECTAs, the tree is finite but might be exponential in the size of the
ECTA (since we need to “un-share” all the shared paths in the DAG).

More generally, the problem of finding an ECTA inhabitant is not in
$\mathsf{NP}$, because the smallest tree represented by an ECTA can be
exponential in the size of the ECTA (as we illustrated in Fig. 10); hence a
general and efficient SAT encoding is not possible. Although future work might
develop a clever SMT encoding using advanced theories, we believe this problem
is far from trivial. After all, Hoogle+ uses an SMT encoding that is
specifically tailored to the type inhabitation problem (_i.e._ it is less
general than ECTA), and yet it is less efficient. As we discussed in §6.2, the
main source of this inefficiency is polymorphism, which makes the search space
of types _infinite_ and precludes a “one-shot” SMT encoding, requiring Hoogle+
to go through a series of finite approximations of the space of types to
consider. Instead, a cyclic ECTA is able to represent the entire infinite
space of types at once, and ECTA enumeration is able to explore this space
efficiently, as our experiments show. We anticipate that ECTAs will outperform
SMT solvers on other similar problems that require searching an _infinite yet
constrained space of terms_.

_Future Work._ One avenue for extension is to enrich the constraint language
supported by ECTAs. The key ingredient for efficiency is that there exists a
constraint-propagation mechanism that can be interleaved with Choose.
Intersection is this constraint-propagation mechanism for equality, but there
may be others. For example, one of our anonymous reviewers suggests that
disequality constraints could be processed by creating an alternative rule to
Suspend which tracks both sides of a disequality, and modifying Choose to
discharge disequality constraints or propagate them into subterms as symbols
are selected.

Another path for extension is to relax the requirement for no constraints on
cycles. The careful reader may notice that Theorem 5.1 only impedes emptiness-
checking; enumerating all satisfying terms up to a fixed size is trivially
decidable. Currently Hectare creates many ECTA nodes for different term sizes,
using a meta-program to iterate through successive ECTAs. With constraints on
cycles, this meta-program could be internalized, shortening the Hectare
implementation even further.

## References

  * (1)
  * Adams and Might (2017) Michael D Adams and Matthew Might. 2017.  Restricting Grammars with Tree Automata.  _Proceedings of the ACM on Programming Languages_ 1, OOPSLA (2017), 1–25.
  * Bachmair and Dershowitz (1994) Leo Bachmair and Nachum Dershowitz. 1994.  Equational Inference, Canonical Proofs, and Proof Orderings.  _Journal of the ACM (JACM)_ 41, 2 (1994), 236–276.
  * Barguñó et al. (2010) Luis Barguñó, Carles Creus, Guillem Godoy, Florent Jacquemard, and Camille Vacher. 2010.  The Emptiness Problem for Tree Automata with Global Constraints. In _2010 25th Annual IEEE Symposium on Logic in Computer Science_. IEEE, 263–272.
  * Barguñó et al. (2013) Luis Barguñó, Carles Creus, Guillem Godoy, Florent Jacquemard, and Camille Vacher. 2013\.  Decidable Classes of Tree Automata Mixing Local and Global Constraints Modulo Flat Theories.  _Logical Methods in Computer Science_ 9 (02 2013).  https://doi.org/10.2168/LMCS-9(2:1)2013
  * Bogaert et al. (1999) Bruno Bogaert, Franck Seynhaeve, and Sophie Tison. 1999\.  The Recognizability Problem for Tree Automata with Comparisons Between Brothers. In _International Conference on Foundations of Software Science and Computation Structure_. Springer, 150–164.
  * Bogaert and Tison (1992) Bruno Bogaert and Sophie Tison. 1992.  Equality and Disequality Constraints on Direct Subterms in Tree Automata. In _Annual Symposium on Theoretical Aspects of Computer Science_. Springer, 159–171.
  * Dauchet (1993) Max Dauchet. 1993\.  Rewriting and Tree Automata. In _French School on Theoretical Computer Science_. Springer, 95–113.
  * Dauchet et al. (1995) Max Dauchet, Anne-Cécile Caron, and Jean-Luc Coquidé. 1995.  Automata for Reduction Properties Solving.  _Journal of Symbolic Computation_ 20, 2 (1995), 215–233.
  * de Moura and Bjørner (2007) Leonardo Mendonça de Moura and Nikolaj Bjørner. 2007.  Efficient E-Matching for SMT Solvers.. In _CADE_ _(Lecture Notes in Computer Science, Vol. 4603)_. Springer, 183–198.
  * Dershowitz (1987) Nachum Dershowitz. 1987\.  Termination of Rewriting.  _Journal of Symbolic Computation_ 3, 1-2 (1987), 69–115.
  * Detlefs et al. (2005) David Detlefs, Greg Nelson, and James B Saxe. 2005\.  Simplify: A Theorem Prover for Program Checking.  _Journal of the ACM (JACM)_ 52, 3 (2005), 365–473.
  * Feng et al. (2017) Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps. 2017.  Component-based synthesis for complex APIs. In _POPL_.
  * Ferdowsifard et al. (2021) Kasra Ferdowsifard, Shraddha Barke, Hila Peleg, Sorin Lerner, and Nadia Polikarpova. 2021\.  LooPy: Interactive Program Synthesis with Control Structures.  _Proc. ACM Program. Lang._ 5, OOPSLA, Article 153 (oct 2021), 29 pages.  https://doi.org/10.1145/3485530
  * Feuillade et al. (2004) Guillaume Feuillade, Thomas Genet, and Valérie Viet Triem Tong. 2004.  Reachability Analysis over Term Rewriting Systems.  _Journal of Automated Reasoning_ 33, 3 (2004), 341–383.
  * Geser et al. (2007) Alfons Geser, Dieter Hofbauer, Johannes Waldmann, and Hans Zantema. 2007.  On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems.  _Information and Computation_ 205, 4 (2007), 512–534.
  * Gissurarson (2018) Matthías Páll Gissurarson. 2018\.  Suggesting Valid Hole Fits for Typed-Holes (Experience Report). In _Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell_ (St. Louis, MO, USA) _(Haskell 2018)_. Association for Computing Machinery, 179–185.
  * Gulwani (2011) Sumit Gulwani. 2011\.  Automating String Processing in Spreadsheets using Input-Output Examples.  _ACM Sigplan Notices_ 46, 1 (2011), 317–330.
  * Guo et al. (2020) Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova. 2020.  Program synthesis by type-guided abstraction refinement.  _Proc. ACM Program. Lang._ 4, POPL (2020), 12:1–12:28.
  * Heineman et al. (2016) George T. Heineman, Jan Bessai, Boris Düdder, and Jakob Rehof. 2016.  A Long and Winding Road Towards Modular Synthesis. In _Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I_. 303–317.  https://doi.org/10.1007/978-3-319-47166-2_21
  * James et al. (2020) Michael B James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, and Nadia Polikarpova. 2020.  Digging for Fold: Synthesis-Aided API Discovery for Haskell.  _Proceedings of the ACM on Programming Languages_ 4, OOPSLA (2020), 1–27.
  * Knuth (1968) Donald E Knuth. 1968\.  Semantics of Context-Free Languages.  _Mathematical Systems Theory_ 2, 2 (1968), 127–145.
  * Koppel (2021) James Koppel. 2021\.  Version Space Algebras are Acyclic Tree Automata.  arXiv:2107.12568 [cs.PL]
  * Krentel (1986) M W Krentel. 1986\.  The Complexity of Optimization Problems. In _Proceedings of the Eighteenth Annual ACM Symposium on Theory of Computing_ (Berkeley, California, USA) _(STOC ’86)_. Association for Computing Machinery, New York, NY, USA, 69–76.  https://doi.org/10.1145/12130.12138
  * Lau et al. (2003) Tessa Lau, Steven A Wolfman, Pedro Domingos, and Daniel S Weld. 2003.  Programming by Demonstration Using Version Space Algebra.  _Machine Learning_ 53, 1 (2003), 111–156.
  * Mitchell (2004) Neil Mitchell. 2004\.  Hoogle.  https://www.haskell.org/hoogle/.
  * Nandi et al. (2020) Chandrakana Nandi, Max Willsey, Adam Anderson, James R Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock. 2020.  Synthesizing Structured CAD models with Equality Saturation and Inverse Transformations. In _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_. 31–44.
  * Nandi et al. (2021) Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, and Zachary Tatlock. 2021.  Rewrite Rule Inference Using Equality Saturation.  _Proc. ACM Program. Lang._ 5, OOPSLA, Article 119 (oct 2021), 28 pages.  https://doi.org/10.1145/3485496
  * Nelson and Oppen (1980) Greg Nelson and Derek C. Oppen. 1980.  Fast Decision Procedures Based on Congruence Closure.  _J. ACM_ 27, 2 (1980), 356–364.
  * Nieuwenhuis et al. (2006) Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. 2006\.  Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL (T).  _Journal of the ACM (JACM)_ 53, 6 (2006), 937–977.
  * Oliveira and Cook (2012) Bruno CdS Oliveira and William R Cook. 2012.  Functional Programming with Structured Graphs. In _Proceedings of the 17th ACM SIGPLAN international conference on Functional programming_. 77–88.
  * Paakki (1995) Jukka Paakki. 1995\.  Attribute Grammar Paradigms—A High-Level Methodology in Language Implementation.  _ACM Computing Surveys (CSUR)_ 27, 2 (1995), 196–255.
  * Pollock and Haan (2021) Joshua Pollock and Altan Haan. 2021.  E-Graphs Are Minimal Deterministic Finite Tree Automata (DFTAs) · Discussion #104 · egraphs-good/egg.  https://github.com/egraphs-good/egg/discussions/104
  * Polozov and Gulwani (2015) Oleksandr Polozov and Sumit Gulwani. 2015.  FlashMeta: A Framework for Inductive Program Synthesis. In _Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications_. 107–126.
  * Premtoon et al. (2020) Varot Premtoon, James Koppel, and Armando Solar-Lezama. 2020\.  Semantic Code Search via Equational Reasoning. In _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_. 1066–1082.
  * Reuß and Seidl (2010) Andreas Reuß and Helmut Seidl. 2010.  Bottom-up Tree Automata with Term Constraints. In _International Conference on Logic for Programming Artificial Intelligence and Reasoning_. Springer, 581–593.
  * Tate et al. (2009) Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. 2009\.  Equality Saturation: A New Approach to Optimization. In _Proceedings of the 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_. 264–276.
  * Urzyczyn (1997) Pawel Urzyczyn. 1997\.  Inhabitation in Typed Lambda-Calculi (A Syntactic Approach). In _Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA ’97, Nancy, France, April 2-4, 1997, Proceedings_. 373–389.  https://doi.org/10.1007/3-540-62688-3_47
  * Van Wyk et al. (2010) Eric Van Wyk, Derek Bodin, Jimin Gao, and Lijesh Krishnan. 2010.  Silver: An Extensible Attribute Grammar System.  _Science of Computer Programming_ 75, 1-2 (2010), 39–54.
  * Wang et al. (2017) Xinyu Wang, Isil Dillig, and Rishabh Singh. 2017.  Synthesis of Data Completion Scripts using Finite Tree Automata.  _Proceedings of the ACM on Programming Languages_ 1, OOPSLA (2017), 1–26.
  * Wang et al. (2018) Xinyu Wang, Isil Dillig, and Rishabh Singh. 2018.  Program synthesis using abstraction refinement.  _Proc. ACM Program. Lang._ 2, POPL (2018), 63:1–63:30.  https://doi.org/10.1145/3158151
  * Willsey et al. (2020) Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2020\.  egg: Fast and Extensible Equality Saturation.  _arXiv preprint arXiv:2004.03082_ (2020).
  * Yang et al. (2021) Yichen Yang, Phitchaya Phothilimthana, Yisu Wang, Max Willsey, Sudip Roy, and Jacques Pienaar. 2021\.  Equality Saturation for Tensor Graph Superoptimization. In _Proceedings of Machine Learning and Systems_ , A. Smola, A. Dimakis, and I. Stoica (Eds.), Vol. 3. 255–268.  https://proceedings.mlsys.org/paper/2021/file/65ded5353c5ee48d0b7d48c591b8f430-Paper.pdf

##  Appendix A Proofs and Additional Formalization

See 3.5

###### Proof.

The reverse direction is trivial, since $\mathsf{cl}(C)$ is a superset of $C$.
Let us focus on the forward direction: that is, pick a $t$ that satisfies $C$
and show that it satisfies $\mathsf{cl}(C)$. The proof is by induction on the
number of steps, where each step constructs a new approximation of the
closure, $C^{n+1}$, by adding a new path $p^{\prime\prime}.p$ to a PEC
$c_{2}\in C^{n}$ if $\exists c_{1}\in C^{n}$ such that
$p^{\prime},p^{\prime\prime}\in c_{1}$ and $p^{\prime}.p\in c_{2}$ but
$p^{\prime\prime}.p\notin c_{2}$. We need to show that if $t\models C^{n}$
then also $t\models C^{n+1}$.

Assume $t\models C^{n}$. Then there exists a unique $t^{\prime}$ such that
$t^{\prime}=t|_{p^{\prime}}=t|_{p^{\prime\prime}}$. But then
$t|_{p^{\prime}.p}=t^{\prime}|_{p}=t|_{p^{\prime\prime}.p}$. Hence $t$
satisfies the new PEC $c_{2}^{\prime}=c_{2}\cup\\{p^{\prime\prime}.p\\}$, and
hence satisfies $C^{n+1}$. ∎

See 3.6

###### Proof.

It is easy to see that a non-prefix-free PEC is inconsistent.

For the reverse direction, we shall show that if each of the $c_{i}$ are
prefix-free, then $C$ is consistent. Consider $c_{1},c_{2}\in C$, and define
$c_{1}\sqsubseteq c_{2}$ if $\exists p_{1}\in c_{1},p_{2}\in c_{2}$ such that
$p_{1}$ is a subpath of $p_{2}$. We show that $\sqsubseteq$ is a partial
order. Reflexivity and transitivity are trivial. For anti-symmetry: suppose
$p_{1},p_{3}\in c_{1}$ and $p_{2},p_{4}\in c_{2}$ with $p_{1}$ a subpath of
$p_{2}$, $p_{4}$ a subpath of $p_{3}$. If $c_{1}=c_{2}$, we are done;
otherwise, we must have $p_{1}\neq p_{2}$ and $p_{3}\neq p_{4}$ by
completeness of $C$. We can thus write $p_{2}=p_{1}.p^{\prime}_{2}$,
$p_{3}=p_{4}.p^{\prime}_{3}$ for some
$p^{\prime}_{2},p^{\prime}_{3}\neq\epsilon$. By completeness of $C$, it
follows that $c_{1}$ contains
$p_{1}=p_{3}=p_{4}.p^{\prime}_{3}=p_{2}.p^{\prime}_{3}=p_{1}.p^{\prime}_{2}.p^{\prime}_{3}$,
which would mean that $c_{1}$ is not prefix-free. Thus, $\sqsubseteq$ is a
partial order.

Because $C$ can be topologically sorted by $\sqsubseteq$, it is trivially
possible to construct a term $t$ such that $C(t)$ by inductively choosing a
term for each successive minimal $c_{i}$. Thus, if each of the $c_{i}$ are
prefix-free, $C$ is consistent. ∎

See 3.19

###### Proof.

Let $e^{\prime}=\mathsf{reduce}(e,c)$, let $p_{i},p_{j}\in c$, and suppose
there is $n\in\mathsf{nodes}(e^{\prime},p_{i})$ such that $n\sqcap
e^{\prime}|_{p_{j}}=\bm{\mathtt{U}}_{\bot}$. Let $n^{*}$ be as defined in
3.18. Then $n\sqcap n^{*}=\bm{\mathtt{U}}_{\bot}$ by associativity. Then
$n\notin\mathsf{nodes}(e|_{p_{i}}^{\sqcap n^{*}},p_{i})$. Because $c$ is
prefix-free, no successive intersect-at-path operation in the definition of
$\mathsf{reduce}(e,c)$ can alter this property, and so
$n\notin\mathsf{reduce}(e,c)$. Therefore, there is no such $n$ with $n\sqcap
e^{\prime}|_{p_{j}}=\bm{\mathtt{U}}_{\bot}$, and so $\mathsf{reduce}(e,c)$
satisfies the reduction criterion for $c$. ∎

See 3.20

###### Proof.

Let $c=\\{p_{1}=\dots=p_{k}\\}$. Without loss of generality, it suffices to
show that $\llbracket e|_{p_{1}}^{\sqcap n^{*}}\rrbracket^{E}=\llbracket
e\rrbracket^{E}$, where $n^{*}$ is defined as in 3.18. We know from
monotonicity that $\llbracket e|_{p_{i}}^{\sqcap
n^{*}}\rrbracket^{E}\subseteq\llbracket e\rrbracket^{E}$, so we need only show
$\llbracket e|_{p_{i}}^{\sqcap n^{*}}\rrbracket^{E}\supseteq\llbracket
e\rrbracket^{E}$.

Consider a term $t\in\llbracket e\rrbracket^{E}$. Then, by definition,
$t\models c$, and $t|_{c}\in\llbracket e|_{p_{i}}\rrbracket^{N}$ for all $i$
by Theorem 3.14, and so $t|_{c}\in\llbracket n^{*}\rrbracket^{N}$ by the
properties of intersection and the definition of $n^{*}$. Since
$t|_{c}\in\llbracket e|_{p_{1}}\rrbracket^{N}$, so $t|_{p_{1}}\in\llbracket
n^{*}\rrbracket^{N}$. Hence $t\in\llbracket e|_{p_{i}}^{\sqcap
n^{*}}\rrbracket^{E}$, so $\llbracket e|_{p_{i}}^{\sqcap
n^{*}}\rrbracket^{E}\supseteq\llbracket e\rrbracket^{E}$. ∎

###  A.1. Undecidable ECTAs

Figure 20. Example encoding of the PCP problem into an ECTA with constraints
on cycles

See 5.1

###### Proof.

By reduction from the Post Correspondence Problem. Consider the instance of
the PCP problem with three cards $(a,baa),(ab,aa),$ and $(bba,bb)$. Any term
represented by the ECTA in Fig. 20 encodes either a solution to this instance
or is the empty solution $\text{final}(\text{end}(\\#,\\#))$. We leave it as
an exercise to the reader to generalize this construction to other instances,
and to unroll this ECTA so as to exclude the empty solution. ∎

###  A.2. Enumeration State

_Denotation._ Defining the denotation of a partially-enumerated term is tricky
because of a circular reference: enumeration states contain partially
enumerated terms, which in turn can reference other parts of the enumeration
state.

We choose to break this circularity by giving an _impredicative_ definition.
Each of the cases in the definition is presented as a _filter_ on the space of
all possible substitutions. The denotation of a partially-enumerated term is a
set of pairs $(t,\rho)$, where the $t$ range over all all terms it may
represent, and the $\rho$ range over all possible substitutions $\rho$
compatible with this choice of term. Intersecting these filtered sets of all
possible substitutions, and then restricting the substitutions to the set of
variables actually used (written $\rho\big{|}_{\text{dom}(\sigma)}$), gives
the desired set of substitutions compatible with the constraints of $\sigma$.

###### Definition A.1 (Denotation of Enumeration State).

$\displaystyle\llbracket\cdot\rrbracket^{PT}_{\sigma}$
$\displaystyle\mathrel{:}\tau\times(\textsf{Var}\rightharpoonup\tau)\rightarrow(\mathbb{P}(\mathcal{T}(\Sigma))\times(\textsf{Var}\rightarrow\tau))$
$\displaystyle\llbracket s(\overline{\tau_{i}})\rrbracket^{PT}_{\sigma}$
$\displaystyle=\left\\{(s(\overline{t_{i}}),\rho)\mathrel{\Big{|}}(t_{i},\rho_{i})\in\llbracket\tau_{i}\rrbracket^{PT}_{\sigma},\rho\text{
arbitrary},\forall j\forall v,\rho(v)=\rho_{j}(v)\right\\}$
$\displaystyle\llbracket\square(n,\overline{\langle
c_{i}=v_{i}\rangle})\rrbracket^{PT}_{\sigma}$
$\displaystyle=\left\\{(t,\rho)\mathrel{\Big{|}}\rho\text{
arbitrary},t\in\llbracket n\rrbracket^{N},t\models\overline{\langle
c_{i}=v_{i}\rangle},t|_{c_{i}}=\rho(v_{i})\right\\}$ $\displaystyle\llbracket
v\rrbracket^{PT}$
$\displaystyle=\left\\{(t,\rho)\mathrel{\Big{|}}(t,\rho)\in\llbracket\sigma[v]\rrbracket^{PT},\rho(v)=t\right\\}$
$\displaystyle\llbracket\sigma\rrbracket^{S}$
$\displaystyle\mathrel{:}(\textsf{Var}\rightharpoonup\tau)\rightarrow(\textsf{Var}\to\mathbb{P}(\mathcal{T}(\Sigma)))$
$\displaystyle\llbracket\sigma\rrbracket^{S}$
$\displaystyle=\left\\{\rho\big{|}_{\text{dom}(\sigma)}\mathrel{\Big{|}}(t_{v},\rho)\in\llbracket\sigma(v)\rrbracket^{PT},\rho(v)=t_{v}\right\\}$

###### Example A.2.

Let $v_{\top}=v_{0}$ and consider the enumeration state

$\displaystyle\sigma=[v_{0}$ $\displaystyle\mapsto
f(\square(\bm{\mathtt{U}}(\bm{\Pi}(a),\bm{\Pi}(b)),\langle\epsilon=v_{1}\rangle),v_{1}),$
$\displaystyle v_{1}$
$\displaystyle\mapsto\square(\bm{\mathtt{U}}(\bm{\Pi}(a),\bm{\Pi}(b)))]$

Then

$\llbracket\sigma(v_{1})\rrbracket^{PT}=\bigcup_{\rho}\left\\{(a,\rho),(b,\rho)\right\\}$

where the union is over all
$\rho\mathrel{:}\textsf{Var}\rightarrow\textsf{Term}$, and

$\llbracket\sigma(v_{0})\rrbracket^{PT}=\big{(}\bigcup_{\rho\big{|}\rho(v_{1})=a}\\{(f(a,\rho(v_{1})),\rho)\\}\big{)}\bigcup\big{(}\bigcup_{\rho\big{|}\rho(v_{1})=b}(f(b,\rho(v_{1})),\rho)\\}\big{)}$

which reduces to the terms $f(a,a)$ and $f(b,b)$ with $\rho(v_{1})$ being $a$
or $b$ accordingly. This yields the final denotation

$\llbracket\sigma\rrbracket^{S}=\left\\{[v_{0}\mapsto f(a,a),v_{1}\mapsto
a],[v_{0}\mapsto f(b,b),v_{1}\mapsto b]\right\\}$

###  A.3. Enumeration Algorithm

###### Definition A.3 (Reachable Enumeration State).

Enumeration state $\sigma$ is a _reachable enumeration state_ if there is an
initial state $\sigma_{0}=[v_{\top}\mapsto\square(n)]$ such that
$\sigma_{0}\longrightarrow^{*}\sigma$.

###### Lemma A.4 (Soundness of Choose-$\square$).

Let $\tau$ be a u-node, and define
$T=\left\\{\tau^{\prime}\middle|\tau\longrightarrow\tau^{\prime}\text{ by
{Choose-}}\square\right\\}$. Then
$\llbracket\tau\rrbracket^{PT}=\bigcup_{\tau^{\prime}\in
T}\llbracket\tau^{\prime}\rrbracket^{PT}$

###### Proof.

By rule Choose-$\square$ and the definition of p-term denotation, we have
$\tau=\square(\bm{\mathtt{U}}(\overline{e}),\overline{\langle
c_{i}=v_{i}\rangle})$, and hence

$\mathbb{T}(\tau)=\\{t\mid
t\in\llbracket\bm{\mathtt{U}}(\overline{e})\rrbracket^{N},t\models\overline{\langle
c_{i}=v_{i}\rangle}\\}$

By the definition of node denotation, we have that

$\mathbb{T}(\tau)=\\{t\mid
t\in\bigcup_{\bm{\Pi}(s,\overline{n^{j}},c)\in\overline{e}}\llbracket\bm{\Pi}(s,\overline{n^{j}},c)\rrbracket^{E},t\models\overline{\langle
c_{i}=v_{i}\rangle}\\}$