Confluence in Lens Synthesis
Anders Miltner1 , Kathleen Fisher2 , Benjamin C. Pierce3 , David Walker4 , andSteve Zdancewic5
1

Princeton University
amiltner@cs.princeton.edu
2
Tufts University
kfisher@eecs.tufts.edu
3
University of Pennsylvania
bcpierce@cis.upenn.edu
4Princeton University
dpw@cs.princeton.edu
5
University of Pennsylvania
stevez@cis.upenn.edu
Abstract
A lens is a program that can be executed both forwards and backwards, from input tooutput and from output back to input again. Domain-specific languages for defining lenses
have been developed to help users synchronize text files, and construct different “views” ofdatabases, among other applications. Recent research has shown how string lenses can besynthesized from their types, which are pairs of regular expressions. However, guaranteeingthat we can synthesize all possible lenses is quite tricky on these languages, due in largepart to the many equivalences on regular expressions.
The proof that all string lenses are synthesizeable involves proving a confluence-like
property, parameterized by a an additional binary relation R. We call this property Rconfluence. In this model, standard confluence is the specific case where R is equality. In
this paper, we show how existing techniques for demonstrating confluence do not work in
the domain of R-confluence, and find that if the rewrite system is =-confluent and satisfies
a commutativity property with R, then the system is R-confluent.

1Introduction

Bidirectional transformations are pervasive in modern software systems, occuring as database
views and view updaters, parsers and pretty-printers, data synchronization tools, and more.
Instead of manually building the functions that comprise a bidirectional transformation, programmers can build them both “at once” using a bidirectional programming language. Bidirectional
programming languages have been developed for creating view updaters [3], Linux configuration
file editors [1], direct manipulation programming systems [11], and more [7, 5, 18]. Lenses area particularly well-behaved class of bidirectional programs, where the underlying transformations are guaranteed to satisfy a number of “round-tripping” laws. Lens-based bidirectional
programming languages often provide round-tripping guarantees through a set of typing rules;
well-typed lens expressions are guaranteed to satisfy the round-tripping laws.
Optician [13], an extension of Boomerang, makes bidirectional programming easier by
supporting synthesis of bidirectional string transformations. More specifically, it takes as input
two regular expressions (R and S , which serve as the type of a Boomerang lens) and a setof examples specifying input-output behavior, and synthesizes a well-typed lens between thelanguages of those regular expressions. For brevity, we will not provide formal definitions forsome aspects of Optician; the interested reader can find such definitions in the original Optician

Confluence in Lens Synthesis

Miltner, Fisher, Pierce, Walker and Zdancewicpaper [13]. Furthermore, examples detailing the use of synthesized lenses in practice (which wealso elide for space) can be found in that paper and follow-up work [8, 14].
To indicate a lens l is well typed, and converts between the languages of R and S , we writel : R ⇔ S . For synthesis, given R and S , we must find a lens l such that l : R ⇔ S . Inthe context of lens synthesis, there are three sorts of lens typing rules: syntax-directed rules,composition, and type equivalence.
For syntax-directed rules, the syntax for the types closely mirrors the syntax of the expressions.
As an example, consider the following rule for disjunction:Or Lens

l1 : R1 ⇔ S1
l2 : R2 ⇔ S2
L(R1 ) ∩ L(R2 ) = ∅L(S1 ) ∩ L(S2 ) = ∅or (l1 , l2 ) : R1 | R2 ⇔ S1 | S2Consider finding a lens of type R1 | R2 ⇔ S1 | S2 . With only syntax-directed rules, the onlylens that can be well-typed would be an or lens.
Composition sequentially composes two lenses.
Composition

l1 : R1 ⇔ R2
l2 : R2 ⇔ R3
l1 ; l2 : R1 ⇔ R3

Composition is difficult in the context of lens synthesis. If trying to synthesize a composition
lens, one has to pull the central regular expression “out of thin air.”
The last typing rule is type-equivalence. If two regular expressions are star-semiring equivalent
to the type of a lens, those equivalent regular expressions also serve as the type of the lens.
Type Equivalencel :R⇔S

R ≡s R 0
l : R0 ⇔ S 0

S ≡s S 0

This rule is difficult in the context of synthesis, as it forces a search through equivalent regularexpressions. This rule can also be applied at any point in the derivation, which makes the searcheven harder.
To address the difficulties with composition and type-equivalence rules, we synthesize lenses inan alternative language of disjunctive normal form (DNF) lenses. DNF lenses are in pseudonormalform, containing no composition operator, and so their synthesis never needs to pull regularexpressions “out of thin air.” The types of DNF lenses are pairs of regular expressions ina pseudonormal form, DNF regular expressions. Because DNF regular expressions are in a
pseudonormal form, fewer equivalent regular expressions need to be searched through.
In our search algorithm, we only search through equivalent regular expressions once, before
processing any syntax directed-rules. We formalize this in the typing of DNF regular expressions
by only permitting the application of type-equivalence once, after all syntactic rules have been
applied. This is enforced by having two typing judgements: one for the “rewriteless” type of thelens (meaning no type-equivalence rules were applied) and one of the “full” type of the lens. Ifdl :̃ DR ⇔ DS , then dl is a DNF lens of rewriteless type DR ⇔ DS . If dl : DR ⇔ DS , then dl
is a DNF lens of full type DR ⇔ DS . The following rule is used to get the full type of a DNF
lens from the rewriteless type.
Rewrite DNF Regex Lens

DR 0 →∗ DR

2DS 0 →∗ DSdl :̃ DR ⇔ DS00dl : DR ⇔ DSConfluence in Lens Synthesis

Miltner, Fisher, Pierce, Walker and Zdancewic

dl2 ~: DR3 ⇔ DS3...

...

DR2...

DS2...

...

...

dl1 ~: DR1 ⇔ DS1⇓R2...

⇓S2...

⇓R1⇓S1

Figure 1: Diagram constructing a well-typed DNF lens between ⇓ R2 and ⇓ S2 . Single lined
arrows indicate rewrites (→), and triple lines indicate equivalence (≡→ ).
Note that instead of using directionless equivalences, Rewrite DNF Regex Lens uses
directioned rewrites. The relationship between the two is formalized by the following theorem:Theorem 1. If R ≡s S , then ⇓ R ≡→ ⇓ S , where ⇓ R and ⇓ S are R and S in DNF form
(respectively), and ≡→ is the reflexive, transitive, and symmetric closure of →.
Proving that our search procedure can generate any lens reduces to proving DNF lenses
complete with respect to our standard lens language. In particular, we wish the prove:
Theorem 2. If l : R ⇔ S , then there exists a DNF lens, dl , such that dl :⇓R ⇔⇓S and thesemantics of l and dl are equivalent.
We prove this propety by induction on the structure of the typing derivation. Particulardifficulty lies in the lens equivalence rule. We begin this case below:l : R 1 ⇔ S1R 1 ≡s R 2
l : R2 ⇔ S 2

S1 ≡ s S2

By induction assumption, there exists dl :⇓R1 ⇔⇓S1 , where the semantics of dl are equivalent
to those of l . By inversion on the derivation of dl :⇓R1 ⇔⇓S1 , there exists DR 1 and DS 1 suchthat:
⇓R1 →∗ DR 1

⇓S1 →∗ DS 1dl :̃ DR 1 ⇔ DS 1dl :⇓R1 ⇔⇓S1

To complete this case, we need to find a DNF lens dl 0 :⇓R2 ⇔⇓S2 with equivalent semantics
to l .
We first show that there exist DR 2 and DS 2 such that ⇓R2 →∗ DR 2 and ⇓DR 1 →∗ DR 2 and⇓S2 →∗ DS 2 and ⇓DS 1 →∗ DS 2 . To do this, we first prove that → is confluent. By Theorem 1,we know that ⇓R1 ≡→ ⇓R2 , so confluence implies the existance of such a DR 2 and DS 2 .
After this, we have dl :̃ DR 1 ⇔ DS 1 and DR 1 →∗ DR 2 and DS 1 →∗ DS 2 . If we can provea confluence-like property that would show the existance of some dl 0 :̃ DR 3 ⇔ DS 3 , where
DR 2 →∗ DR 3 and DS 2 →∗ DS 3 , we would be done. This property is R-confluence for a properlychosen R (which we describe in §2). This case is diagrammed in Figure 1.
3

Confluence in Lens Synthesis

Miltner, Fisher, Pierce, Walker and Zdancewics2

R(s1,t)Figure 2: Rewrite system that satisfies the R-diamond property, but is not R-confluent.

2R-Confluence Formulation

Let S be an underlying set, and → and R be binary relations. The rewrite system (S, →) isR-confluent, if for all s1 , s2 ∈ S, if R(s1 , s2 ), s1 →∗ s01 , and s2 →∗ s02 , then there exist s001 and s002
such that R(s001 , s002 ), s01 →∗ s001 , and s2 →∗ s002 .
In the context of lens synthesis, S is the set of DNF REs, the rewrites are →∗ , and given a
DNF lens dl , Rdl (DR, DS ) is true if there exists a DNF lens dl 0 such that dl 0 :̃ DR ⇔ DS anddl is equivalent to dl 0 .
Now that R-confluence has been formally defined, we can ask ourselves: “What is a goodapproach to proving R-confluence?” One approach is to prove that our rewrite system is locallyconfluent, which is equivalent to =-confluence in a terminating system [6]. Unfortunately, ourrewrites are not terminating, so this approach does not work.
An approach pioneered by Tait and Martin-Löf [2] still works in non-terminating systems.
This approach uses the diamond property: A rewrite system (S, →) satisfies the diamondproperty if s1 → s2 and s1 → s3 implies that there exists s4 such that s2 → s4 , and s2 → s4 . Ifa rewrite system satisfies the diamond property, then it is also confluent. Unfortunately, thisapproach does not work, as the parameterized version of the diamond property does not imply
R-confluence.

3Proving (S,→∗ ) R-Confluent

In the Tait and Martin-Löf approach to proving (S, →) confluent, one must first prove (S, →)satisfies the diamond property. Consider a parameterized property analogous to the diamondproperty, the R-diamond property: A rewrite system (S, →) satisfies the R-diamond property ifs1 → s2 and t1 → t2 and R(s1 , t1 ) implies that there exists s3 , t3 such that s2 → s3 and t2 → t3and R(s3 , t3 ).
However, satisfying the R-diamond property is not sufficient for R-confluence. Consider thesimple rewrite system shown in Figure 2. In this rewrite system, there are 3 elements, s1 , s2 ,and t. In this setup, R(s1 , t) and s1 → s2 . R-confluence requires some s3 , t0 such that s2 →∗ s3and t→∗ t0 and R(s3 , t0 ), but no such values exist.
To get around this issue, we require a different set of properties.
1. (S, →) must be =-confluent.
2. R must be a bisimilulation relation for (S, →∗ ). In other words if R(s1 , t1 ), and s1 →∗ s2 ,then there exists t2 such that t1 →∗ t2 and R(s2 , t2 ); and if R(s1 , t1 ), and t1 →∗ t2 , thenthere exists s2 such that s1 →∗ s2 and R(s2 , t2 ).
Theorem 3. Let (S, →) be =-confluent, and R be a bisimilulation relation for (S, →∗ ). IfR(s1 , t1 ) and s1 →∗ s2 and t1 →∗ t2 , then there exists s3 , t3 such that s2 →∗ s3 and t2 → t3 andR(s3 , t3 ).
4Confluence in Lens Synthesis

Miltner, Fisher, Pierce, Walker and Zdancewic

R(s5,t5)
...

...
s3

R(s4,t4)
...

...

s2

t2
...

...

R(s1,t1)

Figure 3: Diagram showing how we prove the inductive case of R-confluence of the transitive
closure of a rewrite system. R(s4 , t4 ) comes from the inductive hypothesis. The existance of s5
is guaranteed through =-confluence. R(s5 , t5 ) is guaranteed because R is a bisimulation relation.
Proof. By induction length of the reduction of s1 →∗ s2
Case 1 (Base Case). Let R(s1 , t1 ) and t1 →∗ t2 . As R is a bisimulation relation for (S, →∗ ), there
exists s2 such that s1 →∗ s2 and R(s2 , t2 ), as desired.
Case 2 (Inductive Case). Let R(s1 , t1 ) and s1 →∗ s2 and s2 → s3 and t1 →∗ t2 . By the induction
hypothesis, there exists s4 , t4 such that R(s4 , t4 ) and s2 →∗ s4 and t2 → t4 .
Because (S, →) is =-confluent, there exists s5 such that s3 →∗ s5 and s4 →∗ s5 . As (S, →∗ ) isa bisimilulation relation on (S, →∗ ), there exists t5 such that t4 →∗ t5 and R(s5 , t5 ), as desired.
This case is diagrammed in Figure 3.

4

Related Work

The concept of R-confluence is related to the notion of confluence modulo ∼ [6]. The definitionof confluent modulo ∼ is almost the same as ∼-confluence, the only difference is that confluence
modulo ∼ requires ∼ to an equivalence relation. Conditions that suffice to prove a rewrite
system confluent modulo ∼ are not generally sufficient to prove R-confluence (and vice versa).
Furthermore, our bisimulation relations are closely related to local coherence modulo ∼ .
Bisimulation relations come from concurrency theory [15], but a related notion, commuting
rewrites [16], appear in the confluence literature. We require a single rewrite of R to commute
with an arbitrary number of rewrites of →, which commuting rewrites do not express.
The full proof of completeness is contained in the appendix of the full version of the original
optician paper [12]. The original proof of R-confluence for the transitive closure of → required
additional assumptions. These unnecessary assumptions have been identified and removed in thispaper. Future work used the proof of completeness over our lens language to show that quotientbijective lenses are also synthesizeable [8]. Lastly, while synthesizeability was not proven forsymmetric lenses [14], such a proof would likely have proven R-confluence in a similar manner.
This work continues a trend in making programming easier through synthesis [4]. Whilesynthesis is one approach to make bidirectional programming easier, it is not the only approach.
Work has gone into building lenses without requiring a point-free combinator style [10]. Otherwork has found applicative [9] and monadic [17] approaches to compositionally building lenses.
5Confluence in Lens Synthesis

Miltner, Fisher, Pierce, Walker and Zdancewic

References[1] Augeas - A configuration API. http://augeas.net/index.html.
[2] H. P. Barendregt. The Lambda Calculus Its Syntax and Semantics, volume 103. North Holland,
revised edition, 1984. http://www.cs.ru.nl/ henk/Personal Webpage.
[3] Aaron Bohannon, Jeffrey A. Vaughan, and Benjamin C. Pierce. Relational lenses: A language for
updateable views. In Principles of Database Systems (PODS), 2006. Extended version available as
University of Pennsylvania technical report MS-CIS-05-27.
[4] Sumit Gulwani, Alex Polozov, and Rishabh Singh. Program Synthesis, volume 4. NOW, August2017.
[5] Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato, Kazutaka Matsuda, and Keisuke
Nakano. Bidirectionalizing graph transformations. In Proceeding of the 15th ACM SIGPLAN
international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA,September 27-29, 2010, pages 205–216, 2010.
[6] Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems:
Abstract properties and applications to term rewriting systems. J. ACM, 27(4):797–821, October
1980.
[7] Hsiang-Shang Ko, Tao Zan, and Zhenjiang Hu. BiGUL: A formally verified core language forputback-based bidirectional programming. In Proceedings of the 2016 ACM SIGPLAN Workshop
on Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL, USA, January
20 - 22, 2016, pages 61–72, 2016.
[8] Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve
Zdancewic. Synthesizing quotient lenses. Proc. ACM Program. Lang., 2(ICFP), July 2018.
[9] Kazutaka Matsuda and Meng Wang. Applicative bidirectional programming with lenses. SIGPLAN
Not., 50(9):62–74, August 2015.
[10] Kazutaka Matsuda and Meng Wang. Hobit: Programming lenses without using lens combinators.
In Amal Ahmed, editor, Programming Languages and Systems, pages 31–59, Cham, 2018. Springer
International Publishing.
[11] Mikaël Mayer, Viktor Kuncak, and Ravi Chugh. Bidirectional evaluation with direct manipulation.
Proc. ACM Program. Lang., 2(OOPSLA), October 2018.
[12] Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic.
Synthesizing bijective lenses, 2017. https://arxiv.org/abs/1710.03248.
[13] Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. Synthesizing bijective lenses. In Proceedings of the 45th Annual ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, POPL 2018, 2018.
[14] Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve
Zdancewic. Synthesizing symmetric lenses. Proc. ACM Program. Lang., 3(ICFP), July 2019.
[15] Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press,USA, 2011.
[16] Yoshihito Toyama. Commutativity of term rewriting systems. Programming of future generation
computers II, pages 393–407, 1988.
[17] Li-yao Xia, Dominic Orchard, and Meng Wang. Composing bidirectional programs monadically. InLuı́s Caires, editor, Programming Languages and Systems, pages 147–175, Cham, 2019. Springer
International Publishing.
[18] Zirun Zhu, Hsiang-Shang Ko, Pedro Martins, João Saraiva, and Zhenjiang Hu. Biyacc: Roll
your parser and reflective printer into one. In Proceedings of the 4th International Workshop on
Bidirectional Transformations co-located with Software Technologies: Applications and Foundations,
STAF 2015, L’Aquila, Italy, July 24, 2015., pages 43–50, 2015.

6