参考： MLソースを扱うとき - 檜山正幸のキマイラ飼育記 メモ編 デスクトップにIsabelle2016（少し古い）のアイコンがある。 このアイコンは C:\Installed\Isabelle2016\Isabelle2016.exe を指している。 Isabelle2016.exeの実体は、jEditをフロント、PolyML…

Isarのbyはボディがない証明（proof eqd）の略記。byの直後は証明メソッド。 Mizarは推論規則の適用とスキーマの適用をby, fromで区別するが、Isarは高階論理なのでbyだけ。 Isarの前置fromはMizarのfromとは別。Mizarのby相当らしいが要チェック。 Isarの前…

証明は、複合証明 proof ... qed か、自動証明 by ... のどちらか。 自動証明の根拠と複合証明のヘッダ部には証明メソッドが書かれる。 複合証明の本体（ボディ）部は、文（ステートメント）の列。 文（ステートメント）は次の種類： fix文 自由変数の宣言 a…

名前の管理が甘い、名前空間が粗末 ユニコードを考慮してない。アスキー偏重。 Mizar以外は、スクリプト言語またはそのシンタックスシュガー。 ブロック構造を意識してないか曖昧。 文書構造を意識してないか粗末 型クラスがあと付けで歪んでいたり問題を抱…

Mizar Isar let fix assume assume set let set def consider ... such that obtain ... where take (no equivalent) per cases ... proof ... qed suppose next assume (no keyword) have thus show hence then show thesis (?thesis) proof ... end proof …

型クラスのパラメータ問題（トラブルっぽい話）が出てくるのは、指標とモデルの相対性の考察が不足しているせいだと思う。グロタンディーク平坦化を“積分”とみなしてのフビニに定理だと思う。繰り返し積分と同時多重積分の同値性。直積領域の積分ではなくて…

MLのモジュールシステムは禁欲的で、必要最小限の機能だけだが、スッキリしていて好きだ。だが： signatureにパラメータを付けられない。functorは当然にパラメータ（引数）を持つが、functorの値はstructureであってsignatureを値には取れない。 これは当然…

昨日の 型クラスの比較 - 檜山正幸のキマイラ飼育記 メモ編 への補足説明。既存のものに後からゴチャゴチャ文句を言うのは簡単だ。だから文句言う。コアージョン（coercion - 檜山正幸のキマイラ飼育記 メモ編）は必要悪という意味で必須だから、使うのはい…

Standard MLが圧倒的に良くできているな。オーバーロードを意図してない、型システムじゃない、という問題点はあるが、許せる、許せる。Haskellは「悪いお薬」をキメている。当座はとても元気が出るが、いずれは心身を蝕むアレ。型名に対するコアージョンを…

isar-ref "2.2.1 Context elements"

生成規則 generation： 前提（既存証明オブジェクト）がないところから証明オブジェクトを1個作る 変形規則 deformation： 1つの前提から証明オブジェクトを1個作る 組み合わせ規則 combination： 複数の前提から証明オブジェクトを1個作る また、リーズニン…

どうにもならないなーー(溜め息)「除去規則の適用」のレゾリューションアルゴリズムの圏的意味論を考えてみたが、これは複雑。なのに、Isabelleのなかでは天下り。これでは納得出来るわけがない！それはそうと、ポールソンは、メインゴールとサブゴールズと…

CoqでもIsabelleでも同じ。Coqの証明ゲームの表側と裏側 （誰も書かないCoq入門以前 4） - 檜山正幸のキマイラ飼育記 : Coqシステムは、そして自分は、いったい何をやっているんだ？ これが証明って、いったい何でだ？ こういう疑問を払拭できないのは、Coq…

Isabelleの用語法の無茶苦茶さや、概念の混乱、理解のためのミッシングリンク、これらの大きな部分は「次元概念の欠如」によるのではないだろうか？ -- まず間違いない。 参考：シーケント計算、ムービー、高次圏 - 檜山正幸のキマイラ飼育記 メモ編 参考：…

オカシイ、オカシイ。除去規則（elim rule）がIsar satement formatだとobtainsで書かれる。これはオカシくはない、つうかまっとうなんだが、逆に通常の除去規則の書き方はいったいなんなんだ？ ということになる。disjEの例だと： ?P ∨ ?Q ==> (?P ==> ?R) …

ウッヒャーー、またしても新用法を発見。subgoalがsolveすべき対象である命題（＝論理式＝ルール＝定理）で、goalはそれらsubgoal達の集合の意味で使っている。つまり、ゴール＝サブゴールズ。しかし、サブゴールの結論をゴールと呼ぶことがあるから。「ゴー…

メニューツリーのパス: [Plugins]-[Plugin Options] タブ: [Plugin Options] ツリーコントロールのパス: /Isabelle/General レコードのフィールド名: Auto Quickcheck UIの種類を無視してパスで示すと Plugins/Plugin Options/Plugin Options/Isabelle/Gener…

「なるほど」とは思うが、なんか、これしか方法がないのかよ？ とも感じる。 Isabelleではgoal文はないので、lemma "命題" と書いて、この行の表示（カーソルあわせてOutputを見る）で、ゴールを見せる。 タクティクの説明は、apply(タクティク) oops とする…

ストリング図とストリンググラフの関係を使い、グラフ理論的な操作として証明行為＝リーズニングを理解する。キーワード（大事な言葉）の定義： 推論ノード：通常の推論規則を表す。複数（0個もあり）の入力（仮定）と1つの出力（結論）を持つ。 ワイヤー：…

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年…