場合分けによる関数定義はどうするのか？ 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の場合、項としての証明オブジェクトはないし、証明の遂行中の履歴もユーザーから見えている気配がない。その意味で証明オブジェクトの存在は希薄。だが、概念的には何かしらの証明オブジェクトはあるはず。証明オブジェクトを作る過程をリーズニン…

Knowing is not enough,we must apply.Willing is not enough,we must do. だそうで。

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

スレッドをスタートする関数が StartHogeProcess みたいな名前（にしたのは自分）で、プロセスだと思っていて、処理をスタートさせてからメイン側を終了させた。当然にプロセスが終わるので、そのなかのスレッドも終了する。このときの終了の仕方が、かなり…

小野寛晰『情報科学における論理』は、一番よく参照していたと思うが、ない。

現状と対策、、、ほぼ地獄の様相 - 檜山正幸のキマイラ飼育記 メモ編 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）となる。 ルール： オブジェクト論理（ユーザー定義の論…

論理屋が論理的な語りをしない／出来ない、という現実がある。諺に、「医者の不養生」「紺屋（こんや 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文の後に続く部分 …

C-x 8 RET 221e RET C-x 8 RET infinity RET

基本は、滅茶苦茶、恣意的、行き当たりばったり、気分次第、その場限り、思い付きで、イイカゲン、ルール無し、である。が、たまに区別を要求するからタチが悪い！多用されて多義性が強い（オーバーロードが激しい）用語は、その意味を列挙した辞書を作るし…

「これはひどい」としか言いようがない。[追記]研究対象→曖昧な用語法の研究 - 檜山正幸のキマイラ飼育記 メモ編[/追記]他の参考記事： 「ならば」記号の部分 - 檜山正幸のキマイラ飼育記 メモ編 論理の用語、日本語-英語 - 檜山正幸のキマイラ飼育記 メモ編…

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 、それぞれに動詞がある。 テクニカルタームなのか説明の地の文としての言葉なのか? つまり、理論的／技術的な定義があるのか、それ…

これらの意味がわかればだいぶスッキリすると思うのだが、 これは論理学の言葉ではない。 ソフトウェア実装系やそのアルゴリズムを語るときの言葉。 したがって、非宣言的、手続き的、スクリプト的 ウェンツェルは、手続き的・スクリプト的な説明を避けてい…