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

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

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

参照用 記事

集合の添字族とユニオン型とコタプル構成

集合の添字族を話題の中心として、「タプル型とタプル構成」の双対概念である「ユニオン型とコタプル構成」について説明します。

内容:

集合の添字族

Iを集合として、i∈I ごとに集合Aiが対応しているとき、これを集合の添字族(indexed family of sets)とか、添字付けられた集合族、あるいは単に集合族と呼びます。集合Iは添字<そえじ>の集合となります。以下では、主に用語「集合族」を使います(短いので)。

集合族を表すために、{Ai | i∈I} のような書き方がよく用いられますが、ここでは (i∈I | Ai) を使います*1。I = {1, 2, ..., n} のときは、(A1, A2, ..., An) という集合の並び(集合を項目とするタプル)としても表せます。

下付き添字を使いましたが、Ai の代わり A[i] とか A(i) と書いても同じことです。要するに、i |→ Ai という対応なので、集合族とは“集合を値とする関数”に過ぎません。十分に大きな集合Uを用意すれば、Ai⊆U と考えることができるので、Iを添字の集合とする集合族Aは、A:I→Pow(U) という関数です(Pow(U) はUのベキ集合)。

A:I→Pow(U) が集合族のとき、特に断りがないなら、I、U、Aには何の条件も付けません。次の点には注意してください。

  • Iが有限とは限らない。Iは無限集合がかもしれない。
  • Iは空かもしれない。Iが空のとき、A:I→Pow(U) という集合族は一つだけ存在する。
  • Uは空かもしれない。Uが空のとき、A:I→Pow(U) という集合族は一つだけ存在する。
  • i, j∈I、i≠j に対して、Ai = Aj かもしれない。つまり、同じ集合が何度も出現してよい。
  • i∈I に対して、Ai が空かもしれない。

IやUが空だと意味がないときもあるので、(ときに暗黙に)I, Uが空でないと仮定することがあります。より強く、次の条件を付けたほうがいいときもあります。

  • Iは空でなくて、すべての i∈I に対してAiが空ではない。

この条件を非空条件と呼ぶことにします。

集合族のcase文による構成

添字の集合Iが有限集合のときは、添字の集合Iの要素iのそれぞれに対して、集合Aiを具体的に示せばいいのですが、Iが無限集合だとそうもいきません。

Iが無限集合、あるいは有限でも大きな集合のとき、次の方法が有効です; Fは有限集合で、F⊆I とします。Fの要素iにはAiをいちいち具体的に与えます。Fに所属しない残りの要素jには一律に Aj = B と定義します。実用上はこれで十分なことが多いのです。F = {a, b, c} として、擬似コードのif文を使って書けば:

A[i : I] := 
  if i == a then Aa
  else if i == b then Ab
  else if i == c then Ac
  else B

このif文の繰り返しをもう少し簡略に次のように書くことにします。

A[i : I] := 
  case i {
    a => Aa,
    b => Ab,
    c => Ac,
    * => B
  }

集合族の逆像による構成

EとIが集合で、f:E→I が関数(写像)だとします。このとき常に、fから、Iを添字集合とする集合族を一意的に作れます。作り方は簡単で、A:I→Pow(E) を次のように定義します。

  • Ai := f*(i)

ここで、f*(i) は、iにおけるfの逆像集合です。f-1(i) と書くことが多いですが、fの逆写像との混乱を避けるためf*を使いました。より具体的に書けば次のとおりです。

  • Ai := {x∈E | f(x) = i}

一方、集合族 A:I→Pow(U) があるとき、f:E→I が構成できて、集合族 (i∈I | f*(i)) がもとの集合族Aと同じになるように出来ます。まず、集合Eを次のように構成します。

  • E := Σ(i∈I | Ai) = (すべての i∈I に対するAi達の直和集合)

集合族の総和は、「指数法則に類似のセクション公式」でも触れました。Σ(i∈I | Ai) は次のように定義されるのが普通です。

  • Σ(i∈I | Ai) := {(i, a)∈I×U | a∈Ai}

(i, a) におけるiは、データ型に関する用語法では弁別子(descriminator)とかタイプタグ(type tag)、あるいは単にタグと呼ばれます。Σ(i∈I | Ai) は、成分型がAiである弁別子付きユニオン型タグ付きユニオン型と呼ばれるものです。値以外に弁別子(タグ)が付いているので、このユニオン型は排他的になります。ユニオン型の代わりにバリアント型と呼ぶこともありますね。

さて、E := Σ(i∈I | Ai) としてEを定義できたら、関数 f:E→I を次のように定義します。

  • f((i, a)) := i

関数fは、弁別子付きの値(タグ付きの値)に対して、その弁別子(タグ)を対応させる関数です。こうして作ったfから、もとの集合族 A:I→Pow(U) が再現できることは練習問題とします。

以上のことから、任意の関数(写像)と集合族は、逆像を使った構成(とその逆方向の構成)により互いに移りあえることが分かりました。データ型を扱う人は、この変換がサッと出来ると便利だし、出来ないと困ることがありますよ。

総積/総和と非空条件について

集合族 (i∈I | Ai) があると、これらの総積(すべてのiに渡る直積)と総和(すべてのiに渡る直和)を作ることができます。それを、総積記号Π(大文字パイ)と総和記号Σ(大文字シグマ)を使って表します。

  • Π(i∈I | Ai) := (集合族 (i∈I | Ai) の総積)
  • Σ(i∈I | Ai) := (集合族 (i∈I | Ai) の総和)

総積 Π(i∈I | Ai) は、タプル成分に名前が付いている名前付きタプル型*2、総和 Σ(i∈I | Ai) は、先ほど説明した弁別子付きユニオン型となります。名前付きタプル型は、ハッシュマップ、辞書、レコード、(JSONの意味の)オブジェクトなどとしてよく使われていますが、双対である弁別子付きユニオン型の利用例は少ないようです。

任意の集合族に対して総積と総和を作れますが、現実的状況では、Aiが空であるのは嬉しくないことがあります。特に総積では、1個でも空集合が混じっていると総積全体が空になってしまいます。このため非空条件を要求することがあります。

集合族 A:I→Pow(U) が非空かどうかわからないときでも、Aから非空条件を満たすA'を作るのは簡単です。空となる部分を取り除けばいいのです。Iの部分集合I'を次のように定義します。

  • I' = {i∈I | Ai が空ではない}

もとの集合族AをI'上に制限したものをA'とするだけです。

この方法で作ったI'、A'に対して、Π(i∈I | Ai) と Π(i∈I' | A'i) はまったく別物になる可能性があります。しかし、Σ(i∈I | Ai) と Σ(i∈I' | A'i) は事実上同じです。定義を振り返れば分かりますよね。

それと、次の事実は認識しておきましょう。

  • 集合族 A:I→Pow(U) が非空条件を満たすことと、対応する関数(写像) f:E→I が全射であることは同値である。

コタプル構成

今まで集合の族を考えてきましたが、同様にして関数(写像)の族を考えましょう。一般には、fiを関数として、関数の族は (i∈I | fi) と書けます。あまり一般的な族を考えてもとりとめもないので、集合族 (i∈I | Ai) と関連した関数族を考えることにします。

以下では、集合族と関数族が同じ添字集合Iを共有する状況を考えます。同じIに対して、集合族 (i∈I | Ai) と関数族 (i∈I | fi) があるわけです。さらに、集合Yをひとつ固定して、各fiが、fi:Ai→Y とう形をしていると仮定します。

この状況だと、関数族 (i∈I | fi:Ai→Y) は、総和 Σ(i∈I | Ai) 上で定義された関数を一意的に定めます。場合分けによる関数の構成です。有限的に書き下せる例を挙げると:

k(x : Σ(i∈I | Ai)) := 
  if x∈Aa then fa(x)
  else if x∈Ab then fb(x)
  else if x∈Ac then fc(x)
  else g(x)

見れば分かると思いますが; Aa上で定義されたfa、Ab上で定義されたfb、Ac上で定義されたfc、その他部分で定義されたgから、kを定義しています。

型(集合)でディスパッチするtypecase文を使って書けば:

k(x : Σ(i∈I | Ai)) := 
  typecase x {
    Aa => fa(x)
    Ab => fb(x)
    Ac => fc(x)
    *  => g(x)
  }

fa, fb, fc, g から新しい関数kを場合分けで構成してますが、このような構成法をコタプル構成といいます。ユニオン型というデータ型の構成法と、コタプル構成という関数の構成法がちょうど対応してます。ユニオン型/コタプル構成の双対はタプル型/タプル構成ですが、こちらはよく知られているので割愛します。



タプル構成/コタプル構成は、圏論の極限と双対性に基づく概念です。この概念を発展させると、デカルト閉圏、デカルト半環圏、デカルト作用圏などに至り、リッチなデータ型の世界が拡がります。「計算モデル: 大域と局所、不純と純粋」あたりを基点にリンクをたどると、断片的ですが、これらの定式化を話題にしているエントリーが見つかります。

*1:指数法則に類似のセクション公式」では、{Ai | i∈I} という記法も使ってました。

*2:並びを使って表現されるタプル型では、番号または位置により成分を識別します。