関数のファミリー〈族〉からタプル関数を作る操作とコタプル関数を作る操作は双対〈dual〉で、圏論の極限と余極限の双対性に対応します。しかし、型理論やプログラミング言語のなかでは、この双対性が見えにくくなっています。タプル構成は、λΠ計算〈ラムダ・パイ計算〉という計算体系で取り扱えますが、コタプル構成を取り扱うのに適切な計算体系はないようです。そこで、λΠ計算の双対であるVΣ計算〈ブイ・シグマ計算〉を導入して、タプルとコタプルを対等に対称的に扱うことにします。$`\require{color}
\newcommand{\Changed}[1]{ \textcolor{orange}{\text{#1}} }
\newcommand{\ot}{ \leftarrow }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\In}{ \text{ in }}
`$
内容：
はじめに
圏論では、双対な概念がよく登場します。例えば、終対象と始対象は互いに双対です。直積と直和も互いに双対です。終対象←→始対象、直積←→直和 の双対性の一般化として、極限←→余極限の双対性があります。この記事に関係する極限・余極限については、最後の節でまとめます。圏論をご存知なら、先に最後の節を読んだほうがスッキリ理解できるでしょう。
カリー／ハワード／ランベック対応（「カリー／ハワード／ランベック対応の辞書」参照）によれば、圏論的な双対性の対応物は、型理論（ラムダ計算含む）にも論理にも存在するはずです。また、関数型プログラミング言語は型付きラムダ計算に基づいているので、プログラミングのなかでも双対性が存在するはずです。
実際、圏論の双対性の対応物は存在しています。圏論以外の分野では、圏論のように双対性が単純明快に表現されているわけではなくて、見えにくく分かりにくい状況になっています。その理由はおそらく、型理論／論理では、双対性にあまり興味がなかったからでしょう。双対性を扱う道具や技法が整備されてないのです。
ここでは、依存型理論のパイ型の双対であるシグマ型を計算するためにVΣ計算を導入して、プログラミング言語のなかのパイ・シグマ双対性を観測することにします。今回は、論理の話はしません。
記号の約束
今回の話の具体例が欲しくなったら、「具体例（なんの？）」を読んでください。「具体例（なんの？）」はホントに具体例を書いた記事ですが、「抽象的セッティング： タプル構成」「抽象的セッティング： コタプル構成」では抽象的・一般的な記号・記法も導入しています。
前の記事「具体例（なんの？）」の記号・記法をそのまま利用するつもりだったのですが、少し変更します（ほぼ気分だけの問題ですけど）。変更した記号はオレンジ色にしています。
タプル構成の説明のため：
| 「具体例（なんの？）」 | 今回のこの記事 |
|---|---|
| $`X`$ | $`X`$ |
| $`\Changed{Y}`$ | $`T`$ |
| $`I`$ | $`I`$ |
| $`\prod_{i\in I}A_i`$ | $`\prod_{i\in I}A_i`$ |
| $`F_i`$ | $`F_i`$ |
コタプル構成の説明のため：
| 「具体例（なんの？）」 | 今回のこの記事 |
|---|---|
| $`\Changed{X}`$ | $`T`$ |
| $`J`$ | $`J`$ |
| $`\sum_{j\in J}B_j`$ | $`\sum_{j\in J}B_j`$ |
| $`\Changed{Z}`$ | $`Y`$ |
| $`G_j`$ | $`G_j`$ |
$`I, J`$ はインデックス集合〈indexing set〉で、番号〈整数〉や名前〈文字列〉の有限集合とします。例えば、$`I = J = \{1, 2, 3\}`$ とすれば、
$`\quad \prod_{i\in I}A_i = A_1 \times A_2 \times A_3\\
\quad \sum_{j\in J}B_j = B_1 + B_2 + B_3`$
です。直積（掛け算）は分かるでしょうが、直和（足し算）の定義を念のために書いておくと：
$`\quad \sum_{j\in J}B_j = B_1 + B_2 + B_3\\
= \{1\}\times B_1 \cup \{2\}\times B_2 \cup \{3\}\times B_3`$
インデックスを番号にしましたが、インデックスは、キー付きタプル型のキーやタグ付きユニオン型のタグなので、名前〈文字列〉のほうが便利でしょう。
インデックス（キーやタグ）の集合が有限であるという仮定は実は不要です。むしろ、邪魔になります。が、有限性の条件を外すと、無限個の直積／無限個の直和 の説明をしなくてはならないので、今回はインデックス集合は有限だとしておきます。
型判断と関数定義
型理論や論理では、定数記号／変数記号／関数記号／述語記号などを組み合わせた記号的表現を項〈term〉と呼びます。項 $`\psi`$ に対する型判断〈{type | typing} judgement〉とは、次の形のものです。
$`\quad t: T, x: X \vdash \psi : C`$
これは次のような意味を持ちます。
- 変数 $`t`$ の型は $`T`$ である。$`t`$ は今は注目してない変数である。
- 変数 $`x`$ の型は $`X`$ である。
- 項 $`\psi`$ は変数 $`t, x`$ を含むかも知れない。
- 項 $`\psi`$ の型は $`C`$ となる。
型理論では、型判断に名前を付けることはしないのですが、次の形式で名前〈ラベル〉 $`f`$ を付けることにします。
$`\quad f := (t: T, x: X \vdash \psi : C)`$
これは、型付きプログラミング言語の関数定義と同じことです。例えば、TypeScript で書くなら：
var t : T; function f(x : X) : C { return ψ; }
最近僕が興味を持っているLean 4で書くなら：
variable (t : T) def f (x : X) : C := ψ
書き方〈構文〉の違いにイチイチ反応しないで、内容的に同じであることに注意を向けましょう。
- 項 $`\psi`$ は、関数定義の本体〈body〉だと思ってよい。
- 項 $`\psi`$ 内で変数 $`t`$ を使っているかも知れないが、$`t`$ は環境・背景からの情報だと考えて、“$`f`$ への引数”とは当面は考えない（状況により引数と考えることもあるが）。環境・背景からの情報である $`t`$ はここでは背景変数〈background variable〉と呼ぶ。
- $`(x : X)`$ は、関数 $`f`$ の引数変数の型宣言である。
- 型 $`C`$ は、関数 $`f`$ の戻り型〈return type〉である。
背景変数宣言と引数変数宣言を区別するために、縦棒やセミコロンで区切ることもあります。
$`\quad f := (t: T \mid x: X \vdash \psi : C)`$
ここでは特に区切りを入れません。現実には、どこまでが背景か曖昧なことがあるし、背景変数と引数変数の境界をずらすことがあるからです。
項 $`\psi`$ を変数 $`x`$ でラムダ束縛〈ラムダ抽象〉することによって、関数 $`f`$ をカリー化できます。
$`\quad f^\wedge := (t: T \vdash \lambda\, x: X.(\psi : C) : C^X )`$
同じことをTypeScriptで書けば次のようです*1。カリー化をする前のコードも載せています。
var t : T; function f(x : X) : C { return ψ; } function f_curry() : (x : X) => C { return (function (x: X) {return ψ;}); }
型理論とプログラミング言語で、同じことを扱っているのですが、用語や記号が違うのです。
| 型理論 | プログラミング言語（TypeScript） |
|---|---|
| 型判断 | 型を明示した関数定義 |
| 項 $`\psi`$ | 関数ボディの式 ψ |
| 背景変数 $`t`$ | 関数外で宣言された変数 t |
| 背景以外の変数 $`x`$ | 引数変数 x |
| ターゲット型 $`C`$ | 戻り型 C |
| 指数型 $`X^C`$（集合論的記法） | アロー型 (x : X) => C |
| ラムダ抽象された項 $`\lambda\, \cdots`$ | 無名関数式 (function ...) |
| カリー化された型判断 $`f^\wedge`$ | カリー化された関数 f_curry |
型理論、そして多くの関数型言語では、指数型 $`X^C`$ を通常の矢印を使って $`C \to X`$ と書きます。この書き方は圏論をまじえた議論をするときに非常に紛らわしい！*2 ブラケットで囲って $`[C \to X]`$ または $`[X \ot C]`$とします。この書き方は、圏論と型理論の折衷案です。
| 型理論 | 圏論 |
|---|---|
| 指数型 $`C \to X`$ | 指数対象 $`[C, X]`$ |
| 型判断の区切り $`\vdash`$ | 射のプロファイル区切り $`\to`$ |
指数の矢印とプロファイルの矢印が違うことは「Haskellの二重コロン「::」とバインド記号「>>=」の説明」参照。
分野ごとに記法と用語法が違うのは悩みの種ですが、どうにもなりません。用語の対応については「カリー／ハワード／ランベック対応の辞書」を見てください。
ファミリー〈族〉
プログラミング言語では、関数 f に引数 x を渡すときは f(x) 、配列 a にインデックス i でアクセスするときは a[i] 、総称型 K に型引数 X を渡すなら K<X> のように別々な書き方をして、好き勝手な書き方はできません。しかし、ある程度抽象化した議論では、こういう区別は無意味なばかりか弊害があります。例えば、すべて丸括弧で書いて f(x), a(i), K(X) でかまいません。ただし、分かりやすさのためや気分の問題で書き方を変えることはあります。
以下のような書き方は本質的には同義なので、分かりやすさのためや気分により、ことわりなしに置き換えるかも知れないので注意してください。
- $`F_i`$
- $`F(i)`$
- $`F[i]`$
- $`F\:i`$
インデックス $`i\in I`$ ごとに型 $`A_i`$ が割り当てられているとき、対応 $`i \mapsto A_i`$ を型ファミリー〈type family〉と呼びます。正確には indexed family of types ですが、長いので略称します。
実はこの呼び名も方言*3で、型を集合と解釈すると、型ファミリーとは $`I \to |{\bf Set}|`$ という写像に過ぎません。ここで、$`|{\bf Set}|`$ は集合圏の対象の集合 -- つまり、すべての集合の集合*4です。“型ファミリー＝集合値写像”です。
同様に、インデックス $`i\in I`$ ごとに関数 $`F_i`$ が割り当てられているとき、対応 $`i \mapsto F_i`$ を関数ファミリー〈function family〉と呼びます。関数ファミリーを次のどちらかの形で書きます。
- $`(F_i)_{i\in I}`$
- $`(i\in I \mapsto F_i)`$
関数ファミリーに対して、その域〈domain〉と余域〈codomain〉はそれぞれ型ファミリーになります。
- $`(F_i)_{i\in I}`$ ： 関数ファミリー
- $`(\mrm{dom}(F_i))_{i\in I}`$ ： 域の型ファミリー
- $`(\mrm{cod}(F_i))_{i\in I}`$ ： 余域の型ファミリー
我々が考える関数ファミリーは、域と余域に制限を付けます。次のどちらかの関数ファミリーを考えます。
- 域が特定の型 $`X`$ に固定されている。余域は $`i`$ に依存して変わってよい。
$`(F_i : X \to A_i)_{i\in I}`$ - 余域が特定の型 $`Y`$ に固定されている。域は $`i`$ に依存して変わってよい。
$`(G_j : B_j \to Y)_{j\in J}`$
一番目の形の関数ファミリーをスパン・ファミリー〈span family〉、二番目の形の関数ファミリーをコスパン・ファミリー〈cospan family〉と呼ぶことにします。スパン・ファミリーの実例は「具体例（なんの？）」のmakeProductInfo関数の素材関数達、コスパン・ファミリーの実例はcalcPrice関数の素材関数達を見てください。
インデックスに関するラムダ抽象
次のような型判断を考えます。
$`\quad t : T, x : X, i : I \vdash \psi : \alpha`$
ここで：
- $`t`$ は背景変数
- $`x`$ は引数変数
- $`i`$ はインデックス
- $`\psi`$ は、$`t, x, i`$ を含むかも知れない項
- $`\alpha`$ は、$`t, x`$ を含まず、$`i`$ を含むかも知れない型項（型を表す項）
この型判断（無名の関数定義とみなせる）に対して、インデックス（集合 $`I`$ 上を走る変数）でラムダ抽象します。普通のラムダ記号 $`\lambda`$ でもいいのですが、次の理由から $`\wedge`$ を使います。
- インデックス $`i`$ は型項 $`\alpha`$ にも含まれるかも知れないので、（よく知っている）単なるラムダ抽象とは少し違う。
- 後で出てくる双対的な記号 $`\vee`$ と上下逆さまな形をしていて都合がよい。
- $`\wedge`$ は楔〈くさび〉記号だが、大文字ラムダとよく似てる。
インデックスに関するラムダ抽象の構文的なルールは次のとおりです。
$`\quad t : T, x : X, i : I \vdash \psi \;: \alpha\\
\text{↓ インデックスに関するラムダ抽象 ↓}\\
\quad t : T, x : X \vdash \wedge\, i : I. \psi\;: \prod_{i\in I}\alpha`$
$`\prod_{i\in I}`$ が構文的フレーバーが異質で気持ち悪いかも知れません。気になるようなら、$`\Pi\, i : I`$ とでもして、$`\prod_{i\in I}\alpha`$ を $`\Pi\, i : I.\alpha`$ とでも書けばいいでしょう。
ただし、書き方だけの違いで内容が同じなのに、構文的フレーバーに神経質になることは良い習慣とはいえません。「書き方なんて別にどうでもいい」と考えることをオススメします。
[/補足]
項 $`\psi`$ と型項 $`\alpha`$ は構文的な存在（プログラムで言えばソースコードの一部）ですが、項／型項の意味は次のとおりです。
- 型項 $`\alpha`$ は、$`i\in I \mapsto A_i`$ という型ファミリーを定義する。
- 項 $`\psi`$ は、$`t\in T, x \in X, i\in I \mapsto F(t, x, i) \in A_i`$ という関数を定義する。
インデックス $`i\in I`$ は下付きで $`F_i(t, x)`$ と書くことにして、構文より意味に注目するなら次のようになります。
$`\quad t : T, x : X, i : I \vdash F_i(t, x) \;: A_i\\
\text{↓ インデックスに関するラムダ抽象 ↓}\\
\quad t : T, x : X \vdash \wedge\, i : I. F_i(t, x)\;: \prod_{i\in I}A_i`$
$`I`$ は有限集合と仮定していたので、例えば $`I = \{1, 2, 3\}`$ とすると：
$`\quad t : T, x : X, i = 1 \vdash F_1(t, x) \;: A_1\\
\quad t : T, x : X, i = 2 \vdash F_2(t, x) \;: A_2\\
\quad t : T, x : X, i = 3 \vdash F_3(t, x) \;: A_3\\
\text{↓ インデックスに関するラムダ抽象 ↓}\\
\quad t : T, x : X \vdash \wedge\, i : \{1, 2, 3\}. F_i(t, x)\;: \prod_{i\in \{1, 2, 3\}}A_i`$
$`\wedge\, i : \{1, 2, 3\}. F_i(t, x)`$ を、
$`\quad \langle F_i(t, x) \rangle_{i \in \{1, 2, 3\} }\\
= \langle F_1(t, x), F_2(t, x), F_3(t, x) \rangle`$
と展開して書けば：
$`\quad t : T, x : X, i = 1 \vdash F_1(t, x) \;: A_1\\
\quad t : T, x : X, i = 2 \vdash F_2(t, x) \;: A_2\\
\quad t : T, x : X, i = 3 \vdash F_3(t, x) \;: A_3\\
\text{↓ インデックスに関するラムダ抽象 ↓}\\
\quad t : T, x : X \vdash \langle F_1(t, x), F_2(t, x), F_3(t, x) \rangle\;: A_1 \times A_2 \times A_3`$
変数を省略して、圏論風の記法で書けば：
$`\quad F_1 : T \times X \to A_1\\
\quad F_2 : T \times X \to A_2\\
\quad F_3 : T \times X \to A_3\\
\text{↓ インデックスに関するラムダ抽象 ↓}\\
\quad \langle F_1, F_2, F_3 \rangle\ : T\times X \to A_1 \times A_2 \times A_3`$
これは、$`i = 1, 2, 3`$ のインデックスを持つ関数のファミリー〈族〉 $`F_1,F_2, F_3`$ を素材としてタプル関数 $`\langle F_1, F_2, F_3 \rangle`$ を組み立てたことになります。インデックスに関するラムダ抽象は、関数のタプル構成だと言えます。
さらに、変数 $`x: X`$ に関してもラムダ抽象して次の関数が得られます。
$`\quad t : T, x : X, i : I \vdash F_i(t, x) \;: A_i\\
\text{↓ インデックスに関するラムダ抽象 ↓}\\
\quad t : T, x : X \vdash \wedge\, i : I. F_i(t, x)\;: \prod_{i\in I}A_i\\
\text{↓ 通常のラムダ抽象 ↓}\\
\quad t : T \vdash \lambda\, x : X. \wedge\, i : I. F_i(t, x)\;: [X \to \prod_{i\in I}A_i]`$
λΠ計算
前節では、通常のラムダ抽象の記号 $`\lambda`$ とインデックスに関するラムダ抽象の記号 $`\wedge`$ を区別しましたが、本質的な違いはありません。単一の記号で十分です。「インデックス」という呼び方や $`F_i`$ という書き方は、我々が勝手に決めているだけで、「インデックスに関するラムダ抽象は別扱い」というのも強い根拠がありません。
$`\wedge`$ の場合は、型のほうに $`\prod`$ が付くことになりますが、これも、常に $`\prod`$ が付くものだとします。特殊ケースとして、型ファミリーが定数値 $`A_i = C\;\text{forall }i`$ のときは次が成立します。
$`\quad \prod_{i\in I}A_i = \prod_{i\in I}C \cong [I \to C] = C^I`$
つまり、単純な型付きラムダ計算の拡張となる“パイ型を含んだ型付きラムダ計算”を定義できるのです。この拡張された型付きラムダ計算をλΠ計算と呼びます。
λΠ計算では、項を $`\lambda\,i\in I`$ で抽象（$`i`$ を束縛）したときは必ず型項も $`\prod_{i\in I}`$ で抽象（$`i`$ を束縛）します。このような抽象〈束縛〉をラムダ・パイ抽象〈ラムダ・バイ束縛〉、または依存ラムダ抽象〈dependent lambda abstraction〉と呼びます。依存してない場合の依存ラムダ抽象が単純な（以前からの）ラムダ抽象です。
ラムダ・パイ抽象の双対
ラムダ・パイ抽象〈依存ラムダ抽象〉 $`\wedge`$ の双対を記号 $`\vee`$ で書き表します。ラムダ・パイ抽象の双対の操作をブイ・シグマ余抽象〈vee-Sigma coabstraction〉と呼ぶことにします。いきなり「双対」とは言っても分かりにくいので、ラムダ・パイ抽象のときと同じ順序で話をします。
次のような型判断を考えます。
$`\quad t : T, j : J, b_j : \beta \vdash \tau : Y`$
ここで：
- $`t`$ は背景変数
- $`j`$ はインデックス
- $`\beta`$ は、$`t`$ を含まず*5、$`j`$ を含むかも知れない型項
- $`b_j`$ は、$`j`$ ごとに選んだ変数名（特定要素ではない）、変数の具体的な名前はなんでもよい。
- $`\tau`$ は、$`t, j, b_j`$ を含むかも知れない項
- $`Y`$ は固定された型で、項 $`\tau`$ の戻り型
この型判断に対して、インデックス（集合 $`J`$ 上を走る変数）でブイ・シグマ余抽象します。インデックスに関するブイ・シグマ余抽象の構文的なルールは次のとおりです。
$`\quad t : T, j : J , b_j : \beta \vdash \tau : Y\\
\text{↓ インデックスに関するブイ・シグマ余抽象 ↓}\\
\quad t : T, \sum_{j\in J}\beta \vdash \vee\, j : J. \tau \;: Y`$
項／型項の意味は次のとおりです。
- 型項 $`\beta`$ は、$`j\in J \mapsto B_j`$ という型ファミリーを定義する。
- 項 $`\tau`$ は、$`t\in T, j \in J, b_j \in B_j \mapsto G(t, j, b_j) \in Y`$ という関数を定義する。
ここで、$`b_j`$ は $`j`$ ごとに選んだ変数名で、集合 $`B_j`$ 上を走る引数変数です。変数名は何でもよく、$`j`$ から自動的に作った名前でもよいので、$`G(t, j, \text{-}_j)`$ のように無名変数ハイフンとして書いたほうが適切かも知れません。
インデックス $`j\in J`$ は下付きで $`G_j(t, b_j)`$ と書くことにして、構文より意味に注目するなら次のようになります。
$`\quad t : T, j : J, b_j : B_j \vdash G_j(t, b_j) \;: Y\\
\text{↓ インデックスに関するブイ・シグマ余抽象 ↓}\\
\quad t : T, b : \sum_{j\in J} B_j \vdash \vee\, j : J. G_j(t, b_j) ;: Y`$
$`J`$ は有限集合と仮定していたので、例えば $`J = \{1, 2, 3\}`$ とすると：
$`\quad t : T, j = 1, B_1 \vdash G_1(t, b_1) \;: Y\\
\quad t : T, j = 2, B_2 \vdash G_2(t, b_2) \;: Y\\
\quad t : T, j = 3, B_3 \vdash G_3(t, b_3) \;: Y\\
\text{↓ インデックスに関するブイ・シグマ余抽象 ↓}\\
\quad t : T, b :\sum_{j\in\{1, 2, 3\} } B_j \vdash \vee\, j: \{1, 2, 3\}. G_j(t, b_j) \;: Y`$
$`\vee\, j : \{1, 2, 3\}. G_j(t, b_j)`$ を、
$`\quad (\!| G_j(t, b_j) |\!)_{j \in \{1, 2, 3\} }\\
= (\!| G_1(t, b_1) \mid G_2(t, b_2) \mid G_3(t, b_3) |\!)`$
と展開して書けば：
$`\quad t : T, j = 1, B_1 \vdash G_1(t, b_1) \;: Y\\
\quad t : T, j = 2, B_2 \vdash G_2(t, b_2) \;: Y\\
\quad t : T, j = 3, B_3 \vdash G_3(t, b_3) \;: Y\\
\text{↓ インデックスに関するブイ・シグマ余抽象 ↓}\\
\quad t : T, b : (B_1 + B_2 + B_3)
\vdash (\!| G_1(t, b_1) \mid G_2(t, b_2) \mid G_3(t, b_3) |\!) \;: Y`$
変数を省略して、圏論風の記法で書けば：
$`\quad G_1 : T \times B_1 \to Y\\
\quad G_2 : T \times B_2 \to Y\\
\quad G_3 : T \times B_3 \to Y\\
\text{↓ インデックスに関するブイ・シグマ余抽象 ↓}\\
\quad (\!| G_1 \mid G_2 \mid G_3 |\!) : T \times (B_1 + B_2 + B_3 )
\to Y`$
これは、$`i = 1, 2, 3`$ のインデックスを持つ関数のファミリー〈族〉 $`G_1,G_2, G_3`$ を素材としてコタプル関数 $`(\!| G_1 \mid G_2 \mid G_3 |\!)`$ を組み立てたことになります。とはいえ、コタプル関数がいまいち謎かも知れません。次節でもう少し説明することにして、ラムダ抽象をしておきます。
$`\quad t : T, j = 1, B_1 \vdash G_1(t, b_1) \;: Y\\
\quad t : T, j = 2, B_2 \vdash G_2(t, b_2) \;: Y\\
\quad t : T, j = 3, B_3 \vdash G_3(t, b_3) \;: Y\\
\text{↓ インデックスに関するブイ・シグマ余抽象 ↓}\\
\quad t : T, b : (B_1 + B_2 + B_3 ) \vdash
(\!| G_1(t, b_1) \mid G_2(t, b_2) \mid G_3(t, b_3) |\!) \;: Y\\
\text{↓ 通常のラムダ抽象 ↓}\\
\quad t : T \vdash \lambda\, b : (B_1 + B_2 + B_3 ). (\!| G_1(t, b_1) \mid G_2(t, b_2) \mid G_3(t, b_3) |\!) \;: [(B_1 + B_2 + B_3 ) \to Y]`$
パターンマッチ多方向分岐
前節の最後のラムダ式 $`\lambda\, b : (B_1 + B_2 + B_3 ). (\!| G_1(t, b_1) \mid G_2(t, b_2) \mid G_3(t, b_3) |\!)`$ を解釈しましょう。
まず、次のような別名を導入します（単に短く書くためだけ）。$`\newcommand{\B}{\overline{B} }`$
$`\quad \B := (B_1 + B_2 + B_3)`$
$`\B`$ はタグ付きユニオン型なので、次のように書けることを思い出してください。
$`\quad \B := (\{1\}\times B_1) \cup (\{2\}\times B_2) \cup (\{3\}\times B_3)`$
$`b\in \B`$ は次の3つのケースがあります。
- $`b = (1, b_1),\; b_1 \in B_1`$
- $`b = (2, b_2),\; b_2 \in B_2`$
- $`b = (3, b_3),\; b_3 \in B_3`$
上記のラムダ式をより馴染みがある形で書くと次のようになります。$`t`$ は背景変数なので、このラムダ式の外で宣言・定義されています。
$`\lambda\, b : \B.\\
\quad \text{case } b \text{ of}\\
\qquad (1, b_1) \mapsto G_1(t, b_1)\\
\qquad (2, b_2) \mapsto G_2(t, b_2)\\
\qquad (3, b_3) \mapsto G_3(t, b_3)\\
\quad \text{end}`$
これは、パターンマッチによる多方向分岐の式です。実際のプログラミング言語でのキーワードは match with とかが多いかも知れません。パターンマッチ構文がなくても、if文やswitch文でも何とかなります。
ブイ・シグマ余抽象で得られる式
$`\quad \vee\, j: J. G_j(t, b_j) = (\!| G_1(t, b_1) \mid G_2(t, b_2) \mid G_3(t, b_3) |\!)`$
は、入力をパターンマッチして $`G_i`$ に振り分けて処理させるパターンマッチ多方向分岐を実現するものなのです。具体例は「具体例（なんの？）」の後半に書いてあります。
おわりに
以上のことをまとめると：
- 型ファミリーと関数のスパン・ファミリーに対してラムダ・パイ抽象を行うと、関数達のタプル構成と戻り型のパイ構成ができる。
- 型ファミリーと関数のコスパン・ファミリーに対してブイ・シグマ余抽象を行うと、関数達のコタプル構成と引数型のシグマ構成ができる。
- ブイ・シグマ余抽象した結果である“関数のコタプル”とは、パターンマッチ多方向分岐構造に他ならない。
関数達のタプル構成とコタプル構成が圏論的な双対になることは、付録に書いておきました。
ラムダ・パイ抽象とブイ・シグマ余抽象は、次の指数法則の形でも理解できます。
$`\quad (\prod_{i\in I} A_i)^X \cong \prod_{i\in I} (A_i^X)\\
\quad Y^{\sum_{j\in J} B_j} \cong \prod_{j \in J} Y^{B_j}`$
これらの指数法則は、論理の全称導入規則、存在除去規則に対応します。そう、カリー／ハワード／ランベック対応ですね。今日は論理との対応は全然触れませんでしたが、またいずれ機会があれば。
付録：圏論的解釈
背景変数（環境からの情報）があると話が少し複雑になるので、背景変数がない場合を扱います。
有向グラフ $`K, L`$ に対して、その頂点の集合は圏と同様に $`|K|, |L|`$ と書きます。新しい有向グラフ $`M = K*L`$ （$`K`$ と $`L`$ のジョイン）を次のように定義します。
- $`|M| := |K| + |L|`$
- $`K`$ の辺はすべて $`M`$ の辺とする。
- $`L`$ の辺はすべて $`M`$ の辺とする。
- すべての $`(a, b)\in |K|×|L|`$ に対して、$`a`$ から $`b`$ に向かう辺を追加する。
集合 $`I`$ と単元集合 $`\{\top\}`$ を離散有向グラフとみなして作った有向グラフ $`\{\top\}*I`$ をスパングラフ〈span graph〉または錐グラフ〈cone graph〉と呼びます。
同様に、有向グラフ $`I* \{\bot\}`$ をコスパングラフ〈cospan graph〉または余錐グラフ〈cocone graph〉と呼びます。
スパングラフ／コスパングラフは、グラフの辺を射とみなし、頂点ごとの恒等射を追加して圏とみなします。関手 $`F: \{\top\}*I \to {\bf Set}`$ をスパン・ファミリーまたは（集合圏の）錐〈cone〉、関手 $`G: I* \{\bot\} \to {\bf Set}`$ をコスパン・ファミリーまたは（集合圏の）余錐〈cocone〉と呼びます。
集合 $`I`$ を離散圏とみなして、関手 $`A, B:I \to {\bf Set}`$ とは（型は集合だとして）型ファミリー〈type family〉のことです。
スパン・ファミリー〈錐〉 $`F:\{\top\}*I \to {\bf Set}`$ が、“$`I`$ に制限したとき $`A`$ に一致する”なら、底面 $`A`$ の錐〈cone of base $`A`$〉といいます。同様に、コスパン・ファミリー〈余錐〉 $`G:I * \{\bot\} \to {\bf Set}`$ が、“$`I`$ に制限したとき $`B`$ に一致する”なら、余底面 $`B`$ の余錐〈cocone of cobase $`B`$〉といいます。
ここから先、極限と余極限が出てきますが、極限・余極限については次の記事を参照してください。
関手 $`A:I \to {\bf Set}`$ の極限対象〈limit object〉を次のいずれかで書きます。
- $`\mrm{lim}_{i\in I} A_i`$
- $`\prod_{i\in I} A_i`$
- $`\forall i\in I. A(i)`$
- $`\bigwedge_{i\in I} A_i`$
- $`\Pi (i : I). A(i)`$
実際には、書き方のバリエーションや略記法はもっともっとあります。無闇に書き方が多いのは、同じ概念を異なる分野で繰り返し定義したという歴史的経緯によります。
関手 $`A:I \to {\bf Set}`$ の極限錐〈limit cone〉は、極限対象を頂点とする錐です。極限錐の実体は、次のような射影射〈projection morphism〉の集まりです。
$`\quad (\pi_{\xi} : \mrm{lim}_{i\in I} A_i \to A_\xi)_{\xi \in I}`$
特定対象 $`\mrm{lim}_{i\in I} A_i `$ への定数値関手から $`A`$ への自然変換と言っても同じことです。
関手 $`A:I \to {\bf Set}`$ の極限錐 $`\mrm{Lim}\; A`$ （大文字エルに注意）は、$`A`$ を底面とする錐の圏 $`\mrm{Cone}(A: I \to{\bf Set})`$ の終対象なので、錐〈スパン・ファミリー〉$`F`$ から唯一の射
$`\quad F \to \mrm{Lim}\; A \In \mrm{Cone}(A: I \to{\bf Set})`$
が在ります。錐の圏の射は、頂点のあいだの射で決まります。その頂点のあいだの射を次のように書きます。
$`\quad \mrm{tuple}(F) : F(\top) \to \mrm{lim}\; A \In {\bf Set}`$
$`\mrm{tuple}(F)`$ の別な書き方は：
- $`\lambda\, i\in I. F_i`$
- $`\wedge\, i \in I. F_i`$
- $`\langle F_i \rangle_{i \in I}`$
型ファミリー $`B:I \to {\bf Set}`$ とコスパン・ファミリー〈余錐〉$`G:I * \{\bot\} \to {\bf Set}`$ の場合は、話が双対になるだけです。
関手 $`B:J \to {\bf Set}`$ の余極限対象は、次のいずれか（やその他のバリエーション／略記）の記法で書きます。
- $`\mrm{colim}_{j\in J} B_j`$
- $`\sum_{j\in J} B_j`$
- $`\exists j\in J. B(j)`$
- $`\bigvee_{j\in J} B_j`$
- $`\Sigma (j : J). B(j)`$
$`B`$ を底面とする余錐の圏 $`\mrm{Cocone}(B: J \to {\bf Set})`$ の“始対象＝余極限余錐”から余錐〈コスパン・ファミリー〉 $`G`$ への唯一の射があります。
$`\quad \mrm{Colim}\; B \to G \In \mrm{Cocone}(B: J \to {\bf Set})`$
余錐の圏の射は、余頂点のあいだの射で決まり、それを次のように書きます。
$`\quad \mrm{cotuple}(G) : \mrm{colim}\; B \to G(\bot) \In {\bf Set}`$
$`\mrm{cotuple}(G)`$ の別な書き方は：
- $`\vee\, j \in J. G_j`$
- $`(\!| G_j |\!)_{j \in J}`$
