: Synthesizing Bidirectional Programs using Unidirectional Sketches

Masaomi Yamaguchi

Graduate School of Information Sciences
Tohoku University

Currently at Fujitsu.

Kazutaka Matsuda

Graduate School of Information Sciences
Tohoku University

Cristina David

University of Bristol
BS8 1QU

Meng Wang

University of Bristol
BS8 1QU

We propose a technique for synthesizing bidirectional programs from
the corresponding unidirectional code plus a few input/output
examples.  The core ideas are: (1) constructing a sketch using the given unidirectional program as a specification, and (2) filling the
sketch in a modular fashion by exploiting the properties of bidirectional programs.

These ideas are enabled by our choice of
programming language, HOBiT, which is specifically designed to
maintain the unidirectional program structure in bidirectional programming,
and keep the parts that control bidirectional behavior modular.
To evaluate our
approach, we implemented it in a tool called  and used it
to generate bidirectional programs for intricate microbenchmarks, as
well as for a few larger, more realistic problems.  We also compared
to a state-of-the-art unidirectional synthesis tool on the task of
synthesizing backward computations.

<concept_desc>Software and its engineering Domain specific languages</concept_desc>
<concept_desc>Software and its engineering Programming by example</concept_desc>
<concept_desc>Software and its engineering Functional languages</concept_desc>

[500]Software and its engineering Domain specific languages
[500]Software and its engineering Programming by example
[500]Software and its engineering Functional languages

§ INTRODUCTION

Transforming data from one format to another is a common task of
programming: compilers transform program text into syntax trees,
manipulate the trees and then generate low-level code; database
queries transform base relations into views; model-driving software engineering transforms one model into another. Very often,
such transformations will benefit from being bidirectional, allowing
changes to the targets to be mapped back to the sources too (for example the
view-update problem in databases <cit.>, bidirectional model transformation <cit.>, and so on).

As a
response to this need, programming-language researchers started to design
specialized programming languages for writing bidirectional transformations. In particular as
pioneered by Pierce's group at Pennsylvania, a bidirectional transformation (BX), also known as a lens <cit.>, is modeled as a pair of functions
between source and view data objects, one in each direction. The forward function $\GET::S \to V$ maps
a source onto a view, and the corresponding backward function
$\PUT:: S \times V \to S$ reflects any changes in the view back to the source.
Note that $\GET$ is not necessarily injective. Accordingly $\PUT$,
in addition to the updated view,
also takes the original source as an argument. This makes it possible to recover some of the source data
that is not present in the view. Of course, not all pairing of $\GET$$\PUT$ forms are valid BX; they must be related by specific properties known as round-tripping.

s = v                 implies  (s, v) = s Acceptability

(s,v) = s'            implies  s' = v     Consistency

for all $s, s' \in S$ and $v \in V$.
Here, <ref> states that no changes to the source happen if there is no change to the view,
and <ref> states that all changes to the view must be captured in the updated source.

A BX language allows the transformations in both directions to be programmed together and is expected to guarantee round-tripping by construction.

This is a challenging problem for language design, and consequently compromises had to be made (in particular to usability) in favor of guaranteeing round-tripping. In the original lens design <cit.>, lenses can only be composed by stylized lens combinators, which is inconvenient to program with. A lot of research has gone into this area since, for example <cit.>, and the state of the art has progressed a long way since. This includes a language HOBiT <cit.>, which follows a line of research <cit.> that aims to produce BX code that is close in structure to how one will program the $\GET$ function alone in a conventional unidirectional language.
Despite the progresses in language design, BX programming is still considerably more difficult than conventional programming, especially when sophisticated backward behaviors are required. This complexity is largely inherent as one is asked to do more in less: defining behaviors in both directions in a single definition. Even in a language like HOBiT, where programmers are allowed (and indeed encouraged) to approach BX programming from the convenience of conventional unidirectional programming, there are still (necessary) additional code components that need to be added to the basic program structure to specify non-trivial backward behaviors.

Unidirectional Program as Sketch
In this paper we introduce , a program synthesis system that makes BX programming more approachable to mainstream programmers.
In particular, we propose using unidirectional code (i.e., a definition of $\GET$ in a Haskell-like language)
as a sketch of the bidirectional program (which embodies both $\GET$ and $\PUT$).
Consequently, programmers familiar with unidirectional programming can obtain bidirectional programs from unidirectional ones and input/output examples.

In the neighboring field of software verification,
expressing specifications (in our case sketches) as normal code has the effect of boosting the adoption of formal tools
in industry <cit.>, something that bidirectional programming research as a whole may benefit from.

It is not hard to see that this program sketch idea fits well with the
language HOBiT. Unlike most BX languages, HOBiT is designed to keep
bidirectional code as similar in structure as possible to how one may program the unidirectional
$\GET$. Consequently, it is able to benefit from such a sketch and allow
the synthesis process to mostly focus on
parts of the code that specially handle intricate bidirectional behaviors.
This is an attractive solution. On one hand, the specifications are intuitive: users simply write normal unidirectional programs (together with a few input/output examples).
On the other hand,
the specifications as sketches are useful in the synthesis process because they reduce
the search space. Moreover, this design supports gradual “bidirectionalization”
done by incrementally converting existing unidirectional programs into bidirectional ones.
As it will be shown in a comprehensive evaluation in Section <ref>,
our system is highly effective and able to produce high-quality bidirectional programs in
a wide range of scenarios.

Off-the-shelf synthesis is a non-solution
Before diving into the details of our proposed solution, we would like to
take a step back and answer a question that may already be in some readers' minds:
will program synthesis completely replace the need for bidirectional languages? That is, how
about using generic synthesizers to derive a $\PUT$ from an existing $\GET$ in a standard
unidirectional language? After all, there already exist bidirectionalization techniques <cit.> that
are able to derive a $\PUT$ from a $\GET$ though in restricted situations.

When applied naively, this approach does not work.  As an experiment, we tried
using the state-of-the-art program synthesizer Smyth <cit.> to generate the
$\PUT$ from concrete examples and appropriate sketches.  To simplify the problem, we ignored
the round-tripping property between $\GET$ and $\PUT$, and tried to
generate any $\PUT$ (even one that violates the laws). However, even
in this simplified scenario, the synthesizer failed to find a $\PUT$
for simple examples (see Section <ref> for more details).

This is not surprising because, while powerful, program synthesis is very
hard due to the vast search space. The most common ways in which existing
synthesis techniques circumvent this are by picking a reduced domain specific language
to generate programs in <cit.> and by seeding the program search with a sketch
representing the program structure <cit.>.
In this paper, we are interested in synthesizing general purpose programs
and therefore we do not adopt the first strategy.

* We present an application of program synthesis to the area of bidirectional programming.
In particular, we provide an
automated technique for generating bidirectional
transformations in the language HOBiT (Section <ref>). The inputs to our procedure
are the corresponding unidirectional code and a few concrete
examples describing the backward transformation (Section <ref>).

* We exploit bidirectional programming properties, domain-specific
knowledge of HOBiT and type information to efficiently prune the
search space.  In particular, we generate specialized program
sketches from the unidirectional code (Section <ref>), which are then filled
in a modular manner by separating the solving of dependent synthesis tasks

(Sections <ref> and

* We present a classification of bidirectional programming
benchmarks based on the amount of information from the source that
is being lost through the forward transformation
(Section <ref>). We believe that such a
classification is valuable for evaluating the capabilities of our
bidirectional synthesis technique.

* We implemented our bidirectional synthesis technique in a tool
called , and used it to generate bidirectional
programs for the set of benchmarks discussed above (Section <ref>).
The prototype implementation of  is available in the artifact [<https://doi.org/10.5281/zenodo.5494504>] or the repository[<https://github.com/masaomi-yamaguchi/synbit>].

§ BACKGROUND: THE HOBIT LANGUAGE

HOBiT <cit.> is a state-of-the-art higher-order bidirectional programming language.
A distinct feature of HOBiT is its support of a programming style that is
close to the conventional unidirectional programming. The design of the language largely separates the core structure
of programs (which can be shared with the unidirectional definition of $\GET$) from the specification of backward behaviors that
are specific to bidirectional programming. In this section, we will introduce the core features of HOBiT with a focus on demonstrating its
suitability as a target of sketch-based program synthesis. Curious readers who are interested in the full expressiveness power of HOBiT and
the formal systems are encouraged to read the original paper <cit.>.

§.§ A Simple Example

Before getting into HOBiT programs, we start with a familiar definition in Haskell below.
append :: [a] →[a] →[a]

append xs ys =  xs
[ ]      →ys

a : x     →a : append x ys

In the definition, we use explicit case branching (instead of syntax sugar in Haskell) to highlight the
structure of the code.

Now, for a forward function ($\GET$) defined as $\var{append}$, let us investigate what will be suitable behaviors of its $\PUT$.
We denote the $\PUT$ by a HOBiT function $\var{appendB} :: \BX{[a]} \to \BX{[a]} \to \BX{[a]}$. The $\BX{}$-annotated types (highlighted in blue) are
bidirectional types in HOBiT, representing data that are subject to bidirectional computation. $\BX{}$-typed values are manipulated only by operations that satisfy the round-tripping laws, which is enough to ensure the round-tripping property of a whole program <cit.>. As we will see in the sequel, bidirectional types can be mixed with normal unidirectional types to support flexible programming and greater expressiveness.

Bidirectional functions of type $\BX{\sigma} \to \BX{\tau}$ can be executed as bidirectional transformations between $\sigma$ and $\tau$
in HOBiT's interactive environment (or, read-eval-print loop) via  and .

For example, one can run $\var{appendB}$ forwards
(uncurryB appendB) ([1,2], [3,4])

and backwards.
(uncurryB appendB) ([1,2], [3,4]) [5,6,7,8]

([5,6], [7,8])

Note that we have uncurried $\var{appendB}$ before execution by $\var{uncurryB} :: (\BX{a} \to \BX{b} \to \BX{c}) \to \BX{(a,b)} \to \BX{c}$ so that it fits the pattern of
$\BX{\sigma} \to \BX{\tau}$ for bidirectional execution. Specifically $(\var{uncurryB} \A \var{appendB})$ has type $\BX{([a],[a])} \to \BX{[a]}$, and its $\PUT$ has type $([a],[a])\to [a] \to ([a],[a])$.

Now we are ready to explore bidirectional behaviors.

§.§.§ Simple Backward Behavior
The simplest behavior of $\PUT$, as adopted in <cit.>, is to only
allow in-place update of views. In the case of $\var{appendB}$, it means that the changes to the length of
the view list will result in an error.
(uncurryB appendB) ([1,2], [3,4]) [5,6,7,8]

([5,6], [7,8])

(uncurryB appendB) ([1,2], [3,4]) [1,2,3]

To achieve this behavior, a definition in HOBiT reads the following.
appendB :: [a] →[a] →[a]

appendB xs ys =  xs
[ ]      →ys

a : x     →a : appendB x ys

As one can see, this definition is almost identical to that of $\var{append}$ with only the language constructs
such as case and data constructors being replaced by their bidirectional counterparts (underlined and highlighted in blue) that handle values of bidirectional types.

This simplicity comes from the design of HOBiT, as well as the modesty of the scenario. Given that the function is parametric in the list elements, in-place updates mean that the backward execution may simply trace back
exactly the same control flow of the original forward execution. This can be achieved by recursing according to the original source (the first argument of $\PUT$) and only using the updated view (the second argument of $\PUT$) as a supplier of element values.
Therefore, no additional specification is required in the code.

§.§.§ Branch Switching

HOBiT is not limited to such simple behaviors. Its bidirectional language constructs seen above set us up for more sophisticated cases.

Let's say that we now want to handle structural updates in the view, allowing the list length to vary.
(uncurryB appendB) ([1,2], [3,4])

(uncurryB appendB) ([1,2], [3,4]) [5,6,7,8]

([5,6], [7,8])

(uncurryB appendB) ([1,2], [3,4]) [5,6,7,8,9]

([5,6], [7,8,9])

(uncurryB appendB) ([1,2], [3,4]) [5]

([5], [ ])

When the length of the view list changes, we try to change the second list of the source to accommodate that. If the length becomes shorter than that of the first source list, the second source list will be empty and the first source list will also change accordingly.

As one can see, this behavior can no longer be achieved by simply tracing back the original control flow of the forward execution.
The backward execution will have to recurse a different number of times from the original, and how this is done will need to
be additionally specified in the code. Here enters a definition in HOBiT that does exactly this.
appendB :: [a] →[a] →[a]

appendB xs ys =  xs
[ ]      →ys      const True      λ.λ.  [ ]

a : x     →a : appendB x ys      not ∘null      λs.λ.  s

The code is longer than the last version, as expected, but the program structure
remains the same: the additional specification for more sophisticated backward behavior is modularly grouped at the end of
each case branch.
Recall that we plan to use the
unidirectional code as sketches to synthesize bidirectional code; this resemblance to the unidirectional code means that the synthesizing effort may now
concentrate on the part specifying bidirectional behaviors, increasing its effectiveness.

In the above code, we used two distinctive HOBiT features known as exit conditions (marked by the $\BWITH$ keyword) and reconciliation functions (marked by the $\BBY$ keyword). Both are for the purpose of controlling the backward behavior, especially when it no longer follows the original control flow (a behavior we call branch switching).

Exit conditions. An exit condition is an over-approximation of the forward-execution result of the branch, which
always evaluates to True if the branch is taken (dynamically checked in HOBiT). Hence, an exit condition in a $\BCASE$ expression has type $\tau \to \con{Bool}$ if the whole $\BCASE$ expression has type $\BX{\tau}$. The exit conditions are then used
as branching conditions in the backward execution. For example, in the above case of appendB, an empty list as view will
choose the first branch, as the view does not match the condition $\var{not} \circ \var{null}$ of the second branch.
Exit conditions often overlap; when multiple branches match, the original branch used in the forward execution is preferred. If
impossible (as the exit condition of that branch does not hold), the topmost branch will be taken. Like the case of the in-place update we saw previously, if the view-list length is not changed, then in the backward execution of appendB, the exit conditions of the original branches (now used as branching conditions) are always satisfied, and therefore the original branches are always taken.

The situation becomes more interesting when the view update does change the length of the list, for example by making it shorter.
In this case, the view list will be exhausted before the original number of recursions are completed. As a result, the backward
execution will now see $[\,]$ as its view input and a non-empty list as its source input. This means that the original branch at this
point is the second branch, but the exit condition of that does not hold, which forces the first branch to be taken—a branch switch.

Reconciliation functions. We have seen that exit conditions may force branches to switch, which is crucial for handling interesting changes to the view. However, it only solves half of the problem; naive branch switching typically results in run-time failure. The reason is simple: when branch switching happens, the two arguments of $\PUT$ are in an inconsistent state for the branch;
, for $\var{append}$, having an non-empty source list (and an empty view list) is inconsistent for the branch $[] \to \var{ys}$.

Reconciliation functions are used to fix this inconsistency. Basically, they are functions that take the inconsistent sources and views and produce new sources that are consistent with the branch taken. For example, in the definition above, the first branch will have $[\,]$ as the new source, because a switch to this branch means an empty view
and the branch expects the source to be the empty list for further $\PUT$ execution of the branch body.

In general, a reconciliation function in a $\BCASE$ expression is a function of type $\sigma \to \tau \to \sigma$, provided that the whole $\BCASE$ expression has type $\BX{\tau}$, with its scrutinee of type $\BX{\sigma}$.

An interesting observation of this particular example of $\var{append}$ is that the reconciliation function of the cons branch (, $\lambda s. \lambda \dontcare.s$ above) is actually never used. Recall that branch switching only happens when the backward execution tries to follow the original branch but the exit condition of the branch is not satisfied by the updates to the view. This will never happen in the nil branch above with the exit condition $\var{const} \A \con{True}$, which is always satisfied. In other words, regardless of the view update there will not be branch switching to the cons branch and therefore its reconciliation function is never executed. This behavior matches the behavior of $\var{append}$ which recurses on the first source list: when the view list is updated to be shorter than the first source list, the recursion will need to be cut short (thus branch switching to the nil branch); but when the view list is updated to be longer, the additional elements will simply be added to the second source list, which does not affect the recursion (and thus no need of branch switching).

In summary, with reconciliation functions, the backward execution may recover from inconsistent states and resume with a new source.
This is key to successful branch switching and the handling of structural updates to the view.

It is also worth noting that branch switching in HOBiT does not threaten the round-tripping properties.
Intuitively, the key principle of round-tripping is that a branch taken in a forward/backward execution should also be
taken in a subsequent backward/forward execution <cit.>.
When a brach switches in the backward execution, the new branch will produce a source value that matches the pattern of the new branch,
ensuring that a subsequent forward execution will take the same branch. Since the exit conditions are checked as valid post conditions, this correspondence of forward/backward branchings is established, and consequently it guarantees round-tripping.
An inappropriate reconciliation function will
make the backward execution fail but not break round-tripping.
More details can be found in the original paper <cit.>.
In this paper, we not only rely on the fact that HOBiT programs always satisfy round-tripping,
but we also leverage the principle for effective synthesis (Section <ref>).

One can also observe that the exit conditions and reconciliation functions in $\var{appendB}$ are quite simple themselves. However, their interaction with the
rest of the code is intricate. Programmers who write them are therefore required to have a good understanding of how backward execution works and how it can be influenced, which may not come naturally. This combination of simplicity in form and complication in behavior
makes it a fertile ground for program synthesis, which we set out to explore in this paper.

§.§.§ Mixing Bidirectional and Unidirectional Programming

We end this section with another example of variants of $\var{append}$'s backward behavior and its implementation in HOBiT.
The example also demonstrates a feature of HOBiT that supports a mixture of unidirectional and bidirectional programming
for greater expressiveness. Let us consider the following definition.
appendBc :: [a] →[a] →[a]

appendBc xs ys =  xs

[ ]      →ys      λv.  length v length ys      λ.λ.  [ ]

a : x     →a : appendBc x ys      λv.  length v length ys      λ. λ(v:).  [v]

Noticeably, the type of the function is a mixture of bidirectional and unidirectional types, with the second argument as a normal list.
Recall that bidirectional types represent data that are updatable; this type means that the second list is fixed with respect to
backward execution. We will look at a few sample runs before going into the details of the definition. Note that since the second argument is constant in backward execution, there is no longer the need to uncurry the function; one can simply partially apply it as shown below.
(λxs.  appendBc xs )

(λxs.  appendBc xs )

(λxs.  appendBc xs )

In this case, the second list is $\texttt{";"}$ and changes in the view can only affect the first list.
Any attempt to change the last part of the view will (rightly) fail.
(λxs.  appendBc xs )

Now let us go back to the definition. The fact that the second argument $\var{ys}$ is now of a normal (non-bidirectional) type means that it can be used
in the exit conditions and reconciliation functions (which only involve unidirectional terms). During backward execution, the exit conditions dictate that the recursion will terminate (the first branch taken) when the view list is the same length as the original $\var{ys}$. In addition, since $\var{ys}$ has a normal type, it will need to be lifted (as a constant) to the bidirectional world by  so that the $\BCASE$ expression
becomes well typed.
We again refer interested readers to <cit.> for lifting in more general forms.

The mixture of unidirectional and bidirectional programming is a challenge to program synthesis as the search space has become much larger. Still, the fundamental has not changed: a definition of $\GET$ remains a good sketch for HOBiT programs.

This behavior of $\var{appendB}$, however, is not always desirable. For example, provided that strings are represented as lists as in Haskell,
it is common that we append certain constant strings, such as “” and “”, particularly when we output a sequence of strings. In such a situation,
it is expected that such delimiters are unchangeable and changes must be reflected by the first argument of $\var{append}$.
This requirement is realized by the following variant $\var{appendBc}$ of bidirectional appending.
appendBc :: [a] →[a] →[a]

appendBc xs ys =  xs

[ ]      →ys      λv. length v length ys      λ.λ. [ ]

a : x     →a : appendBc x ys      λv. length v length ys      λ. λ(v:).[v]

Here, unlike $\var{appendB}$, the second argument of $\var{appendBc}$ has type $[a]$ instead of $\BX{[a]}$, emphasizing that
the second argument is constant and thus the backward execution can use the information. As a result, we have:
(λxs.  appendBc xs )

(λxs.  appendBc xs )

(λxs.  appendBc xs )

As expected, the update on the delimiter part legitimately fails, as the deliminator is constant.
(λxs.  appendBc xs )

Reconciliation functions

HOBiT stands out from other bidirectional programming languages in its representation of bidirectional transformations:
a bidirectional between $\sigma$ and $\tau$ is represented as a function from $\BX{\sigma} \to \BX{\tau}$ in HOBiT.
One of the advantages of this representation is that, unlike combinator-based approaches such as lenses <cit.>,
one can program bidirectional transformations in the standard functional programming (, applicative) style.
For example, we can write a bidirectional version $\var{appendB}$ of list appending function as below.
appendB :: [a] →[a] →[a]

appendB xs ys =  xs
[ ]      →ys      const True      λ.λ. [ ]

a : x     →a : appendB x ys      not ∘null      λ. λ(v:).[v]

(We do not explain the details of this program at this point.)
Except bidirectional types (such as $\BX{[a]}$) and bidirectional constructs (such as $\BCASE$ and $(\bxop{:})$) (highlighted blue for readability in this paper),
the bidirectional version has the same recursion structure as the standard unidirectional version below.
append :: [a] →[a] →[a]

append xs ys =  xs
[ ]      →ys

a : x     →a : append x ys

This resemblance of unidirectional and bidirectional programs is why we choose HOBiT for synthesis.
In the belief that a bidirectional version can be obtained from a unidirectional program by replacing unidirectional constructs with bidirectional ones,
our task is mainly to synthesize “annotations” used to control backward behavior (more specifically, $\BWITH$ and $\BBY$ parts above),
which simplifies the problem a lot.

The interactive environment (or, so-called read-eval-print loop) of HOBiT provides  and  commands to
execute bidirectional functions of type $\BX{\sigma} \to \BX{\tau}$ as bidirectional transformations between $\sigma$ and $\tau$.
With $\var{uncurryB} : (\BX{a} \to \BX{b} \to \BX{c}) \to \BX{(a,b)} \to \BX{c}$ defined by
uncurryB f x =  x  { (a,b) →f a b  λ. True  λs.λv.}

one can run $\var{appendB}$ forwards
(uncurryB appendB) ([1,2], [3,4])

and backwards.
(uncurryB appendB) ([1,2], [3,4]) [5,6,7,8]

([5,6], [7,8])

(uncurryB appendB) ([1,2], [3,4]) [5,6,7,8,9]

([5,6], [7,8,9])

(uncurryB appendB) ([1,2], [3,4]) [5]

([5], [])

As shown above, this $\var{appendB}$ reflects structural updates by changing the second component as possible.

This behavior of $\var{appendB}$, however, is not always desirable. For example, provided that strings are represented as lists as in Haskell,
it is common that we append certain constant strings, such as “” and “”, particularly when we output a sequence of strings. In such a situation,
it is expected that such delimiters are unchangeable and changes must be reflected by the first argument of $\var{append}$.
This requirement is realized by the following variant $\var{appendBc}$ of bidirectional appending.
appendBc :: [a] →[a] →[a]

appendBc xs ys =  xs

[ ]      →ys      λv. length v length ys      λ.λ. [ ]

a : x     →a : appendBc x ys      λv. length v length ys      λ. λ(v:).[v]

Here, unlike $\var{appendB}$, the second argument of $\var{appendBc}$ has type $[a]$ instead of $\BX{[a]}$, emphasizing that
the second argument is constant and thus the backward execution can use the information. As a result, we have:
(λxs.  appendBc xs )

(λxs.  appendBc xs )

(λxs.  appendBc xs )

As expected, the update on the delimiter part legitimately fails, as the deliminator is constant.
(λxs.  appendBc xs )

§.§ Basic Bidirectional Concepts in HOBiT

Now, let us briefly review the basic bidirectional concepts in HOBiT.
Here, we focus on conveying the intuition underlying the concept, which would be enough for this paper; for technical details, readers are encouraged to consult the original HOBiT paper <cit.>.

§.§.§ Bidirectional Types

Recall that HOBiT represents bidirectional transformations between $\sigma$ and $\tau$
as functions of type $\BX{\sigma} \to \BX{\tau}$.
Here, types like $\BX{\sigma}$ are called bidirectional types (not to be confused with bidirectional typing),
which intuitively mean $\sigma$ type subject to update; thus, one may read $\BX{\sigma}$ as “updatable $\sigma$”.
For example, a bidirectional transformation $\var{incB}$ that increments a source natural number by one
has type $\var{incB} :: \BX{\con{Nat}} \to \BX{\con{Nat}}$ in HOBiT,
where $\con{Nat}$ is the standard datatype for natural numbers à la Peano, with constructors
$\con{Z} : \con{Nat}$ and $\con{S} : \con{Nat} \to \con{Nat}$.

In HOBiT, $\BX{}$-types are treated as a black box. One thing we need to keep in mind is that
they must be treated by designated bidirectional constructs (such as $\bxop{:}$ and $\BCASE$ in $\var{appendB}$), which will be explained soon.
An (overly) intuitive view of a $\BX{\sigma}$-typed value is a pair of an original value (of type $\sigma$) and a receptor of an updated value (again, of type $\sigma$).
In this original-value/update-receptor view, $\var{incB} \A x$ transforms the original value $n$ of $x$ into $\con{S} \A n$,
and, when its receptor receives an updated value $\con{S} \A m$ of the whole expression, passes $m$ to the receptor of $x$.

We may say “the result of $e$ is updated to $u$” when $u$ is the argument/parameter of the corresponding receptor.

§.§.§ Bidirectional Constructors

The most primitive way to manipulate $\BX{}$-typed values is bidirectional constructors, which emphasizes that
constructor applications are injective, and thus we can view them as well-behaved bidirectional transformations.
For example, the $\var{incB}$ function mentioned above can be defined as $\var{incB} = \bxcon{S}$, where $\bxcon{S}$ has type $\BX{\con{Nat}} \to \BX{\con{Nat}}$.
In general, for a constructor $\con{C}$ of type $\tau_1 \to \dots \to \tau_n \to \tau$,
a corresponding bidirectional constructor $\bxcon{C}$ has type $\BX{\tau_1} \to \dots \to \BX{\tau_n} \to \BX{\tau}$.
The intuitive meaning of $\bxcon{C} \A e_1 \A \dots \A e_n$ is rather obvious: if we update the result with $u = \con{C} \A u_1 \A \dots \A u_n$,
each $e_i$ will be updated with $u_i$, and the update propagation fails if the updated value $u$ does not have this form.

§.§.§ Bidirectional Case Analysis

So far we have discussed (parameterized) bidirectional transformations that consist only of constructor applications.
More interesting bidirectional transformations can be defined by bidirectional case analysis.
HOBiT provides a simple but powerful construct for bidirectional case analysis,
whose behavior is almost the same as , the most general conditional lens combinator
in the original lens framework <cit.>, and
whose syntax is inspired by the reversible $\key{if}$ statement in a reversible language Janus <cit.>.
The general syntax of HOBiT's bidirectional case analysis is:

\[
\BCASE~e_0~\BOF~\{ {{p_i}} \to e_i ~\BWITH~e'_i~\BBY~e''_i \}_i
\]

(Like Haskell, we shall omit “$\{$”, “$\}$” and “$;$” if they are clear from the layout.)
Here, each $e'_i$ and $e''_i$ are respectively called exit conditions and reconciliation functions, which are keys to control bidirectional behavior.

Though we could use $\var{appendB}$ to explain $\BCASE$, we shall use the following simpler transformation, where the roles of
exit conditions and reconciliation functions are more evident.
data Member = Student EMail String |Prof EMail String

extMailB :: Member →(Bool, EMail)

extMailB m =  m
Prof    email name    →True, email       const True     λ(Student n). λ.  Prof  n

Student email name    →False, email      not ∘fst     λ.λ.

In the $\GET$ execution, $\var{extMailB}$ extracts email addresses with the flag indicating whether the member is professor or not.
Suppose that Alice is a student with her email address , which is represented as a source $s_0 = \con{Student} \A \texttt{"a0042"} \A \texttt{"Alice"}$.
In this case, the corresponding view is $(\con{False}, \texttt{"a0042"})$:
extMailB s_0

(False, )

Suppose that Alice moves to a different school and her email address is changed accordingly to .
This update is represented as an updated view $(\con{False}, \texttt{"b0123"})$ and reflected to the source as below.
extMailB s_0 (False, )

(Student  )

Let us explain how $\BCASE$ achieves this behavior in $\var{extMailB}$.
In this case, the original value of $m$—the input of $\var{extMailB}$ and thus the source—is $s_0$ and the result of the whole $\BCASE$ is changed to $(\con{False}, \texttt{"b0123"})$.
Unlike the unidirectional $\CASE$, $\BCASE$ in the $\PUT$ execution determines a branch based on an updated value in the $\PUT$ evaluation.
Here exactly is the place where exit condition is used. In this case, both exit conditions become $\con{True}$ for the updated value $(\con{False}, \texttt{b0123})$.
For such a case, HOBiT uses the deterministic prioritized choice where
the original branch (, the branch chosen by the usual case analysis for the original value of the scrutinee) has the highest priority (to fulfill <ref>),
and then comes the topmost. Thus, for this particular example,
the second branch is chosen as it is the original branch; here, the original value of $m$ is $s_0 = \con{Student} \A \texttt{"b0123"} \A \texttt{"Alice"}$.
Then, comparing the branch body $\bxtup{\bxcon{False}, \var{email}}$ and the updated value $(\con{False}, \texttt{"b0123"})$,
HOBiT knows that $\var{email}$ is updated with $\texttt{"b0123"}$. In contrast, we do not know how $\var{name}$ is updated as the variable is not used in the branch body.
In such a case, the original value is used as a substitute (defaulting). Since the original value of the scrutinee $m$ is $s_0$, the original value of
$\var{name}$ is set to $\texttt{"Alice"}$ as the usual execution. Thus, this original value is used as the updated value of $\var{name}$, and accordingly the scrutinee $m$—recall that it is the source—is
updated by $\con{Student} \A \texttt{"b0123"} \A \texttt{"Alice"}$.
Note that the reconciliation functions are not used at all for this update reflection.

Then, suppose in this time that Alice gets promoted to a faculty member with her new email address to .
This update is represented as an updated view $(\con{True}, \texttt{"alice"})$ and reflected to the source as below.
extMailB s_0 (True, )

Again, let us see how this update reflection has been achieved.
Similarly to the previous case, HOBiT chooses a branch by using exit conditions. In this time, only the exit condition associated with the first branch becomes
true for the updated value $(\con{True}, \texttt{"alice"})$, and the first branch is chosen.
However, here comes a problem: the original values of $\var{email}$ and $\var{name}$ are unspecified, because the original value of $m$ is
$s_0 = \con{Student} \A \texttt{"b0123"} \A \texttt{"Alice"}$, which is incompatible with the first branch's pattern $\con{Prof} \A \var{email} \A \var{name}$.
What causes the problem is that a branch chosen in the $\PUT$ execution is different from the original one (branch switching).
HOBiT addresses the problem by using the reconciliation function associated with the chosen branch to recover the “original values”.

A reconciliation function in $\BCASE$ takes an original value of the scrutinee and an updated value of
the whole $\BCASE$, and returns the reconciled original value of the scrutinee.
For this example, by using the reconciliation function $\lambda (\con{Student} \A \dontcare \A n). \lambda \dontcare.\, \con{Prof} \A \texttt{"x"}$ associated with the first branch,
from the original “original value” $s_0$ of $m$ and the updated value $(\con{True}, \texttt{"alice"})$ of the whole $\BCASE$
it produces the reconciled original value of $m$, $\con{Prof} \A \texttt{"x"} \A \texttt{"Alice"}$.
Then, the rest of the story is the similar to the previous case and $m$ is finally updated by $\con{Prof} \A \texttt{"alice"} \A \texttt{"Alice"}$.

This example also involves a trick in the exit conditions to prohibit ones to be demoted to students:
the exit condition associated with the first branch that always returns $\con{True}$, disallowing branch switching to
the second one.

Astute readers may find that <ref> would be violated if we write “incorrect” exit conditions such as $\lambda \dontcare.\con{False}$ in the sense
that they are not post conditions of associated branches, as it disallows us to chose the original branch in the $\PUT$ evaluation of $\BCASE$.
HOBiT uses a simple solution inspired by Janus <cit.> that treats exit conditions as assertions in the $\GET$ evaluation.
Every exit condition trivially becomes a correct post condition under this treatment.

Let us summarize the behavior of
\( \BCASE~e_0~\BOF~\{ {{p_i}} \to e_i ~\BWITH~e'_i~\BBY~e''_i \}_i \).
In the $\GET$ direction, the evaluation is no different from the ordinary one except that it checks if $e'_i$ becomes
true for the result of the chosen branch.
In the $\PUT$ direction:

* The $\BCASE$ expression chooses a branch $i$ such that the associated exit condition $e'_i$ becomes true for a given updated value.
If multiple branches satisfy this condition, $\BCASE$ uses a prioritized choice where the original branch has the
highest priority and then comes the topmost.

* If the chosen branch is different from the original one (branch switching),
the reconciliation function $e''_i$ associated with the branch $i$ is used to
recover the original values of variables in $p_i$, by pattern matching $e''_i \A u_0 \A u$ with $p_i$ where
$u_0$ is the original value of $e_0$ and $u$ is the updated value of the whole $\BCASE$.

* If some of variables in $p_i$ is unused in $e_i$ and their updated values are unknown after the $\PUT$ evaluation of $e_i$,
the original values of the variables are used as their updated values (defaulting).

Now, we are ready to revisit $\var{appendB}$ in the beginning of this section. For the two executions
(uncurryB appendB) ([1,2], [3,4]) [5,6,7,8]

([5,6], [7,8])

(uncurryB appendB) ([1,2], [3,4]) [5,6,7,8,9]

([5,6], [7,8,9])

the original branches are chosen in the execution for all $\PUT$ executions of $\BCASE$.
(uncurryB appendB) ([1,2], [3,4]) [5]

([5], [])

branch switching has occurred for a call of $\var{appendB} \A \var{xs} \A \var{ys}$ where the original values of $\var{xs}$ and $\var{ys}$
are $[2]$ and $[3,4]$, respectively, and when the result is updated with $[\,]$.

§.§.§ Constant Lifting

The last thing left for explanation is constant-lifting $\LIFTU{e}$; $\var{appendBc}$ uses the construct to convert $\var{ys} : [a]$ into $\LIFTU{\var{ys}} : \BX{[a]}$.
Intuitively, when $e$ evaluates to $v$,
the original value $\LIFTU{e}$ is $v$ and its receptor rejects any updated values other than $v$.
Accordingly, $\LIFTU{e}$ has type $\BX{\sigma}$ if $e$ has type $\sigma$.
For example, we have:
(λ. 42) 0

(λ. 42) 0 42

(λ. 42) 0 37

Now we shall believe that the behavior of $\var{appendBc}$ would also be understandable.

We shall note that HOBiT provides a more general syntax that lifts
arbitrary bidirectional transformations between $\sigma$ to $\tau$ as functions of type $\BX{\sigma} \to \BX{\tau}$, trusting the users for their well-behavedness <cit.>;
$\LIFTU{e}$ is a useful special case, obtained from a certain well-behaved bidirectional transformation and thus can be used without risking well-behavedness.

§.§ Syntax

\[
\begin{tarray}{l@{\quad}lcll}
\text{Programs} &
P &::=& f_1 = e_1;\dots; f_n = e_n  \\
\text{Expressions} &
e &::=& x \mid \lambda x.e \mid e_1 \A e_2 \mid \con{C} \A \V{e} \mid \CASE~e_0~\OF~\{ p_i \to e_i \}_i \\
&& | & \bxcon{C} \A \V{e} \mid \CASE~e_0~\OF~\{ \bx{{p_i}} \to e_i ~\WITH~e'_i~\BY~e''_i \}_i \mid \LIFTU{e} \\
\text{Patterns} &
p &::=& x \mid \con{C} \A \V{p}
\end{tarray}
\]

Syntax of (a Part of) HOBiT: $x$ and $f$ range over variables, and $\con{C}$ ranges over constructors

Since HOBiT is used both for an input and output of our synthesis method,
we here clarify the syntax of the HOBiT programs that we consider in this paper (Fig. <ref>).
All the constructs have already been explained in the previous section,
while we have used some syntactic sugars (such as Haskell-style function definitions).
We do not repeat the explanations here.

As usual, we assume that patterns $p$ are linear; , no variables occur twice in $p$.
Is the following restriction necessary if we do not show formal semantics?
We also assume for simplicity that patterns do not overlap both for $\CASE$ and $\BCASE$.

§.§ A Taste of Type System

Types in HOBiT have the following form.

\[
\begin{tarray}{lcll}
A, B    &::=& \con{Bool} \mid A \to B \mid \BX{\sigma} \mid \dots  \\
\end{tarray}
\]

The $\dots$ part depends on predefined datatypes; we shall allow any datatype as long as
every constructor in the datatype have (not necessarily one) simple types.
Here, we write $\sigma$ for the types for which partially correct (, correct if succeeds) equality checking is given.[
This definition of types is notably generous than the original <cit.>, in which datatypes must be inductive and
$\sigma$ must not contain $\to$ and $\BX{}$. The restrictions in the original type system come from their correctness proof
using logical relations, where these restrictions are useful for avoiding circular discussions. However, the same authors <cit.>
recently developed a reversible language Sparcl along the similar idea to HOBiT, and the restrictions are lifted
thanks to their correctness proof that relies only on syntactic or operational techniques such as the subject reduction.
We conjecture that a similar discussion
applies to HOBiT, and shall ignore the original restrictions. Interestingly, this treatment matches the implementation of HOBiT, which
allows arbitrary user-defined datatypes and there is no distinction with $A$ and $\sigma$; equality check on functions or updatables
always results in a run-time error as OCamls' .
As demonstrated, the most characteristic type in HOBiT is a bidirectional type $\BX{\sigma}$, which intuitively denotes
“updatable $\tau$”—data subject to update in bidirectional transformation.
This also means that bidirectional transformations in HOBiT handles $\sigma$-types rather than $A$.
Although some examples in this paper use polymorphic types (such as $\var{appendB} :: \BX{[a]} \to \BX{[a]} \to \BX{[a]}$),
we shall consider only simple types for simplicity in this paper;
extension of our synthesis method to the ML-style polymorphism ($\LET$-polymorphism) is straightforward (actually, the implementation can handle such examples).
[We do not distinguish $A$ and $\sigma$ when we consider polymorphism, as we use polymorphic equality as mentioned in the previous footnote.]

Recall that HOBiT adopts a staged semantics in which $\BX{\sigma}$-typed values are interpreted as quoted bidirectional transformations.
The type system reflects the idea and uses a dual context system <cit.> as $\Gamma ; \Delta \vdash e : A$,
where $\Gamma$ holds bindings generated in the first (unidirectional) stage,
and $\Delta$ holds ones generated in the second (bidirectional) stage.
Since bidirectional transformations in HOBiT works on $\sigma$-types, $\Delta(x)$ must also be a $\sigma$-type for any $x$.
Here, we shall excerpt some important typing rules below, which would be sufficient for illustrating the idea of the type system;
see Appendix <ref> for the complete definition of the typing relation.

\begin{gather*}
\infer
{ \Gamma ; \Delta \vdash x : A }
{ \Gamma(x) = A }
\quad
\infer
{ \Gamma ; \Delta \vdash x : \BX{\sigma} }
{ \Delta(x) = \sigma }
\quad
\infer
{ \Gamma; \Delta \vdash \lambda x.e : A \to B }
{ \Gamma, x : A ; \Delta \vdash e :  B}
\\[3pt]
\infer
{ \Gamma; \Delta \vdash \BCASE~e_0~\BOF~\{ {{p_i}} \to e_i~\BWITH~e'_i~\BBY~e''_i \}_i : \BX{\sigma} }
{ \Gamma; \Delta \vdash e_0 : \BX{\tau}
\quad
\{ \Delta_i \vdash p_i : A \quad \Gamma ; \Delta, \Delta_i \vdash e_i : \BX{\sigma} \quad \Gamma; \Delta \vdash e'_i : \sigma \to \con{Bool} \quad \Gamma; \Delta \vdash e''_i : \tau \to \sigma \to \tau  \}_i
\end{gather*}

Observe that $\lambda$ (and $\CASE$, though not presented here) introduces variables in $\Gamma$, while
$\BCASE$ introduces variables in $\Delta$.
Also, observe that the pattern-introduced variables $\Delta_i$ are not visible in exit conditions and reconciliation functions,
as they are used before the bidirectional pattern matching.

§ SYNTHESIS OF HOBIT PROGRAMS USING UNIDIRECTIONAL PROGRAMS AS SKETCHES

In this section, we describe our technique for synthesizing bidirectional programs in HOBiT. Throughout the section, we will use the familiar case of
append as the running example.

§.§ Overview

Before presenting the technical details, we start with an informal overview of the synthesis process.

takes in a unidirectional program (written in a subset of Haskell) and a small number of
input/output examples of the required backward behavior, and produces a HOBiT program that behaves like the input unidirectional program in the forward direction and is guaranteed to satisfy the round-tripping laws and conform to the given examples in the backward direction. More details on the guarantees of our system are given later in Section <ref>.

As an example, in the case of append, we provide the following specification to .

\begin{align*}
%  \var{appendPair} &: ([\con{Int}], [\con{Int}]) \to [\con{Int}] \\
& \var{append} :: [\con{Int}] \to [\con{Int}] \to [\con{Int}]                                                                                \\
%   appendPair                 & = \lambda \var{l}.\, \CASE~\var{l}~\OF~\{ (\var{xs}, \var{ys}) \to \var{append} \A \var{xs} \A \var{ys} \}                         \\
& \var{append}                 = \lambda \var{xs}.\, \lambda \var{ys}.\, \CASE~\var{xs}~\OF~\{ [\,] \to \var{ys} ;\; (a:x) \to a : \var{append} \A x \A \var{ys} \} \\[\blanklineskip]%
& \texttt{:put} \A (\var{uncurryB} \A \var{appendB})  \A ([1,2,3], [4,5]) \A  [6,2]  = ([6,2], [\,])
\end{align*}

The definition of append above is completely standard. The user-provided input/output example specifies that the view list may be updated
to a smaller length. As we have seen in Section <ref>, append needs to be
uncurried before bidirectional execution, which is also reflected in the input/output example above where the source is a pair
of lists. One interesting observation is that this bidirectional execution provides a call context of the function to be
synthesized, which speeds up the synthesis
process by narrowing down the choices of appendB's type.

For the given specification,  produces the following result.

appendB :: [Int] →[Int] →[Int]

appendB = λxs.  λys.   xs  {
[ ] →ys

λv.  v  { x →True;  →False }

λs. λv.  v  { x →[ ]

(a:x) →a : append x ys

λv.  v  { z : zs→True;  →False }

λs. λv.  v  { z : zs →

As one can see, this program is equivalent to the hand-written definition in Section <ref>;
the only difference is that the synthesized version does not use library functions such as const and null.[Obvious cosmetic simplification could be made to part of the code for readability. But that is an orthogonal concern.]

Roughly speaking, the synthesis process that produces the above result involves two major components: the generation of
a suitable sketch with holes and the filling of the holes. We will look at the main steps below.

Generation of sketches

The sketch is expected to be largely similar in structure to the unidirectional definition (thanks to the design of HOBiT),
but there are a few details to be ironed out. First of all, one needs to decide the type of the target function.
Recall that HOBiT is a powerful language that supports the mixing of unidirectional and bidirectional programming.
Thus, for a type such as append's, there are several possibilities such as $\BX{[\con{Int}]} \to \BX{[\con{Int}]} \to \BX{[\con{Int}]}$, $\BX{[\con{Int}]} \to [\con{Int}] \to \BX{[\con{Int}]}$, $[\BX{\con{Int}}] \to \BX{[\con{Int}]} \to \BX{[\con{Int}]}$, and so on. It is therefore crucial to narrow down the choices to control the search space. The call context in the input/output example(s) in the specification
is useful for this step, as it can effectively restrict its type.
We will discuss more
details on this in Section <ref>. For now, it is sufficient to know that for the specification given in this example, the only
viable type is $\var{appendB} :: \BX{[\con{Int}]} \to \BX{[\con{Int}]} \to \BX{[\con{Int}]}$.

The next step is to build a sketch based on the unidirectional definition given in the
specification. The type we have from above straightforwardly implies that the $\CASE$ construct
in $\var{append}$'s definition is to be replaced by the bidirectional $\BCASE$, which
expects exit conditions and reconciliation functions to be added (as holes ($\GHole$) in the sketch).

appendB = λxs.  λys.   xs  {
[ ] →ys

(a:x) →a : appendB x ys      }

Both the exit conditions and reconciliation functions are simply
unidirectional functions. Thus in theory, one can try to use a
generic synthesizer to generate them. However, this naive method will miss out
on a lot of information that we know about these functions. Recall that, given a $\BCASE$ branch
$\var{p} \to \var{e} $, its corresponding exit condition must
return true for all possible evaluations of $\var{e}$; similarly, the
results of its reconciliation function must match p and
the second argument of the reconciliation function must be an evaluation result of
e. We therefore capture such knowledge with
specialized sketches, which make use of
two types of specialized holes that are parameterized with additional information: exit-condition hole ($\EHoleS{\var{e}}$), and reconciliation-function hole ($\RHoleS{p}{e}$). This results in the following sketch for this example.

appendB     = λxs.  λys.   xs  {
[ ] →ys
ys   [ ]ys;

(a:x) →a : append x ys

a : append x ys

(a:x)a : append x ys}

In the spirit of component-based synthesis <cit.>, we generate code by composing components from a library
that includes
$\CASE$ and $\BCASE$ expressions,
$\con{Bool}$ constructors and operators, as well as list and tuple
constructors. As we will explain in Section <ref>,
this library can be augmented with auxiliary components provided by the

In this example, the sketch generation is quite deterministic.

In general, especially when multiple functions must be synthesized together and auxiliary components are provided,
there could be
multiple candidate sketches. In such a case, we use a lazy approach that nondeterministically tries exploring one candidate and
generating any other.

Sketch completion step I: shape-restricted holes

With the sketch ready, we can proceed to fill the holes.
As a first step in the sketch completion process, we make use of the
information captured by the specialized holes to generate some parts
of the code for exit conditions and reconciliation functions. This step
does not involve any search.

appendB = λxs.  λys.   xs  {
[ ] →ys
λv.  v  { x →;  →False }

λs. λv.  v  { x →
[ ]

(a:x) →a : append x ys

λv.  v  { z : zs→;  →False }

λs. λv.  v  { z : zs →

The specialized holes are replaced with $\lambda$-abstractions with $\CASE$ structures.
The result involves a different type of holes we call shape-restricted holes ($\SHole{p}$);
such holes can only be filled with expressions that may match the pattern $p$. For example, for $\SHole{a : x}$, the empty list is not a valid candidate. A generic hole ($\Hole$) is a special case where the pattern is a wildcard that matches every term.

For exit conditions, the translation used the information encoded by
exit condition holes to figure out when $\con{False}$ should be
returned—recall that, for a $\BCASE$ branch $\var{p \to
\var{e}}$, exit conditions should return $\con{False}$ for any
results that cannot be produced by e.  In the case of
appendB, this means that for the second branch in the sketch,
the exit condition must return $\con{False}$ for any empty list.
(Here, z and zs are fresh variables.)
For the first
branch, this information does not help us eliminate any candidates.
(Again, x is a fresh variable.)
The $\CASE$ construct
generation uses all the information encoded by the exit condition
holes. Consequently, the holes left in the
sketch are generic ones.

For reconciliation functions, the newly generated
shape-restricted holes capture the fact that for a $\BCASE$ branch $\var{p} \to \var{e}$,
the result of the reconciliation function must match $p$. Thus, the first branch
of appendB has $\SHole{[\,]}$ while the second one $\SHole{a:x}$.
We further know that the second argument of the reconciliation function
must be a result of e, which allows us to generate the $\CASE$
structure shown in the sketch.

Sketch completion step II: search and filtering

The last step is to fill the remaining shape-restricted holes.

At this point, we leave off using the information in the unidirectional input program, and turn our attention to the input/output example(s).
To fill the holes,
we generate $\beta$-normal forms where functions are $\eta$-expanded, and filter the candidates
by checking against the examples(s).

A problem with using the example(s) to filter out incorrect candidates
is that it is for the whole program, which includes several holes. A
naive use of the example(s) means that filtering has to be delayed until
late in the synthesis process when all the holes are filled.
This is inefficient.

Conversely, our ideal goal is to have a modular filtering process, where we can
simultaneously check candidate exit conditions and reconciliation functions independently of each other.
For this purpose, our solution is to leverage domain-specific knowledge of HOBiT.

Specifically, we make use of the fact that $\PUT \A (s,v)$ and $\GET
\A (\PUT \A (s,v))$ must follow the same execution trace in terms of
taken branches, as explained in the discussion on round-tripping in HOBiT (see the corresponding paragraph in Section <ref>).

This enables us to fix the control flow of the $\PUT$ behavior for the given input/output example(s) without referring to exit conditions,
so that we can separate the search for exit conditions from reconciliation functions.

We will discuss this in more
detail later in the overview, as well as in Section <ref>.

the use of the trace information also enables us to
address the issue of non-terminating $\PUT$ executions. In a naive
generate-and-test synthesis approach, some of the generated candidates may
be non-terminating, which poses issues for the testing phase. As we assume
that the $\PUT$ execution must always follow the finite branching trace of $\GET$,
we never generate such programs.
Here, we assumed that the input/output unidirectional
program is terminating for the original and updated sources of the
input/output examples. More details on this will be presented in Section <ref>.

Filtering of exit conditions based on branch traces

We continue with the partially filled sketch for appendB above (reproduced below), with the holes numbered for easy reference.

appendB = λxs.  λys.   xs  {
[ ] →ys
λv.  v  { x →_1;  →False }

λs. λv.  v  { x →
[ ]_3

(a:x) →a : append x ys

λv.  v  { z : zs→_2;  →False }

λs. λv.  v  { z : zs →

What are the constraints on the holes that we can derive from the input/output example below?

\[
\texttt{:put} \A (\var{uncurryB}~ \var{appendB}) \A ([1,2,3], [4,5]) \A [6,2]  = ([6,2], [])
\]

As mentioned above, $\texttt{:put} \A (uncurryB~ appendB) \A ([1,2,3], [4,5]) \A [6,2]$ must choose the branches chosen by $\texttt{:get} \A (\var{uncurryB} \A \var{appendB}) \A ([6,2],[])$.
We shall call a history of chosen branches a branch trace.
For $\texttt{:get} \A (\var{uncurryB} \A \var{appendB}) \A ([6,2],[])$, the branch trace is:

(i) the cons branch (where $\var{xs}$ is $[6,2]$),

(ii) the cons branch (where $\var{xs}$ is $[2]$),

(iii) the nil branch (where $\var{xs}$ is $[]$).

We now follow the same trace for $\texttt{:put} \A ((uncurryB~ appendB) ~([1,2,3], [4,5])~ [6,2])$ and each
step will give rise to a constraint on the exit condition of the branch.

(i) $a : \var{append} \A x \A \var{ys}$ (and therefore the $v$) has the value of the updated view $[6,2]$, and $\Hole_2$ must evaluate to $\con{True}$ in this context. Therefore, $\Hole_2[6/z, [2]/\var{zs}, [6,2]/v] \equiv \con{True}$.

(ii) $a : \var{append} \A x \A \var{ys}$ (and therefore the $v$) has the value of the updated view $[2]$, and $\Hole_2$ must evaluate to $\con{True}$ in this context. Therefore, $\Hole_2[2/z, [\,]/\var{zs}, [2]/v] \equiv \con{True}$.

(iii) $\var{ys}$ (and therefore the $v$) has the value of $[\,]$, and $\Hole_1$ must evaluate to $\con{True}$ in this context. Therefore, $\Hole_1[[\,]/x, [\,]/v] \equiv \con{True}$.

These constraints are useful in generating the exit conditions independently. As a matter of fact, in the case of $\var{appendB}$ both
$\Hole_1$ and $\Hole_2$ are simply filled by the expression $\con{True}$ which satisfies all the constraints.

There are no trace constraints generated for holes 3 and 4 though. So they will be generated according to the shape restrictions only.
Hole 3 must be $[\,]$ while Hole 4 can be filled by a non-empty list.
Recall that, in this example, the reconciliation functions of the
cons branch are never used. And therefore, arbitrary default terms will fill Hole 4 just fine, which produces the output we saw
at the beginning of this subsection.

Filtering of reconciliation functions based on branch traces
The branch traces are also used to filter reconciliation functions. (This is not needed in this example
as the nil branch was already fixed in the filling of shape-restricted holes and the cons branch can be arbitrary.)
The important insight here is that reconciliation functions can be filtered independently from the exit conditions, resulting in
significant efficiency gain. The reason is that the branch traces carry all the information that is needed to test reconciliation functions (recall
that the exit conditions are only for determining branching in backward execution; and since the branching is known in the branch traces there is no need for exit conditions.). We will see examples of this in Section <ref>.

In the rest of this section, we will go through each step of the synthesis process in detail.

§.§ Input to Our Method

Remember from the overview that our technique takes as input some typed unidirectional code and a set of input/output examples illustrating the backward transformation.
Formally, this translates to the following 4-tuple $I = (P, \Gamma, f_1, \ExSet)$:

* $P = \{f_i = e_i \}_i$ is a program in the unidirectional fragment of HOBiT,
where $f_i = e_i$ stands for a function/value definition of $f_i$ by the value of $e_i$.

* $\Gamma = \{ f_i : A_i \}_i$ is a typing environment for $P$; ,
each $e_i$ has type $A_i$ under $\Gamma$.

* $f_1$ is the entry point function, whose type is expected to have the form $\sigma_1 \to \tau_1$;
[We use metavariables $A, B,\dots$ for types in general and $\sigma, \tau,\dots$ for those that can be sources or views. In <cit.>, the latter kind of types do not contain $\BX{}$ and $\to$, but their implementation does not distinguish the two (which in fact is safe). Thus, we do not strictly respect the restriction on $\sigma$-types in our technical development.
this is used to prune the search space as explained in Section <ref>.

* $\ExSet = \{ (s_k, v_k, s_k') \}_k$ is a (finite) set of well-typed input/output examples for a bidirectional version of the entry point $f_1$;
for the $k$-th example, $s_k$ is the original source, $v_k$ is the updated view and $s_k'$ is the updated source.

The input program $P$ may contain functions that are not
reachable from the entry point but can be used during program generation.

We call such functions auxiliary functions and add them to our
library of default synthesis components.  As mentioned earlier in
Section <ref>, the default library includes $\CASE$ and
$\BCASE$ expressions, $\con{Bool}$ constructors and operators, as well
as list and tuple constructors.

For the appendB example, the input is formally expressed as:

\begin{align*}
P_\mathrm{app}      & = \{ \var{appendB} = \lambda \var{xs}.\, \lambda \var{ys}.\, \CASE~\var{xs}~\OF~\{ [\,] \to \var{ys} ;\; (a:x) \to a : \var{appendB} \A x \A \var{ys}, \var{uncurryB} = \dots \} \} \\
\Gamma_\mathrm{app} & = \{ \var{appendB} : [\con{Int}] \to [\con{Int}] \to [\con{Int}], \var{uncurryB} : \dots \}                                                                                \\
f_{1\mathrm{app}}   & = \var{uncurryB} \A \var{appendB}                                                                                \\
\ExSet_\mathrm{app} & = \{ (([1,2,3], [4,5]), [6,2], ([6,2],[])) \}\text{.}                                                                                %\qedhere
\end{align*}

Here, we omit the definition and the type of $\var{uncurryB}$ but state it is a part of the input program.

§.§ Generation of Sketches

As shown in the overview, we start by generating bidirectional sketches from the unidirectional code.

The basic idea of the sketch generation is to replace unidirectional constructs with bidirectional ones nondeterministically:
when $\CASE$ is replaced with $\BCASE$, exit conditions and reconciliation functions are left as holes.
Interestingly, replacing all unidirectional constructs (if they have corresponding bidirectional ones) may not be the best solution;
as demonstrated in $\var{appendBc} :: \BX{[a]} \to [a] \to \BX{[a]}$ in Section <ref>,
we sometimes need to leave some parts unidirectional to achieve the given bidirectional behavior.

The starting point of sketch generation is deciding the type of the
target function.  We expect the unidirectional code to
contain an entry point function $f_1 : \sigma_1 \to \tau_1$ (e.g., uncurry append in Example <ref>). This helps
us reduce the number of generated type signatures as we know that the
target entry point function to be synthesized must have type
$\BX{\sigma_1} \to \BX{\tau_1}$. Also, we further prune the search space
by eliminating type signatures that do not obey the call context in the
input/output examples.

Type signature generation
We first define the relation $A \leadsto A'$ as:
$A'$ is the type obtained from $A$ by replacing an arbitrary number of sub-components $\sigma$ in $A$ by $\BX{\sigma}$ nondeterministically,
as long as $\sigma$ does not contain function types.
We do not replace $\sigma$ containing function types to avoid generating apparently non-useful types
such as $\BX{(\con{Int} \to \con{Int})}$ and $\BX{[\con{Int} \to \con{Int}]}$.

Next, we provide the typing environment generation relation $\Gamma \leadsto \Gamma'$, where $\Gamma'$ is the typing environment corresponding to the bidirectional program.

For $\Gamma = \{f_1 : \sigma_1 \to \tau_1 \} \cup \{f_i : A_i\}_{i > 0}$, the typing environment generation relation $\Gamma \leadsto \Gamma'$ is defined if

$\Gamma' = \{ f_1 : \BX{\sigma_1} \to \BX{\tau_1} \} \cup \{ f_i : A_i' \}_{i > 0}$,

where $A_i \leadsto A_i'$ for each $i > 0$.

Type-directed sketch generation

Once we have (a candidate) typing environment $\Gamma'$, the next step is to generate corresponding sketches in a type-directed manner.

Very briefly, the type system in HOBiT <cit.> uses a dual context system <cit.>. The typing relation can be written as $\Gamma ; \Delta \vdash e : A$,
where $\Gamma$ and $\Delta$ respectively are called unidirectional and bidirectional typing environments, and hold
variables introduced by unidirectional and bidirectional contexts respectively.

See Appendix <ref> for the concrete typing rules.

The sketch generation is done by using a relation $\GenTmp{\Gamma'}{\Delta'}{A'}{\Gamma}{e}{A}{e'}$, which
reads that, from a term-in-context $\Gamma ; \emptyset \vdash e : A$, sketch $e'$ is generated according to the given target typing environments $\Gamma'$ and $\Delta'$, and target type $A'$
so that $\Gamma' ; \Delta' \vdash e' : A'$ holds after the sketch has been completed (i.e., no unfilled holes) in a type-preserving way.
Notice that $\Gamma'$, $\Delta'$ and $A'$ are also a part of the input in $\GenTmp{\Gamma'}{\Delta'}{A'}{\Gamma}{e}{A}{e'}$; , its outcome is only $e'$.
We omit the concrete generation rules in the main text but put them in Fig. <ref> in Appendix <ref>, because they are technical but straightforward.
We omit the concrete generation rules due to the space limitation, and put them in the extended version of this paper <cit.>.

We note that the rules are overlapping (i.e., several may be applicable at a given step), which makes sketch generation nondeterministic.

The sketch generation is defined formally as below.

Suppose that $\Gamma \leadsto \Gamma'$.
Then, for $P = \{ f_i : e_i \}_i$,
the sketch generation relation $P \leadsto P'$ is defined if

$ P' = \{ f_i : e'_i \}_i$,

where $\GenTmp{\Gamma'}{\emptyset}{\Gamma'(f_i)}{\Gamma}{e_i}{\Gamma(f_i)}{e'_i}$.

§.§ Sketch Completion Step I: Shape-Restricted Holes

In general, there will be several possible sketches for a given
unidirectional program.
As mentioned in Section <ref>, in such a case,

we use a lazy approach that nondeterministically tries exploring one candidate and generating any other.

In this section we describe
the sketch exploration
process. In particular, we start by using the information captured by
the specialized holes to generate parts of the code for exit
conditions and reconciliation functions.

§.§ Sketch Completion Step II: Search and Filtering

The last step is to fill the remaining shape-restricted and generic
holes.  This process involves type-directed generation of candidates and filtering based on user-provided input/output examples.
For simplicity of presentation, we do not explicitly capture the type of the code to be
generated in the shape-restricted holes; instead, we recover it
from the sketch and typing environment $\Gamma$.

§.§.§ Generating Candidates for Shape Restricted Holes

In this section, we describe the process of filling in shape restricted holes $\SHole{p}$.
To achieve this, we generate terms of shape p in $\beta$-normal forms where functions are $\eta$-expanded.

Specifically, we produce expressions $U^p$ in the following grammar, which restricts their shape to p:

\[
\begin{tarray}{l@{\quad}l}
%\text{Top-level Normal Forms} &
\begin{tarray}{lcll}
U^p &::=& V^p \mid \CASE~x \A V_1 \A \dots \A V_n~\OF~\{ p_i \to U_i^p \}_i
\end{tarray}\\
%\text{Other Normal Forms} &
\begin{tarray}{lcl@{\qquad}l}
V^p &::=& \lambda x. U & (p = x) \\
&\mid& x \A V_1 \A \dots \A V_n \\
&\mid& \con{C} \A V_1^{p_1} \A \dots \A V_n^{p_n} & (p = \con{C} \A p_1 \A \dots \A p_n \text{~or \(p,p_1,\dots,p_n\) are all variables})
\end{tarray}
\end{tarray}
\]

To simplify the presentation, we omit $p$ and write $V$ or $U$ if $p$ is a variable.
In this grammar, the purpose of $U$ is to have $\CASE$s in the outermost positions (but inside $\lambda$);
a $\CASE$ in a context $K[\CASE~e~\OF~\{ p_i \to e_i \}_i]$
can be hoisted as $\CASE~e~\OF~\{ p_i \to K[e_i] \}_i$, which is a transformation known as commuting conversion.
If $p$ is not a variable, we can only generate constructors as specified by $p$
($p = \con{C} \A p_1 \A \dots \A p_n $  or  $(p,p_1,\dots,p_n)$ are all variables).
Otherwise, if $p$ is a variable, the only knowledge we assume about it is its type. Thus, any of the
productions for $V^{p}$ would be considered.
Note that $x$/$C$ are drawn from the current context; , they may be components provided by users.

Types are used for two purposes in this type-directed generation.
The rather obvious purpose is to limit the search space for $x$ and $\con{C}$; notice that, since we know their types,
we also know the types of their arguments allowing us to perform type-directed synthesis for them as well.
The other purpose is to reduce redundancy with respect to $\eta$-equivalence by only generating
$\lambda x.U$ for function types and $\CASE$s only for non-function types.

A caveat is the generation of $x \A V_1 \A \dots \A V_n$ at the scrutinee position of $\CASE$, which cannot be done in a type-directed way as its type is not given a priori;
instead, its type is synthesized by using the type of $x$.

§.§ Heuristics

In this section, we discuss some heuristics we found effective when exploring the search space.

Assigning costs to choices.
Our generation is prioritized by assigning a positive cost to each
nondeterministic choice in the sketch generation.

Programs with lower costs are generated earlier than those with higher costs.  An advantage of
this approach is that it is easy to integrate with lazy nondeterministic generation
methods <cit.>, which is the core of our
prototype implementation.  Another advantage is that smaller programs
naturally have higher priority (, lower costs), as the generation of
large programs usually involves many choices, reflecting our belief
that smaller programs are typically preferable.

Canonical forms of $\con{Bool}$-typed expressions.

Generation of $\con{Bool}$-typed expressions is a common task, especially in our context as
exit conditions always return $\con{Bool}$ values. However, a naive generation of $\con{Bool}$-typed expressions may lead to redundancies, for example, $\con{True} \mathbin{\texttt{\&\&}} e$ and $e$ may be considered two distinct expressions during the search.

So when filling holes of type $\con{Bool}$, we generate expressions in disjunctive normal form, in which
atomic propositions are expressions of the form $x \A V_1 \A \dots \A V_n$ with $x : A_1 \to \dots \to A_n \to \con{Bool} \in \Gamma$.

While this eliminates redundancy due to distributivity, associativity and zero and unit elements,
it does not address commutativity and idempotence.

Provided that there is a strict
total order $\prec$ on expressions, both sorts of redundancy could be addressed easily by
generating $e_2$ after $e_1$ so that $e_1 \prec e_2$ holds.
Currently we do not do this in our implementation in order to avoid
the additional overhead of checking $e_1 \prec e_2$.

Other effective improvements.
In addition to the heuristics mentioned above, we make use of some simple but effective techniques.
For example, for $\BCASE$ with a single branch, we do not try to synthesize
exit conditions or reconciliation functions. An exit condition $\lambda \dontcare.\con{True}$ and a reconciliation function $\lambda s.\lambda v.s$ suffice for such a branch.

We do not generate redundant case expressions such as
$\lambda s.\lambda v.\CASE~ v~ \OF \{ z \to \cdots \}$.

When the pattern $p$ of a branch does not contain any variables, we deterministically choose $\lambda \dontcare.\lambda \dontcare.p$ as its reconciliation function.

For a $\CASE$ whose patterns $\{\mathcal{P}(e_i)\}_i$ do not overlap, we do not leave holes in exit conditions as replacing them with $\con{True}$ is sufficient.

This section reports our prototype implementation of the proposed synthesis method, which is
available in <https://github.com/masaomi-yamaguchi/synbit>.

The prototype system is implemented in Haskell as an extension to the original prototype implementation of HOBiT by Matsuda,[<https://bitbucket.org/kztk/hibx/>]
which also uses Haskell.
As we have mentioned in the previous section, our synthesis method utilizes the lazy nondeterministic generation.
For this step, the prototype implementation uses a variant of <cit.>'s library that implements Curry-like nondeterministic computation in Haskell,
with an extension with weights on nondeterministic choices, which serve as priorities in searching.
Basically, a choice to increase the program size has a positive weight so that smaller programs have higher priorities in searching.

§ EXPERIMENTS

We implemented the proposed idea as a proof-of-concept system, , in Haskell[The implementation is available in the artifact <https://doi.org/10.5281/zenodo.5494504> or in <https://github.com/masaomi-yamaguchi/synbit>].
is given as an extension to the original HOBiT
implementation <cit.>.

We measure the effectiveness of our proposed method in the following three experiments.

* Microbenchmarks, classified in terms of information loss (Section <ref>).

* More realistic problems including XML transformations and string parsing (Section <ref>).

* Comparisons with the other state-of-the-art synthesis methods (Section <ref>).

The experiments were conducted on a Windows Subsystem for Linux (WSL)
2 running on a laptop PC with 2.30 GHz Intel(R) Core(TM) i7-4712HQ CPU
and 16 GB memory, 13 GB out of which were assigned to WSL 2.  The host
OS was Windows 10 (build NO. 19042.685), and the guest OS was Ubuntu
20.04.1 LTS.  We used GHC 8.6.5 to compile  with the
optimization flag .  Execution times were measured by
a popular library in Haskell for benchmarking, which estimates the
true execution time by the least-squares method.
Any case running longer than 10 minutes was reported as a timeout.

§.§ Microbenchmarks Classified by Information-Loss

To construct the microbenchmarks, we classify programming problems according to the level of difficulty.
Recall that the main challenge of BX is to incorporate the information that is in the source but absent in the view in order to create an updated source.
For structure rich data represented by algebraic datatypes, this includes the structure of the source data, especially the part that the $\GET$ function recurs on. With that, we arrive at the following classes.

All information of the recursion structure is present in the view (, $\var{map}$).

Some information of the recursion structure is present in the view (, $\var{append}$).

No information of the recursion structure is present in the view (, $\var{lookup}$).

The rule of thumb is that the more information is present in the view, the easier is it to define a $\PUT$ that
handles structural changes to the view. Take $\var{map}$ as an example, the function is bijective in terms of the list structure.
As a result, a $\PUT$ function can share the recursion structure of the $\GET$, mapping whatever structural changes from the view back to the source.
This becomes harder with the loss of structure information in the view. Take $\var{append}$ as an example. The boundary between the first source list, which $\GET$ recurs on, and the second source list is gone in the view. As a result, if a $\PUT$ function is to share the recursive structure of the $\GET$, the backward execution will always try to replenish the first source list first before leaving the remaining view elements as the second source list[unless we know that the second list is fixed as in $\var{appendBc}$]. This is what $\var{appendB}$ does. Any divergence from this behavior will require a different recursive
structure for $\PUT$, which drastically increases the search space as it loses the guidance of the $\GET$-based sketch.

We thus expect that the performance of   varies according to the difficulty classes. For Class-  problems,
synthesis is likely to be successful for any given input/output examples (thus handling any structural changes);
for Class-  problems, synthesis is likely to be successful for some given input/output examples;
and for Class-  problems, synthesis is only possible for input/output examples that are free from structural changes.

The results of experiments for categorized examples

Problem                      Recursion on              Class             Result      Time (s)
$\var{double}$               Nat                           Yes         0.050

$\var{uncurryReplicate}$     Nat                           Yes         0.050

$\var{mapNot}$               List                          Yes         0.052

$\var{mapReplicate}$         Nat and List                  Yes         0.130

$\var{snoc}$                 List                          Yes         0.150

$\var{length}$               List                          Yes         0.040

$\var{lengthTail}$           List (tail recursive)         Yes         0.220

$\var{reverse}$              List (tail recursive)         Yes         1.300

$\var{mapFst}$               List                          Yes         0.016

$\var{add}$                  Nat                           Yes         0.045

$\var{append}$               List                          Yes         0.034

$\var{appendBc}$             List                          Yes         5.600

$\var{professor}$            List                          Yes         0.023

$\var{lines}$                List                          Timeout     1c-

$\var{lookup}$               List                          Timeout     1c-

The benchmark programs and the synthesis results are summarized in Table <ref>, which should be
read together with Table <ref> where
the input/output examples used for the experiments are shown (which can also be used as a reference for the forward execution behaviors of the
input functions).
Also, we used the following auxiliary functions: equality over natural numbers for lengthTail,
reverse and appendBc, and length in addition for the latter two.
The definitions of all the functions listed and the full synthesis results can be found in the artifact [<https://doi.org/10.5281/zenodo.5494504>] or the repository[<https://github.com/masaomi-yamaguchi/synbit>] together with the  implementation.

Input/output examples: for readability, we shall write $n$ for $\con{S}^n \A \con{Z}$ (integer constants are also used in $\var{snoc}$, $\var{reverse}$, $\var{mapFst}$ and $\var{append}$), and
$\var{st}_n$/$\var{pr}_n$/$\var{pr}_n'$ for $\con{Student} \A \texttt{"st\(n\)"}$/$\con{Professor} \A \texttt{"pr\(n\)"}$/$\con{Professor} \A \texttt{"pr\(n\)'"}$.

Original Source                                                     (Original View)                                                                    Updated View                                        Updated Source
1                                                                   2                                                                                6                                                   3

5                                                                   10                                                                                4                                                   2

(, 2)                                                                                ,                                     (, 3)

(True, 3)                                                     [True, True, True]                                               [False,False]                           (False, 2)

$[\con{True}, \con{False}]$                                         $[\con{False}, \con{True}]$                                                        $[\con{True},\con{True},\con{False}]$               $[\con{False},\con{False}, \con{True}]$

$[(\texttt{'b'}, 2)]$                                               $[\texttt{"bb"}]$                                                                  $[\texttt{"aaa"}, \texttt{"b"}, \texttt{"cc"}]$     $[(\texttt{'a'}, 3), (\texttt{'b'}, 1), (\texttt{'c'}, 2)]$

$[(\texttt{'a'}, 3), (\texttt{'b'}, 1), (\texttt{'c'}, 2)]$         $[\texttt{"aaa"}, \texttt{"b"}, \texttt{"cc"}]$                                    $[\texttt{"bb"}]$                                   $[(\texttt{'b'}, 2)]$

$([1,2,3],4)$                                                       $[1,2,3,4]$                                                                        $[1,2,3]$                                           $([1,2], 3)$

$([1,2,3],4)$                                                       $[1,2,3,4]$                                                                        $[1,2,3,4,5,6]$                                     $([1,2,3,4,5], 6)$

$[1,2]$                                                             $2$                                                                                $4$                                                 $[1,2,0,0]$

$/\var{lengthTail}$     $[2,0]$                                                             $2$                                                                                $1$                                                 $[2]$

$[\con{True}, \con{True}]$                                          $[\con{True}, \con{True}]$                                                         $[\con{False}, \con{True}, \con{True}]$             $[\con{True}, \con{True}, \con{False}]$

$[1,2,3,4]$                                                         $[4,3,2,1]$                                                                        $[6,5]$                                             $[5, 6 ]$

$[(1,\texttt{'a'}),(2, \texttt{'b'}), (3,\texttt{'c'})]$            $[1,2,3]$                                                                          $[1,3]$                                             $[(1,\texttt{'a'}), (3,\texttt{'b'})]$

$[(2, \texttt{'b'}), (3,\texttt{'c'})]$                             $[2,3]$                                                                            $[0,1,2,3]$                                         $[\bbt (0,\texttt{'b'}),(1,\texttt{'c'}),                   \\(2,\texttt{'a'}), (3,\texttt{'a'})]\ee$

$(2,3)$                                                             $5$                                                                                $7$                                                 $(2,5)$

$(2,3)$                                                             $5$                                                                                $1$                                                 $(1,0)$

$([1,2,3,4], [5])$                                                  $[1,2,3,4,5]$                                                                      $[6,2]$                                             $([6,2], [])$

$([1,2,3,4], [5])$                                                  $[1,2,3,4,5]$                                                                      $[1,2,3,4,5,6]$                                     $([1,2,3,4], [5,6])$

$\texttt{"apple"}$                                                  $\texttt{"apple;;"}$                                                               $\texttt{"pineapple;;"}$                            $\texttt{"pineapple"}$

$\texttt{"apple"}$                                                  $\texttt{"apple;;"}$                                                               $\texttt{"plum;;"}$                                 $\texttt{"plum"}$

$[ \var{st}_1, \var{st}_2, \var{pr}_1, \var{st}_3, \var{pr}_2]$     $[\var{pr}_1, \var{pr}_2]$
$[\var{pr}_1', \var{pr}_2', \var{pr}_3']$                           $[ \var{st}_1, \var{st}_2, \var{pr}_1', \var{st}_3, \var{pr}_2', \var{pr}_3']$

$[ \var{st}_1, \var{st}_2, \var{pr}_1, \var{st}_3, \var{pr}_2]$     $[\var{pr}_1, \var{pr}_2]$
$[\var{pr}_1']$                                                     $[ \var{st}_1, \var{st}_2, \var{pr}_1', \var{st}_3]$

$\texttt{"aa\textbackslash nbb\textbackslash ncc"}$                 $[\mathtt{"aa"}, \mathtt{"bb"},\mathtt{"cc"}]$                                     $[\texttt{"aa"}, \texttt{"bb"}]$                    $\texttt{"aa\textbackslash nbb"}$

$\texttt{"aa"}$                                                     $[\mathtt{"aa"}]$                                                                  $[\texttt{"aa"}, \texttt{"bb"}]$                    $\texttt{"aa\textbackslash nbb"}$

$\texttt{"aa\textbackslash n"}$                                     $[\mathtt{"aa"}]$                                                                  $[\texttt{"aa"}, \texttt{"bb"}]$                    $\texttt{"aa\textbackslash nbb\textbackslash n"}$

$([(1,10), (2,200), (3,33)], 2)$                                    $200$                                                                              $10$                                                $([(1,10), (2,200), (3,33)], 1)$

$([(1,10), (2,200), (3,33)], 2)$                                    $200$                                                                              $33$                                                $([(1,10), (2,200), (3,33)], 3)$

Class  As we can see,  handles programs in this class with ease.

An interesting case is $\var{reverse}$. On the conceptual level, the function is embarrassingly bijective
and should be straightforward to invert. However, in practice the story is much more complicated, especially for the
linear-time accumulative list reversal (the naive non-accumulative implementation has quadratic complexity in a functional language).
It is well known in the program inversion literature <cit.>
that tail recursive functions (which are often needed for accumulation) are challenging to handle due to overlapping branch bodies.

The $\var{reverse}$ definition we use in the benchmark includes a small fix: it takes an additional parameter that represents the length of the list in the accumulation parameter. It is sufficient to guarantee the success of .

Class   As we can see,  also performs well for this class. But as explained above, the success is conditional on the input/output examples that the $\PUT$ is required to satisfy. Take $\var{append}$ as an example, if the following example is included, which demands the second list being filled before the original first list is fully reconstructed, the synthesis will fail, as a solution must have a different recursion structure from that of the sketch.

Original Source        (Original View)     Updated View     Updated Source
$([1,2,3,4], [5])$     $[1,2,3,4,5]$       $[6,2]$          $([6], [2])$

An interesting case is $\var{lines}$, which splits a string by $\texttt{'\textbackslash n'}$ to produce a list of strings. The synthesis becomes a lot harder when the examples (as seen in Table <ref>) require the preservation of the existence of the newline in the last position. This combined with structural
changes to the view list cannot be captured by the recursion structure of the
sketch, which explains the failure.

Functions such as $\var{lookup}$ completely lose the source structures.
Consequently,  will not be able to handle any example of structural changes. In the case of $\var{lookup}$, a structural change means that the view value is changed to another value associated to a different key in the source (as seen in Table <ref>). Just for demonstration, if only non-structural changes are considered, as in the following example
where the changed view does not switch to a different key,
will be able to successfully generate a program.

Original Source                        (Original View)     Updated View     Updated Source
$([(1,10), (2,200), (3,33)],\, 2)$     $200$               $10$             $([(1,10), (2,10), (3,33)],\, 2)$

However, this is not interesting as the strength of HOBiT lies in its ability to
handle structural changes through branch switching.

§.§ Larger and More Involved Example

Next, we evaluate  on some larger examples, which are closer to realistic use cases.
In particular, we look at two types of transformations: XML queries and string parsing.

§.§.§ XML Transformations

We examined six queries from  XML Query Use Cases[<https://www.w3.org/TR/xquery-use-cases>] (“TREE” Use Case).
Table <ref> provides brief explanations for these queries and

Figure <ref> shows the skeleton of the XML document used as the original source for them.
Such XML documents are represented in HOBiT by a rose-tree datatype.

We ignored Document Type Definitions for simplicity—we could handle such constraints by fusing a partial identity function checking them to a $\GET$ function.
We also provided the constant “title” as an auxiliary component to our synthesis engine.

Table <ref> contains the results of this experiment.
Column “Updates” indicates the updates of the source query triggered by the given input/output examples,
whereas columns “LOC$_\mathrm{in}$” and “LOC$_\mathrm{syn}$” denote the number of lines of code in the original and the synthesized query, respectively.

The results show that  can synthesize fairly large
HOBiT programs. In particular, the number of AST nodes synthesised ranges from 73 (for Q4) to 471 (for Q5),
corresponding to 17 lines of code for Q4 and 80 for Q5.
(The programs are too large to be displayed in the main body of this paper.
See Appendix <ref> for the concrete input and output of  for Q1,
which serves as a representative of the six to illustrate their complexity.)
(The programs are too large to be displayed in this document.
We refer interested readers to our extended report <cit.> for a full XML example.)

The reason Q6 takes significantly more time than the rest
is that it assumes that each section has a title
element. Consequently, when handling insertion of sections, the
generated reconciliation function needs to construct a section with a

<book><title>Data on the Web</title>
<author>Serge Abiteboul</author><author>Peter Buneman</author><author>Dan Suciu</author>
<section id="intro" difficulty="easy">
<title>Web Data and the Two Cultures</title>
<figure height="400" width="400">
<title>Traditional client/server architecture</title><image source="csarch.gif"/>
<section id="syntax" difficulty="medium">…</section>

An XML document used as an original source for Queries Q1 to Q6.

Explanations of the examined XML queries: the descriptions are quoted from XML Query Use Case, where “Book1” refers the source XML.

Problem     Description (quoted)
Q1          “Prepare a (nested) table of contents for Book1, listing all the sections and their titles. Preserve the original attributes of each <section> element, if any.”

Q2          “Prepare a (flat) figure list for Book1, listing all the figures and their titles. Preserve the original attributes of each <figure> element, if any.”

Q3          “How many sections are in Book1, and how many figures?”

Q4          “How many top-level sections are in Book1?”

Q5          “Make a flat list of the section elements in Book1. In place of its original attributes, each section element should have two attributes, containing the title of the section and the number of figures immediately contained in the section.”

Q6          “Make a nested list of the section elements in Book1, preserving their original attributes and hierarchy. Inside each section element, include the title of the section and an element that includes the number of figures immediately contained in the section.”

The results of experiments for XML examples.

Problem                 \(\mathrm{LOC}_\mathrm{in}\)      \(\mathrm{AST}_\mathrm{in}\)     Updates in I/O examples                        Time (s)                             \(\mathrm{LOC}_\mathrm{syn}\)     \(\mathrm{AST}_\mathrm{syn}\)
3*Q1     3*11               3*136             Add attribute(s)                               3*0.35      3*42               3*319

Remove section(s)

Change title(s) and attribute value(s)
4*Q2     4*23               4*199             Remove figure(s)                               4*0.97      4*69               4*406

Change title(s)

Change attribute value(s)

Add Attribute
3*Q3     3*20               3*191             Decrease figure count                          3*0.43      3*63               3*339

Increase section count

Decrease section count
2*Q4     2*9                2*97              Increase section count                         2*0.14                2*26               2*170

Decrease section count
4*Q5     4*35               4*342             Decrease figure count                          4*1.20      4*115              4*813

Increase figure count

Remove section(s)

Change title(s)
4*Q6     4*31     4*236             Increase figure count(s)                       4*10.00     4*90               4*530

Decrease figure count(s)

Add section(s) with title and figure count

Change title(s)

§.§.§ Lexer and Parser

We also examined a simple recursive decent (specifically, LL(1)) lexer and parser.

The lexer takes in strings (i.e., $\{ \texttt{(}, \texttt{)}, \texttt{S}, \texttt{Z}, \texttt{+} \}^{*}$)
and returns a sequence of tokens represented by the following datatype.

Token = TNum Nat |LPar |RPar |Plus

Note that natural numbers such as  are processed in this step.
Then, the parser takes in the output of the lexer, , a sequence of the tokens above,
and returns an abstract syntax tree, according to the following grammar.

\[
s ::= n \mid \texttt{(}s\texttt{)} \texttt{+} \texttt{(} s \texttt{)}
\]

The lexer and parser considered here are injective, which is uncommon in practice.
Typically, a lexer loses information about white spaces (layouting) and comments,
and a parser may remove syntactic sugars and redundant parentheses[A notable exception is the parser for GHC/Haskell, which keeps syntactic sugars and parentheses for better error messaging.].

Sometimes, though, such lost information is attached to the abstract syntax trees,
making the parsing process injective <cit.>.

Experimental results for the lexer and parser.

\(\mathrm{LOC}_\mathrm{in}\)     \(\mathrm{AST}_\mathrm{in}\)
Time (s)     \(\mathrm{LOC}_\mathrm{syn}\)     \(\mathrm{AST}_\mathrm{syn}\)
Lexer      15                     88

Change on natural numbers
remove/insert tokens

0.094                            69                               265

Parser     10                     45
Replacement of whole AST and back

0.550                  29                                         121

Table <ref> summarizes the experimental results.

In Figure <ref>, we provide the parser generated by  as it is the more intricate of the two.
Notice that the $\con{LPAR}$ case in $\var{go}$ requires quite an involved reconciliation function.

\begin{align*}
\bb
\var{pExp} :: {\BX{[\con{Token}]}} \to {\BX{\con{Exp}}}                                                                                \\
\var{pExp} \A \var{ts} = \BLET~(e,[\,]) = \var{go} \A \var{ts}~\BIN~e                                                                                \\[\blanklineskip]%
\var{go} :: {\BX{[\con{Token}]}} \to \BX{(\con{Exp}, [\con{Token}])}                                                                                \\
\var{go} \A \var{ts} =
\BCASE~\var{ts}~\BOF~                                                                                \\
\ \ \
\bbt
\con{TNum} \A n:r & \to                                                                                & \bx{(}\bx{\con{ENum}} \A n\,\bx{,}\,r\bx{)}                                                                                \\
&                                                                                & \bbt \BWITH                                                               & \lambda v.\, \CASE~v~\OF~\{ (\con{ENum}\A\dontcare,\dontcare)\to \con{True};\;\dontcare \to \con{False}\}           \\
\BBY              & \lambda s.\lambda v.\, \CASE~v~\OF~\{ (\con{ENum}\A a,\dontcare)\to \con{TNum} \A a:s\} \ee                                                                                \\
\con{LPAR}:r_1    & \to                                                                                & \BLET~(e_1,\con{RPar}:\con{Plus}:\con{LPar}:r_2)=\var{go}\A\var{r_1}~\BIN                                                                                \\
&                                                                                & \BLET~(e_2,\con{RPar}:\con{Plus}:\con{LPar}:r_3)=\var{go}\A\var{r_2}~\BIN                                                                                \\
&                                                                                & \quad \bx{(}\bx{\con{EAdd}} \A e_1 \A e_2\,\bx{,}\, r_3\bx{)}                                                                                \\
&                                                                                & \bbt \BWITH                                                               & \lambda v.\,\CASE~v~\OF~\{ (\con{EAdd}\A\dontcare\A\dontcare,\dontcare)\to \con{True};\;\dontcare \to \con{False}\} \\
\BBY              & \lambda s.\lambda v.\,\CASE~v~\OF~\{ (\con{EAdd} \A \dontcare \A \dontcare, \dontcare) \to \con{LPar} : \con{TNum}\A\con{Z} : \con{RPar}: \con{Plus} :\con{LPar} : \con{TNum}\A\con{Z}:\con{RPar}:s\} \ee
\ee
\ee\end{align*}

Synthesized Bidirectional Parser

§.§ Comparison with Smyth

A fair comparison with other synthesis systems is not always easy
due to the different set-ups. For example, we
cannot compare directly with Optician <cit.>, the state of the art lens synthesizer, as its inputs and outputs
are too different from ours (see Section <ref> for a non-experimental comparison).

Instead, we pick Smyth <cit.>, a state-of-the-art synthesis tool that synthesizes unidirectional
programs from sketches and input/output
examples—a set-up that is similar to ours.
We provide to Smyth hand-written sketches of $\PUT$ in the form of “base case sketches” <cit.>, which are incomplete programs for which the step case branches are left as holes
while the base case branches are pre-filled, and the same input/output examples as the experiments in Table <ref>.
We omit the round-tripping requirement for Smyth and only
check whether the tool is able to produce $\PUT$ functions that satisfy the

Table <ref> shows the results of the comparison (with more details in the artifact [<https://doi.org/10.5281/zenodo.5494504>] or the repository[<https://github.com/masaomi-yamaguchi/synbit>]).
successfully synthesized 13 out of 15 cases, whereas Smyth succeeded only in 7 cases.
We believe that the main reason for the difference is the  required $\PUT$ functions tend to be quite complex, usually more so than their corresponding $\GET$.

It is worth noting that Smyth succeeded for $\var{lookup}$, where  failed.
For this particular case, a $\PUT$ program that conforms to the input/output example is represented by the key-value-flipped version of $\GET$, which was ruled out in  by a sketch.

Results of comparative experiments with Smyth: “No” means that Smyth reported failure in 10 min.
Problem                      Class                  Smyth
$\var{double}$                   Yes            Yes

$\var{uncurryReplicate}$         Yes            Yes

$\var{mapNot}$                   Yes            Yes

$\var{mapReplicate}$             Yes            Yes

$\var{snoc}$                     Yes        No

$\var{length}$                   Yes            Yes

$\var{lengthTail}$               Yes            Yes

$\var{reverse}$                  Yes        No

Problem               Class                  Smyth
$\var{mapFst}$            Yes        No

$\var{add}$               Yes        No

$\var{append}$            Yes        No

$\var{appendBc}$          Yes        No

$\var{professor}$         Yes        No

$\var{lines}$             Timeout        Timeout

$\var{lookup}$            Timeout        Yes

§ RELATED WORK

Optician <cit.> is the state-of-the-art framework for synthesizing lenses <cit.>.
Both their framework and ours implicitly guarantee the round-tripping properties
by using bidirectional programming languages (lenses/HOBiT) as targets. However, a direct comparison of performance is difficult due
to the very different set-ups. Their target lenses are specialized for string transformations, while HOBiT
considers general datatypes. And correspondingly, the core of their input specification is
regular expressions describing
data formats, while that of ours is standard functional programs serving as sketches.

Due to such differences in set-ups, even though we could translate a specification for Optician (regular expressions and input/output examples) to one for  (a $\GET$ program and input/output examples), such a translation would
involve many arbitrary choices (especially the choice of a  $\GET$ for Synbit) that affect synthesis,
effectively ruling out a meaningful comparison (see Appendix <ref>
for an illustrative example on the difficulty).

Despite the very different approaches,
it is interesting to observe a common design principle shared by both: leveraging the strengths of the underlying
bidirectional languages. Optician's regular-expression-based specification matches perfectly with the simplicity of the lens languages and their
close connection to advanced types, while  takes full advantage of HOBiT's alignment to conventional functional programming.
On a more technical note, Optician <cit.> is able to prioritize
the generated programs by quantitative information flow. It is not clear how this may be used in  as the
computation of the quantitative information flow will be difficult for a language with arbitrary recursion.

Other synthesis efforts for bidirectional programming

In a vision paper, <cit.> suggests some directions
of synthesizing bidirectional programs from $\GET$ programs by leveraging the round-tripping properties.
Specifically, he suggests using the round-tripping properties to generate input/output examples for synthesis.
Using <ref>, if one can generate $s$ in some ways (assuming the totality of $\GET$), then
examples of backward behavior may arise from $\PUT \A (s, \GET \A s) = s$. But a naive application of this
without considering <ref>
may result in incorrect $\PUT$ behavior such as $\PUT \A (s,v) = s$. To remedy the situation, Voigtländer suggests
restricting $\PUT$ to use the second argument $v$; , the argument must be relevant in the sense of relevant typing.
Voigtländer also suggests using <ref> to restrict the form of $\PUT$ to satisfy $\PUT \A (s,v) \in \GET^{-1}(v)$,
which is indeed effective for simple $\GET$s such as $\GET = \var{head}$ (in this case the right-hand side must have the form of $v : \dontcare$).
However, synthesis in this direction does not guarantee correctness with respect to round-tripping, and
an additional verification process will then be needed.

The PINS framework <cit.> applies path-based synthesis to program inversion, a program
transformation that derives the inverse of an (injective) program.
The path-based synthesis was able to derive inverses for involved programs such as LZ77 and LZW compression which the other existing inversion methods at the present time cannot handle.
However, since it focuses only on a finite number of paths, the system does not guarantee correctness: the resulting programs may not always be inverses.
PINS also uses sketches and component functions given by users.

Program inversion
Program inversion is a technique related to bidirectional programming, but there are important differences.
In program inversion, input programs are expected to be injective and thus serve as complete specifications,
which is not the case in bidirectional programming. As a result, in  input/output examples are used
to further specify the required backward behavior.

Despite the differences, program inversion and bidirectional programming do share some common techniques.
For example, using postconditions (as exit conditions in HOBiT) to determine control flows (especially branches) in inverses is a very common approach in the literature <cit.>.
A more interesting connection is the concept of partial inversion <cit.>, which uses
binding-time analysis before inversion so that the inverses can use static data as inputs as well.
Types in HOBiT can be seen as binding time where non-$\BX{}$-types are seen as static,
and our type-directed sketch generation (Section <ref>), with the lazy nondeterministic generation,
can be viewed as a type-based binding-time analysis <cit.>.
The idea of partial inversion is further extended so that the return values of inverses are treated as “static inputs” as well <cit.>, and
the pin operator <cit.> is proposed  to capture such a behavior
in an invertible language.

However, the utility of the operator in bidirectional programming rather than invertible programming is still under exploration,
and thus our current synthesis method does not include it.

Bidirectionalization is a program transformation that derives a bidirectional
transformation from a unidirectional transformation.
In a sense, this can be seen as a simple type of synthesis.

<cit.>, based on the constant-complement view updating <cit.>,
analyze injectivity (information-loss) of a program and then derive a complement by gathering lost information to obtain a bidirectional version.
This method requires a strong restriction on input programs for effective analysis: they must be affine (no variables can be used more than once) and treeless <cit.> (only variables can be arguments of functions) so that the injectivity analysis becomes exact.
<cit.> makes use of parametricity <cit.> to interpret polymorphic functions as bidirectional transformations. The technique is restricted to polymorphic functions. Probably more importantly, it can only handle non-structural updates—the equivalent of HOBiT without the ability of branch switching. Several extensions of the idea have been proposed <cit.>. In general, bidirectionalization is
far less expressive than the state-of-the-art synthesis frameworks such as Optician/lenses and /HOBiT.

General program synthesis

A popular direction in program synthesis that inspired our work is
program sketching, where programmers express their insights about a
program by writing sketches, i.e., partial programs encoding the
structure of a solution while leaving its low-level details
unspecified in the form of holes
<cit.>. As opposed to our technique,
<cit.> can only be applied to integer
benchmarks and does not support other data types such as lists or
trees. Also, it mostly focuses on properties, rather than examples, by
relying on Counterexample Guided Inductive Synthesis
(CEGIS) <cit.>, where a candidate
solution is iteratively refined based on counterexamples provided by a
verification technique. There is actually a large body of works based
on the CEGIS architecture
<cit.>. Often, such
approaches expect formal specifications describing the behavior of
the target program, which

can be difficult to write or expensive to check against using automated verification techniques.
Conversely, our specification consists of the unidirectional program and input/output
examples, which we believe is intuitive and easy to use, without
requiring prior understanding of logic.

The original work on program sketching has inspired a multitude of
follow-up directions.  Some of the most related to our work are
which, similarly to our technique, are type-directed and guided by input/output examples. As
opposed to these approaches, we exploit information about the
unidirectional program in order to prune the search space for the
bidirectional correspondent. As shown in our experimental
evaluation, simply applying synthesis techniques designed for
unidirectional code is not effective.

Another direction that inspired us is that of component-based
synthesis <cit.>, where the target program is generated by composing components from a library.  Similarly to these approaches, we
use a given library of components as the building blocks of our
program generation approach.

Equivalence reduction
Program synthesis techniques make use of equivalence reduction in order to
reduce the number of equivalent programs that get explored.
For example, <cit.>
prune the search space using observational equivalence with respect to a set of input/output examples, i.e., two programs are considered to be in the same equivalence class if, for all given inputs in the set of input/output examples, they produce the same outputs. Alternatively, <cit.> generate only programs in a specific normal form, where term rewriting is used to transform a program into its normal form. In <cit.>, Koukoutos et al. make use of attribute grammars to only produce certain types of expressions in their normal form, thus skipping other expressions
that are syntactically different, yet semantically equivalent.
In our work, we found that the lightweight heuristics described in Section <ref>
worked well. However, we do plan on exploring some of the equivalence
reduction techniques discussed here as future work.

§ CONCLUSION

We proposed a synthesis method for bidirectional transformations, whose novelty lies in the use of $\GET$ programs as sketches.
We described the idea in detail and implemented it in a prototype system , where
lazy nondeterministic generation has played an important role.
Through the experiments, we demonstrated the effectiveness of the proposed method and clarified its limitations.

A future direction is to make use of program analysis and verification techniques in the synthesis of exit conditions.
This would enable us to guarantee stronger soundness as discussed in Section <ref>.

Another future direction is to extend the target language (HOBiT) based on our experience in order to synthesize more bidirectional

We thank Eijiro Sumii and Oleg Kiselyov for their helpful and instructive comments on an earlier stage of this research,
and Hiroshi Unno for fruitful discussions on future directions.
This work was partially supported by JSPSJSPShttps://www.jsps.go.jp/ KAKENHI Grant Numbers JSPS15H02681, JSPS19K11892 and JSPS20H04161,
JSPS Bilateral Program, Grant Number JSPSJPJSBP120199913, Kayamorithe Kayamori Foundation of Informational Science Advancementhttp://www.kayamorif.or.jp/, EPSRCEPSRChttps://epsrc.ukri.org/ Grant EXHIBIT: Expressive High-Level Languages for Bidirectional Transformations (EPSRCEP/T008911/1), RoyalSocietyRoyal Society Grant Bidirectional Compiler for Software Evolution (RoyalSocietyIES\R3\170104), and Royal Society University Research Fellowship On Advancing Inductive Program Synthesis (RoyalSocietyUF160079).

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

[Abate, Bessa, Cattaruzza, Cordeiro, David,
Kesseli, Kroening, and PolgreenAbate et al2017]
authorpersonAlessandro Abate, personIury
Bessa, personDario Cattaruzza, personLucas C.
Cordeiro, personCristina David, personPascal
Kesseli, personDaniel Kroening, and personElizabeth
Polgreen. year2017.
Automated Formal Synthesis of Digital Controllers
for State-Space Physical Plants. In booktitleComputer Aided
Verification - 29th International Conference, CAV 2017, Heidelberg,
Germany, July 24-28, 2017, Proceedings, Part I
(seriesLecture Notes in Computer Science,
Vol. volume10426), editorpersonRupak
Majumdar and personViktor Kuncak (Eds.).
publisherSpringer, pages462–482.

[Abate, David, Kesseli, Kroening, and
PolgreenAbate et al2018]
authorpersonAlessandro Abate, personCristina
David, personPascal Kesseli, personDaniel Kroening,
and personElizabeth Polgreen. year2018.
Counterexample Guided Inductive Synthesis Modulo
Theories. In booktitleComputer Aided Verification - 30th
International Conference, CAV 2018, Held as Part of the Federated Logic
Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I
(seriesLecture Notes in Computer Science,
Vol. volume10981), editorpersonHana
Chockler and personGeorg Weissenbacher (Eds.).
publisherSpringer, pages270–288.

[Albarghouthi, Gulwani, and
KincaidAlbarghouthi et al2013]
authorpersonAws Albarghouthi, personSumit
Gulwani, and personZachary Kincaid.
Recursive Program Synthesis. In
booktitleComputer Aided Verification - 25th International
Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013.
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume8044), editorpersonNatasha
Sharygina and personHelmut Veith (Eds.).
publisherSpringer, pages934–950.

[Almendros-Jiménez and
VidalAlmendros-Jiménez and Vidal2006]
authorpersonJesús Manuel
Almendros-Jiménez and personGermán Vidal.
Automatic Partial Inversion of Inductively
Sequential Functions. In booktitleImplementation and
Application of Functional Languages, 18th International Symp osium, IFL
2006, Budapest, Hungary, September 4-6, 2006, Revised Selected Papers
(seriesLecture Notes in Computer Science,
Vol. volume4449),
editorpersonZoltán Horváth,
personViktória Zsók, and personAndrew
Butterfield (Eds.). publisherSpringer,

[Bancilhon and SpyratosBancilhon and
authorpersonFrançois Bancilhon and
personNicolas Spyratos. year1981.
Update Semantics of Relational Views.
journalACM Trans. Database Syst.
volume6, number4 (year1981),

[Bohannon, Foster, Pierce, Pilkiewicz, and
SchmittBohannon et al2008]
authorpersonAaron Bohannon, personJ. Nathan
Foster, personBenjamin C. Pierce, personAlexandre
Pilkiewicz, and personAlan Schmitt.
Boomerang: resourceful lenses for string data. In
booktitleProceedings of the 35th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2008, San Francisco,
California, USA, January 7-12, 2008,
editorpersonGeorge C. Necula and
personPhilip Wadler (Eds.). publisherACM,

[Chong, Cook, Kallas, Khazem, Monteiro,
Schwartz-Narbonne, Tasiran, Tautschnig, and TuttleChong
et al2020]
authorpersonNathan Chong, personByron Cook,
personKonstantinos Kallas, personKareem Khazem,
personFelipe R. Monteiro, personDaniel
Schwartz-Narbonne, personSerdar Tasiran,
personMichael Tautschnig, and personMark R.
Tuttle. year2020.
Code-level model checking in the software
development workflow. In booktitleICSE-SEIP 2020: 42nd
International Conference on Software Engineering, Software Engineering in
Practice, Seoul, South Korea, 27 June - 19 July, 2020,
editorpersonGregg Rothermel and
personDoo-Hwan Bae (Eds.). publisherACM,

[Damas and MilnerDamas and Milner1982]
authorpersonLuís Damas and
personRobin Milner. year1982.
Principal Type-Schemes for Functional Programs. In
booktitleConference Record of the Ninth Annual ACM
Symposium on Principles of Programming Languages, Albuquerque, New Mexico,
USA, January 1982, editorpersonRichard A. DeMillo
(Ed.). publisherACM Press, pages207–212.

[David, Kesseli, Kroening, and LewisDavid
et al2018]
authorpersonCristina David, personPascal
Kesseli, personDaniel Kroening, and personMatt
Lewis. year2018.
Program Synthesis for Program Analysis.
journalACM Trans. Program. Lang. Syst.
volume40, number2 (year2018),

[David, Kroening, and LewisDavid
et al2015]
authorpersonCristina David, personDaniel
Kroening, and personMatt Lewis.
Unrestricted Termination and Non-termination
Arguments for Bit-Vector Programs. In booktitleProgramming
Languages and Systems - 24th European Symposium on Programming, ESOP 2015,
Held as Part of the European Joint Conferences on Theory and Practice of
Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume9032), editorpersonJan Vitek
(Ed.). publisherSpringer, pages183–204.

[Davies and PfenningDavies and
authorpersonRowan Davies and personFrank
Pfenning. year2001.
A modal analysis of staged computation.
journalJ. ACM volume48,
number3 (year2001), pages555–604.

[de Jonge and Visserde Jonge and
authorpersonMaartje de Jonge and
personEelco Visser. year2011.
An Algorithm for Layout Preservation in Refactoring
Transformations. In booktitleSoftware Language Engineering
- 4th International Conference, SLE 2011, Braga, Portugal, July 3-4, 2011,
Revised Selected Papers (seriesLecture Notes in Computer
Science, Vol. volume6940),
editorpersonAnthony M. Sloane and
personUwe Aßmann (Eds.). publisherSpringer,

[Feng, Martins, Wang, Dillig, and RepsFeng
et al2017]
authorpersonYu Feng, personRuben Martins,
personYuepeng Wang, personIsil Dillig, and
personThomas W. Reps. year2017.
Component-based synthesis for complex APIs. In
booktitleProceedings of the 44th ACM SIGPLAN Symposium
on Principles of Programming Languages, POPL 2017, Paris, France, January
18-20, 2017, editorpersonGiuseppe Castagna and
personAndrew D. Gordon (Eds.). publisherACM,

[Feser, Chaudhuri, and DilligFeser
et al2015]
authorpersonJohn K. Feser, personSwarat
Chaudhuri, and personIsil Dillig.
Synthesizing data structure transformations from
input-output examples. In booktitleProceedings of the 36th
ACM SIGPLAN Conference on Programming Language Design and Implementation,
Portland, OR, USA, June 15-17, 2015,
editorpersonDavid Grove and
personStephen M. Blackburn (Eds.). publisherACM,

[Fischer, Kiselyov, and ShanFischer
et al2011]
authorpersonSebastian Fischer, personOleg
Kiselyov, and personChung-chieh Shan.
Purely functional lazy nondeterministic
journalJ. Funct. Program. volume21,
number4-5 (year2011), pages413–465.

[Foster, Greenwald, Moore, Pierce, and
SchmittFoster et al2007]
authorpersonJ. Nathan Foster,
personMichael B. Greenwald, personJonathan T. Moore,
personBenjamin C. Pierce, and personAlan Schmitt.
Combinators for bidirectional tree transformations:
A linguistic approach to the view-update problem.
journalACM Trans. Program. Lang. Syst.
volume29, number3 (year2007).

[Foster, Pilkiewicz, and PierceFoster
et al2008]
authorpersonJ. Nathan Foster,
personAlexandre Pilkiewicz, and personBenjamin C.
Pierce. year2008.
Quotient lenses. In
booktitleProceeding of the 13th ACM SIGPLAN
international conference on Functional programming, ICFP 2008, Victoria,
BC, Canada, September 20-28, 2008, editorpersonJames
Hook and personPeter Thiemann (Eds.).
publisherACM, pages383–396.

[Glück and KawabeGlück and
authorpersonRobert Glück and
personMasahiko Kawabe. year2005.
Revisiting an automatic program inverter for Lisp.
journalSIGPLAN Notices volume40,
number5 (year2005), pages8–17.

[Gomard and JonesGomard and Jones1991]
authorpersonCarsten K. Gomard and
personNeil D. Jones. year1991.
A Partial Evaluator for the Untyped
journalJ. Funct. Program. volume1,
number1 (year1991), pages21–69.

authorpersonDavid Gries.
booktitleThe Science of Programming.
publisherSpringer, Heidelberg, Chapter 21 Inverting

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

authorpersonStephen J. Hegner.
Foundations of Canonical Update Support for Closed
Database Views. In booktitleICDT
(seriesLecture Notes in Computer Science,
Vol. volume470), editorpersonSerge
Abiteboul and personParis C. Kanellakis (Eds.).
publisherSpringer, pages422–436.

[Hofmann, Pierce, and WagnerHofmann
et al2011]
authorpersonMartin Hofmann,
personBenjamin C. Pierce, and personDaniel Wagner.
Symmetric lenses. In
booktitleProceedings of the 38th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2011, Austin, TX,
USA, January 26-28, 2011, editorpersonThomas Ball
and personMooly Sagiv (Eds.). publisherACM,

[Hu and KoHu and Ko2016]
authorpersonZhenjiang Hu and
personHsiang-Shang Ko. year2016.
Principles and Practice of Bidirectional
Programming in BiGUL. In booktitleBidirectional
Transformations - International Summer School, Oxford, UK, July 25-29, 2016,
Tutorial Lectures (seriesLecture Notes in Computer
Science, Vol. volume9715),
editorpersonJeremy Gibbons and
personPerdita Stevens (Eds.). publisherSpringer,

[Jha, Gulwani, Seshia, and TiwariJha
et al2010]
authorpersonSusmit Jha, personSumit
Gulwani, personSanjit A. Seshia, and personAshish
Tiwari. year2010.
Oracle-guided component-based program synthesis.
In booktitleProceedings of the 32nd ACM/IEEE International
Conference on Software Engineering - Volume 1, ICSE 2010, Cape Town, South
Africa, 1-8 May 2010, editorpersonJeff Kramer,
personJudith Bishop, personPremkumar T. Devanbu,
and personSebastián Uchitel (Eds.).
publisherACM, pages215–224.

authorpersonSusumu Katayama.
Systematic search for lambda expressions. In
booktitleRevised Selected Papers from the Sixth Symposium on
Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24
September 2005 (seriesTrends in Functional Programming,
Vol. volume6), editorpersonMarko C. J. D.
van Eekelen (Ed.). publisherIntellect,

[Kiselyov and ThompsonKiselyov and
editorpersonOleg Kiselyov and
personSimon J. Thompson (Eds.). year2012.
booktitleProceedings of the ACM SIGPLAN 2012
Workshop on Partial Evaluation and Program Manipulation, PEPM 2012,
Philadelphia, Pennsylvania, USA, January 23-24, 2012.

[Kneuss, Kuraj, Kuncak, and SuterKneuss
et al2013]
authorpersonEtienne Kneuss, personIvan
Kuraj, personViktor Kuncak, and personPhilippe
Suter. year2013.
Synthesis modulo recursive functions. In
booktitleProceedings of the 2013 ACM SIGPLAN
International Conference on Object Oriented Programming Systems Languages
& Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN,
USA, October 26-31, 2013, editorpersonAntony L.
Hosking, personPatrick Th. Eugster, and
personCristina V. Lopes (Eds.). publisherACM,

[Ko, Zan, and HuKo et al2016]
authorpersonHsiang-Shang Ko, personTao
Zan, and personZhenjiang Hu. year2016.
BiGUL: a formally verified core language for
putback-based bidirectional programming. In
booktitleProceedings of the 2016 ACM SIGPLAN Workshop on
Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL,
USA, January 20 - 22, 2016, editorpersonMartin
Erwig and personTiark Rompf (Eds.).
publisherACM, pages61–72.

authorpersonRichard E. Korf.
Inversion of Applicative Programs. In
editorpersonPatrick J. Hayes (Ed.).
publisherWilliam Kaufmann, pages1007–1009.

[Kort and LämmelKort and
authorpersonJan Kort and personRalf
Lämmel. year2003.
Parse-Tree Annotations Meet Re-Engineering
Concerns. In booktitle3rd IEEE International Workshop on
Source Code Analysis and Manipulation (SCAM 2003), 26-27 September 2003,
Amsterdam, The Netherlands. publisherIEEE Computer Society,

[Koukoutos, Kneuss, and KuncakKoukoutos
et al2016]
authorpersonManos Koukoutos, personEtienne
Kneuss, and personViktor Kuncak.
An Update on Deductive Synthesis and Repair in the
Leon Tool. In booktitleProceedings Fifth Workshop on
Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016
(seriesEPTCS, Vol. volume229),
editorpersonRuzica Piskac and
personRayna Dimitrova (Eds.). pages100–111.

[Lubin, Collins, Omar, and ChughLubin
et al2020]
authorpersonJustin Lubin, personNick
Collins, personCyrus Omar, and personRavi Chugh.
Program sketching with live bidirectional
journalProc. ACM Program. Lang.
volume4, numberICFP (year2020),

authorpersonChristopher Lutz.
titleJanus: a time-reversible language.
Letter to R. Landauer. Available on:

[Maina, Miltner, Fisher, Pierce, Walker, and
ZdancewicMaina et al2018]
authorpersonSolomon Maina, personAnders
Miltner, personKathleen Fisher, personBenjamin C.
Pierce, personDavid Walker, and personSteve
Zdancewic. year2018.
Synthesizing quotient lenses.
journalProc. ACM Program. Lang.
volume2, numberICFP (year2018),

[Matsuda, Hu, Nakano, Hamana, and
TakeichiMatsuda et al2007]
authorpersonKazutaka Matsuda,
personZhenjiang Hu, personKeisuke Nakano,
personMakoto Hamana, and personMasato Takeichi.
Bidirectionalization transformation based on
automatic derivation of view complement functions. In
booktitleProceedings of the 12th ACM SIGPLAN
International Conference on Functional Programming, ICFP 2007, Freiburg,
Germany, October 1-3, 2007, editorpersonRalf Hinze
and personNorman Ramsey (Eds.). publisherACM,

[Matsuda, Inaba, and NakanoMatsuda
et al2012]
authorpersonKazutaka Matsuda, personKazuhiro
Inaba, and personKeisuke Nakano.
Polynomial-time inverse computation for
accumulative functions with multiple data traversals, See
DBLP:conf/pepm/2012, pages5–14.

[Matsuda, Mu, Hu, and TakeichiMatsuda
et al2010]
authorpersonKazutaka Matsuda,
personShin-Cheng Mu, personZhenjiang Hu, and
personMasato Takeichi. year2010.
A Grammar-Based Approach to Invertible Programs.
In booktitleESOP (seriesLecture Notes in
Computer Science, Vol. volume6012),
editorpersonAndrew D. Gordon (Ed.).
publisherSpringer, pages448–467.

[Matsuda and WangMatsuda and Wang2015a]
authorpersonKazutaka Matsuda and
personMeng Wang. year2015a.
Applicative bidirectional programming with lenses.
In booktitleProceedings of the 20th ACM SIGPLAN
International Conference on Functional Programming, ICFP 2015, Vancouver,
BC, Canada, September 1-3, 2015,
editorpersonKathleen Fisher and
personJohn H. Reppy (Eds.). publisherACM,

[Matsuda and WangMatsuda and Wang2015b]
authorpersonKazutaka Matsuda and
personMeng Wang. year2015b.
"Bidirectionalization for free" for monomorphic
journalSci. Comput. Program.
volume111 (year2015), pages79–109.

[Matsuda and WangMatsuda and Wang2018a]
authorpersonKazutaka Matsuda and
personMeng Wang. year2018a.
Applicative bidirectional programming: Mixing
lenses and semantic bidirectionalization.
journalJ. Funct. Program.  volume28
(year2018), pagese15.

[Matsuda and WangMatsuda and Wang2018b]
Matsuda   Wang:2018:HOBiT
authorpersonKazutaka Matsuda and
personMeng Wang. year2018b.