このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

集合圏における依存カリー同型

雑記／備忘

ラムダ計算の意味論においては、カリー同型が中心的な概念です。となると、依存ラムダ計算の意味論には依存カリー同型が必要になります。とりあえずは一番具体的なデカルト閉圏である集合圏において依存カリー同型を考えてみます。$`\newcommand{\id}{\mathrm{id} }
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\hyp}{\text{-}}
\newcommand{\In}{\text{ in }}
\newcommand{\T}[1]{\mathscr{#1}}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\Ev}{\triangleleft}
`$

内容：

集合圏におけるカリー同型

集合圏では次のモノは全部同じです。

  1. $`{\bf Set}(A, B)`$ ： 外部ホムセット（通常のホムセット）
  2. $`[A, B]`$ ： 内部ホムセット＝内部ホム対象＝指数対象
  3. $`\mrm{Map}(A, B)`$ ： すべての写像〈関数〉からなる集合
  4. $`B^A`$ ： 集合の指数演算（の結果）

どの記法を使うかは気分次第ですが、短く書けるという理由で今日は累乗〈ベキ〉形式 $`B^A`$ を主に使います。

集合圏におけるカリー同型は次のように書けます。

$`\quad {\bf Set}(A\times B, C)\cong {\bf Set}(A, C^B)`$

この同型を与える左から右への写像がカリー化、右から左への写像が反カリー化です。

  • カリー化： $`\mrm{Curry}_{A, B, C}:{\bf Set}(A\times B, C)\to {\bf Set}(A, C^B) \In {\bf Set}`$
  • 反カリー化：$`\mrm{Uncurry}_{A, B, C}:{\bf Set}(A, C^B) \to {\bf Set}(A\times B, C) \In {\bf Set}`$
  • 可逆性： $`{\mrm{Curry}_{A, B, C}}^{-1} = \mrm{Uncurry}_{A, B, C}`$

反カリー化は、評価射 $`\mrm{ev}`$ によって書きくだせます。

  • $`\mrm{ev}_{B, C} : C^B\times B \to C \In {\bf Set}`$
  • $`\mrm{Uncurry}_{A, B, C}(g) = \mrm{ev}_{B, C}\circ (g \times \id_B)\:\text{ for }g \in {\bf Set}(A, C^B)`$

ここで、$`\circ`$ は反図式順の関数結合記号です。

$`f`$ のカリー化を $`f^\cap`$ や $`f^\wedge`$ で略記します。肩に乗った $`\wedge`$ はラムダ $`\lambda`$ に似てるので憶えやすいでしょう。$`g`$ の反カリー化は $`g_\vee`$ とします。

  • $`f^\wedge = \mrm{Curry}_{A, B, C}(f) \in {\bf Set}(A, C^B)\:\text{ for }f \in {\bf Set}(A\times B, C)`$
  • $`g_\vee = \mrm{Uncurry}_{A, B, C}(g) \in {\bf Set}(A\times B, C)\:\text{ for }g \in {\bf Set}(A, C^B)`$

この記法を使って先の評価射の等式を書くと：

$`\quad g_\vee = \mrm{ev}_{B, C}\circ ( g(\hyp), \hyp)`$

ハイフン記号は無名ラムダ変数です。$`g = f^\wedge`$ と置くと：

$`\quad f = (f^\wedge)_\vee = \mrm{ev}_{B, C}\circ ( f^\wedge(\hyp), \hyp)`$

引数変数を使って書けば：

$`\quad f(x, y) = \mrm{ev}_{B, C}\circ ( f^\wedge(x), y )`$

$`\mrm{ev}_{B, C}\circ (\hyp, \hyp)`$ を中置演算子記号 $`\hyp \Ev \hyp`$ により書けば：

$`\quad f(x, y) = f^\wedge(x) \Ev y`$

通常、中置演算子記号を単なる併置で書いて、$`f^\wedge`$ をギリシャ文字 $`\lambda`$ を使って書きます*1。つまり：

$`\quad f(x, y) = (\lambda\,t.f(s, t))[x/s]\; y`$

$`[x/s]`$ は自由変数 $`s`$ の置き換えで、代入に相当します。ここらへんも曖昧にした乱暴な書き方をすれば：

$`\quad f(x, y) = \lambda\,y.f(x, y)\; y`$

ここまで情報を落としてしまうと、（一見分かりやすく感じるかも知れませんが）肝心なところは見えなくなってますね。極端な略記はやめて、元に戻って考えてください。型をキチンと書くのが曖昧さへの対処になります。それと、型をワイヤーで表現したストリング図を描くのもオススメです。

型を丁寧に明示した書き方は：

$`\quad \big\langle x\in A, y\in B \mapsto f(x, y) \in C\big\rangle\\
= \big\langle x\in A, y\in B \mapsto \lambda\,t\in B.f(x, t)\;y \in C\big\rangle\\
\quad : A\times B \to C \In {\bf Set}
`$

上の等式の右辺（下側）で、暗黙化されてしまっている $`\mrm{ev}`$ と、$`\mrm{ev}`$ に渡す型〈集合〉の情報も書くと次のようになります。

$`\big\langle (A, B, C \in |{\bf Set}|), x\in A, y\in B \mapsto \mrm{ev}_{A, B, C}(\lambda\,t\in B.f(x, t), y) \in C\big\rangle`$

ファミリー

"indexed family of sets" の呼び名は山のようにあります（「用語のバリエーション記述のための正規表現 // 英語と日本語での例」参照）。ここでは単に「ファミリー」または「族」と呼ぶことにします。

ファミリー $`F`$ は次のような写像です。

$`\quad F:I \to |{\bf Set}| \In {\bf SET}`$

写像の余域である $`|{\bf Set}|`$ は大きな集合なので、大きな集合も含む集合圏 $`{\bf SET}`$ で考えます。

インデックス集合（ファミリーの域）が $`I`$ であるファミリーの全体は、$`\mrm{MAP}(I, |{\bf Set}|)`$ と書けます。$`\mrm{MAP}(\hyp, \hyp) = {\bf SET}(\hyp, \hyp)`$ です。

$`F, G\in \mrm{MAP}(I, |{\bf Set}|)`$ に対して、$`F`$ から $`G`$ へのファミリーのあいだの準同型写像 $`\alpha`$ は、次のようなファミリーです。

$`\quad i\in I \mapsto (\alpha_i : F(i) \to G(i) \In {\bf Set})`$

自然変換の定義と似てますが、実は自然変換そのものと思ってかまいません。集合 $`I`$ を離散圏だと思ったモノを $`I|_{\le 1}`$ と書くと*2、次が成立します。

$`\quad {\bf SET}(I, |{\bf Set}|) \cong |{\bf CAT}(I|_{\le 1}, {\bf Set})| \In {\bf SET}`$

ファミリーのあいだの準同型写像は、関手圏 $`{\bf CAT}(I|_{\le 1}, {\bf Set})`$ の射、つまり自然変換です。ファミリー（関手）とそのあいだの準同型写像（自然変換）を一緒に考えると圏になるので、それを $`{\bf Fam}[I]`$ とします。

$`\quad {\bf Fam}[I] := {\bf CAT}(I|_{\le 1}, {\bf Set})\\
\quad |{\bf Fam}[I]| = |{\bf CAT}(I|_{\le 1}, {\bf Set})| \cong {\bf SET}(I, |{\bf Set}|)
`$

集合 $`I`$ と離散圏 $`I|_{\le 1}`$ を同一視して、圏の圏の指数対象である関手圏を累乗〈ベキ〉記法で書くと、次のように簡潔に書けます。

$`\quad {\bf Fam}[I] := {\bf Set}^I \In {\bf CAT}`$

$`I`$ と $`I|_{\le 1}`$ 、$`|{\bf CAT}(I|_{\le 1}, {\bf Set})|`$ と $`{\bf SET}(I, |{\bf Set}|)`$ は適宜同一視します。

依存集合

$`I`$ を集合として、$`I`$ に依存する集合とは、オーバー圏〈スライス圏〉（「オーバー圏、アンダー圏」参照） $`{\bf Set}_{/I}`$ の対象です。「$`I`$ 上の依存集合の圏」とは、オーバー圏 $`{\bf Set}_{/I}`$ の別名です。依存集合〈depended set〉という呼び名を使うのは、依存型理論の意味論に使う下心があるからです。他の呼び名もあります、参考までに僕が知っている呼び名（ファミリーの圏の呼び名も含めて）を列挙すると：

  1. 多項式の圏〈多項式関手の圏〉
  2. コンテナの圏
  3. 集合論的バンドルの圏
  4. カローラ・フォレスト〈低木林〉の圏
  5. メニュー圏
  6. インデックス付き集合〈indexed set〉の圏

$`I`$ 上の依存集合は、$`f:A \to I`$ という写像に過ぎません（写像に何の条件も付きません）。2つの依存集合のあいだの射は次の可換図式を満たす写像 $`\varphi`$ のことです。

$`\require{AMScd}
\begin{CD}
A @>{\varphi}>> B \\
@V{f}VV @VV{g}V\\
I @= I
\end{CD}\\
\text{commutative in }{\bf Set}
`$

集合 $`I`$ 上の依存集合とそのあいだの射からなる圏（オーバー圏ですが）を $`{\bf DepSet}[I]`$ と書きます。

$`\quad {\bf DepSet}[I] := {\bf Set}_{/I}`$

依存集合の圏 $`{\bf DepSet}[I]`$ とファミリーの圏 $`{\bf Fam}[I]`$ は圏同値になります。

  • $`{\bf DepSet}[I] \cong {\bf Fam}[I] \In {\bf CAT}`$ ： 圏同値
  • $`{\bf Fam}[I] \to {\bf DepSet}[I] \In {\bf CAT}`$ ： シグマ型構成で与えられる。
  • $`{\bf DepSet}[I] \to {\bf Fam}[I] \In {\bf CAT}`$ ： 逆像ファミリーで与えられる。

次の2つの射が、圏同値で対応しているとします。

  • $`(\varphi: (f:A \to I) \to (g:B \to I)) \In {\bf DepSet}[I]`$
  • $`(\alpha: (F:I \to |{\bf Set}|) \to (G:I \to |{\bf Set}|) ) \In {\bf Fam}[I]`$

次のような関係があります。$`\pi_\hyp`$ はシグマ型構成の標準射影です。

  • $`F \mapsto (A, f)`$
    • $`A := \sum_I F`$
    • $`f := \pi_F : \sum_I F \to I`$
  • $`G \mapsto (B, g)`$
    • $`B := \sum_I G`$
    • $`g := \pi_G : \sum_I G \to I`$
  • $`\alpha \mapsto \varphi`$
    • $`\varphi(i, x) := \alpha_i(x)`$
  • $`(A, f) \mapsto F`$
    • $`F(x) := f^{-1}(x)`$ （逆写像ではなくて逆像集合）
  • $`(B, g) \mapsto G`$
    • $`G(x) := g^{-1}(x)`$ （逆写像ではなくて逆像集合）
  • $`\varphi \mapsto \alpha`$
    • $`\alpha_i(x):= \varphi(i, x)`$

ゆっくりジックリ考えてみれば自明に見えるでしょう。

この圏同値の“圏の次元”を上げると、ファイバー付き圏〈fibred category〉とインデックス付き圏〈indexed category〉のあいだのグロタンディーク同型になります。「依存集合←→ファミリー」の対応は、グロタンディーク同型の0次元バージョンと言えます。

依存カリー同型

依存カリー同型の主張を先に書いてしまうと：

$`\quad {\bf DepSet}[I](X \rtimes I, \sum_I F) \cong {\bf Set}(X, \prod_I F)`$

$`\sum_I, \prod_I`$ は、シグマ型構成とパイ型構成です。$`\rtimes`$ は後で説明しますが、とりあえずは直積 $`\times`$ と思ってかまいません。通常のカリー同型と同様に次のようになります。

  • 依存カリー化： $`\mrm{DepCurry}_{X, I, F} : {\bf DepSet}[I](X \rtimes I, \sum_I F) \to {\bf Set}(X, \prod_I F) \In {\bf Set}`$
  • 依存反カリー化： $`\mrm{DepUncurry}_{X, I, F} : {\bf Set}(X, \prod_I F) \to {\bf DepSet}[I](X \rtimes I, \sum_I F) \In {\bf Set}`$
  • 可逆性： $`{\mrm{DepCurry}_{X, I, F}}^{-1} = \mrm{DepUncurry}_{X, I, F}`$

依存反カリー化は、依存評価射 $`\mrm{dep\_ev}`$ によって書きくだせます。

  • $`\mrm{dep\_ev}_{I, F} : (\prod_I F) \times I \to \sum_I F `$
  • $`\mrm{DepUncurry}_{X, I, F}(g) = \mrm{dep\_ev}_{I, F}\circ (g \times \id_I)`$

射 $`f\in {\bf DepSet}[I](X \rtimes I, \sum_I F)`$ と $`g\in {\bf Set}(X, \prod_I F)`$ の具体的な表示は次の形を使いましょう。

$`\quad f = \big\langle
x\in X, i\in I \mapsto f(x, i) \in F(i) \big\rangle\\
\quad g = \big\langle
x\in X \mapsto \lambda\, i\in I. g_i(x) \in \prod_I F \big\rangle
`$

ラムダ抽象とタプルは同じことなので（「タプル・コタプルとVΣ計算」参照）、次のように書いてもかまいません。

$`\quad \langle g_i(x)\rangle_{i\in I} = \lambda\, i\in I. g_i(x)`$

また、大きな山形括弧の内部にある $`i\in I`$ をインデキシングだと解釈することもできるので、次のようにも書けます。

$`\quad f = \big\langle
x\in X \mapsto f(x, i) \in F(i) \big\rangle_{i\in I }\\
\quad g = \big\langle
x\in X \mapsto \langle g_i(x)\rangle_{i\in I} \in \prod_I F \big\rangle
`$

この形を見ると、依存カリー同型が、大きなタプル $`\big\langle\hyp\big\rangle_{i\in I}`$ と小さなタプル $`\langle \hyp \rangle_{i\in I} `$ の相互変換なのだと見当が付くでしょう*3。

なお、大きなタプルは、型理論における型付け判断〈typing judgement〉に相当します。型理論の書き方なら次のようです*4。

$`\quad
x : X,\; i : I \vdash f(x, i) : F(i)\\
\quad
x : X \vdash \lambda\, i : I. g_i(x) : \Pi\, i\in I. F
`$

論理なら以下の書き方でしょう。証明可能性に関するメタ命題です。論理では、証明が存在するかどうかに興味があるので、その他の情報が省略されています（省略しないほうがいいと僕は思うけど*5）。

$`\quad
X \vdash F(i) \text{ for }i\in I\\
\quad
X \vdash \forall i\in I. F
`$

依存集合の圏、もう少し

集合 $`I`$ 上の依存集合の圏 $`{\bf DepSet}[I]`$ をもう少し調べましょう。

依存集合の圏とファミリーの圏は圏同値（事実上同じ圏だと思ってよい）ので、ファミリー $`F\in |{\bf Fam}[I
]|`$ を使って依存集合を表すのが普通です。ファミリー $`F`$ のシグマ構成を $`\sum_I F`$ とすると、標準的な射影
$`\quad \pi_F : \sum_I F \to I`$
が一意的に決まるので、$`\pi_F : \sum_I F \to I`$ でもって $`I`$ 上の依存集合を表します。

依存集合は写像なので、$`\pi_F : \sum_I F \to I`$ と書くべきですが、写像の域 $`\sum_I F`$ により依存集合を代表させます。いわゆる“記号の乱用” $`\sum_I F = (\pi_F : \sum_I F \to I)`$ だと思えばいいでしょう。

さて、集合 $`A`$ に対して、$`\pi_1 : I\times A \to I`$ と $`\pi_2 : A\times I \to I`$ は $`I`$ 上の依存集合です（$`\pi_1, \pi_2`$ は直積の射影です）。次のように記述します。

$`\quad I \ltimes A := (\pi_1 :I \times A \to I)\\
\quad A \rtimes I := (\pi_2 : A \times I \to I)`$

$`i\in I \mapsto A \in |{\bf Set}|`$ で定義される定数値ファミリーを $`K^A`$ とすると、次が成立します。

$`\quad \sum_I \mrm{K}^A \cong I \ltimes A \cong A \rtimes I`$

$`\sum_I \mrm{K}^A`$ を単に $`\sum_I A`$ と書いてしまうことも多いので、横着した記法で書けば：

$`\quad \sum_I A \cong I \ltimes A \cong A \rtimes I`$

以下の同型もよく使われる重要なものです。

$`\quad {\bf DepSet}(A\rtimes I, B \rtimes I) \cong {\bf Set}(A \times I, B)
`$

この同型を使うと、通常の（単純な形の）カリー同型が、依存カリー同型の特別な場合であることを示せます（次節）。

依存カリー同型と単純なカリー同型

依存カリー同型と、関連する同型を列挙します。

  1. $`{\bf DepSet}[I](X \rtimes I, \sum_I F) \cong {\bf Set}(X, \prod_I F)`$ （依存カリー同型）
  2. $`{\bf DepSet}[I](X \rtimes I, C \rtimes I) \cong {\bf Set}(X \times I, C)`$ （前節参照）
  3. $`\sum_I C = \sum_I \mrm{K}^C \cong I \times C \cong C \times I`$ （前節参照）さらに
    $`(\pi_{\mrm{K}^C}: \sum_I \mrm{K}^C \to I) \cong (\pi_1:I \times C \to I) \cong (\pi_2: C \times I \to I)`$
  4. $`\prod_I C = \prod_I \mrm{K}^C \cong C^I = \mrm{Map}(I, C)`$

最後〈4番目〉の同型は、以下のようにわかります。$`\mrm{Sect}(\hyp)`$ は写像のセクションの集合です。

$`\quad \prod_I C = \prod_I \mrm{K}^C \\
:= \mrm{Sect}(\pi_{\mrm{K}^C } : \sum_i \mrm{K}^C \to I) \\
\cong \mrm{Sect}(\pi_1 : I \times C \to I) \\
\cong \mrm{Map}(I, C) \\
= C^I
`$

上記の箇条書きで列挙した同型は、「1番、2番、3番、4番の同型」として引用します。

1番の同型〈依存カリー同型〉から通常の（単純な）カリー同型を導いてみます。

$`\quad {\bf DepSet}[I](X \rtimes I, \sum_I F) \cong {\bf Set}(X, \prod_I F)\\
F = \mrm{K}^C \text{ を代入}\\
\quad {\bf DepSet}[I](X \rtimes I, \sum_I \mrm{K}^C) \cong {\bf Set}(X, \prod_I \mrm{K}^C)\\
\text{3番の同型と4番の同型から}\\
\quad {\bf DepSet}[I](X \rtimes I, C \rtimes I) \cong {\bf Set}(X, C^I) \\
\text{2番の同型から}\\
\quad {\bf Set}(X \times I, C) \cong {\bf Set}(X, C^I)
`$

カリー／グロタンディーク・ガーデン

依存カリー同型を考える際には、次の3つの圏が登場しました。

  • $`{\bf Fam}[I]`$
  • $`{\bf DepSet}[I]`$
  • $`{\bf Set}`$

3つと言いましたが、それは $`I`$ を固定した場合で、$`I`$ を動かせば無数の圏が生まれます。また、依存性を持たない集合の圏 $`{\bf Set}`$ も、単元集合上の依存集合の圏 $`{\bf DepSet}[{\bf 1}]`$ とみなせます。

つまり、様々な $`I`$ に対する $`{\bf Fam}[I], {\bf DepSet}[I]`$ 達が居て、それらはグロタンディーク同型（の0次元バージョン）で結ばれています。また、（今日は詳しく述べませんが）$`u: I \to J`$ のような写像があると、$`u`$ は圏のあいだの関手を誘導します。

たくさんの圏達は、システマティックにデザインされ良く整備された庭園のような風景を形成します。庭園のデザインの中核コンセプトは依存カリー同型とグロタンディーク同型で与えられるので、圏達が形成する構造と風景を仮にカリー／グロタンディーク・ガーデン〈Curry-Grothendieck garden〉と呼びましょう。カリー／グロタンディーク・ガーデンは広大で、地上（0次元部分）だけではなくて上の階層（高次元部分）にも拡がっています。

カリー／グロタンディーク・ガーデンの奥まで（そして上の層まで）散策するのはなかなかに骨の折れる作業です。しかし入口付近に関しては遊歩道があるので、そこで足ならしをすることは出来そうです。

*1:ここらへんの記述は構文論と意味論がゴッチャになっています。ギリシャ文字を使うとかは構文側の話です。

*2:この書き方は「圏の離散化、切り捨て、次元調整」参照。この書き方、圏の対象を表す絶対値記号と見間違えるリスクがあるかも。

*3:関数を表すラムダ式とタプルは同じモノなので、「大きなタプル／小さなタプル」とは「大きなラムダ式／小さなラムダ式」です。「大きなラムダ式／小さなラムダ式」という言葉は、14年前に書いた記事「セミナー補足：関数コードの実行エンジン」以来使い続けているのですが、（当然ながら）普及はしませんね。でも、「大きなラムダ式＝大きなタプル」と「小さなラムダ式＝小さなタプル」を区別しないとラムダ計算／型理論は理解できないと思いますよ。

*4:型理論のなかでもたくさんの方言があります。

*5:省略の程度や省略の方法が分野ごとに違うことが、カリー／ハワード／ランベック対応を理解する障害になっています。