思い付いたことを順不同にダダーっと箇条書きにする。後で整理する。まだごった煮。先に意味領域： 集合の集合がある。小さい具象圏の対象集合 ＝ Type ＝ |Sem| 0, 1 はType内にある。0, 1∈Type 型がAの個体〈individual〉とは、1からのAへの射のこと。 関…

論理AND、合接、論理積、連言、コンジャンクション 論理OR、離接、論理和、選言、ディスジャンクション 論理NOT、否定、{ニ | ネ}ゲーション 含意、条件{法}?、インプリケーション 多義語： 矛盾： 矛盾命題＝偽命題＝偽的命題〈falsy prop.〉、演繹システム…

言語・習慣・文化のせいで、せっかくの原則がうまく使えない例がカリー／ハワード対応。なんとかしてキレイに整理する。演繹システムでは不明瞭で、プログラミング・システムでは明瞭な概念： システム組み込み vs ユーザー定義 ライブラリによるシステムの…

http://d.hatena.ne.jp/m-hiyama-memo/20181102/1541141733の最後の余談を敷衍する。domain of discourse の訳語に論域を使う。すると、命題関数の域は論域となる。「論域＝命題関数の域」で事情が少しハッキリする。シーケントにおける自由変数の指定は、論…

記法バイアスと記法独立な把握： 順序随伴を例として - 檜山正幸のキマイラ飼育記では、 標準的テキスト記法の強烈なバイアスに支配されている、あるいは記法の獄舎に投獄されているからです。 自ら「記法の獄舎」に閉じこもりたい傾向（思考、指向、嗜好）…

結局、多義語の意味をキチンと区別して分解して丁寧に解釈する。関数： 関数 基本テキスト 定義したテキスト 符号 名前 基本関数名 関数名 エントリーポイント／インデックス 関数記述 - ラムダ関数項 関数オブジェクトコード 関数本体式 - 項 関数本体コー…

関数名＝関数記号＝関数インデックス＝エントリーポイント 関数＝関数実体＝関数名の意味＝写像 関数定義＝関数の定義体＝関数のソースコード＝関数のテキスト＝関数の式 関数コード＝コンパイルされた関数＝バイナリの関数＝関数のオブジェクトコード 関数…

まず、同義語のまとめ。 指標⊆仕様＝セオリー＝プレゼンテーション＝コンピュータッド＝ポリグラフ＝グラフ＝箙 モデル＝構造＝代数＝加群＝表現 基本構図は： A ∈0 n-AlgD(τ, A) これの文脈は、 τ ∈0 n-Thy D ∈0 (n+1)-Thy A ∈0 (n+1)-AlgD'(τ', A') 文脈内…

高次圏論的な指標の理論 - 檜山正幸のキマイラ飼育記 メモ編で挙げた類義語に追加して再掲。 指標 コンピュータッド ポリグラフ グラフ 箙 プレゼンテーション 仕様 セオリー スキーマ モデル 代数 加群 表現 マシン インスタンス ドクトリン ブランド フレ…

ε ヒルベルトのイプシロンε 空文字列ε イプシロン・デルタのε （正実数） 余単位のε evalのε モノイド関手のε ε:I→F(I) エディントンのイプシロンε δ クロネッカーのデルタδ 対角集合の特徴関数のδ （クロネッカーのデルタの真偽値版） 対角・分岐のδ（特に…

古式テンソル〈old-style tensor〉 極性付き複行列 非モダンテンソル〈nonmodern tensor〉 混合テンソル代数の要素 モダンテンソル〈modern tensor〉 テンソルの多圏の射 行列を極性付き複行列に埋め込むには、Mat(A, B) → MMat(B, A#) を使う。全体的に絵図…

a:I→X がindexed basisだとは、aの線形拡張a~が全単射線形写像になること。 Iをindex set、aをindexingと呼ぶ。 IがXの部分集合で、aが包含写像のとき、self indexingまたはdirect indexingと呼ぶ。 IとJのあいだに集合同型 s:I→J があって、<:b(s(j))|a(i)> = δ(i, j) が成</:b(s(j))|a(i)>…

テンソル積空間を特徴づける双線形 τ:X×Y→XY を構造写像と呼ぶ。 XY, τ(x, y), τ(A×B) に同じ記号（xy, AY）が使われる。概念的に区別せよ。 双対基底、双対フレームが、「双対ではない」ことを強く注意すべき。 双対フレーム{射}?は、フレーム射の双対の逆…

図そのものより、図示の基礎を書く。デカルト閉圏Cを固定して、I := IdC、直積を∧、単位を1、始対象を0とする。Δ:C→C×C はコピー、Πi:C×C→C は射影、K:C→I は一点への潰し、S:C×C→C×Cはスワップ。 自然変換 自然変換の記号 プロファイル 名前 略称 ι I⇒I 恒…

形式(的)?体系 {形式(的)? | フォーマル}{体系 | システム} {形式(的)? | フォーマル}?{体系 | システム}

defintion and example - 檜山正幸のキマイラ飼育記 メモ編 同義語・多義語の例 - 檜山正幸のキマイラ飼育記 メモ編 指標とモデルと意味論 - 檜山正幸のキマイラ飼育記 メモ編 代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編 決める側…

coherence {axiom | equation | relation | identity | constraint | law} {一貫性 | 整合性}{公理 | 等式 | 関係 | 恒等式 | 制約 | 法則}

{definition (form)? | specification | signature | (type)? class | interface | concept} {example | model | (type)? instance | structure | implementation | class | algebra}

表記のゆれも考慮すると、用語表記は爆発する、という話。 https://ncatlab.org/nlab/show/Lawvere+theory 考えられる表記は、まず、 {代数的 | ローヴェル}{理論 | セオリー} 「ローヴェルの代数的セオリー」もある。「的」の有無もあるから、 {代数(的)? |…

愚痴： さまざまな「ならば」達 - 檜山正幸のキマイラ飼育記 文字や記号はいつだって足りないのだ - 檜山正幸のキマイラ飼育記 論理記号のいろいろ - 檜山正幸のキマイラ飼育記 型推論に関わる論理の概念と用語 その1 - 檜山正幸のキマイラ飼育記 絵算（スト…

ステイ／メリディスの次の論文、とても良い。 Title: Logic as a distributive law Author: Mike Stay, Lucius Gregory Meredith URL: https://arxiv.org/abs/1610.02247 僕がふだん考えていることだから、問題意識が一致して分かりやすい。本論じゃないとこ…

昨日 代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編、次の用語を導入した。当たり前で自己説明的な言葉だと思う。 (n-)?代数(的)?定義(形式)? (n-)?定義(形式)? 同義語が： (n-)?指標 (n-)?仕様 (n-)?セオリー (n-)?型クラス (n-)?イ…

内容： 代数的定義形式 代数的定義形式の同義語群 アンビエント 定義形式のアンカリング 単位対象と格上げ 値k-射と定義形式の格上げ モデルとモデルの圏 TBD：ローヴェル・フレームワーク TBD：族と抽象と脱抽象 代数的定義形式n-圏と関連する圏論的実体〈c…

システム全体もひとつの指標を持つから、それをシステム指標と呼び、Ωで表す。システム指標に含まれる名前はso-called大域名で、いつでもどこからでも自由に参照できる。システム指標Ωの環境（文脈）下にあるトランスフォーマーtを次のように書く。 Ω| t:Σ→Γ…

「公式」はよく使う言葉だが、意味わからん。公式＝オフィシャルは入れない。日本語群 公式 等式 恒等式 定理 命題 英語群 formula equation identity theorem proposition これらを同義語か異義語かで分類しようとすると、困ったことになる。

オブジェクト：オブジェクト指向、レコードデータ、圏論、アトム付き集合論でアトムまたは集合 クラス：オブジェクト指向、集合論の類、型クラス インスタンス：オブジェクト指向、集合・類の要素、データベーススキーマの状態、一般の状態空間の状態 分布：…

タプルとリレーション - 檜山正幸のキマイラ飼育記 メモ編も参照。 構造体〈ストラクチャ〉のメンバー レコードのフィールド リスト／配列の項目〈アイテム〉 タプル／ベクトルの成分 名前・値ペア-集合〈set of name-value pairs〉の要素 辞書〈ディクショ…

追加 削除 変更 まとめて SQLコマンド INSERT DELETE UPDATE ここでの用語 insert delete modify update CRUD create delete update 追加（＝挿入）操作で表すこと： 誕生、発生、参加、加入、 削除操作で表すこと：死滅、消滅、退去、脱退、退出 変更操作で…

適切に語るべき言葉が（通常の日本語のなかでは）見つからないので、人工的な表記を導入するしかない。同義語の併記専用に、山形括弧（'〈'と'〉'）と縦棒（論理OR記号）を使う。 魑魅魍魎〈ちみもうりょう〉が跋扈〈ばっこ〉する。 一意識別子〈識別子 | ID…

方言識別マーカー 長い名前 代替語の使用 同義語併記 異義語併記 方言識別マーカー 特定分野の方言はそれと分かるようにマークする。例： 《タプル》 《リレーション》 長い名前 多義語の片方（あるいは両方）を形容詞・副詞で修飾する。 線グラフと関数グラ…