Resumption-Based Categorical Geometry of Interaction for Effects

1

Resumption-Based Categorical

Geometry of Interaction for Effects

室屋晃子 (蓮尾研究室)

2014年2月12日

2

Resumption-Based Categorical

Geometry of Interaction for Effects

室屋晃子 (蓮尾研究室)

2014年2月12日

Naohiko Hoshino, Koko Muroya, Ichiro Hasuo, Memoryful Geometry of Interaction:

From Coalgebraic Components fo Algebraic Effects ,

submitted to LICS '14

3

目的

プログラムを

ステートマシンに

変換する

● 高階関数型プログラミング

● 計算効果つき

非決定的、確率的、量子

L I R

q/0 q/0 q/1 q/1

●

sequential machine

●

stream transducer

●

Mealy machine

4

目的

プログラムを

ステートマシンに

変換する

←for effects

←resumption-based

←categorical Geometry 　of Interaction

● 高階関数型プログラミング

● 計算効果つき

非決定的、確率的、量子

L I R

q/0 q/0 q/1 q/1

5

ステートマシンへの変換例

非決定的な選択

6

ステートマシンへの変換例

⊕

I

λf. (f 1)+1

＊ λf. f 0

＊

λx. x

＊

L I R

q/n⁰ q/n⁰ q/n¹ q/n¹

7

先行研究　 [Hasuo & Hoshino, LICS'11]

プログラムを

パイプに

変換する

● 高階関数型プログラミング

● 計算効果つき

非決定的、確率的、量子

categorical Geometry of Interaction

[Abramsky, Haghverdi & Scott, MSCS'02]

realizability

[Longley, PhD thesis]

8

: 確率的 : 非決定的

: 計算効果なし

先行研究　 [Hasuo & Hoshino, LICS'11]

パイプ ＝ 関数 ＋ 計算効果

f

A B

モナド

a⁰ a a^{1 2} ...

b⁰ b b^{1 2} ...

9

: 確率的 : 非決定的

: 計算効果なし

先行研究　 [Hasuo & Hoshino, LICS'11]

パイプ ＝ 関数 ＋ 計算効果

モナド

a⁰ a a^{1 2} ...

b⁰ b b^{1 2} ...

f

A

B

10

: 確率的 : 非決定的

: 計算効果なし

先行研究　 [Hasuo & Hoshino, LICS'11]

パイプ ＝ 関数 ＋ 計算効果

モナド

a⁰ a a^{1 2} ...

b⁰ b b^{1 2} ...

f

A

B

11

: 確率的 : 非決定的

: 計算効果なし

先行研究　 [Hasuo & Hoshino, LICS'11]

パイプ ＝ 関数 ＋ 計算効果

モナド

a⁰ a a^{1 2} ...

b⁰ b b^{1 2} ...

0.1

0.2 0.5

f

A

B

12

パイプへの変換例

λx. x λf. f 0

適用→パイプの相互接続 評価→トークンの動き

　　　パイプ間のやりとり

13

パイプへの変換例

λx. x λf. f 0

適用→パイプの相互接続 評価→トークンの動き

　　　パイプ間のやりとり

λf. f 0 λx. x ask: f

ask: x ans: x = 0

ans: f 0 = 0 ans: 0

14

パイプへの変換例

λx. x λf. f 0

適用→パイプの相互接続 評価→トークンの動き

　　　パイプ間のやりとり

λf. f 0 λx. x ask: f

ask: x ans: x = 0

ans: f 0 = 0 ans: 0

15

パイプへの変換例

λx. x λf. f 0

適用→パイプの相互接続 評価→トークンの動き

　　　パイプ間のやりとり

λf. f 0 λx. x ask: f

ask: x ans: x = 0

ans: f 0 = 0 ans: 0

16

パイプへの変換例

λx. x λf. f 0

適用→パイプの相互接続 評価→トークンの動き

　　　パイプ間のやりとり

λf. f 0 λx. x ask: f

ask: x ans: x = 0

ans: f 0 = 0 ans: 0

17

パイプへの変換例

λx. x λf. f 0

適用→パイプの相互接続 評価→トークンの動き

　　　パイプ間のやりとり

λf. f 0 λx. x ask: f

ask: x ans: x = 0

ans: f 0 = 0 ans: 0

18

パイプへの変換例

λx. x λf. f 0

適用→パイプの相互接続 評価→トークンの動き

　　　パイプ間のやりとり

λf. f 0 λx. x ask: f

ask: x ans: x = 0

ans: f 0 = 0 ans: 0

19

パイプへの変換例

λx. x λf. f 0

適用→パイプの相互接続 評価→トークンの動き

　　　パイプ間のやりとり

λf. f 0 λx. x ask: f

ask: x ans: x = 0

ans: f 0 = 0 ans: 0

cf. ゲーム意味論

[Abramsky, Jagadeesan & Malacaria, '00]

[Hyland & Ong, '00]

20

パイプへの変換例

21

パイプへの変換例

22

パイプへの変換例

23

パイプへの変換例

⊕ λf. (f 1)+1

λf. f 0 λx. x

24

パイプへの変換例

⊕ λf. (f 1)+1

λf. f 0 λx. x

25

パイプへの変換例

⊕ λf. (f 1)+1

λf. f 0 λx. x

26

パイプへの変換例

⊕ λf. (f 1)+1

λf. f 0 λx. x

ans: f 0 = 0

27

パイプへの変換例

⊕ λf. (f 1)+1

λf. f 0 λx. x

ans: f 0 = 0

28

パイプへの変換例

⊕ λf. (f 1)+1

λf. f 0 λx. x

ans: 1

29

パイプへの変換例

⊕ λf. (f 1)+1

λf. f 0 λx. x

ans: 1

「記憶」が必要

「記憶」が必要

30

「記憶」の実現

プログラム ＋「記憶」

パイプ ＋「記憶」

31

「記憶」の実現

プログラム ＋「記憶」→ 継続渡し形式

パイプ ＋「記憶」→ ステートマシン

[Hasuo & Hoshino, LICS'11]

[Abramsky, Haghverdi & Scott, MSCS'02] で説明

32

「記憶」の実現

プログラム ＋「記憶」→ 継続渡し形式

パイプ ＋「記憶」→ ステートマシン

[Hasuo & Hoshino, LICS'11]

[Abramsky, Haghverdi & Scott, MSCS'02] で説明

今回の成果：

ステートマシンの具体的構成を与える

→ 計算効果つき高階プログラムの変換の 　 一般的フレームワーク

今回の成果：

ステートマシンの具体的構成を与える

→ 計算効果つき高階プログラムの変換の 　 一般的フレームワーク

33

: 確率的 : 非決定的

: 計算効果なし

「記憶」の埋め込み

ステートマシン ＝ パイプ ＋ 内部状態

x

c

B

モナド

34

ステートマシンへの変換例

⊕

I

λf. (f 1)+1

＊ λf. f 0

＊

λx. x

＊

L I R

35

ステートマシンへの変換例

⊕

I

λf. (f 1)+1

＊ λf. f 0

＊

λx. x

＊

L I R

2項演算子

ステートマシン上の↓ 2項演算

36

ステートマシンへの変換例

⊕

L

λf. (f 1)+1

＊ λf. f 0

＊

λx. x

＊

L I R

2項演算子

ステートマシン上の↓ 2項演算

37

ステートマシンへの変換例

⊕

R

λf. (f 1)+1

＊ λf. f 0

＊

λx. x

＊

L I R

2項演算子

ステートマシン上の↓ 2項演算

38

ステートマシンへの変換例

⊕

I

λf. (f 1)+1

＊ λf. f 0

＊

λx. x

＊

L I R

39

今回の成果

プログラムをステートマシンに変換する 一般的フレームワーク

● 高階関数型プログラミング

● 計算効果つき

40

今回の成果

プログラムをステートマシンに変換する 一般的フレームワーク

1.計算効果をモデルする

an algebraic operation α on a monad

2.ステートマシンを modular に構成する

3.ステートマシンによる表示的意味論を与える

a category on resumptions

● 高階関数型プログラミング

● 計算効果つき

41

今回の成果

プログラムをステートマシンに変換する 一般的フレームワーク

1.計算効果をモデルする

an algebraic operation α on a monad

2.ステートマシンを modular に構成する

3.ステートマシンによる表示的意味論を与える

a category on resumptions

● 高階関数型プログラミング

● 計算効果つき

投稿版 卒論

42

今後の展望

具体的な計算効果に対する応用

●

非決定的計算、確率的計算

●

量子計算

関連手法との比較

●

Geometry of Synthesis [Ghica, ICFP'11

]

高階関数型のプログラムを論理回路に変換する

[Hasuo & Hoshino, LICS'11]

の簡略化？

「記憶」の埋め込み？