Token-passing semantics
with and without rewriting
Koko Muroya(RIMS, Kyoto University& University of Birmingham)

Steven W. T. Cheung
Dan R. Ghica(University of Birmingham)

CRECOGI meeting
2018(RIMS,(Paris),08 October2018
MuroyaKyoto
U. & U. B’ham.)Token-passing semantics
without rewriting

2Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics without rewriting
execution models, provided by Girard’s GoI,of functional programming● call-by-name λ-calculus [Danos&Regnier ‘99] [Mackie ‘95]
● call-by-value λ-calculus [Fernandez&Mackie ‘02]
● and more: PCF, effects, concurrency...

3

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics without rewriting
execution models, provided by Girard’s GoI,of functional programming● call-by-name λ-calculus [Danos&Regnier ‘99] [Mackie ‘95]
● call-by-value λ-calculus [Fernandez&Mackie ‘02]
(MELL) proof net,
● and more: PCF, effects, concurrency...
λ-graph, ...
programdiagramevaluation

token passing

4

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics without rewriting
programdiagramevaluation

token passing

resulttoken data/position

live demo:
Jamping Abstract Machine for call-by-name λ-calculus [DR99]
https://koko-m.github.io/GoI-Visualiser/

5

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics without rewriting
programλ-graph + !-boxes

evaluation

token passing + jumping

resulttoken data/position

live demo:
Jamping Abstract Machine for call-by-name λ-calculus [DR99]
https://koko-m.github.io/GoI-Visualiser/

6

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics without rewriting
programdiagram

evaluation

token passing

resulttoken data/position

execution models of functional programming● compiler [Mackie ‘95]
● higher-order synthesis [Ghica ‘07]

7

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics
with rewriting

8

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics with rewriting
execution models of functional programming● call-by-name & call-by-value λ-calculus [Sinot ‘05]
● call-by-need & fully lazy λ-calculus [Sinot ‘06]
● call-by-need & call-by-value λ-calculus [−&Ghica ‘17]conventional small-step semantics,
diagramatically (+ more)

9

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics with rewriting
execution models of functional programming● call-by-name & call-by-value λ-calculus [Sinot ‘05]
inspired by● call-by-need & fully lazy λ-calculus [Sinot ‘06]
virtual reduction● call-by-need & call-by-value λ-calculus [−&Ghica‘17][Danos&Regnier‘93]
programdiagramredex searchtoken passing

reduction

diagramrewritingevaluation10

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics with rewriting
programdiagramredex searchtoken passing

reduction

diagramrewritingevaluation

resultdiagramlive demo:
Dynamic GoI Machine for call-by-value λ-calculus [KG17]
https://koko-m.github.io/GoI-Visualiser/
11

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics with rewriting
λ-graph +!-boxes

programredex searchtoken passing

reduction

diagramrewritingevaluation

λ-graph +!-boxes

resultlive demo:

Dynamic GoI Machine for call-by-value λ-calculus [KG17]
https://koko-m.github.io/GoI-Visualiser/
12

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics with rewriting
programdiagramredex searchtoken passing

reduction

diagramrewritingevaluation

resultdiagram

execution models of functional programming● with robustness [S05] [S06]● with time/space efficiency [MG17]
13

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics with rewriting
programdiagramredex searchtoken passing

reduction

diagramrewritingevaluation

resultdiagramwhenever possible
execution models of functional programming● with robustness [S05] [S06]● with time/space efficiency [MG17]
14

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics with rewriting
programdiagramredex searchtoken passing

reduction

diagramrewritingevaluation

resultdiagram

execution models of functional programming selective?
● with robustness [S05] [S06]● with time/space efficiency [MG17]
15

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics
with and without rewriting

16

Muroya (RIMS, Kyoto U. & U. B’ham.)token-passing semantics without rewriting… space efficiency

token-passing semantics with rewriting… time efficiency
selective rewriting
non-trivial space/time balancing?

17

Muroya (RIMS, Kyoto U. & U. B’ham.)token-passing semantics without rewriting… space efficiency

token-passing semantics with rewriting… time efficiency
selective rewriting
non-trivial space/time balancing?

18

anotherperspective
Muroya (RIMS, Kyoto U. & U. B’ham.)token-passing semantics without rewriting… result given by the token

token-passing semantics with rewriting… result given by a diagram
selective rewriting
programming with dual result… given by the token and a diagram?
19Muroya (RIMS, Kyoto U. & U. B’ham.)token-passing semantics without rewriting… result given by the token

token-passing semantics with rewriting… result given by a diagram
selective rewriting
programming with “computation graphs”… result being value with computation graph
20

Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”
valuewith computation graphresult● construction● manipulation

21

Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”
TensorFlow, Google’s machine-learning library

W = tf.Variable(...)
b = tf.Variable(...)
y = W * x_data + b
x_data = ...
y_data = ...
sess = tf.Session()sess.run(init)
sess.run(train)
x_data = ...
sess = tf.Session()sess.run(init)
y_initial_values =sess.run(y)construction
machine-learning modelwith parameters
manipulation
model training(imperative parameter update)value extraction
output prediction

22

Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”
TensorFlow, Google’s machine-learning library

W = tf.Variable(...)
b = tf.Variable(...)
y = W * x_data + b

construction“variables”

x_data = ...
y_data = ...
sess = tf.Session()sess.run(init)
sess.run(train)

Wxb*

x_data = ...
sess = tf.Session()sess.run(init)
y_initial_values =sess.run(y)+y23Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”
TensorFlow, Google’s machine-learning library

W = tf.Variable(...)
b = tf.Variable(...)
y = W * x_data + b

construction

x_data = ...
y_data = ...
sess = tf.Session()sess.run(init)
sess.run(train)“variables”“parameters”
Wxb*

x_data = ...
sess = tf.Session()sess.run(init)
y_initial_values =sess.run(y)+y24Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”
TensorFlow, Google’s machine-learning library

W = tf.Variable(...)
b = tf.Variable(...)
y = W * x_data + b

manipulation

x_data = ...
y_data = ...
sess = tf.Session()sess.run(init)
sess.run(train)in-place (imperative)
parameter update
W’xb’

*

x_data = ...
sess = tf.Session()sess.run(init)
y_initial_values =sess.run(y)+y25Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”
TensorFlow, Google’s machine-learning library

W = tf.Variable(...)
b = tf.Variable(...)
y = W * x_data + b

manipulation
output prediction
x_datax_data = ...
y_data = ...
sess = tf.Session()sess.run(init)
sess.run(train)

W’xb’

*

x_data = ...
sess = tf.Session()sess.run(init)
y_initial_values =sess.run(y)+y26Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”
Self-Adjusting Computation [Acar ‘05]

“spreadsheet”(Incremental, an OCaml library)
let x = Inc.Var.create 1 inlet y = Inc.map2(Inc.Var.watch x)(Inc.Var.watch x) ~f:( + ) in
let z = Inc.Var.create 2 inlet w = Inc.map2(Inc.Var.watch y)(Inc.Var.watch z) ~f:( + ) in
let w_obs = Inc.observe w in
Inc.Var.set x 3;

construction
acyclic dependency graphwith “modifiables/cells”

Inc.stabilize ();manipulation
change propagation
value extraction

print_int(Inc.Observer.value_exn w_obs)
27

Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”“spreadsheet”

Self-Adjusting Computation [Acar ‘05]
(Incremental, an OCaml library)
let x = Inc.Var.create 1 inlet y = Inc.map2(Inc.Var.watch x)(Inc.Var.watch x) ~f:( + ) in
let z = Inc.Var.create 2 inlet w = Inc.map2(Inc.Var.watch y)(Inc.Var.watch z) ~f:( + ) in
let w_obs = Inc.observe w in
Inc.Var.set x 3;

construction“modifiables”“cells”
21x

Inc.stabilize ();z+print_int(Inc.Observer.value_exn w_obs)

y+w_obs = 428

Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”“spreadsheet”

Self-Adjusting Computation [Acar ‘05]
(Incremental, an OCaml library)
let x = Inc.Var.create 1 inlet y = Inc.map2(Inc.Var.watch x)(Inc.Var.watch x) ~f:( + ) in
let z = Inc.Var.create 2 inlet w = Inc.map2(Inc.Var.watch y)(Inc.Var.watch z) ~f:( + ) in
let w_obs = Inc.observe w in
Inc.Var.set x 3;

constructionchange set2

3x

Inc.stabilize ();z+

print_int(Inc.Observer.value_exn w_obs)

y+w_obs = 429

Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”“spreadsheet”

Self-Adjusting Computation [Acar ‘05]
(Incremental, an OCaml library)
let x = Inc.Var.create 1 inlet y = Inc.map2(Inc.Var.watch x)(Inc.Var.watch x) ~f:( + ) in
let z = Inc.Var.create 2 inlet w = Inc.map2(Inc.Var.watch y)(Inc.Var.watch z) ~f:( + ) in
let w_obs = Inc.observe w in
Inc.Var.set x 3;

manipulation
change propagation

23x

Inc.stabilize ();z+

print_int(Inc.Observer.value_exn w_obs)

y+w_obs = 830

Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”“spreadsheet”

Self-Adjusting Computation [Acar ‘05]
(Incremental, an OCaml library)
let x = Inc.Var.create 1 inlet y = Inc.map2(Inc.Var.watch x)(Inc.Var.watch x) ~f:( + ) in
let z = Inc.Var.create 2 inlet w = Inc.map2(Inc.Var.watch y)(Inc.Var.watch z) ~f:( + ) in
let w_obs = Inc.observe w in
Inc.Var.set x 3;

value extraction
observation

23x

Inc.stabilize ();z+print_int(Inc.Observer.value_exn w_obs)

y+w_obs = 831

Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”
Probabilistic Programming[program]

construction
stochastic model + observations[run-time system]

manipulation
stochastic inference
value extraction
posterior distribution

32

Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”
valuewith computation graphresult● construction● manipulation
TensorFlow
imperative parameter update on machine-learning model
Self-Adjusting Computation
change propagation on acyclic dependency graph
Probabilistic Programming
inference on stochastic model
33

Muroya (RIMS, Kyoto U. & U. B’ham.)token-passing semantics without rewriting… result given by the token

token-passing semantics with rewriting… result given by a diagram
selective rewriting
programming with “computation graphs”… result being value with computation graph
34

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics with & without rewriting
programdiagramredex searchtoken passing

reduction

diagram rewriting

construction

selective
diagram rewriting

manipulation

diagram rewriting

value extraction

token data

evaluation

computationgraphs

35

Muroya (RIMS, Kyoto U. & U. B’ham.)Programming with “computation graphs”
valuewith computation graphresult● construction● manipulation
Idealised TensorFlow [−,Cheung&Ghica ‘18]
functional parameter update on machine-learning model
Synchronous Self-Adjusting Computation
change propagation on cyclic dependency graph

36

Muroya (RIMS, Kyoto U. & U. B’ham.)Synchronous Self-Adjusting Computation
live demo: https://cwtsteven.github.io/GoI-SAC-Visualiser/x = {1}y = x + xz = {2}w = y + z
link x to 3;

construction
cyclic dependency graphwith “modifiables/cells”_ = step ()_ = step ()w;

manipulation
cell-wise change propagation37

multiple
independent tokens
without
rewriting
Muroya (RIMS,
Kyoto U. & U. B’ham.)Synchronous Self-Adjusting Computation
live demo: https://cwtsteven.github.io/GoI-SAC-Visualiser/(* alternating signal *)x = {true}
link x to ~x;_ = step ()_ = step ()construction
cyclic dependency graphwith “modifiables/cells”

manipulation
cell-wise change propagation38

multiple
independent tokens
withoutrewriting
Muroya (RIMS,Kyoto U. & U. B’ham.)token-passing semantics without rewriting… result given by the token

token-passing semantics with rewriting… result given by a diagram
selective rewriting
programming with “computation graphs”… result being value with computation graphgiven by the token and a diagram with “cells”
39

Muroya (RIMS, Kyoto U. & U. B’ham.)Token-passing semantics with & without rewriting
programdiagramredex searchtoken passing

reduction

diagram rewriting

construction

selective
diagram rewriting

manipulation

diagram rewriting

value extraction

token data

evaluation

computationgraphs40

Muroya (RIMS, Kyoto U. & U. B’ham.)Directions● sit back and lay the foundation?
○ “cells”, special constants■ shared but never duplicated■ blocking rewrite● more applications?
○ differentiating (higher-order) computation graphs○ digesting meta-level stochastic inference

41

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