アルファベット アルファベットの要素： {アクション | 入力 | 刺激}?{ラベル | レター | 記号 | シンボル | 信号}、インストラクション{記号 | ラベル | ニモニック}? 遷移、作用、実行 遷移系、マシン、エンジン 状態{空間 | 集合} ムーブ、ムーブペア、ム…

穴あきストリング図 ケリー／マックレーン・グラフ 多様体 ボックス＝サークル バー＝ストリング 境界 ポート＝ピン 符号、符号付き色 境界条件 ワイヤー リンク 複体構造のセル ワイヤリング リンキング 球体と同相の多様体（ボール、ブロブ）の境界（球、…

ドット＝ポート＝ピン＝ソケット＝スロット エッジ＝アーク≒ワイヤー≒ケーブル＝バス ボックス＝サークル＝スフィア≒カローラ＝ブーケ≒インターフェース 入れ子ダイアグラム＝星座＝メタツリー オープンエッジ≒ハーフエッジ＝ダート＝フラグ

僕はA案だが。 A案 B案 C案 指標 指標 セオリー セオリー セオリー 代数 モデル 代数 モデル

置換〈substitution〉 展開〈expansion〉 穴埋め〈fill-in〉 ズームイン〈zoom-in〉 分析〈analyze〉 逆は 縮約 折りたたみ ズームアウト ブラックボックス化

元の概念（例：多様体） そこからはみ出した概念（例：境界を考える） 2つの排他的概念（例：境界無し、境界あり） 元の概念の再確認（例： 境界無し） 統合した概念（例：境界があってもなくてもよい） 実例 1： 多様体 境界付き多様体 多様体と境界付き多…

同義語、曖昧多義語が多いのを利用して、連想ゲームをする。「代入」の用法： 上書き割り当て〈overwrite assignment〉 手続き型プログラミング言語の代入文 束縛〈binding〉 関数型プログラミング言語の let, where など 置換〈substitution〉プレースホル…

縦方向が同義語。 番号 構造 下側 下側要素 縦線 縦線要素 1 アリーナ 位置集合 位置 方向集合 方向 2 林 根集合 根 低木 葉 3 コンテナ 形状集合 形状 位置集合 位置 4 型ファミリー インデックス集合 インデックス 型 インスタンス 5 バンドル ベース空間 …

無名： 集合 要素 型 インスタンス 空間 点 関係 ? 写像 ? 写像の要素相当概念は、呼び出し／発動〈call | invocation | インボケーション〉と呼ぶことにする。関係のインスタンスは、RDFでは (a, b)∈R を (a, R, b) と書いてトリプルと呼ぶ。 関数の呼び出…

「シェープ」の意味が曖昧 直感的な意味での形状。ツリーやバンブーなどのグラフと思ってよいので、形状グラフ。 形状グラフのラベル 形状グラフのポジション集合 形状グラフとボジション集合の組（構造） ラベルとボジション集合の組（構造） 当初は形状グ…

hugoのタクソノミーの説明 - (新) 檜山正幸のキマイラ飼育記 メモ編 再度。 RDF用語 Hugo用語 普通の言い方 主語 値 {二項}?関係の域の要素 述語, プロパティ タクソノミー {二項}?関係 目的語, (値 | ターゲット) ターム {二項}?関係の余域の要素 毎度毎度…

ポインティング対象（始対象または単位対象）からの射を[!状態]または[!ポイント]と呼ぶ。 真偽対象への射を[!述語]と呼ぶ。 ポインティング対象への射を[!余ポイント]。 真偽対象からの射はあまり問題にしない。 時間的に変動するナニカの時点スナップショ…

ボキャブラリー（タームの集まり） タームが多義語だから笑っちゃう スキーマ オントロジー レキシコン ディクショナリ シソーラス コーパス タクソノミー ノーメンクレイチャー

データベースへの操作で： 用法その1 update ： レコードの値を変更する modification ： update, create, delete 用法その2 update ： modification, create, delete modification ： レコードの値を変更する ちなみに、modification は 2-transfor だし。

[クラス=学級] [クラス=組] [クラス=授業] [クラス@日常] [(クラス=階級)@日常] [クラス@教育] [クラス@オブジェクト指向言語] [クラス@OOP] [クラス@関数型言語] [クラス=型クラス] [クラス@集合論] [クラス@数学] [クラス=真のクラス] [クラス=真のクラス=…

話が通じない原因が全単射と可逆写像を別物だと思っていたことだった。たくさんの言葉があると、すべて同義語とは判断しにくいらしい。 全単射 双射 バイジェクション 可逆{写像 | 射} 同型{写像}? 1：1対応

可換モノイドは、モノイドの☓☓☓に加えて、◯◯◯の☓☓☓を付け加えて定義される代数系である。 ☓☓☓ 公理 等式 法則 条件 性質 〇〇◯ 交換法則 可換律 可換性 演算の交換可能性

多プロファイル 成分・書字順 成分・反書字順 成分・カリー化 f: → X f(*, x) f(x | *) f()(x) f: X → f(x, *) f(* | x) f(x)() f: → X, Y f(*, (x, y)) f(x, y | *) f()(x, y) f: X, Y → f(​(x, y), *) f(* | x, y) f(x, y)() f: X → Y f(x, y) f(y | x) f(…

論理的形容詞 測度 非負実数値関数 テンソル〈多行列〉 (無し) 準確率測度 準述語 準マルコフ・テンソル 規格化 確率測度 規格化述語＝単位述語 マルコフ・テンソル 劣規格化 劣確率測度 述語＝ファジー述語 劣マルコフ・テンソル シャープ シャープ測度 古…

曖昧多義語の例：確率変数 単なる可測写像 確率空間からの可測写像 確率空間のあいだの測度保存写像 特に、同時確率分布の射影写像 確率空間、または確率空間の台集合を変域とする変数 確率測度 標本空間 可測空間 可測写像の域 可測写像の余域 確率空間の台…

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, この言い回しにはさんざん悩まされた。「ゴール」に意味が。 証明状態 メインゴール …

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

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:ε →…

http://watanabe-www.math.dis.titech.ac.jp/users/swatanab/Renshu_0.pdf このテキストでは、確率分布＝確率変数による前送り測度。確率変数は、確率空間（の台可測空間）からのRへの可測写像。

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

「用語ペアの関係性」の続き。 ⊆： 包含的 ⊆→ ： 規準的埋め込み可能 ⊥： 排他的 ∪： 総称 環、可換環、非可換環 用法 1： 環 ＝ 可換環 ⊆ 非可換環 用法 2： 可換環 ⊆ 非可換環 ＝環 用法 3： 可換環 ⊥ 非可換環、環 ＝ 可換環∪非可換環 数、単項式、多項式…

まだまだ改善の余地がある。コンパクト論理に限定するとして、 論理式＝生成対象の集合 F から作った自由コンパクト圏 原子証明＝生成射＝シーケントの集合 S から作った自由コンパクト圏 コンパクト圏〈コンパクト閉圏〉は、射の同値書き換え〈equivalent r…

形式的に定義しない言葉 証明 → 証拠{図 | 式}またはリーズニング{図 | 式} 公理 → 原子定理 命題 → 論理式、定理 推論、推論規則 → 原子証拠{図 | 式}、原子リーズニング{図 | 式} 形式的に定義する言葉 項、原子項 論理式、原子論理式 文脈 シーケント 証…

多義語・曖昧語がオーバーロードのときもあれば、総称のときもある。オーバーロードと総称の境界はハッキリしない。 総称語は全体を意味するのであって、個別ケースにはあまり使われない。 オーバーロードされた語は個別ケースに使われるが、複数ケースで同…

「原子」「複合」 を使う。次の表の欄に入る語は正式なテクニカルタームとして定義する。 原子 (複合) 構成規則 項 論理式 証明 リーズニング リーズニングが一番ゴタゴタで、 証明{図}?の構成規則の概念とかぶる。 コンビネータ由来のリーズニングと、2-射…