• 検索結果がありません。

The dynamic Geometry of Interaction machine

N/A
N/A
Info
ダウンロード
Protected

Academic year: 2022

シェア "The dynamic Geometry of Interaction machine"

Copied!
151
0
0

読み込み中.... (全文を見る)

今ダウンロードする ( 151 ページ )

全文

(1)

Muroya (U. B’ham.)

The dynamic Geometry of Interaction machine

a call-by-need graph rewriter

Koko Muroya & Dan R. Ghica (University of Birmingham)

CSL (Stockholm), 21 Aug. 2017

(2)

Muroya (U. B’ham.)

Quantitative analysis

by GoI-style token passing of

space-time trade-off

of program execution cost

2

(3)

Muroya (U. B’ham.)

Quantitative analysis

by GoI-style token passing of

space-time trade-off

of program execution cost

semantics of linear logic

3

(4)

Muroya (U. B’ham.)

Quantitative analysis

by GoI-style token passing of

space-time trade-off

of program execution cost

semantics of linear logic

abstract machines for lambda-calculus

4

(5)

Muroya (U. B’ham.)

Interaction abstract machine (IAM)

●[Danos & Regnier ’99]

●call-by-name evaluation

●designed after Geometry of Interaction [Girard ’89]

semantics of linear logic

5

(6)

Muroya (U. B’ham.)

6

Interaction abstract machine (IAM)

GoI token passing fixed graph

(7)

Muroya (U. B’ham.)

7

Interaction abstract machine (IAM)

GoI token passing fixed graph

(8)

Muroya (U. B’ham.)

8

Interaction abstract machine (IAM)

GoI token passing fixed graph

(9)

Muroya (U. B’ham.)

9

Interaction abstract machine (IAM)

GoI token passing fixed graph

(10)

Muroya (U. B’ham.)

10

Interaction abstract machine (IAM)

GoI token passing fixed graph

(11)

Muroya (U. B’ham.)

11

Interaction abstract machine (IAM)

GoI token passing fixed graph

(12)

Muroya (U. B’ham.)

12

Interaction abstract machine (IAM)

GoI token passing fixed graph

(13)

Muroya (U. B’ham.)

13

Interaction abstract machine (IAM)

GoI token passing fixed graph

(14)

Muroya (U. B’ham.)

14

Interaction abstract machine (IAM)

GoI token passing fixed graph

(15)

Muroya (U. B’ham.)

15

Interaction abstract machine (IAM)

GoI token passing fixed graph

(16)

Muroya (U. B’ham.)

16

Interaction abstract machine (IAM)

GoI token passing fixed graph

(17)

Muroya (U. B’ham.)

17

Interaction abstract machine (IAM)

GoI token passing fixed graph

(18)

Muroya (U. B’ham.)

18

Interaction abstract machine (IAM)

GoI token passing fixed graph

(19)

Muroya (U. B’ham.)

19

Interaction abstract machine (IAM)

GoI token passing fixed graph

(20)

Muroya (U. B’ham.)

20

Interaction abstract machine (IAM)

GoI token passing fixed graph

(21)

Muroya (U. B’ham.)

21

Interaction abstract machine (IAM)

GoI token passing fixed graph

(22)

Muroya (U. B’ham.)

22

Interaction abstract machine (IAM)

GoI token passing fixed graph

(23)

Muroya (U. B’ham.)

23

Interaction abstract machine (IAM)

GoI token passing fixed graph

(24)

Muroya (U. B’ham.)

24

Interaction abstract machine (IAM)

GoI token passing fixed graph

(25)

Muroya (U. B’ham.)

25

Interaction abstract machine (IAM)

GoI token passing fixed graph

(26)

Muroya (U. B’ham.)

26

Interaction abstract machine (IAM)

GoI token passing fixed graph

(27)

Muroya (U. B’ham.)

27

Interaction abstract machine (IAM)

GoI token passing fixed graph

(28)

Muroya (U. B’ham.)

28

Interaction abstract machine (IAM)

GoI token passing fixed graph

(29)

Muroya (U. B’ham.)

29

Interaction abstract machine (IAM)

GoI token passing fixed graph

(30)

Muroya (U. B’ham.)

30

Interaction abstract machine (IAM)

GoI token passing fixed graph

(31)

Muroya (U. B’ham.)

31

Interaction abstract machine (IAM)

GoI token passing fixed graph

(32)

Muroya (U. B’ham.)

32

Interaction abstract machine (IAM)

GoI token passing fixed graph

(33)

Muroya (U. B’ham.)

33

Interaction abstract machine (IAM)

GoI token passing fixed graph

(34)

Muroya (U. B’ham.)

34

Interaction abstract machine (IAM)

GoI token passing fixed graph

(35)

Muroya (U. B’ham.)

35

Interaction abstract machine (IAM)

GoI token passing fixed graph

(36)

Muroya (U. B’ham.)

36

Interaction abstract machine (IAM)

GoI token passing fixed graph

(37)

Muroya (U. B’ham.)

37

Interaction abstract machine (IAM)

GoI token passing fixed graph

(38)

Muroya (U. B’ham.)

38

Interaction abstract machine (IAM)

GoI token passing fixed graph

(39)

Muroya (U. B’ham.)

39

Interaction abstract machine (IAM)

GoI token passing fixed graph

(40)

Muroya (U. B’ham.)

40

Interaction abstract machine (IAM)

GoI token passing fixed graph

(41)

Muroya (U. B’ham.)

41

Interaction abstract machine (IAM)

GoI token passing fixed graph

(42)

Muroya (U. B’ham.)

42

Interaction abstract machine (IAM)

GoI token passing fixed graph

(43)

Muroya (U. B’ham.)

43

Interaction abstract machine (IAM)

GoI token passing fixed graph

(44)

Muroya (U. B’ham.)

44

Interaction abstract machine (IAM)

GoI token passing fixed graph

(45)

Muroya (U. B’ham.)

45

Interaction abstract machine (IAM)

GoI token passing fixed graph

(46)

Muroya (U. B’ham.)

46

Interaction abstract machine (IAM)

GoI token passing fixed graph

(47)

Muroya (U. B’ham.)

47

Interaction abstract machine (IAM)

GoI token passing fixed graph

(48)

Muroya (U. B’ham.)

48

Interaction abstract machine (IAM)

GoI token passing fixed graph

(49)

Muroya (U. B’ham.)

49

Interaction abstract machine (IAM)

GoI token passing fixed graph

(50)

Muroya (U. B’ham.)

50

Interaction abstract machine (IAM)

GoI token passing fixed graph

(51)

Muroya (U. B’ham.)

51

Interaction abstract machine (IAM)

GoI token passing fixed graph

(52)

Muroya (U. B’ham.)

52

Interaction abstract machine (IAM)

GoI token passing fixed graph

(53)

Muroya (U. B’ham.)

53

Interaction abstract machine (IAM)

GoI token passing fixed graph

(54)

Muroya (U. B’ham.)

54

Interaction abstract machine (IAM)

GoI token passing fixed graph

(55)

Muroya (U. B’ham.)

Storeless abstract machine (SAM)

●[Danvy & Zerny ’13]

●call-by-need evaluation

●syntactical environment

55

(56)

Muroya (U. B’ham.)

Storeless abstract machine (SAM)

redex searching term rewriting

56

(57)

Muroya (U. B’ham.)

Storeless abstract machine (SAM)

redex searching term rewriting

57

(58)

Muroya (U. B’ham.)

Storeless abstract machine (SAM)

redex searching term rewriting

58

(59)

Muroya (U. B’ham.)

Storeless abstract machine (SAM)

redex searching term rewriting

59

(60)

Muroya (U. B’ham.)

Storeless abstract machine (SAM)

redex searching term rewriting

60

(61)

Muroya (U. B’ham.)

Storeless abstract machine (SAM)

redex searching term rewriting

61

(62)

Muroya (U. B’ham.)

Storeless abstract machine (SAM)

redex searching term rewriting

62

(63)

Muroya (U. B’ham.)

Storeless abstract machine (SAM)

redex searching term rewriting

63

(64)

Muroya (U. B’ham.)

Storeless abstract machine (SAM)

redex searching term rewriting

64

(65)

Muroya (U. B’ham.)

Storeless abstract machine (SAM)

redex searching term rewriting

65

(66)

Muroya (U. B’ham.)

Storeless abstract machine (SAM)

redex searching term rewriting

66

(67)

Muroya (U. B’ham.)

IAM vs. SAM

67

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

(68)

Muroya (U. B’ham.)

IAM vs. SAM

68

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

space efficient

time efficient

(69)

Muroya (U. B’ham.)

IAM vs. SAM

69

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

space efficient

time efficient unified

framework?

(70)

Muroya (U. B’ham.)

Quantitative analysis

by GoI-style token passing of

space-time trade-off

of program execution cost

semantics of linear logic

abstract machines for lambda-calculus

70

(71)

Muroya (U. B’ham.)

IAM vs. SAM

71

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

space efficient

time efficient unified

framework?

(72)

Muroya (U. B’ham.)

72

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

space efficient

time efficient

GoI token passing graph rewriting

Dynamic GoI machine (DGoIM)

unified framework?

(73)

Muroya (U. B’ham.)

73

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

space efficient

time efficient

GoI token passing graph rewriting

Dynamic GoI machine (DGoIM)

unified framework?

[Sinot ’05 & ’06]

(74)

Muroya (U. B’ham.)

74

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

space efficient

time efficient

GoI token passing graph rewriting

Dynamic GoI machine (DGoIM)

unified framework?

(75)

Muroya (U. B’ham.)

75

DGoIM = IAM + proof-net cut elimination

GoI token passing graph rewriting

(76)

Muroya (U. B’ham.)

76

DGoIM = IAM + proof-net cut elimination

GoI token passing graph rewriting

(77)

Muroya (U. B’ham.)

77

DGoIM = IAM + proof-net cut elimination

GoI token passing graph rewriting

(78)

Muroya (U. B’ham.)

78

DGoIM = IAM + proof-net cut elimination

GoI token passing graph rewriting

(79)

Muroya (U. B’ham.)

79

DGoIM = IAM + proof-net cut elimination

GoI token passing graph rewriting

(80)

Muroya (U. B’ham.)

80

DGoIM = IAM + proof-net cut elimination

GoI token passing graph rewriting

(81)

Muroya (U. B’ham.)

81

DGoIM = IAM + proof-net cut elimination

GoI token passing graph rewriting

redex detected

(82)

Muroya (U. B’ham.)

82

DGoIM = IAM + proof-net cut elimination

GoI token passing graph rewriting

(1) trigger rewriting

(83)

Muroya (U. B’ham.)

83

DGoIM = IAM + proof-net cut elimination

GoI token passing graph rewriting

redex detected

(84)

Muroya (U. B’ham.)

84

DGoIM = IAM + proof-net cut elimination

GoI token passing graph rewriting

(2) keep passing

(85)

Muroya (U. B’ham.)

DGoIM: flexible interleaving

85

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

space efficient

time efficient

GoI token passing graph rewriting

DGoIM

passes-only

unified framework?

(86)

Muroya (U. B’ham.)

DGoIM: flexible interleaving

86

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

space efficient

time efficient

GoI token passing graph rewriting

DGoIM

passes-only rewrites-first

unified framework?

(87)

Muroya (U. B’ham.)

Quantitative analysis

by GoI-style token passing of

space-time trade-off

of program execution cost

semantics of linear logic

abstract machines for lambda-calculus

87

(88)

Muroya (U. B’ham.)

DGoIM: flexible interleaving

88

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

space efficient

time efficient

GoI token passing graph rewriting

DGoIM

passes-only rewrites-first

unified framework?

(89)

Muroya (U. B’ham.)

DGoIM: rewrites-first interleaving

89

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

space efficient

time efficient

GoI token passing graph rewriting

DGoIM

passes-only rewrites-first

unified framework?

(90)

Muroya (U. B’ham.)

Rewrites-first DGoIM: states

90

(91)

Muroya (U. B’ham.)

Rewrites-first DGoIM: states

91

multiplicative-exponential proof net

(92)

Muroya (U. B’ham.)

Rewrites-first DGoIM: states

92

simplified data of IAM

multiplicative-exponential proof net

(93)

Muroya (U. B’ham.)

Rewrites-first DGoIM: transitions

93

pass transitions rewrite transitions

proof-net cut elimination selected

GoI token passing

(94)

Muroya (U. B’ham.)

Rewrites-first DGoIM: transitions

94

pass transitions rewrite transitions

proof-net cut elimination selected

GoI token passing

(95)

Muroya (U. B’ham.)

Rewrites-first DGoIM: transitions

95

pass transitions rewrite transitions

rewrites-first interleaving

proof-net cut elimination selected

GoI token passing

(96)

Muroya (U. B’ham.)

Translate lambda-terms

96

“call-by-value translation” of intuitionistic logic to linear logic [Girard ’87]

only values can be copied

(97)

Muroya (U. B’ham.)

Rewrites-first DGoIM: implement call-by-need

97

SAM (call-by-need)

DGoIM

correctness via weak simulation

(98)

Muroya (U. B’ham.)

Rewrites-first DGoIM: implement call-by-need

98

time efficient

time cost analysis à la [Accattoli ’16]

(99)

Muroya (U. B’ham.)

DGoIM: rewrites-first interleaving

99

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

space efficient

time efficient

GoI token passing graph rewriting

DGoIM

passes-only rewrites-first

unified framework?

(100)

Muroya (U. B’ham.)

IAM vs. rewrites-first DGoIM

100

(101)

Muroya (U. B’ham.)

IAM vs. rewrites-first DGoIM

101

(102)

Muroya (U. B’ham.)

IAM vs. rewrites-first DGoIM

102

(103)

Muroya (U. B’ham.)

IAM vs. rewrites-first DGoIM

103

(104)

Muroya (U. B’ham.)

IAM vs. rewrites-first DGoIM

104

(105)

Muroya (U. B’ham.)

IAM vs. rewrites-first DGoIM

105

(106)

Muroya (U. B’ham.)

106

IAM vs. rewrites-first DGoIM

(107)

Muroya (U. B’ham.)

107

IAM vs. rewrites-first DGoIM

(108)

Muroya (U. B’ham.)

108

IAM vs. rewrites-first DGoIM

(109)

Muroya (U. B’ham.)

109

IAM vs. rewrites-first DGoIM

(110)

Muroya (U. B’ham.)

110

IAM vs. rewrites-first DGoIM

(111)

Muroya (U. B’ham.)

111

IAM vs. rewrites-first DGoIM

(112)

Muroya (U. B’ham.)

112

IAM vs. rewrites-first DGoIM

(113)

Muroya (U. B’ham.)

113

IAM vs. rewrites-first DGoIM

(114)

Muroya (U. B’ham.)

114

IAM vs. rewrites-first DGoIM

(115)

Muroya (U. B’ham.)

115

IAM vs. rewrites-first DGoIM

(116)

Muroya (U. B’ham.)

116

IAM vs. rewrites-first DGoIM

(117)

Muroya (U. B’ham.)

117

IAM vs. rewrites-first DGoIM

(118)

Muroya (U. B’ham.)

118

IAM vs. rewrites-first DGoIM

(119)

Muroya (U. B’ham.)

119

IAM vs. rewrites-first DGoIM

(120)

Muroya (U. B’ham.)

120

IAM vs. rewrites-first DGoIM

(121)

Muroya (U. B’ham.)

121

IAM vs. rewrites-first DGoIM

(122)

Muroya (U. B’ham.)

122

IAM vs. rewrites-first DGoIM

(123)

Muroya (U. B’ham.)

123

IAM vs. rewrites-first DGoIM

(124)

Muroya (U. B’ham.)

124

IAM vs. rewrites-first DGoIM

(125)

Muroya (U. B’ham.)

125

IAM vs. rewrites-first DGoIM

(126)

Muroya (U. B’ham.)

126

IAM vs. rewrites-first DGoIM

(127)

Muroya (U. B’ham.)

127

IAM vs. rewrites-first DGoIM

(128)

Muroya (U. B’ham.)

128

IAM vs. rewrites-first DGoIM

(129)

Muroya (U. B’ham.)

129

IAM vs. rewrites-first DGoIM

(130)

Muroya (U. B’ham.)

130

IAM vs. rewrites-first DGoIM

(131)

Muroya (U. B’ham.)

131

IAM vs. rewrites-first DGoIM

(132)

Muroya (U. B’ham.)

132

IAM vs. rewrites-first DGoIM

(133)

Muroya (U. B’ham.)

133

IAM vs. rewrites-first DGoIM

(134)

Muroya (U. B’ham.)

134

IAM vs. rewrites-first DGoIM

(135)

Muroya (U. B’ham.)

135

IAM vs. rewrites-first DGoIM

(136)

Muroya (U. B’ham.)

136

IAM vs. rewrites-first DGoIM

(137)

Muroya (U. B’ham.)

137

IAM vs. rewrites-first DGoIM

(138)

Muroya (U. B’ham.)

138

IAM vs. rewrites-first DGoIM

(139)

Muroya (U. B’ham.)

139

IAM vs. rewrites-first DGoIM

(140)

Muroya (U. B’ham.)

140

IAM vs. rewrites-first DGoIM

(141)

Muroya (U. B’ham.)

141

IAM vs. rewrites-first DGoIM

(142)

Muroya (U. B’ham.)

142

IAM vs. rewrites-first DGoIM

(143)

Muroya (U. B’ham.)

143

IAM vs. rewrites-first DGoIM

(144)

Muroya (U. B’ham.)

144

IAM vs. rewrites-first DGoIM

(145)

Muroya (U. B’ham.)

145

29 passes 16 rewrites

IAM vs. rewrites-first DGoIM

(146)

Muroya (U. B’ham.)

146

29 passes 16 rewrites

IAM vs. rewrites-first DGoIM

(147)

Muroya (U. B’ham.)

147

29 passes 16 rewrites

IAM vs. rewrites-first DGoIM

(148)

Muroya (U. B’ham.)

148

48 passes 29 passes

16 rewrites

IAM vs. rewrites-first DGoIM

(149)

Muroya (U. B’ham.)

Quantitative analysis

by GoI-style token passing of

space-time trade-off

of program execution cost

semantics of linear logic

abstract machines for lambda-calculus

149

(150)

Muroya (U. B’ham.)

DGoIM: flexible interleaving

150

GoI token passing fixed graph

redex searching term rewriting

IAM (call-by-name) SAM (call-by-need)

space efficient

time efficient

GoI token passing graph rewriting

DGoIM

passes-only rewrites-first

unified framework?

(151)

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

参照

今ダウンロードする ( PDF - 151 ページ - 1.38 MB )

関連したドキュメント

Resumption-Based Categorical Geometry of Interaction for Effects

Naohiko Hoshino, Koko Muroya, Ichiro Hasuo, Memoryful Geometry of Interaction:.. From Coalgebraic Components fo Algebraic Effects , submitted to

Efficient implementation of evaluation strategies

interaction abstract machine token passing on fixed graph. call

Hypernet Semantics of Programming Languages

These abstract machines are inspired by Girard’s Geometry of Interaction, and model program execution as dynamic rewriting of graph representation of a pro- gram, guided and

Token-passing semantics with and without rewriting

redex search token passing reduction diagram rewriting. computation

Dynamic GoI machine

Theorem A.1. The dynamic GoI machine simulates the call-by-need storeless abstract machine [Danvy & Zerny ’13] in linear cost, i.e. Reversible, irreversible and optimal

Geometry of Interaction explained

The framework is based on a traced symmetric monoidal category, and it yields a certain compact closed category as a model of linear combinatory algebra, covering as much as

Recursion and Adequacy in Memoryful Geometry of Interaction

The mGoI framework provides token machine semantics of effectful computations, namely computations with algebraic effects, in which effectful λ-terms are translated to transducers..

Spectral Theory for a Mathematical Model of the Weak Interaction—Part I: The Decay of the

The total Hamiltonian, which is the sum of the free energy of the particles and antiparticles and of the interaction, is a self-adjoint operator in the Fock space for the leptons