The dynamic Geometry ofInteraction machinea call-by-need graph rewriter
Koko Muroya & Dan R. Ghica(University of Birmingham)
CSL (Stockholm),21 Aug.
2017
Muroya(U. B’ham.)Quantitative analysis
by GoI-style token passingofspace-time trade-off
of program execution cost2

Muroya (U. B’ham.)Quantitative analysis
by GoI-style token passingofsemantics oflinear logic

space-time trade-off
of program execution cost3

Muroya (U. B’ham.)Quantitative analysis
by GoI-style token passingofsemantics oflinear logic

space-time trade-off
of program execution cost
abstract machines for lambda-calculus
4

Muroya (U. B’ham.)Interaction abstract machine (IAM)●[Danos & Regnier ’99]
●call-by-name evaluation●designed after Geometry of Interaction [Girard ’89]
semantics oflinear logic

5

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

6

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

7

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

8

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

9

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph10

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

11

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

12

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph13

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

14

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph15

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph16

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph17

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph18

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

19

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

20

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

21

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

22

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

23

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph24

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

25

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

26

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passingfixed graph27

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

28

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

29

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

30

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph31

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph32

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph33

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

34

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

35

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

36

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph37

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph38

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

39

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

40

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

41

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

42

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

43

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

44

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

45

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph46

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

47

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph48

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

49

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

50

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

51

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph

52

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph53

Muroya (U. B’ham.)Interaction abstract machine (IAM)
GoI token passing
fixed graph54

Muroya (U. B’ham.)Storeless abstract machine (SAM)●[Danvy & Zerny ’13]
●call-by-need evaluation●syntactical environment

55

Muroya (U. B’ham.)Storeless abstract machine (SAM)

redex searchingterm rewriting

56

Muroya (U. B’ham.)Storeless abstract machine (SAM)

redex searchingterm rewriting

57Muroya (U. B’ham.)Storeless abstract machine (SAM)

redex searchingterm rewriting

58

Muroya (U. B’ham.)Storeless abstract machine (SAM)

redex searchingterm rewriting

59

Muroya (U. B’ham.)Storeless abstract machine (SAM)

redex searchingterm rewriting

60

Muroya (U. B’ham.)Storeless abstract machine (SAM)

redex searchingterm rewriting

61

Muroya (U. B’ham.)Storeless abstract machine (SAM)

redex searchingterm rewriting

62

Muroya (U. B’ham.)Storeless abstract machine (SAM)

redex searchingterm rewriting

63

Muroya (U. B’ham.)Storeless abstract machine (SAM)

redex searchingterm rewriting

64

Muroya (U. B’ham.)Storeless abstract machine (SAM)

redex searchingterm rewriting

65

Muroya (U. B’ham.)Storeless abstract machine (SAM)

redex searchingterm rewriting

66

Muroya (U. B’ham.)IAM vs. SAM

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

67

Muroya (U. B’ham.)IAM vs. SAM

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

spaceefficienttimeefficient68

Muroya (U. B’ham.)IAM vs. SAM

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

space
efficient

time
efficientunifiedframework?
69

Muroya (U. B’ham.)Quantitative analysis
by GoI-style token passingofsemantics oflinear logic

space-time trade-off
of program execution cost
abstract machines for lambda-calculus
70

Muroya (U. B’ham.)IAM vs. SAM

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

spaceefficienttime
efficientunifiedframework?
71

Muroya (U. B’ham.)Dynamic GoI machine (DGoIM)
GoI token passing
graph rewriting

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

space
efficient

time
efficientunifiedframework?
72

Muroya (U. B’ham.)Dynamic GoI machine (DGoIM)
GoI token passing
graph rewriting[Sinot ’05 & ’06]

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

space
efficient

time
efficientunifiedframework?
73

Muroya (U. B’ham.)Dynamic GoI machine (DGoIM)
GoI token passing
graph rewriting

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

space
efficient

time
efficientunifiedframework?
74

Muroya (U. B’ham.)DGoIM = IAM + proof-net cut elimination
GoI token passing
graph rewriting

75

Muroya (U. B’ham.)DGoIM = IAM + proof-net cut elimination
GoI token passing
graph rewriting76

Muroya (U. B’ham.)DGoIM = IAM + proof-net cut elimination
GoI token passing
graph rewriting

77

Muroya (U. B’ham.)DGoIM = IAM + proof-net cut elimination
GoI token passing
graph rewriting

78

Muroya (U. B’ham.)DGoIM = IAM + proof-net cut elimination
GoI token passing
graph rewriting

79

Muroya (U. B’ham.)DGoIM = IAM + proof-net cut elimination
GoI token passing
graph rewriting

80

Muroya (U. B’ham.)DGoIM = IAM + proof-net cut elimination
GoI token passing
graph rewriting

redex
detected81

Muroya (U. B’ham.)DGoIM = IAM + proof-net cut elimination
GoI token passing
graph rewriting(1) triggerrewriting

82

Muroya (U. B’ham.)DGoIM = IAM + proof-net cut elimination
GoI token passing
graph rewriting

redexdetected83

Muroya (U. B’ham.)DGoIM = IAM + proof-net cut elimination
GoI token passing
graph rewriting(2) keeppassing

84

Muroya (U. B’ham.)DGoIM: flexible interleaving
DGoIM
GoI token passing
graph rewriting
passes-only

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

space
efficient

time
efficientunified
framework?
85

Muroya (U. B’ham.)DGoIM: flexible interleaving
DGoIM
GoI token passing
graph rewriting
passes-only

rewrites-first

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

space
efficienttimeefficientunifiedframework?
86

Muroya (U. B’ham.)Quantitative analysis
by GoI-style token passingofsemantics oflinear logic

space-time trade-off
of program execution cost
abstract machines for lambda-calculus
87

Muroya (U. B’ham.)DGoIM: flexible interleaving
DGoIM
GoI token passing
graph rewriting
passes-only

rewrites-first

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

space
efficient

time
efficientunifiedframework?
88

Muroya (U. B’ham.)DGoIM: rewrites-first interleaving
DGoIM
GoI token passing
graph rewriting
passes-only

rewrites-first

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

space
efficient

time
efficientunifiedframework?
89

Muroya (U. B’ham.)Rewrites-first DGoIM: states90

Muroya (U. B’ham.)Rewrites-first DGoIM: states
multiplicative-exponential proof net

91

Muroya (U. B’ham.)Rewrites-first DGoIM: states
multiplicative-exponential proof net

simplified
data of IAM
92

Muroya (U. B’ham.)Rewrites-first DGoIM: transitions
pass transitions

rewrite transitions

selected
GoI token
passing

proof-net
cut elimination

93

Muroya (U. B’ham.)Rewrites-first DGoIM: transitions
pass transitions

rewrite transitions

selected
GoI token
passing

proof-net
cut elimination

94

Muroya (U. B’ham.)Rewrites-first DGoIM: transitions
pass transitions

rewrite transitions

selected
GoI token
passing

proof-net
cut elimination

rewritesf

irst inter95

leaving
Muroya (U. B’ham.)Translate lambda-terms“call-by-value translation” of intuitionistic logic to linear logic[Girard ’87]
only values
can be copied

96

Muroya (U. B’ham.)Rewrites-first DGoIM: implement call-by-need
DGoIM
SAM (call-by-need)correctness via weak simulation
97

Muroya (U. B’ham.)Rewrites-first DGoIM: implement call-by-needtime cost analysis à la [Accattoli ’16]

timeefficient98

Muroya (U. B’ham.)DGoIM: rewrites-first interleaving
DGoIM
GoI token passing
graph rewriting
passes-only

rewrites-first

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

space
efficient

time
efficientunifiedframework?
99

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

100

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

101

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

102

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

103

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

104

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

105

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

106

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

107

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

108

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

109

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

110

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

111

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

112

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

113

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

114

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

115

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

116

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

117

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

118

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

119

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

120

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

121

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

122

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

123

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

124

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

125

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

126

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

127

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

128

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

129

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

130

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

131

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

132

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

133

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

134

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

135

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

136

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

137

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

138

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

139Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

140

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

141

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

142

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

143

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

144

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

29 passes
16 rewrites

145

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

29 passes
16 rewrites

146

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

29 passes
16 rewrites

147

Muroya (U. B’ham.)IAM vs. rewrites-first DGoIM

48 passes

29 passes
16 rewrites

148

Muroya (U. B’ham.)Quantitative analysis
by GoI-style token passingofsemantics oflinear logic

space-time trade-off
of program execution cost
abstract machines for lambda-calculus
149

Muroya (U. B’ham.)DGoIM: flexible interleaving
DGoIM
GoI token passing
graph rewriting
passes-only

rewrites-first

IAM (call-by-name)

SAM (call-by-need)

GoI token passing
fixed graphredex searchingterm rewriting

spaceefficient

timeefficientunifiedframework?
150

Muroya (U. B’ham.)Future work
●flexible interleaving○IAM (call-by-name) -- SAM (call-by-need) spectrum○call-by-value?
●token-guided rewriting of “higher-order” data-flow graphs?
○TensorFlow (https://www.tensorflow.org/)○self-adjusting computation (http://www.umut-acar.org/self-adjusting-computation)

151

Muroya (U. B’ham.)