Token-passing semantics with and without rewriting

(1)

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)

(2)

Token-passing semantics

without rewriting

(3)

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...

(4)

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, ...

(5)

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

(6)

Token-passing semantics without rewriting

live demo:

Jamping Abstract Machine for call-by-name λ-calculus [DR99]

program λ-graph + !-boxes

evaluation token passing + jumping result token data/position

(7)

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

(8)

Token-passing semantics

with rewriting

(9)

Token-passing semantics with rewriting

● 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)

(10)

Token-passing semantics with rewriting

● 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]

(11)

Token-passing semantics with rewriting

live demo:

Dynamic GoI Machine for call-by-value λ-calculus [KG17]

program diagram

evaluation

result diagram

(12)

Token-passing semantics with rewriting

live demo:

Dynamic GoI Machine for call-by-value λ-calculus [KG17]

program λ-graph +

!-boxes

evaluation

result λ-graph +

!-boxes

(13)

Token-passing semantics with rewriting

● with robustness [S05] [S06]

● with time/space efficiency [MG17]

program diagram

evaluation

result diagram

(14)

Token-passing semantics with rewriting

program diagram

evaluation

result diagram

whenever possible

(15)

Token-passing semantics with rewriting

program diagram

evaluation

result diagram

selective?

(16)

Token-passing semantics

with and without rewriting

(17)

token-passing semantics without rewriting

… space efficiency

token-passing semantics with rewriting

… time efficiency

non-trivial space/time balancing?

selective rewriting

(18)

token-passing semantics without rewriting

… space efficiency

token-passing semantics with rewriting

… time efficiency

non-trivial space/time balancing?

another perspective

selective rewriting

(19)

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

(20)

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

(21)

Programming with “computation graphs”

result value

with computation graph

● construction

● manipulation

(22)

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 = ...

y_initial_values = sess.run(y)

construction

machine-learning model with parameters

manipulation

model training

(imperative parameter update) value extraction

output prediction

(23)

Programming with “computation graphs”

y_data = ...

construction

x

*

W b

+

y

“variables”

(24)

Programming with “computation graphs”

y_data = ...

construction

x

*

W b

+

y

“variables”

“parameters”

(25)

Programming with “computation graphs”

y_data = ...

manipulation

x

*

W’ b’

+

y

in-place (imperative) parameter update

(26)

Programming with “computation graphs”

y_data = ...

manipulation

x

*

W’ b’

+

y x_data

output prediction

(27)

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)

(28)

Programming with “computation graphs”

construction

“spreadsheet”

print_int

1

+

2

+

“modifiables”

“cells”

x z

y

(29)

Programming with “computation graphs”

construction

“spreadsheet”

print_int

3

+

2

+

change set

x z

y

(30)

Programming with “computation graphs”

manipulation

“spreadsheet”

print_int

3

+

2

+

change propagation

x z

y

(31)

Programming with “computation graphs”

value extraction

“spreadsheet”

print_int

3

+

2

+

observation

x z

y

(32)

Probabilistic Programming

Programming with “computation graphs”

construction

stochastic model + observations

manipulation

stochastic inference value extraction

posterior distribution

[program]

[run-time system]

(33)

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

● construction

● manipulation

(34)

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

(35)

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

(36)

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

● construction

● manipulation

(37)

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

(38)

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

(39)

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

(40)

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

(41)

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