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

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

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 （シーケント矢印は二重矢印）…

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

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

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

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 …

条件や性質〈命題〉の定義と、モノの定義は違う。モノを定義するとは、存在させる〈make it exist〉こと。 生成 構成的生成 超越的生成 正当化：存在命題 → スコーレム関数〈選択関数 | セレクター〉 正当化：一意性命題 → 一意値 条件確認〈検証 | 正当化〉

次は同義語 多相型 総称型 型構成子 パラメータ付き型 インデックス付き型 型ファミリー 適切な言葉は型値関数、使うのは型ファミリーにする。型ファミリーとは、Xを集合として、F:X → |C| という写像。Cの対象を型と呼べば、型値関数。X⊆|C| のときが総称型…

ツリーデータ型のモナドのモナドを具体的に書き下すととなると、けっこう難しいようだ。何が障害かというと： 型がうまく定義できない。 空型と単位型 部分集合型、内包的記法 ベキ集合型 直積型 指数型 直和型 依存和型 依存積型 型カインド 処理がうまく書…

コンピューターサイエンスの学習は、職業エンジニアになることを阻害する https://zenn.dev/nakanishi/articles/d3d8ff5529832f2acf6c 言っていることは正しいし、こういう意見の人はけっこう多いけど、まとまった文章がないから助かる。記事を消してしまう…

印象 連想 憶測 共感 信頼

日常的な言葉を用語にする。例：やせた、広い、大きい、理論、一様、単調、建物 難しい言葉・造語を用語にする。例： 亜真接続付き多様体、特恵近傍系、特殊フロベニウス代数装備圏 メリット デメリット 1 親しみやすい。簡単そうな印象を与える。 専門用語…

sumii先生情報： > 「2x」や「x^2」は「多項式」ではない、 知りませんでした。確かに謎ですね。

カーソルと削除キーの話で、ABC|DEF で、縦棒が文字カーソル〈カレット〉だとする。 BSはカーソルの前の文字（例のC）を消す Delはカーソルの後の文字（例のD）を消す ウーン、カーソルが左から右で進行するから、カーソルに乗り移って考えると、「Dが自分の…

正確には：

排他的否定、拡張的否定、制限的否定 - (新) 檜山正幸のキマイラ飼育記 メモ編 否定の接頭辞 un -- undecidable, uncurry 決定不能、反カリー in -- incomplete 不完全 non -- non-commutative 非可換 i -- irrational, irrelevant 無理数、無関連 de -- dec…

※ {パターン}! は、パターンのインスタンスから空文字列は除くことを意味する。 {事前|初期}{{確率}?{分布}}! P:1→* Θ による{統計 | 確率}モデル M:Θ→* X の{ベイズ}?反転〈{Bayesian}? converse〉を、F-P （）と書く。ドバーカットは、 。 同時{{確率}?{分…

「これからは通販で買い物、何でもオンラインだからなー」とか言っているオッサン（爺さんの僕よりは若い）が、タブレットの使い方を教わっていたのだが、次の概念（むしろ言葉）でつまずいていた。 URL 全角／半角 （ウゲッ） 戻る{ボタン}? UNDO DELETE サ…

プロファイルに関するアノテーションを括弧に入れて下付きとする。 P(X,Y) ： X×Y上の同時確率分布、プロファイルは 1→X×Y、(X,Y|) だけど、一部省略。 P(Y|X) ： XからYへのマルコフ核。プロファイルは X→Y、これを逆順（反図式順）に Y|X と書く。 P(X) ：…

次のどうってない公式が、実は重要だと気付いた。 For A, B⊆X, Δ-1(A×B) = A∩B （対角公式） 積事象が、A×B か A∩B かが不明なのは、この公式で同一視しているからだろう。A, B を可測空間Xの事象〈可測集合〉（シグマ代数の要素）だとして考えると次の可換…

Pは人の集まりで、“無作為な”標本抽出の確率分布μが載っている。3つの確率変数を、 そのときの年齢 a:P→N 身長 h:P→R 男女の別 g:P→{男, 女} として、同時確率変数 <a, h>, <a, g>, <h, g>, <a, h, g> などを考える。同時確率分布（無作為抽出測度の前送り）、部分周辺化＝条件周辺化、</a,></h,></a,></a,>…

同義語 同時 ＝ 積空間上の 例：同時分布 ＝ 積空間上の分岐 ＝ 積空間上の測度 周辺 ＝ 積空間の因子空間上の 条件付け〈conditioning〉／条件付き確率とは： 同時確率分布を、周辺事象で条件付けて、周辺確率分布を作ること。そうやって作った周辺確率分布…

確率の話 有限集合の話 測度論 全事象 有限集合 X 集合 X (暗黙) ベキ集合 Pow(X) シグマ集合代数 ΣX (暗黙) (暗黙) 測度空間 (X, ΣX) 事象 Xの部分集合 A∈Pow(X) 可測集合 A∈ΣX 確率 確率加法的関数 μ 確率測度 μ 同義語と省略 分布 ＝ 測度 例：質量分布 …

「非」、「不」、"un", "in", "non-" などの否定の接頭辞の用法： 大きい集合＝非小集合、非ハウスドルフ空間、不連続関数、非コンパクト集合などは排他的否定になる。 非可換環は、可換環の拡張概念になる。 非確率的写像は、確率的写像の制限概念になる。…

STEMコミュニケーション論は「わかりにくさ」の研究だが、わかりにくさの原因が伝達手段／言語的コミュニケーション側にある場合を対象にする。個別的な現象を列挙すると： 形式的意味、心理的意味、辞書的意味の三者の乖離や相互干渉 辞書的意味＝自然言語…