論文メモ The Declarative Imperative

December 5, 2020

宣言型言語Datalogを拡張した言語でネットワークプロトコルと分散システムを開発した7年間の経験から、次世代の並列分散プログラミング言語の基礎になる理論上の予想を4つ提唱した。 Datalogは、論理プログラミング言語Prologのサブセットの構文をもった言語である。予想の説明に使われるDatalogの拡張言語Dedalusは、分散システムのノードが互いの時刻を直接的に推論できない性質を、送受信するデータから離れたノードの時刻を推論する問題に帰着する。

Dedalusは、Detalogの関係の右端に時相をもつように拡張されている。以下にDedalusとDatalogのコードを例示する。左にあるDedalusは、右にあるDatalogの糖衣構文をもち、時相\(T, S\)が省略されている。最後の例にある@asyncは、頭部のタイムステップが非決定的に決まることを意味する。

toggle(1) :- state(0).           toggle(1, T) :- state(0, T).
toggle(0) :- state(1).           toggle(0, T) :- state(1, T).
state(X)@next :- toggle(X).      state(X, S) :- toggle(X, T), succ(T, S).
announce(X)@async :- toggle(X).  announce(X, S) :- toggle(X, T), choice({X,T}, {S}).

ひとつめの予想は、「プログラムが単調なDatalogで表現でき、かつそのときに限り、協調的なアクセスがなくても結果整合性を保証する。」であり、ここでの単調は、事実を追加してもプログラムに含まれる推論結果を影響しないことを意味する。例えば、集約関数、更新、削除がなく、クエリのみからなるプログラムは単調になる。

ふたつめの予想は、「ノード間のメッセージが非単調な導出に関わるとき、かつそのときの限り、因果関係を表すメッセージの順序が与えられなくてはいけない。」であり、言いかえると、メッセージが非単調な含意をもつとき、かつそのとき限り、メッセージが過去に送られるタイムパラドックスが発生する。純粋に単調なプログラムであればメッセージの順序に依存しない。

みっつめの予想は、「Dedalusのプログラムの実行に必要な最小のタイムステップは、計算量に相当する。」であり、タイムステップの推移は、ステートマシンの状態遷移に対応し、並列計算のアルゴリズムの計算複雑度をしめす。計算に必要なタイムステップの数は非単調な繰り返しの回数に対応する。

最後の予想は、「任意のDedalusのプログラムは、帰納または非同期の規則が不可欠のプログラムに書き換えることができる。」になる。帰納、非同期の規則は、上の例の3, 4番目にあたる。不可欠の意味は、帰納または非同期の規則を変更、除外するとプログラムの結果が変わることを意味する。

論文をこちらからダウンロードできます。