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)

LOLA(Oxford),7 July
2018
Muroya2018(U. B’ham.
& RIMS,KyotoU.)

Call-by-value beta-law

golden standard of (functional) program equivalence andcompiler optimisation“A function can be applied to a value before evaluation
without changing the outcome”

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

Call-by-value beta-law

golden standard of (functional) program equivalence andcompiler optimisation… respected by most intrinsic/extrinsic language extensions

3

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

Call-by-value beta-law

basic operations(nat, int, float, ...)
golden standard of (functional) program equivalence andcompiler optimisation… respected by most intrinsic/extrinsic language extensions

4

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

Call-by-value beta-law

algebraic
data structures
golden standard of (functional) program equivalence andcompiler optimisation… respected by most intrinsic/extrinsic language extensions

5

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

Call-by-value beta-law

recursion
golden standard of (functional) program equivalence andcompiler optimisation… respected by most intrinsic/extrinsic language extensions

6

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

Call-by-value beta-law

conditional
statement
golden standard of (functional) program equivalence andcompiler optimisation… respected by most intrinsic/extrinsic language extensions

7

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

Call-by-value beta-law

algebraic effects& handlers
golden standard of (functional) program equivalence andcompiler optimisation… respected by most intrinsic/extrinsic language extensions

8

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

Call-by-value beta-law

control operators
golden standard of (functional) program equivalence andcompiler optimisation… respected by most intrinsic/extrinsic language extensions

9

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

Call-by-value beta-law

golden standard of (functional) program equivalence andcompiler optimisation… respected by most intrinsic/extrinsic language extensions
justification by (operational) semantics, but how?
10

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

Call-by-value beta-law

golden standard of (functional) program equivalence andcompiler optimisation… respected by most intrinsic/extrinsic language extensions
justification by (operational) semantics, but how?
11

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

Question
Given an extension of untyped λ-calculus,
what semantic property of the extension
validates the call-by-value beta-law?
12

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

Question
Given an extension of untyped λ-calculus,
what operational-semantic property of the extension
validates the call-by-value beta-law?
13

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

Question
Given an extension of untyped λ-calculus,
what operational-semantic property of the extension
validates the call-by-value beta-law?

Answer?

14

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

Question
Given an extension of untyped λ-calculus,
what operational-semantic property of the extension
validates the call-by-value beta-law?

Answer?
A formal answer is yet to be stated…
But a graph-rewriting perspective provides:● a useful & robust method● key observations
15

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

Methodology
Given an operational semantics of an extended λ-calculus:
closedterm

basic
constant

define the contextual equivalence by:prove the beta-law:and observe some sufficient condition.
16

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

Methodology
Given an operational semantics of an extended λ-calculus:
closedterm

basic
constantdefine the contextual equivalence by:prove the beta-law:and observe some sufficient condition.
17

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

Which operational semantics?
● easy to extend (esp. by nondeterminism, observables)● easy to prove a contextual equivalence18

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

Which operational semantics?
● easy to extend (esp. by nondeterminism, observables)● easy to prove a contextual equivalencesmall-step reduction

19

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

Which operational semantics?
● easy to extend (esp. by nondeterminism, observables)● easy to prove a contextual equivalencesmall-step reduction… obscures a sub-term of interest :-(redex searching(i.e. decomposition into evaluation context & redex)
obscures `t`
20

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

Which operational semantics?
● easy to extend (esp. by nondeterminism, observables)● easy to prove a contextual equivalencesmall-step “token-guided” graph-rewriting

closedterm

basic
constant

21

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

Which operational semantics?
● easy to extend (esp. by nondeterminism, observables)● easy to prove a contextual equivalencesmall-step “token-guided” graph-rewriting

closedterm

graph representation
with unique open edge

22

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

Which operational semantics?
● easy to extend (esp. by nondeterminism, observables)● easy to prove a contextual equivalencesmall-step “token-guided” graph-rewriting

closedterm

distinguishededge/node as“token”

graph representation
with unique open edge

23

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

Which operational semantics?
● easy to extend (esp. by nondeterminism, observables)● easy to prove a contextual equivalencesmall-step “token-guided” graph-rewriting● redex searching (moving the token)● rewriting (replacing a sub-graph)24

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

Which operational semantics?
● easy to extend (esp. by nondeterminism, observables)● easy to prove a contextual equivalencesmall-step “token-guided” graph-rewritinggarbage● redex searching (moving the token)● rewriting (replacing a sub-graph)25

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

Which operational semantics?
● easy to extend (esp. by nondeterminism, observables)● easy to prove a contextual equivalencesmall-step “token-guided” graph-rewriting… keeps a sub-term of interest traceable :-)26

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

Which operational semantics?
● easy to extend (esp. by nondeterminism, observables)● easy to prove a contextual equivalencesmall-step “token-guided” graph-rewriting● visible interaction between the token

and a sub-graph○ redex searching○ rewriting
vsstep-wise reasoning to prove a contextual equivalence
27

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

Methodology
Given operational semantics of an extended λ-calculus:
closedterm

define the contextual equivalence by:same basic
constants

prove the beta-law:and observe some sufficient condition.
28

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

Case study: linear λ-calculus + “linear” recursionGiven operational semantics:
closedterm

define the contextual equivalence by:same basic
constants

prove the beta-law:and observe some sufficient condition.
29

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

Case study: linear λ-calculus + “linear” recursion
Given operational semantics:
closedterm

basic
constant

linearvariable“linear”
recursion30

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

Case study: linear λ-calculus + “linear” recursion
Given operational semantics:
closedterm

define the contextual equivalence by:same basic
constants

prove the beta-law:and observe some sufficient condition.
31

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

Case study: linear λ-calculus + “linear” recursion… prove the beta-law:same“graph-context”
with matchinginterface
nogarbage
created32

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

Case study: linear λ-calculus + “linear” recursion… prove the beta-law by step-wise reasoning:same“graph-context”
with matchinginterface
nogarbage
created33

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

Case study: linear λ-calculus + “linear” recursion… prove the beta-law by step-wise reasoning:
1. redex searching “within”
graph-context
2. rewriting “in” graph-context
same“graph-context”
with matchinginterface

3. visiting the hole34

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

Case study: linear λ-calculus + “linear” recursion
1. redex searching “within” graph-context (1/6)

searchingstoppedat a value

35

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

Case study: linear λ-calculus + “linear” recursion
1. redex searching “within” graph-context (2/6)

searchingstopped
at a value

36

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

Case study: linear λ-calculus + “linear” recursion
1. redex searching “within” graph-context (3/6)

a redex found37

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

Case study: linear λ-calculus + “linear” recursion
1. redex searching “within” graph-context (4/6)

right-to-leftcall-by-value

38

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

Case study: linear λ-calculus + “linear” recursion
1. redex searching “within” graph-context (5/6)

right-to-leftcall-by-value

39

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

Case study: linear λ-calculus + “linear” recursion
1. redex searching “within” graph-context (6/6)

a redex found40

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

Case study: linear λ-calculus + “linear” recursion
1. redex searching within graph-context (6 cases)

observation: only one node is inspected at each step

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

Case study: linear λ-calculus + “linear” recursion
2. rewriting “in” graph-context (1/3)

call-by-value
beta-reduction

42

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

Case study: linear λ-calculus + “linear” recursion
2. rewriting “in” graph-context (2/3)

call-by-value
beta-reduction

43

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

Case study: linear λ-calculus + “linear” recursion
2. rewriting “in” graph-context

observation: the hole is not involved

44

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

Case study: linear λ-calculus + “linear” recursion
2. rewriting “in” graph-context (3/3)

reduction forrecursion

45

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

Case study: linear λ-calculus + “linear” recursion
2. rewriting “in” graph-context (3/3)`G` contains:● all reachable nodes
reduction forrecursionfrom `μ`● hence,○ none of the hole○ or, all of the hole46

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

Case study: linear λ-calculus + “linear” recursion
2. rewriting “in” graph-context (3/3)

the hole isreduction forrecursion● not involved● or, duplicated as apart of `G`

47

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

Case study: linear λ-calculus + “linear” recursion
2. rewriting “in” graph-context

observation: the hole is not involved, or is duplicated as awholeobservation 2: each rewriting step is “history-free”

48

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

Case study: linear λ-calculus + “linear” recursion
3. visiting the hole (1/1)

49

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

Case study: linear λ-calculus + “linear” recursion
3. visiting the hole (1/1)

1right-to-leftcall-by-value

50

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

Case study: linear λ-calculus + “linear” recursion
3. visiting the hole (1/1)

2searchingstoppedat a value

51

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

Case study: linear λ-calculus + “linear” recursion
3. visiting the hole (1/1)

3right-to-leftcall-by-value

52

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

Case study: linear λ-calculus + “linear” recursion
3. visiting the hole (1/1)

4searching
stoppedat a value

53

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

Case study: linear λ-calculus + “linear” recursion
3. visiting the hole (1/1)

a redex found554

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

Case study: linear λ-calculus + “linear” recursion
3. visiting the hole (1/1)

beta-reduction
655

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

Case study: linear λ-calculus + “linear” recursion
3. visiting the hole (1/1)

6056

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

Case study: linear λ-calculus + “linear” recursion
3. visiting the hole (1 case)observation: the hole is reduced

57

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

Case study: linear λ-calculus + “linear” recursion
Given operational semantics:
closedterm

define the contextual equivalence by:same basic
constants

prove the beta-law by step-wise reasoning:and observe some sufficient condition.
58

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

Case study: linear λ-calculus + “linear” recursion… prove the beta-law by step-wise reasoning,and observe that:
1. redex searching only inspects one node at each step
2. rewriting preserves, duplicates or simply reduces abeta-redex.
3. rewriting is “history-free”.

59

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

Case studies so far… prove the beta-law by step-wise reasoning,and observe that:
1. redex searching only inspects one node at each step
2. rewriting preserves, duplicates or simply reduces abeta-redex.
3. rewriting is “history-free”.
✓ untyped pure λ-calculus✓ basic operations, recursion, if-statement✓ control operators: call/cc, shift/reset● algebraic effects & handlers
60

method needs
to be slightly
adjusted
Muroya (U. B’ham. & RIMS, Kyoto U.)

Question
Given an extension of untyped λ-calculus,
what operational-semantic property of the extension
validates the call-by-value beta-law?

Answer?
A formal answer is yet to be stated…
But a graph-rewriting perspective provides:● a useful & robust method● key observations
61

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