どうかしてるぜ！Isabelleマニュアルの分かりにくさも尋常ではないが、それを執拗に詮索している僕も常軌を逸しているかもな。どうかしてるぜ。Isabelleコミュニティの人は、「どうかしているぜ」な用語の曖昧さ／乱用を自覚してるのだろうか？ あまり意識し…

Pure等号の推移律はPureの公理（か定理）に入っている。"x == y ==> f x == f z" は示せなかったので、axiomatizationで公理とする。つまり、ファクト（定理データベース）の状況は、 transitiv: ?x == ?y ==> ?y == ?z ==> ?x == ?y eq_preserve: ?x == ?y …

theoremなどを使って証明した最後に結果（定理のステートメントに対応する命題シェマ）が表示されるが、axiomatizationで公理を導入すると命題シェマが表示されない。find_theorems nama: コマンドを使う必要がある。find_* コマンドを使って状況確認するっ…

Pureでどうやって証明する？ 自明に思えるが、やり方が分からない。 typedecl A axiomatization f:: "A ⇒ A" lemma uniq: "x == y ==> f x == f y"

IsabelleやCoqだけを責めることは出来ないな。論理学の用語や概念が曖昧だったんだよな。ものごとをハッキリさせるはずの学問が曖昧な記述で済ませていた。だから、ソフトウェア実装でも曖昧な概念と用語法が引き継がれ、混乱がより悪化した、という事情だろ…

propositin, fact, goal と並べて書いてあるのを見て、ひょっとして、と思った。 propositionとは、真偽の判定を伴わない単なるexpression、つまり論理式のこと factとは、propositionに |- のマークが付いたもの。つまり、判断主張文。 goalとは、propositi…

証明支援系って、ほんとにマダマダ - 檜山正幸のキマイラ飼育記 メモ編 現状がこれでは、先が長くて気が遠くなる。 証明オブジェクトは人間が見ても意味不明（Coq）か、見えない（Isabelle）。 リーズニングの記録としての証明スクリプト（＝タクティクの列…

isar-refのp.46に書いてある話。コンテキストとは、処理系が持っている定理＆ルールのデータベースのことだとする。このコンテキストが見えないことがわかりにくさの大きな原因だ。さらに、コンテキストは入れ子になる。Isarでは、コンテキストを可視化する…

おまえは何を考えているんだ？ 教えてくれ！ - 檜山正幸のキマイラ飼育記 メモ編 apply(assumption) でゴールが解けてしまうことが多いが、具体的な仮定（コンテキストが持っている定理）がどれかワカランことがある。autoだけでなくて、なんかの根拠をつか…

型推論してくれるのはいいけど、その結果がどうであるかを知りたい。 autoで証明してくれるのはいいけど、何をしたのか教えてくれ。 resolutionで、ユニフィケーションの結果を教えてくれ。 何を考えてるかワカランぞ、教えてくれ。教えてくれないのか？ お…

proof method周辺 - 檜山正幸のキマイラ飼育記 メモ編 isar-refの"Chapter 7 Proof scripts"あたりに書いてある。 セオリーのトップレベルで使うキーワードはセオリーコマンド theoremなどのゴール提示コマンで証明モード（リーズニングモード）に入る。 証…

型の表記として、 [A, B] => B は許されている。 命題の表記として、[| P; Q |] ==> R は許されていない。まさかの未定義！ Pureを生で使ってはいけないのは、こういう変な癖があって使いにくいからか。この奇妙な文法の背景が分からない。

一番上はOK、NGとコメントしてあるのは構文エラー definition "right_unit_law == (!!n.(n + 0 == n))" definition "right_unit_law1 == !!n.(n + 0 == n)" (* NG *) definition "right_unit_law2 == (!!n. n + 0 == n )" definition "(right_unit_law3) == …

マダマダというか、ダメダメというか。とっても使いにくい。30年間作り続けてこのレベルってことは、あと30年くらいはかかるのかな、生きてネーよ、チクショー。次が欠けている。 情報検索機能 アウトライン機能 リソース管理機能 ビジュアライズ機能 情報の…

Title: Automated Theory Interpretation Author: Immanuel Normann Pages: 138 URL: https://svn.eecs.jacobs-university.de/svn/eecs/archive/phd-2008/normann.pdf 学位論文。歴史とか用語法とかまとめようと頑張っている。読み物としても面白い。この論…

Pureをいじっているが、性悪なシステムだな。 接頭辞PROPの意味が分からない。他の構文とは違う、かなり特殊。 型propには定数がなくて、true, falseもない。 PureとIFOLで関数適用の構文が違うのが非常にストレスだし、間違う。 prop型の定数はaxiomatizati…

情報検索の機能が低い。find_* とか print_* だけ。小洒落た機能はない。キーワード（コマンド名）に対して、そのコマンドがどのセオリーやどのMLファイルに由来するかも検索できないようだ。ディレクトリ内からファイルを探してソース読むしか無いようだ。s…

場合分けによる関数定義はどうするのか？ funとかの高級な方法使わないで。 項の計算（単純化）はどうするのか？ これもvalueとか使わずPureのレベルで。 定義（宣言）した型に対するユーザー定義の等号はどうやって定義するのか？

axiomatizationは、シグニチャ部と公理（の論理式）部からなる。IFOL.thy : axiomatization eq :: "['a, 'a] ⇒ o" (infixl "=" 50) where refl: "a = a" and subst: "a = b ==> P(a) ==> P(b)"構造は、localeやclassと同じだが、fixes/assumes ではなくて、…

fact(s) -- まだ謎。おそらくは、contextと同義。 constant -- 狭義の定数記号だけではなく、関数記号、関係記号、述語記号、定理に付けられたラベルなどは定数と呼ぶ。高階論理なので、関数、述語、関係なども意味領域のモノ（個体）となるから、定数と呼ん…

Isabelleの場合、項としての証明オブジェクトはないし、証明の遂行中の履歴もユーザーから見えている気配がない。その意味で証明オブジェクトの存在は希薄。だが、概念的には何かしらの証明オブジェクトはあるはず。証明オブジェクトを作る過程をリーズニン…

isar-refとかimplementtion文書で： stateが状態（名詞）と述べる（提示する、主張する）のときがある。Isar/VMでは、述べるの意味のstateが状態の名前として使われている。"state"という名前で「述べる」の意味のstateがある。 argumentが引数のときと、議…

現状と対策、、、ほぼ地獄の様相 - 檜山正幸のキマイラ飼育記 メモ編 Pureの型prop 命題論理の命題変数 論理式（一番標準的だと思える） 閉じた論理式（自由変数を含まない） 型がpropであるラムダ項 MLのデータ型thm MLのデータ型thmのデータインスタンス M…

現状と対策、、、ほぼ地獄の様相 - 檜山正幸のキマイラ飼育記 メモ編の方針で、1エントリに1語ずつ説明していく。[用語法][多義語]タグを付けて、タイトルにも「多義語：」と入れる。 辞書的意味 証明が済んだ論理式（ほぼ、辞書的意味） ML言語のthmデータ…

全称束縛変数をパラメータと呼ぶらしい。Coqだと、公理をパラメータと呼んでいたりしたな。公理も作業仮説であり仮のものと考えると、文字通り仮引数だからだろう。理論を手続きと考えての仮引数。この発想だと、定理は出力＝戻り値か。理論を「証明の集まり…

TTYはダメだ、と言いながらOutputパネルはほぼTTY。そのため： 出力が長いときに、切られる。 出力から文字列を探せない。GUIでよくある「目でgrep」、辛い！ 出力がリンクやボタンであればいいのに。例外は thy_deps だが、ショボい。 コピペは出来る。が、…

attributeもテクニカルタームらしい。オプションとかアノテーションとかに近いものらしい。定理に対して、なんらかの付加情報を付ける働きがあるようだ。構文範疇にattributeがある。attributeは、'[' 名前 引数のカンマ区切り並び ']' の形で、ブラケットだ…

proof constantって、登録されてた定理のことかも。find_constsで定数を検索できる。その表示は、名前（ラベル）と型の組のリスト。find_theoremsでは、名前（ラベル）と命題（あるいはシーケント）の組のリスト。どちらも名前付けられているモノ。モノが項…

参照：よく分からん用語 - 檜山正幸のキマイラ飼育記 メモ編 solve -- テクニカルタームのこともある。goalをsolveする、というし、solved goalともいう。solve this problem とかは日常語だろう。 answer -- ユニフィケーションの結果である束縛をanswerと…

Isabelleの場合： 定理： 実装言語MLのデータ型thmとそのインスタンスを定理と呼び、それに引きずられている。実装レベルでは、たいていの概念がthmデータで表現されているので、なんでも定理（＝thm）となる。 ルール： オブジェクト論理（ユーザー定義の論…