Hypernet semantics and robust observational equivalence

(1)

Hypernet semantics and

robust observational equivalence

Koko Muroya

(RIMS, Kyoto University)

joint work with

(2)

Overview

1. Motivation: robustness of observational equivalence

2. Hypernet semantics

3. Locality & step-wise reasoning

4. Discussion: complication of simulation notion

(3)

Overview

(4)

Observational equivalence on program fragments

“Do two program fragments behave the same?”

“Is it safe to replace a program fragment with another?”

let x = 100 in let y = 50 in y + y

(5)

Observational equivalence on program fragments

let x = 100 in let y = 50 in y + y

(6)

Observational equivalence on program fragments

let x = 100 in let y = 50 in y + y

let y = 50 in y + y

(7)

Observational equivalence on program fragments

let x = 100 in let y = 50 in y + y

let y = 50 in

y + y 50 + 50

(8)

Observational equivalence on program fragments

let x = 100 in let y = 50 in y + y

let y = 50 in

y + y 50 + 50

let x = 100 in let y = 50 in y + y

let x = 100 in

50 + 50 50 + 50

(9)

Observational equivalence on program fragments

let x = 100 in let y = 50 in y + y

let y = 50 in

y + y 50 + 50

let x = 100 in let y = 50 in y + y

let x = 100 in

50 + 50 50 + 50

? ?

?

(10)

Observational equivalence on program fragments

If YES (“Two program fragments are observationally equal.”):

• justification of compiler optimisation

• program verification

let x = 100 in let y = 50 in y + y

let y = 50 in

y + y 50 + 50

let x = 100 in let y = 50 in y + y

let x = 100 in

50 + 50 50 + 50

? ?

?

(11)

Observational equivalence on program fragments

(12)

Observational equivalence on program fragments

“What program fragments behave the same?”

the beta-law

(λx .M) N ≃ M[x := N] a parametricity law

𝚕𝚎𝚝 a = 𝚛𝚎𝚏 1 𝚒𝚗 λx . (a := 2; !a) ≃ λx.2

(13)

Robustness of observational equivalence

“When do program fragments behave the same?”

Does the beta-law always hold?

the beta-law

(λx .M) N ≃ M[x := N]

(14)

Robustness of observational equivalence

No, it’s violated if program contexts use OCaml’s Gc module:

the beta-law

(λx .M) N ≃ M[x := N]

(λx.0) 100 ≄ 0

for memory management

(15)

Robustness of observational equivalence

No, it’s violated if program contexts use OCaml’s Gc module:

the beta-law

(λx .M) N ≃ M[x := N]

(λx.0) 100 ≄ 0

for memory

(16)

Robustness of observational equivalence

“What fragments, in which contexts, behave the same?”

(17)

Robustness of observational equivalence

… in the presence of (arbitrary) language features:

pure vs. effectful (e.g. vs. ) encoded vs. native (e.g. vs. ) extrinsics (e.g. )

50 + 50 ref 1

State ref

Gc.stat

(18)

Robustness of observational equivalence

… in the presence of (arbitrary) language features

Our (big) goal:

analysing robustness/fragility of observational equivalence, using a general framework

(19)

Robustness of observational equivalence

… in the presence of (arbitrary) language features

Our result:

analysing robustness/fragility of observational equivalence, using a graphical framework

• hypernet semantics: a graphical abstract machine

(20)

Overview

(21)

Hypernet semantics

● program execution by a graphical abstract machine

● programs as

certain hierarchical hypergraphs (“hypernets”)

● execution as

step-by-step strategical update of hypernets

(22)

Programs, graphically as hypernets

Idea: abstracting away variable names, and more…

program hypernet (hierarchical hypergraph)

(1 + 2) * 3

1 2 3

+

*

(23)

Programs, graphically as hypernets

(1 + 2) * 3

1 2 3

+

*

nodes

(24)

Programs, graphically as hypernets

(1 + 2) * 3

1 2 3

+

*

hyperedges

(25)

Programs, graphically as hypernets

(x + y) * z (i + j) * k

+

*

(26)

Programs, graphically as hypernets

(x + y) * z (i + j) * k

+

*

x y z

(27)

Programs, graphically as hypernets

(x + y) * z (i + j) * k

+

*

i j k

(28)

Programs, graphically as hypernets

x + x

+

(29)

Programs, graphically as hypernets

x + x

+

sharing

(30)

Programs, graphically as hypernets

if x > 0 then 3 else 4 + 5

0 5

>

if

+ 4 3

(31)

Programs, graphically as hypernets

if x > 0 then 3 else 4 + 5

0 5

>

if

+ 4 3

hierarchical hyperedge

(hyperedge labelled with

(32)

Programs, graphically as hypernets

(λx. x + x) 3

3

λ

@ +

(33)

Programs, graphically as hypernets

new a = 1 in a := 2; !a

! :=

2 1

(34)

Programs, graphically as hypernets

new a = 1 in a := 2; !a

! :=

; 2 1

atom

(35)

Programs, graphically as hypernets

new a = 1 in a := 2; !a

:= ! 2 1

atom occurences

(36)

Programs, graphically as hypernets

(37)

Programs, graphically as hypernets

• making blocks of deferred computation explicit

• accommodating atoms (reference names/locations)

(38)

Program execution, graphically

Idea: updating hypernets step-by-step

(39)

Program execution, graphically

1 2 4

+

+ 3

4

3

+

+ 3

1 2

+ 7

3

+

7

10

(40)

Program execution, graphically

+ 3

+

3 3

6

let x = 3 in

x + x 3 + 3

(41)

Program execution, graphically

3

λ

@ +

+ 3

+

3 3

6

(42)

Program execution, graphically

… and strategically, using focus with three modes:

• depth-first redex search

• backtracking

• triggering update of hypernet

?

✓

↯

(43)

Program execution, graphically

Idea: updating hypernets step-by-step … and strategically, using focus

1 2 4

+

+ 3

(44)

Program execution, graphically

1 2 4

+

3 depth-first redex search

?

(45)

Program execution, graphically

1 2 4

+

?

(46)

Program execution, graphically

1 2 4

+

?

(47)

Program execution, graphically

1 2 4

+

+ 3

backtracking

✓

(48)

Program execution, graphically

1 2 4

+

+ 3

?

depth-first redex search

(49)

Program execution, graphically

1 2 4

+

+ 3

✓

backtracking

(50)

Program execution, graphically

1 2 4

+

+ 3

triggering update of hypernet

↯

(51)

Program execution, graphically

4

3

+

+ 3

?

(52)

Program execution, graphically

4

3

+

+ 3

backtracking

✓

(53)

Program execution, graphically

4

3

+

+ 3

?

(54)

Program execution, graphically

4

3

+

+ 3

?

(55)

Program execution, graphically

4

3

+

+ 3

backtracking

✓

(56)

Program execution, graphically

4

3

+

+ 3

?

(57)

Program execution, graphically

4

3

+

+ 3

✓

backtracking

(58)

Program execution, graphically

4

3

+

+ 3

↯

(59)

Program execution, graphically

3

+

7

?

(60)

Program execution, graphically

3

+

7

backtracking

✓

(61)

Program execution, graphically

3

+

7

(62)

Program execution, graphically

10

?

(63)

Program execution, graphically

10

backtracking

(64)

Program execution, graphically

3

λ

@ +

(65)

Program execution, graphically

3

λ

@ +

(66)

Program execution, graphically

3

λ

@ +

?

(67)

Program execution, graphically

3

λ

@ +

backtracking

✓

(68)

Program execution, graphically

3

λ

@ +

?

(69)

Program execution, graphically

3

λ

@ +

✓ backtracking

(70)

Program execution, graphically

3

λ

@ +

↯

(71)

Program execution, graphically

3 +

(72)

Program execution, graphically

3 +

?

(73)

Program execution, graphically

3 +

↯

(74)

Program execution, graphically

3

+

?

(75)

Program execution, graphically

3

+ 3

backtracking

✓

(76)

Program execution, graphically

3

+ 3

?

(77)

Program execution, graphically

3

+ 3

✓

backtracking

(78)

Program execution, graphically

3

+ 3

↯

(79)

Program execution, graphically

6

?

(80)

Program execution, graphically

6

backtracking

✓

(81)

Hypernet semantics

● programs as

● execution as

(82)

Hypernet semantics

● programs as

● execution as

● state = hypernet with focus

● transition = move of focus, or update of hypernet

? ✓ ↯

(83)

Overview

(84)

Proof of observational equivalence, using locality

(85)

Proof of observational equivalence, using locality

“Do two sub-graphs behave the same in hypernet semantics?”

(86)

Proof of observational equivalence, using locality

★ Sub-graphs can represent parts of a program that are not necessarily well-formed,

e.g. parts relevant to a certain reference:

… new a = 1 in … (λx. a := 2; !a) … (λx. a := 2; !a) …

(87)

Proof of observational equivalence, using locality

… new a = 1 in … (λx. a := 2; !a) … (λx. a := 2; !a) …

(88)

Proof of observational equivalence, using locality

… new a = 1 in … (λx. a := 2; !a) … (λx. a := 2; !a) …

Idea of locality:

analysing behaviour of program fragments,

(89)

Proof of observational equivalence, using locality

Claim: “Behaviour of a sub-graph G can be matched by behaviour of a sub-graph H.”

(90)

Proof of observational equivalence, using locality

For any context C, if

then

P

✓

C

G⋯ G^⋯

G⋯

?

C

⋯H ^⋯H

⋯H Q

⋯

(91)

Proof of observational equivalence, using locality

Proof idea (simplified):

1. take contextual closure R of (G,H)

2. prove that the contextual closure R is a simulation

(92)

Proof of observational equivalence, using locality

R C

G⋯ G^⋯

G⋯

f

C

H⋯ ^⋯H

⋯H

f

(93)

Proof of observational equivalence, using locality

R is closed under contexts, by definition

R C

G⋯ G^⋯

G⋯

f

C

H⋯ ^⋯H

⋯H

f

(94)

Proof of observational equivalence, using locality

R C

G⋯ G^⋯

G⋯

f

C ⋯ ^⋯H

P

f’

(95)

Proof of observational equivalence, using locality

P

f’

R C

G⋯ G^⋯

G⋯

f

⋯

(96)

Proof of observational equivalence, using locality

C

G⋯ G^⋯

G⋯

f

C’

G⋯

G⋯ ^f’ G^⋯ G⋯

C’ ⋯ ^f’ ^⋯H ⋯

R R

C ⋯ ^⋯H

(97)

Proof of observational equivalence, using locality

C

G⋯ G^⋯

G⋯

f

C’

G⋯

G⋯ ^f’ G^⋯ G⋯

R R

⋯

Idea of locality:

(98)

Proof of observational equivalence, using locality

2. prove that the contextual closure R is a simulation … by case analysis of transition

C

G⋯ G^⋯

G⋯

f

C’

G⋯

G⋯ ^f’ G^⋯ G⋯

C’ ⋯ ^f’ ^⋯H ⋯

R R

C ⋯ ^⋯H Idea of locality:

tracing sub-graphs during transition, move, or trigger update

(99)

Proof of observational equivalence, using locality

2. prove that the contextual closure R is a simulation Case (1) move of focus or inside context

R C

G⋯ G^⋯

G⋯

f

⋯

? ✓

(100)

Proof of observational equivalence, using locality

R C

G⋯ G^⋯

G⋯

f

C ⋯ ^⋯H

? ✓

C

G⋯ G^⋯

G⋯

f’

(101)

Proof of observational equivalence, using locality

R C

G⋯ G^⋯

G⋯

f

⋯

? ✓

C

G⋯ G^⋯

G⋯

f’

R

⋯

(102)

Proof of observational equivalence, using locality

2. prove that the contextual closure R is a simulation Case (2) move of focus or , entering G^? ^✓

R C

G⋯ G^⋯

G⋯

f

C ⋯ ^⋯H

(103)

Proof of observational equivalence, using locality

2. prove that the contextual closure R is a simulation Case (2) move of focus or , entering G

R C

G⋯ G^⋯

G⋯

f

⋯

? ✓

C

G⋯ G^⋯

G⋯

f’

(104)

Proof of observational equivalence, using locality

2. prove that the contextual closure R is a simulation Case (2) move of focus or , entering G

R C

G⋯ G^⋯

G⋯

f

C ⋯ ^⋯H

? ✓

C

G⋯ G^⋯

G⋯

f’

sound condition of “safety(G,H) identified:

(105)

Proof of observational equivalence, using locality

2. prove that the contextual closure R is a simulation Case (3) update of hypernet

R C

G⋯ G^⋯

G⋯

↯

⋯

P

?

(106)

Proof of observational equivalence, using locality

R C

G⋯ G^⋯

G⋯

C ⋯ ^⋯H

↯

P

?

(107)

Proof of observational equivalence, using locality

R C

G⋯ G^⋯

G⋯

⋯

↯

P

?

sound condition of (G,H)

(108)

Proof of observational equivalence, using locality

2. prove that the contextual closure R is a simulation by case analysis

(109)

Proof of observational equivalence, using locality

(110)

Overview

(111)

Complication of simulation notion

Characterisation Theorem

Robust and safe template induce observational equivalences.

(for deterministic & “reasonable” languages)

(112)

Characterisation Theorem

Robust and safe template induce observational equivalences.

(for deterministic & “reasonable” languages)

Complication of simulation notion

Observation:

(113)

Complication of simulation notion

• The standard simulation suffices for GC:

(114)

Complication of simulation notion

• The standard simulation suffices for GC:

C

G G

f G

C’

G ^f’ G G G

C’ ^f’

R R

C

(115)

Complication of simulation notion

• A weak simulation is desired for some arithmetic laws:

(116)

Complication of simulation notion

1 2

+ +

3

1

R

?

2 3

1 +

+

1 2

+

+ 3

?

(117)

Complication of simulation notion

1 2

+ +

3

1

R

?

2 3

1 +

3

+ 3

1 5

?

1 2

+

+ 3

?

6

✓

6

R

(118)

Complication of simulation notion

• A weak simulation is desired:

f P

f Q R

1

(119)

Complication of simulation notion

f P

f Q R

f’ P’

f’ Q’

R

1

m n

(120)

Complication of simulation notion

f P

f Q R

f’ P’

f’ Q’

R

1

m n

(121)

Complication of simulation notion

• A weak simulation up to observational equivalence is desired, to identify different ways of sharing:

1 1 1 1

(122)

Complication of simulation notion

• A weak simulation up to observational equivalence is desired, to identify different ways of sharing:

working on graphs modulo structural equivalence using up-to technique with structural equivalence

1 1 1 1

(123)

Complication of simulation notion

• A weak simulation up to observational equivalence is desired:

f P

f Q R

1

(124)

Complication of simulation notion

f P

f Q R

1 _f’ P’

f’ Q’

m n

(125)

Complication of simulation notion

f P

f Q R

1 _f’ P’

f’ Q’

m n

R

f’ P’

f’ Q’

R

≃

R

≃

(126)

Complication of simulation notion

f P

f Q R

f’ P’

f’ Q’

R

1

m

n _f’ P’

f’ Q’

R

≃

R

≃

(127)

Complication of simulation notion

f P

f Q R

f’ P’

f’ Q’

R

1

m

n _f’ P’

f’ Q’

R

≃

R

≃

1+n ≥ m

non- expanding

(128)

Overview

(129)

Conclusion

● a (general) framework for analysing and proving robustness of observational equivalence

● current key limitation: determinism

• hypernet semantics: a graphical abstract machine

• local & step-wise reasoning to prove observational equivalence, with the concept of robustness

(130)

Future directions

● complication of simulation notion

● What causes complication of simulation notion?

● How can this complication be justified?

● Are there relevant simulation notions?

(131)

Future directions

● Sand’s improvement theory

(incorporating cost reduction in observational equivalence)

● The number of steps can already be dealt with, by the quantitative restrictions on the weak up-to simulation.