📘

[読書メモ] プログラミング Haskell 2ed. 第17章

2024/03/24に公開

Haskell

tech

プログラミング Haskell 2ed. (以下テキストと呼ぶ) 第17章について, 自分なりの理解をメモしたもの.

前回(第16章)

1. 概要

第16章では天下り的に与えられたコンパイラの正しさを構造的帰納法を使って証明した. 第17章では逆に正しさの記述(仕様)からコンパイラを体系的に導く(テキストではソース言語から目標言語への変換と記載されている). 導き方は以下の2通り示されている.

一連の手順を踏んだ変換(スタックの追加, 継続の追加, 高階関数の除去)
正しさの記述から直接導出

このように導出するメリットは以下のとおり.

体系的に導出できる
導出過程から正しさが明らか

2. 文法と意味(ソース言語)

前回のテキスト16.7と同じ.

Data Expr = Val Int | Add Expr Expr

eval :: Expr -> Int
eval (Val n) = n
eval (Add x y) = eval x + eval y

整数の加算のみの言語. 評価関数(あるいはソース言語のコンパイラ) eval により, Expr が通常の整数の加算の式に変形(コンパイル)され, 計算はHaskell環境が行う(つまりHaskell環境が実行器).

以下では, この言語をスタックを使う中間言語(目標言語)にコンパイルするコンパイラと中間言語を実行する実行器を導出する. なお, 中間言語の仕様については特に明示されていないが, 加算だけの言語なので, スタックなしの言語(ソース言語)からスタックありの言語(中間言語(目標言語))へ変換する, くらいのイメージでよいのではないかと思う.

3. 一連の手続きによる導出

ソース言語を徐々に拡張することにより目標言語のコンパイラと実行器を導出する.

3.1 スタックの追加

まず, ソース言語にスタックを導入し, 加算を実行する際のメモリとして利用する. Wikipediaによると, スタックとは「データを後入れ先出し（LIFO: Last In First Out）の構造で保持するもの」である. スタックを導入するということは, データの保存場所としてのスタックを用意するだけでなく, 当然スタックの操作(pushとpopに相当するもの)も実装する必要がある. (ただし, 今の事例では, popについては使う場面が Add に関連する部分のみであることから, Add の処理を考えるときに合わせて考える.)

データの保存場所としてのスタックはリストで表現することにする(これはリストのcons演算子:でLIFOを自然に表現できるので合理的).

type Stack = [Int]

スタックをメモリとして使用する評価関数の改良版 eval' はソース言語 Expr を受け取り, 計算を行い, 結果が格納されたスタックを返す. したがって, Expr -> Stack という型を持つことが予想される. しかし, その場合, Expr を受け取ってから結果を導出するまでの全体を考える必要がある. これでは大変なので, ここではかわりに途中の 1 step だけを考える. すなわち, 処理の途中のある時点の状態が与えられたときに, そこから 1 step 処理を進める関数として eval' を定義する. ある時点では処理途中の Stack と次に処理すべき Expr が与えられ, eval' により処理が実行され, 結果の Stack が返される. したがって eval' は以下の型になる.

eval' :: Expr -> Stack -> Stack

eval' で処理してゆく途中の 1 step を考える. ある式 e を評価する(eval e)と, その結果は整数になり, それは eval' を使った場合には, メモリであるスタックの一番上に格納されるはず(スタックの下部にはそこまでの過程で処理した結果が積まれているはず). したがって, eval' は式 e とスタック s を使って, 以下のような関係を満たすはず.

eval' e s = eval e : s

あとはこの関係を満たすように構造的帰納法を使って eval' の定義を導けばよい(導出についてはテキスト17.3参照).

結果は以下のとおり.

eval' :: Expr -> Stack -> Stack
eval' (Val n) s = push n s
eval' (Add x y) s = add (eval' y (eval' x s))

push :: Int -> Stack -> Stack
push n s = n : s

add :: Stack -> Stack
add (m : n : s) = n+m : s

push と add がスタックを操作するために導入した補助関数である.

eval' は計算途中の 1 step をイメージして導出したものであるが, 引数に与える式 e を与えられた式全体, 初期状態のスタック s を空([])とすれば, 式全体を処理することができる.

例えば, `Add (Add (Val 2) (Val 3)) (Val 4)' は次のように処理される.

eval' (Add (Add (Val 2) (Val 3)) (Val 4)) []
= add (eval' (Val 4) (eval' (Add (Val 2) (Val 3)) []))
= add (push 4 (add (eval' (Val 3) (eval' (Val 2) []))))
= add (push 4 (add (push 3 (push 2 [])))) -- (*)
= [9]

3.2 継続の追加

前節で導入した eval' は, ソース言語を Stack を使って計算する push や add へ変換している. 次のステップとして, これらを明示的に取り出すことを考える. これらの関数はいずれも Stack -> Stack の型をもつので, 式は Stack を処理する関数の列(合成関数)に変換される. ある時点でこれらの関数の列を見れば, それはこの後 'Stack` に対してその後実行される処理を表しており, これは「継続」と解釈できる.

ちなみに wikipedia によると, 継続(continuation)とは「プログラムを実行中のある時点において, 評価されていない残りのプログラム（the rest of the program）を表現するものであり, ... 関数（function）として表現されるもの」(途中一部省略)である.

まずは継続の型を定義する. 継続(およびその構成要素である各関数)は Stack を入力に取り, 式 Expr から変換された処理を行って結果としての Stack を返す. したがって, 以下のような型になる.

type Cont = Stack -> Stack

Cont は継続(continuation)にちなんだ名称であるが, 上の定義の意味での継続を表すだけでなく，それを構成する個々の処理(関数)も同じ型で表していることに注意する.

Expr から Cont に変換する eval'' は Expr を「Stack を操作する関数の列」に変換するものであるから, Expr -> Cont の型を持つように思えるが, Stack を追加した時と同様, 一度に全てを変換するのではなく, 途中の 1 step の変換を考える. すなわち, 次に変換すべき Expr と変換済みの継続 Cont を受け取り, 処理を追加した継続　Cont を返す関数として定義する.

eval'' :: Expr -> Cont -> Cont

この時, eval'' が満たすべき性質は以下のとおり.

eval'' e c s = c (eval' e s)

意味は, 継続 c に e を変換した処理を追加して s　に適用したものは, e を処理した結果をスタックに積んでから c を適用した結果と等しくなるはず, である.

スタックを追加した時と同様, この関係を満たすように構造的帰納法を使って eval'' の定義を導けばよい(導出についてはテキスト17.4参照).

eval'' :: Expr -> Cont -> Cont
eval'' (Val n) c s = c (push n s)
eval'' (add x y) c s = eval'' x (eval'' y (c . add)) s

Val n に対しては, . を逆適用して以下のように書き換えて, s に依存しない形にしておくとよりわかりやすいと思った.

eval'' :: Expr -> Cont -> Cont
eval'' (Val n) c = c . (push n)
eval'' (add x y) c = eval'' x (eval'' y (c . add))

なお, eval' と eval'' の間には id を恒等継続(受け取ったスタックをそのまま返す継続)として, 以下の関係が成立する.

eval' e = eval'' e id

例えば, `Add (Add (Val 2) (Val 3)) (Val 4)' は次のように処理される.

eval' (Add (Add (Val 2) (Val 3)) (Val 4))
= eval'' (Add (Add (Val 2) (Val 3)) (Val 4)) id
= eval'' (Add (Val 2) (Val 3)) (eval'' (Val 4) (id . add))
= eval'' (Add (Val 2) (Val 3)) (id . add . (push 4))
= eval'' (Val 2) (eval'' (Val 3) (id . add . (push 4) . add))
= id . add . (push 4) . add . (push 3) . (push 2)

スタックを操作する関数の列が明示的に取り出せていることに注意(前節の例の(*)部分と同じ内容になってる).

3.3 高階関数の除去

前節で, 継続を導入することによりスタック(メモリ)に対する一連の処理を取り出すことができたが, 継続として取り出された一連の処理は個々の処理(関数 Cont :: Stack -> Stack)を合成した合成関数となっている. 関数であるから, 処理内容を示すだけでなく, 実際の処理(計算)も行ってしまう. そのため, この節ではこれを中間言語(一連の処理の指示書)と実行器(指示に従い実際に処理を実行する部分)に分離する. 具体的には関数である Cont を単なる型 Code に置き換えるとともに, Code を処理する実行器 exec を実装する. exec は基本的に Code を Cont もどすように置き換えれば実装できる. 更に, Cont の中身は push, add であるから最終的に exec は, これらの操作を引き受けて, Code に従ったスタック操作も実装することになる.

まずは Code を定義する. 前節の最後の例をみてもわかるように, 必要なのは id, push, add の3つの関数に対応する型になる.

data Code = HALT | PUSHU Int Code | ADD Code
    deriving Show

これを使って eval', eval'' を書き換える. 書き換えに際して, Cont の場合, 中身は関数である(Cont :: Stack -> Stack)ので, 「先」に実施する処理が「内側」(.の「右側」)になる. 例えば関数 $f_1$ の後, 関数 $f_2$ を実行する場合, $f_2 \circ f_1$ となる. しかし Code の場合, PUSH や ADD の引数の Code は「後」に実施する処理を表す想定なので, 「後」に実施する処理が「内側」になる. したがって, テキストでは「内側」と「外側」を入れ替えるための関数(コンビネーター)を用意し, 書き換えた後で Code への入れ替えを行っている. 書き換え後の関数をそれぞれ comp, comp' とすると, 最終的に以下の関数を得る(導出についてはテキスト17.5参照).

comp :: Expr -> Code
comp e = comp' e HALT

comp' :: Expr -> Code -> Code
comp' (Val n) c = PUSH n c
comp' (Add x y) c = comp' x (comp' y (ADD c))

これを実行するための実行器として exec を以下のように定義する(Code から Cont に変換するときに「内側」と「外側」が入れ替わっていることに注意).

exec :: Code -> Cont
exec HALT = id
exec (PUSH n c) = (exec c) . push n
exec (ADD c) = (exec c) . add

さらに Cont :: Stack -> Stack であったので, 明示的に Stack を使って書き換えると,

exec :: Code -> Stack -> Stack
exec HALT s = s
exec (PUSH n c) s = exec c (n:s)
exec (ADD c) (m : n : s) = exec c (n+m :s)

このように最終的に push や add といった関数は exec の機能に含まれるようになっている.

こまでの書き換えが実際に正しいことは以下の等式を証明することにより確認できる(eval', eval'' の組み合わせが, comp, comp', exec の組み合わせと同じになることを確認する).

exec (comp e) s = eval' e s
exec (comp' e c) s = eval'' e (exec c) s

eval', eval'' は更に変形することができるので, 結局, 以下の等式が得られる(exec c は Stack -> Stack (すなわち Cont) の型を持つことに注意).

exec (comp e) s = eval e : s
exec (comp' e c) s = exec c (eval e : s)

1つ目の式は, 「式 e を中間言語に変換(コンパイル)し, 実行したものは, 式 e を直接スタックに適用した結果に等しくなるはず」, 2つ目は, 「コンパイル済みの c とともに式 e を処理した結果は継続に相当する部分 exec c と式 e をスタックに適用した結果に等しくなるはず」, ということを表している.

3.4 ここまでのまとめ

ここまでの流れをまとめると以下のようになる.

ソース言語(Expr と eval)にスタックを導入し, 同時にスタックを操作する関数 push と add を導入
スタックを操作する関数(push と add)の列を Cont として定義
eval', eval'' により Expr を Cont に変換
Cont に対応する型(中間言語)として Code を定義
comp と comp' により Expr を Code に変換
exec (実行器)により Code を Cont に変換(これで実行可能になる)
「Code を Cont に変換し push と add によりスタック操作」を「Code をもとに exec がスタック操作」に簡略化

これで, Expr, Stack, Code, comp, comp', exec によりソース言語(Expr)を目標言語(Code)に変換し, 実行する体系が得られた.

次節では型と満たすべき式(仕様)から同様の体系をより簡易に導出する.

4. 正しさの記述からの導出

この節では前節までと異なり, 仕様から実装を導く.

4.1 問題設定

問題設定は以下の通り.

ソース言語(Expr)

data Expr = Val Int | ADD Expr Expr
eval :: Expr -> Int
eval (Val n) = n
eval (Add x y) = eval y + eval x

中間言語(Code)
コンパイラに要請される型

comp :: Expr -> Code
comp' :: Expr -> Code -> Code
exec :: Code -> Stack -> Stack
type Stack = [Int]

仕様(満たすべき式)

exec (comp e) s = eval e : s
exec (comp' e c) s = exec c (eval e : s)

(ここで c は後の処理で実行されるべき Code である点に注意.)

これらの条件から Code, comp, comp' を決めていく.

4.2 導出

求めたいのはコンパイラなので, 基本的な考え方は仕様の左辺の comp e や comp' e c を何等かの Code に変換するにはどうしたらよいか, ということである(Code 自体も未定義なので, 都合のいいように定義してゆく). 使えるのはソース言語の定義なので, まず右辺の eval e の部分を変形してゆき, 構造的帰納法で一般的な結論を導くことを考える.

まず, 仕様の2つ目の式について,

基底部(Base case):

exec (comp' (Val n) c) s
= exec c (eval (Val n) : s)
= exec c (n : s)

この結果は「comp' (Val n) c をコンパイルした c' (まだ未定) を実行すると, exec c (n : s) になるべき」ということを意味する. c'は n と cを型引数にとるような何かであるので, それを PUSH n c と定義する. したがって,

comp' (Val n) c = PUSH n c
exec (PUSH n c) s = exec c (n : s)

再帰部(Inductive case):

exec (comp' (Add x y) c) s
= exec c (eval (Add x y) : s)
= exec c (eval x + eval y : s) -- (*)

ここで x と y はどちらも Expr なので,

exec (comp' x c') s = exec c' (eval x : s)
exec (comp' y c') s = exec c' (eval y : s)

上の式の c' に下の式の comp' y c' を代入してみると,

exec (comp' x (comp' y c')) s
= exec (comp' y c') (eval x : s)
= exec c' (eval y : eval x : s)

この c' は, それを評価した結果が exec c (eval x + eval y : s) となるような何かであれば上の再帰部の (*) を再現できる. この何かは型引数 c を取るので, このような c' を ADD c と定義する. すなわち,

exec (comp' x (comp' y (ADD c)) s
= exec (ADD c) (eval y : eval x : s)
= exec c (eval x + eval y : s)

この式を上の再帰部の式と見比べると, 最終的に以下を得る.

comp' (Add x y) c = comp' x (comp' y (ADD c))
exec (ADD c) (m : n : s) = exec c (n + m : s)

次に仕様の1つ目の式について考える. 式を再掲すると,

exec (comp e) s = eval e : s

右辺の形を見ると, 2つ目の式の右辺に出てきたものと似ている. したがって, もし, comp e = comp' e c' となる c' があったとすると,

exec (comp e) s
= exec (comp' e c') s
= exec c' (eval e : s)

であり, もし, c' が exec c' (eval e : s) = eval e : s 満たせば, それが探していた結果である. このような性質を満たす c' を HALT とすると, HALT は以下のように定義される.

comp e = comp' e HALT
exec HALT s = s

以上をまとめると, 以下のようになり, 前節の手順で求めたものと同じものが求められた.

data Code = HALT | PUSH Int Code | ADD Code

comp :: Expr -> Code
comp e = comp' e HALT

comp' :: Expr -> Code -> Code
comp' (Val n) c = PUSH n c
comp' (Add x y) c = comp' x (comp' y (ADD c))

exec :: Code -> Stack -> Stack
exec HALT s = s
exec (PUSH n c) s = exec c (n : s)
exec (ADD c) (m : n : s) = exec c (n+m : s)

5. まとめ

第16章で使用したコンパイラ(と同等なもの)を2通りの方法で導出した.

一つ目の方法はソース言語のロジックを関数の列(継続)として取り出し, それを目的言語に変換しつつ，実行器を作成してゆく方法であった.

一方, 2つ目の方法はソース言語と仕様(満たすべき式)から式変形と構造的帰納法で目的言語と実行器を求める方法である.

2つ目の方法の方が通常のプログラミングの流れに近い気がするが, 式変形と構造的帰納法の助けを借りて, かなり簡略化されているように感じた. また, 出来上がったプログラムにはループもカウンタ変数もなく, データの再帰的な構造(Code とか Stack とか)によりループに相当する部分が処理されていて, 関数型プログラミングの醍醐味を感じられた.

高校の時に数学的帰納法の最初にやる応用問題で「 $n$ 段の階段を1段ずつ, もしくは2段ずつ(1段飛ばし)で登る登り方の数を求めよ」というのがあった. 正面から場合の数を数えようとすると段数が偶数なのか奇数なのかとか1段飛ばしが何回入るかなど, 非常にめんどくさそうなのに, 最初と途中の一歩だけ考えて漸化式を立てると嘘みたいに簡単に解ける, というのを思い出した.

構造的帰納法を活用したプログラミングも最初(基底部)と途中の 1 step (再帰部)だけしっかり考えれば, 途中は再帰的な構造により自動的に処理されるので, 非常に効率的にプログラミングできるんだな, とちょっと感動した.