アリーナ周り - (新) 檜山正幸のキマイラ飼育記 メモ編 も参照。以下はほぼ同義語： バンドル ファミリー コンテナ ファイバー付き集合 順序なしの低木林 低木林は低木〈シュラブ〉の林だが、 低木＝カローラ＝単頂点ループなし半グラフ＝付点有限集合 林＝…

finite-product-preserving functor をデカルト関手と呼ぶこともあるし、バンドルのデカルト射を保存する関手をデカルト関手と呼ぶこともある。 cartesian functor デカルト自然変換も、自然性四角形がデカルト四角形である自然変換と： cartesian natural t…

第一段階： 型＝集合、インスタンス＝要素、関数も（関数空間型の）インスタンス 第二段階： 型＝集合、型ファミリー＝関数、型ファミリーはインスタンスとは別 第三段階： 型は特殊な型ファミリー、インスタンス＝セクション 第四段階： 型＝型ファミリー …

本編（メリス／ジルバーガーの圏論的判断計算 - 檜山正幸のキマイラ飼育記 (はてなBlog)）で書いた文言： 非対称（対称とは限らない、しかし対称でもかまわない）色付きオペラッド〈non-symmetric colored operad〉 「色付き」も「色無しでもかまわない」も…

最外表明と対象化引用符 - (新) 檜山正幸のキマイラ飼育記 メモ編 で述べた最外表明、重要だ。命題を P として、肯定的最外表明 Holds P とする。命題を述語で対象化〈objectify | 具体化 | 客体化 | 物体化〉して、肯定的最外表明を等式で表わすと：True_X …

「集合の要素とモノイドの要素は違う、あるいは、モノイドは要素を持てないのではないか？」の背景として： 「彼の会社のビル」を「彼のビル」とは言わない。 「会社のビルの窓」を「会社の窓」と言ってもよい。 「ベクトル空間のスカラー体の要素」を「ベク…

「多義語」タグで、同義語、類義語も扱う。 音・綴・義 「綴」は「テツ」と読む。もちろん、文字にしたときの綴り〈つづり〉のこと。 同音異綴語 異義語：台集合、大集合〈large set〉 異義語：全順序集合、前順序集合 同義語： ベキ集合、べき集合、冪集合…

符号 負号

右随伴関手 随伴系の役割り名 左随伴関手のパートナー〈相方〉の意味。制限された系〈ペア〉での役割り名。二項関係の関与者役割り名＝二項述語の引数名 形容詞： 右随伴が形容詞。「随伴系が存在して、その右随伴関手となりえる」 レトラクト 埋め込みとレ…

めっちゃ美味しいごはん屋さんに行きたい。 「めっちゃ美味しいごはん屋」さんに行きたい。 めっちゃ「美味しいごはん屋さん行きたい」。

同義語句による置き換え〈replacement〉 例： pointing function ＝ example 変形ルールによる変形 例： example of type Nat named k → example k returns type Nat 省略可能な情報の省略と補完 例： type T → type T in U 注記情報の追加と削除（これも省…

記述の事例： 圏論/小さいとは限らない【形】 -(同義)→ 圏論/大きい 圏論/小さくない【形】 -(同義)→ 圏論/真に大きい 圏論/大きい集合 -(同義)→ 集合論/クラス 圏論/小さい集合 -(同義)→ 集合論/集合 圏論/小さくない集合 -(同義)→ 集合論/真のクラス 一般/…

厳密には同義語ではないが。 半辺 枝〈branch〉（望月） 開放辺〈open edge〉 非接続辺〈dangling edge〉 フラグ ダート 外線〈external line〉 外部辺〈external edge〉 テール 外フラグ〈outer flag〉 外部フラグ〈external flag〉 脚 ヘア〈毛〉 リード〈…

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

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

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

名前〈ラベル〉と型項のペアを型宣言、あるいは単に宣言と呼ぶ。型項は判断のパック形式〈packed form〉のことがある。したがった、判断も宣言にエンコード〈パッキング〉できる。宣言＝型宣言を束縛子ということもある。名前を型に束縛するから。しかし、名…

帰納的型の値コンストラクタ記号 帰納的型の型名は、パラメータを持つと型コンストラクタ 構造体型は、単一の値コンストラクタを持つ帰納的型だが、フィールド名をコンストラクタとも言う。 オブジェクト指向のコンストラクタは、単元集合またはパラメータ集…

postulate 公準 prerequisite 要請 assumption 仮定 antecedent 前件 premise 前提〈プロミス〉 hypothesis 仮説 context 文脈 environment 環境

axiom, constant, parameter, hypothesis などは同義語であり、どれを選ぶかは好みの問題。 axiom exclusive_middle {P :Prop} : P∧￢P → False : Prop constant exclusive_middle {P :Prop} : P∧￢P → False : Prop parameter exclusive_middle {P :Prop} :…

gitの誤認例：.gitignore, --squash - (新) 檜山正幸のキマイラ飼育記 メモ編 にて： 今まで、変な説明を見ても記録しなかったが、これからは記録に残そう。 https://qiita.com/ryosuketter/items/a6047b0270ea999fd51b 今回は、ステージングエリアから、ワ…

オブジェクトIDを何と呼ぶか？ ID ： 省略 オブジェクト ： 識別子と参照対象物を同一視 リビジョン番号 ： コミットオブジェクトの場合はそうなる コミット ： 識別子と参照対象物を同一視、かつ参照対象物が特定のタイプのとき SHA-1 ： オブジェクトIDの…

Σ〈$`\Sigma`$〉なんらかの意味の指標、D〈$`D`$〉はドクトリンだとして、$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\In}{ \text{ in } } \newcommand{\mrm}[1]{ \mathrm{#1} } %`$$`\quad \cat{C} = \mrm{Th}^D(\Sigma)`$とする。$`\cat{E}`$ を同…

終対象への唯一射や、単位対象への構造射 delete morphism descarder eraser discharger terminal morphism vanishing morphism bang garbage morphism（gs圏のこじつけ） counit もう一方の射は、 comultiplication duplicator copy morphism diagonal morp…

構文論： 基本概念 別名 ラベル 名前, 変数, 不定元, 定数, 識別子 シング n-射, もの, 実体, 具体物 割り当て 束縛, 代入, 関連付け〈association〉 リテラル 定数, 名前, 記号 コネクティブ 演算{子}?記号 コンビネーション 項, 式, 図式 ※ 論理のリテラル…

リテラルは、シングの束縛〈割り当て | 結びつき〉を持つ名前〈ラベル〉 宣言文は名前〈ラベル〉へのプロファイルの割り当て ソフト定義文は名前〈ラベル〉へのコンビネーション〈項〉の割り当て、マクロ・ラベルを生成する。 ハード定義文は名前〈ラベル〉…

名前とラベルは同義語。束縛と割り当ては同義語。広義のタイピングとプロファイリングは同義。束縛にはハード束縛とソフト束縛がある（後述）。 束縛される前のラベルは変数 ハード束縛された後のラベルはリテラル 束縛の種類： ハード束縛： 名前〈変数〉に…

とある論文で使っていた用語法： シーケントの左辺 ＝ antecedent〈前件〉 シーケントの右辺 ＝ succedent〈後件〉 イニシャルシーケント ＝ 公理シーケント シーケントの推論規則用語： 上式 ＝ premises〈仮定〉 下式 ＝ conclusion〈結論〉 前件、後件、…

https://arxiv.org/abs/2102.03044 の冒頭、同語義： {mathematical | logical | rigorous | formal | rational}* {derivation | proof} 単なる多義語ならいいのだけど、実際には曖昧語になっているのがタチが悪い。

まず、次は同義語扱いしたほうがいい。 変数の型宣言 型コンテキスト 0-指標 ポイント1-射だけの1-指標 構造体定義 レコード定義 テーブルスキーマ 例えば、 variable x, y : Real, c : Color type-context {x:Real, y:Real, c:Color} 0-signature _ { 0-mor…