Confluence in Lens Synthesis
Anders Miltner, Kathleen Fisher, Benjamin Pierce, David Walker, Steve Zdancewic

1

Lenses?

2

Lenses are Synchronizers
Lens

3Lenses are Synchronizers
Lens
getputcreate4

Lenses are Synchronizers
Lens

5Lenses are Synchronizers
Lens{}

lname : Milton,
fname : Andrés

6

Lenses are Synchronizers
Lens{}

lname : Milton,
fname : Andrésget

7

Andrés Milton

Lenses are Synchronizers
Lens{}

lname : Milton,
fname : AndrésAndrés Milton

8Lenses are Synchronizers
Lens{}

lname : Milton,
fname : AndrésAnders Miltner9

Lenses are Synchronizers
Lens{}

lname : Milton,
fname : Andrés

put

10Anders Miltner

Lenses are Synchronizers
Lens{}

lname : Miltner,
fname : Anders

put

11

Anders Miltner

Lenses are Pervasive
Lens Variants

Lens Domains

Bĳections

Strings

Classical Lenses

Relational Algebras

Quotient Lenses

Parsing + Pretty Printing

Symmetric Lenses

Data Structures

Edit Lenses

Sets

Simple Symmetric Lenses

Combinations of Above12

Lenses are Pervasive
Lens Variants

Lens Domains

BĳectionsStrings

Classical Lenses

Relational Algebras

Quotient Lenses

Parsing + Pretty Printing

Symmetric Lenses

Data Structures

Edit Lenses

Sets

Simple Symmetric Lenses

Combinations of Above

DSLs for writing lenses in various domains
13

Lenses are Pervasive
Lens Variants

Lens Domains

Bĳections

Strings

14

Lenses are Pervasive
Lens Variants

Lens Domains

Bĳections

Strings

15[Bohannon, et. al. 2008]

Ad-Hoc RegEx

JSON RegEx

Lens e16

Stephen Cole Kleene

Kleene, Stephen Cole

let name= [A-Z][a-z]* inlet name_map= Id(name) inlet first_map = name_map ~ Id(“ “) in
let firsts_map = first_map* in
let sep_map= const(“”,”,”) in
let head_map= sep_map . firsts_map in
head_map ~ name_map

17Stephen Cole Kleene

Kleene, Stephen Cole

let name= [A-Z][a-z]* in
let name_map= Id(name) in
let first_map = name_map ~ Id(“ “) in
let firsts_map = first_map* in
let sep_map= const(“”,”,”) in
let head_map= sep_map . firsts_map in
head_map ~ name_map

18Stephen Cole Kleene

Kleene, Stephen Cole

let name= [A-Z][a-z]* in
let name_map= Id(name) in
let first_map = name_map ~ Id(“ “) in
let firsts_map = first_map* in
let sep_map= const(“”,”,”) in
let head_map= sep_map . firsts_map in
head_map ~ name_map

19Stephen Cole Kleene

Kleene, Stephen Cole

let name= [A-Z][a-z]* in
let name_map= Id(name) in
let first_map = name_map ~ Id(“ “) in
let firsts_map = first_map* in
let sep_map= const(“”,”,”) in
let head_map= sep_map . firsts_map in
head_map ~ name_map

20Stephen Cole Kleene

Kleene, Stephen Cole

let name= [A-Z][a-z]* in
let name_map= Id(name) in
let first_map = name_map ~ Id(“ “) in
let firsts_map = first_map* in
let sep_map= const(“”,”,”) in
let head_map= sep_map . firsts_map in
head_map ~ name_map

21Stephen Cole Kleene

Kleene, Stephen Cole

let name= [A-Z][a-z]* in
let name_map= Id(name) in
let first_map = name_map ~ Id(“ “) in
let firsts_map = first_map* in
let sep_map= const(“”,”,”) in
let head_map= sep_map . firsts_map in
head_map ~ name_map

22Stephen Cole Kleene

Kleene, Stephen Cole

let name= [A-Z][a-z]* in
let name_map= Id(name) in
let first_map = name_map ~ Id(“ “) in
let firsts_map = first_map* in
let sep_map= const(“”,”,”) in
let head_map= sep_map . firsts_map in
head_map ~ name_map

23Stephen_Cole_Kleene

Kleene,_Stephen_Cole

let name= [A-Z][a-z]* in
let name_map= Id(name) in
let first_map = name_map ~ Id(“ “) in
let firsts_map = first_map* in
let sep_map= const(“”,”,”) in
let head_map= sep_map . firsts_map in
head_map ~ name_map

24

Lens Grammare :=const(s1,s2)| Id(R)| e1 . e2| e1 ~ e2| e1 | e2| e*| e1 ; e225constant
identity
concatenation
swap
union
iteration
composition

Lens Typing Judgment
Why?

26

Lens Typing Judgment
Why?
1. To specify the languages the lens
maps between

27

Lens Typing Judgment
Why?
1. To specify the languages the lens
maps between
2. To guarantee that the get and put
functions are well-defined, and areinverses

28

Lens Typing Judgment
Why?
1. To specify the languages the lens
maps between
2. To guarantee that the get and put
functions are well-defined, and areinversesAlso… it’s useful for synthesis!

29Lens Typing Judgment

e:R⇔S

30

Lens Typing Judgment
Regular Expression Typee:R⇔S
Lens term

31

Lens Typing Judgmente : R ⇔ S means

32

Lens Typing Judgmente : R ⇔ S means
Lens e provides 2 functions:e.put from L(R) to L(S)e.get from L(S) to L(R)33

Lens Typing Judgmente : R ⇔ S means
Lens e provides 2 functions:e.put from L(R) to L(S)e.get from L(S) to L(R)Consequences:e.put (e.get s) = se.get (e.put r) = r

e.put and e.get
are inverses
34

Lens Typing Rules
3 sorts of rules

35Lens Typing Rules
3 sorts of rules
1. Syntax-Directed Rules (concatenation, iteration, …)

36

Lens Typing Rules
3 sorts of rules
1. Syntax-Directed Rules (concatenation, iteration, …)
2. Composition37

Lens Typing Rules
3 sorts of rules
1. Syntax-Directed Rules (concatenation, iteration, …)
2. Composition
3. Type Equivalence38

Lens Typing Rules
3 sorts of rules
1. Syntax-Directed Rules (concatenation, iteration, …)
2. Composition
3. Type Equivalence

39

Example Syntax-Directed Rule

? : R1 . R2 ⇔ S1 . S2

40

Example Syntax-Directed Rule

? : R1 . R2 ⇔ S1 . S2

? : R1 ⇔ S1? : R2 ⇔ S2

41

Example Syntax-Directed Rule

? : R1 . R2 ⇔ S1 . S2

e1 : R1 ⇔ S1e2 : R2 ⇔ S242Example Syntax-Directed Rule? : R1 . R2 ⇔ S1 . S2

e1 : R1 ⇔ S1e2 : R2 ⇔ S243

Example Syntax-Directed Rulee1 . e2 : R1 . R2 ⇔ S1 . S2

e1 : R1 ⇔ S1

e2 : R2 ⇔ S2

44

Example Syntax-Directed Rule? : R* ⇔ S*?:R⇔S

45

Example Syntax-Directed Rulee* : R* ⇔ S*e:R⇔S

46

Syntax-Directed Rule Base Case

?:R⇔R

47

Syntax-Directed Rule Base Case

id(R) : R ⇔ R48

Syntax-Directed Rule Base Case?:s⇔t49

Syntax-Directed Rule Base Case

const(s,t) : s ⇔ t

50

Lens Typing Rules
3 sorts of rules
1. Syntax-Directed Rules (concatenation, iteration, …)
2. Composition
3. Type Equivalence51Composition?:R⇔T?:R⇔S?:S⇔T

52

Composition

e1 ; e2 : R ⇔ T

e1 : R ⇔ S

e2 : S ⇔ T

53

Composition

e1 ; e2 : R ⇔ T

e1 : R ⇔ S

e2 : S ⇔ T

54

Composition Inadmissibility
ABCD

perm1

CABD

perm2

CADB

let l= Id([A-Z])
in
let perm1 = ((l . l) ~ l) . l in
let perm2 = l . l . (l ~ l)inperm1 ; perm255

Solution:
Use Alternative Language
DNF Lenses

56Solution:
Use Alternative Language
DNF Lenses
No composition operator

57

Lens Typing Rules
3 sorts of rules
1. Syntax-Directed Rules (concatenation, iteration, …)
2. Composition
3. Type Equivalence58Type Equivalencel:R⇔S
R ≡s R’S ≡s S’l : R’ ⇔ S’59

Example Type Equivalence Rule

? : R.(S | T) ⇔ R.S | R.T

60

Example Type Equivalence Rule

? : R.(S | T) ⇔ R.S | R.T

61

Example Type Equivalence Rule

? : R.(S | T) ⇔ R.S | R.T? : R <=> X? : (S | T) <=> X

62

Example Type Equivalence Rule

? : R.(S | T) ⇔ R.S | R.T

63

Example Type Equivalence Rule

? : R.(S | T) ⇔ R.S | R.T? : X <=> R.S? : X <=> R.T

64

Example Type Equivalence Rule

? : R.(S | T) ⇔ R.S | R.T

65

Example Type Equivalence Rule

? : R.(S | T) ⇔ R.S | R.T? : R.S | R.T ⇔ R.S | R.T

66

Example Type Equivalence Rule

? : R.(S | T) ⇔ R.S | R.T? : R.S | R.T ⇔ R.S | R.T
Search through equivalent regular expression pairs

67

Example Type Equivalence Rule

? : R.(S | T) ⇔ R.S | R.T? : R.S | R.T ⇔ R.S | R.T
Search through equivalent regular expression pairs

68Solution:
Use Alternative Language
DNF Regular Expressions

69

Solution:
Use Alternative Language
DNF Regular Expressions•

Pseudo-canonical form

70

Solution:
Use Alternative Language
Disjunctions
Concatenations

DNF Regular Expressions•

Pseudo-canonical form

71

Iterations, Variables,and Strings

Solution:
Use Alternative Language
Disjunctions
Concatenations

DNF Regular Expressions•Pseudo-canonical form“a” . (“b” | “c”)

Iterations, Variables,and Strings(“a”.“b”) | (“a”.“c”)
72

Solution:
Use Alternative Language
Disjunctions
Concatenations

DNF Regular Expressions

Iterations, Variables,and Strings
DNF Lenses are actually typed between DNF regularexpression pairs•

Pseudo-canonical form“a” . (“b” | “c”)(“a”.“b”) | (“a”.“c”)
73

Example Type Equivalence Rule

R* = “” | RR*
R* = “” | R*R

74

Example Type Equivalence Rule
? : R* ⇔ “” | (R.R*)

R* = “” | RR*
R* = “” | R*R? : “” | (R.R*) ⇔ “” | (R.R*)

75

Example Type Equivalence Rule
? : R* ⇔ “” | (R.R*)

R* = “” | RR*
R* = “” | R*R? : “” | (R.R*) ⇔ “” | (R.R*)

NOT Syntactically Equal in DNF Form!
76

DNF Lens Typing Judgement(s)DNF Lens Typing

dl : DR ⇔ DS
Rewriteless DNF Lens Typing~

dl : DR ⇔ DS
77

DNF Lens Typing Judgement(s)DNF Lens Typing

Addresses
Rewrites

dl : DR ⇔ DS
Rewriteless DNF Lens Typing~dl : DR ⇔ DS
78

Addresses
Syntax-DirectedRules

We have a complete searchalgorithm for DNF lenses…
We can convert DNF lenses into
bijective lenses…

Is this a complete search
procedure for bijective lenses?
79Completeness Theorem

For all

l:R⇔S

80

Completeness Theorem

For all

There exists

l:R⇔Sdl : DR ⇔ DS
Where DR and DS
are R and S in DNF
form

81

Completeness Theorem

For all

There exists

Such thatl:R⇔Sdl : DR ⇔ DS[[l]] = [[dl]]Where DR and DS
are R and S in DNFform82

By Induction over the derivationofl :…….
R⇔S

83

Whole Bunch of Cases• Syntax-Directed Rules• Conjunction• Disjunction• …
• Composition• Type Equivalence84Whole Bunch of Cases• Syntax-Directed Rules• Conjunction• Disjunction• …
• Composition• Type Equivalence85Case: Type Equivalence86Case: Type Equivalence

By induction assumption there exists dl, DR1, DS1, such thatdl : DR1 ⇔ DS1
With equivalent semantics to l87

Case: Type Equivalence

By induction assumption there exists dl, DR1, DS1, such thatdl : DR1 ⇔ DS1
With equivalent semantics to l88

Case: Type Equivalence89Case: Type Equivalence

90Case: Type EquivalenceR ≡s R’ ⇒ DR ≡ DR’→91

Case: Type EquivalenceR ≡s R’ ⇒ DR ≡ DR’→

DR1 ≡ DR1’DR2 ≡ DR2’→→

92

Case: Type Equivalence• Prove → satisfies thediamond property• This implies the existence ofsuch a DR3 and DS393

Case: Type EquivalenceaGO'5䋽'6

• Need dl2 equivalent to dl• Need DR3 →* DR4 and

DS3 →* DS4



'5

'6


'5¶





aGO'5䋽'6
“Looks” a lot like confluence!
'5
94



'6¶

'6

Let’s abstract this problemaGO'5䋽'6




'5

'6


'5¶







aGO'5䋽'6

'5

'6¶

'6

95

Let’s abstract this problem
5 VW

aGO'5䋽'6




'5






a
GO'5䋽'6

'5

W



'6¶


'6



V

'6


'5¶



96

5 VWLet’s abstract this problem
5 VW

aGO'5䋽'6




'5

'5¶


V

'6

aGO'5䋽'6







W



'6¶

5 VW


~R(DR,DS) if there exists a lens dl’ such that dl’ : DR ⇔ DS, and dl is equivalent to dl’'5
'6
97

R-Confluence
5 VW
If R(s1,t1) and s1 →* s2 and t1 →* t2
Then there exists s3 and t3 such that- s2 →* s3- t2 →* t3- R(s3,t3)

V

W



5 VW

98



Sufficient Condition?
If → is confluent, and (R,→*) is bisimilar,Then → is R-confluent

5 VW




V

W



5 VW

99

Sufficient Condition?
If → is confluent, and (R,→*) is bisimilar,
Then → is R-confluent(R,→*) is bisimilar if, for all s,t where R(s,t)
If s →* s’, then there exists t’ such thatt →* t’ and R(s’,t’)
If t →* t’, then there exists s’ such thats →* s’ and R(s’,t’)…

R(s’ , t’)
100



V

W

5 VW

R(s , t)…

5 VW

Sufficient Condition?
If → is confluent, and (R,→*) is bisimilar,
Then → is R-confluent(R,→*) is bisimilar if, for all s,t where R(s,t)
If s →* s’, then there exists t’ such thatt →* t’ and R(s’,t’)
If t →* t’, then there exists s’ such thats →* s’ and R(s’,t’)…

R(s’ , t’)
101



VW



5 VW

R(s , t)…

5 VW

Sufficient Condition?
If → is confluent, and (R,→*) is bisimilar,
Then → is R-confluent(R,→*) is bisimilar if, for all s,t where R(s,t)
If s →* s’, then there exists t’ such thatt →* t’ and R(s’,t’)
If t →* t’, then there exists s’ such thats →* s’ and R(s’,t’)…

R(s’ , t’)
102



VW



5 VW

R(s , t)…

5 VW

Sufficient Condition?
If → is confluent, and (R,→*) is bisimilar,
Then → is R-confluent(R,→*) is bisimilar if, for all s,t where R(s,t)
If s →* s’, then there exists t’ such thatt →* t’ and R(s’,t’)
If t →* t’, then there exists s’ such thats →* s’ and R(s’,t’)…

R(s’ , t’)
103



V

W

5 VW

R(s , t)…

5 VW

Sufficiency Proof
If → is confluent, and (R,→*) is bisimilar,Then → is R-confluent

5 VW

By induction on the length of the reduction of s1 →* s2V

W



5 VW

104



Sufficiency Proof Base CaseR(s , t)…

…

R(s’ , t’)105Sufficiency Proof Base CaseR(s , t)…

…

R(s’ , t’)106Sufficiency Proof Inductive Step

107

Sufficiency Proof Inductive Step

108

Sufficiency Proof Inductive Step

109

Sufficiency Proof Inductive Step110

Case: Type Equivalence111Case: Type EquivalenceaGO'5䋽'6



'5

'6'5¶





aGO'5䋽'6

'5

112



'6¶

'6

Case: Type EquivalenceR(DR,DS) if there exists a lens dl’ such that dl’ : DR ⇔ DS, and dl is equivalent to dl’aGO '5 䋽'6










'5

'6


'5¶





a
GO'5䋽'6

'5

113



'6¶

'6

Case: Type EquivalenceR(DR,DS) if there exists a lens dl’ such that dl’ : DR ⇔ DS, and dl is equivalent to dl’aGO'5䋽'6
We prove → is confluent, and (R,→*) is bisimilar

'5

'6


'5¶





aGO'5䋽'6

'5

114



'6¶

'6

Related Notions
Confluence Modulo Equivalence

5 VW




VW



5 VW

115[Huet 1980]

Related Notions
Confluence Modulo Equivalence

Confluence

116[Huet 1980]

Related Notions
Confluence Modulo Equivalence

Confluence
Bisimilarity

117[Huet 1980]

Related Notions
Bisimilarity

118

Related Notions
Bisimilarity
Common in state transition systems

119

Related Notions
Bisimilarity
Common in state transition systems
Related to commuting rewrites

120[Toyama 1988]

Related Notions
Bisimilarity
Common in state transition systems
Related to commuting rewrites
R(s , t)…

…

R(s’ , t’)121[Toyama 1988]

Related Notions
Bisimilarity
Common in state transition systems
Related to commuting rewrites
sR

…

R

…

s’R

…

Rt

R(s , t)

…

…

t’

…

R(s’ , t’)122[Toyama 1988]

Conclusions
We can synthesize lenses, by synthesizing in an alternative form
This alternative form is equivalent
Proof requires a confluence-like property, R-confluence
Confluence + Bisimilarity with R

123

R-confluence