Resumption-Based Categorical
Geometry of Interaction for Effects

室屋晃子 (蓮尾研究室)
2014年2月12日
1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 LICS '14
室屋晃子 (蓮尾研究室)
2014年2月12日
2目的プログラムを●高階関数型プログラミング●

計算効果つき非決定的、確率的、量子ステートマシンに
sequential machine● stream transducer● Mealy machine
●

q/0

変換するL

q/0

I

q/1

q/1

R3

目的プログラムを←for effects●

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

計算効果つき非決定的、確率的、量子ステートマシンにq/0変換する

Lq/0I←resumption-based
q/1

q/1

R

←categorical Geometryof Interaction

4

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

非決定的な選択5

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

I＊
λf. f 0q/n0

Lq/n0Iq/n1⊕＊
λf. (f 1)+1

＊
λx. x

q/n1

R

6

先行研究

[Hasuo & Hoshino, LICS'11]

プログラムを●

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

計算効果つき非決定的、確率的、量子パイプに変換する

categorical Geometry of Interaction[Abramsky, Haghverdi & Scott, MSCS'02]
realizability[Longley, PhD thesis]
7

先行研究

[Hasuo & Hoshino, LICS'11]

パイプ ＝ 関数 ＋ 計算効果
モナドAfB: 計算効果なしa0 a1 a2 ...

: 確率的

b0 b1 b2 ...

: 非決定的8

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

パイプ ＝ 関数 ＋ 計算効果
モナド

Af
B

: 計算効果なし

a0 a1 a2 ...

: 確率的

b0 b1 b2 ...

: 非決定的9

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

パイプ ＝ 関数 ＋ 計算効果
モナド

Af
B

: 計算効果なし

a0 a1 a2 ...

: 確率的

b0 b1 b2 ...

: 非決定的10

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

パイプ ＝ 関数 ＋ 計算効果
モナド

Af
B

: 計算効果なし

a0 a1 a2 ...

: 確率的

0.50.2: 非決定的0.1b0 b1 b2 ...

11

パイプへの変換例
適用→パイプの相互接続
評価→トークンの動き
パイプ間のやりとり
λf. f 0

λx. x

12

パイプへの変換例
適用→パイプの相互接続
評価→トークンの動き
パイプ間のやりとり
λf. f 0λx. x

λf. f 0ask: fλx. x
ask: xans: x = 0ans: f 0 = 0
ans: 013

パイプへの変換例
適用→パイプの相互接続
評価→トークンの動き
パイプ間のやりとり
λf. f 0λx. x

λf. f 0ask: fλx. x
ask: xans: x = 0
ans: f 0 = 0
ans: 014

パイプへの変換例
適用→パイプの相互接続
評価→トークンの動き
パイプ間のやりとり
λf. f 0λx. x

λf. f 0ask: fλx. x
ask: xans: x = 0
ans: f 0 = 0
ans: 015

パイプへの変換例
適用→パイプの相互接続
評価→トークンの動き
パイプ間のやりとり
λf. f 0λx. x

λf. f 0ask: fλx. x
ask: xans: x = 0
ans: f 0 = 0
ans: 016

パイプへの変換例
適用→パイプの相互接続
評価→トークンの動き
パイプ間のやりとり
λf. f 0λx. x

λf. f 0ask: fλx. x
ask: xans: x = 0
ans: f 0 = 0
ans: 017

パイプへの変換例
適用→パイプの相互接続
評価→トークンの動き
パイプ間のやりとり
λf. f 0λx. x

λf. f 0ask: fλx. x
ask: xans: x = 0
ans: f 0 = 0
ans: 018

パイプへの変換例
適用→パイプの相互接続
評価→トークンの動き
パイプ間のやりとり
λf. f 0λx. x

λf. f 0ask: fλx. x
ask: xans: x = 0

cf. ゲーム意味論
ans:'00]0[Abramsky, Jagadeesan & Malacaria,[Hyland & Ong, '00]

ans: f 0 = 019

パイプへの変換例

20

パイプへの変換例

21

パイプへの変換例

22

パイプへの変換例

λf. f 0⊕λf. (f 1)+1

λx. x

23

パイプへの変換例

λf. f 0⊕λf. (f 1)+1

λx. x

24

パイプへの変換例

λf. f 0⊕λf. (f 1)+1

λx. x

25

パイプへの変換例

ans: f 0 = 0
λf. f 0⊕λf. (f 1)+1

λx. x

26

パイプへの変換例

ans: f 0 = 0
λf. f 0⊕λf. (f 1)+1λx. x

27

パイプへの変換例

ans: 1
λf. f 0⊕λf. (f 1)+1λx. x

28

パイプへの変換例

ans: 1
λf. f 0⊕λf. (f 1)+1

λx. x

「記憶」が必要「記憶」が必要29

「記憶」の実現
プログラム ＋「記憶」

パイプ ＋「記憶」

30

「記憶」の実現
プログラム ＋「記憶」→ 継続渡し形式[Hasuo & Hoshino, LICS'11]

パイプ ＋「記憶」→ ステートマシン[Abramsky, Haghverdi & Scott, MSCS'02] で説明

31

「記憶」の実現
プログラム ＋「記憶」→ 継続渡し形式[Hasuo & Hoshino, LICS'11]

パイプ ＋「記憶」→ ステートマシン[Abramsky, Haghverdi & Scott, MSCS'02] で説明
今回の成果：
今回の成果：
ステートマシンの具体的構成を与える
ステートマシンの具体的構成を与える→→ 計算効果つき高階プログラムの変換の計算効果つき高階プログラムの変換の一般的フレームワーク
一般的フレームワーク

32

「記憶」の埋め込み
ステートマシン ＝ パイプ ＋ 内部状態
xA

モナドcB

: 計算効果なし: 非決定的: 確率的33

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

IL＊
λf. f 0⊕IR＊
λf. (f 1)+1＊
λx. x34

ステートマシンへの変換例
2項演算子↓ステートマシン上の2項演算

IL＊
λf. f 0⊕IR＊
λf. (f 1)+1＊
λx. x35

ステートマシンへの変換例
2項演算子↓ステートマシン上の2項演算

LL＊
λf. f 0⊕IR＊
λf. (f 1)+1＊
λx. x36ステートマシンへの変換例
2項演算子↓ステートマシン上の2項演算

RL＊
λf. f 0⊕IR＊
λf. (f 1)+1

＊
λx. x

37

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

IL＊
λf. f 0⊕IR＊
λf. (f 1)+1

＊
λx. x

38

今回の成果

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

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

39

今回の成果

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

計算効果つきプログラムをステートマシンに変換する
一般的フレームワーク
1.計算効果をモデルする
an algebraic operation α on a monad

2.ステートマシンを modular に構成する
3.ステートマシンによる表示的意味論を与える
a category on resumptions
40

今回の成果

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

計算効果つきプログラムをステートマシンに変換する
一般的フレームワーク
1.計算効果をモデルする
an algebraic operation α on a monad

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

卒論
投稿版

3.ステートマシンによる表示的意味論を与える
a category on resumptions
41今後の展望
具体的な計算効果に対する応用●
非決定的計算、確率的計算●
量子計算[Hasuo & Hoshino, LICS'11]の簡略化？

関連手法との比較● Geometry of Synthesis [Ghica, ICFP'11 など]
高階関数型のプログラムを論理回路に変換する「記憶」の埋め込み？
42