Muroya (U. B’ham. & RIMS, Kyoto U.)
A Graph-Rewriting
Perspective of the Beta-Law
Dan R. Ghica
Todd Waugh Ambridge (University of Birmingham)
S-REPLS 9 (Univ. Sussex), 25 May 2018
Koko Muroya
(University of Birmingham
& RIMS, Kyoto University) work in progress
Equivalence of programs
syntactical equation
operational equivalence denotational
equality
t = u
Do t and u denote the same (mathematical) object?
Given any “closing”
context C, do
evaluations of C[t]
and C[u] yield the
Muroya (U. B’ham. & RIMS, Kyoto U.)
Equivalence of programs
3
syntactical equation
operational equivalence denotational
equality
graphically?
t = u
Do t and u denote the same (mathematical) object?
Given any “closing”
context C, do
evaluations of C[t]
and C[u] yield the same value?
call-by-value equational
theory
contextual (operational)
equivalence [Plotkin ‘75]
Muroya (U. B’ham. & RIMS, Kyoto U.)
call-by-value equational
theory
5
contextual (operational)
equivalence [Plotkin ‘75]
call-by-value equational
theory
contextual (operational)
equivalence [Plotkin ‘75]
SECD machine
Muroya (U. B’ham. & RIMS, Kyoto U.)
7
call-by-value equational
theory
contextual (operational)
equivalence soundness
[Plotkin ‘75]
SECD machine
call-by-value equational
theory
contextual (operational)
equivalence
graph-rewriting
graphically
Muroya (U. B’ham. & RIMS, Kyoto U.)
9
call-by-value graph-equational
theory graphically
contextual (operational)
equivalence
call-by-value graph-equational
theory graphically
contextual (operational)
equivalence
all and only values are duplicable
Muroya (U. B’ham. & RIMS, Kyoto U.)
11
call-by-value graph-equational
theory graphically
contextual (operational)
equivalence
call-by-value graph-equational
theory graphically
contextual (operational)
equivalence
alpha-law: trivial beta-law: refined
(cf. explicit substitution)
Muroya (U. B’ham. & RIMS, Kyoto U.)
13
call-by-value graph-equational
theory graphically
contextual (operational)
equivalence
alpha-law: trivial beta-law: refined
(cf. explicit substitution)
call-by-value graph-equational
theory graphically
contextual (operational)
equivalence
alpha-law: trivial beta-law: refined
(cf. explicit substitution)
Muroya (U. B’ham. & RIMS, Kyoto U.)
15
call-by-value graph-equational
theory graphically
contextual (operational)
equivalence
alpha-law: trivial beta-law: refined
(cf. explicit substitution)
contextual (operational)
equivalence graphically
call-by-value graph-equational
theory
alpha-law: trivial
beta-law: refined (cf. explicit substitution)
SECD
Muroya (U. B’ham. & RIMS, Kyoto U.)
17
call-by-value graph-equational
theory graphically
graph-contextual (operational)
equivalence
alpha-law: trivial
beta-law: refined (cf. explicit substitution)
graph-rewriting machine
call-by-value graph-equational
theory graphically
graph-contextual (operational)
equivalence
alpha-law: trivial
beta-law: refined (cf. explicit substitution)
dGoI
Muroya (U. B’ham. & RIMS, Kyoto U.)
19
SECD machine dGoI machine
● stack of closures
● environment
● control string
● dump
● graph
● evaluation control (“token”)
● rewriting flag
● computation stack
● box stack
SECD machine dGoI machine
Muroya (U. B’ham. & RIMS, Kyoto U.)
21
SECD machine dGoI machine
dGoI-machine transitions
Muroya (U. B’ham. & RIMS, Kyoto U.)
23
call-by-value graph-equational
theory graphically
graph-contextual (operational)
equivalence
alpha-law: trivial
beta-law: refined (cf. explicit substitution)
dGoI machine
call-by-value graph-equational
theory graphically
graph-contextual (operational)
equivalence
alpha-law: trivial
beta-law: refined (cf. explicit substitution)
dGoI
soundness
Muroya (U. B’ham. & RIMS, Kyoto U.)
25
call-by-value graph-equational
theory graphically
graph-contextual (operational)
equivalence soundness
alpha-law: trivial
beta-law: refined (cf. explicit substitution) 1. lift an axiom to a binary relation on
(dGoI-machine) states
call-by-value graph-equational
theory graphically
graph-contextual (operational)
equivalence soundness
1. lift an axiom to a binary relation on (dGoI-machine) states
2. show the binary relation is a
“U-simulation”
Muroya (U. B’ham. & RIMS, Kyoto U.)
27
call-by-value graph-equational
theory graphically
graph-contextual (operational)
equivalence soundness
1. lift an axiom to a binary relation on (dGoI-machine) states
2. show the binary relation is a
“U-simulation”
simulation
call-by-value graph-equational
theory graphically
graph-contextual (operational)
equivalence soundness
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
Muroya (U. B’ham. & RIMS, Kyoto U.)
“Until the difference is reduced”
29
call-by-value graph-equational
theory graphically
graph-contextual (operational)
equivalence soundness
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
Muroya (U. B’ham. & RIMS, Kyoto U.)
31
call-by-value graph-equational
theory graphically
graph-contextual (operational)
equivalence
alpha-law: trivial
beta-law: refined (cf. explicit substitution)
dGoI machine
soundness
modular proof using U-simulations
Equivalence of programs
syntactical equation
operational equivalence denotational
equality
graphically?
t = u
Do t and u denote the same (mathematical) object?
Given any “closing”
context C, do
evaluations of C[t]
and C[u] yield the
Muroya (U. B’ham. & RIMS, Kyoto U.)
Equivalence of programs
33
syntactical equation
operational equivalence denotational
equality
graphically?
t = u
Do t and u denote the same (mathematical) object?
Given any “closing”
context C, do
evaluations of C[t]
and C[u] yield the same value?
modular proof of soundness using U-simulations
so what?
Muroya (U. B’ham. & RIMS, Kyoto U.)
Equivalence of programs
35
syntactical equation
operational equivalence
graphically?
t = u
Given any “closing”
context C, do
evaluations of C[t]
and C[u] yield the same value?
modular proof of soundness using U-simulations
Equivalence of programs
syntactical equation
operational equivalence
graphically?
t = u
Given any “closing”
context C, do
evaluations of C[t]
and C[u] yield the modular proof of soundness
related proof techniques:
logical relations
applicative bisimulations
envirionmental bisimulations...
Muroya (U. B’ham. & RIMS, Kyoto U.)
Equivalence of programs
37
syntactical equation
operational equivalence
graphically?
t = u
Given any “closing”
context C, do
evaluations of C[t]
and C[u] yield the same value?
modular proof of soundness using U-simulations
semantical criteria of primitive operations (function constants) to preserve beta-law?
Equivalence of programs
syntactical equation
operational equivalence
graphically?
t = u
Given any “closing”
context C, do
evaluations of C[t]
and C[u] yield the modular proof of soundness
cost-sensitive equivalence?
(cf. [Schmidt-Schauss & Dallmeyer, WPTE ’17]
