13.5 リストに対する数学的帰納法 リストも再帰的にオブジェクトが構築される型なので、数学的帰納法で論証できる。 reverse (reverse xs) = xsの証明。 xs = [] の場合 reverse (reverse []) = reverse [] = [] xs = ns のときに reverse (reverse xs) = xs…

ついに最終章！ この最終章では、Haskellプログラミングを論証する方法を紹介する。まず等式推論の復習から始め、それがHaskellにどのように適用できるかを考える。そして、数学的帰納法という重要な技法を説明し、連結演算子を数学的帰納法に似た手法で除去…

12.9 練習問題 以下の式において、簡約可能式はどこか？また、選び出した簡約可能式が、最も内側か、 最も外側か、両方か、いずれでもないかを考えよ。 こんな感じ？簡約可能式に抜け漏れがなければいいけど。 1+(2*3) 2*3...最内 1+()...最外（追記）原著の…

問題文だけ転記。 12.9 練習問題 以下の式において、簡約可能式はどこか？また、選び出した簡約可能式が、最も内側か、 最も外側か、両方か、いずれでもないかを考えよ。 1+(2*3) (1+2)*(2+3) fst (1+2, 2+3) (λx→1+x) (2*3) 式 fst (1+2, 2+3) を評価する際…

12.5 無限のデータ構造 Haskellの遅延評価は、無限のデータ構造を相手にした時も、必要がない限り無限回の評価は行わない。 一般的に、遅延評価は次のような性質を持つ。すなわち、遅延評価を用いると、式が利用される文脈が要求する回数だけしか、その式は…

12.1 導入 一般的な命令型言語は、同じ式に対する評価順序が違うと結果が変わることがあるが、Haskellではどのような順序で評価しても(停止するのでない限り)同じ結果が得られる。 ぐぐってみたら、「チャーチ・ロッサー性」というのかな？ 12.2 評価戦略 簡…