[読書メモ] プログラミング Haskell 2ed. 第16章
プログラミング Haskell 2ed. (以下テキストと呼ぶ, ページ数は日本語版のページ数) 第16章 について, 自分なりの理解をメモしたもの.
1. プログラミング Haskell 2ed. について
数ある Haskell の入門書の中で個人的に一番お気に入りの本. C言語における「プログラミング言語C」(カーニハン, リッチー), Python における「Python言語によるプログラミングイントロダクション」(グッターグ) みたいな印象を受ける構成になっている. 説明は簡潔ですっきりしていて読みやすいがその分自分である程度考え, サンプルコードを写経しながら読み進む必要がある. また, 言語の解説だけでなく, (関数型)プログラミング自体に対する示唆にも富んでいて, 関数がファーストクラスオブジェクトになっただけでこんなに表現力が上がる(頭の使い方が変わる)のか, と感じた.
Haskell 等の関数型プログラミングを勉強しだすと, とかくモナドとか圏論とかに心を奪われがちになるが, この本を読むと,「モナドとか圏論について悩む前に関数型プログラミングに精通すべき!」という気持ちになる(どこにも書いてないです, あくまで個人の感想です). オススメです!
2. 構造的帰納法
特に定義もなく説明されており, それでも内容は理解できるが, 一応 Wikipedia の定義を転載すると以下のとおり.
「構造的帰納法は, (リストや木構造のように)再帰的に定義された構造のある種の x に関する全称命題 ∀x. P(x) を証明する手法である.」
イメージとしては, 高校で習う数学的帰納法をプログラミングに適用したような感じ. 数学的帰納法では数列(漸化式)を対象にして命題を証明したが, 構造的帰納法では数列(漸化式)の代わりに再帰的なデータ構造を用いる.
以下, テキストで少しわかりにくかった部分を抜粋(++ 演算子は2項演算子で2つのリストを引数に取り, Nodeは2つのツリーを引数に取るので, 一見似ているが, 帰納法の適用は大分違う).
2.1 リストを使った例: reverse の分配法則
(テキスト p.236)
命題:
reverse (xs ++ ys) = reverse ys ++ reverse xs
[証明]
基底部(Base case):
まず, xs ++ ys = [] ++ ys の時, 命題が成立することを示す.
reverse ([] ++ ys)
= reverse ys -- [] ++ はなくても同じ
= reverse ys ++ [] -- ++ [] は追加しても同じ
= reverse ys ++ reverse [] -- [] は reverse しても同じ
再帰部(Inductive case):
次に, xs ++ ys について命題が成立するとき x:xs ++ ys について命題が成立することを示す.
reverse (x:xs ++ ys)
= reverse (x : (xs ++ ys)) -- ++ 演算子の性質
= reverse (xs ++ ys) ++ [x] -- reverse の定義
= reverse ys ++ reverse xs ++ [x] -- 仮定より
= reverse ys ++ reverse (x:xs) -- reverse の定義
以上より reverse に対して命題が成立することが示せた. □
ここで, なぜ xs についてだけ証明すればよいかというと, ++ 演算子が任意の ys に対して, 「xs の再帰により再帰的に定義されている」から. ちなみに ++ 演算子の定義は以下のとおり(テキスト p.64).
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)
つまり, xs ++ ys が全体として「再帰的に定義された構造」なので，その基底部と再帰部について証明すればよい, ということ(だと思う).
2.2 ツリーを使った例: Tree型に対する関手則
(テキスト p.237, p.248 練習問題8 の一部)
命題:
ツリー
Data Tree = Leaf Int | Node Tree Tree
Instance Functor Tree where
-- fmap :: (a -> b) -> Tree a -> Tree b
fmap g (Leaf x) = Leaf (g x)
fmap g (Node l r) = Node (fmap g l) (fmap g r)
に対し,
fmap (g . h) = fmap g . fmap h
が成立する.
[証明]
基底部(Base case):
まず, Leaf x に対して, 命題が成立することを示す.
fmap (g . h) (Leaf x)
= Leaf ((g . h) x) -- fmap を適用
= Leaf (g (h x)) -- . 逆を適用
= fmap g (Leaf (h x)) -- g に fmap を逆適用
= fmap g (fmap h (Leaf x)) -- h に fmap を逆適用
= (fmap g . fmap h) (Leaf x) -- fmap g と fmap h に . を適用
再帰部(Inductive case):
次に l, r について命題が成立するとき, Node l r に対して命題が成立することを示す.
fmap (g . h) (Node l r)
= Node (fmap (g . h) l) (fmap (g . h) r) -- fmap を適用
= Node ((fmap g . fmap h) l) ((fmap g . fmap h) r) -- l, r に対する仮定を適用
= Node (fmap g (fmap h l)) (fmap g (fmap h r)) -- . を逆適用
= fmap g (Node (fmap h l) (fmap h r)) -- fmap を逆適用
= fmap g (fmap h (Node l r)) -- fmap を逆適用
= (fmap g . fmap h) (Node l r) -- fmap g と fmap h に . を適用
以上より Tree に対して命題が成立することが示せた. □
ツリーも再帰的に定義された構造であるため, 構造的帰納法を適用できる. ツリーの場合は手前の枝両方とも途中の式変形に使用するので, 両方の枝に対して命題の成立を仮定する必要がある. 数学的帰納法でも直前の
3. コンパイラの正しさ
(テキスト p.242 16.7)
ここではやや天下り的にコンパイラが与えられ, そのコンパイラ(およびその改良版)の正確性を構造的帰納法で証明している.
コンパイラ自体の導出については次章(第17章)で議論される.
3.1 言語(文法と意味)
この節(および次章)では以下で定義されるような, 整数と加算からなる言語を考える.
文法:
data Expr = Val Int | Add Expr Expr
この言語の解釈は以下のとおり.
意味:
eval :: Expr -> Int
eval (Val n) = n
eval (Add x y) = eval x + eval y
例えば, Add (Add (Val 2) (Val 3)) (Val 4) は (2+3)+4 と解釈される. つまり, eval は, 文法に従った式を Haskell がそのまま実行可能な式に翻訳(コンパイル)する, と解釈できる. この場合の実行器に相当するのが Haskell の実行環境そのものとなる(と思う).
以下ではこの定義は所与として議論が進む.
3.2 コンパイラ
Expr と eval だけでも計算は可能であるが, この節ではさらに以下の要素を加えたコンパイラのシステムを考える(あくまで例示のための拡張であり, 今考えている文法に対しては, 拡張の必然性はない(と思う)).
- 計算の途中結果を保存する(
Stack) - 式を中間言語(演算子
OpのリストCode)に変換するコンパイラ(comp,comp') - 中間言語を実行し, 結果を計算する実行器(
exec)
具体的には以下のとおり.
type Stack = [Int]
type Code = [Op]
data Op = PUSH Int | ADD
comp :: Expr -> Code
comp (Val n) = [PUSH n]
comp (Add x y) = comp x ++ comp y ++ [ADD]
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 [] s = s
exec (PUSH n : c) s = exec c (n : s)
exec (Add : c) (m : n : s) = exec c (n+m : s)
comp は式を解釈して, スタックに対する操作(Op)を順番に配列(Code) に格納してゆく. exec は Code に従い, スタックを操作しながら式の値をセットしたり, 計算結果を格納したりしてゆく.
(ここで, comp' は comp' e c = comp e ++ cを満たすように定義されたもので(以下の 3.4 を参照), 特に comp e = comp' e [] である.)
Expr が与えられると, comp' もしくは comp により中間言語に変換され, exec により計算が実行される.
例えば, 式 Add (Add (Val 2) (Val 3)) (Val 4) は
[PUSH 2, PUSH 3, ADD, PUSH 4, ADD]
にコンパイルされ実行される. また, exec により実行時のスタックは以下のように推移してゆく.
[]
(PUSH 2) -> [2]
(PUSH 3) -> [3,2]
(ADD) -> [5]
(PUSH 4) -> [4,5]
(ADD) -> [9]
3.3 コンパイラの正しさの確認
上で与えらたコンパイラが正しいかどうかを確認するため, コンパイラが満たすべき性質を特定し, 実際にその性質が満たされていることを確認する.
もともと Expr と eval だけで結果を計算できることから, コンパイラの計算結果がこれと等しければ, コンパイラが正しい, と言える. つまり, 以下の関係が成立してなければならない.
exec (comp e) [] = [eval e]
ここで, 空のスタック [] を, 任意のスタック s に拡張(最初からスタックに何か積んであってもよい)しても一般性は失われない.
exec (comp e) s = eval e : s
更に一般化するため, comp を comp'に書き換える.
exec (comp' e []) s = eval e : s
空のコード部分に任意のコード c を導入(現在の式の計算の後, さらに別の計算が残っていてもよい)し, 最終的に以下の関係式を得る.
exec (comp' e c) s = exec c (eval e : s)
ここで, comp' の性質 comp' e c = comp e ++ c (以下の 3.4 参照)と, exec の分配法則 exec (comp e ++ c) s = exec c (exec (comp e) s) (証明はテキスト p.244)を使った.
以上より, コンパイラが満たすべき性質は以下のように書ける.
性質:
exec (comp' e c) s = exec c (eval e : s)
これは「式 e をコンパイルして, 任意のコード c とともに実行した結果は, 式 e の評価結果を一番上に置いたスタックに対してその任意のコード c を実行した結果と等しい.」ということを表している.
テキストでは実際にこの性質が満たされていることが証明されている.
3.4 comp' の導出(練習問題11)
comp' は comp' e c = comp e ++ c を満たすように決められる. 具体的には基底部と再帰部に分けて comp e の定義を使って式変形していく.
基底部(Base case):
comp' (Val n) e
= comp (Val n) ++ c
= [PUSH n] ++ c -- comp を適用
= PUSH n : c -- ++ を簡約
再帰部(Inductive case):
comp' (add x y) e
= comp (add x y) ++ c
= comp x ++ comp y ++ [ADD] ++ c -- comp を適用
= comp x ++ comp y ++ (ADD : c) -- 最後の ++ を簡約
= comp' x (comp y ++ (ADD : c)) -- comp x に条件を適用
= comp' x (comp' y (ADD : c)) -- comp y に条件を適用
したがって, 前節に記載した comp' の定義が導かれた. □
4. まとめ
構造的帰納法を用いることにより, プログラムの正確性や, 満たすべき性質について, 一般的な形で証明することができる. 実際にプログラムやテストを実行せずに一定の正確性や特徴を担保できる, というのは素晴らしい.
Discussion