Efficient implementation of evaluation strategies
via token-guided graph rewriting
Koko Muroya & Dan R. Ghica (University of Birmingham)
Muroya (U. B’ham.)
TARGET
balancing space cost & time cost of program execution
2
abstract machines for
lambda-calculus
● abstract machines of same end result
○ number of beta-reduction
Motivation: series of non-strict evaluation
Sestoft’s abstract machine
Crégut’s lazy Krivine
abstract machine
Bologna optimal abstract machine Krivine
abstract machine
call by call by Lévy’s optimal
Muroya (U. B’ham.)
● abstract machines of same end result
○ number of beta-reduction
○ time cost
Motivation: series of non-strict evaluation
4
Krivine abstract machine
Sestoft’s abstract machine
Crégut’s lazy Krivine
abstract machine
Bologna optimal abstract machine call by
name
call by need
Accattoli et al.
Lévy’s optimal reduction
● abstract machines of same end result
○ number of beta-reduction
○ time cost
○ space cost
Motivation: series of non-strict evaluation
Krivine abstract machine
Sestoft’s abstract machine
Crégut’s lazy Krivine
abstract machine
Bologna optimal abstract machine call by call by
Accattoli et al.
Lévy’s optimal
Muroya (U. B’ham.)
● abstract machines of same end result
○ space cost
Motivation: series of non-strict evaluation
6
Krivine abstract machine
call by name interaction
abstract machine
[Danos & Regnier ‘99]
● GoI-style token passing
● fixed graph
● term rewriting
● abstract machines of same end result
○ space cost vs time cost… trade-off?
Question
Sestoft’s abstract machine
Crégut’s lazy Krivine
abstract machine
Bologna optimal abstract machine Krivine
abstract machine
call by call by Lévy’s
interaction abstract machine
Muroya (U. B’ham.)
GOAL
unified framework
that can balance space cost & time cost of program execution
8
GOAL
unified framework
that can balance space cost & time cost of program execution
token-guided graph-rewriting abstract machine for lambda-calculus
Muroya (U. B’ham.)
Token-guided graph rewriting
GoI-style token passing,
interleaved with graph rewriting
10
Token-guided graph rewriting
GoI-style token passing,
interleaved with graph rewriting
Muroya (U. B’ham.)
Token-guided graph rewriting
GoI-style token passing,
interleaved with graph rewriting
12
Token-guided graph rewriting
GoI-style token passing,
interleaved with graph rewriting
Muroya (U. B’ham.)
Token-guided graph rewriting
GoI-style token passing,
interleaved with graph rewriting
14
Token-guided graph rewriting
GoI-style token passing,
interleaved with graph rewriting
Muroya (U. B’ham.)
Token-guided graph rewriting
GoI-style token passing,
interleaved with graph rewriting
16
Token-guided graph rewriting
GoI-style token passing,
interleaved with graph rewriting
redex detected
Muroya (U. B’ham.)
Token-guided graph rewriting
GoI-style token passing,
interleaved with graph rewriting
18
(1) trigger rewriting
Token-guided graph rewriting
GoI-style token passing,
interleaved with graph rewriting
redex detected
Muroya (U. B’ham.)
Token-guided graph rewriting
GoI-style token passing,
interleaved with graph rewriting
20
(2) keep passing
Token-guided graph rewriting
GoI-style token passing,
interleaved with graph rewriting
(1) trigger rewriting
(2) keep passing
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
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
Muroya (U. B’ham.)
Non-strict evaluation:
time cost improvement
24
● graph rewriting system with token passing
● interleaving strategy
● translation
of lambda-terms
● proof nets
● passes-only
● “call-by-value”
translation
interaction abstract machine token passing on fixed graph
call by name
call by need
call by
Non-strict evaluation:
time cost improvement
● graph rewriting system with token passing
● interleaving strategy
● translation
of lambda-terms
interaction abstract machine
● proof nets
● passes-only
● !(A ⊸ B)
call-by-name time cost
token passing on fixed graph
Muroya (U. B’ham.)
Non-strict evaluation:
time cost improvement
26
● graph rewriting system with token passing
● interleaving strategy
● translation
of lambda-terms
interaction abstract machine
● proof nets
● passes-only
● !(A ⊸ B)
call-by-name time cost
● proof nets
● rewrites-first
● !(A ⊸ B)
call-by-need time cost [- & Ghica, CSL ‘17]
time cost analysis à la [Accattoli ’16]
token passing on fixed graph
graph rewriting
Non-strict evaluation:
space cost improvement?
● graph rewriting system with token passing
● interleaving strategy
● translation
of lambda-terms
● proof nets
● passes-only
● “call-by-value”
translation
interaction abstract machine token passing on fixed graph
Krivine abstract machine
term rewriting
Muroya (U. B’ham.)
Non-strict evaluation:
space cost improvement?
28
● graph rewriting system with token passing
● interleaving strategy
● translation
of lambda-terms
● proof nets
● passes-only
● “call-by-value”
translation
interaction abstract machine
Krivine abstract machine
● proof nets
● passes-only
● !(A ⊸ B), (!A) ⊸ B call-by-name time cost
token passing on fixed graph
call by name
term rewriting
Non-strict evaluation:
space cost improvement?
● graph rewriting system with token passing
● interleaving strategy
● translation
of lambda-terms
● proof nets
● passes-only
● “call-by-value”
translation
interaction abstract machine
Krivine abstract machine
● proof nets
● passes-only
● !(A ⊸ B), (!A) ⊸ B call-by-name time cost
token passing on fixed graph
● proof nets
● rewrites-first
● (!A) ⊸ B
call-by-name time cost graph rewriting
Muroya (U. B’ham.)
Strict evaluation
30
● graph rewriting system with token passing
● interleaving strategy
● translation
of lambda-terms
● proof nets
● passes-only
● “call-by-value”
translation
● -graphs
● rewrites-first
● !(A ⊸ B)
call-by-value time cost [- & Ghica, WPTE ‘17]
time cost analysis à la [Accattoli ’16]
graph rewriting
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
series of
● non-strict evaluation
● strict evaluation
Muroya (U. B’ham.)
Analyse token-guided graph rewriting
via term rewriting + explicit redex searching [Sinot ‘05]
32
https://cwtsteven.github.io/GoI-Visualiser/CBV-with-CBV-embedding/index.html
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
series of
● non-strict evaluation
● strict evaluation
analysis via term rewriting
