圏論 vs 順序論

大きかも知れない圏の2-圏 順序集合の圏
余完備な余デカルト圏 順序完備なミート半束
余連続な自己関手 連続な自己関数
自然変換 関数順序
自己関手のランベック代数 自己単調関数の劣不動点
モナド 閉包作用素
モナドのアイレンベルク/ムーア代数 閉包作用素の不動点
自己関手の自由モナド 自己単調関数の不動点関数
自由モナド生成関手 不動点オペレーター
圏論的不動点方程式 順序論的不動点方程式
圏論的不動点不等式 順序論的不動点不等式
自由忘却随伴系 ガロア接続

$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\In}{\text{ in } }
\newcommand{\twoto}{ \Rightarrow}
%`$

以下の表で、要素順序〈射〉は矢印、関数順序〈2-射〉は二重矢印で示す。アイレンベルク/ムーア代数の構造射にはダッシュを付けて目印にする。ホムセットを単に丸括弧で略記する。

$`{\bf CAT}\in |2\mathbb{CAT}|`$ $`{\bf Ord}\in |2{\bf CAT}|`$
$`\cat{C} \in |{\bf CAT}|`$ $`L \in |{\bf Ord}|`$
$`f:A \to B \In \cat{C}`$ $`a \to b \In L`$
$`F:\cat{C}\to \cat{C} \In {\bf CAT}`$ $`f: L\to L \In {\bf Ord}`$
$`[\cat{C}, \cat{C}]\in |{\bf CAT}|`$ $`[L, L] \in |{\bf Ord}|`$
$`\alpha ::F \twoto G : \cat{C}\to \cat{C}\In {\bf CAT}`$ $`f \twoto g :L \to L \In {\bf Ord}`$
$`\alpha :F \to G \In [\cat{C}, \cat{C}]`$ $` f\to g \In [L, L]`$
$`\mrm{LamAlg}(F) \in |{\bf CAT}|`$ $`\mrm{Prefix}(f) \in |{\bf Ord}|`$
$`(A, \alpha) \in |\mrm{LamAlg}(F)|`$ $`(a, f(a) \le a)\in |\mrm{Prefix}(f)|`$
$`\mrm{Mnd}(\cat{C}) \in |{\bf CAT}|`$ $`\mrm{Clop}(L) \in |{\bf Ord}|`$
$`M \in |\mrm{Mnd}(\cat{C})|`$ $`m \in |\mrm{Clop}(L)|`$
$`(A, \alpha') \in |\mrm{EMAlg}(M)|`$ $`(a, m(a) = a) \in |\mrm{Fix}(m)|`$
$`\mrm{EMAlg}(M) \in |{\bf CAT}|`$ $`\mrm{Fix}(m) \in |{\bf Ord}|`$
$`\mathscr{F} F \in |\mrm{Mnd}(\cat{C})|`$ $`\mu f \in \mrm{Clop}(L)`$
$`\mathscr{F}:[\cat{C}, \cat{C}] \to \mrm{Mnd}(\cat{C})`$ $`\mu: [L, L] \to \mrm{Clop}(L)`$
$`\mathscr{U}:\mrm{Mnd}(\cat{C}) \to [\cat{C}, \cat{C}]`$ $`\xi : \mrm{Clop}(L) \to [L, L]`$
$`\mathscr{F} \dashv \mathscr{U}`$ $`\mu \dashv \xi`$
$`(\mathscr{F}F, M) \cong (F, \mathscr{U}M)`$ $`(\mu f, m) = (f , \xi m)`$

レンズ用語

  1. 困っている。
  2. 何がプレーンレンズ〈バニラレンズ〉か分からない。
  3. 元祖レンズの有法則/無法則は、まーハッキリしている。
  4. 単相レンズ〈monomorphic lens〉と双相レンズ〈ニ相レンズ | bimorphic lens〉の区別はあるが、一般的とも言えない。ヘッジーズ〈Headges〉の用語。
  5. 単相レンズ=元祖レンズ だと思ってよい。
  6. 双相レンズ=ニ相レンズを双方向レンズはマズかったと思う。
  7. レンズの圏の対象はインターフェイスとかバンダリーとも言うようだ。
  8. インターフェイス〈バンダリー〉が (A, A) である圏の射が単相レンズで、(A, B) である圏の射が双相レンズかな。
  9. 「read/writeパート」、「forward/backward」パートは使われている。
  10. オプティックは残余〈residual〉で記述される。残余は内部記憶になる。フォワード通過時に残余に内部記憶が生成されて、バックワード通過時に記憶が使用される。
  11. mixed optic のフレームワークでは、フォワードパートの圏 $`\mathcal{C}`$ とバックワードの圏 $`\mathcal{D}`$ と残余の圏 $`\mathcal{M}`$ が出てきて、$`\mathcal{M}`$ が作用域となるアクテゴリ構造を持つ。
  12. 本編記事だと、「具象レンス vs 抽象レンズ」「具象オプティック vs 抽象オプティック」の分類もしていた。
  13. 具象レンスの圏は $`{\bf ConcLens}`$
  14. フォワードパートを 1stパート、バックワードパートを 2ndパートとも呼ぶが、もちろん恣意的。
  15. F-レンズは、インデックス付き圏 F から誘導されるスピヴァックのレンズ概念。後日、関手レンズ〈functor lens〉、グロタンディーク・レンズとも呼ばれるようになった。
  16. パラメータ付き射〈{parametric | parametesized} morphism〉と余パラメータ付き射の概念を導入する。混合オプティックは、残余のパラメータ付き射、余パラメータ付き射のペアになる。
  17. op が結合の反対圏、co がモノイド積の反対圏。
  18. 依存レンズとは、スピヴァックのF-レンズ(グロタンディーク・レンズ)のFを局所デカルト圏のスライシングにしたもの。
  19. 結果的に、自分が今使っている「依存レンズ」は集合圏ベースの依存レンズ、しいて言えば具象依存レンズ〈concrete dependent lens〉。
  20. 依存オプティックは非常に複雑な概念だ。

続・表計算

そうそう、セルに型が付くのだった。セルに型フィールドと値フィールドがある。

特定番地のセルのフィールドに値が入っていることを

$`\quad \text{A2.Val} = 7\\
\quad \text{A2.Typ} = {\bf N}
%`$

まとめて

$`\quad \text{A2} = (7 : {\bf Nat})`$

次の機能がある。

  • 型推論
  • 明示的な型の指定
  • 明示的型指定による型チェック
  • 型指定の自動化

ガジェット設定の例

$`\quad \text{A1.Typ} = X\\
\quad \text{A1.Val} = ?\\
\quad \text{B1.Typ} = Y\\
\quad \text{B1.Val} = f(\text{A1.Val})\\
\quad \text{A2.Typ} = F(\text{A1.Val})\\
\quad \text{A2.Val} = \varphi_{\text{A.1.Val}}(\text{B2.Val})\\
\quad \text{B2.Typ} = G(\text{B1.Val}) \\
\quad \text{B2.Val} = ?
%`$

A1.Val と B2.Val がユーザー入力で、A2.Val が計算結果。

依存関数

  1. 型ファミリーのセクション $`x \in \mathrm{Sect}(\pi:\Sigma(I, F) \to I) = \Pi(I, F)`$
  2. 関数型ファミリーのセクション $`x \in \mathrm{Sect}(\pi:\Sigma(I, [F, G]) \to I) = \Pi(I, [F, G])`$

一番は依存リストで、ニ番はインデックス付き関数〈indexed function = indexed family of functions〉だな。

  1. 値-indexed 値 = 関数 $`X \to Y \text{ in }{\bf Set}`$
  2. 値-indexed 型 = 型ファミリー $`X \to |{\bf Set}| \text{ in }{\bf SET}`$
  3. 型-indexed 型 = 総称型、型構成子、型レベル関数 $`|{\bf Set}|\to |{\bf Set}|\text{ in }{\bf SET}`$
  4. 値-indexed 関数 = 高階関数(の一種)、反カリー化して多変数関数 $`X \to Z^Y\text{ in }{\bf Set}`$
  5. 型-indexed 関数 = 多相関数 $`|{\bf Set}| \to \mathrm{Mor}({\bf Set})\text{ in }{\bf SET}`$
  6. 関数-indexed 関数 = 高階関数(の一種)、作用素 $`Y^X \to T^S \text{ in }{\bf Set}`$
値-indexed 関数-indexed 型-indexed
関数 汎関数 ?(例:デフォルト)
関数 高階関数 高階関数〈作用素〉 多相関数
ファミリー ?(例:域、余域) 型構成子

例え話に表計算

ヒエー、僕は使ったことない。

  1. 表計算ソフト〈スプレッドシート〉が便利なのは、入力に対する自動計算/自動再計算をやってくれるから。
  2. 高機能かつDomainSpecificな電卓〈カリキュレーター〉として使える。
  3. セル番地は A1, C30 のように英字と数字の並び、英字部分が横座標(列名)、数字部分が縦座標(行番号)。
  4. スピヴァックは、複数のセルと関数から作った機能的かたまりをガジェットと呼んでいた。
  5. つまり、シート内にガジェットを配置する。計算ガジェットと呼ぶといいだろう。
  6. 「=式」と入力すると計算値が得られる。
  7. 式内のセル番地参照はコピーされると相対的な位置関係から書き換えが起きるらしい。つまり、自分自身からのオフセット座標と、シートの絶対座標がある。
  8. 絶対座標指定は、$A$1 のようにドル記号をつける。何も付けないと内部的にオフセット参照と解釈されている。オフセット座標は (-3, +1) とか書けばいいか。
  9. 構文論と意味論が作れそう。

構文論:

  1. 値リテラル
  2. 絶対セル番地
  3. 相対セル番地=オフセット座標(基準セル必要)
  4. 絶対セル範囲式
  5. 相対セル範囲式(基準セル必要)
  6. 名前(式に束縛される)
  7. 算術演算子
  8. 範囲演算子
  9. 論理演算子
  10. その他の関数
  11. 束縛 : 絶対番地 = 式
  12. 状態 : 束縛の集合、シートのセルに対する式の割り当て
  13. ガジェット: シート状態から作る入出力を持つオートマトン

意味論はガジェットの意味論を展開したほうが有意義だろう。ガジェットは、入力に対して、そのときの状態に応じた出力を計算する。ガジェットは、シート束縛状態に入力セル群と出力セル群を指定して定義できる。

ベテラン(?)の意見

Quoraの「TypeScriptって気持ち悪くないですか?」なる質問に、以下のコードと共に:

Aだと変数aに代入するときにエラーにならないのですが、Bだと変数aに代入するときに型のエラーになるんです。
え、なんで?同じ動きしているはずなのに。

    const getA = () => { 
      return 123; 
    } 
     
    const isString = (v: any) => { 
      return typeof v === 'string'; 
    }; 
     
    let a: string | null; 
     
    const main = () => { 
      const _a = getA(); 
     
      // if (typeof _a !== 'string') { return; }  // A エラー
      if (!isString(_a)) { return; }  // B OK
     
      a = _a; 
     
      console.log(`${a}`); 
    }; 
     
    main(); 

なるほど(苦笑)。

次の文言もよくある。「開発言語/開発ツールなんてどうでもよくて、成果物が問題」という論法。

TypeScriptの装飾って開発者体験をあげるためだけなので、顧客体験にはほぼ影響しないわけで、私は仕事でプロダクト(生産物)に価値を与えたいのであって、開発者が幸せになるためという理由でデコトラのように電飾ギラギラのマウンティングとるために派手に自分のコードをコテコテしたいわけではないんです。

一種の詭弁だが、騙されやすい。

グロタンディーク構成とツリー/フォレスト

次のような対応があると思う。

  • テレスコープ ←→ フォレスト
  • テレスコープのシグマ構成圏の対象 ←→ フォレストのパス
  • テレスコープのシグマ構成圏の対象集合 ←→ フォレストのパス集合

テレスコープに関して、レベルk(k - 0, 1, ...)のベース圏を考える。レベル0のベース圏はインデキシング圏。フォレストをツリー化して二人対戦ゲーム状態ツリーと考える。ターンl(l = 0, 1, ..)の手番を考える。

  • テレスコープのレベルkでのパイ構成 ←→ ゲームのターン(k + 1)での戦略の集合

シグマ構成でdisjointな和ができて、パイ構成でセクションの集合ができる。セクション=決定性の戦略。

依存カリー同型と依存フビニ定理

カリー同型とフビニ定理は切っても切れない。フビニ定理は、カリー同型で互いに移る高階関数と多変数関数の積分が一致することを主張している。

同様に、依存カリー同型と依存フビニ定理は切っても切れない。依存フビニ定理は、カリー同型で互いに移る高階依存ファミリー〈繰り返し依存ファミリー〉とテレスコープ〈複項依存ファミリー〉のシグマ構成〈グロタンディーク構成〉が本質的に一致することを主張している。

依存版のカリー同型/フビニ定理は、精密に議論する必要がある。

これかな?$`\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{cat}[1]{\mathcal{#1} }
`$

$`\mrm{Fam}(\int_{x\in A} B(x), \cat{C}) \cong \Pi(\lambda\, x\in A. \mrm{Fam}(B(x), \cat{C}) )
%`$

あるいは、

$`[ \sum_{x\in A} B(x), \cat{C}] \cong \prod(\lambda\, x\in A. [B(x), \cat{C}])
%`$

あるいは、

$`\cat{C}^{\sum_{x\in A} B(x)} \cong \prod_{x\in A} \cat{C}^{B(x)}
%`$

フビニは:

$`\int_{(a, b)\in \int_{x\in A} B(x)} F(a, b) \cong
\int_{x\in A}(\lambda\, x\in A. \int_{y\in B(x)} F(x, y))
`$

あるいは

$`\sum(\sum(A \mid B)\mid F) \cong
\sum(A \mid \lambda\, x.\sum(B(x) \mid F(x, -)))
`$

依存カリー同型

カリー同型は、複関数〈multifunction | 多重関数 | 多変数関数〉と高階関数〈higher-order function〉との1:1対応を与える。同様に、依存カリー同型は、依存複関数と依存高階関数のあいだの対応を与える。さらに、関数を関手に一般化するると、依存複関手と依存高階関手のあいだの対応を与える。$`\newcommand{\cat}[1]{\mathcal{#1} }
%`$

依存複関手はテレスコープ〈telescope〉と呼び、依存高階関手は繰り返しファミリー〈iterated family〉と呼ぶ。長さ2のテレスコープ〈2項依存関手〉の場合を述べる。

$`(\cat{C}, F, G)`$ を長さ2のテレスコープとすると、

$`G:\int_{\cat{C}} F \to {\bf CAT}`$

依存カリー化を次のように定義する。

$`G^{\cap F} := \lambda\, x: \cat{C}.\int_{F(x)}G_x(-)`$

ここで:

  • 積分記号はグロタンディーク構成。
  • $`x:\cat{C}`$ は $`x`$ が圏 $`\cat{C}`$ の対象または射を走る変数だと宣言している。
  • $`G_x(-) = G(x, -)`$

$`[\cat{C}, {\bf CAT}]`$ をインデックス付き圏の全体とする。インデックス付き圏は圏のファミリーと言っても同じ。さらに、

$`[*, {\bf CAT}] := \int_{x : {\bf Cat}} [x, {\bf CAT}]`$

と定義する。すると、標準的なファイブレーションがある。

$`\pi: [*, {\bf CAT}] \to {\bf Cat}`$

一方で、忘却関手もある。

$`U: [*, {\bf CAT}] \to {\bf CAT}`$

次に、$`H:\cat{C} \to [*, {\bf CAT}]`$ に対して依存反カリー化を定義する。

$`H`$ と標準射影の結合を $`\underline{H}`$ とする。依存反カリー化 $`H_\cup`$ は次のプロファイルを持つ二項依存関手になる。

$`H_\cup : \int_\cat{C} \underline{H} \to {\bf CAT}`$

$`H_\cup`$ は、$`(\cat{C}, \underline{H}, H_\cup)`$ というテレスコープで書ける。つまり、高階ファミリーの依存反カリー化はテレスコープ〈複項依存関手〉になる。

示すべきは次:

  • $`(G^{\cap F})_{\cup} \cong G`$
  • $`(H_\cup)^{\cap \underline{H}} \cong H`$

高階ファミリーとテレスコープ

テレスコープとグロタンディーク構成とグロタンディーク/フビニの定理の関係:

indexed thing = indexed family of things を単にファミリーと呼ぶ。インデックス付き圏もファミリーになる。テレスコープはファミリーに関して定義できる。テレスコープの第1成分から、第n成分はファミリーになる。n = 0 ならインデキシングシングだけ、n = 1 なら単一のファミリーになる。つまり、テレスコープは、グロタンディーク構成/シグマ構成を挟んだファミリーの拡張概念になる。

一方で、高階ファミリーは次のように定義する。

  1. 0階のファミリーはベースシング
  2. 1階のファミリーはファミリー
  3. 2階のファミリーはファミリーを値とするファミリー
  4. 2階のファミリーは2階のファミリーを値とするファミリー
  5. n階のファミリーは(n -1)階のファミリーを値とするファミリー

高階ファミリーとテレスコープが対応する依存カリー同型があると思われる。高階ファミリーはテレスコープに分解〈decompose | factorize〉できる。逆に、テレスコープは高階ファミリーに合成〈synthesize | 統合 | 集約〉できる。

テレスコープのシグマ構成と高階ファミリーのシグマ構成が同型であることを主張するのがフビニの定理。ツリー/フォレスト理論や述語論理での対応物を見つけたい。

n-ファミリーの定義は次:

$`F: \delta I \to n{\bf Cat} \text{ in }(n +1){\bf CAT}\\
\text{where }I \in_0 n{\bf Cat}, \delta :n{\bf Cat} \to (n + 1){\bf CAT}
%`$

n = 0:

$`F: \delta I \to {\bf Set} \text{ in }{\bf CAT}\\
\text{where }I \in_0 {\bf Set}, \delta :{\bf Set} \to {\bf CAT}
%`$

n = 1:

$`F: \delta I \to {\bf Cat} \text{ in }2{\bf CAT}\\
\text{where }I \in_0 {\bf Cat}, \delta :{\bf Cat} \to 2{\bf CAT}
%`$

一貫性法則と一貫性定理

くどいが:

  • 一貫性法則は命題である。
  • 一貫性定理は、一貫性法則という命題が真であると保証している定理(証明付き)

法則は単なる命題で、定理は真である保証。一貫性法則という命題を公理として要求するときは一貫性要求。「一貫性公理」と言うとバランスはいいのだが、一貫性条件と混乱する。一貫性法則要求公理とかになる。

テレスコープとグロタンディーク構成

Wikipediaに ニコラース・ホーヴァート・ド・ブラウン という項目があるので、「ド・ブラウン」にする。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1} }
%`$

Automathの論文 "Telescopic mappings in typed lambda calculus" by N.G. de Bruijn が次にある。

ここから「テレスコープ」を借用する。ただし、

  • ド・ブラウンのテレスコープは、テレスコープ{列 | リスト | タプル | レコード}と呼ぶ。
  • テレスコープは、テレスコープ列を対象とする圏を作る一種のスキーマ。

アイディアは次の論文。

テレスコープは $`(\cat{C}, P_1, \cdots, P_n)`$ という列で、

  1. $`\cat{C}_0 = \cat{C}`$ は小さい圏
  2. $`P_1:\cat{C}_0 \to {\bf CAT}`$ はインデックス付き圏
  3. $`\cat{C}_1 = \Sigma (\cat{C}_0, P_1)`$ はグロタンディーク構成の平坦化
  4. $`P_2:\cat{C}_1 \to {\bf CAT}`$ はインデックス付き圏
  5. 以下同様。

テレスコープのグロタンディーク構成を次のように定義する。

$`\Sigma(\cat{C}, P_1, \cdots, P_n) := \Sigma(\cat{C}_{n-1}, P_n)`$

小さい圏 $`\cat{C}`$ 上の長さ $`n`$ のテレスコープの全体を $`\mrm{Teles}_n(\cat{C})`$ とする。すべての長さのテレスコープの全体を $`\mrm{Teles}(\cat{C})`$ とする。

$`\mrm{Teles}(\cat{C}) = \sum_{n = 0}^\infty \mrm{Teles}_n(\cat{C})`$

$`\vec{P} = (P_1, \cdots, P_n)`$ と置いて、

$`(\cat{C}, \vec{P}) = (\cat{C}, P_1, \cdots, P_n)`$

とする。$`\vec{P} = ()`$ でもよい。$`\Sigma(\cat{C}, \vec{P})`$ がグロタンディーク構成となる。

テレスコープとそのグロタンディーク構成、それと次のグロタンディーク構成との関係を明らかにしたい。

$`\mrm{IndCat}(\cat{C}, \int_{\cat{J}\in |{\bf Cat}|} \mrm{IndCat}(\cat{J}, {\bf CAT})`$

これは、$`\cat{C}`$ 上の長さ2のテレスコープの全体になりそうだが。次元を下げて、ツリー&フォレストで確認したい。

長さnのテレスコープ $`(\cat{C}, \vec{P})`$ に対して、圏 $`\Sigma(\cat{C}, \vec{P})`$ の対象をテレスコープ列と呼ぶ。テレスコープ列は、ツリーのルートからリーフに向かうパスに相当する。したがって、階層構造/入れ子構造を表す。