Maestumプログラミング、囲碁、読書の話題この広告は、90日以上更新していないブログに表示しています。Haskell第6章は証明について。数学的帰納法による証明を説明し、それを元にfoldl、foldrといった高階関数の性質を証明し、今後は個別の処理について証明するときの論理をfoldlとfoldrの性質を使って簡略化・普遍化する。すべての自然数についての命題を証明するには、すべての自然数が0か、別の自然数の後者(successor)であるP(0)は成立するP(n)が成立するならP(n+1)も成立する最初の項目は前提として、後の二つを証明すればいい。任意の自然数mに対して、P(0)が成立し、そして有限回(m回)P(n)->P(n+1)をしてP(m)が成立する、ということがわかる。nを証明してみる(実はHaskell2010ではこのように書けないが・・・)。nが成立していると仮定する、という帰納法の前提の意である。有限のリスト有限のリストは自然数と似た構造を持っている。すべてのリストは空リスト[]か、他のリストに要素を一つ追加したx:xsという形をしている。P(x:xs)が成立することが証明できれば、任意のリストxsについてP(xs)を証明したことになる。xs上記一行の法則が任意の有限リストに対して成り立つことを証明する。[]とベースは簡単なので省略する。ys)というのは、何が起きているかをちょっと考えれば直感的には正しそうだが、やはり証明する必要がある。Listとは1:2:3:undefinedのような、末尾要素にundefinedを持つリストのこと。listとして任意のxでx:xs」とも定義できる。xsが成り立つと証明する。...とつづくシーケンスの極限だと考えることができる。completeであるという概念が出てくる。completeである。listについても証明できれば無限リストについても証明したことになる。x:xsについてはすでに有限リストで証明済みなので、これで++が有限、Partial、無限リストすべてにおいて結合律を満たすことが証明できた。undefined}undefinedここで満足してしまうと落とし穴にはまる、という点。listがundefinedのみを要素に持つわけではない)。ys)という法則を(証明してから)使ったが、これはysがundefinedの時は成り立たない。undefinedとなるからだ。listの時に使いまわせるか否かは気をつける必要がある。listにおいては成り立たず、そして無限リストにおいても同じく成り立たない。reverseが対合であるのは有限リストが引数の時のみである。)はてなブログをはじめよう!zehnpaardさんは、はてなブログを使っています。ブログを報告するスターをつけました引用をストックしましたストック一覧を見る閉じる引用するにはまずログインしてくださいログイン閉じる引用をストックできませんでした。再度お試しください閉じる限定公開記事のため引用できません。