terminology 構造的データ /* 参考： * セクションとタプル https://m-hiyama.hatenablog.com/entry/2022/06/14/153042 */ vocabulary 構造的データ-明確 { {インデックス付けられた}?集合族 インデックス集合 定数値の集合族 インデックス集合の要素 集合族…

terminology _ vocabulary 論理-明確な語句 { 述語記号 真偽値集合の要素 集合圏の真偽値集合のn-直積を域として真偽値集合を余域とする射 集合圏の特定対象のn-直積を域として真偽値集合を余域とする射 集合圏の真偽値集合を余域とする射 自由変数を含む古…

terminology _ vocabulary 圏と射-統一的 { 0-圏 1-圏 0-圏の0-射 0-圏の1-射 1-圏の0-射 1-圏の1-射 1-圏の恒等1-射 1-圏の2-射 } context 圏と射-常識的 for 圏と射-統一的 { 集合 := 0-圏 圏 := 1-圏 集合の要素 := 0-圏の0-射 集合の要素の等値性 := 0-…

後で資料にする。 terminology 述語と関係 vocabulary 論理の述語 { 0項述語 1項述語 2項述語 無項述語〈nulary predicate〉 単項述語〈unary predicate〉 二項述語〈binary predicate〉 n項述語 述語 /* ボキャブラリー内部の同義語指定にはイコール */ 0項…

随時追加変更 Submitted: 1 May 2013 Title: The operad of wiring diagrams: formalizing a graphical language for databases, recursion, and plug-and-play circuits Author: David I. Spivak URL: https://arxiv.org/abs/1305.0297 PDF: https://arxiv.…

vocabulary of (predicate)s 多様体 { 境界を許す広義多様体 境界を許さない狭義多様体 } context Extended for 多様体 { 多様体 := 境界を許す広義多様体 境界無し多様体 := 境界を許さない狭義多様体 境界有り多様体 := 境界を許す広義多様体 ∧ ￢境界を許…

descriptionモジュールとterminologyモジュールにするか。モジュール名・名前空間があるが、description〈desc〉とterminology〈term〉は異なる名前空間〈名前コンテンナ〉。 description TransitionSystem signture RightTransitionSystem within (C in Mon…

module TransitionSystem signture RightTransitionSystem within (C in MonCAT) { sort A sort S operation t: S×A → S } signature DetTransitionSystem := TransitionSystem within Set signature ParTransitionSystem := TransitionSystem within Partia…

指標による定義： module TransitionSystem signture RightTransitionSystem within (C in MonCAT} { sort A sort S operation t: S×A → S alias alphabet := A alias state-space := S alias right-transition := t alias transition := right-transition }…

vocabulary Panda { パンダ レッサーパンダ ジャイアントパンダ } context Now for Panda { パンダ := ジャイアントパンダ レッサーパンダ := レッサーパンダ _ := パンダ } context Old for Panda { パンダ := レッサーパンダ _ := ジャイアントパンダ _ :=…

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

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

Title: Shapely monads and analytic functors Authors: Richard Garner, Tom Hirschowitz Submitted: 18 Dec 2015 (v1), 10 Oct 2017 (v3) Pages: 52p URL : https://arxiv.org/abs/1512.05980 多項式の一般化。多圏と類似物がまとめてあるのがいい。多射に…

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

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

ワイヤリング図 ケリー／マックレーン・グラフ ボックス ライン〈棒〉 入力ピン マイナス頂点 出力ピン プラス頂点 ワイヤー 有向辺 内部ワイヤー 横方向辺 公開ワイヤー 縦方向辺 ボックスの自己ループは、同一線〈棒〉内リンク（辺）となる。分岐するリン…

共通する発想： 個体〈モノ〉は世界全体との関係性においてしか理解できない。 集合論： モノ〈集合〉 $`a`$ が分かる ⇔ 宇宙内の任意のモノ $`x`$ に対して $`x\in a`$ かどうか完全に判断できる。 圏論： モノ〈対象〉 $`a`$ が分かる ⇔ 圏内の任意のモノ …

圏論 プログラミング 対象 型 射 関数、手続き、etc. (無名 1) 型構成子 関手 (無名 2) (無名 3) アドホック多相関数 自然変換 パラメトリック多相関数 備考： (無名 1) は、対象構成子または単に構成子〈コンストラクタ〉と呼べばよい。拡張スタイルのモナ…

教育的に不可避な方便 回避可能な嘘 儀礼的な〈お約束としての〉嘘 ： 厳密には嘘だが、ほとんど慣例化している表現。 例： 集合Gは群とする。 弾力的な嘘 ： 解釈側が文脈を考慮しながら弾力的に解釈すれば意味が通じると期待できる表現。例： ツリー状のス…

ファミリー／バンドル同型定理 $`\quad {\bf CAT}(\delta A, {\bf Set}) \cong {\bf Set}_{/A} \text{ in }{\bf CAT}`$対象部分だけを取り出すと：$`\quad \mathrm{MAP}(A, |{\bf Set}|) \cong |{\bf Set}_{/A}| \text{ in }{\bf SET}`$対象部分を別表記を使…

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

以下、https://arxiv.org/pdf/0706.1033.pdf （「コック達論文」として言及）のズーム複体を見ていて、思ったこと； ゲンツェンのNK証明図とLK証明図の関係がストリング図とメタストリング図の関係として説明できるだろう、ということ。まず、コック達論文用…

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

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

型無し演算子指標は untyped operator signature だが、untyped ＝ single sorted 。また、演算子は代数的指標の演算〈operation〉。したがって、 op:(S, ..., S) → S と書ける。通常のプログラミング言語と同様に引数変数を使うと、 op: (a:S, ..., z:S) → …

次の可換図式がある。$`\require{AMScd} \begin{CD} |{\bf FinSet}| @>{\mathrm{card}}>> {\bf N}\\ @AAA @AAA \\ |{\bf ThinSet}| @>{\mathrm{IsNonEmpty}}>> {\bf B} \end{CD}\\ \:\\ \text{commutative in }{\bf SET}`$やせた集合は空集合または単元集合…

型： String: 文字列、特にバリデーション〈検査〉しない。 MailAddr ⊆ String: バリデーションする。 ZipCode ⊆ String: バリデーションする。 旧スキーマ： ( givenName : String, familyName : String, mailAddr : MailAddr, userId: String, geoAddr : S…

集合 A の要素の順列の個数と、集合 A の分割〈パーティション〉に順番〈全順序〉を付けたモノの個数は同じ。だが、解釈が違う。以上の事実は、バンドルの移送方向（前送り〈押し出し〉か引き戻し）に関して基本的な見方を与える。同様に、組み合わせ的な議…

n-圏の離散化持ち上げ〈discretization {lift | promotion | ascent}〉をδ、打ち切り引き下げ〈truncation {fall | demotion | descent}〉をτとすると。$`\quad {\bf SET}(A, \tau {\bf Set}) \cong \tau {\bf CAT}(\delta A, {\bf Set})\text{ in }{\bf SET…

書き方と印象。文字は変えない。 $`(f_i:A_i \to B_i)_{i\in I}`$ まー、写像の族だわな、うん。 $`(f[i]:A[i] \to B[i])_{i\in I}`$ スキーマ〈集合の配列〉 A とスキーマ〈集合の配列〉 B のあいだの値変換に見える。$`i\in \{1, 2, 3\}`$ とか。 $`(f_i:A…