Local reasoning for robust
observational equivalence
Koko Muroya(RIMS, Kyoto University& University of Birmingham)

Dan R. Ghica
Todd Waugh Ambridge(University of Birmingham)

LOLA 2019 (Vancouver), 23 June 2019

Local reasoning for robust
observational equivalence
Koko Muroya(RIMS, Kyoto University& University of Birmingham)

Dan R. Ghica
Todd Waugh Ambridge(University of Birmingham)

LOLA 2019 (Vancouver), 23 June 2019

Reasoning about observational equivalence“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

?

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

?

let y = 50 iny + y

let x = 100 in
50 + 50?

?

50 + 50

50 + 50

Muroya (RIMS, Kyoto U. & U. B’ham.)Reasoning about observational equivalence“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

?

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

?

let y = 50 iny + y

let x = 100 in
50 + 50?

?

50 + 50

50 + 50

If YES:• justification of compiler optimisation• program verification

Muroya (RIMS, Kyoto U. & U. B’ham.)Reasoning about observational equivalence“Do two program fragments behave the same?”

Muroya (RIMS, Kyoto U. & U. B’ham.)Reasoning about observational equivalence“Do two program fragments behave the same?”“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

Muroya (RIMS, Kyoto U. & U. B’ham.)Reasoning about observational equivalence“Do two program fragments behave the same?”“When do program fragments behave the same?”the beta-law(λx . M) N ≃ M[x := N ]Does the beta-law always hold?

Muroya (RIMS, Kyoto U. & U. B’ham.)Reasoning about observational equivalence“Do two program fragments behave the same?”“When do program fragments behave the same?”the beta-law(λx . M) N ≃ M[x := N ]Does the beta-law always hold?
No, it’s violated if program contexts use OCaml’s Gc module:(λx.0) 100 ≄ 0

for memory
management

Muroya (RIMS, Kyoto U. & U. B’ham.)Reasoning about observational equivalence“Do two program fragments behave the same?”
What fragments, in which contexts?

Muroya (RIMS, Kyoto U. & U. B’ham.)Reasoning about observational equivalence“Do two program fragments behave the same?”
What fragments, in which contexts?
… in the presence of (arbitrary) language features:

pure vs. effectful (e.g. 50 + 50 vs. ref 1 )encoded vs. native (e.g. State vs.

ref)extrinsics (e.g. Gc.stat )foreign language calls

Muroya (RIMS, Kyoto U. & U. B’ham.)Reasoning about observational equivalence“Do two program fragments behave the same?”
What fragments, in which contexts?
… in the presence of (arbitrary) language features

Analysing robustness/fragility of observational equivalence,with a general framework

Muroya (RIMS, Kyoto U. & U. B’ham.)A general framework
to analyse robustness/fragility of observational equivalence:
1. the Spartan calculus

2. a universal abstract machine

3. locality & equational reasoning

Muroya (RIMS, Kyoto U. & U. B’ham.)1. the Spartan calculus
programmingt, u ::== copying via variables∣ x ∣ 𝚋𝚒𝚗𝚍 x → u 𝚒𝚗 t

+ sharing via atoms/names∣ a ∣ 𝚗𝚎𝚠 a ⊸ u 𝚒𝚗 t

+ thunking∣ x.t+ algebra∣ ϕ(t, …, t; x ⃗ . u, …, x ⃗ . u)

Muroya (RIMS, Kyoto U. & U. B’ham.)1. the Spartan calculus
programming= copying via variablest, u ::=∣ x ∣ 𝚋𝚒𝚗𝚍 x → u 𝚒𝚗 t

reference to(a copy of) computation+ sharing via atoms/names∣ a ∣ 𝚗𝚎𝚠 a ⊸ u 𝚒𝚗 t

location of(shared) computation+ thunking∣ x.t+ algebra∣ ϕ(t, …, t; x ⃗ . u, …, x ⃗ . u)

Muroya (RIMS, Kyoto U. & U. B’ham.)1. the Spartan calculus
programming= copying via variablest, u ::=∣ x ∣ 𝚋𝚒𝚗𝚍 x → u 𝚒𝚗 t

reference to(a copy of) computation+ sharing via atoms/names∣ a ∣ 𝚗𝚎𝚠 a ⊸ u 𝚒𝚗 t

location of(shared) computation+ thunking+ algebra

delaying
computation with boundvariable(s)∣ x.t∣ ϕ(t, …, t; x ⃗ . u, …, x ⃗ . u)

Muroya (RIMS, Kyoto U. & U. B’ham.)1. the Spartan calculus
programming= copying via variablest, u ::=∣ x ∣ 𝚋𝚒𝚗𝚍 x → u 𝚒𝚗 t

reference to(a copy of) computation+ sharing via atoms/names∣ a ∣ 𝚗𝚎𝚠 a ⊸ u 𝚒𝚗 t

location of(shared) computation+ thunking

delaying
computation with boundvariable(s)+ algebra∣ x.t∣ ϕ(t, …, t; x ⃗ . u, …, x ⃗ . u)

language features as(extrinsic) operations
Muroya (RIMS, Kyoto U. & U. B’ham.)1. the Spartan calculus
programmingt, u ::== copying via variables∣ x ∣ 𝚋𝚒𝚗𝚍 x → u 𝚒𝚗 t

+ sharing via atoms/names∣ a ∣ 𝚗𝚎𝚠 a ⊸ u 𝚒𝚗 t

+ thunking∣ x.t+ algebra∣ ϕ(t, …, t; x ⃗ . u, …, x ⃗ . u)
language features as(extrinsic) operations
Muroya (RIMS, Kyoto U. & U. B’ham.)1. the Spartan calculus
programmingt, u ::== copying via variables∣ x ∣ 𝚋𝚒𝚗𝚍 x → u 𝚒𝚗 t

+ sharing via atoms/names∣ a ∣ 𝚗𝚎𝚠 a ⊸ u 𝚒𝚗 t

+ thunking∣ xeager.t
arguments

deferredarguments(thunks)∣ ϕ(t, …, t; x ⃗ . u, …, x ⃗ . u)

+ algebra
language features as(extrinsic) operations

Muroya (RIMS, Kyoto U. & U. B’ham.)1. the Spartan calculus
programming

language features as(extrinsic)
operations= copying
via variables
0,1,2,3,…
𝙿𝙻𝚄𝚂(t, u)

𝙻𝙰𝙼𝙱𝙳𝙰(; x . t)

+ sharing via atoms/names
𝙰𝙿𝙿(t, u)𝙸𝙵(t; u1, u2)+ thunking

𝙻𝙾𝙾𝙺𝚄𝙿(t; x . u)

𝙳𝙴𝚁𝙴𝙵(t)𝙰𝚂𝚂𝙸𝙶𝙽(t, u)+ algebrat, u ::=∣ x ∣ 𝚋𝚒𝚗𝚍 x → u 𝚒𝚗 t

∣ a ∣ 𝚗𝚎𝚠 a ⊸ u 𝚒𝚗 t

∣ xeager.t
arguments

deferredarguments(thunks)∣ ϕ(t, …, t; x ⃗ . u, …, x ⃗ . u)

Muroya (RIMS, Kyoto U. & U. B’ham.)A general framework
to analyse robustness/fragility of observational equivalence:
1. the Spartan calculus
programming = copying + sharing + thunking + algebra
2. a universal abstract machine

3. locality & equational reasoning

Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph

Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraphhypernet(Spartan) term

(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)

1

2

3

+

*

Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraphhypernet(Spartan) term

(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)

nodes
1

2

3

+

*

Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraphhypernet(Spartan) term

(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)

hyperedges
1

2

3

+

*

Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet(1 + 2) × 3
𝚃𝙸𝙼𝙴𝚂(𝙿𝙻𝚄𝚂(1,2),3)“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

(λx . x + x) 3
𝙰𝙿𝙿(𝙻𝙰𝙼𝙱𝙳𝙰(; x . 𝙿𝙻𝚄𝚂(x, x)), 3)

hypernet

×

3

+
λ
@

Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

(λx . x + x) 3
𝙰𝙿𝙿(𝙻𝙰𝙼𝙱𝙳𝙰(; x . 𝙿𝙻𝚄𝚂(x, x)), 3)

hypernetcopying
×

3

+
λ
@

Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

(λx . x + x) 3
𝙰𝙿𝙿(𝙻𝙰𝙼𝙱𝙳𝙰(; x . 𝙿𝙻𝚄𝚂(x, x)), 3)

hypernet×

hyperedge
labelled withhypernet3+
λ@Muroya (RIMS, Kyoto U. & U. B’ham.)(λx . x + x) 3

Muroya (RIMS, Kyoto U. & U. B’ham.)(λx . x + x) 3

“focus”• bring query ? up
• bring answer ✓/↯ down
• trigger rewrite ↯Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraph(Spartan) term

hypernet

𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗 (a := 2; !a)1

𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗
𝚂𝙴𝙲(𝙰𝚂𝚂𝙸𝙶𝙽(a,2); 𝙳𝙴𝚁𝙴𝙵(a))

hyperedge
labelled withhypernet

×
2

I

×

:=

I
;

Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraphhypernet(Spartan) term

1

𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗 (a := 2; !a)
𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗
𝚂𝙴𝙲(𝙰𝚂𝚂𝙸𝙶𝙽(a,2); 𝙳𝙴𝚁𝙴𝙵(a))

sharing

×
2

I

×

:=

I
;

Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraphhypernet(Spartan) term

1

𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗 (a := 2; !a)
𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗
𝚂𝙴𝙲(𝙰𝚂𝚂𝙸𝙶𝙽(a,2); 𝙳𝙴𝚁𝙴𝙵(a))

nameoccurrences

×
2

I

×

:=

I
;

Muroya (RIMS, Kyoto U. & U. B’ham.)2. A universal abstract machine
computation = focussed “hypernet” rewriting• higher-order hypergraph• hierarchical hypergraphprogram

hypernetprogram fragment

sub-hypernet(sub-graph)

program execution

moves of focus(query / answer)&
focussed rewrites
Muroya (RIMS, Kyoto U. & U. B’ham.)A general framework
to analyse robustness/fragility of observational equivalence:
1. the Spartan calculus
programming = copying + sharing + thunking + algebra
2. a universal abstract machine
computation = focussed “hypernet” rewriting
3. locality & equational reasoning

Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning“Do two program fragments behave the same?”

Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning“Do two program fragments behave the same?”“Do two sub-graphs behave the same in focussed rewriting?”

Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning
Locality of graph syntax“Does 𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗 λx . (a := 2; !a) behave the same as λx . 2 ?”Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning
Locality of graph syntax“Does 𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗 λx . (a := 2; !a) behave the same as λx . 2 ?”with linear syntax:⋯ 𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗 ⋯⋯λx . (a := 2; !a) ⋯ λx . (a := 2; !a) ⋯λx . 2⋯

λx . 2⋯

Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning
Locality of graph syntax“Does 𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗 λx . (a := 2; !a) behave the same as λx . 2 ?”with linear syntax: comparison between sub-terms⋯ 𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗 ⋯⋯λx . (a := 2; !a) ⋯ λx . (a := 2; !a) ⋯λx . 2⋯

λx . 2⋯

Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning
Locality of graph syntax“Does 𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗 λx . (a := 2; !a) behave the same as λx . 2 ?”with linear syntax: comparison between sub-terms⋯ 𝚗𝚎𝚠 a ⊸ 1 𝚒𝚗 ⋯⋯λx . (a := 2; !a) ⋯ λx . (a := 2; !a) ⋯λx . 2⋯

λx . 2⋯

with graph syntax: comparison between sub-graphs

Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning“Do two program fragments behave the same?”“Do two sub-graphs behave the same in focussed rewriting?”

Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning
Locality of focussed rewriting“How does a sub-graph behave?”

Case analysis
1. query/answer in context
2. query to the sub-graph
3. answer to the sub-graph
4. focussed rewrite in context
Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning
Locality of focussed rewriting“How does a sub-graph behave?”↑ ?/✓/↯

Case analysis

Case analysis

1. query/answer in context(no interference)

2. query to the sub-graph
3. answer to the sub-graph
4. focussed rewrite in context
Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning
Locality of focussed rewriting“How does a sub-graph behave?”↑?

Case analysis

Case analysis

1. query/answer in context(no interference)

2. query to the sub-graphinterference

3. answer to the sub-graph
4. focussed rewrite in context
Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning
Locality of focussed rewriting↑ ✓/↯“How does a sub-graph behave?”

Case analysis

Case analysis

1. query/answer in context(no interference)

2. query to the sub-graphinterference

3. answer to the sub-graphinterference

4. focussed rewrite in context
Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning
Locality of focussed rewriting“How does a sub-graph behave?”↑↯

Case analysis

Case analysis

1. query/answer in context(no interference)

2. query to the sub-graphinterference

3. answer to the sub-graphinterference

4. focussed rewrite in context

possible interference
Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning“Do two sub-graphs behave the same in focussed rewriting?”

Case analysis

with the sub-graphs:

1. query/answer in context(no interference)

2. query to the sub-graphsinterference

3. answer to the sub-graphsinterference

4. focussed rewrite in context

possible interference

Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning“Do two sub-graphs behave the same in focussed rewriting?”
the sub-graphs are
Case analysis

interfered the same:

1. query/answer in context(always)

2. query to the sub-graphs

if input-safe

3. answer to the sub-graphs

if output-closed

4. focussed rewrite in context

if robust

Characterisation Theorem
Robust templates induce observational equivalences.
Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning“Do two sub-graphs behave the same in focussed rewriting?”
the sub-graphs are
Case analysis

interfered the same:

1. query/answer in context(always)

2. query to the sub-graphs

if input-safe

3. answer to the sub-graphs

if output-closed

4. focussed rewrite in context

if robust

Characterisation Theorem
Robust templates induce observational equivalences.
Muroya (RIMS, Kyoto U. & U. B’ham.)3. Locality & equational reasoning“Do two sub-graphs behave the same in focussed rewriting?”
the sub-graphs are
Case analysis

interfered the same:

1. query/answer in context(always)

2. query to the sub-graphs

if input-safe

3. answer to the sub-graphs

if output-closed

4. focussed rewrite in context

if robust

Characterisation Theorem
Robust templates induce observational equivalences.
Muroya (RIMS, Kyoto U. & U. B’ham.)A general framework
to analyse robustness/fragility of observational equivalence:
1. the Spartan calculus
programming = copying + sharing + thunking + algebra
2. a universal abstract machine
computation = focussed “hypernet” rewriting
3. locality & equational reasoning
Characterisation Theorem
Robust templates induce observational equivalences.

Muroya (RIMS, Kyoto U. & U. B’ham.)Directions● beyond determinism● nondeterminism,probability, I/O● refined notion ofobservational equivalence● concurrency● rewriting with multiple
focusses(cf. multi-token GoI)
● types● weak notion of safety● tooling● https://tnttodda.github.io/
Spartan-Visualiser/● cost analysis● observational
equivalence with cost
improvement(improvement theory)● cost model of focussed
hypernet rewriting(cf. dynamic GoI)
● strengthening mathematics● hypernets = trees +hierarchy + copying +sharing● focussed DPO rewriting● reasoning with graphcontexts

Muroya (RIMS, Kyoto U. & U. B’ham.)