Isabelle
論理屋が論理的な語りをしない／出来ない、という現実がある。諺に、「医者の不養生」「紺屋（こんや or こうや）の白袴」とかあるけど、ちょっと違うな。他人のために尽くしていて自分には手が回らない、ってのとは違う。「儒者の不身持（じゅしゃのふみも…
isar-overviewのBNFによる構文範疇としては、fact ::= label 。labelの定義はないが、たぶん識別子だろう。論理式を識別する名前がラベルとすれば、factは論理式の名前ってことになる。 tutorialにはfactの定義はない。 isar-refには、logical contentとは、…
http://www4.di.uminho.pt/~mjf/pub/SFV-CurryHoward-2up.pdf にいいことが書いてある。 Shallow encoding (Logical Frameworks).The type theory is used as a logical framework, a meta system for encoding a specific logic one wants to work with. Th…
こうすればCoqに入門できそうだ （誰も書かないCoq入門以前 5） - 檜山正幸のキマイラ飼育記 : そして、説明に使う言葉がまた問題です。Coqの説明には、関数型言語、論理、型理論などの言葉が入り混じって登場します。型理論の用語や記号が無茶苦茶のグチャ…
素直に「ルールXxxを適用する」と読まない！ ルールは常識的な上から下の推論図で描かれる。推論（リーズニング）は逆方向だから、 ルールXxxを逆適用する
Findタブって、find_* コマンドと同じじゃん。なんだよコレーー。
A proposition is a well-typed term of type prop, a theorem is a proven proposition. theoremはproven propositionsとか言っているが、 thmデータをtheoremと言っていることが一番多い感じ。 ポールソンは、theoremはruleだ、と言っているし、 ウェンツ…
現状と対策、、、ほぼ地獄の様相 - 檜山正幸のキマイラ飼育記 メモ編の方針で、1エントリに1語ずつ説明していく。[用語法][多義語]タグを付けて、タイトルにも「多義語：」と入れる。 辞書的意味 Isar文書内で、theoremコマンドによるIsar文の後に続く部分 …
基本は、滅茶苦茶、恣意的、行き当たりばったり、気分次第、その場限り、思い付きで、イイカゲン、ルール無し、である。が、たまに区別を要求するからタチが悪い！多用されて多義性が強い（オーバーロードが激しい）用語は、その意味を列挙した辞書を作るし…
「これはひどい」としか言いようがない。[追記]研究対象→曖昧な用語法の研究 - 檜山正幸のキマイラ飼育記 メモ編[/追記]他の参考記事： 「ならば」記号の部分 - 檜山正幸のキマイラ飼育記 メモ編 論理の用語、日本語-英語 - 檜山正幸のキマイラ飼育記 メモ編…
implementation文書4章、ここに色々書いてあった。だけど、けっこう無茶苦茶。 initial claim ＝ final goal だぁーー。backward reasoningだから。 {final,main,primary,initial}{goal,claim,statement,thesis,proposition}はどう組み合わせても、ほぼ同義 …
名詞で言えば、implication, deduction, reasoning, inference, derivation, proof, entailement, verification, judgment 、それぞれに動詞がある。 テクニカルタームなのか説明の地の文としての言葉なのか? つまり、理論的／技術的な定義があるのか、それ…
これらの意味がわかればだいぶスッキリすると思うのだが、 これは論理学の言葉ではない。 ソフトウェア実装系やそのアルゴリズムを語るときの言葉。 したがって、非宣言的、手続き的、スクリプト的 ウェンツェルは、手続き的・スクリプト的な説明を避けてい…
何度も同じことを繰り返し書くが、そのときどきの現状報告 assertion あまり使われてない claim 構文範疇のclaimはある thesis - "?theis"というシェマ変数（schematic variable）はある。哲学用語だと「ヘーゲルの弁証法の正」、命題、テーゼだとか。複数形…
どう違う？
print_options 便利。
http://isabelle.in.tum.de/library/HOL/HOL-Isar_Examples/outline.pdf では、 引用符をやめている。 ハイフンを名前に使っている。
オールドスタイルの証明コマンド／証明メソッドは、isar-refの"9.2 Basic proof tools"にある。
次は最初から使える。 typedecl 型または型構成子を導入できる。型レベルでの定数（＝型名）と定関数（＝型構成子）のシグネチャ宣言のようなもの。 class 型クラスは使える。「class 名前だけ」というのも特別にあって、これでユニバーサルな型クラスを定義…
lemmas（複数形！）というコマンドがある。lemmas G = A B C のように書いて、複数の定理をグルーピングできる。lemmas X = A なら、定理Aに別名Xを与えることが出来る。これを使うと、特定の名前Aの定理の内容を目視できる。ダミーの名前 X を使って、lemma…
シグネチャ（って言うかどうか知らんが）の宣言のとき、foo: "'a => 'a => X" (infix "$$" 70) のようにしてmixfix構文と優先度を指定できる。シグネチャで指定し忘れても、後からmixfixの宣言だけ出来る。 notation 名前 ( mixfix指定 )と書けばいい。mixfi…
definition はPureレベルで使える。definitionは定数定義、関数定義に使えるが、形式としては、等号的公理の追加になる。"左辺 == 右辺" で、「右辺により左辺が定義される」と読むようだ。左辺は定数、関数・演算子の呼び出し形式とか。書き換え規則を定義…
NGと書いてあるところだけダメ。 (* on top of Pure *) axiomatization A:: "'a ⇒ prop" and B:: "'a ⇒ prop" and P :: "prop" and Q :: "prop" term "op ==> P Q" term "P ==> Q" (* NG *) term "(A a)" term "(B b)" term "op ==> (A a) (B b)" term "(A a…
論理の説明が論理的にされることはほぼないので、用語法がイイカゲンで、曖昧・多義的・気分次第・行き当たりばったりであることはショーガナイとは思っているが、なんかガイドラインくらいは欲しい。どこにもガイドラインはない。自分で作ろう。多義的で注…
歴史を調べないと分からない処理系、てのも困ったもんだが、 エジンバラLFが「ロジカルフレーム」として先行か？ λPrologってのもある。 スコットのLCF理論が背景 ミルナーのMLで実装 CoqはIsabelleの後: Isabelle 1986年、Coq 1989年 3年後 [追記] "Logic o…
IFOL上のセオリーだと、term "(%x. (%y. x)) a" がエラーになる。その理由は、setup Pure_Thy.old_appl_syntax_setupというコマンドが実行されており、これによって、Pureの併置による適用の構文がキャンセルされて、x(y) という形でないと適用とはみなされ…
空列はPureの項ではない。 任意の識別子は項になる。 型推論される。 勝手な識別子の型は型変数 'a とされる。型総称な変数ということだろう。 併置は適用演算のはず。 ラムダ抽象は %x. A 、ピリオドの直後の空白は必須。 η変換は自動で行う。 β変換も自動…
proof method, tactic, rule, proof script, proof command あたり。proof commandの定義はない。commandの分類に、theory command, proof commandとかあって、lemmaはproofコマンドに分類されてる。「lemmaはゴールコマンドだ」とかの記述もあった。コマン…
文書指向へと舵を切ったウェンツェルだが、まだまだ全然だし、先は長いし、苦難が予想される。 用語法、メンタルモデルがスクリプト指向のまま。 ウェンツェル自身もfact, goalを多用している。 論理の概念・用語法と、ソフトウェアとしての証明系の用語・文…
infix operatorの優先度の一覧が欲しいだけど、isabelle infix operator precedence とかでググッてもあんまり分からん。Coqだと、公開されているHTMLマニュアルが引っかかったけど、Isabelleは粒度がでかいPDFだからなーー。[追記] introの"4.1.1 Infix Ann…
