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)
Token-passing semantics
without rewriting
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...
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...
program diagram
evaluation token passing
(MELL) proof net, λ-graph, ...
Token-passing semantics without rewriting
live demo:
Jamping Abstract Machine for call-by-name λ-calculus [DR99]
https://koko-m.github.io/GoI-Visualiser/
program diagram
evaluation token passing result token data/position
Token-passing semantics without rewriting
live demo:
Jamping Abstract Machine for call-by-name λ-calculus [DR99]
https://koko-m.github.io/GoI-Visualiser/
program λ-graph + !-boxes
evaluation token passing + jumping result token data/position
Token-passing semantics without rewriting
execution models of functional programming
● compiler [Mackie ‘95]
● higher-order synthesis [Ghica ‘07]
program diagram
evaluation token passing result token data/position
Token-passing semantics
with rewriting
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)
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]
program diagram
evaluation
redex search token passing
reduction diagram rewriting
inspired by virtual reduction [Danos&Regnier ‘93]
Token-passing semantics with rewriting
live demo:
Dynamic GoI Machine for call-by-value λ-calculus [KG17]
https://koko-m.github.io/GoI-Visualiser/
program diagram
evaluation
redex search token passing
reduction diagram rewriting
result diagram
Token-passing semantics with rewriting
live demo:
Dynamic GoI Machine for call-by-value λ-calculus [KG17]
https://koko-m.github.io/GoI-Visualiser/
program λ-graph +
!-boxes
evaluation
redex search token passing
reduction diagram rewriting
result λ-graph +
!-boxes
Token-passing semantics with rewriting
execution models of functional programming
● with robustness [S05] [S06]
● with time/space efficiency [MG17]
program diagram
evaluation
redex search token passing
reduction diagram rewriting
result diagram
Token-passing semantics with rewriting
execution models of functional programming
● with robustness [S05] [S06]
● with time/space efficiency [MG17]
program diagram
evaluation
redex search token passing
reduction diagram rewriting
result diagram
whenever possible
Token-passing semantics with rewriting
execution models of functional programming
● with robustness [S05] [S06]
● with time/space efficiency [MG17]
program diagram
evaluation
redex search token passing
reduction diagram rewriting
result diagram
selective?
Token-passing semantics
with and without rewriting
token-passing semantics without rewriting
… space efficiency
token-passing semantics with rewriting
… time efficiency
non-trivial space/time balancing?
selective rewriting
token-passing semantics without rewriting
… space efficiency
token-passing semantics with rewriting
… time efficiency
non-trivial space/time balancing?
another perspective
selective rewriting
token-passing semantics without rewriting
… result given by the token
token-passing semantics with rewriting
… result given by a diagram
programming with dual result
… given by the token and a diagram?
selective rewriting
token-passing semantics without rewriting
… result given by the token
token-passing semantics with rewriting
… result given by a diagram
programming with “computation graphs”
… result being value with computation graph
selective rewriting
Programming with “computation graphs”
result value
with computation graph
● construction
● manipulation
TensorFlow, Google’s machine-learning library
Programming with “computation graphs”
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 model with parameters
manipulation
model training
(imperative parameter update) value extraction
output prediction
TensorFlow, Google’s machine-learning library
Programming with “computation graphs”
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
x
*
W b
+
y
“variables”
TensorFlow, Google’s machine-learning library
Programming with “computation graphs”
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
x
*
W b
+
y
“variables”
“parameters”
TensorFlow, Google’s machine-learning library
Programming with “computation graphs”
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)
manipulation
x
*
W’ b’
+
y
in-place (imperative) parameter update
TensorFlow, Google’s machine-learning library
Programming with “computation graphs”
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)
manipulation
x
*
W’ b’
+
y x_data
output prediction
Self-Adjusting Computation [Acar ‘05]
(Incremental, an OCaml library)
Programming with “computation graphs”
construction
acyclic dependency graph with “modifiables/cells”
manipulation
change propagation value extraction
“spreadsheet”
let x = Inc.Var.create 1 in let y = Inc.map2
(Inc.Var.watch x)
(Inc.Var.watch x) ~f:( + ) in let z = Inc.Var.create 2 in let 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;
Inc.stabilize ();
print_int
(Inc.Observer.value_exn w_obs)
Self-Adjusting Computation [Acar ‘05]
(Incremental, an OCaml library)
Programming with “computation graphs”
construction
“spreadsheet”
let x = Inc.Var.create 1 in let y = Inc.map2
(Inc.Var.watch x)
(Inc.Var.watch x) ~f:( + ) in let z = Inc.Var.create 2 in let 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;
Inc.stabilize ();
print_int
(Inc.Observer.value_exn w_obs)
1
+
2
+
“modifiables”
“cells”
x z
y
Self-Adjusting Computation [Acar ‘05]
(Incremental, an OCaml library)
Programming with “computation graphs”
construction
“spreadsheet”
let x = Inc.Var.create 1 in let y = Inc.map2
(Inc.Var.watch x)
(Inc.Var.watch x) ~f:( + ) in let z = Inc.Var.create 2 in let 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;
Inc.stabilize ();
print_int
(Inc.Observer.value_exn w_obs)
3
+
2
+
change set
x z
y
Self-Adjusting Computation [Acar ‘05]
(Incremental, an OCaml library)
Programming with “computation graphs”
manipulation
“spreadsheet”
let x = Inc.Var.create 1 in let y = Inc.map2
(Inc.Var.watch x)
(Inc.Var.watch x) ~f:( + ) in let z = Inc.Var.create 2 in let 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;
Inc.stabilize ();
print_int
(Inc.Observer.value_exn w_obs)
3
+
2
+
change propagation
x z
y
Self-Adjusting Computation [Acar ‘05]
(Incremental, an OCaml library)
Programming with “computation graphs”
value extraction
“spreadsheet”
let x = Inc.Var.create 1 in let y = Inc.map2
(Inc.Var.watch x)
(Inc.Var.watch x) ~f:( + ) in let z = Inc.Var.create 2 in let 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;
Inc.stabilize ();
print_int
(Inc.Observer.value_exn w_obs)
3
+
2
+
observation
x z
y
Probabilistic Programming
Programming with “computation graphs”
construction
stochastic model + observations
manipulation
stochastic inference value extraction
posterior distribution
[program]
[run-time system]
TensorFlow
imperative parameter update on machine-learning model Self-Adjusting Computation
change propagation on acyclic dependency graph Probabilistic Programming
inference on stochastic model
Programming with “computation graphs”
result value
with computation graph
● construction
● manipulation
token-passing semantics without rewriting
… result given by the token
token-passing semantics with rewriting
… result given by a diagram
programming with “computation graphs”
… result being value with computation graph
selective rewriting
Token-passing semantics with & without rewriting
program diagram
evaluation
redex search token passing reduction diagram rewriting
computation graphs
construction selective
diagram rewriting manipulation diagram rewriting value extraction token data
Idealised TensorFlow [−,Cheung&Ghica ‘18]
functional parameter update on machine-learning model Synchronous Self-Adjusting Computation
change propagation on cyclic dependency graph
Programming with “computation graphs”
result value
with computation graph
● construction
● manipulation
live demo: https://cwtsteven.github.io/GoI-SAC-Visualiser/
Synchronous Self-Adjusting Computation
construction
cyclic dependency graph with “modifiables/cells”
manipulation
cell-wise change propagation
x = {1}
y = x + x z = {2}
w = y + z link x to 3;
_ = step () _ = step () w;
multiple
independent tokens
live demo: https://cwtsteven.github.io/GoI-SAC-Visualiser/
Synchronous Self-Adjusting Computation
construction
cyclic dependency graph with “modifiables/cells”
manipulation
cell-wise change propagation
(* alternating signal *) x = {true}
link x to ~x;
_ = step () _ = step ()
multiple
independent tokens
token-passing semantics without rewriting
… result given by the token
token-passing semantics with rewriting
… result given by a diagram
programming with “computation graphs”
… result being value with computation graph
selective rewriting
Token-passing semantics with & without rewriting
program diagram
evaluation
redex search token passing reduction diagram rewriting
computation graphs
construction selective
diagram rewriting manipulation diagram rewriting value extraction token data
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
