前回読んだ時と、まったく印象が違う
哲学的な修辞がうっとうしいので、それは読み飛ばしているんですが、「易しい」。こんなに易しかったか? 前回も、
「こんなところで、選択公理使うのかよ」
と思って、今回も、同様に感じたんだけど、さすがに、選択公理勉強しまくったので、今回は、それほど違和感なかったです。
この本の良いところは、Natural Deduction と Sequent Calculus の両方が入っているところ。前回は、Sequent Calculus をかなりうっとうしく感じたんだけど、今回は、
Prolog そのものだよね
で、するする読める。いや、もちろん、理解していたはずなんだけどな。Linear Logic だと、A,A を A に置き換えるとか、A,B を B,A に置き換えるとかが制限されるんだけど、Prolog と考えれば、それも当り前なんだよね。
86年の講義を89年に本したものらしいですが、当時、慶應の講義で Curry Howard 対応を学んだはずだし、Prolog は勉強しまくったので、この本の内容は、ちゃんと頭に入っているはずんだけどなぁ。その割に、新鮮なのは何故だ〜
Cut elimination まで、いけるかどうかは、まだわかりません。学生と読むと良いと思うが、まぁ、どうでも良いか。
選択公理を使うのは、強正規化定理で使う、有限分岐な有限長の枝しかない木は有限(Konig補題)です。有限しか出て来てないが、無限でないってあたりで選択公理が噛んでくるわけね。有限分岐な無限な木は必ず無限長の枝を含むと同等なので、無限集合から無限集合を作る必要が出て来るようです。選択公理が成立しないと、有限分岐な有限長の枝から無限な木が作るれるのか?! 対偶の有限分岐な無限な木なんだが無限長の枝を作れないってのは、選択公理が成立しないなら、そんなものかなという感じ。選択公理が成立しない場合の無限って、なんか、ずいぶん小さな無限だなぁ。有限と無限がうまく切り割れられてない感じ。意外に世界は、そんな構造かも?
No comments:
Post a Comment