記憶つき相互作用の幾何における再帰と妥当性
Recursion and Adequacy inMemoryful Geometry of Interaction

室屋 晃子 (蓮尾研)2016.2.1 修論発表

概要
コンパイラ / 高位合成
[Mackie ’95] [Ghica ’07]

暗黙的計算量理論[Dal Lago ’06]

GoI
[Girard ’89]

memoryful GoI[Hoshino, M. & Hasuo ’14]

2

memoryful GoI
with recursion

Muroya (U. Tokyo)

背景：GoI•

Geometry of Interaction (相互作用の幾何)•表示的 (要素還元的) 意味論••

線形論理に対して [Girard ’89]•

関数型プログラムに対して操作的な性質•

計算の経過を表現

3

Muroya (U. Tokyo)

背景：GoI•

Geometry of Interaction (相互作用の幾何)•表示的 (要素還元的) 意味論••

線形論理に対して [Girard ’89]•

関数型プログラムに対して操作的な性質
トークンマシン意味論•

計算の経過を表現[Mackie ’95] [Danos & Regnier ’99]
3

Muroya (U. Tokyo)

背景：トークンマシン意味論
関数型プログラム

トークンマシン

4

Muroya (U. Tokyo)

背景：トークンマシン意味論
関数型プログラム

トークンマシン

4

Muroya (U. Tokyo)

背景：トークンマシン意味論
関数型プログラム

トークンマシンq4

Muroya (U. Tokyo)

背景：トークンマシン意味論
関数型プログラムq

トークンマシン

4

Muroya (U. Tokyo)

背景：トークンマシン意味論
関数型プログラム1

トークンマシン

4

Muroya (U. Tokyo)

背景：トークンマシン意味論
関数型プログラム1

トークンマシン

4

Muroya (U. Tokyo)

背景：トークンマシン意味論
関数型プログラム•コンパイル技術への応用 [Mackie ’95] [Ghica ’01]•

暗黙的計算量理論への応用 [Dal Lago ’06]•

圏論による定式化 [Abramsky et al. ’02]

トークンマシン5

Muroya (U. Tokyo)

概要
コンパイラ / 高位合成
[Mackie ’95] [Ghica ’07]

暗黙的計算量理論[Dal Lago ’06]

GoI
[Girard ’89]

memoryful GoI[Hoshino, M. & Hasuo ’14]

6

memoryful GoI
with recursion

Muroya (U. Tokyo)

背景：memoryful GoI [Hoshino, M. & Hasuo ’14]関数型プログラム ＋ 計算副作用( x. x + x) (3 t0.1 5)

メモリつきトークンマシン＊L

7

Muroya (U. Tokyo)

背景：memoryful GoI [Hoshino, M. & Hasuo ’14]関数型プログラム ＋ 計算副作用( x. x + x) (3 t0.1 5)

代数的副作用 [Plotkin & Power ’01]
非決定的選択 M t N• 確率的選択M tp N• 大域変数の参照、更新•lookupl (Mv1 , . . . , Mv|Val| )updatel,v (M )メモリつきトークンマシン＊

L

7

Muroya (U. Tokyo)

背景：memoryful GoI [Hoshino, M. & Hasuo ’14]関数型プログラム ＋ 計算副作用( x. x + x) (3 t0.1 5)

副作用つきミーリーマシン＊
q/3 7! 0.1

メモリつきトークンマシン＊

q/3 7! 1

L8

L

q/5 7! 0.9

R

q/5 7! 1

Muroya (U. Tokyo)

概要
コンパイラ / 高位合成
[Mackie ’95] [Ghica ’07]

暗黙的計算量理論[Dal Lago ’06]

GoI
[Girard ’89]

memoryful GoI[Hoshino, M. & Hasuo ’14]

9

memoryful GoIwith recursion

Muroya (U. Tokyo)

結果：memoryful GoI with recursion
関数型プログラム ＋ 計算副作用 ＋ 再帰

メモリつきトークンマシン

10

Muroya (U. Tokyo)

結果：memoryful GoI with recursion
関数型プログラム ＋ 計算副作用 ＋ 再帰

メモリつきトークンマシン

11

Muroya (U. Tokyo)

結果：memoryful GoI with recursion
関数型プログラム ＋ 計算副作用 ＋ 再帰

fix(F ) = F (F (F (· · · )))Girard style···Mackie style

メモリつきトークンマシン

12

Muroya (U. Tokyo)

結果：memoryful GoI with recursion
Prop. (Girard style as fixed point wrt. “cross connection”)

A

N×AAA

N×A

N×A

A

N×AcccAcc'...

N×A

13cAccc...

N×A

Muroya (U. Tokyo)

結果：memoryful GoI with recursion
Prop. (Girard style as supremum of finite approximations)
A
N×Ac
AAc

is the supremum of the ω-chain

...

c

N×A

A
N×A

⊥

⊥
Ac

⊥

!

...

A
N×Ac
A

N×A⊥

⊥

...

N×A!

c
A

N×Ac

⊥

...

! ···

N×A

(i)
Figure 3.5: The ω-chain of Finite Approximations FixG (X, c, x)x0

BwherecE

B

x0

Proposition 3.3.6.ALet (X, c, x)
A : A + N × A ! A + N × A be a T -transducer.
(i)
14 T -transducers forms an ω-chain
The family {FixG (X, c, x) : A ! A}i∈ω ofMuroya (U. Tokyo)

結果：memoryful GoI with recursion
Thm. (coincidence of Girard style & Mackie style)Girard style

Mackie style···15

Muroya (U. Tokyo)

結果：memoryful GoI with recursion
関数型プログラム ＋ 計算副作用 ＋ 再帰

Girard style···Mackie style

メモリつきトークンマシン

16

Muroya (U. Tokyo)

J K : CT ⌃ (Valnat ) ! T N that is a strict continuous function preserving the operations specified by ⌃. When the monad T is equalato the powerset monad P, this interpretation corresponds to forgetN
ting branching structures of effect values (i.e. branching structures
0of program execution): for example two effect values (1 t 2) t 3 and1 t (2 t 3) are identified as a set {enc(1), enc(2), enc(3)} ✓ PN
関数型プログラム＋ndet
計算副作用＋ 再帰 choice operation.
where t 2 ⌃is the nondeterministic
Now we can state adequacy of the translation L M.
e omitted
Theorem 6.4 (adequacy). Any closed term M of base type nat†satisfies
J|M|K=LMM.
y use them 5.7 we
6.3 Proof of Adequacy
depicted
メモリつきToプログラムのprove Theorem 6.4 we introduce
a language L⌃ following [25].
トークンマシンのIn thislanguage all occurrencesof recursion are restricted to finite
評価結果
original
実行結果
depth. Namely L⌃ is made fromthe target language L⌃ , by replacamework
ing the term constructor rec with rec(i) for each i 2 N and by
e do notadding a constant ⌦⌧ for each type ⌧ . In the definition of the small
tegorical
メモリつきトークンマシン
step operational semantics, transitions
egory ofPer. The
rec(i+1) (f : ! ⌧, x : ). M
work: the(i)!
(x:.
M)[rec(f : ! ⌧, x : ). M/f]
to reflect
17

結果：memoryful GoI with recursion(0)

Muroya (U. Tokyo)

例：再帰的な確率プログラム

コイントスの結果

プログラムの返り値

確率

H

00.4

TH

1

0.4 * 0.62

TTH

20.4 * 0.63

TTTH

3

0.4 * 0.64

18

Muroya (U. Tokyo)

例：再帰的な確率プログラム

プログラムの評価結果

19

Muroya (U. Tokyo)

例：再帰的な確率プログラム

プログラムの評価結果得られるメモリつきトークンマシンの実行結果
19

Muroya (U. Tokyo)

例：再帰的な確率プログラム

20

Muroya (U. Tokyo)

例：再帰的な確率プログラム

ε, q

20

Muroya (U. Tokyo)

例：再帰的な確率プログラム1: Tε, q

20

Muroya (U. Tokyo)

例：再帰的な確率プログラム

⬜, q

1: T

20

Muroya (U. Tokyo)

例：再帰的な確率プログラム

⬜, q

1: T
2: T

20

Muroya (U. Tokyo)

例：再帰的な確率プログラム

1: T

⬜⬜, q

2: T

20

Muroya (U. Tokyo)

例：再帰的な確率プログラム

1: T

⬜⬜, q

2: T
3: H

20

Muroya (U. Tokyo)

例：再帰的な確率プログラム⬜⬜⬜, q

1: T
2: T
3: H

⬜⬜⬜, 020

Muroya (U. Tokyo)

例：再帰的な確率プログラム

1: T
2: T

⬜⬜, 1

3: H

20

Muroya (U. Tokyo)

例：再帰的な確率プログラム

1: T
2: T
3: H
⬜, 2

20

Muroya (U. Tokyo)

例：再帰的な確率プログラム

1: Tε, 2

2: T
3: H

20

Muroya (U. Tokyo)

可視化ツール TtT

http://koko-m.
github.
io/TtT/可視化ツール TtT

http://koko-m.
github.
io/TtT/

概要
コンパイラ / 高位合成
[Mackie ’95] [Ghica ’07]

暗黙的計算量理論[Dal Lago ’06]

GoI
[Girard ’89]

memoryful GoI[Hoshino, M. & Hasuo ’14]

22

memoryful GoI
with recursion

Muroya (U. Tokyo)

今後の課題
関数型プログラム ＋ 計算副作用 ＋ 再帰

• 必要なリソース量の見積もり
memoryful GoI
with recursion••

メモリつきトークンマシン

状態空間 / トークンのデータ実行コストの削減•プログラム評価コストとの対応

23

Muroya (U. Tokyo)

論文•Naohiko Hoshino, Koko Muroya & Ichiro Hasuo, “Memoryful Geometry of Interaction: from coalgebraic
components to algebraic effects.”
In Proc. of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic andthe 29th Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS 2014), paper 52, 2014.

•Koko Muroya, Naohiko Hoshino & Ichiro Hasuo, “Memoryful Geometry of Interaction II: recursion andadequacy.”
In Proc. of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL 2016), p. 748–760, 2016.

口頭発表•••“Compiling effectful terms to transducers: prototype implementation of memoryful Geometry ofInteraction” (preliminary report).
•

the 5th Workshop on Syntax and Semantics of Low-Level Languages (LOLA 2014),
Vienna, Austria, 2014 年 7 月.

•

第 25 回代数、論理、幾何と情報科学研究集会 (ALGI 25), 神奈川大学, 2014 年 8 月.

“Memoryful Geometry of Interaction with recursion” (preliminary report).
•

理論計算機科学と圏論ワークショップ (CSCAT 2015), 鹿児島大学, 2015 年 3 月.

•

the 6th Workshop on Syntax and Semantics of Low-Level Languages (LOLA 1015),
Kyoto, Japan, 2015 年 7 月.

“Memoryful Geometry of Interaction II: recursion and adequacy.”•the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016),
St. Petersburg, FL, USA, 2016 年 1 月.

⌃-algebra CT ⌃ (Valnat ) over the set Valnat . On the other hand,for each operation op 2 ⌃, the monad T has an ar(op)-ary al`M:⌧
gebraic operation op on it. This means that the set T N, which isne a T isomorphic to SetT (1, N), is a continuous ⌃-algebra. Therefore we⇤style morphism
can lift the function enc : Valnat ! T N Girard
to a unique
J K : CT ⌃ (Vala strict continuous function ·prenat ) ! T N that
関数型プログラム＋ 計算副作用＋is再帰··
serving the operations specified by ⌃. When the monad T is equal
ato the powerset monad P, this interpretation corresponds
toforgetMackie style
Nting branching structures of effect values (i.e. branching structures
0Thm.
(coincidenceof Girard
style &Mackieof programexecution):for example
twoeffectstyle)values (1 t 2) t 3 and1 t (2 t 3) are identified as a set {enc(1), enc(2), enc(3)} ✓ PN
where t 2 ⌃ndet is the nondeterministic choice operation.
Now we can state adequacy of the translation L M.
omittedTheorem 6.4 (adequacy). Any closed term M of base type nat†satisfies J|M|K = LMM .
y use them 5.7 we
6.3 Proof of Adequacy
depicted
メモリつきトークンマシン
To prove Theorem 6.4 we introduce a language L⌃ following [25].
Inthislanguage
alloccurrences
ofrecursion
arerestricted
tofinite
TtT
original 可視化ツール
depth. Namely L⌃ is made from the target language L⌃ , by replachttp://koko-m.github.io/TtT/
amework
ing the term constructor rec with rec(i) for each i 2 N and by25
e do notMuroya (U. Tokyo)

結論：memoryful GoI with recursion

研究計画
確率プログラム上のベイズ推論
コンパイラ / 高位合成
プログラム評価コストの反映

計算副作用つき関数型プログラムへのGoI による意味論(memoryful GoI)
26

Muroya (U. Tokyo)