cocolog:84021412

T. Nipkow & L. C. Paulson & M. Wenzel 『Isabelle/HOL』を読んだ。2002年に出た本で、前回 [cocolog:83987064] で読んだ Isabelle2015 の tutorial.pdf の古いバージョンにあたる。 (JRF 0733)

JRF 2015年11月30日 (月) Tweet

『Isabelle/HOL』(T. Nipkow & L. C. Paulson & M. Wenzel 著, Springer LNCS 2283, 2002年)
http://www.amazon.co.jp/dp/3540433767

JRF2015/11/305961

ずっと気になってて、Amazon の欲しい物リストに登録していて、2009年についに買ったんだけど、今になるまで読まなかった。

前回、tutorial.pdf を読んで、この本を読むと、どうもこの本は tutorial.pdf の古いバージョンであることがわかった。

だいたい同じ内容ではあるが、この先、Isabelle を「使う」ことを考えれば、２回読んどくのも悪くなかろう…もったいないし…ということで今回、読んだ。

JRF2015/11/301314

……。

Isabelle2015 の tutorial.pdf とこの本ではこの表記が少しずつ変わっている他、大枠は同じだった。

JRF2015/11/307108

ただ、終了性(termination)を証明しながら使う recdef という関数定義が、そんな難しいことを必要としない fun に変わって載っていて、その部分が機能的に欠落しているという印象を受けた。

JRF2015/11/306585

また、type class の例が、新しいほうは群論で structured Isar proof を使っていたが、古いほうは、順序理論で apply ... done 形式の証明だった。順序理論はいずれやりたいと思っていたので、「やっぱり」先にやられていたなという印象を持った。でも、type class みたいなことは ZF 上ではどうやるんだろう…という疑問は残った。

JRF2015/11/303061

大きな違いは、ほんと、それぐらいだと思う。あと新しいほうには Find Theorem の方法等の関連も載っていたぐらいか。

その割には読むのに時間がかかった。tutorial.pdf のほうをちゃんと読めてなかったということだと思う。

JRF2015/11/308904

……。

以前やったラムダ計算のα同値の関する証明を見ると、tactic だけでなく tactical もかなり使っていて、それは現在の Isabelle/Isar では対応していないようだ。複数の定理を変数にまとめるようなこともしているので、その扱いをどうするかも考えないといけない。もし、Isabelle2015 に以前の証明を対応させようとすればの話だが。でも、それはとても面倒くさい。はっきりいってやる気が起きない。

JRF2015/11/306572

コンピュータ上で証明しなかったが、Barendregt のαの定義(↓)でも OK だと手書きのノート上では考えていた(そのノートは今見つからない)。でも、今、Barendregt の定義の書き方を見ると以前持っていた印象と違ってとまどう。その証明もしたいというのが心に引っかかってることだったのだが。

JRF2015/11/308995

『The Lambda Calculus, Its Syntax and Semantics』(H. P. Barendregt 著, North Holland, 1985年)
http://www.amazon.com/dp/0444875085

JRF2015/12/19134

typo 「Barendregt のαの定義」→「Barendregt のα同値の定義」。

JRF2015/12/28817