ガチ勢になるための圏論勉強会 第一回 まとめ

Partake で発表したガチ勢になるための圏論勉強会 第一回では A.Pitts の Relational Properties of Domains の第一節と第三節を読んだ (第二節は本文を読んでからのほうが意味が分かりそうなので後回しした) ので、それのまとめ。というか分量的に言えばでっかい注釈。

ところで blogger で脚注を書いてそこに本文からリンクを貼るの自動化する方法知ってる人が居たら教えて下さい。この記事では全部手打ちしてるので…

第一節: この論文の目的と範囲

この論文の本題は再帰的に定義されたデータ型に機械的に表示 (denotation) を与える方法を確立すること、それからその表示を元にして、そのデータ型を扱うプログラムについて帰納法や余帰納法と言った証明テクニックを使うことを正当化する事。 具体例は論文では与えられていないが、こういう話だと考えられる。例えば OCaml で

type int_list = Nil | Cons of int * int_list

という定義があった時、これは有限の整数のリスト全てを含む集合 (型) であって、この型を使った関数

let rec map f = function
  | Nil -> Nil
  | Cons (x,xs) -> Cons (f x, map f xs)

let id x = x 

などについてmap id xsが常にxsと等価であるとかそういう事実を示すには普通に帰納法を使えば良い[注1]。int_listは Nil に有限回 Cons をつけて作ったデータ全ての集合で、かつそれ以外のデータを含まないのだから、map id Nil = Nil とmap id xs = xs ならば map id (Cons (x,xs)) = Cons (x,xs) を示すという具合だ。(以下、必要に応じて(::), [] などの糖衣構文を使う。)

しかしこのやり方は遅延データ構造には使えない。Haskell で

type IntList = Nil | Cons Int IntList

と書けばこれは無限リストも含むので、上記のような Nil から始めてうんたらかんたらという帰納法は Nil を含まないリストを取りこぼしてしまう。そもそもこういう型にはどういうデータが含まれていてどういうデータが含まれていないのだろう? [1,2,3,...] ++ [42]のように無限に続いたリストの後に、おまけのように[42]がくっついているようなデータは含まれていると考えたほうがいいのだろうか?[注2] 同様の問題は OCaml で関数や lazy を使って遅延リストをエンコードした場合にも起きる。

この Pitts の論文では、こうした再帰的に定義された型に対して、遅延が含まれていてもいなくてもその型に含まれるデータ全体の集合と、そのデータ型についてあれこれ証明する時に使えるテクニックを systematic に導出する方法を与える。このテクニックにより computational adequacy の証明なども簡単に行えるようになる。

第三節: 領域方程式の最小解

今回カバーした部分はセットアップ部分なのでそれほど難解な内容は無い。再帰的なデータ型は $\alpha \cong \Phi\,\alpha$ という領域方程式の最小解と解釈する。例えば整数のリストは $\alpha \cong 1 + (\text{Int} \times \alpha)$ を満たす集合 $\alpha$ [注3]。$\Phi$ は $(+),(\times),(\rightarrow)$ を組み合わせて作るが、これらの領域構築子は次のように正格・非正格のバリエーションがある。以下、$\mathbf{Cpo}_\bot$ は⊥を含む完備部分順序 (= pointed cpo = cppo) とそれらの間の正格連続関数からなる圏。全ての射 $f$ について $f\,\bot =\bot$ が要請されることに注意。また、これらの関手は全て局所連続と言って、射への作用を $\operatorname{Hom}(A,B)$ に制限した物がどの $A,B$ についても連続関数になる。

Lifting 関手 $-_{\bot} : \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$

新たな最小限 $\bot$ を付け足す。この関手を射 $f$ に適用してできる射 $f_\bot$ は
$$\begin{align*} f_\bot\,\bot &= \bot \\ f_\bot\,x &= f\,x & \text{($\bot$ 以外)} \end{align*}$$

積関手 $(\times), (\otimes) : \mathbf{Cpo}_\bot \times \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$

普通の集合論的なデカルト積 $A\times B = \{ (a,b) : a \in A, b \in B \}$ に $(a,b) \sqsubseteq (x,y) \Longleftrightarrow a \sqsubseteq x \land b \sqsubseteq y$ という順序を入れると $(\bot_A,\bot_B)$ を最小元に持つ cppo になる。$(a, \bot_B)$ や $(\bot_A, b)$ が $(\bot_A,\bot_B)$ と別物の扱いで、$(,)$ が非正格な構築子になる。ただし Haskell の (A,B) 型はデカルト積ではなくその lift $(A\times B)_\bot$ と一致する。この関手を射 $(f,g)$ に適用してできる射 $f\times g$ は
$$(f\times g)\,(x,y) = (f\, x, f\, y)$$ 非正格性により引数が $(x,y)$ の形をしていると仮定している事に注意。
一方潰れた積 (smash product) の $(\otimes)$ は $(,)$ 構築子を正格にとるため、$(a, \bot_B)$, $(\bot_A, b)$, $(\bot_A, \bot_B)$ を全部一つの $\bot$ に潰す。それ以外はデカルト積と一緒。OCaml の a * b は $A\otimes B$ になる。$f\otimes g$ は
$$\begin{align*} (f \otimes g)\,(x,y) &= (f\,x, g\,y) \\ (f \otimes g)\,\bot &= \bot \end{align*}$$

和関手 $(+), (\oplus) : \mathbf{Cpo}_\bot \times \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$

集合論的な非交和 $A\uplus B = \{\operatorname{inl}\,a : a \in A\} \cup \{\operatorname{inr}\,b : b \in B\}$ は $\operatorname{inl}\,a$ と $\operatorname{inr}\,b$ を一切比較不可能にするような順序で完備部分順序になるが、それだと⊥を持たないので新たに付け足す: $$A+B = (A\uplus B)_\bot$$ これは $\operatorname{inl}\,\bot$ や $\operatorname{inr}\,\bot$ が $\bot$ とは別になるので $\operatorname{inl}, \operatorname{inr}$ が非正格になり、Haskell の Either A B と一致する。射への作用は $$\begin{align*} (f + g )\,(\operatorname{inl}a) &= \operatorname{inl}(f\,a) \\ (f + g )\,(\operatorname{inr}b) &= \operatorname{inr}(g\,b) \\ (f + g)\,\bot &= \bot \end{align*}$$ 一方予め $A$ と $B$ からそれぞれの⊥を消した集合 $A_\downarrow = A - \{\bot_A\}$ と $B_\downarrow$ を作り、それの非交和に改めて最小元を付け足すと構築子 $\operatorname{inl}$, $\operatorname{inr}$ を正格にとる潰れた和 (coalesced sum) ができる。
$$A\oplus B = (A_\downarrow \uplus B_\downarrow)_\bot$$ OCaml の variant は $A \oplus B$。射への作用は
$$\begin{align*} (f \oplus g )\,(\operatorname{inl}a) &= \left\{\begin{array}{ll}\operatorname{inl}\,(f\,a) & (f\,a \neq \bot) \\ \bot & (f\,a = \bot)\end{array}\right\} = \operatorname{inl}_\bot(f\,a) \\ (f \oplus g )\,(\operatorname{inr}b) &= \left\{\begin{array}{ll}\operatorname{inl}\,(g\,a) & (g\,a \neq \bot) \\ \bot & (g\,a = \bot)\end{array}\right\} = \operatorname{inr}_\bot(g\,b) \\ (f \oplus g)\,\bot &= \bot \end{align*}$$ 注意: Pitts はなぜか $(+)$ の方だけ避けている。ひょっとしたら今後出てくる定理が当てはまらない場合があるのかも知れない。$(+)$ の射への作用は局所連続性は持つが、非正格である。

関数空間関手 $(\rightarrow), (\mathrel{-\kern{-1ex}\circ}) : \mathbf{Cpo}_\bot^\text{op} \times \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$

$A \rightarrow B$ は $A$ から $B$ への正格とは限らない連続関数全体の集合で、順序は $f \sqsubseteq g \Leftrightarrow \forall x.\ f\,x \sqsubseteq g\,x$ (point-wise ordering) で $\lambda \_.\,\bot$ を最小元に持つ。$\bot$ と $\lambda \_.\bot$ を同一視することに注意。Haskell では関数型をパターンマッチで分析できないため $\bot$ と $\lambda \_.\bot$ を区別する手段が無いので、A -> B の表示はそのまま $A \rightarrow B$ になる。
関数空間関手の射 $(f,g) : (A,B) \rightarrow (C,D)$ への作用は $$\begin{align*} (f \rightarrow g) &: (A \rightarrow B) \rightarrow (C \rightarrow D)\\ (f \rightarrow g) &= g \circ - \circ f \end{align*}$$ となる。正格関数空間 $A \mathrel{-\kern{-1ex}\circ} B$ は $A \rightarrow B$ を正格関数だけに制限したもの。それ以外は $(\rightarrow)$ と一緒。


さて、上記の関手を組み合わせてできた $\Phi$ が与えられた時 $\alpha \cong \Phi\,\alpha$ なる cppo $\alpha$ は大抵複数あるが、データ型の解釈では特に「最小」の解が求められる。直観的には [1,2,3,...] ++ [42] のように計算に携わらない「ゴミ」が混じったデータを排除するという事だ。最小性により解が一意に定まるし、また計算結果について証明する時に意味のない区別を排除する事にもなる。[注4]
Pitts は「最小性の定義はいくつかある」と書いているが、単に集合として最小 (i.e. $(\subseteq)$ について最小) でいいのかどうかは書いていない。それでもいいのだけど射以外の概念を持ちだした定義なので圏論的に筋が悪いという事かも知れない。
ともかく射のみによる圏論的な最小性の定義を模索するのだが、ここで一つ問題がある。例えば $\Phi\,\alpha = \alpha \rightarrow \alpha$ の場合、$\Phi$ は引数 $\alpha$ を反変にも共変にも使うので $\mathbf{Cpo}_\bot$ からの関手にならない。そこで $\Phi$ の引数を共変位置と反変位置で別の引数に分けて、profunctor (この用語の和訳を誰かプリーズ) $\hat{\Phi}$ にする。例えば $$\Phi\,\alpha = \alpha \oplus (\alpha \rightarrow \alpha \otimes \text{Int})$$ なら別々の引数 $\alpha^-$, $\alpha^+$ を用意して $$\hat{\Phi}\,(\alpha^-, \alpha^+) = \alpha^+ \oplus (\alpha^- \rightarrow \alpha^+ \otimes \text{Int})$$ とする。こうして作った $\hat{\Phi} : \mathbf{Cpo}_\bot^\text{op} \times \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$ に対して $i : \hat{\Phi}\,(D,D) \cong D$ となるような $D$ が存在すればそれは当然、元の領域方程式 $\Phi\,\alpha \cong \alpha$ の解になる。こういう $i,D$ の対を不変性 (invariant)、特に $D$ を不変対象 (invariant object) と呼ぶ。この $\hat{\Phi}$ に対して最小性は次のように定義できる。
定義3.2 $\hat{\Phi} : \mathbf{Cpo}_\bot^\text{op} \times \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$ を、射に対する作用が連続な関手とする。不変性 $i : F\,(D,D) \cong D$ について $\operatorname{fix}\,(\lambda f.\ i\circ \hat{\Phi}\,(f,f)\circ i^{-1})$ が恒等関数である時、$i,D$ は最小であるという。但し $\operatorname{fix}$ は (上記の関数空間のところで定義された) 関数同士の順序に対して最小であるような不動点を求める関数。

この定義は $\hat{\Phi}$ を(遅延)リスト型を生成する関手 $\hat{\Phi}\,(\alpha^-, \alpha^+) = 1 + (\text{Int} \times \alpha^+)_\bot$ に置き換えて考えると分かりやすい。$\delta := (\lambda f.\ i\circ \hat{\Phi}\,(f,f)\circ i^{-1})$ とすると、 $$\begin{align*} \delta\,f\,[] &= [] \\ \delta\,f\,(x:y) &= i(f\,(\operatorname{inr}(x,y))) \end{align*}$$ つまりリスト型の引数の中からリスト型のフィールドを探してそこに $f$ を適用するという関数になる。詳細には $i^{-1}$ でリスト型を $(+), (\uplus), -_\bot$ を使った表現にバラし、その結果に $f$ を fmap しているという事になる。この調子で $\delta^n\,\bot$ を展開すると $$\begin{array}{lclll} \delta\,\bot\,[] &=& [] \\ \delta\,\bot\,(x:y) &=& i\,\bot &=& \bot \\ \delta^2\,\bot\,(x:y) &=& i(\operatorname{inr}(x,\delta\,\bot\,y)) &=& x:\bot \\ \delta^2\,\bot\,(x:y:z) &=& i(\operatorname{inr}(x,\delta\,\bot\,(y:z))) &=& x:y:\bot \\ \delta^3\,\bot\,(x:y:z) &=& i(\operatorname{inr}(x,\delta\,\bot\,y:z)) &=& x:y:\bot \\ \delta^3\,\bot\,(x:y:z:w) &=& i(\operatorname{inr}(x,\delta^2\,\bot\,(y:z:w))) &=& x:y:z:\bot \\ &\vdots& \end{array}$$ という具合で、$\delta^n\,\bot$ は長さ $n$ の prefix を取り、それ以降は⊥で置き換える関数になる[注5]。$\operatorname{fix}\delta$ はそれの極限だから、 $$\begin{align*} \operatorname{fix}\delta\,\bot\,(x_1:x_2:x_3:\cdots) &= \bigsqcup\{\bot, (x_1:\bot), (x_1:x_2:\bot), \ldots \} \\ &= x1:x_2:x_3:\cdots \end{align*}$$ となる。つまり、入力リストに終端があるならそこまでコピーし、終端がないなら先頭から有限ステップで到達できる全要素をコピーするのでこれらの入力に対し恒等関数になる。一方、前出の [1,2,3...] ++ [42] という、無限遠に続きを持つリストは有限 prefix 全ての最小上限ではないので、このデータを含む集合は $\alpha \cong 1 + (\text{Int} \times \alpha)_\bot$ の最小解にならない。同様の理由で [1..] ++ [42] というプログラムが生成するデータは[1..]と同じ物にならざるを得ない。これは両者を区別するような関数が Haskell 内で実装不可能であるという直観に合致する。
ここでは非正格な $(+),(\times)$ を使ったが、正格な $(\oplus),(\otimes)$ を使うと 有限リストが出来る。具体的には $\delta^n$ の返り値を構築するときの $\operatorname{inr}$ が正格なので、入力リストの長さが $n$ 未満でない限り戻り値全体が⊥になる。
定理3.3はこうした最小性を満たす解が常に存在すると主張している。

三行まとめ

• 再帰データの領域は $(+),(\times),(\rightarrow)$ からなる関手 $\Phi$ に対して $i : D \cong \Phi\,D$ なる最小の $i,D$ の $D$
• ただし $(+),(\times),(\rightarrow)$ にはそれぞれ正格版と非正格版があり、しかも一般には $\Phi(\alpha^-, \alpha^+)$ と反変位置・共変位置を分けないと関手にならない
• $\operatorname{fix}(\lambda f.\ i\circ \operatorname{fmap}f \circ i^{-1}) = \operatorname{id}$ なら最小

多分次は定理 3.3 の証明から。

注1: OCaml でも let rec x = Cons (0, x) とかすれば無限リストが作れるがここでは無視する。

注2: 混乱のないように書いておくと、そういうリストは存在しないと考えるべき。Haskell で [1..] ++ [42]と書いた時に生成されるデータは[1..]とだけ書いた時にできるデータと同じだ。[1..]の部分は有限時間で辿り終える事ができないので、++[42]の部分はプログラムの実行に一切影響を与えない。したがって表示意味論的には++[42]は消える(無視される)。

注3: ここで 1 というのは値が一種類しか無い型 (OCaml でいう unit、Haskell では ()) で、variant は和、複数引数のコンストラクタは積とみなしている。こうした $\alpha$ に関する方程式を領域方程式と呼ぶ。

注4: 例えば [1,2,3,...] ++ [42] というデータを含まない解を採用しておけば [1..] ++ [42] というコードと [1..] というコードの意味 (表示; 返り値) が一致するので、f [1..] が何かの仕様を満たすことが分かった時、それをわざわざ f ([1..] ++ [42]) について証明し直さなくて良い。

注5: 一般には入力を深さ $n$ まで探索してそれより深い位置に出現する $\alpha$ を $\bot$ しか含まない型に置き換える。