bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

米田の補題 ー 継続渡しのプログラム

6.5 継続渡しのプログラム

1980年代後半に情報科学を学んだ人々にとって、アベルソンとサスマン夫妻が書かれた『計算機プログラムの構造と解釈』は思い出に残る本だったと思う。私も、情報科学の中でどれが最も良い本であったかと問われればこの本をあげる。
f:id:bitterharvest:20180405100542j:plain

この本が出版された当時、ゼミで学生たちに講読させた。しかも、まだ翻訳されていなかったので、原書で読んだ。C言語ぐらいの知識しかない学生たちが、いきなり、Schemeでプログラミングの原理を理解しようと取り組んだため、色々な事件が起きた。ある女子学生は、毎日、クラスとオブジェクトのお化けが夢に出てくると悩まされていた。徹也に次ぐ徹夜で輪講の準備をしてきた学生は、発表の後、トイレで倒れるという事件もあった。英文科を出たお母さんが息子のために翻訳をした文章を大学に行く前に渡してくれる、という麗しい家庭の話もあった。

この本の中で、最も理解しにくかったのは、継続渡しだと思う。米田の補題と結びついていることを知ると、理解しにくかったことに納得できるが、当時のゼミ生の苦労は並大抵ではなかった。この当時の卒業生に会うと、懐かしそうにオブジェクト指向の話をするので、彼らにとっては今では楽しい思い出になっているのであろう。

そこで、継続渡しのプログラムの例をHaskellで少しだけ説明しよう。

米田の補題は、Haskellでは次のように書くことができた。

forall x. (a -> x) -> F x ~= F a

であった。

そこで、\(F\)を恒等射とし、\(x\)を\(r\)で置き換えると、

forall r. (a -> r) -> r ~= a

となる。これと可換図式との対応を示すと下図のようになる。
f:id:bitterharvest:20190527143005p:plain
これは次のように解釈することができる。この式の右側は任意のデータ型\(a\)を取ることを意味する。そして、左側は\(a\)のためのハンドラー\(a \rightarrow r\)を利用する関数であることを示す。さらに、右側は左側で置き換えてもよいことを示している。

この解釈はさらに次のように変えることもできる。ハンドラーは、\(a\)を入力として残りの計算をする関数と見なすことができる。これは次のように考えることが可能になる。

a -> (a -> r) -> r

可換図式との対応を示すと以下のようになる。
f:id:bitterharvest:20190527143028p:plain
それでは、簡単な例から示そう。与えられた数\(a\)に対して、関数\((+3)\)を施し、そして、ハンドラー\(k\)を行うことを考えよう。この関数を\(add3CSP\)としよう。

add3CSP :: (Num a) => a -> (a -> r) -> r
add3CSP a k = k $ (+3) a

可換図式との対応を下図に示す。
f:id:bitterharvest:20190527143045p:plain
いくつか実験してみよう。

Prelude> add3CSP 4 (+5)
12
Prelude> add3CSP 3 (*4)
24
Prelude> add3CSP 6 sqrt
3.0
Prelude> add3CSP (-6) abs
3

それでは、\(+3\)の代わりに階乗としたらどうであろうか。これは少し面倒くさい。

通常、階乗は次のように実装される。

fac :: (Num a, Eq a) => a -> a
fac 0 = 1
fac n = n * fac (n -1)

実行結果も示しておこう。

fac 4
24

継続渡しスタイルでは、実行すべき関数を返す。従って、次のように考える。\(n\)の階乗の計算の後にハンドラー\(k\)を実行する関数は、\(n-1\)の階乗の計算の後に、これに\(n\)を掛けるという計算を行い、その後にハンドラー\(k\)を実行することと同じである。そこで、\((n-1)\)までの階乗の計算結果を\(ret\)で返してもらうことにすると、次のようにプログラムを実装することができる。

facCSP :: (Num a, Eq a) => a -> (a -> r) -> r
facCSP 0 k = k 1
facCSP n k = facCSP (n-1) $ \ret -> k (n * ret)

可換図式との対応を示すと下図になる。
f:id:bitterharvest:20190527143113p:plain
分かりにくいかもしれないが、少し、実行してみよう。

*Main> facCSP 4 (+2)
26
*Main> facCSP 4 (*3)
72
*Main> facCSP 4 sqrt
4.898979485566356

それでは、どのように実行されているのかを見に行くこととしよう。

facCSP 3 k 
= facCSP 2 $ \ret2 -> k (3 * ret2)
= facCSP 1 $ \ret1 -> (\ret2 -> k (3 * ret2)) (2 * ret1)
= facCSP 0 $ \ret0 -> (\ret1 -> (\ret2 -> k (3 * ret2)) (2 * ret1)) (1 * ret0)
= (\ret0 -> (\ret1 -> (\ret2 -> k (3 * ret2)) (2 * ret1)) (1 * ret0)) 1
= (\ret1 -> (\ret2 -> k (3 * ret2)) (2 * ret1)) (1 * 1) 
= (\ret2 -> k (3 * ret2)) (2 * 1)
= k (3 * 2)

上記の式の展開で、それぞれの式は計算をするのに十分な情報を持ち合わせていることに気がつく。そこで、計算を中断したとしても、計算は途中で中断しても、継続して計算ができることが分かる。ユーザインターフェースのプログラムは、センターとユーザとの通信で行われ、中断を伴う。従って、ユーザインターフェースのプログラムでは、継続渡しスタイルのプログラムが使われる。

また、今回は説明を簡単にするために、自然変換に恒等射\(Id = \{Id_A,Id_R\}\)を用いたが、別な射も用いることができる。