帰納的にデータ型を定義するとき：$`\require{color} % Using \newcommand{\NN}[1]{ \textcolor{orange}{\text{#1}} } % New Name \newcommand{\NX}[1]{ \textcolor{orange}{#1} } % New EXpression \newcommand{\T}[1]{ \text{#1} } \newcommand{\B}[1]{ \m…

カリー／ハワード／ランベック対応を徹底するには： calc/compute（動作・行為）とprove（動作・行為）proof（すること）を同義とする。 function returns a velue of type T と theorem returns a witness of prop T を同義とする。 prop は広義の型の一種…

名前空間、知識記述〈knowledge description〉の名前空間と用語レキシコンの名前空間は別。 名前空間名と名前空間階層ツリー 名前の分類子、分類子による名前空間のパーティショニング。異なるパーティションの同一ローカル名は異なる。 「名前空間名」は名…

テンプレートは、穴〈スロット〉を埋めることにより具体物を作り出すことが目的。 穴〈スロット〉がないテンプレートをリテラル・テンプレート、あるいは単にリテラルと呼ぶ。それだけで具体物。 穴が実際にあるテンプレートは非リテラル・テンプレート。「…

in◯◯, un◯◯, non-◯◯, dis◯◯, ◯◯less◯◯, ◯◯ without ◯◯、非◯◯、不◯◯、無◯◯、◯◯なし◯◯ など。用法： 制限的用法 拡張的用法 排他的用法 冗長な用法 非可換／可換： 拡張的用法： デフォルトで環が可換のときの、非可換環。スーパー指標を追加して、既存指標「…

同義語句による置き換え〈replacement〉 例： pointing function ＝ example 変形ルールによる変形 例： example of type Nat named k → example k returns type Nat 省略可能な情報の省略と補完 例： type T → type T in U 注記情報の追加と削除（これも省…

$`\require{color} % Using \newcommand{\NN}[1]{ \textcolor{orange}{\text{#1}} } % New Name \newcommand{\NX}[1]{ \textcolor{orange}{#1} } % New EXpression `$$`\text{volatile namespace}\\ \text{we define function }\NN{f1}\\ \quad \text{by pos…

define applying end が定義の構文だが、キーワード applying の直後に記述フォーマット名を付けてよい。つうか、付けるのが推奨。 applying record-schema-template-diagram ◯◯ end applying record-schema-template-text ◯◯ end applying standaard-arithm…

次は同義 $`\text{we define example of type }T \text{ named }e`$ $`\text{we define pointing function } e \text{ returns type }T`$ example〈事例 | 具体例〉は pointing function に展開されるが、of は語順を変えてしまう。of は戻り値型を先に記述…

使用法変種とは usage variant 、使用法により記号が変化する。本質的な意味は変わらない。 $`\mapsto`$ ： 割り当て単位〈assignment unit〉を記述する。 $`:\in`$ ： 割り当てが、所属宣言であることを示す。 $`:=`$ ： 割り当てが、代入単位であることを…

中括弧の使用法が、列挙記法〈外延的記法〉と内包的記法で違いすぎる。暫定的だが、記法を決める。 集合の列挙記法： $`\{a, b, c\}`$ 集合の名前隠蔽内包的記法： $`\{\!| x :\in X \mid \cdots |\!\}`$ 縦棒を追加、厳密にZFCの意味で使う。ただし、$`\{\!…

リスト／タプル囲み括弧（具体データ構成子記号／型項構成子記号の一部と考える） 引数囲み括弧（評価演算の二項演算子記号の一部と考える） 演算の優先度括弧（パーズツリーに影響する） まとまり括弧（パーズツリーに影響しない） 規則と注意 引数囲み括弧…

$`\newcommand{\Imp}{\mathop{ =\!\!\triangleright }} \newcommand{KER}{ \mathrel{\stackrel{\rightharpoonup}{\sim}} } % Kleene Equarity Right \newcommand{KEL}{ \mathrel{\stackrel{\leftharpoonup}{\sim}} } % Kleene Equarity Left \newcommand{\le…

主語 we 動詞 declare, define, approve〈アプルーブ〉 副動詞 request, respond 名前の修飾語 type, function typeへの副修飾語 logical, type-param, prop-param functionへの副修飾語 section, bundle, type-velued, prop-valued, partial 終止語 end そ…

主動詞： declare〈宣言する〉, define〈定義する〉, approve〈承認する〉 副動詞： request〈要求する〉, respond〈応答する〉 主語は We, One of us, I だが、省略可能。組み合わせは： declare 名前 仕様 ： 名前を宣言する。存在に関しては中立。 declar…

https://arxiv.org/pdf/1311.7642 の2.1 のクライスリ構造〈クライスリ拡張構造〉$`\newcommand{\T}[1]{\text{#1}} \newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\text{ in }} \newcommand{\twoto}{\Rightarro…

全称変数は、型宣言された変数で、その型の任意のモノを表す。任意変数と言ってもいい。$`\require{color} \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} } \newcommand{\for}{\Keyword{for } } \newcommand{\assume}{\Keyword{assume } } \newco…

URL: https://courses.engr.illinois.edu/cs576/sp2015/doc/isar-overview.pdf Title: A Tutorial Introduction to Structured Isar Proofs Author: Tobias Nipkow ブラケットは檜山が挿入。 a [tactic] proof is a more or less structured sequence of com…

Title: Kalish/Montague and Ja´skowski Natural Deduction Authors: Mohammad M. Ajallooeian, Francis Jeffry Pelletier Pages: 9p URL: https://mirror.las.iastate.edu/tex-archive/macros/latex/contrib/natded/extended_doc.pdf $`\newcommand{\mrm}[1…

Title: A Browsable Format for Proof Presentation Date: June 1996 Authors: Jim Grundy, Turku Centre Pages: 8p URL: https://www.researchgate.net/publication/2359706_A_Browsable_Format_for_Proof_Presentation structured calculational proof に…

次の計算系がある。 計算対象物 CC圏 CC複圏 CC多圏 （広義）射 ◯ ◯ ◯ コンビネータ △ ◯ ◯ アレンジメント △ ◯ ◯ CCは Cartesian Closed ◯：うまく定式化できる。 △：ある程度は定式化できる。 演算： 射に対して： 結合、直積、カリー化、評価 コンビネータ…

lambda ： ラムダ抽象 assume backlog ： バックログラムダ抽象 postulate / demand 要請、ラムダ抽象だがバックログだとマークする。ラムダ変数はバックログ変数＝スタブ＝ダミー。 prepare ： 引数の準備 next ： 区切り記号 and_also ： 区切り記号 end …

関数・定理の定義・記述 Γ |- ψ : A 型推論問題の質問 Γ |-? ψ : ? 項推論問題の質問 Γ |-? ? : A プロファイル宣言 Γ |- _ : A （アンダースコアは不定の意味） 単なる省略 Γ |- ψ : _ （不定だが、型推論で確定可能） ホムセット {f | f: Γ |- _ : A} 毎回…

判断・主張と質問・問題の区別ができること。 命題と事実と証拠と証明の区別が出来ること。 証明とリーズニングの区別が出来ること。 ローカル前提とグローバル・コンテストの区別が出来ること。 公理や前提と先送りの区別ができること。 コンテスト環境とバ…

ライブラリとバックログは双対的な存在。ライブラリ／パッケージ管理と同程度にバックログ管理機能が必要。現状、何もしてくれない。Idrisのholeがある程度はバックログ管理。

式〈項〉をギリシャ文字で書くとして α providing x:X, y:Y のような形がproviding式。これは、 within {x:X, y:Y} α assuming x:X, y:Y α と同じだが、providing, justificatin は定義義務／証明義務が発生する。providingで導入された宣言は、バックログ（…

翻訳： let → we_have := → by_using, because_of return → we_conclude, we_showed suffice let/return式 let x1: A1 := τ1 let x2: A2 := τ2 ‥‥ return α: C end別な書き方： we_have x1: A1 by_using τ1 we_have x2: A2 by_using τ2 ‥‥ we_conclude C by_…

theorem half_DeMorgan premise h: ￢A∧￢B entails ￢(A∨B) proof we have not_a: ￢A by using And_left with h we have not_b: ￢B by using And_light with h we conclude ￢(A ∨ B) by using Or_tuple with not_a and not_b end 定理 ド・モルガンの半…

この論文、参考になる。 https://kwarc.info/people/frabe/Research/KRW_isabelle_19.pdf Making Isabelle Content Accessible in Knowledge Representation Formats Michael Kohlhase, Florian Rabe, Makarius Wenzel 日付はハッキリしないが、2020以降なの…

http://www.omdoc.org/pubs/omdoc1.2.pdf の印刷ページ21（p.37）から：Definition 3.2.5 (Monoid) A monoid is a semigroup $`S = (G, \circ)`$ with an element $`e\in G`$, such that $`e ◦ x = x`$ for all $`x ∈ G`$. $`e`$ is called a left unit of $…