Thinking Functionally with Haskell勉強メモ: 第６章１ 数学的帰納法による証明

第６章は証明について。まずは数学的帰納法による証明を説明し、それを元にfoldl、foldrといった高階関数の性質を証明し、今後は個別の処理について証明するときの論理をfoldlとfoldrの性質を使って簡略化・普遍化する。

今回は数学的帰納法の話。

自然数

数学的帰納法ですべての自然数についての命題を証明するには、

• すべての自然数が0か、別の自然数の後者（successor）である
• P(0)は成立する
• P(n)が成立するならP(n+1)も成立する

最初の項目は前提として、後の二つを証明すればいい。任意の自然数mに対して、P(0)が成立し、そして有限回（m回）P(n)->P(n+1)をしてP(m)が成立する、ということがわかる。

Haskellで累乗の定義：

exp :: Num a => a -> Int -> a
exp x 0      = 1
exp x (n+1) = x * exp x n

と数学的帰納法を使ってexp x (m+n) = exp x m * exp x nを証明してみる（実はHaskell2010ではこのように書けないが・・・）。

Case 0 左辺

exp x (0 + n)

= {0+a = a}
exp x n

Case 0 右辺

exp x 0 * exp x n

= {exp x 0 = 1}
1 * exp x n

= {1 * a = a}
exp x n

Case m+1 左辺

exp x (m+1+n)

= {exp a (b+1) = a * exp a b}
x * exp x (m + n)

= {induction}
x * exp x m * exp x n

Case m+1 右辺

exp x (m+1) * exp x n

= {exp a (b+1) = a * exp a b}
x * exp x m * exp x n

inductionとは、Case m+1についての証明では、exp x (m+n) = exp x m * exp x nが成立していると仮定する、という帰納法の前提の意である。 というわけでcase 0とcase m+1で右辺と左辺が等価であることが証明できたので、すべての自然数mにおいてexp x (m+n) = exp x m * exp x nが証明できた。

有限のリスト

有限のリストは自然数と似た構造を持っている。すべてのリストは空リスト[]か、他のリストに要素を一つ追加したx:xsという形をしている。

なのでP([])を証明でき、任意のxについてP(xs) -> P(x:xs)が成立することが証明できれば、任意のリストxsについてP(xs)を証明したことになる。

例えば

[] ++ ys = ys
(x:xs) ++ ys = x:(xs ++ ys)

の二つの規則を使って++が結合律を満たす、つまり(xs ++ ys) ++ zs = xs ++ (ys ++ zs)が成立することを証明してみる；

Case [] 左辺

([] ++ ys) ++ zs

= {[] ++ ys = ys}
ys ++ zs

Case [] 右辺

[] ++ (ys ++ zs)

= {[] ++ ys = ys}
ys ++ zs

Case x:xs 左辺

((x:xs) ++ ys) ++ zs

= {(x:xs) ++ ys = x:(xs ++ ys)}
(x:(xs ++ ys)) ++ zs

= {(x:xs) ++ ys = x:(xs ++ ys)}
x:((xs ++ ys) ++ zs)

Case x:xs 右辺

(x:xs) ++ (ys ++ zs)

={(x:xs) ++ ys = x:(xs ++ ys)}
x:(xs ++ (ys ++ zs))

= {induction}
x:((xs ++ ys) ++ zs)

次は以下二行の定義を使って

reverse [] = []
reverse (x:xs) = reverse xs ++ [x]

reverse (reverse xs) = xs

上記一行の法則が任意の有限リストに対して成り立つことを証明する。

reverse (reverse xs)

= reverse []

= []

とベースは簡単なので省略する。

Case x:xs

reverse (reverse x:xs)

= {reverse (x:xs) = reverse xs ++ [x]}
reverse (reverse xs ++ [x])

= {これから証明する命題}
x: (reverse (reverse xs))

= {induction}
x:xs

reverse (ys ++ [y]) = y: (reverse ys)というのは、何が起きているかをちょっと考えれば直感的には正しそうだが、やはり証明する必要がある。

Case [] 左辺

reverse ([] ++ [y])

= {reverse [] = []}
reverse ([] ++ [y])

= {[] ++ xs = xs}
reverse [y]

= {reverse (x:xs) = reverse xs ++ [x]}
reverse [] ++ [y]

= {reverse [] = []}
[] ++ [y]

= {[] ++ xs = xs}
[y]

Case [] 右辺

y : (reverse (reverse []))

= {reverse [] = []}
y : (reverse [])

= {reverse [] = []}
y : []

= {x:[] = [x]}
[y]

Case z:zs 左辺

reverse ((z:zs) ++ [y])

= {(x:xs) ++ ys = x:(xs ++ ys)}
reverse (z : (zs ++ [y]))

= {reverse x:xs = reverse xs ++ [x]}
reverse (zs ++ [y]) ++ [z]

= {induction}
(y: reverse zs) ++ [z]

Case z:zs 右辺

y : (reverse z:zs)

= {reverse x:xs = reverse xs ++ [x]}
y : (reverse zs ++ [z])

= {x:xs ++ ys = x : (xs ++ ys)}
(y : reverse zs) ++ [z]

で証明終わり。

Partial List

Partial Listとは

1:2:3:undefined

のような、末尾要素にundefinedを持つリストのこと。日本語だとなんだろうか？

自然数のように、「undefinedか、xsがpartial listとして任意のxでx:xs」とも定義できる。

これを使って数学的帰納法でpartial list xsと任意のリストysにおいて

xs ++ ys = xs

が成り立つと証明する。

case undefined

undefined ++ ys

= {undefined ++ xs = undefined}
undefined

case x:xs

(x:xs) ++ ys

= {(x:xs) ++ ys = x : (xs ++ ys)}
x : (xs ++ ys)

= {induction}
x : xs

無限リスト

無限リストは第９章のメインテーマなので詳細な説明は省かれているが、基本的に無限リストは

undefined, a:undefined, a:b:undefined, a:b:c:undefined ...

とつづくシーケンスの極限だと考えることができる。（[], a:[], ...じゃだめなのか？だめかも、と直感的に思うが、そのへんも詳しく第９章にでているのだろうか）

ここである属性Pがchain completeであるという概念が出てくる。

もしが上記のようなPartial listのシーケンスで、その極限がxsだとしたら、もし任意のnにおいてが成り立つのならも成り立つ、という場合、Pはchain completeである。

例としては

• すべての変数が全称量化されているHaskell式e1、e2を使った等式 e1 = e2
• PとQがchain completeだとして、その論理積P∧Q

（逆に不等号式や存在量化を含む式などはchain completeとはならない）

たとえば

(xs ++ ys) ++ zs = xs ++ (ys ++ zs)

これは変数が全称量化されている等式なので、先ほどの有限リストについての証明に加えてpartial listについても証明できれば無限リストについても証明したことになる。

Case undefined 左辺

(undefined ++ ys) ++ zs
= {undefined ++ xs - undefined}
undefined ++ zs

= {undefined ++ xs - undefined}
undefined

Case undefined 右辺

undefined ++ (ys ++ zs)

= {undefined ++ xs - undefined}
undefined

Case x:xsについてはすでに有限リストで証明済みなので、これで++が有限、Partial、無限リストすべてにおいて結合律を満たすことが証明できた。

気をつけないといけないポイントとしては、例えばreverse (reverse xs) = xsを証明しようとして

Case undefined

reverse (reverse undefined)

= {reverse undefined = undefined}
reverse undefined

= {reverse undefined = undefined}
undefined

ここで満足してしまうと落とし穴にはまる、という点。

なぜならpartial listに関しては

reverse (reverse xs) = undefined

なので、reverse (reverse xs) = xsは成り立たない（すべてのpartial listがundefinedのみを要素に持つわけではない）。

有限リストの時はreverse (reverse x:xs) = x:xsを証明するときにreverse (ys ++ [y]) = y: (reverse ys)という法則を（証明してから）使ったが、これはysがundefinedの時は成り立たない。

reverse (undefined ++ [y])
= reverse undefined
= undefined

y: (reverse ys)
= y: undefined

となるからだ。このように、有限リストの時のcase x:xsの証明がpartial listの時に使いまわせるか否かは気をつける必要がある。

この場合は使い回せず、実際reverse (reverse xs) = xsはpartial listにおいては成り立たず、そして無限リストにおいても同じく成り立たない。reverseが対合であるのは有限リストが引数の時のみである。