wopro rk ingre
ssA Graph-Rewriting
Perspective of the Beta-Law
Dan R. Ghica
Todd Waugh Ambridge(University of Birmingham)

Koko Muroya(University of Birmingham& RIMS, Kyoto University)

S-REPLSMuroya
9 (Univ.
25 May2018(U. Sussex),
B’ham. & RIMS,Kyoto
U.)Equivalence of programs
denotational
equality
Do t and u denote thesame (mathematical)
object?

syntacticalequation

operational
equivalencet = u

Given any “closing”
context C, doevaluations of C[t]and C[u] yield thesame value?
2Muroya (U. B’ham. & RIMS, Kyoto U.)

Equivalence of programs
denotational
equality
Do t and u denote thesame (mathematical)
object?

syntacticalequationt = ugraphically?

operational
equivalence
Given any “closing”
context C, doevaluations of C[t]and C[u] yield thesame value?

3

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

call-by-value
equational
theory[Plotkin ‘75]

4contextual(operational)
equivalence

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

call-by-value
equational
theory[Plotkin ‘75]

5contextual(operational)
equivalence

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

call-by-value
equational
theory[Plotkin ‘75]

contextual(operational)
equivalence

SECD machine

6

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

call-by-value
equational
theorysoundness[Plotkin ‘75]

contextual(operational)
equivalence

SECDmachine7

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

call-by-value
equational
theorygraphicallycontextual(operational)
equivalencegraph-rewritingmachine8

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

call-by-value
graph-equational
theorygraphically9contextual(operational)
equivalence

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

call-by-value
graph-equational
theorygraphicallycontextual(operational)
equivalence

all and only values are duplicable10

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

call-by-value
graph-equational
theorygraphically11

contextual(operational)
equivalence

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

call-by-value
graph-equational
theorygraphicallycontextual(operational)
equivalencealpha-law: trivial
beta-law: refined(cf. explicit substitution)

12

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

call-by-value
graph-equational
theorygraphicallycontextual(operational)
equivalencealpha-law: trivial
beta-law: refined(cf. explicit substitution)

13

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

call-by-value
graph-equational
theorygraphicallycontextual(operational)
equivalencealpha-law: trivial
beta-law: refined(cf. explicit substitution)

14

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

call-by-value
graph-equational
theorygraphicallycontextual(operational)
equivalencealpha-law: trivial
beta-law: refined(cf. explicit substitution)

15

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

call-by-value
graph-equational
theorygraphicallycontextual(operational)
equivalencealpha-law: trivialbeta-law: refined (cf. explicit substitution)

SECD
machine16

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

call-by-value
graph-equational
theorygraphicallygraph-contextual(operational)
equivalencealpha-law: trivial
beta-law: refined (cf. explicit substitution)

graph-rewritingmachine17

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

call-by-value
graph-equational
theorygraphicallygraph-contextual(operational)
equivalencealpha-law: trivial
beta-law: refined (cf. explicit substitution)dGoI
machine18

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

SECD machine●●●●dGoI machine

stack of closuresenvironment
control stringdump● graph● evaluation control(“token”)● rewriting flag
● computation stack● box stack19

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

SECD machinedGoI machine

20

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

SECD machinedGoI machine

21

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

dGoI-machine transitions

22

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

call-by-value
graph-equational
theorygraphicallygraph-contextual(operational)
equivalencealpha-law: trivial
beta-law: refined (cf. explicit substitution)dGoI
machine23

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

call-by-value
graph-equational
theorysoundnessgraphicallygraph-contextual(operational)
equivalencealpha-law: trivial
beta-law: refined (cf. explicit substitution)dGoI
machine24

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

call-by-value
graph-equational
theorysoundnessgraphicallygraph-contextual(operational)
equivalencealpha-law: trivial
beta-law: refined (cf. explicit substitution)
1. lift an axiom to a binary relation on(dGoI-machine) states

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

call-by-value
graph-equational
theorysoundnessgraphicallygraph-contextual(operational)
equivalence

1. lift an axiom to a binary relation on(dGoI-machine) states

2. show the binary relation is a
“U-simulation”

26

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

call-by-value
graph-equational
theorysoundnessgraphicallygraph-contextual(operational)
equivalence

1. lift an axiom to a binary relation on(dGoI-machine) states

2. show the binary relation is a
“U-simulation”
simulation27

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

call-by-value
graph-equational
theorysoundnessgraphicallygraph-contextual(operational)
equivalence

1. lift an axiom to a binary relation on(dGoI-machine) states

2. show the binary relation is a
“U-simulation”
simulation...until the difference is reduced

28

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

“Until the difference is reduced”

29

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

call-by-value
graph-equational
theorysoundnessgraphicallygraph-contextual(operational)
equivalence

1. lift an axiom to a binary relation on(dGoI-machine) states

2. show the binary relation is a
“U-simulation”
simulation...until the difference is reduced

30

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

call-by-value
graph-equational
theorysoundnessgraphicallygraph-contextual(operational)
equivalence

modular proof using U-simulations
alpha-law: trivial
beta-law: refined (cf. explicit substitution)dGoImachine
31

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

Equivalence of programs
denotational
equality
Do t and u denote thesame (mathematical)
object?

syntacticalequationt = ugraphically?

operational
equivalence
Given any “closing”
context C, doevaluations of C[t]and C[u] yield thesame value?

32

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

Equivalence of programs
denotational
equality
Do t and u denote thesame (mathematical)
object?

syntacticalequationt = ugraphically?

modular proof of soundness
using U-simulations
33

operational
equivalence
Given any “closing”
context C, doevaluations of C[t]and C[u] yield thesame value?
Muroya (U. B’ham. & RIMS, Kyoto U.)

so what?

34

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

Equivalence of programs

syntacticalequationt = ugraphically?

modular proof of soundness
using U-simulations
35

operational
equivalence
Given any “closing”
context C, doevaluations of C[t]and C[u] yield thesame value?
Muroya (U. B’ham. & RIMS, Kyoto U.)

Equivalence of programs

syntacticalequationt = urelated proof techniques:
logical relations
applicative bisimulations
envirionmental bisimulations...

graphically?

modular proof of soundness
using U-simulations
36

operational
equivalence
Given any “closing”
context C, doevaluations of C[t]and C[u] yield thesame value?
Muroya (U. B’ham. & RIMS, Kyoto U.)

Equivalence of programs
semantical criteria of primitive
operations (function constants)
to preserve beta-law?
syntacticalequationt = ugraphically?

modular proof of soundness
using U-simulations
37

operational
equivalence
Given any “closing”
context C, doevaluations of C[t]and C[u] yield thesame value?
Muroya (U. B’ham. & RIMS, Kyoto U.)

Equivalence of programs

cost-sensitive equivalence?
(cf. [Schmidt-Schauss & Dallmeyer,
WPTE ’17]

syntacticalequationt = ugraphically?

modular proof of soundness
using U-simulations
38

operational
equivalence
Given any “closing”
context C, doevaluations of C[t]and C[u] yield thesame value?
Muroya (U. B’ham. & RIMS, Kyoto U.)