thm 定理名 というコマンドで定理＝ルールを表示できるが、存在しない定理名を指定すると、Undefined fact と出る。ということは、実装上は、既存の定理をfactと呼んでいるようだ。print_statement 定理名 というコマンドで表示されるのは、定理名（ラベル）…

KalvalaのGentle Introductionにある自然演繹とユニフィケーションの絵、Nipkowの http://isabelle.in.tum.de/coursematerial/PSV2009-1/session45/document.pdf の絵とか。ダメダメだ。頑張って親切に説明しているが、誤解を助長するだけだろう。やっぱりス…

根本的にナニカが抜けているかも - 檜山正幸のキマイラ飼育記 メモ編 なぜ分かりにくいのか？ の分析 - 檜山正幸のキマイラ飼育記 メモ編 ポールソンにしろ1994年KalvalaのGentle Introductionにしろ、アルゴリズムと証明論を結ぶ話をしてない。まったくと言…

数量の感覚 - 檜山正幸のキマイラ飼育記 メモ編 の件：ここにまとめておく。足していく（つもり）。 日常的な数量の色々 体重 身長 クラスや会社や組織の人数 価格 移動の距離 移動の時間 ペットボトルの容量 ビルの高さ 部屋やフロアの広さ 荷物の重さ 株価…

長さ（道のり）、比、面積と体積などに関して、あまり感覚を持ってない人はいる。出来れば成人前に感覚を養ったほうがいいけど、大人になってからでも生活で意識すれば鍛えることは出来るだろう。数量や空間に対する基本的な感覚の欠如は意外と（本人も周り…

impI, assoc, transとかは、誰でもどこでも使いそうな名前なので、まずバッティングするだろう。find_theorems name: で検索して、修飾されたフルネームで指定するのが安全。

タクティク方式が分かりにくいのはサンザン指摘されているが、何故分かりにくいのか？ の分析がされてないのではないか。ユーザーは、 何に対して、 何をすべきか？ 何をしたのか？ がサッパリ把握できないのが問題なのだ。「何」に対する提示、ヒンティング…

1994年のGentle Introductionとか読むと、処理系の発展・進化はいいとして、説明や教育に関しては、退行した感がある。かつては強調されていた諸点が今は触れられなくなったのは、そのことがコミュニティの内部で常識化したせいだろう。が、新参者にとっては…

やた、やっとデバッガ的なナニカを見つけた。 https://arxiv.org/pdf/1406.0292v1.pdf

tipsつうか、jEditの常識だろうが、 変数 - 青 定数 - 黒 束縛変数 - 緑 型変数 - 紫 型定数 - 黒 キーワード - 薄めの青、緑 コメント - 茶色 内側構文 - 背景：薄い灰色 まだ評価してない - 背景：ピンク 計算中 - 背景：濃いめの紫 エラー - 背景：赤

というわけで、プログラミング言語としてのIsabelleを調べよう。1980, 90年代の資料とMLソースコードか。現在のシステムは大規模複雑だから、MLソースコードを読むのは辛い。Isabelle86のコードとか残っているといいのだが。[追記]あった。 https://www.repo…

今のIsabelleに感じる違和感と難解さって、高級指向（高級志向じゃなくて、高水準言語指向）が過ぎるせいでは？ そんな気がした。志、方向性（志向）としての高水準化、ドキュメント指向、宣言指向は否定しないが、まだ出来てないのに、ユーザーに押し付け過…

進化なのか、退行なのか？ - 檜山正幸のキマイラ飼育記 メモ編に出した Title: A Gentle Introduction to Isabelle Author: Sara Kalvala URL: http://www.informatik.uni-bremen.de/~cxl/lehre/isakurs/tutorial.ps Pages: 12 サラ・ケベレ(?)女史の1994年…

どうかしてるぜ！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…