日本ソフトウェア科学会第 33 回大会 (2016 年度) 講演論文集

頂点主体グラフ処理の構成的アルゴリズム論に基づく
定式化
森畑 明昌
近年大規模グラフデータの並列分散処理の文脈では頂点主体グラフ処理（Vertex-centric Graph Processing）が注
目されている．頂点主体グラフ処理では，各頂点が独立に行う振る舞いを指定することでグラフ処理を記述する．これは単純だが表現力があり，並列分散計算に適している．代表的な実装としては Google の Pregel，およびそれに触発された，Giraph，GPS，PowerGraph などが挙げられる．頂点主体グラフ処理は一般のグラフアルゴリズムに比べれば単純ではあるが，依然としてその正しさの確認や効率化のための変換は困難である．本発表では，この困難に対し，リスト処理プログラムに対する変換を木構造処理へと一般化するアプローチとして知られる構成的アルゴリ
ズム論の観点から取り組む．構成的アルゴリズム論では，構造再帰を用いてプログラムを記述することで，帰納法による正しさの証明，およびそれから導かれるプログラム変換規則を活用する．しかし，直接頂点主体グラフ処理は明
示的な構造再帰ではないため，これは直接適用できない．本発表では，頂点主体グラフ処理が，無限木の生成と，その十分大きな部分木に対する構造再帰として定式化できることを指摘する．この定式化により，既存の構成的アルゴリズム論で知られた変換技法がそのまま利用できるようになる．

Vertex-centric graph processing is an emerging methodology for processing huge graphs. Vertex-centric
graph processing consists of iteration of a computation that each vertex independently does and therefore
suitable for parallel and/or distributed environments. It was proposed by Google as the Pregel framework,
and its followers include Apache’s Giraph, GPS, and PowerGraph. While vertex-centric graph processing
is relatively simple and expressive, it is still diﬃcult to develop eﬃcient and correct programs based on themethodology. In this presentation, we propose to use the theory of constructive algorithmics to reduce thediﬃculty. Although constructive algorithmics enable us to certify/improve programs by using calculationallaws (program transformations), they are not directly applicable to vertex-centric graph processing. Whilethe existing theory is formalized based on structural recursions and inductions, graph processing is usually
not structural recursion but iteration. This presentation bridges this gap by decomposing vertex-centric
graph processing into a composition of a structural recursion on suﬃciently large trees and a generationof possibly infinite trees. This decomposition enables us to use known calculational laws for manipulating
vertex-centric graph processing.

つ †1 ．そのため，アクティブなユーザに限ったとし

1 はじめにても，Facebook 上での友人関係は，数十億頂点のグ

近年，Web，ソーシャルネットワーキングサービ

ラフになる．このような巨大なグラフを一台の計算

ス，道路交通網，タンパク質の相互作用など，様々な機で処理するのは，計算時間の観点からも計算に要文脈で巨大なグラフデータが扱われるようになってするメモリの観点からも現実的ではない．そのため，いる．例えば，Facebook は 2016 年 3 月末現在，約巨大なグラフを効率的に分散・並列処理する必要があ

16.5 億人の月単位アクティブユーザー（MAU）をもる．しかし，グラフの分散・並列処理は簡単ではない．
そもそもグラフアルゴリズムは複雑になりがちであVertex-centric Parallel Processing by Constructive
Algorithmics.
Akimasa Morihata, 東 京 大 学 大 学 院 総 合 文 化 研 究 科,
Graduate School of Arts and Sciences, The University of Tokyo.

り，逐次実装すらそれほど簡単ではない場合が多い．
分散・並列実装となると，さらに同期，通信，デッド†1 http://newsroom.fb.com/company-info/ロックや無限ループの回避，障害対応などの難しさがすることで，構造の上の帰納法を活用する点にある．

加わり，とても標準的なプログラマの手におえるもの

このアプローチにより，特に木構造を操作するプログではない．

ラムに対しては，融合変換 [7, 21]，組化変換 [8]，並巨大なグラフを比較的簡単に分散・並列処理す

列化変換 [9] 等が提案されている．しかし，構成的ア

るためのアプローチとして，近年頂点主体グラフ

ルゴリズム論はグラフ処理に対してはあまり有用で処理（vertex-centric graph processing）が注目されはないとされてきた．これは，グラフアルゴリズムのている．これは Google による Pregel [11] の提案に始まり，以降 Apache Giraph†2 ，PowerGraph [6]，多くは構造再帰としては理解しがたく，それゆえ構造

GPS [20]，Pregel+ [10] 等，様々なシステムが提案・いためであった．

帰納法に基づく既存の変換手法がうまく活用できな実装されている．頂点主体グラフ処理は，各計算ス

本発表の主要な成果は，本質的には頂点主体グラフ

テップで各頂点がどのような処理を行うかによって記処理が無限木に対する構造再帰計算と同一視できる，述される．典型的には，各頂点は近傍から送られてきということを示すことである．この結果は即座に以下たメッセージを使い何らかの計算を行い，また近傍への二点を導く．まず，既存の構造再帰に基づくプログと何らかのメッセージを送信する．例えば，単一始点ラム変換規則が適用できる．これは，頂点主体グラフ

最短路の計算であれば，各頂点は各計算ステップにお処理の効率化に役立つ可能性が高い．次に，どのよういて，現時点で分かっている自分への最短距離を送信

なグラフ処理を頂点主体で記述できるかの一つの指し，また同時に，受け取った近傍への最短距離から自針となる．構造再帰が頂点主体に対応するという結果分への最短距離を（可能なら）更新する．このとき，は，例えばクエリなどは頂点主体で記述しやすそうだ

各頂点での計算は独立であるため，並列・分散環境でという直感を与える一方，処理が構造に必ずしも基づの実装に適している．

かない，特に処理の方針が動的に計算された値に依存

上述の研究は，グラフ処理を頂点主体の形式で記述するようなものは，頂点主体では素直には記述できなすれば，効率の良い並列・分散実装が得られる可能性いであろうということを示唆する．よって，本発表のが高い，ということを示している．しかし，グラフ処

結果は，頂点主体グラフ処理を系統的に構築するため

理を頂点主体の形式で記述するのはそれほど簡単での基盤として，一定の価値があると思われる．

はない．例えば，単一始点最短路に対するダイクスト

技術的には，本研究の要点は，頂点主体グラフ処

ラ法は，現時点で距離の分かっている頂点のうち最も理を適切な中間データ構造の生産と消費に分離す近いものを選ぶ，という処理を繰り返すが，この処理る点にある．このとき，中間データ構造の消費者をは大域的な情報の計算であり，頂点主体の考え方とは

構造再帰とすることで，既存の構成的アルゴリズム

相性が良くない．そのため，頂点主体の形でグラフ処論の成果を応用する．このように，適切な中間デー理を記述するための方法論や指針があることが望ま

タ構造を考えることで構成的アルゴリズム論の手法

しい．

を一般化するアプローチは既知ものである．古くは本発表では，この問題に対し，構成的アルゴリズム

hylomorphism [12] によって一般の再帰を扱う際に現論 [2, 24] の観点から取り組む．構成的アルゴリズムれている．また，動的計画法の導出 [14] や並列アル論は「変換によるプログラム構成」の一種であり，効

ゴリズムの導出 [15] でも同様の考え方が用いられて率を気にせず記述した明らかに正しいプログラムかいる．しかし，これらの研究で考えられていた中間ら，プログラム変換を繰り返すことで効率の良い実装

データ構造は単なる木構造であった．本研究では，（有を得る方法論である．構成的アルゴリズム論の特徴

限の）木構造の集合の無限列を中間データ構造とする

は，プログラムを構造再帰の組み合わせによって記述

点が技術的な特徴である．この無限列によって，グラフを表すような無限木を捉え，頂点主体グラフ計算を†2 http://giraph.apache.org/

定式化する．

• 計算ステップをさらなる繰り返しが必要なくな

2 準備るまで行う．

本稿では関数型言語 Haskell [17] の記法をプログラ

詳細はフレームワークにも依存し，必ずしも上の構造

ム記述に用いる．特に明示的に述べない限り，評価規に完全に適合するとは限らない．例えば，近傍でない

則によらず，つまり遅延評価を仮定せずとも，停止す頂点との通信を許す場合，aggregator と呼ばれる形

るようなプログラムのみを扱う．これは parametric-

での大域的な情報集約を許す場合，マスターが各頂点

ity [19, 23] を利用するためである．

とは独立に計算を行うことを許す場合，等がありう

また，圏論に関する基本的な知識，特に圏，関手，る．これらのバリエーションについては後で議論する

自然変換に関する知識を仮定する．ただし，圏論に詳ことにして，以下ではまず上述の形式を前提に定式化

しくない読者は，「対象」を「型」，「射」を「関数」，

を行う．

「関手」を「型コンストラクタ」，自然変換を「多相頂点主体グラフ処理でパラメータとなるのは，各型関数」と読み替えることで，議論の本質的な部分は頂点でどのような計算を行うかと，どのような通信理解することができるはずである．

を行うか，いつ計算を止めるか，である．いま，通信演 算 子 × は 直 積 を 構 成 し ，A × B = {(a, b) |は近傍と行うことが分かっているため，毎計算ステッa ∈ A, b ∈ B} である（圏論的には積双関手である）．

プにおいて全頂点がそれに関連づけられた値を全て関連 す る 演 算とし て ，⟨f, g⟩ x = (f x, g x) によの近傍へ送る，とすれば，通信の方法はパラメタとすり ⟨−, −⟩ を定義する．また，+ はタグ付き和（圏る必要がない．もちろん，この通信方式は多くの余剰論的には余積双関手）を与え，A + B = {inl a |なメッセージを送るであろうが，各頂点での計算の際

a ∈ A} ∪ {inr b | b ∈ B} である．関連する演算としに余剰なものを取り除くとすれば，定式化の上ではて，[f, g] (inl x) = f x および [f, g] (inr y) = g y で問題がない．また，いつ計算を止めるかについては，ある．

Emoto ら [4] の既存研究同様，計算は停止せず，計グラフ G = (V, E) は頂点集合 V と辺集合 E の組

算のトレースを表す無限列を生成するとすれば，一旦である．さらに，頂点や辺に対しては値が関連づけら考えなくても良い．こうすると，本質的なパラメータ

れているとする．以下特に断らない限り，A を頂点には各頂点でどのような計算を行うかだけとなる．

関連づけられた値の型，B を辺に関連づけられた値の型として用いる．

以上の観察を具体化する．いま，G をグラフを表す型構成子とする．以降の議論のため，この構成
子は頂点の値の型 A をパラメータとする関手であ3 頂点主体グラフ処理の定式化るとする．通信の際に交わされるメッセージは，送

まず，議論の対象とする頂点主体グラフ処理を定式

信元の頂点の値とメッセージが通過する辺の値の化する．頂点主体グラフ処理は，典型的には以下のよ

組の集合，つまり {(A, B)} 型をもつ．各頂点でのうな構造をなす．

計算は，メッセージと現在の頂点の値を用いて頂• 処理全体は計算ステップの繰り返しからなる．各点の値を更新するもの，つまり (A, {(A, B)}) → A

計算ステップでは，データの通信，および各頂点型の関数である．ここでも以降の議論のため，関手への独立な処理を行う．

M(X) = (X, {(X, B)}) を導入し，この型を MA → A• 最初の計算ステップでは，各頂点に初期値を割り当て，近傍頂点へメッセージを送るとしておく．このとき，我々が与えたいコンビネータ

ωτ の型は ωτ :: ∀α. (Mα → α) → Gα → [Gα] であ• 初回を除く各計算ステップでは，各頂点は，近り，すなわち頂点での計算をパラメータとし，グラフ傍頂点からのメッセージを受け取り，何らかの計からグラフの列（実際には無限列）をうむものであ

算をローカルに行い，近傍頂点へのメッセージをる．τ :: ∀α. Gα → GMα は通信の構造を表現するパ

送信する．

ラメータであり，各頂点の値として通信結果を挿入する関数である．τ は自然変換であり，グラフの構造には依存するものの各頂点の具体的な値には依存しないことに注意せよ．これを用いて ωτ は以下のように定義される．

ば，リストやハイパーグラフを表すものであっても構わない．

• GA のパラメタ A は頂点の値を表す必要はない．
例えば辺の値であってもよく，その場合には上のωτ f g = g : ωf (Gf (τ g))

定式化は「辺主体グラフ処理」と理解できる．

ここで，Gf は関手 G によって導かれる「関手 map」

• F は近傍との通信を表す構造である必要はない．

関数であり，各頂点に（正確には各頂点の値に）f を

例えば，aggregator がある場合には，近傍から適用する．

のメッセージに加え全頂点の値が利用できることになるため，F(X) = (X, {(X, B)}, {X}) となる

コンビネータ ωτ は以下の重要な性質を満たす．
′

定理 1 関数 h が h ◦ f = f ◦ h を満たすなら，のが自然であろう．

′

map (Gh) ◦ ωτ f = ωτ f ◦ Gh

• τ は近傍との通信を行うものである必要はない．

が成り立つ．

例えば 2 ホップ先までの通信を許すとしても良証明 Parametricity [19, 23] により簡単に示すこと

いし，全頂点間の通信を許しても良い．さらに，

2

通信に加えてグラフの構造を変形してもかまわができる．

前述の通り，多くの頂点主体グラフ処理では，最初ない．

のステップでは他のステップと異なり初期値等を各頂最後の点について少々補足を行う．τ はグラフ構造

点に割り当てる処理を行う．この点まで含めると，頂の変形を許すため，計算ステップ毎に通信の方法が変点主体グラフ処理は化するような計算，例えば高速フーリエ変換のバタフωτ f ◦ Gf0

ライ通信や，リストランキングでのポインタ飛ばし，′と定式化することができる．ここで f0 :: A → A は′′

さらには隣接頂点の併合などを行っても構わない．そ初回の計算ステップに対応し，f :: MA → A はそれのため，広い範囲の並列グラフアルゴリズムを表すこ以降の計算ステップに対応する．

とができる．しかし一方で，τ が自然変換なければな

例：単一始点最短路

らないため，τ は頂点の値に依存した通信やグラフの例としてある始点 s から他の頂点への最短路を求変形を行うことはできない．例えばプリフロー・プッ

めることを考える．初期化の計算 f0 はシュの最大流アルゴリズムでは各頂点に設定されたポ

f0 v = if v が始点 s then 0 else +∞テンシャル値に依存してフローを流す．このような通となる．繰り返し内では，既知の最短路をもとに距離信は今回の定式化では直接は表現できない．ただし，を更新するので，全ての隣接頂点にフローを流した上で，通信の受け′′

f (w, ms) = min w (min{w + b | (w , b) ∈ ms})

手が彼我のポテンシャル値を確認し，必要に応じてフとすればよい．これらを用いた

ローを破棄するような定式化をすることはできる．

sp s = ωτ f ◦ Gf0

いずれにせよ，今回採用した定式化は非常に一般的の計算は，距離が負になる閉路が無い限り，ある一定なものであり，既存の頂点主体グラフ処理のほとんど要素から後ろは各頂点が始点からの最短距離を保持を包含し，さらにそれ以外のケースをも含みうるようしたグラフとなるような無限リストを生成する． 2

なものである．それゆえ，以下ではこの定式化に対し以上の定式化は，頂点主体グラフ処理を含む一般化て議論を行う．

になっていることに注意せよ．特に，以下の議論（定理 1 を含む）では，G および F が関手であること，及4 構造再帰と頂点主体グラフ処理の同値性

び τ が自然変換であることしか用いない．このこと

4. 1 同値性の証明

は以下を意味する．

• G はグラフを表す関手である必要はない．例え我々の目的は，どのような計算であれば ωτ によって実現できるかを，構造再帰の観点から定式化することである．しかし，ωτ は構造再帰ではないので，適切な中間データ構造を与える必要がある．既存研究でfold F f f0 (Leaf a)=

f0 a

考えられてきたのは主に木構造に対する構造再帰で

fold F f f0 (Node t ts)

あるから，中間データ構造は木構造であることが望ま= f (fold F f f0 t) (map (fold F f f0 ) ts)以上の定義のもとで，以下の等式が成り立つ．これ

しい．以上の理由から，本研究では中間データ構造として，無限木によるグラフの表現を考える．
グラフを無限木だと理解するのは自然ではある．しは後に述べる定理 2 のインスタンスなので，証明はそちらに譲る．

かし，このアプローチにはいくつかの技術的な困難がmap (G(fold F f f0 )) ◦ ωτ Node ◦ G Leaf = ωτ f ◦ Gf0

ある．

この等式において，右辺は頂点主体グラフ処理であ• 無限木に対する構造再帰とは何か，はそれほどる．左辺は，頂点主体グラフ処理と構造再帰の合成と明確ではない．既存研究では主にボトムアップ構なっている．頂点主体グラフ処理では，各頂点が木構

造再帰計算が議論されてきたが，無限木に対して造を保持するグラフの無限列を生成している．このボトムアップの計算は意味をなさない．しかし，木構造はそれぞれ，その頂点を根とする無限木（の根トップダウンの計算も，計算過程が木を下るにつから有限深さまでのもの）に対応する．構造再帰は，

れ枝分かれしてしまうため，その意味は明確では

この各木構造に対してボトムアップ計算を行う．このない．

両者が一致すると言うことは，頂点主体グラフ処理と• 無限木に対する計算は停止性に注意を払う必要

は，宣言的意味としては，各頂点を根とする無限木をがある．特に，停止しない計算は system F では各頂点で独立に十分に深い頂点からボトムアップに計表現できないため，parametricity（ひいては定算することに等しい，ということを意味する．

理 1）が素直には利用できなくなる．

例：単一始点最短路（再訪）

以上の問題を解決するため，ω の場合と同様，無限単一始点最短路問題について以上の議論を適用し，木を扱うのではなく，無限木を生成する計算のトレー

fold の定義を展開すると，木構造を以下の構造再帰スを表す無限列を扱う．要するに，第 k 要素が高さ

関数 sp fold で消費する計算として，

k の木となるような無限列を考え，この列中の有限番目の要素について議論を行う．これにより，現れる木

sp s = map (Gsp fold ) ◦ ωτ Node ◦ G Leaf

構造は全て有限サイズとなるため，上記問題が回避でと定式化される．
sp fold (Leaf v)

きる．実のところ，ω はこのような定式化を行うため=に無限列を生成するものとして定義している．
以上の洞察に基づき，議論を具体化する．まず，中間データ構造となる木構造を定義する．これは，直感的には，X ∼= MX をデータタイプ宣言とみたときに定義されるデータ構造として与えられる．例えば，F(X) = (X, {(X, B)}) であれば，data TreeB = Node (TreeB , [(TreeB , B)]) | Leaf A
によって定義される TreeB が中間データ構造の型である．定義から明らかなように，Leaf A はこの定義を意味のあるものとするために必要となる．
次に，この木構造の上のボトムアップな構造再帰を考える．定義は以下となる．

if v が始点 s then 0 else +∞sp fold (Node (t, ts))=

let w = sp fold tw′ = min{sp fold t′ + b | (t′ , b) ∈ ts}

in min w w′
高さ k の木 Node (t, ts)) では，t がその頂点までの長さ k − 1 の経路を，ts が隣接頂点までの長さ k − 1 の経路とその頂点への辺を表現しており，そのそれぞれから再帰的に最短経路を計算するものとなっている．
つまり，基本的には，葉から根までの最短経路を計算していると見なすことができる．これは，グラフを無限木だとみなした場合には，最短路問題の自然な理解となっている．

2

以上の議論は M の具体的な性質に依存せず一般に成り立つ．以下，構成的アルゴリズム論でのデータタ
イプ一般構造再帰の理論に基づき概要を述べる．定式化の詳細は既存文献 [2, 24] を参照せよ．

定理 2 は，頂点主体グラフ処理が，頂点主体グラ
フ処理による無限木生成と構造再帰の 2 つによって

いま，関手 M′ を M′ (X) = M(X) + A と定義し，′

4. 2 同値性の意義′

特徴付けられることを示している．ここで注意すべM が始代数 (µM , inM′ ) を持つと仮定する．この仮定

きは，無限木生成部分は τ すなわち通信の構造のみ

は多くの場合自然に満たされる．例えば，M がコン

によって確定することである．つまり，通信の構造を′

テナ状の構造であった場合，M は始代数をもつ [1]．

変化させないのであれば，頂点主体グラフ処理の変

この始代数が中間データ構造に対応し，特に inM′ は換や最適化は構造再帰の変換や最適化に帰着される．

データコンストラクタに対応する．このとき，この始

このことは，既存の構成的アルゴリズム論で提案され代数に対する構造再帰は fold（catamorphism とも呼た定理がそのまま利用できることを示唆する．以下，′

ばれる）によって与えられる．関数 ϕ :: M A → A に融合変換，組化変換，貪欲アルゴリズムの導出を例によって特徴付けられる fold は以下の等式によって特その効果を説明する．
融合変換

定される．

fold M′ ϕ ◦ inM′ = ϕ ◦ M′ (fold M′ ϕ)

融合変換とは，二つの関数の合成を一つにまとめる

このとき，以下の定理が成り立つ．

ことで，中間的な計算結果を取り除き，効率を改善す

定理 2 以下の等式が成り立つ．
map (G(fold M′ [ϕ, ϕ0 ])) ◦ ωτ (inM′ ◦ inl) ◦ G(inM′ ◦ inr)

るプログラム変換である．構造再帰の融合変換に関し= ωτ ϕ ◦ Gϕ0
証明 定理 1 を用いる．以下の通り，定理の前提条件

定理 3 ([12]) f ◦ ϕ = ϕ′ ◦ Ff ならば以下の等式が成は満たされている．
fold M′ [ϕ, ϕ0 ] ◦ inM′ ◦ inl

f ◦ fold F ϕ = fold F ϕ′[ϕ, ϕ0 ] ◦ M′ (fold M′ [ϕ, ϕ0 ]) ◦ inl

れる．
系 4 f ◦ ϕ = ϕ′ ◦ Mf ならば以下の等式が成り立つ．

{ M′ の定義 }map (Gf ) ◦ ωτ ϕ ◦ Gϕ0 = ωτ ϕ′ ◦ G(f ◦ ϕ0 )[ϕ, ϕ0 ] ◦ inl ◦ M(fold M′ [ϕ, ϕ0 ])証明 まず以下を示す．
f ◦ fold M′ [ϕ, ϕ0 ] = fold M′ [ϕ′ , f ◦ ϕ0 ]{ [−, −] の定義 }=ϕ ◦ M(fold M′ [ϕ, ϕ0 ])これをふまえた以下の式変形が定理を証明する．
LHS

⇐
⇔

{ 定理 1 }ωτ ϕ ◦ G(fold M′ [ϕ, ϕ0 ]) ◦ G(inM′ ◦ inr)
{ G は関手 }f ◦ [ϕ, ϕ0 ] ◦ inr = [ϕ′ , f ◦ ϕ0 ] ◦ M′ f ◦ inr⇔⇔′{ M の定義 }{ 前提条件 }True
これをふまえた以下の式変形により証明できる．

{ [−, −] の定義 }ωτ ϕ ◦ Gϕ0{ M′ および [−, −] の定義 }f ◦ ϕ = ϕ′ ◦ Mf ∧ f ◦ ϕ0 = f ◦ ϕ0

{ fold の定義 }ωτ ϕ ◦ G([ϕ, ϕ0 ] ◦ inr)=

{ 入力による場合分け }f ◦ [ϕ, ϕ0 ] ◦ inl = [ϕ′ , f ◦ ϕ0 ] ◦ M′ f ◦ inl ∧ωτ ϕ ◦ G([ϕ, ϕ0 ] ◦ M′ (fold M′ [ϕ, ϕ0 ]) ◦ inr)={ 定理 3 }f ◦ [ϕ, ϕ0 ] = [ϕ′ , f ◦ ϕ0 ] ◦ M′ fωτ ϕ ◦ G(fold M′ [ϕ, ϕ0 ] ◦ inM′ ◦ inr)=2

これと定理 2 を組み合わせることで以下の系が得ら

=

=

り立つ．

{ fold の定義 }==ては以下が知られている．

2

⟨ϕ̃1 ◦ M′ fst, ϕ̃2 ◦ M′ snd ⟩ = [ϕ, ⟨ϕ1,0 , ϕ2,0 ⟩]LHS={ 定理 2 }⇔ωτ (inM′ ◦ inl) ◦ G(inM′ ◦ inr)=

= [ϕ, ⟨ϕ1,0 , ϕ2,0 ⟩] ◦ inl′{ map および G の性質 }ωτ (in=◦ inl) ◦ G(inM′

= [ϕ, ⟨ϕ1,0 , ϕ2,0 ⟩] ◦ inr◦ inr)⇔{ 上記 }{ ⟨f ◦ g, h ◦ g⟩ = ⟨f, h⟩ ◦ g ，M′ の定義 }⟨ϕ̃1 ◦ inl ◦ Mfst, ϕ̃2 ◦ inl ◦ Msnd ⟩′map (G(fold M′ [ϕ , f ◦ ϕ0 ])) ◦= [ϕ, ⟨ϕ1,0 , ϕ2,0 ⟩] ◦ inlωτ (inM′ ◦ inl) ◦ G(inM′ ◦ inr)=∧′⟨ϕ̃1 ◦ M fst, ϕ̃2 ◦ M snd ⟩ ◦ inr

map (G(f ◦ fold M′ [ϕ, ϕ0 ])) ◦M′{ 入力による場合分け }⟨ϕ̃1 ◦ M′ fst, ϕ̃2 ◦ M′ snd ⟩ ◦ inl

map (Gf ) ◦ map (G(fold M′ [ϕ, ϕ0 ])) ◦⟨ϕ̃1 ◦ inr, ϕ̃2 ◦ inr⟩ = [ϕ, ⟨ϕ1,0 , ϕ2,0 ⟩] ◦ inr{ 定理 2 }⇔2RHS
系 4 は定理 1 からより直接的に証明することもできるが，上記の証明は，我々のアプローチの意義を明確に示している．M と M′ の間のわずかのギャップを埋めることさえできれば，頂点主体グラフ処理の変換は{ [−, −] の定義 }⟨ϕ1 ◦ Mfst, ϕ2 ◦ Msnd ⟩ = ϕ∧⟨ϕ1,0 , ϕ2,0 ⟩ = ⟨ϕ1,0 , ϕ2,0 ⟩次に以下を示す．
⟨Gf, Gg⟩ = ⟨Gfst, Gsnd ⟩ ◦ G⟨f, g⟩⇔{ ⟨f ◦ g, h ◦ g⟩ = ⟨f, h⟩ ◦ g }⟨Gf, Gg⟩ = ⟨Gfst ◦ G⟨f, g⟩, Gsnd ◦ G⟨f, g⟩⟩

構造再帰の変換からほぼ自明に導かれる．

⇔

組化変換

る，ループ融合のような変換である．構造再帰の組
化変換に関して，ここでは最もシンプルな以下を考える．
定理 5 ([8]) ϕ = ⟨ϕ1 ◦ Ffst, ϕ2 ◦ Fsnd ⟩ とすると以⇔={ 定理 2 および ⟨f ◦ g, h ◦ g⟩ = ⟨f, h⟩ ◦ g }zip ◦ ⟨map G(fold M′ ϕ̃1 ), map G(fold M′ ϕ̃2 )⟩ ◦2ωτ (inM′ ◦ inl) ◦ G(inM′ ◦ inr)=

れる．

{ zip と map の性質 }map ⟨G(fold M′ ϕ̃1 ), G(fold M′ ϕ̃2 )⟩ ◦系 6 ϕ = ⟨ϕ1 ◦ Mfst, ϕ2 ◦ Msnd ⟩ とすると以下の等式が成り立つ．ここで zip :: ∀α, β. (Gα, Gβ) →{ ⟨−, −⟩ の性質 }⟨Gf, Gg⟩ = ⟨Gf, Gg⟩
以上をふまえた以下の式変形により証明できる．
LHS

下の等式が成り立つ．

これと定理 2 を組み合わせることで以下の系が得ら{ G は関手 }⟨Gf, Gg⟩ = ⟨G(fst ◦ ⟨f, g⟩), G(snd ◦ ⟨f, g⟩)⟩組化変換とは，二つの独立な処理を一つにまとめ⟨fold F ϕ1 , fold F ϕ2 ⟩ = fold F ϕ∧ωτ (inM′ ◦ inl) ◦ G(inM′ ◦ inr)=

{ 上記 }G(α, β) は 2 つの同じ形状のグラフの対応する頂点をmap ⟨Gfst, Gsnd ⟩ ◦ G⟨fold M′ ϕ̃1 , fold M′ ϕ̃2 ⟩ ◦併合する関数である．
zip ◦ ⟨ωτ ϕ1 ◦ Gϕ1,0 , ωτ ϕ2 ◦ Gϕ2,0 ⟩ωτ (inM′ ◦ inl) ◦ G(inM′ ◦ inr)

= map ⟨Gfst, Gsnd ⟩ ◦ ωτ ϕ ◦ G⟨ϕ1,0 , ϕ2,0 ⟩証明 以下，ϕ̃i = [ϕi , ϕi,0 ] (i ∈ {1, 2}) とする．まず={ 定理 5 および上記 }map ⟨Gfst, Gsnd ⟩ ◦ Gfold M′ [ϕ, ⟨ϕ1,0 , ϕ2,0 ⟩] ◦
ωτ (inM′ ◦ inl) ◦ G(inM′ ◦ inr)

以下を示す．

={ 定理 2 }2
map ⟨Gfst, Gsnd ⟩ ◦ ωτ ϕ ◦ G⟨ϕ1,0 , ϕ2,0 ⟩ここでも，頂点主体グラフ処理の組化が構造再帰の組化に帰着されている．証明の方針はほぼ融合変換の場合と同じである．

貪欲アルゴリズムの導出した．

貪欲アルゴリズムの導出に関しては以下の定理が知られている．min⪯ :: {A} → A を集合から順序 ⪯の意味で最小のものを満たす関数とし，σ は一点集合

本研究の以前にも，グラフ処理を構造再帰を用いて記述しようとする試みは存在する．

Erwig [5] は active pattern という抽象データ構造を構成する関数とする．

を代数的データ構造のようにパターンマッチする手

定理 7 (貪欲定理 [2]) 関数 ϕ :: F{A} → {A} が ⪯法を提案し，これを用いることで，幅優先探索などの上で単調ならば，以下の等式が成り立つ．

様々なグラフ処理が構造再帰のように扱えることを示2した．また，篠埜ら [25] はこれを拡張し，中間デー

左辺式では fold F ϕ によって多くの要素が列挙される

タ構造の生成と消費（hylomorphism）を考えること可能性があるが，左辺では再帰の度に min⪯ が適用

で，ダイクストラ法のようなアルゴリズムも記述でされるため，一点集合のみが得られる．これを用いる

きることを示している．Buneman ら [3] はグラフ構と以下の系が得られる．

造データベースに対する問い合わせ言語 UnQL を提min⪯ ◦ fold F ϕ = fold F (σ ◦ min⪯ ◦ ϕ)

系 8 関数 ϕ :: M{A} → {A} が ⪯ の上で単調なら案した．この言語はグラフを無限木だと見たときのば，以下の等式が成り立つ．ただし G ⪯ は全ての頂構造再帰として理解することができる．Hamana [16]点が ⪯ で小さいものを小さいとする半順序であり，と Oliveira ら [18] はいずれも，グラフ（特にグラフ

minG⪯ の結果は常に定義されるものとする．また，のサイクリックな構造）を代数的データ構造に近い形

G∈ :: ∀α. G{α} → {Gα} は各頂点に格納された集合

で形式的に扱う方法を模索した．Hamana はグラフの値を組み合わせてグラフの集合を構築する計算でを木構造に近いものと見なし，バックエッジを木構造ある．
map (minG⪯ ◦ G∈) ◦ ωτ ϕ ◦ Gϕ0

をトラバースするポインタとして扱った．Oliveira ら
はパラメトリック高階抽象構文の技法がバックエッジ= map G∈ ◦ ωτ (σ ◦ min⪯ ◦ ϕ) ◦ G(min⪯ ◦ ϕ0 )2
証明 (証明の概略) 補題としてminG⪯ ◦ G∈ = G∈ ◦ G min⪯が必要となる．これは relational calculus [2, 13] を用いるとそれほど難しくなく証明できるが，本稿の範囲を超えるので割愛する．さらに補題として
min⪯ ◦ fold M′ [ϕ, ϕ0 ]の取り扱いに有効であることを指摘した．いずれも，それらの定式化のもとで，構造再帰が適切に定められることを示している．
それぞれの研究で定義している構造再帰はその詳細が異なる．例えば，Erwig の手法による構造再帰は各頂点を各々1 度ずつ処理するが，Buneman らのもの

= fold M′ [σ ◦ min⪯ ◦ ϕ, min⪯ ◦ ϕ0 ]が必要だが，これは定理 7 および入力の場合分けによや Oliveira らのものはサイクリックな部分を何度も周り簡単に示すことができる．以下の証明は定理 3 のな「構造」だと見なすかによって構造再帰の定義が変2わるためである．本研究に最も近いのは Buneman ら場合と同様である．

回する可能性がある．これは結局，グラフをどのようのものであるが，彼らの UnQL はグラフデータベー

5 関連研究スへの問い合わせに特化したものであり，汎用のもの

本研究は Emoto ら [4] の研究の影響を強く受けてではない．UnQL の大部分は頂点主体グラフ処理といる．Emoto らは頂点主体計算を関数プログラミン

して実装できることが分かっている [22] ため，本研グの観点から分析し，それに基づき領域限定言語を制究は彼らのものを一般化するものだと言える．

作した．彼らの領域限定言語は本研究での ωτ によるより本質的な違いは，既存研究がグラフに対する

頂点主体グラフ処理の定式化とほぼ対応する．本研究

構造再帰を定義し，それを用いてグラフ処理を記述

ではこれに ωτ というシンプルな定式化を与え，さらすることを考えたのに対し，本研究では，広く使われにこれが構造再帰によって特徴付けられることを示ている手法である頂点主体グラフ処理から始め，それが構造再帰によって特徴付けられることを示した

点にある．前述の通りグラフに対する構造再帰については様々な方針があるため，どのような定義が「適切」なのかという議論がついて回るが，本研究はそのような議論に対して頂点主体グラフ処理の見地から一石を投じた形になっている．とはいえ，これら関連研究との関係の精査は今後の課題である．

6 おわりに本稿では，頂点主体グラフ処理が ωτ というコンビ
ネータによって捉えることができることを示し，これが構造再帰による処理と同一視できること，さらにそれによって既存のプログラム変換規則を応用できることを示した．これらは，頂点主体グラフ処理をを系統的に構成するための基礎理論の一部として有用であろうと思われる．
現時点での成果はまだ予備的なものであり，さらなる発展が求められる．特に，動的計画法の導出 [2, 13, 14] を扱えるかどうかは興味深いところである．また，実際の頂点主体グラフ処理に応用してみるケーススタディも必要であろう．さらに，本研究で導入したコンビネータである ωτ の応用例を頂点主体
グラフ処理以外でも考えることができればより興味深い．
謝辞 本研究の初期の成果についての，Parallelism

Oblivious Parallel Programming ミーティングのメ
ンバーとの議論に感謝する．本研究は日本学術振興会
学術研究助成基金助成金 (若手研究 (B) 15K15965)の助成を受けている．

参 考 文 献[ 1 ] Abbott, M., Altenkirch, T., and Ghani, N.: Containers: Constructing strictly positive types, Theor.
Comput. Sci., Vol. 342, No. 1 (2005), pp. 3–27.
[ 2 ] Bird, R. S. and de Moor, O.: Algebra of Programming, Prentice Hall, 1997.
[ 3 ] Buneman, P., Fernandez, M. F., and Suciu,
D.: UnQL: A Query Language and Algebra for
Semistructured Data Based on Structural Recursion. VLDB J. Vol. 9, No. 1 (2000), pp. 76-110.
[ 4 ] Emoto, K., Matsuzaki, K., Hu, Z., Morihata, A.,
and Iwasaki, H.: Think Like a Vertex, Behave Likea Function! A Functional DSL for Vertex-Centric
Big Graph Processing, 2016 ACM SIGPLAN International Conference on Functional Programming,

ICFP 2016, Nara, Japan, September 19-20, 2016,
Sumii, E.(ed.), ACM, 2016. To appear.
[ 5 ] Erwig M., Functional Programming with
Graphs, Proceedings of the 2nd ACM SIGPLAN
International Conference on Functional Programming, ICFP’97, Amsterdam, The Netherlands,
June 9-11, 1997, ACM, 1997. pp. 52–65.
[ 6 ] Gonzalez, J. E., Low, Y., Gu, H., Bickson,D., and Guestrin, C.: PowerGraph: Distributed
Graph-Parallel Computation on Natural Graphs,
10th USENIX Symposium on Operating Systems
Design and Implementation, OSDI 2012, Hollywood, CA, USA, October 8-10, 2012, Thekkath, C.
and Vahdat, A.(eds.), USENIX Association, 2012,
pp. 17–30.
[ 7 ] Hu, Z., Iwasaki, H., and Takeichi, M.: Deriving
Structural Hylomorphisms From Recursive Definitions, Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming(ICFP ’96), Philadelphia, Pennsylvania, May 2426, 1996., Harper, R. and Wexelblat, R. L.(eds.),
ACM, 1996, pp. 73–82.
[ 8 ] Hu, Z., Iwasaki, H., Takeichi, M., and Takano,
A.: Tupling Calculation Eliminates Multiple Data
Traversals, Proceedings of the 2nd ACM SIGPLAN
International Conference on Functional Programming, ICFP’97, Amsterdam, The Netherlands,
June 9-11, 1997, ACM, 1997, pp. 164–175.
[ 9 ] Hu, Z., Takeichi, M., and Chin, W.-N.: Parallelization in Calculational Forms, POPL ’98:
Proceedings of the 25th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, January 19-21, 1998, San Diego, CA, USA,ACM Press, 1998, pp. 316–328.
[10] Lu, Y., Cheng, J., Yan, D., and Wu, H.: LargeScale Distributed Graph Computing Systems: An
Experimental Evaluation, Proceedings of the VLDB
Endowment, Vol. 8, No. 3 (2014), pp. 281–292.
[11] Malewicz, G., Austern, M. H., Bik, A. J. C.,
Dehnert, J. C., Horn, I., Leiser, N., and Czajkowski,
G.: Pregel: a system for large-scale graph processing, Proceedings of the ACM SIGMOD International Conference on Management of Data, SIGMOD 2010, Indianapolis, Indiana, USA, June 610, 2010, Elmagarmid, A. K. and Agrawal, D.(eds.),
ACM, 2010, pp. 135–146.
[12] Meijer, E., Fokkinga, M. M., and Paterson, R.:
Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire., Functional Programming
Languages and Computer Architecture, 5th ACM
Conference, Cambridge, MA, USA, August 26-30,
1991, Proceedings, Hughes, J.(ed.), Lecture Notes
in Computer Science, Vol. 523, Springer, 1991,
pp. 124–144.
[13] Morihata, A.: Calculational Approach to Automatic Algorithm Construction, PhD Thesis, Department of Mathematical Informatics, Universityof Tokyo, 2009.

[14] Morihata, A.: A Short Cut to Optimal Sequences, New Generation Comput., Vol. 29, No. 1(2011), pp. 31–59.
[15] Morihata, A. and Matsuzaki, K.: Balanced
trees inhabiting functional parallel programming,
Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming,
ICFP 2011, Tokyo, Japan, September 19-21, 2011,
Chakravarty, M. M. T., Hu, Z., and Danvy, O.(eds.),
ACM, 2011, pp. 117–128.
[16] Hamana, M.: Initial Algebra Semantics for
Cyclic Sharing Tree Structures, Logical Methods in
Computer Science, Vol. 6, No. 3, 2010.
[17] Peyton Jones, S.(ed.): Haskell 98 Language andLibraries: The Revised Report, Cambridge University Press, Cambridge, UK, 2003.
[18] Oliveira, B. C. d. S., and Cook, W. R.: Functional programming with structured graphs. ACM
SIGPLAN International Conference on Functional
Programming, ICFP’12, Copenhagen, Denmark,September 9-15, 2012, ACM, 2012, pp. 77–88.
[19] Reynolds, J. C.: Types, Abstraction andParametric Polymorphism, Information Processing,Vol. 83 (1983), pp. 513–523.
[20] Salihoglu, S. and Widom, J.: GPS: a graph processing system, Conference on Scientific and Sta-tistical Database Management, SSDBM ’13, Baltimore, MD, USA, July 29 - 31, 2013, Szalay, A., Budavari, T., Balazinska, M., Meliou, A., and Sacan,A.(eds.), ACM, 2013, pp. 22:1–22:12.
[21] Takano, A. and Meijer, E.: Shortcut Deforestation in Calculational Form, Conference Recordof FPCA’95 SIGPLAN-SIGARCH-WG2.8 Conference on Functional Programming Languages andComputer Architecture. La Jolla, CA, USA, 25-28
June 1995, ACM, 1995, pp. 306–313.
[22] Tung, L.-D.: Pregel meets UnCAL: A systematic framework for transforming big graphs, 31stIEEE International Conference on Data Engineering Workshops, ICDE Workshops 2015, Seoul,
South Korea, April 13-17, 2015, 2015, pp. 250–254.
[23] Wadler, P.: Theorems for Free!, FPCA’89 Conference on Functional Programming Languages andComputer Architecture. Imperial College, London,
England, 11-13 September 1989, ACM, New York,
1989, pp. 347–359.
[24] 岩崎 英哉: 構成的アルゴリズム論, コンピュータソ
フトウェア, Vol. 15, No. 6, (1998), pp. 547–560.
[25] 篠埜 功, 胡 振江, 武市 正人: グラフの探索の再帰的定義と変換, コンピュータソフトウェア, Vol. 17, No. 3,(2000), pp. 2–19.