2006-07-01 [長年日記]
λ. Re: 超べきとTransitive collapse
わかりやすい解説ありがとうございます。 detailは理解できてませんが、イメージはすごく良くわかります。
解説を読んで、最初は超冪というのは Vκ のように値域がクラスになっているような関数空間のことかと思ったのですが、<URL:http://en.wikipedia.org/wiki/Ultrapower> をみると、ウルトラフィルタによる同値類のことなのですね。
λ. コメントスパム
久しぶりにコメントスパム喰らった。スパマは死ね。
tDiaryをバージョンアップしてスパムフィルタを導入したほうがよいのかなぁ……
【2006-07-06追記】 tDiary 2.1.4 にあげて、とりあえずURLを大量に含むコメントをスパム扱いにした。
λ. 数学の表現の媒体としてのコンピュータ
- <URL:http://homepage3.nifty.com/mogami/diary/d0606.html#26t1>
- <URL:http://homepage3.nifty.com/mogami/diary/d0606.html#29t1>
メモ色々。 (書きかけ)
数学の難しさ
<URL:http://homepage3.nifty.com/mogami/diary/d0606.html#26t2>
「数学を理解する事は難しいと思っている人もいるかも知れないが、難しいのは省略された暗黙の前提や、説明されていない記号法や演繹則を知らないということに過ぎない。」というのは本当にそうなんだろうか。例えば、ベクトルや行列に関する前提・記号法・演繹側を理解すれば線形代数の証明は追えるようになる。しかし、いくら証明を追えたとしても例えば『プログラミングのための線形代数』で解説されているようなイメージを持てなければ線形代数を理解したとは言えないように思える。また、そのようなイメージを持つまでの過程において、記号法や演繹則を理解することがそれほど大きな割合を占めているとは思えない。そもそも数学を理解するということはどういうことだろう？
それから、「上記のようなシステムによって全ての細部を記述できるようになれば、数学の証明を理解する事は将棋の棋譜から対局を再現するのと同じ程度に易しいことになるだろう。」というのには同意できない。将棋の棋譜はシーケンシャルなものなのに対して、数学の証明はより複雑な構造を持っている。形式的証明に似ているのは計算機のプログラムで、プログラムには全ての細部が記述されているが、複雑なプログラムを理解するのは将棋の棋譜から対局を再現することよりもはるかに難しい。
定理証明系
既に指摘があるが、CoqやAgdaのような定理証明系は「人間が能動的に証明する。機械は正しく無いまたは不明な部分を消極的に指摘する」という考えに基づいてはいると思う。Tactics等によってある程度自動的に証明を探索することは出来るが、あくまで人間が証明することの補助に過ぎないと思うし。
シンデレラ
ところで、平面幾何ソフト「シンデレラ」というものもあり、こいつの上で平面幾何を考えるのは結構快適。こいつは記号論理に基づいた検証ではなく、自由に動かせる要素をランダムに動かしてテストすることを繰り返すことによって検証を行っている。検証方法はQuickCheckみたいなもんだな。
