はしごを登る：
プログラムの観測緻密化・観測効率化への新しいアプローチ

室屋 晃子(京都大学 数理解析研究所)
お茶の水女子大学浅井研セミナー, 18 March 2024

自己紹介
室屋晃子（むろやこうこ）● 京都大学 数理解析研究所 助教 (2018.4–)● ← 🇬🇧バーミンガム大学 コンピュータ科学専攻 博士課程 (2016.4–2020.7)● ← 東京大学大学院 情報理工学系研究科コンピュータ科学専攻 修士課程
(2014.4–2016.3)● ← 東京大学 情報科学科 ← 理科一類 (2010.4–2014.3)

2

Muroya (RIMS, Kyoto U.)自己紹介
室屋晃子（むろやこうこ）● プログラム意味論● プログラム実行の数理モデリング● プログラムの振る舞いの形式的な比較

3

Muroya (RIMS, Kyoto U.)

プログラムの振る舞いの形式的な比較● プログラムの観測緻密化 (observational refinement) を数学的に証明する● u が t の観測緻密化である⟺ あらゆる文脈 C に対して、プログラム C[t] の全ての振る舞いはプログラム C[u] で再現できる● 例：

let x = 1 inlet y = 3 iny + yの観測緻密化は43 + 3である

Muroya (RIMS, Kyoto U.)

プログラムの振る舞いの形式的な比較● プログラムの観測効率化 (observational improvement) を数学的に証明する● u が t の観測効率化である⟺ あらゆる文脈 C に対して、プログラム C[t] の全ての振る舞いはより効率的にプログラム C[u] で再現できる● 例：

let x = 1 inlet y = 3 iny + yの観測効率化は53 + 3である

Muroya (RIMS, Kyoto U.)

プログラムの振る舞いの形式的な比較● プログラムの観測効率化 (observational improvement) を数学的に証明する● u が t の観測効率化である⟺ あらゆる文脈 C に対して、プログラム C[t] の全ての振る舞いはより効率的にプログラム C[u] で再現できる● 例：

let x = 1 inlet y = 3 iny + yの観測効率化は3 + 3である証明のためには「振る舞い」や「効率」の定義が必要
5

Muroya (RIMS, Kyoto U.)自己紹介
室屋晃子（むろやこうこ）● プログラム意味論● プログラム実行の数理モデリング● プログラムの振る舞いの形式的な比較

6

Muroya (RIMS, Kyoto U.)

プログラム実行の数理モデリング● いわゆる操作的意味論● （関数型）プログラムの振る舞い⟺ 評価ステップの列⟺…

7

Muroya (RIMS, Kyoto U.)

プログラム実行の数理モデリング● いわゆる操作的意味論● （関数型）プログラムの振る舞い⟺ 評価ステップの列⟺ 評価文脈を用いた項書き換えの列● 例：(fun x -> x + x) (1 + 2)→

8(fun x -> x + x) 3→

3 + 3→

6Muroya (RIMS, Kyoto U.)

プログラム実行の数理モデリング● いわゆる操作的意味論● （関数型）プログラムの振る舞い⟺ 評価ステップの列⟺ トークンを用いたグラフ書き換えの列● 例： https://fyp.jackhughesweb.com/

9

Muroya (RIMS, Kyoto U.)

プログラム実行の数理モデリング● いわゆる操作的意味論● （関数型）プログラムの振る舞い⟺ 評価ステップの列⟺ トークンを用いたグラフ書き換えの列● 例： https://fyp.jackhughesweb.com/

9

Muroya (RIMS, Kyoto U.)

プログラムの観測効率化の証明● プログラムの評価ステップが定義できると、証明可能になる● u が t の観測効率化である⟺ あらゆる文脈 C に対して、プログラム C[t] の全ての振る舞いはより効率的にプログラム C[u] で再現できる

10

Muroya (RIMS, Kyoto U.)

プログラムの観測効率化の証明● プログラムの評価ステップが定義できると、証明可能になる● u が t の観測効率化である⟺ あらゆる文脈 C に対して、プログラム C[t] が k ステップで値 v になる
ならば、プログラム C[u] は l ≤ k となる l ステップで同じ値 v になる11

Muroya (RIMS, Kyoto U.)

プログラムの観測効率化の証明● プログラムの評価ステップが定義できると、証明可能になる● u が t の観測効率化である⟺ あらゆる文脈 C に対して、プログラム C[t] が k ステップで値 v になる
ならば、プログラム C[u] は l ≤ k となる l ステップで同じ値 v になる● ナイーブには、とても大変● あらゆる文脈 C を調べる必要● 評価ステップの列の全体を比べる必要
12

Muroya (RIMS, Kyoto U.)

プログラムの観測効率化の証明● プログラムの評価ステップが定義できると、証明可能になる● u が t の観測効率化である⟺ あらゆる文脈 C に対して、プログラム C[t] が k ステップで値 v になる
ならば、プログラム C[u] は l ≤ k となる l ステップで同じ値 v になる● 有名な証明技法： logical relation [Plotkin '73], applicative bisimulation [Abramsky ’90]
● 主に観測緻密化が対象

13

Muroya (RIMS, Kyoto U.)

プログラムの観測効率化の証明● プログラムの評価ステップが定義できると、証明可能になる● u が t の観測効率化である⟺ あらゆる文脈 C に対して、プログラム C[t] が k ステップで値 v になる
ならば、プログラム C[u] は l ≤ k となる l ステップで同じ値 v になる● 新しいアプローチ：「はしごを登る」● 左足：評価ステップの列を数ステップずつに分割する

評価ステップの定義に立ち入らない● 右足：評価ステップを数ステップずつ比較する
評価ステップの定義
14を解析する

Muroya (RIMS, Kyoto U.)はしごの左足：評価ステップの列の分割● 評価ステップ → の定義には立ち入らない● 模倣 ⇒ を用いて分割する

⇓⇓
⇓

⇓

=

C[t] → → → ⋯⋯ → v （k ステップ）

C[u] → → → ⋯ → v（l ≤ k となる l ステップ）● 定理 [M. ’20] 評価ステップが決定的なとき、上のような模倣が存在するならば

u が t の観測効率化である
15

Muroya (RIMS, Kyoto U.)はしごの左足：評価ステップの列の分割● 評価ステップ → の定義には立ち入らない● 模倣 ⇒ を用いて分割する
kp → → p′⇓⇓lq → q′（l ≤ k）

● 定理 [M. ’20] 評価ステップが決定的なとき、上のような模倣が存在してC[t] ⇒ C[u] ならば￼￼u が t の観測効率化である
16

Muroya (RIMS, Kyoto U.)はしごの左足：評価ステップの列の分割● 評価ステップ → の定義には立ち入らない● 模倣 ⇒ を用いて分割する
kp → → p′⇓⇓lq → q′（l ≤ k）

● 定理 [M. ’20] 評価ステップが決定的なとき、上のような模倣が存在してC[t] ⇒ C[u] ならばどのように構成するか？

￼￼

u が t の観測効率化である
16

Muroya (RIMS, Kyoto U.)はしごの右足：評価ステップの比較● 評価ステップの定義を解析する
kp → → p′⇓⇓lq → q′（l ≤ k）

￼￼

● 評価ステップ → と模倣 ⇒ が上を満たすための条件を求める

17

Muroya (RIMS, Kyoto U.)はしごの右足：評価ステップの比較● 評価ステップの定義を解析する
kp → → p′⇓⇓lq → q′（l ≤ k）

● 評価ステップ → と模倣 ⇒ が上を満たすための条件を求める● →：書き換えルールを評価文脈の中で適用

￼￼● ⇒：書き換えルールをあらゆる文脈の中で適用
18Muroya (RIMS, Kyoto U.)はしごの右足：評価ステップの比較● 評価ステップの定義を解析する
kp → → p′⇓⇓lq → q′（l ≤ k）

● 評価ステップ → と模倣 ⇒ が上を満たすための条件を求める● →：書き換えルールを評価文脈の中で適用

￼￼● ⇒：書き換えルールをあらゆる文脈の中で適用
19

E[n + m] → E[n + m]
C[0 + m] ⇒ C[m]C[n + m] ⇒Muroya
C[m+n](RIMS, Kyoto U.)はしごの右足：評価ステップの比較● 評価ステップの定義を解析する
kp → → p′⇓⇓lq → q′（l ≤ k）

● 評価ステップ → と模倣 ⇒ が上を満たすための条件を求める● →：書き換えルールを評価文脈の中で適用

￼￼● ⇒：書き換えルールをあらゆる文脈の中で適用20E[(λx . t) v] → E[t{v/x}]
C[(λx . t) v] → C[t{v/x}]
C[λx . v x] ⇒ Muroya
C[v](RIMS, Kyoto U.)はしごの右足：評価ステップの比較● 評価ステップの定義を解析する
kp → → p′⇓⇓lq → q′（l ≤ k）● 項評価系 (ℰ, Ectx, ℛ) を用いる

E[(λx . t) v] → E[t{v/x}]
C[(λx . t) v] → C[t{v/x}]
C[λx . v x] ⇒ C[v]● →：書き換えルール ∈ ℰ を評価文脈 ∈ Ectx の中で適用

￼￼● ⇒：書き換えルール ∈ ℛ をあらゆる文脈の中で適用
21

Muroya (RIMS, Kyoto U.)はしごの右足：評価ステップの比較● 評価ステップの定義を解析する
kp → → p′⇓⇓lq → q′（l ≤ k）

E[(λx . t) v] → E[t{v/x}]
C[(λx . t) v] → C[t{v/x}]
C[λx . v x] ⇒ C[v]

● 項評価系 (ℰ, Ectx, ℛ) を用いる

● 定理 [M&H. ’24] 「良い」項評価系において、全ての p, q に対して上が成り立ち￼￼

C[t] ⇒ C[u] ならば、u が t の観測効率化である
22

Muroya (RIMS, Kyoto U.)はしごの右足：評価ステップの比較● 評価ステップの定義を解析するが決定的→•p評価ステップ
k→ → p′•⇓模倣 ⇒⇓が評価結果を保つ

E[(λx . t) v] → E[t{v/x}]l ⇒ が評価文脈 ∈ Ectx を保つ•q模倣（l ≤ k）→ q′C[(λx . t) v] → C[t{v/x}]

C[λx.
vx]
⇒C[v]
書き換えルールが線形である∈ℰ,ℛ•● 項評価系 (ℰ, Ectx, ℛ) を用いる

● 定理 [M&H. ’24] 「良い」項評価系において、全ての ⇐ → 分岐が合流して￼￼

C[t] ⇒ C[u] ならば、u が t の観測効率化である
23

Muroya (RIMS, Kyoto U.)はしごの右足：評価ステップの比較● 評価ステップの定義を解析する
例：

kp → → p′• 値呼びラムダ計算⇓⇓• エフェクトハンドラ (shallow handling)E[(λx . t) v] → E[t{v/x}]l（l ≤ k）
q → q′

C[(λx . t) v] → C[t{v/x}]
C[λx . v x] ⇒ C[v]

● 項評価系 (ℰ, Ectx, ℛ) を用いる

● 定理 [M&H. ’24] 「良い」項評価系において、全ての ⇐ → 分岐が合流して￼￼

C[t] ⇒ C[u] ならば、u が t の観測効率化である
24

Muroya (RIMS, Kyoto U.)

プログラムの観測効率化の証明● プログラムの評価ステップが定義できると、証明可能になる● u が t の観測効率化である⟺ あらゆる文脈 C に対して、プログラム C[t] が k ステップで値 v になる
ならば、プログラム C[u] は l ≤ k となる l ステップで同じ値 v になる● 新しいアプローチ：「はしごを登る」● 左足：評価ステップの列を数ステップずつに分割する● 右足：評価ステップを数ステップずつ比較する

25

Muroya (RIMS, Kyoto U.)はしごを登る● 確率● 非決定性・入出力● 参照・継続● 不停止● 純粋左足：右足：

評価ステップの列の分割評価ステップの比較

26

Muroya (RIMS, Kyoto U.)はしごを登る● 確率● 非決定性・入出力● 参照・継続
● 不停止
● 純粋
左足：

右足：

評価ステップの列の分割

評価ステップの比較

26

Muroya (RIMS, Kyoto U.)はしごを登る● 確率● 非決定性・入出力● 参照・継続
● 不停止
● 純粋
左足：

右足：

評価ステップの列の分割

評価ステップの比較

26

Muroya (RIMS, Kyoto U.)はしごの左足（2歩目）：評価ステップの列の分割● 評価ステップ → の定義には立ち入らない● 模倣 ⇒ を用いて分割する

kM−kp → p′′ →⇓p′⇓lq → q′（l ≤ k）

● 定理 [M&S&U. ’20] 評価ステップが非決定的なとき、上のような模倣が存在してC[t] ⇒ C[u] ならば￼￼￼￼u が t の観測効率化である
27

Muroya (RIMS, Kyoto U.)はしごを登る● 確率● 非決定性・入出力● 参照・継続
● 不停止
● 純粋
左足：

右足：

評価ステップの列の分割

評価ステップの比較

28

Muroya (RIMS, Kyoto U.)はしごを登る● 確率● 非決定性・入出力● 参照・継続
● 不停止
● 純粋
左足：

右足：

評価ステップの列の分割

評価ステップの比較

28

Muroya (RIMS, Kyoto U.)はしごを登る● 確率● 非決定性・入出力● 参照・継続
● 不停止
● 純粋
左足：

右足：

評価ステップの列の分割

評価ステップの比較

28

Muroya (RIMS, Kyoto U.)はしごを登る● 確率● 非決定性・入出力● 参照・継続
● 不停止
● 純粋
左足：

右足：

評価ステップの列の分割

評価ステップの比較

28

Muroya (RIMS, Kyoto U.)はしごを登る● 確率● 非決定性・入出力● 参照・継続
● 不停止
● 純粋
左足：

右足：

評価ステップの列の分割

評価ステップの比較

28

Muroya (RIMS, Kyoto U.)はしごを登る● 確率● 非決定性・入出力● 参照・継続
● 不停止
● 純粋
左足：

右足：

評価ステップの列の分割

評価ステップの比較

28

Muroya (RIMS, Kyoto U.)