The Geometry ofComputation-Graph
Abstraction
Koko Muroya(University of Birmingham& RIMS, Kyoto University)

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

LICS
2018
(Oxford),12 July
2018
Muroya(U. B’ham.
& RIMS,
KyotoU.)TensorFlow ( https://www.tensorflow.org/ )an EDSL, for machine learning, with computation graphs

Idealised TensorFlow
a calculus with higher-order with computation graphs

2

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

Background: TensorFlow ( https://www.tensorflow.org/ )an EDSL, for machine learning, with computation graphs
data-flow networks with changeable components
constant
operation“variable”
with a tentative value“input”3

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

Background: TensorFlow ( https://www.tensorflow.org/ )an EDSL, for machine learning, with computation graphs
data-flow networks with changeable components
constant
operation“variable” “cell”
with a tentative value“input”4

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

Background: Computation in TensorFlow
an EDSL, for machine learning, with computation graphs
modelbuild
input `x`

two cellswith tentativevalues `W` and `b`example: simple linear regression f(x) = W * x + b

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

Background: Computation in TensorFlow
an EDSL, for machine learning, with computation graphs
model

outputbuild

useby plugging invalues to inputs

trainby updating values of cells
using (input & desired output) data
6

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

Background: Computation in TensorFlow
an EDSL, for machine learning, with computation graphs
model

outputbuild

useby plugging invalues to inputs

train

cells automatically collected
at run-timeby updating values of cells
using (input & desired output) data
7

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

Background: Programming in TensorFlow
an EDSL, for machine learning, with computation graphs
model

outputbuild

use

x_data = ...
sess = tf.Session()sess.run(init)
y_initial_values = sess.run(y)train
W = tf.Variable(...)
b = tf.Variable(...)
y = W * x_data + b

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

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

TensorFlow ( https://www.tensorflow.org/ )an EDSL, for machine learning, with computation graphs✓✓●●

automatic collection of cells
automatic differentiation
limited integration with a host language
imperative update of cells

9

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

TensorFlow ( https://www.tensorflow.org/ )an EDSL, for machine learning, with computation graphs✓✓●●

automatic collection of cells
automatic differentiation
limited integration with a host language
imperative update of cellsIdealised TensorFlow
a calculus with higher-order computation graphs✓✓✓➢

automatic collection of cells
automatic differentiation
full integration
functional update of cells
10

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Computation in Idealised TensorFlow
a calculus with higher-order computation graphs
model

outputbuilduse

train

higher-order computation graph● input as function argument● cell as it is11

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Computation in Idealised TensorFlow
a calculus with higher-order computation graphs
model

outputbuild

use

by function application

train

12

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Computation in Idealised TensorFlow
a calculus with higher-order computation graphs
model

outputbuild

use

train ?

13

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Computation in Idealised TensorFlow
a calculus with higher-order computation graphs
model

outputuse

build

decoupled model
graph
abstraction

use

train
14

Muroya (U. B’ham. & RIMS, Kyoto U.)Graph abstraction
run-time operation to automatically collect cells
modeldecoupled model

graph
abstraction

15

Muroya (U. B’ham. & RIMS, Kyoto U.)Graph abstraction
run-time operation to automatically collect cells

via language construct `Abs`

1. pure function, representing parameterised model
2. opaque vector○ size determined at run-timecells may be○ order of elements obscured
contributed byfree variables
16

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

Functional, not imperative, training

decoupled model

train
17

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

Functional, not imperative, training
new values of cells computed,yielding (again) an opaque vector

decoupled model… with parameterised model unchanged

train
18

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Computation in Idealised TensorFlow
a calculus with higher-order computation graphs
model

outputuse

build

decoupled modelgraphabstraction

use

train
19

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Programming in Idealised TensorFlow● built a model using cells

20

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Programming in Idealised TensorFlow● built a model using cells● get a decoupled model using graph abstraction

21

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Programming in Idealised TensorFlow● built a model using cells● get a decoupled model using graph abstraction● train a model, by calculating new values of cells

22

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Programming in Idealised TensorFlow● built a model using cells● get a decoupled model using graph abstraction● train a model, by calculating new values of cells● use the trained model, yielding output23

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Programming in Idealised TensorFlow
simply-typed λ-calculus, extended by:● cells … containing field elements● graph abstraction `Abs` … in implication form `A`● opaque vectors … with operations

24

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Semantics of Idealised TensorFlow
a “dynamic Geometry of Interaction machine” [M. & Ghica ‘17], atoken-guided graph-rewriting abstract machine● redex searching by moving the “token”● rewriting by replacing a sub-graph● observing value by looking at data carried by the“token”
implementing call-by-value evaluation,25

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Semantics of Idealised TensorFlow
a “dynamic Geometry of Interaction machine” [M. & Ghica ‘17], atoken-guided graph-rewriting abstract machine● redex searching by moving the “token”● rewriting by replacing a sub-graphcomputation with computation graphs● observing value by looking at data carried by the“token”
implementing call-by-value evaluation,

26

Muroya (U. B’ham. & RIMS, Kyoto U.)Proposed Semantics of Idealised TensorFlow
a “dynamic Geometry of Interaction machine” [M. & Ghica ‘17], atoken-guided graph-rewriting abstract machine● redex searching by moving the “token”● rewriting by replacing a sub-graphcomputation with computation graphs● observing value by looking at data carried by the“token”
implementing call-by-value evaluation,… to prove● type-soundness● program equivalence○ restricted call-by-value beta-law○ garbage collection27

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

TensorFlow ( https://www.tensorflow.org/ )an EDSL, for machine learning, with computation graphs✓✓●●

automatic collection of cells
automatic differentiation
limited integration with a host language
imperative update of cells

Idealised TensorFlow
a calculus with higher-order computation graphs✓✓✓➢

automatic collection of cells
automatic differentiation
full integration
functional update of cells
28

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

TensorFlow ( https://www.tensorflow.org/ )an EDSL, for machine learning, with computation graphs✓✓●●

automatic collection ofonline
cells visualiser
automaticdifferentiation
https://cwtsteven.github.io/GoI-TF-Visualiser/C
BV-with-CBN-embedding/index.html
limited integration
with a host language
imperative update of cells… to see Idealised Tensorflow in full action!

Idealised TensorFlow
a calculus with higher-order computation graphs✓✓✓➢

automatic collection of cells
automatic differentiation
full integration
functional update of cells
29

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

TensorFlow ( https://www.tensorflow.org/ )an EDSL, for machine learning, with computation graphs✓✓●●DecML,implementation(s)as an OCaml PPX
automaticcollectionof cells
automatic differentiation extension
https://github.com/DecML/decml-ppx
limited integration with a host language
https://github.com/reubenrowe/ocaml-decml
imperative update of cells[Cheung, Darvariu, Ghica, M. & Rowe, FLOPS ‘18]

Idealised TensorFlow
a calculus with higher-order computation graphs✓✓✓➢

automatic collection of cells
automatic differentiation
full integration
functional update of cells
30

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

Conclusion
calculi with higher-order computation graphs?
token-guided graph rewriting (“dynamicGeometry of Interaction),
powerful & flexible operational semantics✓ automatic cell collection in TensorFlow
language support for the bureaucracy ofmodel parameters in machine learning● automatic differentiation in TensorFlow● dependency between cells à la self-adjusting computation●31

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