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

曖昧表現は： 名前・記号の借用 例： G = (G, *, 1) 省略 例： G = (G, *) 名前・記号の多義的使用〈オーバーロード〉 曖昧表現の解決は、データベース検索。検索条件はパターンマッチ問題〈ユニフィケーション問題〉となる。パターンマッチ問題を解いて曖昧…

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

ミクシン指標の導入と削除には、extends ではなくて、次を使う。 employs 宣言 ： 雇用する、採用する include ディレクティブ ： ミクシン（スニペット）を実際に挿入展開する dismisses 宣言 ： 解雇する、免責する。

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

関数があるとき、引数型と戻り型の仕様が型プロファイル、単にプロファイルとも呼ぶ。プロファイル概念は集合圏の射以外でも考えられる。引数変数を含む項を使って関数を定義するときの $`\cdots \mapsto \cdots`$ は戻り値指定〈return value disignation〉…

視点移動とフットワーク： 階層的宇宙のなかで自分がどこのいるのか？ 区別する／区別しない（同一視する／しない）、どちらの立場か？ 例： 引数なし関数名と定数名 名前が定数名〈固有名〉か変数名〈不定名〉か？ スコープに依存（事項）。 名前のスコープ…

$`\Gamma \mapsto \psi : T`$ が判断のとき、コンテキストのラベル〈名前〉をすべて取り除いたものを $`\widehat{\Gamma}`$ とする。プロファイルは：$`\quad \widehat{\Gamma}\to T`$$`f := \big\langle \Gamma \mapsto \psi : T\big\rangle`$ が定義のとき…

圏論 型理論 論理 メタ論理 指数 [_, _] [_→_], → ⇒, → (⇒) 項の定義 |→ |→, |- |-, |→ (|-) プロファイル → →, ~~> →, ~~> (→) ホムセット {_→_} {_→_}, {_~~>_} {_→_}, {_~~>_} {_(→)_}

区別するなら ◯、しないなら／出来ないなら ☓、無意味なら - 。プログラミング言語に関しては、定義時と呼び出し時で二つ。△はやる気になればやれるが、普通はやらない、ほぼ☓。 集合圏 デカルト閉圏 TypeScript Lean 4 関数と関数データ ◯ - ◯, ☓ ◯, ☓ 関数…

関数・定理の定義・記述 Γ |- ψ : 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_…

論理記号 導入規則 除去規則 ∧ And導入 And除去左, And除去右 ∨ Or導入左, Or導入右 Or導入 ⇒ Imp導入 Imp除去 T True導入 (通常の証明) ⊥ (背理法による証明) False除去 ￢ Not導入 Not除去 1 And intro 基本証明 2 And elim left 基本証明 3 And elim righ…

digraph { logic[label="形式化された\n定義／公理／定理／証明"] ts[label="TypeScript\nプログラムコード"] js[label="JavaScript\nプログラムコード\n(不要)"] logic -> ts[label=" 人手で相互翻訳", dir=both] ts -> js[label=" トランスパイラが翻訳 "]…

And_intro And intro And_left And elim left And_right And elim right Or_inl Or intro left Or_inr Or intro right fun_OR_MAKE なぜか無い 後で定義 Or elim 特殊 Imp intro MP（不要だが） Imp elim trivial True intro EFQ False elim 不要 Not intro …

アロー関数とアロー〈二重矢印記号〉を使った関数空間型の記述 declareを使った外部環境の型宣言 オンライン・プレイグラウンド 対応： TypeScript 疑似言語 function theorem const evidence declare function axiomatic theorem declare const axiomatic e…

型と値は区別する必要がある。 計算と演算を区別するのは難しい。曖昧に区別されていることもあるが、混同して使っても差し支えない。 関数と計算は一応区別するが、ヘッド部（後述）の有る無しの違いしかないので、混同して使っても差し支えない。 型と型の…

テーゼ： 十分に強力な型システム／型チェッカーを持ったプログラミング言語は、証明記述／証明検証に使える。 型 命題 型変数 命題変数 型定数 命題定数 型構成子 命題結合子 型の値 命題の証拠 計算・関数 証明・定理 計算・関数のプロファイル 証明可能性…

digraph { label="proof" subgraph cluster_not_a { label="not_a" h[shape=triangle] And_left h -> And_left[ label="￢A∧￢B"] } subgraph cluster_not_b { label="not_b" h1[shape=triangle, label="h"] And_right h1 -> And_right[ label="￢A∧￢B"] An…

全部事実上同義語。 平叙文 疑問文 型判断 型質問 シーケント 質問シーケント 関数定義 関数定義要求 定理記述 定理証明要求 クロージャ 大きいラムダ式 大きいタプル 大きいlet式

$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\hyp}{ \text{-} } `$$`\mrm{K}^X_I`$ を $`I`$ 上の定数ファミリーとして、$`A`$ を任意のファミリーとする。ファミリーの射$`\quad \mrm{K}^X_I \to A \text{ on }I`$は、グロタンディーク同型により次…

証明項の帰結という言葉を入れてみる。 型理論 論理 計算項 証明項 計算項の型 証明項の帰結 型付け〈typing〉 帰結付け〈consequencing〉 型{付け}?判断 帰結{付け}?判断 型チェック 命題チェック? 帰結チェック? 項の検証? 証明{項}?の検証 項の型推論 証…

eviは証拠〈evidence〉の略記だとする。命題と証明の圏 $`{\bf Ded}`$ から集合圏への関手が定義できる。 $`P\in |{\bf Ded}| \mapsto \mathrm{evi}(P) := {\bf Ded}(\top, P)`$ $`(f:P \to Q) \text{ in }{\bf Ded} \mapsto \mathrm{evi}(f) := {\bf Ded}(\…

依存型に一般化したカリー同型：$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\In}{ \text{ in } } `$$`\quad \cat{C} \in |{\bf Cat}|\\ \quad A:I \to |\cat{C}|_0 \In {\bf Set}\\ \quad \prod_{i\in I} \ca…

関数の意味： 関数そのもの＝集合圏の射 関数定義 関数{定義}?ヘッド＋関数{定義}?ボディ 関数定義ボディは計算項 定理・証明の意味： 定理（証明）そのもの＝演繹圏の射 定理記述 定理{記述}?ヘッド＋定理{記述}?ボディ 定理記述ボディは証明項 「証明」の…

前提： 条件{節}? conditional clause 事実： 主張 assertive sentence 判断： 証拠付き主張 ／ 証拠 with Evidence 質問： 疑問文 interrogative sentence / Question コンテキスト、項、戻り型〈return type〉がある。 コンテキスト 項 戻り型 記号 知識 …