こんにちは､びしょ〜じょです｡これはWORD Advent Calendar 2017の記事です｡
12月23日といえば今上天皇の誕生日!!!! みんなで祝いましょう｡
この日はめでたいなぁ､国民の祝日にしましょう｡
!!!以下に詳細が!!!
ア〜
時は2016年の頭､我らがWORD部員である(当時)M2のN氏｡
就職先は地球防衛軍日本支部であるところの陸軍自衛隊であることを発表した｡
毎日角ふじ1へ行き毎日早起き筋トレをおこなうと告げ､可能な限り実行していた｡
そんなEDF隊員見習いの姿勢に俺達は感化された……!
時は2016年の頭､テレビアニメ『ヴァルキリードライヴ マーメイド』2が放映されていた｡
激しいバトル､島やウイルスの謎､そしてちょっとエッチなサービスシーン､百合……｡
そんな中､武器を持たずに己が身一つで戦う"ゼロ･アーム"の異名を持つ魅力的なキャラクター､ 時雨霞 さん｡
パートナーの見城ひびきさんを想いながら強く戦い続ける姿勢に俺(達)は感化された……!
感化されすぎて2016年4月に髪型を時雨霞さんにした……!!!
一切の運動を放棄して棒に脂と皮が張り付いたような四肢の俺達ベルトコンベアーの理系BOYがダンベルを持ち上げようものなら肩が脱臼してしまう｡
まずは自重を使ったトレーニングから開始してダンベルプルーフな身体をビルドしなければならない｡
EDF5を夜通しやってたら24日になっちゃった
ここから別の記事
皆さんは例外処理のあるlambda calculusをCPS変換するとき､全てのコントロールエフェクトもCPSで済ませたいがために例外処理もCPS変換したくなるでしょう｡
以下のような言語を考える｡
\[
\begin{array}{rrl}
e & ::= & x\mid \lambda x.e \mid e\,e\\\\
& \mid & e\,\mathbf{handle}\,\overrightarrow{\mathit{Exn}\left(x\right)\rightarrow e}\\\\
& \mid & \mathbf{raise}\,\mathit{Exn}\left(e\right)
\end{array}
\]
\(e\,\mathbf{handle}\,\overrightarrow{\mathit{Exn}(x)\rightarrow e'}\)は実質\(\mathbf{try}\,e\,\mathbf{with}\,\overrightarrow{\mathit{Exn}(x)\rightarrow e'}\)ですね｡
操作的意味論は君の中に既にあるはずだ｡
既存の手法としてDouble-Barreled CPSというものが知られています3｡
継続ともう一つ例外処理に対応する関数､つまりdouble-barreledなCPSを作ります｡
\[
\begin{array}{c}
\fbox{\lceil e\rceil = e_{cps}}\\\\
\begin{array}{rcl}
\lceil \lambda x. e \rceil & = & \lambda k. \lambda h. \lambda x. \lambda k'. \lambda h'. \lceil e \rceil\, k'\, h'\\\\
\lceil x \rceil & = & \lambda k. \lambda h. k\, x\\\\
\lceil e_1\, e_2\rceil & = & \lambda k. \lambda h. \lceil e_1\rceil\,\left(\lambda f. \lceil e_2\rceil \left(\lambda a. f\,a\,k\,h\right)\,h\right)\,h\\\\
\lceil e_1\,\mathbf{handle}\,\mathit{Exn}\left(x\right)\rightarrow e_2\rceil & = & \lambda k. \lambda h. \lceil e_1\rceil\, k\, \left(\lambda x. \lceil e_2\rceil\, k\,h\right) \\\\
\lceil \mathbf{raise}\,\mathit{Exn}\left(e\right)\rceil & = & \lambda k.\lambda h.\lceil e\rceil \,h\,h\\\\
\end{array}
\end{array}
\]
\(e_{cps}\)は\(e\)のサブセットっぽいのでなんだかいい感じですね｡
例外ハンドラのアーム(\(Exn(x)\rightarrow e\))を継続として(\(\lambda x.\lceil e\rceil\)) 第2の継続パラメータに渡すわけですな｡
お察しの通り､この手法では1つの例外処理に対して1つの継続を追加している｡
では複数の例外処理に対して我々はどうする? まさかn+1-barreled CPS? いやいやそれはちょっと……｡
ハンドラを貯めて逐次ぶっ放すような感じにしていくか｡
\(h\)を(例外名とハンドラ関数のペア)のリストとして､初期値を空リストとして与える｡
\[
\begin{array}{rcl}
\lceil \lambda x.e\rceil_h & = & \lambda k. \lambda x.\lambda k'. \lceil e\rceil_h\, k'\\\\
\lceil x\rceil_h & = & \lambda k. k\,x\\\\
\lceil e_1\,e_2\rceil_h & = & \lambda k.\lceil e_1\rceil_h \left(\lambda f.\lceil e_2\rceil \left(\lambda a. f\,a\,k\right)\right)\\\\
\left\lceil e\,\mathbf{handle}\,\overrightarrow{\mathit{Exn}\left(x\right)\rightarrow e'} \right\rceil_h & = & \lambda k.\lceil e\rceil_{h'}\,k\ %
\mathit{where}\ h' = \overrightarrow{\left(Exn,\lambda k'.\lambda x.\lceil e'\rceil\,k'\right)}\, @\, h\\\\
%
\left\lceil \mathbf{raise}\,\mathit{Exn}\left(e\right) \right\rceil_h & = &\left(%
\begin{array}{ll}
\lambda k.\lceil e\rceil_h f_\mathit{Exn} & \mathrm{if}\,h=h'\,@\,\left(\left(\mathit{Exn}, f_\mathit{Exn}\right) :: \mathit{tl}\right)\\\\
\mathrm{undefined} & \mathit{otherwise}
\end{array}\right.
\end{array}
\]
オッ? いい感じな気もするが……｡
\(\lambda\)抽象を変換したあと､その関数を使うというときに困りそうです｡
次のようなケースを考えてみる｡
\[
\begin{array}{rcl}
\begin{array}{l}
\mathbf{let}\,f\,x=\mathbf{raise}\,\mathit{Exn}\left(x\right)\,\mathbf{in}\\\\
f\,m\,\mathbf{handle}\,\mathit{Exn}\left(x\right)\rightarrow x
\end{array} &=&%
\left(\lambda f. f\,m\,\mathbf{handle}\,\mathit{Exn}\left(x\right)\rightarrow x\right)\,%
\left(\lambda x.\mathbf{raise}\,\mathit{Exn}\left(x\right)\right)
\end{array}
\]
関数fの中でraiseしとります｡
9.1で変換するとどうなるか……?
どうなるかというと､引数である\(\lambda\)の中のraiseをちゃんとハンドルできないので爆発します｡
これはなぜか｡
9.1では\(\lambda\)抽象を作る際のハンドラはそのコンテキストで生まれたハンドラを使ってしまっているので､
外側のコンテキストである関数内のhandleが作るハンドラ群を使えないのである｡
ハンドラをダイナミックにばらまくので､記述言語だけで回していくには厳しい｡
のでCPS termを拡張したい｡
\[
\begin{array}{rrl}
e_{cps} & ::= & x \mid \lambda x. e_{cps} \mid e_{cps}\, e_{cps}\\\\
& \mid& \left[\right] \\\\
& \mid& e_{cps} :: e_{cps} \mid e_{cps} @ e_{cps} \\\\
& \mid& \left(\mathit{Exn}, e_{cps} \right)\\\\
& \mid& \mathbf{lookup}(\mathit{Exn}, e_{cps})\\\\
\end{array}
\]
はい
\[
\begin{array}{c}
\fbox{\lceil e\rceil=e_{cps}}\\\\
\begin{array}{rcl}
\lceil \lambda x.e\rceil & = &%
\lambda k. \lambda h. \lambda x.\lambda k'. \lambda h'. \lceil e\rceil\, k'\, h'\\\\
\lceil x\rceil & = & \lambda k. \lambda h. k\,x\\\\
\lceil e_1\,e_2\rceil & = &%
\lambda k. \lambda h. \lceil e_1\rceil \left(\lambda f.\lceil e_2\rceil \left(\lambda a. f\,a\,k\,h\right)\, h\right)\, h\\\\
\left\lceil e\,\mathbf{handle}\,\overrightarrow{\mathit{Exn}\left(x\right)\rightarrow e'} \right\rceil & = &%
\lambda k.\lambda h. \lceil e\rceil\,k\, \left(\overrightarrow{\left(\mathit{Exn},\lambda k'.\lambda h'. \lceil e' \rceil\, k'\,h'\right)} \,@\, h\right)\\\\
\left\lceil \mathbf{raise}\,\mathit{Exn}\left(e\right) \right\rceil & = & \lambda k.\lambda h. \left(\lambda f_\mathit{Exn}. \lceil e \rceil\, f_\mathit{Exn}\,f_\mathit{Exn} \right) \mathbf{lookup}\left(\mathit{Exn},h\right)
\end{array}
\end{array}
\]
先程の例を変換してみましょう｡
\[
\begin{array}{rcl}
\lceil e\rceil & = & \lambda k. \lambda h. \left\lceil \lambda f. f\,m\,\mathbf{handle}\,\mathit{Exn}\left(x\right)\rightarrow x \right\rceil%
\left(\lambda f. \left\lceil \lambda x.\mathbf{raise}\,\mathit{Exn}\left(x\right) \right\rceil \left( \lambda a. f\,a\,k\,h\right)\,h\right)\,h\\\\
&=& \lambda k.\lambda h. \left(\lambda k_0.\lambda h_0. \lambda f. \lambda k_0'. \lambda h_0'. \left(\left(\lambda k_2.\lambda h_2. \left(\lambda k_3.\lambda h_3. k_3\,f\right) \left(\lambda f'. \left(\lambda k_4.\lambda h_4. k_4\,m\right) \left(\lambda m'. f'\,m'\,k_2\,h_2 \right)\,h_2 \right)\,h_2\right)\, k_1\, \left(\left(\mathit{Exn}, \lambda k_5.\lambda h_5.\lambda x. \lambda k_6. \lambda h_6. k_6\,x\right) \,::\, h_1\right)\right) \, k_0'\,h_0'\right) \left(\lambda f. (\lambda k_7. \lambda h_7. \lambda x. \lambda k_7'. \lambda h_7'. \left(\lambda k_8. \lambda h_8. \left(\lambda f_\mathit{Exn}. \left(\lambda k_9. \lambda h_9. k_9 x\right) f_\mathit{Exn} f_\mathit{Exn}\right) \mathbf{lookup}\left(\mathit{Exn}, h_8\right)\right) k_7'\,h_7')\, \left(\lambda a. f\,a\,k\,h\right)\, h \right)\,h
\end{array}
\]
こんなもんですか? あとは作者の気持ちに沿ってrunしていくと
\[
\mathit{run}\, \lceil e\rceil = \lceil e\rceil \left(\lambda k. k\right) [] = \cdots \cdots
\]
あ〜〜やりたくない､これは読者の皆さんへの課題としますが､多分いい感じにハンドラが動くんでしょう｡
素晴らしいことに変換規則が間違ってますね｡
次のような感じだと正解だろうか｡
\[
\begin{array}{rcl}
\lceil \lambda x.e\rceil & =&%
\lambda k. \lambda h. k \left(\lambda x.\lambda k'. \lambda h'. \lceil e\rceil\, k'\, h'\right)\\\\
\lceil x\rceil & = & \lambda k. \lambda h. k\,x\\\\
\lceil e_1\,e_2\rceil & = &%
\lambda k. \lambda h. \lceil e_1\rceil \left(\lambda f.\lceil e_2\rceil \left(\lambda a. f\,a\,k\,h\right)\, h\right)\, h\\\\
\lceil e\,\mathbf{handle}\,\overrightarrow{\mathit{Exn}\left(x\right)\rightarrow e'} \rceil & = &%
\lambda k.\lambda h. \lceil e\rceil\,k\, \left(\overrightarrow{\left(\mathit{Exn},\lambda x. \lceil e' \rceil\, k\,h\right)} \,@\, h\right) \ \\\\
\lceil \mathbf{raise}\,\mathit{Exn}\left(e\right) \rceil & =& \lambda k.\lambda h. \lceil e\rceil \left(\lambda v. \left(\mathbf{lookup}\left(\mathit{Exn}, h\right)\right)\, v\right)\, h
\end{array}
\]
正しさを検証するのは皆さんへの宿題とします｡
かんたんな実装を載せますんで後は頼んだ｡
という話を明日研究室のゼミで話すかもしれない｡
