Efficient implementation ofevaluation strategies
via token-guided graph rewriting
Koko Muroya & Dan R. Ghica(University of Birmingham)
WPTE (Oxford),8 Sep.
2017
Muroya(U. B’ham.)TARGETbalancing space cost & time costof program execution
abstract machinesforlambda-calculus
2

Muroya (U. B’ham.)Motivation: series of non-strict evaluation● abstract machines of same end result○ number of beta-reduction

Krivineabstract
machinecall bynameSestoft’s
abstract
machinecall byneed

Crégut’s
lazy Krivine
abstractmachine
3Bologna
optimalabstractmachine
Lévy’s optimal
reduction
Muroya (U. B’ham.)Motivation: series of non-strict evaluation● abstract machines of same end result○ number of beta-reduction○ time cost

Krivineabstract
machinecall bynameSestoft’s
abstract
machinecall byneed

Crégut’s
lazy Krivine
abstract
machine
4Accattoli et al.

Bologna
optimalabstract
machineLévy’s optimalreduction
Muroya (U. B’ham.)Motivation: series of non-strict evaluation● abstract machines of same end result○ number of beta-reduction○ time cost
○ space cost

Krivineabstract
machinecall byname

Sestoft’s
abstract
machinecall byneed

Crégut’s
lazy Krivine
abstractmachine5

Accattoli et al.

Bologna
optimalabstract
machineLévy’s optimal
reduction
Muroya (U. B’ham.)Motivation: series of non-strict evaluation● abstract machines of same end result○ space costinteraction
abstract
machineKrivineabstract
machine[Danos & Regnier ‘99]

● GoI-style token passing● fixed graph● term rewriting

call byname6

Muroya (U. B’ham.)Question● abstract machines of same end result○ space cost vs time cost… trade-off?
interaction
abstractmachineKrivine
abstract
machinecall bynameSestoft’s
abstract
machinecall byneed

Crégut’s
lazy Krivine
abstractmachine
7

Bologna
optimalabstract
machineLévy’soptimal
Muroya (U. B’ham.)GOAL
unified frameworkthat can balance space cost & time costof program execution

8

Muroya (U. B’ham.)GOAL
unified frameworkthat can balance space cost & time costof program execution
token-guided graph-rewriting abstract machine
for lambda-calculus
9

Muroya (U. B’ham.)Token-guided graph rewriting
GoI-style token passing,interleaved with graph rewriting10

Muroya (U. B’ham.)Token-guided graph rewriting
GoI-style token passing,interleaved with graph rewriting

11

Muroya (U. B’ham.)Token-guided graph rewriting
GoI-style token passing,interleaved with graph rewriting

12

Muroya (U. B’ham.)Token-guided graph rewriting
GoI-style token passing,interleaved with graph rewriting

13

Muroya (U. B’ham.)Token-guided graph rewriting
GoI-style token passing,interleaved with graph rewriting

14

Muroya (U. B’ham.)Token-guided graph rewriting
GoI-style token passing,interleaved with graph rewriting

15Muroya (U. B’ham.)Token-guided graph rewriting
GoI-style token passing,interleaved with graph rewriting

16

Muroya (U. B’ham.)Token-guided graph rewriting
GoI-style token passing,interleaved with graph rewriting

redex
detected17

Muroya (U. B’ham.)Token-guided graph rewriting
GoI-style token passing,interleaved with graph rewriting(1) trigger
rewriting18

Muroya (U. B’ham.)Token-guided graph rewriting
GoI-style token passing,interleaved with graph rewriting

redex
detected

19

Muroya (U. B’ham.)Token-guided graph rewriting
GoI-style token passing,interleaved with graph rewriting(2) keeppassing

20

Muroya (U. B’ham.)Token-guided graph rewriting
GoI-style token passing,interleaved with graph rewriting(1) triggerrewriting(2) keeppassing

21

Muroya (U. B’ham.)Token-guided graph rewriting
for lambda-calculus
flexibility, by choices of:● graph rewriting system, with token passing○ proof nets
● interleaving strategy○ trigger rewriting vs. keep passing● translation of lambda-terms○ !(A ⊸ B), (!A) ⊸ B
22

Muroya (U. B’ham.)Token-guided graph rewriting
for lambda-calculus
flexibility, by choices of:● graph rewriting system, with token passing● interleaving strategy● translation of lambda-terms
to…
● balance space cost & time cost

23

Muroya (U. B’ham.)● graph rewriting systemwith token passing● interleaving strategy● translationof lambda-terms

Non-strict evaluation:
time cost improvement

token passing
on fixed graphinteraction
abstract
machinecall bynamecall byneed
24

Muroya (U. B’ham.)● graph rewriting systemwith token passing● interleaving strategy● translationof lambda-terms

Non-strict evaluation:
time cost improvement

token passing
on fixed graph● proof nets
● passes-onlyinteraction
abstract● !(A ⊸ B)
machinecall-by-name time costcall byneed25

Muroya (U. B’ham.)● graph rewriting systemwith token passing● interleaving strategy● translationof lambda-terms

Non-strict evaluation:
time cost improvement

token passing
on fixed graph[- & Ghica, CSL ‘17]

● proof nets

● proof nets

● passes-onlyinteraction
abstract● !(A ⊸ B)
machinecall-by-name time cost

● rewrites-firstgraphrewriting● !(A ⊸ B)
call-by-need time costtime cost analysis
à la [Accattoli ’16]
26

Muroya (U. B’ham.)Non-strict evaluation:
space cost improvement?

token passing
on fixed graph● graph rewriting systemwith token passing● interleaving strategy● translationof lambda-terms

term
rewritinginteraction
abstract
machineKrivineabstract
machinecall by name27

Muroya (U. B’ham.)Non-strict evaluation:
space cost improvement?

token passing
on fixed graph● graph rewriting systemwith token passing● interleaving strategy● translationof lambda-terms

term
rewriting● proof nets
● passes-onlyinteraction
abstract● !(A ⊸ B), (!A) ⊸ B
machinecall-by-name time cost

Krivineabstract
machinecall by name28

Muroya (U. B’ham.)● graph rewriting systemwith token passing● interleaving strategy● translationof lambda-terms

Non-strict evaluation:
space cost improvement?

token passing
on fixed graphgraphrewriting● proof nets

● proof nets

● passes-onlyinteraction
abstract● !(A ⊸ B), (!A) ⊸ B
machinecall-by-name time cost

Krivine● rewrites-first
abstract● (!A) ⊸ Bmachine
call-by-name time costcall by name29

Muroya (U. B’ham.)● graph rewriting systemwith token passing● interleaving strategy● translationof lambda-terms

Strict evaluation[- & Ghica, WPTE ‘17]●-graphs● rewrites-firstgraphrewriting● !(A ⊸ B)
call-by-value time costtime cost analysis
à la [Accattoli ’16]30

Muroya (U. B’ham.)Token-guided graph rewriting
for lambda-calculus
series of● non-strict evaluation● strict evaluation

flexibility, by choices of:● graph rewriting system, with token passing● interleaving strategy● translation of lambda-terms
to…
● balance space cost & time cost31

Muroya (U. B’ham.)Analyse token-guided graph rewriting
via term rewriting + explicit redex searching [Sinot ‘05]

https://cwtsteven.github.io/GoI-Visualiser/CBV-with-CBV-embedding/index.html
32

Muroya (U. B’ham.)Token-guided graph rewriting
for lambda-calculus
series of● non-strict evaluation● strict evaluation

flexibility, by choices of:● graph rewriting system, with token passing● interleaving strategy● translation of lambda-terms
to…
● balance space cost & time cost

33

analysis via
term rewriting

Muroya (U. B’ham.)