Co-data 【新歓ブログリレー2017 21日目】

こんにちはphi16です。traPではプログラム担当です。今回はふしぎなおはなしをします。これもまた部内wikiから拾ってきたものです。

プログラムではいろんなデータを扱うと思います。いろんなデータに対して操作を行って新しいデータを作り、情報を抽出したり。
データとは何でしょうか。何を以ってデータと言うのでしょうか。いくら情報を持っているはずでもそれを取り出す方法がなければ情報が無いことと同じです。暗号などはこれを基礎として作られていますね。

逆に言えばデータというのは操作を伴って初めてデータとして存在しうるのです。

ならばデータとは操作そのものではないでしょうか。

まえがき

いわゆるデータ、Data に対して余データ、Codata と呼ばれる概念があります。これは一般のデータが有限であるのに対して無限の情報を表現するものです。無限の情報をどうやってコンピュータで表現すれば良いでしょうか？

内部は無限の情報であったとしても、データというのは本質的に操作によってでしか情報を取り出す事ができません。無限回の操作を行わなければ内部に無限の情報が含まれていることがわからないのです。「有限回の操作しか行わないこと」を以って無限のデータを実際に構築することができます。

例はそんなに難しくはありません。

struct Tree {
  Tree* left;
  int value;
  Tree* right;
};

Tree t;
t.left = &t;
t.value = 1;
t.right = &t;

tはどんな情報を持っているでしょうか？left,rightは自分自身を指していますが、アドレスという情報を知らなければこれは全てのノードに1を持つ無限の二分木と区別が付きません。

また、こんな例もあります。

var a = {};
a.value = 1;
a.next = a;

これも同じで、オブジェクト間の同等性を知ることができなければ無限に続く1の列と区別が付きません。

このようにして無限のデータを表現する、Codataの概念を獲得することができました。ではこれで何が出来るのでしょうか？通常のデータと何が違うのでしょうか。そんなおはなしをしていきます。

最近はStream型として有名になってきたかもしれませんね。1つの具体例にすぎませんが。

Codataを表現する

構造の型が $S$ であるとします。 $S$ が 2つの $i n t$ 型を丁度持つとしたとき、これを $S = i n t \times i n t$ と表記します。要は掛け算記号を使うということです。

これによって、今までの例では t の型は $S = S \times i n t \times S$ と表せます。(ポインタにNULLが入らないものとします)
また、a の方は $S = i n t \times S$ となることがわかります。(同様にundefined,nullでないものとします)

これを一般化して、 $S = F (S)$ の形式としてCodataを表します。つまり $F$ を指定すればいいわけです。
無限二分木のときは、 $F (X) = X \times i n t \times X$ となります。
無限リストでは $F (X) = i n t \times X$ ですね。

これによって再帰構造を $S = F (S)$ の部分だけに押し込めることが出来たので、扱いやすくなりました。

Coiteration : 余反復

Coiterationとは、Codataを作り出す方法の一つです。先程は「全ての要素が同じ値を持つ構造」しか作れませんでしたが、勿論そんなことはありません。

まぁ上で例示した方法ではどちらも出来ないですけど、それは本質ではありません。

一般的に考えてみましょう！

$S$ を表現するためにはもちろん $F (S)$ を表現できればいいわけで、 $F (S)$ というのは $S$ の各要素のことです。つまり $S$ の各要素を定めれば $S$ が定まります。これは当然ですね。

ここで発想の転換をします : 「 $S$ の各要素で $S$ を構成する」のではなく、「 $S$ から $S$ の各要素を取り出す関数によって $S$ を定義する」のです。

本質的に(抽象的に)、必要な構造は $S$ から $S$ の各要素を拾い出す関数たちです。
無限二分木の場合は $l e f t : S \to S, v a l u e : S \to i n t, r i g h t : S \to S$ を与えれば良いわけです。
無限リストなら $h e a d : S \to i n t, t a i l : S \to S$ となります。

陽にデータを持つ必要はありません！ これが重要なところです。全てのデータアクセスをこの関数群を通して行えば良いのですから、困ることはありません。

例えば $h e a d (s) = 1, t a i l (s) = s$ という関数群を考えると、先頭は明らかに $1$ 、その次も $1$ と、無限に $1$ が続くリストを表現できていることがわかります。この調子です。

複数の関数をまとめてあげることで、無限二分木では $⟨ l e f t, v a l u e, r i g h t ⟩ : S \to S \times i n t \times S$ 、無限リストでは $⟨ h e a d, t a i l ⟩ : S \to i n t \times S$ があればいいということがわかります。
簡単に一般化できて、 $S \to F (S)$ と捉えることができます。これによって要素へのアクセスが可能となります。

さらに一般化して、任意の写像 $X \to F (X)$ を生成規則とみなしてみます。
集合 $X$ に対して $a : X \to F (X)$ を持っているとき、 $x \in X$ に対して $a (x) \in F (X)$ を計算することができます。 $F (X) = X \times X$ などとしてみると $a (x) = (p, q)$ となりますが、 $p, q$ それぞれに対して $a$ を適用することで更に $a (p), a (q) \in F (X)$ を獲得することができます。これは実質的に $x$ がもともと $a (p), a (q)$ を内部に情報として持っていたということと区別が付きません。

アクセサ $a : X \to F (X)$ を備えた集合 $X$ は、アクセサの働きによりCodataと同様の振る舞いをすることがわかります。
$X \neq = F (X)$ ではありますが、 $S = X \times (X \to F (X))$ とすることで、 $S = F^{'} (S)$ となるようなCodataを構成できるのです！

というわけで、これがCoiterationです。 $X \times (X \to F (X))$ さえあればCodataを構成できるのです。

では例を考えてみましょう！とりあえずは無限リスト $F (X) = i n t \times X$ のことを考えます。

自明な例

$X = {*}, h e a d_{X} (*) = 1, t a i l_{X} (*) = *$ とし、 $s \in S = X \times (X \to F (X))$ として $s = (*, ⟨ h e a d_{X}, t a i l_{X} ⟩)$ すると、先程言ったように全ての要素が $1$ の無限リストを表します。

自然数列

$X = i n t, h e a d_{X} (n) = n, t a i l_{X} (n) = n + 1$ とし、 $s = (0, ⟨ h e a d_{X}, t a i l_{X} ⟩)$ を考えると、

$h e a d (s) = h e a d_{X} (0) = 0$
$t a i l (s) = (t a i l_{X} (0), ⟨ h e a d_{X}, t a i l_{X} ⟩) = (1, ⟨ h e a d_{X}, t a i l_{X} ⟩)$
$h e a d (t a i l (s)) = h e a d ((1, ⟨ h e a d_{X}, t a i l_{X} ⟩)) = h e a d_{X} (1) = 1$

となり、結果的に $0, 1, 2, 3, 4, \dots$ という自然数の無限列を表すことが出来てることがわかります。

Fibonacci数列

$X = i n t \times i n t, h e a d_{X} ((a, b)) = a, t a i l_{X} ((a, b)) = (b, a + b)$ とし、 $s = ((1, 1), ⟨ h e a d_{X}, t a i l_{X} ⟩)$ を考えると、

$h e a d (s) = 1$
$h e a d (t a i l (s)) = 1$
$h e a d (t a i l (t a i l (s))) = 2$
$h e a d (t a i l (t a i l (t a i l (s)))) = 3$
$h e a d (t a i l (t a i l (t a i l (t a i l (s))))) = 5$

と、Fibonacci数列を表していることがわかります。

Copattern : 余パターンマッチ

この無限リストにはどんな操作ができるでしょうか？
例えば先頭に新しく要素 $v : i n t$ を付け加える関数 $c o n s_{v} : S \to S$ が欲しかったり。
例えば全要素に関数 $f : i n t \to i n t$ を適用する関数 $m a p_{f} : S \to S$ が欲しかったり。
例えば $i \in N$ 番目の要素を取り出す関数 $i n d e x_{i} : S \to i n t$ が欲しかったりします。

ではまず、 $c o n s_{v}$ は、どうやって定義すれば良いでしょうか？とりあえず私たちはCoiterationを組めば $S$ を作れるので、試してみましょう。

$X = (0, 1, i n t, S)$ とし、

$h e a d_{X} ((0, v, s)) = v h e a d_{X} ((1, v, s)) = h e a d (s) t a i l_{X} ((0, v, s)) = (1, v, s) t a i l_{X} ((1, v, s)) = (1, v, t a i l (s))$

これから $c o n s_{v} (s) = ((0, v, s), ⟨ h e a d_{X}, t a i l_{X} ⟩)$ と定義すれば、最初は $v$ 、後からは $s$ が順番に出てくる無限リストを構成できます。

しかし、本質的なところはこれではないはずです。 やりたいことはもっと単純なわけで、簡単に表現できていいはずなのです。

原義に立ち返ると、 $⟨ h e a d, t a i l ⟩$ が定義できればよかったはずなのです。逆に言えばこれらに対する全てのマッチングを書けば十分 $S$ を定義したことになるはずです！

所謂パターンマッチは「データ構造の構成方法に関するマッチ」ですが、今回は「データ構造の分解方法に関するマッチ」なのです。これを余パターンマッチと呼び、マッチに使う「パターン」をCopattern (余パターン)と呼ぶわけなのです。

$h e a d (c o n s_{v} (s)) = v t a i l (c o n s_{v} (s)) = s$

つまりこれで十分ではないでしょうか？本来ならば関数の挙動を後から定義することなど出来ないはずですが、私達が扱っているのはDataではなくCodataなのです。これによって $c o n s_{v} (s)$ を十分定義することができるのです。

そしてこのように全ての分解方法に対して定義を示すことで関数を定義する方法をCoinduction(余帰納法)といいます。

余パターンマッチがあると様々な定義をわかりやすく書くことができます。

$h e a d (s) = 1, t a i l (s) = s$ は全ての要素が $1$ の無限リストを表します。
$h e a d (s) = 1, h e a d (t a i l (s)) = 2, t a i l (t a i l (s)) = s$ とすると、 $1, 2, 1, 2, \dots$ という無限リストを表現できます。

$h e a d (t a i l (s)) = 2$ などと書いて良いのでしょうか？**良いのです！**何故ならこれは(余)パターンマッチなのですから。
パターンで (x,(y,z)) = dat; と書くように、余パターンもネストしていいのです。

Corecursion : 余再帰

先程言った、全要素に $f$ を適用する関数 $m a p_{f}$ も余パターンマッチで記述することができます。

$h e a d (m a p_{f} (s)) = f (h e a d (s)) t a i l (m a p_{f} (s)) = m a p_{f} (t a i l (s))$

確かに $m a p_{f} (s)$ を定義していそうですが、最後の $m a p_{f} (t a i l (s))$ が気になります。これは $m a p_{f}$ が再帰していることを表します。

これは正しく停止するのでしょうか？再帰が停止しなければ定義できたとは言えません。

$c o n s_{v}$ を使って見慣れた再帰の形になおしても同じことです。

$m a p_{f} (s) = c o n s_{f (h e a d (s))} (m a p_{f} (t a i l (s)))$

再帰の停止に必要な基底段階の定義が無いのです。

しかし、まぁ、停止はせずとも定義は出来ているはずなのです。何故なら私達が扱っているのはCodataなので、再帰をしてデータ構造を作り出す過程を無限に行うことができます。実際にデータ構造の中身を見るには $t a i l$ などの関数を使わねばならず、実際 $h e a d, t a i l$ に対する挙動は明確に示されています。

このように、Codataの構造で再帰して新たなCodataを作る書き方をCorecursion(余再帰)といいます。無限に見える書き方にも関わらず、余再帰によって定まる関数は正しく定義されるのです。余再帰的定義から作り出される実際の関数のことをCofixpoint(余不動点)といいます。

なお、普通の再帰をCodata上で動かすこともできます。先程の $i n d e x_{i}$ は素直な再帰の例ですね。

$i n d e x_{0} (s) = h e a d (s) i n d e x_{i + 1} (s) = i n d e x_{i} (t a i l (s))$

ちょっと世界が広がった感じがしませんか。

余再帰のおもしろい例として、幅優先探索があります。深さ優先探索は再帰で素直に書けましたよね。幅優先探索は余再帰で素直に書けるのです。

(無限)二分木 $t$ を幅優先探索することを考えます。普通なら「キューを作って」「一番上のノードを入れて」「子ノードをキューに入れる」というのを無限に繰り返していきます。

発想の転換です。全要素が既に入ったキューをもう持っているとするのです。キューの各要素は $i n t$ ではなく、Codata $S$ です。

この全要素が既に入ったキューというのは勿論無限リストになるわけですから、CoiterationやCopatternで定義ができます。今回はCopatternを使いましょう。

$h e a d (f l a t t e n (s)) = l e f t (h e a d (s)) h e a d (t a i l (f l a t t e n (s))) = r i g h t (h e a d (s)) t a i l (t a i l (f l a t t e n (s))) = f l a t t e n (t a i l (s)) h e a d (b f s (t)) = t t a i l (b f s (t)) = f l a t t e n (b f s (t))$

とりあえず具体的にどんな $q = b f s (t)$ が構成されたかを見てみましょう。

$i n d e x_{0} (q) = h e a d (q) = t i n d e x_{1} (q) = h e a d (f l a t t e n (q)) = l e f t (h e a d (q)) = l e f t (t) i n d e x_{2} (q) = h e a d (t a i l (f l a t t e n (q))) = r i g h t (h e a d (q)) = r i g h t (t) i n d e x_{3} (q) = h e a d (t a i l (t a i l (f l a t t e n (q)))) = h e a d (f l a t t e n (f l a t t e n (q))) = l e f t (l e f t (q)) i n d e x_{4} (q) = r i g h t (l e f t (q)) i n d e x_{5} (q) = l e f t (r i g h t (q)) i n d e x_{6} (q) = r i g h t (r i g h t (q)) i n d e x_{7} (q) = l e f t (l e f t (l e f t (q)))$

なんだか確かに幅探索していそうですね。考え方としては、まず $h e a d$ に $t$ を入れておき、後続の余再帰で $t$ を取り出した時にその $l e f t$ と $r i g h t$ を返すようにする、という感じです。結果、それらがキューに入り、また余再帰で各節点の $l e f t$ と $r i g h t$ がキューに入っていき、これを無限に繰り返します。

実際にプログラムとして動かすことも勿論出来ます。

無限二分木 $t$ として次を考えます。(Stern-Brocot Tree)

一応Haskellのコードをおいておきます。

import Data.Ratio

data Tree a = Node (Tree a) a (Tree a)

cf :: Maybe Rational -> [Integer] -> Rational
cf (Just r) [] = r
cf (Just r) (x:xs) = cf (Just $ fromIntegral x + 1 / r) xs
cf Nothing  [] = 0
cf Nothing  (x:xs) = cf (Just $ fromIntegral x) xs

make :: Bool -> [Integer] -> Tree Rational
make b (x:xs) = Node (make True l) (cf Nothing $ x:xs) (make False r) where
  (l,r) = if b
    then (x+1 : xs, 2 : x-1 : xs)
    else (2 : x-1 : xs, x+1 : xs)

t :: Tree Rational
t = make False [1]

この木は各節点が $Q$ の要素を持っているので、 $F (X) = X \times Q \times X$ で表せますね。

幅優先探索は次で定義されます。

bfs :: Tree a -> [Tree a]
bfs t = t : ext (bfs t) where
  ext ((Node l _ r):qs) = l : r : ext qs

あとは適当に値を抽出するようにするとこんな感じで動きます。ちなみにbfsをちょっと工夫すると、今何段目を探索中であるかなどの情報を付け加えることもできるようになります。

まとめ

Data では

Iteration によって畳み込みを行い
Pattern で要素に分解することによって Induction で関数を定義し
Algebra 上の Fixpoint を計算することで Recursion を行えるようにするのに対し

Codata では

Coiteration によって構築を行い
Copattern で要素を記述することによって Coinduction で関数を定義し
Coalgebra 上の Cofixpoint を計算することで Corecursion を行えるような体系でした。

普通のDataは分解することが主ですが、Codataでは構築することが主となります。

そしてまぁ、こういう Data←→Codata のような対応関係を双対といいます。帰納法と余帰納法、パターンマッチと余パターンマッチ、再帰と余再帰は双対なわけです。更に言うと幅優先探索は深さ優先探索の双対なのかもしれません。

今までのwell-knownなデータ構造から双対をうまくとることで新しい世界ができることもあるわけです。
Duality everywhere、です。

たのしくないですか？

おわりに

Codataの話だけでも意味のある内容だと思っていますが、実はもっと興味深い内容を含んでいるような気がします。一番最初に書いた、「データとは操作そのものではないか？」ということです。

一般的なプログラミング言語では、操作する対象は実際にメモリなどに存在しているビット列の成すデータでしょう。でもそれは本質ではないのです。
私達が本当にやりたかった処理はビット列を操作することではなくデータそのものを解釈し操作することのはずです。

実際の表現を知らずとも操作方法さえわかっていればデータを操作することができます。これが抽象化ということです。
Representation に関しては私達は関与する必要がなく、Interface と Syntax を重視すべきなのです。

だからもうC言語はダメなんです。あまりにも実表現に近すぎるのです。抽象化ができると主張したところで他の言語には勝てません。C言語で大きなシステムを組むという技術に最早意味はないのです。

抽象化というものを学ぶときに一番良いのは数学です。ちゃんとした数学というのは「具象を抽象に持ち上げる」という流れが必ず存在します。抽象の上での操作を具象に映すことで幅広い応用を可能にするのです。プログラミングの流れと大して変わりません。

具象がわからないと抽象を理解できないという話をよく聞きますが、それはそれで良いのです。重要なのは「抽象にたどり着くこと」であり、具象の段階で止まってしまうのはもったいないかなと思います。いろんなプログラミング言語は具象の1つであり、その共通構造というものを抽象化して認識することで全てのプログラミング言語が書けるようになる。理想化した話ではありますが、間違った話では無いはずです。

抽象化というものや、ものの本質などを考える数学の分野が圏論です。正確に言えば本質を捉えることで概念を統一したり、異なる分野の関連を調べる理論です。今回のCodataの話も圏論で議論することができます。興味があれば覗いてみるといいかもしれません。

参考文献

Copatterns -- Programming Infinite Structures by Observations http://www2.tcs.ifi.lmu.de/~abel/popl13.pdf
Fixpoint Computations and Coiteration https://www.csc.depauw.edu/~bhoward/papers/KSU-CIS-95-1.pdf
なぜ Haskell ではキューが軽んじられているか？ http://d.hatena.ne.jp/kazu-yamamoto/20121107/1352259739