Synthesis of Recursive ADT Transformations
from Reusable Templates
Jeevana Priya Inala1 , Nadia Polikarpova1 , Xiaokang Qiu2 , Benjamin S. Lerner3 ,
and Armando Solar-Lezama1

arXiv:1507.05527v3 [cs.PL] 16 Apr 2017

1

MIT
3

{jinala, polikarn, asolar}@csail.mit.edu
2
Purdue University xkqiu@purdue.edu
Northeastern University blerner@ccs.neu.edu

Abstract. Recent work has proposed a promising approach to improving
scalability of program synthesis by allowing the user to supply a syntactic
template that constrains the space of potential programs. Unfortunately,
creating templates often requires nontrivial effort from the user, which
impedes the usability of the synthesizer. We present a solution to this
problem in the context of recursive transformations on algebraic datatypes. Our approach relies on polymorphic synthesis constructs: a small but
powerful extension to the language of syntactic templates, which makes it
possible to define a program space in a concise and highly reusable manner,
while at the same time retains the scalability benefits of conventional
templates. This approach enables end-users to reuse predefined templates
from a library for a wide variety of problems with little effort. The paper
also describes a novel optimization that further improves the performance
and the scalability of the system. We evaluated the approach on a set of
benchmarks that most notably includes desugaring functions for lambda
calculus, which force the synthesizer to discover Church encodings for
pairs and boolean operations.

1

Introduction

Recent years have seen remarkable advances in tools and techniques for automated
synthesis of recursive programs [8,1,13,4,16]. These tools take as input some form
of correctness specification that describes the intended program behavior, and a
set of building blocks (or components). The synthesizer then performs a search
in the space of all programs that can be built from the given components until
it finds one that satisfies the specification. The biggest obstacle to practical
program synthesis is that this search space grows extremely fast with the size of
the program and the number of available components. As a result, these tools
have been able to tackle only relatively simple tasks, such as textbook data
structure manipulations.
Syntax-guided synthesis (SyGuS) [2] has emerged as a promising way to
address this problem. SyGuS tools, such as Sketch [18] and Rosette [20,21]
leverage a user-provided syntactic template to restrict the space of programs the
synthesizer has to consider, which improves scalability and allows SyGus tools to

tackle much harder problems. However, the requirement to provide a template
for every synthesis task significantly impacts usability.
This paper shows that, at least in the context of recursive transformations
on algebraic data-types (ADTs), it is possible to get the best of both worlds.
Our first contribution is a new approach to making syntactic templates highly
reusable by relying on polymorphic synthesis constructs (PSC s). With PSC s,
a user does not have to write a custom template for every synthesis problem,
but can instead rely on a generic template from a library. Even when the user
does write a custom template, the new constructs make this task simpler and
less error-prone. We show in Section 4 that all our 23 diverse benchmarks are
synthesized using just 4 different generic templates from the library. Moreover,
thanks to a carefully designed type-directed expansion mechanism, our generic
templates provide the same performance benefits during synthesis as conventional,
program-specific templates. Our second contribution is a new optimization called
inductive decomposition, which achieves asymptotic improvements in synthesis
times for large and non-trivial ADT transformations. This optimization, together
with the user guidance in the form of reusable templates, allows our system to
attack problems that are out of scope for existing synthesizers.
We implemented these ideas in a tool called SyntRec, which is built on
top of the open source Sketch synthesis platform [19]. Our tool supports expressive correctness specifications that can use arbitrary functions to constrain
the behavior of ADT transformations. Like other expressive synthesizers, such
as Sketch [18] and Rosette [21,20], our system relies on exhaustive bounded
checking to establish whether a program candidate matches the specification.
While this does not provide correctness guarantees beyond a bounded set of
inputs, it works well in practice and allows us to tackle complex problems, for
which full correctness is undecidable and is beyond the state of the art in automatic verification. For example, our benchmarks include desugaring functions
from an abstract syntax tree (AST) into a simpler AST, where correctness is
defined in terms of interpreters for the two ASTs. As a result, our synthesizer
is able to discover Church encodings for pairs and booleans, given nothing but
an interpreter for the lambda calculus. In another benchmark, we show that the
system is powerful enough to synthesize a type constraint generator for a simple
programming language given the semantics of type constraints. Additionally,
several of our benchmarks come from transformation passes implemented in our
own compiler and synthesizer.

2

Overview

In this section, we use the problem of desugaring a simple language to illustrate
the main features of SyntRec. Specifically, the goal is to synthesize a function
dstAST desugar(srcAST src){. . .}, which translates an expression in source AST into
a semantically equivalent expression in destination AST. Data type definitions
for the two ASTs are shown in Figure 1: the type srcAST has five variants (two
of which are recursive), while dstAST has only three. In particular, the source
2

adt dstAST{
NumD{ int v; }
BoolD{ bit v; }
BinaryD{ opcode op; dstAST a; dstAST b;}}

adt srcAST{
NumS{ int v; }
TrueS{ }
FalseS{ }
BinaryS{ opcode op; srcAST a; srcAST b;}
BetweenS{ srcAST a; srcAST b; srcAST c;}}

adt opcode{ AndOp{} OrOp{} LtOp{}}

Fig. 1: ADTs for two small expression languages
language construct BetweenS(a, b, c), which denotes a < b < c, has to be desugared
into a conjunction of two inequalities. Like case classes in Scala, data type variants
in SyntRec have named fields.
Specification. The first piece of user input required by the synthesizer is the
specification of the program’s intended behavior. In the case of desugar, we would
like to specify that the desugared AST is semantically equivalent to the original
AST, which can be expressed in SyntRec using the following constraint:
assert( srcInterpret (exp) == dstInterpret(desugar(exp)) )

This constraint states that interpreting an arbitrary source-language expression exp
(bounded to some depth) must be equivalent to desugaring exp and interpreting the
resulting expression in the destination language. Here, srcInterpret and dstInterpret
are regular functions written in SyntRec and defined recursively over the
structure of the respective ASTs in a straightforward manner. As we explain
in Section 3.4, our synthesizer contains a novel optimization called inductive
decomposition that can take advantage of the structure of the above specification
to significantly improve the scalability of the synthesis process.
Templates. The second piece of user input required by our system is a syntactic
template, which describes the space of possible implementations. The template
is intended to specify the high-level structure of the program, leaving low-level
details for the system to figure out. In that respect, SyntRec follows the SyGuS
paradigm [2]; however, template languages used in existing SyGuS tools, such as
Sketch or Rosette, work poorly in the context of recursive ADT transformations.
For example, Figure 2 shows a template for desugar written in Sketch, the
predecessor of SyntRec. It is useful to understand this template as we will show,
later, how the new language features in SyntRec allow us to write the same
template in a concise and reusable manner. This template uses three kinds of
synthesis constructs already existing in Sketch: a choice (choose(e1 ,...,en )) must
be replaced with one of the expressions e1 , . . . , en ; a hole (??) must be replaced
with an integer or a boolean constant; finally, a generator (such as rcons) can
be thought of as a macro, which is inlined on use, allowing the synthesizer to
make different choices for every invocation† . The task of the synthesizer is to fill
in every choice and hole in such a way that the resulting program satisfies the
specification.
†

Recursive generators, such as rcons , are unrolled up to a fixed depth, which is a
parameter to our system.

3

dstAST desugar(srcAST src){
switch(src ) {
case NumS:
return rcons( src .v );
... /∗ Some cases are elided ∗/
case BinaryS:
dstAST a = desugar(src.a), b = desugar(src .b);
return rcons(choose(a, b, src .op));
case BetweenS:
dstAST a = desugar(src.a), b = desugar(src .b),
c = desugar(src .c );
return rcons(choose(a, b, c ));
}}

generator dstAST rcons(fun e) {
if (??) return e ();
if (??) {
int val = choose(e(), ??);
return new NumD(v = val); }
if (??) {
bit val = choose(e(), ??);
return new BoolD(v = val);}
if (??) {
dstAST a = rcons(e);
dstAST b = rcons(e);
opcode op = choose(e(), new AndOp(),...,
new LtOp());
return new BinaryD(op = op, a= a, b = b);}
}

Fig. 2: Template for desugar in Sketch
The template in Figure 2 expresses the intuition that desugar should recursively
traverse its input, src , replacing each node with some subtree from the destination language. These destination subtrees are created by calling the recursive,
higher-order generator rcons (for “recursive constructor”). rcons(e) constructs a
nondeterministically chosen variant of dstAST, whose fields, depending on their
type, are obtained either by recursively invoking rcons, by invoking e (which is
itself a generator), or by picking an integer or boolean constant. For example,
one possible instantiation of the template rcons(choose(x, y, src .op)) ‡ can lead to
new BinaryD(op = src.op, a = x, b = new NumD(5)). Note that the template for desugar
provides no insight on how to actually encode each node of scrAST in terms of
dstAST, which is left for the synthesizer to figure out. Despite containing so little
information, the template is very verbose: in fact, more verbose than the full
implementation! More importantly, this template cannot be reused for other
synthesis problems, since it is specific to the variants and fields of the two data
types. Expressing such a template in Rosette will be similarly verbose.
Reusable Templates. SyntRec addresses this problem by extending the template language with polymorphic synthesis constructs (PSC s), which essentially
support parametrizing templates by the structure of data types they manipulate.
As a result, in SyntRec the end user can express the template for desugar with a
single line of code:
dstAST desugar(srcAST src) { return recursiveReplacer ( src , desugar );

}

Here, recursiveReplacer is a reusable generator defined in a library; its code is
shown in Figure 3. When the user invokes recursiveReplacer ( src ,desugar), the body
of the generator is specialized to the surrounding context, resulting in a template
very similar to the one in Figure 2. Unlike the template in Figure 2, however,
recursiveReplacer is not specific to srcAST and dstAST, and can be reused with no
‡

When an expression is passed as an argument to a higher-order function that expects
a function parameter such as rcons , it is automatically casted to a generator lambda
function. Hence, the expression will only be evaluated when the higher-order function
calls the function parameter and each call can result in a different evaluation.

4

1
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

generator T recursiveReplacer <T, Q>(Q src,
fun rec) {
switch(src){
case?:
T[ ] a = map(src.fields?, rec );
return rcons(choose(a[??],
field ( src )));
}}}
generator T rcons<T>(fun e) {
if (??) return e ();
else return new cons?(rcons(e));
}
generator T field <T,S>(S e) {
return (e.fields?) [?? ];
}

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

dstAST desugar(srcAST src) {
switch(src ) {
case NumS: return new NumD(v = src.v);
case TrueS: return new BoolD(v = 1);
case FalseS : return new BoolD(v = 0);
case BinaryS:
dstAST[2] a = {desugar(src.a ), desugar( src .b)};
return new BinaryD(op = src.op, a = a[1],
b = a [2]);
case BetweenS:
dstAST[3] a = {desugar(src.a ), desugar( src .b),
desugar( src .c)};
return new BinaryD(op = new AndOp(),
a = new BinaryD(op = new LtOp(), a = a[0],
b = a[1])
b = new BinaryD(op = new LtOp(), a = a[1],
b = a [2]));
}}

Fig. 3: Left: Generic template for recursiveReplacer Right: Solution to the running
example
modifications to synthesize desugaring functions for other languages, and even
more general recursive ADT transformations. Crucially, even though the reusable
template is much more concise than the Sketch template, it does not increase
the size of the search space that the synthesizer has to consider, since all the
additional choices are resolved during type inference. Figure 3 also shows a
compacted version of the solution for desugar, which SyntRec synthesizes in
about 8s. The rest of the section gives an overview of the PSC s used in Figure 3.
Polymorphic Synthesis Constructs. Just like a regular synthesis construct,
a PSC represents a set of potential programs, but the exact set depends on
the context and is determined by the types of the arguments to a PSC and its
expected return type. SyntRec introduces four kinds of PSC s.
1. A Polymorphic Generator is a polymorphic version of a Sketch generator. For example, recursiveReplacer is a polymorphic generator, parametrized by
types T and Q. When the user invokes recursiveReplacer ( src ,desugar), T and Q are
instantiated with dstAST and srcAST, respectively.
2. Flexible Pattern Matching (switch(x) case?: e) expands into pattern matching code specialized for the type of x. In our example, once Q in recursiveReplacer
is instantiated with srcAST, the case? construct in Line 4 expands into five cases
(case NumS, ..., case BetweenS) with the body of case? duplicated inside each of
these cases.
3. Field List (e. fields? ) expands into an array of all fields of type τ in a particular
variant of e, where τ is derived from the context. Going back to Figure 3, Line
5 inside recursiveReplacer maps a function rec over a field list src . fields? ; in our
example, rec is instantiated with desugar, which takes an input of type srcAST.
Hence, SyntRec determines that src . fields? in this case denotes all fields of type
srcAST. Note that this construct is expanded differently in each of the five cases
that resulted from the expansion of case?. For example, inside case NumS, this
5

construct expands into an empty array (NumS has no fields of type srcAST), while
inside case BetweenS, it expands into the array {src .a, src .b, src .c}.
4. Unknown Constructor (new cons?(e1 , ...,en )) expands into a constructor
for some variant of type τ , where τ is derived from the context, and uses the
expressions e1 , . . . , en as the fields. In our example, the auxiliary generator rcons
uses an unknown constructor in Line 11. When rcons is invoked in a context that
expects an expression of type dstAST, this unknown constructor expands into
choose(new NumD(...), new BoolD(...), new BinaryD(...)). If instead rcons is expected to
return an expression of type opcode, then the unknown constructor expands into
choose(new AndOp(),...,new LtOp()). If the expected type is an integer or a boolean,
this construct expands into a regular Sketch hole (??).
Even though the language provides only four PSC s, they can be combined in
novel ways to create richer polymorphic constructs that can be used as library
components. The generators field and rcons in Figure 3 are two such components.
The field component expands into
P := {adti }i {fi }i
adt := adt name { variant1 . . . variantn }
an arbitrary field of type τ , where τ
variant := name {l1 : τ1 . . . ln : τn }
is derived from the context. Its imθ := τ | T | θ[ ] | f un | θ1 → θ2
τ := prim
plementation uses the field list PSC
 | {li : τi }i<n
P | name
|
namei lki : τki k<n
to obtain the array of all fields of
prim := bit | int
type τ , and then accesses a random
ˆ
f := f | fˆ | fˆ
element in this array using an intef := τout name ({xi : τi }i ) e
ger hole. For example, if field (e) is
fˆ := generator τout name ({xi : τi }i ) e
ˆ
used in a context where the type of
fˆ := generator θout nameh{Ti }i i ({xi : θi }i ) e
e
:= e | ê | êˆ
e is BetweenS and the expected type
e := x | let x : θ = e1 in e2 | f (e)
is srcAST, then field (e) expands into
| switch (x) { case namei : ei }i
{e.a, e.b, e.c}[??] which is semantically
| e.l | new name({li = ei }i )
| {{ei }i } | e1 [e2 ] | assert (e)
equivalent to choose(e.a, e.b, e.c).
ê := ?? | choose({ei }i )| fˆ(e)
The rcons component is a polymorˆ
êˆ := fˆ(e) | new cons?({ei }i )
phic version of the recursive construc| e. fields? | switch(x){case? : e}
tor for dstAST in Figure 2, and can produce ADT trees of any type up to a
Fig. 4: Kernel language
certain depth. Note that since rcons is
a polymorphic generator, each call to rcons in the argument to the unknown
constructor (Line 11) is specialized based on the type required by that constructor and can make different non-deterministic choices. Similarly, it is possible to
create other generic constructs such as iterators over arbitrary data structures.
Components such as these are expected to be provided by expert users, while
end users treat them in the same way as the built-in PSC s. The next section
gives a formal account of the SyntRec’s language and the synthesis approach.
i

3
3.1

SyntRec Formally
Language

Figure 4 shows a simple kernel language that captures the relevant features of
SyntRec. In this language, a program consists of a set of ADT declarations
6

followed by a set of function declarations. The language distinguishes between a
ˆ
standard function f , a generator fˆ and a polymorphic generator fˆ. Functions can
be passed as parameters to other functions, but they are not entirely first-class
citizens because they cannot be assigned to variables or returned from functions.
Function parameters lack type annotations and are declared as type f un, but
their types can be deduced from inference. Similarly, expressions are divided into
standard expressions that does not contain any unknown choices (e), existing
ˆ The language also
synthesis constructs in Sketch (ê), and the new PSC s (ê).
has support for arrays with expressions for array creation ({e1 , e2 , ..., en }) and
array access (e1 [e2 ]). An array type is represented as θ[ ]. In this formalism, we
use the Greek letter τ to refer to a fully concrete type and θ to refer to a type
that may involve type variables. The distinction between the two is important
because PSC s can only be expanded whenPthe types of their context are known.
We formalize ADTs as tagged unions
varianti , where each of the variants
τ=
is a record type varianti = namei lki : τki k<ni . Note that ADTs in SyntRec
are not polymorphic. The notation {ai }i is used to denote the {a1 , a2 , ...}.
3.2

Synthesis Approach

ˆ
Given a user-written program P̂ that can potentially contain PSC s, choices and
holes, and a specification, the synthesis problem is to find a program P in the
language that only contains standard expressions (e) and functions (f ). SyntRec
solves this problem using a two step approach as shown below.:
ˆ
P̂
(PSCs, choices
and holes)

Type-Directed
Expansion
Rules

P̂
(choices
and holes)

Constraintbased
Synthesis

P
(no synthesis
constructs)

First, SyntRec uses a set of expansion rules that uses bi-directional type
checking to eliminate the PSC s. The result is a program that only contains
choices and holes. The second step is to use a constraint-based approach to solve
for these choices. The next subsections will present each of these steps in more
detail.
3.3

Type-Directed Expansion Rules

We will now formalize the process of specializing and expanding the PSC s into
sets of possible expressions. We should first note that the expansion and the
specialization of the different PSC s interact in complex ways. For example, for
the case? construct in the running example, the system cannot determine which
cases to generate until it knows the type of src , which is only fixed once the
polymorphic generator for recursiveReplacer is specialized to the calling context.
On the other hand, if a polymorphic generator is invoked inside the body of
a case? (like rcons in the running example), we may not know the types of the
7

arguments until after the case? is expanded into separate cases. Because of this,
type inference and expansion of the PSC s must happen in tandem.
We formalize the process of expanding PSC s using two different kinds of
judgements. The typing judgement Γ ` e : θ determines the type of an expression
by propagating information bottom-up from sub-expressions to larger expressions.
On the other hand, PSC s cannot be type-checked in a bottom-up manner;
instead, their types must be inferred from the context. The expansion judgment
θ
Γ `e −
→ e0 expands an expression e involving PSC s into an expression e0 that
does not contain PSC s (but can contain choices and holes). In this judgment,
θ is used to propagate information top-down and represents the type required
in a given context; in other words, after this expansion, the typing judgement
Γ ` e0 : θ must hold. We are not the first to note that bi-directional typing [15]
can be very useful in pruning the search space for synthesis [13,16], but we are the
first to apply this in the context of constraint-based synthesis and in a language
with user-provided definitions of program spaces.

τ

F UN

FL

FPM

o
Γ ; {xi : τi }i<n ` e −→
e0

 ⊥
→ τo f {xi : τi }i<n e0
Γ ` τo f {xi : τi }i<n e −

Γ ` e : {li : τi }i<n

{li :τi }i<n

0

Γ ` e −−−−−−−→ e
τ

{τij = τ0 }j

(τ0 [ ] = τ )

0

Γ ` e. fields? −
→ {{e .lij }j }

 0

P
Γ = Γ ;x :
namei lki : τki



n 0

Γ ; x : lki : τki

k<ni


k<ni

θ

` e −
→ ei

o
i

θ

Γ ` switch (x) { case? : e } −
→ switch (x) { case namei : ei }i
τi

τi

k
k
eimk
e1 −→
ei1k . . . em −→
n

U C1

τ
Γ ` new cons? (e1 . . . em ) −
→ choose new namei lki = choose {eirk }r<m


τ = Σnamei lki : τki

U C2

k<ni

o 
k<ni

i

τ = prim
τ
→ ??
Γ ` new cons? (e1 . . . em ) −


θout fˆ h{Ti }i {pi : θi}i e
Γ ` ei : τiin f or i < k

S = Unify {(θout , θ)} ∪ (θi , τiin ) i<k
S(θi )

PG

ei −−−→ e0i

S(θ)

f or i ≤ k + n
e[{e0i /pi }i ] −−−→ e0
θ
ˆ
f (e0 . . . ek . . . ek+n ) −
→ e0

Fig. 5: Expansion rules for various language constructs
The expansion rules for functions and PSC s are shown in Figure 5. At the top
level, given a program P , every function in P is transformed using the expansion
rule FUN. The body of the function is expanded under the known output type
of the function. The most interesting cases in the definition of the expansion
judgment correspond to the PSC s as outlined below. The expansion rules for the
other expressions are straightforward and are elided for brevity.
8

Field List The rule FL shows how a field list is expanded. If the required type
is an array of τ0 , then this PSC can be expanded into an array of all fields of
type τ0 .
Flexible Pattern Matching For each case, the body of case? is expanded while
setting x to a different type corresponding to each variant namei lki : τki k<ni as
shown in the rule FPM. Here, the argument to switch is required to be a variable
so that it can be used with a different type inside each of the different cases. Note
that each case is expanded independently, so the synthesizer can make different
choices for each ei .
Unknown constructor If the required type is an ADT, the rule UC1 expands
the expressions passed to the unknown constructor based on the type of each
field of each variant of the ADT and uses the resulting expressions to initialize
the fields in the relevant constructor. It returns a choose expression with all these
constructors as the arguments. If the required type is a primitive type (int or
bit), the unknown constructor is expanded into a Sketch hole by the rule UC2.
Polymorphic Generator Calls When the expansion encounters a call to a
polymorphic generator, the generator will be expanded and specialized according
to the PG rule. When a generator is called with arguments {ei }i , we can separate
the arguments into expressions that can be typed using the standard typing
judgement, and expressions such as new cons? (...) that cannot. In the rule, we
assume, without loss of generality, that the first k expressions can be typed and
the reminder cannot. The basic idea behind the expansion is as follows. First,
the rule obtains the types of the first k arguments and unifies them with the
types of the formal parameters of the function to get a type substitution S. The
arguments to the original call are expanded with our improved knowledge of the
types, and the body of the generator is then inlined and expanded in turn. The
actual implementation also keeps track of how many times each generator has
been inlined and replaces the generator invocation with assert false when the
inlining bound has been reached.
The above expansion rules fail if a type variable is encountered in places
where a concrete type is expected, and in such cases the system will throw an
error. For example, expressions such as field ( field (e)) , where field is as defined
in Figure 3, cannot by type-checked in our system because the expected type of
the inner field call cannot be determined using top-down type propagation.
3.4

Constraint-based Synthesis

Once we have a program with a fixed number of integer unknowns, the synthesis
problem can be encoded as a constraint ∃φ. ∀σ. P (φ, σ) where φ is a control
vector describing the set of choices that the synthesizer has to make, σ is the
input state of the program, and P (φ, σ) is a predicate that is true if the program
satisfies its specification under input σ and control φ. Our system follows the
standard approach of unrolling loops and inlining recursive calls to derive P and
uses counterexample guided inductive synthesis (CEGIS) to solve this doubly
quantified problem [18]. For readers unfamiliar with this approach, the most
relevant aspect from the point of view of this paper is that the doubly quantified
9

problem is reduced to a sequence of inductive synthesis steps. At each step,
the system generates a solution that works for a small set of inputs, and then
checks if this solution is in fact correct for all inputs; otherwise, it generates a
counter-example for the next inductive synthesis step.
Applying the standard approach can, however, be problematic in our context
especially with regards to inlining recursive calls. For instance, consider the
example from Section 2. Here, the function desugar that has to be synthesized is a
recursive function. If we were to inline all the recursive calls to desugar, then a given
concrete value for the input σ such as BetweenS(a = NumS(...), b = BinaryS(...), ...) ,
will exercise multiple cases within desugar (BetweenS, NumS and BinaryS for the
example). This is problematic in the context of CEGIS, because at each inductive
synthesis step the synthesizer has to jointly solve for all these variants of desugar
which greatly hinders scalability when the source language has many variants.
3.5

Inductive Decomposition

The goal of this section is to leverage the inductive specification to potentially
avoid inlining the recursive calls to the synthesized function. This idea of treating
the specification as an inductive hypothesis is well known in the deductive verification community where the goal is to solve the following problem: ∀σ. P (φ0 , σ).
However, in our case, we want to apply this idea during the inductive synthesis
step of CEGIS where the goal is to solve ∃φ. P (φ, σ0 ) which has not been explored
before.
Definition 1 (Inductive Decomposition). Suppose the specification is of
the form interps (e) = interpd (trans(e)) where trans is the function that needs
to be synthesized. Let trans(e0 ) be a recursive call within trans(e) where e0 is
strictly smaller term than e. Inductive Decomposition is defined as the following
substitution: 1. Replace trans(e0 ) with a special expression e0 . 2. When inlining
function calls, apply the following rules for the evaluation of e0 :
interpd ( e0 ) −−−−−→ interps (e0 )
e0 in any other context −−−−−→ trans(e0 )
i.e. Inductive Decomposition works by delaying the evaluation of a recursive
trans(e0 ) call by replacing it with a placeholder that tracks the input e0 . Then,
if the algorithm encounters these placeholders when inlining interpd in the
specification, it replaces them directly with interps (e0 ) which we know how
to evaluate, thus, eliminating the need to inline the unknown trans function.
This replacement is sound because the specification states interpd (trans(e0 )) =
interps (e0 ). If the algorithm encounters the placeholders in any other context
where the inductive specification can not be leveraged, it defaults to evaluating
trans(e0 ).
Theorem 1. Inductive Decomposition is sound and complete. In other words,
if the specification is valid before the substitution, then it will be valid after the
substitution and vice-versa.
10

A proof of this theorem can be found in the tech report [6]. Although the
Inductive Decomposition algorithm imposes restrictions on which recursive calls
can be eliminated, it turns out that for many of the ADT transformation scenarios,
the algorithm can totally eliminate all recursive calls to trans. For instance, in the
running example, because of the inductive structure of dstInterpret , all placeholders
for recursive desugar calls will occur only in the context of dstInterpret (desugar(e ’))
which can be replaced by srcInterpret (e ’) according to the algorithm. Thus, after
the substitution, the desugar function is no longer recursive and moreover, the
desugaring for the different variants can be synthesized separately. For the
running example, we gain a 20X speedup using this optimization. Our system
also implements several generalizations of the aforementioned optimization that
are detailed in the tech report [6].

4

Evaluation

Benchmarks We evaluated our approach on 23 benchmarks as shown in Figure 6.
All benchmarks along with the synthesized solutions can be found in the tech
report [6]. Since there is no standard benchmark suite for morphism problems, we
chose our benchmarks from common assignment problems (the lambda calculus
ones), desugaring passes from Sketch compiler and some standard data structure
manipulations on trees and lists. The AST optimization benchmarks are from a
system that synthesizes simplification rules for SMT solvers [17].

Templates The templates for all our benchmarks use one of the four generic
descriptions we have in the library. All benchmarks except arrAssertions , NegNorm
and AST optimizations use a generalized version of the recursiveReplacer generator
seen in Figure 3 (the exact generator is in the tech report). This generator is
also used as a template for problems that are very different from the desugaring
benchmarks such as the list and the tree manipulation problems, illustrating
how generic and reusable the templates can be. The arrAssertions benchmark
differs slightly from the others as its ADT definitions have arrays of recursive
fields and hence, we have a version of the recursive replacer that also recursively
iterates over these arrays. The NegNorm benchmark requires a template that has
nested pattern matching. Another interesting example of reusability of templates
is the AST optimization benchmarks. All 5 benchmarks in this category are
synthesized from a single library function. The template column in Figure 6 shows
the number of lines used in the template for each benchmark. Most benchmarks
have a single line that calls the appropriate library description similar to the
example in Section 2. Some benchmarks also specify additional components such
as helper functions that are required for the transformation. Note that these
additional components will also be required for other systems such as Leon and
Synquid.
11

4.1

Experiments

Methodology All experiments were run on a machine with forty 2.4 GHz Intel
Xeon processors and 96GB RAM. We ran each experiment 10 times and report
the median.
Hypothesis 1: Synthesis of complex routines is possible Figure 6 shows
the running times for all our benchmarks (T−opt column). SyntRec can synthesize all but one benchmark very efficiently when run on a single core using
less than 1GB memory—19 out of 23 benchmarks take ≤ 1 minute. Many of
these benchmarks are beyond what can be synthesized by other tools like Leon,
Rosette, and others and yet, SyntRec can synthesize them just from very general
templates. For instance, the lcB and lcP benchmarks are automatically discovering
the Church encodings for boolean operations and pairs, respectively. The tc
benchmark synthesizes an algorithm to produce type constraints for lambda
calculus ASTs to be used to do type inference. The output of this algorithm is a
conjunction of type equality constraints which is produced by traversing the AST.
Several other desugaring benchmarks have specifications that involve complicated
interpreters that keep track of state, for example. Some of these specifications
are even undecidable and yet, SyntRec can synthesize these benchmarks (up to
bounded correctness guarantees). The figure also shows the size of the synthesized
solution (code column)§ .
There is one benchmark ( langState ) that cannot be solved by SyntRec using
a single core. Even in this case, SyntRec can synthesize the desugaring for 6 out
of 7 variants in less than a minute. The unresolved variant requires generating
expression terms that are very deep which exponentially increases the search
space. Luckily, our solver is able to leverage multiple cores using the random
concretization technique [7] to search the space of possible programs in parallel.
The column T− parallel in Figure 6 shows the running times for all benchmarks
when run on 16 cores. SyntRec can now synthesize all variants of the langState
benchmark in about 9 minutes.
The results discussed so far are obtained for optimal search parameters for
each of the benchmarks. We also run an experiment to randomly search for
these parameters using the parallel search technique with 16 cores and report the
results in the T−search column. Although these times are higher than when using
the optimal parameters for each benchmark (T− parallel column), the difference is
not huge for most benchmarks.
Hypothesis 2: The Inductive Decomposition improves the scalability.
In this experiment, we run each benchmark with the Inductive Decomposition
optimization disabled and the results are shown in Figure 6 (T−unopt column).
This experiment is run on a single core. First of all, the technique is not applicable
for the AST optimization benchmarks because the functions to be synthesized
are not recursive. Second, for three benchmarks—the λ-calculus ones and the
tc benchmark, we noticed that their specifications do not have the inductive
structure and hence, the optimization never gets triggered.
§

Solution size is measured as the number of nodes in the AST representation of the
solution

12

Desugar
AST optim Analysis
List
Tree

Bench
lang
langState
regex
elimBool
compAssign
langLarge
arrAssertions
NegNorm
lcB
lcP

Description
template code T-opt T-parallel T-search
Running example
1
50 7.5
8.6
85.9
Running example with mutable state
1
62
⊥
527.2
1746.9
Desugaring regular expressions
1
22 2.0
3.3
9.1
Boolean operations to if else
1
21 1.5
2.9
7.5
Eliminates compound assignments
1
42 16.6
20.9
31.8
Desugaring a large language
1
126 61.2
58.0
49.7
Add out of bounds assertions
3
40 37.2
50.5
66.7
Computes negation normal form
3
57 21.2
13.6
64.4
Boolean operations to λ-calculus
1
55 43.1
47.4
40.6
Pairs to λ-calculus
1
41 163.6 258.2
288.3

T-unopt
152.5
⊥
3.3
2.4
176.2
⊥
53.0
⊥
43.1
163.6

tc

Type constraints for λ-calculus

8

41 168.9

68.0

201.9

168.9

andLt
andNot
andOr
plusEq
mux
lIns
lDel
lUnion
tIns
tDel
tDelMin
tDelMax

AST optimization 1
AST optimization 2
AST optimization 3
AST optimization 4
AST optimization 5
List insertion
List deletion
Union of two lists
Binary search tree insertion
Binary search tree deletion
Binary search tree delete min
Binary search tree delete max

1
1
1
1
1
1
2
1
1
4
2
2

15 3.1
6
2.6
12 3.7
18 3.3
6
2.4
12 1.5
14 4.0
10 8.7
48 20.7
63 224.8
18 27.1
18 25.9

3.1
3.0
3.1
3.0
3.0
2.3
4.6
2.7
14.5
227.4
32.2
30.8

13.2
13.0
14.0
14.0
12.4
2.2
4.1
4.8
41.6
286.1
57.7
54.4

N/A
N/A
N/A
N/A
N/A
2.1
3.1
2.1
11.6
298.9
24.9
25.9

Fig. 6: Benchmarks. All reported times are in seconds. ⊥ stands for timeout (>
45 min) and N/A stands for not applicable.
But for the other benchmarks, it can be seen that inductive decomposition
leads to a substantial speed-up on the bigger benchmarks. Three benchmarks
time out (> 45 minutes) and we found that langState times out even when run in
parallel. In addition, without the optimization, all the different variants need to
be synthesized together and hence, it is not possible to get partial solutions. The
other benchmarks show an average speedup of 2X with two benchmarks having
a speedup > 10X. We found that for benchmarks that have very few variants,
such as the list and the tree benchmarks, both versions perform almost similarly.
To evaluate how the performance depends on the number of variants in the
initial AST, we considered the langLarge benchmark that synthesizes a desugaring
for a source language with 15 variants into a destination language with just 4
variants. We started the benchmark with 3 variants in the source language while
incrementally adding the additional variants and measured the run times both with
the optimization enabled and disabled. The graph of run time against the number
of variants is shown in Figure 7. It can be seen that without the optimization
the performance degrades very quickly and moreover, the unoptimized version
times out (> 45 min) when the number of variants is > 11.
4.2

Comparison to other tools

We compared SyntRec against three tools—Leon, Synquid and Rosette that
can express our benchmarks. The list and the tree benchmarks are the typical
13

Time

benchmarks that Leon and Synquid can solve and they are faster than us on
these benchmarks. However, this difference is mostly due to SyntRec’s final
verification time. For these benchmarks, our verification is not at the state of the
art because we use a very naive library for the set related functions used in their
specifications. We also found that Leon and Synquid can synthesize some of our
easy desugaring benchmarks that requires constructing relatively small ADTs
like elimBool and regex in almost the same time as us. However, Leon and Synquid
were not able to solve the harder desugaring problems including the running
example. We should also note that this comparison is not totally apples-to-apples
as Leon and Synquid are more automated than SyntRec.
For comparison against Rosette, we
should first note that since Rosette is
1000
also a SyGus solver, we had to write
optimized
very verbose templates for each benchunoptimized
800
mark. But even then, we found that
600
Rosette cannot get past the compilation stage because the solver gets
400
bogged down by the large number
200
of recursive calls requiring expansion.
For the other smaller benchmarks that
0
3 4 5 6 7 8 9 10 11 12 13 14 15
were able to get to the synthesis stage,
Number of variants
we found that Rosette is either comparable or slower than SyntRec. For Fig. 7: Run time (in seconds) versus the
example, the benchmark elimBool takes number of variants of the source lanabout 2 minutes in Rosette compared guage for the langLarge benchmark with
to 2s in SyntRec. We attribute these and without the optimization.
differences to the different solver level
choices made by Rosette and Sketch
(which we used to built SyntRec upon).

5

Related Work

There are many recent systems that synthesize recursive functions on algebraic
data-types. Leon [3,8,9] and Synquid [16] are two systems that are very close
to ours. Leon, developed by the LARA group at EPFL, is built on prior work
on complete functional synthesis by the same group [10] and moreover, their
recent work on Synthesis Modulo Recursive Functions [8] demonstrated a sound
technique to synthesize provably correct recursive functions involving algebraic
data types. Unlike our system, which relies on bounded checking to establish
the correctness of candidates, their procedure is capable of synthesizing provably
correct implementations. The tradeoff is the scalability of the system; Leon
supports using arbitrary recursive predicates in the specification, but in practice
it is limited by what is feasible to prove automatically. Verifying something like
equivalence of lambda interpreters fully automatically is prohibitively expensive,
which puts some of our benchmarks beyond the scope of their system. Synquid [16],
14

on the other hand, uses refinement types as a form of specification to efficiently
synthesize programs. Like our system, Synquid also depends on bi-directional type
checking to effectively prune the search space. But like Leon, it is also limited to
decidable specifications. There has also been a lot of recent work on programming
by example systems for synthesizing recursive programs [13,4,1,14]. All of these
systems rely on explicit search with some systems like [13] using bi-directional
typing to prune the search space and other systems like [1] using specialized
data-structures to efficiently represent the space of implementations. However,
they are limited to programming-by-example settings, and cannot handle our
benchmarks, especially the desugaring ones.
Our work builds on a lot of previous work on SAT/SMT based synthesis
from templates. Our implementation itself is built on top of the open source
Sketch synthesis system [18]. However, several other solver-based synthesizers
have been reported in the literature, such as Brahma [5]. More recently, the work
on the solver aided language Rosette [21,20] has shown how to embed synthesis
capabilities in a rich dynamic language and then how to leverage these features
to produce synthesis-enabled embedded DSLs in the language. Rosette is a very
expressive language and in principle can express all the benchmarks in our paper.
However, Rosette is a dynamic language and lacks static type information, so in
order to get the benefits of the high-level synthesis constructs presented in this
paper, it would be necessary to re-implement all the machinery in this paper as
an embedded DSL.
There is also some related work in the context of using polymorphism to
enable re-usability in programming. [11] is one such approach where the authors
describe a design pattern in Haskell that allows programmers to express the
boilerplate code required for traversing recursive data structures in a reusable
manner. This paper, on the other hand, focuses on supporting reusable templates
in the context of synthesis which has not been explored before. Finally, the
work on hole driven development [12] is also related in the way it uses types to
gain information about the structure of the missing code. The key difference
is that existing systems like Agda lack the kind of symbolic search capabilities
present in our system, which allow it to search among the exponentially large
set of expressions with the right structure for one that satisfies a deep semantic
property like equivalence with respect to an interpreter.

6

Conclusion

The paper has shown that by combining type information from algebraic datatypes together with the novel Inductive Decomposition optimization, it is possible
to efficiently synthesize complex functions based on pattern matching from
very general templates, including desugaring functions for lambda calculus that
implement non-trivial Church encodings.
Acknowledgments: We would like to thank the authors of Leon and Rosette
for their help in comparing against their systems and the reviewers for their
feedback. This research was supported by NSF award #1139056 (ExCAPE).
15

References
1. A. Albarghouthi, S. Gulwani, and Z. Kincaid. Recursive program synthesis. In
CAV, pages 934–950, 2013.
2. R. Alur, R. Bodík, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia,
R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. Syntax-guided synthesis. In
Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA,
October 20-23, 2013, pages 1–8, 2013.
3. R. Blanc, V. Kuncak, E. Kneuss, and P. Suter. An overview of the leon verification
system: Verification by translation to recursive functions. In Proceedings of the 4th
Workshop on Scala, SCALA ’13, pages 1:1–1:10, New York, NY, USA, 2013. ACM.
4. J. K. Feser, S. Chaudhuri, and I. Dillig. Synthesizing data structure transformations
from input-output examples. In Proceedings of the 36th ACM SIGPLAN Conference
on Programming Language Design and Implementation, Portland, OR, USA, June
15-17, 2015, pages 229–239, 2015.
5. S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loop-free programs.
In PLDI, pages 62–73, 2011.
6. J. P. Inala, X. Qiu, B. Lerner, and A. Solar-Lezama. Type assisted synthesis of
recursive transformers on algebraic data types. CoRR, abs/1507.05527, 2015.
7. J. Jeon, X. Qiu, A. Solar-Lezama, and J. S. Foster. Adaptive concretization
for parallel program synthesis. In International Conference on Computer Aided
Verification, pages 377–394. Springer, 2015.
8. E. Kneuss, I. Kuraj, V. Kuncak, and P. Suter. Synthesis modulo recursive functions.
In OOPSLA, pages 407–426, 2013.
9. V. Kuncak. Verifying and synthesizing software with recursive functions - (invited
contribution). In ICALP (1), pages 11–25, 2014.
10. V. Kuncak, M. Mayer, R. Piskac, and P. Suter. Complete functional synthesis.
In Proceedings of the 2010 ACM SIGPLAN conference on Programming language
design and implementation, PLDI ’10, pages 316–329, 2010.
11. R. Lämmel and S. P. Jones. Scrap your boilerplate: a practical design pattern for
generic programming, volume 38. ACM, 2003.
12. U. Norell. Dependently typed programming in agda. In Proceedings of the 6th
International Conference on Advanced Functional Programming, AFP’08, pages
230–266, Berlin, Heidelberg, 2009. Springer-Verlag.
13. P. Osera and S. Zdancewic. Type-and-example-directed program synthesis. In
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language
Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 619–630,
2015.
14. D. Perelman, S. Gulwani, D. Grossman, and P. Provost. Test-driven synthesis. In
PLDI, page 43, 2014.
15. B. C. Pierce and D. N. Turner. Local type inference. ACM Trans. Program. Lang.
Syst., 22(1):1–44, Jan. 2000.
16. N. Polikarpova, I. Kuraj, and A. Solar-Lezama. Program synthesis from polymorphic
refinement types. In Proceedings of the 37th ACM SIGPLAN Conference on
Programming Language Design and Implementation, PLDI ’16, pages 522–538, New
York, NY, USA, 2016. ACM.
17. R. Singh and A. Solar-Lezama. Swapper: A framework for automatic generation
of formula simplifiers based on conditional rewrite rules. In Formal Methods in
Computer-Aided Design, 2016.

16

18. A. Solar-Lezama. Program Synthesis By Sketching. PhD thesis, EECS Dept., UC
Berkeley, 2008.
19. A. Solar-Lezama. Open source sketch synthesizer. 2012.
20. E. Torlak and R. Bodík. Growing solver-aided languages with rosette. In Onward!,
pages 135–152, 2013.
21. E. Torlak and R. Bodík. A lightweight symbolic virtual machine for solver-aided
host languages. In PLDI, page 54, 2014.

17

A

Benchmarks and Library Components

All the benchmarks along with corresponding synthesized solutions can be found
at https://bitbucket.org/jeevana_priya/syntrec-benchmarks/src. The library
generators and components are in the lib.skh file in the above repository. The
solutions generated by SyntRec are a little verbose because of the temporary
variables and also beacuse the function outputs are converted into reference
parameters.

B

Static Semantics of SyntRec language

The typing rules for the language work as one would expect. For example, the
type of a field access from a record is the type of the field.
Γ ` e : {{li : τi }i }
l = li
Γ ` e.l : τ

τ = τi

Values in the ADT are created through constructors.

name = namet
{lk = lkt
τadt = Σnamei {lki : τki }k<ni
Γ ` new name(lj = ej ) : τadt

Γ ` ek : τkt }k<nt

The most interesting rule is the one for switch. The rule, shown below, assumes
that the argument x to switch is a variable whose type is an ADT where each
variant corresponds to one of the cases in the switch. The body of each case is
then type checked under the assumption that the type of x is the type associated
with the corresponding variant.

0
Γ = (Γ ; x : τadt )
τadt = Σnamei {lki : τki }k<ni

0
{(Γ ; x : {lki : τki }k<ni ) ` ei : τ }i
Γ ` switch (x) { case namei : ei }i : τ

C

Dynamic Semantics of SyntRec language

The dynamic semantics evaluate expressions under an environment σ that
tracks the values of variables. ADT values are represented with a named record
hname, {li = vi }i i that has the name of the corresponding variant and the values
for each field. This is illustrated by the rule for the constructor.
{σ, ei → vi }i
v = hname, {li = vi }i i
σ, new name ({li = ei }i ) → v
The name stored as part of the record is used by the switch statement in order
to choose which branch to evaluate.
σ (x) = hname, {li = vi }i i namej = name
σ, ej → v
σ, switch (x) { case namei : ei }i → v
18

and it is easy to show that the typing rules ensure that the field access rule below
will always find a matching field li = l .
σ, e → hname, {li = vi }i i l = li
σ, e.l → v

D

v = vi

Proof of Inductive Decomposition theorem

The proof has two parts; first we show that the substitution is complete, meaning
that if the original specification is valid for a given synthesized trans function,
then it will still be valid after we perform the substitution. Second, we show
that the substitution is sound i.e. if the original specification does not hold for a
given trans, then it will also not hold after the substitution. Also note that we
can assume that there is only one recursive call (trans(e0 )) that undergoes the
transformation, because if replacing one call has no effect, then the calls can be
replaced one by one until all the calls have been replaced.
Completeness: We start by assuming that the specification is indeed valid for
a particular trans. In this case, interpd ( e0 ) is in fact equivalent to interps (e0 )
(since the specification is valid for all e). Hence, the specification is still valid
after the substitution.
Soundness: Let us assume that the specification does not hold, and let ex be
the smallest ADT value such that interps (ex ) 6= interpd (trans (ex )) . We define
smallest in terms of the maximum depth of recursion of ex (the height of the tree,
if we think of ex as a tree). Now, if ex is not recursive, we are done since the
substitution will only affect recursive values. Now, if ex is recursive and assume
that there is a recursive trans(e0x ) that gets replaced by the substitution. Here,
since e0x is smaller than ex and because ex is the smallest ADT that does not
satisfy the specification, interpd ( e0x ) is still equivalent to interps (e0x ). Hence,
the substitution has no impact on validity of ex and so, ex will also fail the
specification.
Note that the proof of soundness above only works because the recursive calls
inside trans operate on trees that are smaller than the input tree. This is an
important condition that is usually enforced by the template; if it were not to
hold, the transformation could take a buggy implementation (one that has an
infinite recursion, for example) and make it appear correct.

E

Structural constraints for full application of Inductive
Decomposition

Below, we first define the several structural constraints such that if these constraints were to hold, then the inductive decomposition will totally eliminate all
recursive trans calls.
Definition 2 (Recursive
Transformer).
P
Given an ADT τ = i Qi lji : τji j<n , a function f is a Recursive Transi
former if it has the following form:
19

f (e) := switch (e) {case Qi : procQi ({f (e.ljik )}k<bi , {e.lji 0 }k<b0i )}
k

Where none of the fields e.lji 0 are of type τ (but all the fields e.ljik must be of
k
type τ for the recursive call to be well typed).
In other words, f will pattern match on e, and in each case it will make
recursive calls on certain fields of e and process the results through an arbitrary
function procQi before returning them.
Definition 3 (Recursive Morphism).
A Recursive Morphism is a Recursive Transformer with the following
additional constraint:
procQi (v0 , . . . vk , v00 , . . . , vk0 ) = ψ[v0 , . . . vk ] where v0 . . . vk are the terms involving the recursive calls to this morphism function and ψ is an expression that
constructs an ADT tree (potentially of a different type than τ ) with v0 . . . vk as
some of the leaves and ψ itself does not depend on them, so
procQi (u0 , . . . uk , v00 , . . . , vk0 ) = ψ[u0 , . . . uk ] with the same ψ.
For example, the desugar function is a recursive morphism where ψ for each
case is the unknown expression tree of type dstAST that is generated by the rcons
function in the template (line 6 in Figure 3). On the other hand, the interpreters
in the running example that compute the value of an expression from the values of
its sub-expressions are examples of recursive transformers by the above definition,
but are not morphisms because they read the recursively evaluated values.
Lemma 1. Let interps , interpd bentwo recursive
transformers that
o
n operate
o on
P
P
i
si
i
di
two recursive data types τs = i Ki lj : τj
and τd = i Qi lj : τj
j<ni

j<mi

respectively and they both produce values of type τr . Additionally, suppose trans
is a recursive morphism from τs to τd . Under these constraints, the inductive
decomposition optimization will eliminate all recursive trans calls and thus,
making trans non-recursive.

F

Generalizations of Inductive Decomposition

Inductive decomposition can be generalized relatively easily to cases when the
interpreter takes additional arguments. This is useful, for example, for an interpreter that must take as input the state of the program in addition to an AST.
In this case, the specification will have the form
interps (e, S) = interpd (trans (e) , S)

Here, the inductive decomposition can be modified as follows:
interpd ( e0 , S) −−−−−→ interps (e0 , S)
This works because we are replacing what would have been a call to interpd (ν, S)
where ν would have been the result of calling trans(e0 ) with a call to interps (e0 , S).
20

A more interesting generalization involves the case when trans(e) takes some
parameters. For example, in cases when the transformation is type directed,
trans may take as a parameter a symbol table which gets updated as part of
the recursive calls to trans . In that case, the specification will look like the one
below.
interps (e, S) = interpd (trans (e, Γ ) , S)
assuming Γ = F (S);

Without the constraint that Γ is a function of S, the specification would almost
guarantee that trans ignores Γ , since Γ only appears on the right-hand side of
the equality. When trans is a type directed transformation, for example, F would
produce a symbol table with the types of the variables in the state S.
In this case, the inductive decomposition algorithm looks as follows: First,
replace trans(e0 , Γ ) with the special expression e0 , Γ . Second, apply the following
rules for the evaluation of e0 , Γ :
1.interpd ( e0 , Γ , S) −−−−−→ interps (e0 , S) if Γ = F (S)
2. e0 , Γ in any other case −−−−−→ trans(e0 , Γ )
In this case, the placeholder for trans function must thread its extra parameter Γ through its recursive calls, possibly transforming it along the way. The
transformation of interpd looks much like it did in the previous generalization,
but in addition to adding a call to to interps (e0 , S), the optimization will also
have to include an check that Γ = F (S). We found that for simple interpreters
and morphisms, this additional check is not a significant constraint; it will hold
whenever the state of the transformer is some abstraction of the program state (as
is the case with types). The cases where it does not hold, are cases where the state
Γ tracks some aspect of the program that is not tracked by the interpreter, for
example, whether a given construct has been seen or not. In such cases, however,
it is relatively easy to extend the interpreter to track this additional aspect as
part of its state.

21

