全称変数は、型宣言された変数で、その型の任意のモノを表す。任意変数と言ってもいい。$`\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 $…

まだ未整理だが、とりあえず備忘メモ。まず、対称性がある操作達。 無制限タプル構成 無制限コタプル構成（無制限タプル構成の双対） 有限タプル構成（無制限から制限） 有限コプル構成（有限タプル構成の双対） 依存カリー化 カリー化（依存カリー化の非依…

フォワード・リーズニング用に、ステージと同じコンビネータ・コマンドがある： 連言導入用コンビネータ： 既存のn個の証明から連言への証明を作る。 全称導入用コンビネータ： 既存のパラメータ付き証明から全称への証明を作る。 選言除去用コンビネータ： …

ステージ内に居るシーケントは： 事実シーケント 質問シーケント〈問題シーケント | ゴール〉 やること： 事実シーケントの構成（味方を増強する） 質問シーケントの分解（敵を衰弱させる／消滅させる） ステージの種類は： 連言導入用ステージ（連言成分〈…

次のようなキーワードの名前スコープと使い方について考える。 def, theorem let in, let return providing return where section module package 名前とスコープに関する概念： イミュータブル名〈プログラム定数〉とミュータブル名〈プログラム変数〉 公理…

コンテキストと指標は、構文的には区別できないのだが、次の違いがある。 指標はインスティチューション的な意味での指標である。 指標のあいだの射は指標射で、モデル圏のあいだのリダクト関手を定義する。 コンテキストは、固定した指標に対する構文的圏の…

$`\require{color} % 緑色 \newcommand{\In}{ \text{ in }} \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\For}{\Keyword{For } } % 使用 \newcommand{\Let}{\Keyword{Let } }% 使用 \newco…

判断シーケント＝関数定義があるとする。$`\quad a : (\Gamma \vdash t : \beta)`$これを次のようにパックする。$`\quad (a : [\Gamma \to \beta], a := t^\wedge)`$ここで、$`t^\wedge`$ は項のフルカリー化。パックした定義は、環境コンテキストに追加でき…

$`\require{color} % 緑色 \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\Providing}{\Keyword{Providing } }% \newcommand{\When}{\Keyword{When } }% \newcommand{\And}{\Keyword{And } }% \newcommand{\Holds}{\Keyword{Holds…

単に「コンテキスト」は混合コンテキスト 純コンテキスト＝宣言コンテキスト 混合コンテキスト＝宣言と定義のリスト 定義は、宣言（x:A）と割り当て（x:=t）のペア シーケントは三種類： 判断シーケント、事実シーケント、質問シーケント 判断シーケントは、…

ムービーはデータ構造 ムービーはフレームとトランジションからなる。 フレームはステージの構造的な集まり。 ステージはツリー構造を持つ。カレントステージが一意に決まる。 ステージは、シーケントとサブステージの集まり。 シーケントは判断シーケントか…

型の導入規則とは、型の生成規則で、型だけではなくて要素の構成規則も含む。 型を型構成子で生成する。 要素を要素〈値〉構成子で生成する。要素生成子は関数である。 型の除去規則とは、型の消費規則で、関数による要素の構成規則（「構成」で間違ってない…

テキスト ピクチャー ラベル（名前) ワイヤー頂点 型（命題含む） 色付きワイヤー 項 ストリング図 宣言 入力端頂点とワイヤー コンテキスト ワイヤーパレット シーケント ノード 公理シーケント 展開不可能ノード 割り当て 展開可能ノード ステージ パレッ…

散文化は prosify。 映像作品を、通常の文章に直して伝えること。 映像作品を鑑賞することは誰でも出来るが、ノベライズ／散文化は難しい。

「状況」、「シーン」なども用語候補だが、「ステージ」を使う。コマンドは、ステージ上の判断／質問を操作する。またステージ自体もコマンドで操作する。同じ名前に対して、フォワードコマンド doXxx とバックワードコマンド undoXxx がある。全般的な管理…

型 ←→ 命題 ←→ 対象 関数（要素含む） ←→ 定理（証拠含む） ←→ 射 関数コンビネータ ←→ 定理コネクティブ？（言及も命名もされない） ←→ オペレーター／コンビネータ リーズニング・コマンド 対応物がないゲーム・コマンド 圏論的に整理するなら もの〈シン…

次を区別しなくてはならない。 命題 証明〈証拠〉 判断〈主張〉シーケント 質問〈問題 | 問い合わせ〉シーケント フォワードリーズニング（推論ルール含む） バックワードリーズニング（バックワード推論ルール含む） 定理は、証拠〈証明〉を引数として証拠…