溜る & HOL

早めにぽしゃった仕事のために、昨日は暇でした。なんだが、それを理由にさぼっていた仕事が溜っているらしい。でも、今日も、それには手を付けないつもり。どれも月曜日で良いらしいので。(おぃおぃ...)

査読の仕事もあったはずだが、どこから引き受けたか、もはや覚えてないです。どうでもいい論文だと思ったが、引用している論文のチェックが面倒。どれも古いがだいじょうぶか? とか思う。確か、down load できるものは全部落したはず。有料のがいくつかあった。儲けすぎなんだよ。この手のものも予算から落せると良いのだが... 落せるとは思えず。まぁ、先生を貧乏にさせる陰謀なんでしょう。

Mac OS X 10.4 で、HOLを Moscow ML で動かす時に、BDD library が symbol を解決できないのは、やっぱり、strip しているせいだってのがわかりました。

　 strip no longer removes relocation entries under any condition.

とか書いてあるが、どうも嘘らしい。でも、このHOLって、やっぱり

　普通の人が使うのは不可能

だと思った。84年に先輩が言っていたのを、20年たって確認しただけだった。

それに、

　proved

とか出るだけじゃ、役に立たないし... もう少しLogic Tutorialみたいな形で使いたいんだが...

数学の証明とかは、すべて、HOLの上で動いて、実際に正しい証明かどうかを検証できたりすると面白いと思う。ただ、

　形式的な推論として正しい

ってのと、

　数学の証明として正しい

のは、別なことが多い。実際、そういうことをやっている人もいるんだろうとは思いますが...