ラムダ図は、ラムダノードとワイヤーからなる。 ラムダノードは三角または台形で描く。 ノードに接合するワイヤーには、入力ワイヤー（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…