ET Seminar

ET seminar's slide
まず講師をされた alohakun さんに敬意を表したいと思います。自分の研究について7時間総攻撃というのは生半可な事ではないから。ETの全体像から例を踏まえて説明して下さったおかげで、魔術的だった部分が明くなりました。それはそれとしてETの理論が詳らかになったかと言うと、幾つか疑問が残ったのでメモしておきます。

Formalization of the Equivalent Transformation Computation Model Kiyoshi Akama and Ekawit Nantajeewarawat
この論文では、SLD導出で無限時間後に証明可能な回文問題を、ETが有限時間でどう解決するかという例が示されています。まず引き合いに出されているPrologの例ですが、

palindrome(X) :- reverse(X, X).
?- palindrome([1|X]), palindrome([2|X]).
X = [] ;
.. % Infinite Loop

という風に無限ループに陥ります。これがETでは、次のルールを適当なタイミングで適用する事により解決を図っています。

rv(*x, *y), rv(*x, *z) => {=(*y, *z)}, rv(*x, *y).

Prologユーザの目線で考えるとこれは明かにメタな言及で、実現するにはメタインタプリタのレイヤでアトムの操作が必要になりますから、メタ操作を意識せず実現というのは一つの到達点なのだと思います。ただPrologユーザはこれを弱点というより利点だと考えている場合が割りとあります(但し、高階型の支援が無い事はPrologの明かな欠点)。

さて気になるのはこのETルールの、仕様からの生成可能性や、仕様に対する正当性の証明です。Prologでも勝手にルールを与えて(変えて)構わないなら、先の回文問題の無限ループは回避出来ます。特に、最近このルールが自動導出出来るようになったという事で、その成果は大変興味深いので論文が待ち遠しいのですが、その自動導出プログラムはTuring Completeなのか？また入力に対して計算量のオーダーはどの程度なのか？ルールが持つプライオリティはどのように決定可能か？この辺りにアドバンテージがあると、ETがPrologの理論的限界の先にあるという気分も分かるのですが、現時点ではPrologのランタイムを分断して議論しているという印象を持ってしまいます(あくまで個人的に)。

というのも、特定の仕様Dに対して正当なETルールがどれほど存在するのかは、決定が非常に難しいと思うからです。もし数が無限個か、或いは決定出来ない場合、ルール集合に半順序関係を入れるなどしなければ、ルール導出プログラムや仕様に対する正当性の証明の停止性を決定出来ないと思うのです。そうなると、ここで"ET処理系に対するHow"が入ってくるのではないでしょうか？

以上の疑問が残るものの、仕様空間とプログラム空間を分けて議論する事は圏論で説明したら綺麗になりそうだし、多重集合の書き換え系はそれ自体が便利なのでどんどん開発を進めて欲しいし、仕様の如何によってはリッチ(古典的)な否定が定義出来るのかもしれなくて便利な気がするし、といった感じでAfter Workに期待です。