設定は： <script src="https://cdn.jsdelivr.net/npm/mathjax@2/MathJax.js?config=TeX-AMS_HTML"> </script> <script> MathJax.Ajax.config.path["Contrib"] = "//cdn.mathjax.org/mathjax/contrib"; MathJax.Hub.Config({ CommonHTML: { linebreaks: { automatic: true } }, "HTML-CSS": { linebreaks: { automatic: true } …

次の記事参照、ありがたや。 https://maxima.hatenablog.jp/entry/2020/08/14/150228 <script type="text/javascript" src="https://cdn.jsdelivr.net/npm/mathjax@2/MathJax.js?config=TeX-AMS_HTML"> </script> <script type="text/javascript">//

↓が起源らしい。 Nicolaas G. de Bruijn, Telescopic mappings in typed lambda calculus, Information and Computation 91 (1991), no. 2, 189–204. https://www.win.tue.nl/automath/archive/pdf/aut103.pdf RICHARD GARNER "TWO-DIMENSIONAL MODELS OF TY…

rw h は等式的法則 h （hは等式的法則のラベル）を使ってターゲット内の項を別な項で置き換える。 rw ←h とすると、a=>b 方向のリライトをする。矢印が逆！ rw h とすると、a まったく！

constantは、域が単位対象＝空リストである射を宣言する。図では三角ノードになる。variableは、名前付きのワイヤーを準備する。意図としては、その名前付きワイヤーはラムダ束縛するつもりだから、事実上束縛変数の選言。変数名は混乱の原因になるから、で…

https://leanprover.github.io/reference/tactics.html#basic-tactics This tactic applies to a goal whose goal has the form t ~ u where ~ is a reflexive relation, この言い回しにはさんざん悩まされた。「ゴール」に意味が。 証明状態 メインゴール …

デカルト閉復圏とラムダ計算 - (新) 檜山正幸のキマイラ飼育記 メモ編、ラムダ図 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。とても良い描画法を思いついた。青で書いているのは黒がなかったせい。ラムダハウスは関手ボックス／関手ストライプ／オペレ…

ラムダ図は、ラムダノードとワイヤーからなる。 ラムダノードは三角または台形で描く。 ノードに接合するワイヤーには、入力ワイヤー（0本以上）、ラムダワイヤー（0本以上）、出力ワイヤー（1本だけ）がある。ラムダノードは逆行ワイヤーとして描く。 ワイ…

「-----」は、アトミックな証明＝推論ルール 「~~~~~」は、アトミックとは限らない証明（アトミックを排除しない） 「=====」は、アトミックなリーズニング＝タクティク 「+++++」は、アトミックとは限らないリーズニング＝スクリプト (A∧B)→C ⇒ A→(B→C) の…

連言ボックス、選言ボックス、全称ボックス、存在ボックス - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。モヤモヤを晴らすためにすること。 ラムダ項の圏論的位置付けをハッキリさせる。 単なる圏ではなくて復圏〈オペラッド〉を使う。 デカルト閉復圏＝…

区別しない習慣が悪い癖。 連言リストと選言リストの区別 連言リストと選言リストは明確に分かるようにする。 連言リスト ∧(A, B, C) 選言リスト ∨(A, B, C) または、 連言リスト (A, B, C) 選言リスト (A | B | C) 単元リストと空リストのとき区別できない…

加減乗 +, -. * 逆行列 inv(-) 転置行列 ' ランク rank(-) カーネルの基底 null(-) 行列式 det(-) トレース trace(-) 三角化 triu(-), tril(-) 方程式を解く linsolve(A, b) Ax = b を解く。

考えながらダラダラと書く。まず普通のシーケント計算： Γ, A ⇒ B ---------- 含意導入 Γ ⇒ A→B Γ, x:A ⇒ P(x) ----------------- 全称導入 Γ ⇒ ∀x:A.P(x)こう見ると確かに似てる。PがAとの依存性がないとは、P(x) = B が常に成立。よって、∀x:A.P(x) = ∀x:A…

Leanの定義構文のプロファイル部は完全なシンタックスシュガーで、無視されて、内部的にはフルカリー化版が記憶される。そそもそも、内部の還元エンジン〈reductione engine〉がフルカリー化されたポイント射しか扱えない。これが、圏論的解釈とラムダ計算的…

Lean ILean 復CCC 論理 : ⇒ → → → → [,] ⊃ 空白 :: : (なし) ∧ ∧ × ∧ true true 1 T false false 0 ⊥ 空白区切り 空白区切り カンマ区切り カンマ区切り (なし) (なし) ストリング図 横棒図 命題 命題 対象 論理式 命題リスト 命題リスト 対象リスト 論理式…

選言ボックスと二面ノード - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。絵は裏写りがすごくて、ゴミが入っていたりする。図の右下はゴミ（別な図の一部）。左から右、上から下の順で説明。 ∀elim ： ∀i∈I.A ⇒ A(a) （⇒はシーケント矢印）の証明。ケーブ…

いいこと思いついた。たいぶいいこと思いついた。NK風証明図のストリング図による描画で、けっこう困るのが選言〈論理OR〉の処理。これの描画法を思いついた。思いついた時系列に沿って説明する。分配法則 A∧(B∨C) ⇒ A∧B ∨ A∧C （シーケント矢印は二重矢印）…

variables (P Q:Prop) theorem sample (hp : P) (hq : Q) : P ∧ Q ∧ P := begin apply and.intro, -- 5 assumption, -- 4 apply and.intro, -- 3 assumption, -- 2 assumption -- 1 endtry it! ☆ ☆ ---------- 1 ---------- 2 P, Q → P P, Q → Q ☆ ---------…

ゴールズ状態にはカーソルがあって、現ゴールが決まっている。それは表示上の一番上または一番左のゴールで、アタック（タクティクの適用）は常に現ゴールに対して行われる。したがって、逆リーズニングツリーを上から下、左から右に描けば、上から下の方向…

コンテキスト内のセットアップではない型宣言を仮説〈hypothesis〉と呼ぶ。ラムダリスト内の型宣言を仮定〈assumption〉と呼ぶ。だが、仮説によりターゲットが直接得られるときにう使うタクティク名は premise, hypothesis ではなくて、asspumption （by ass…

Leanのシーケントは、ゴール＝リクエストとして出てくるが、その形式は コンテキスト ⊢ ターゲット コンテキストは型宣言のカンマ区切り列、ターゲットは型式〈かたしき〉。その意味はリクエストだから、 コンテキスト ⊢? _:ターゲット 例： p q : Prop, hp …

https://leanprover.github.io/reference/tactics.htmlを見ても、自然言語で書いてあるだけ。これでは分からない！！順行リーズニングと逆行リーズニングをペアにして、絵で説明しないと。

id : an identifier expr : an expression : a sequence of identifiers and expressions (a : α) where a is an identifier and α is a Type or a Prop. バインダーズは、列となっている。列とリストの区別はあるのかな？ 列＝構文上のリスト かな？ Leanで…

format or template plan and materials performance or execution performer schedule media or channel

Ireneではない。ideal Lean 理想化Lean。 Lean ILean 圏論 論理 A→B→C A B → C [A, B → C] A⊃B⊃C or A∧B⊃C (a:A)(b:B):C A B ⇒ C A, B → C A, B → C f (a:A)(b:B):C f (A B) ⇒ C f: A, B → C f: A, B → C (a:A)(b:B)⊢ C A B ⊢? C - - f:A → B f ()⇒A→B f:ε →…

Leanの学習の障害・壁、http://wwwf.imperial.ac.uk/~buzzard/docs/buzzard_big_proof2019.pdf からの引用： Type 1: Basic learning curve issues with the software. Type 2: Missing tactics (“Coq can do it but Lean can’t”). Type 3: Consequences of …

同義語 構造体＝レコード。これは便利だ。構造体型は帰納的型だから、データは帰納的データ。帰納的データ（＝帰納的型のデータ）は定義によりリテラル表示を持つ。リテラル表示のコンビニエンスとしていくつかの記法がサポートされている。 名前付きレコー…

システムの健全性 システムの十全性 システムの完全性 モデルと文の充足〈満足〉関係 文の充足可能性

論理 型 命題 型 命題Pの証明 型Tの式 証明内の根拠 式内の定数名 含意 関数型 前件 域型〈ソース型〉 後件 余域型〈ターゲット型〉 シーケント プロファイル 仮定 コンテキスト 結論 ターゲット 証明 証拠式 定理記述 オブジェクト定義 公理記述 定数宣言 …

論理： 矢印 左 右 含意〈implication〉 ⊃ 前件〈antecedent〉 後件〈succedent〉 伴意〈entailment〉→ 仮定〈assumption〉 結論〈conclusion〉 証明可能性〈be-provable〉判断 仮定〈assumption〉 結論〈conclusion〉 妥当性〈validity〉判断 モデル〈model…