論文振り返り

僕の論文が小馬鹿にされているのを聞いて、むっとして反論を考えていたのだけど、冷静になって考えてみると、そうした反論は論文中に書かれているべきであり、また実際にいろいろと反省すべき点もあので、せっかくの機会に過去の論文を振り返り、反省を次の論文に生かしたいと思って書いています。

"An Intersection Type System for Deterministic Pushdown Automata" (IFIP TCS 2012)

Minamide & Tozawa (APLAS 2006) の CFL-RHL (= Regular Hedge grammar の生成する Language) 包含判定アルゴリズムが、自然に CFL-SPDL (= Superdeterministic Push-Down オートマトンの受理する Language) 包含判定に拡張できるということを示した論文。元々は高階に拡張することを念頭に置いていたため型システムの言葉で書いてあり、それがタイトルにも入っているが、交差型（Intersection type）は本質ではなく、査読者にも不評だった。Minamide & Tozawa 式の記法のような、オートマトンの専門家に読みやすい記法にするべきだったと、今は思う。（当時は型の記法の方が "万人にとって" 分かり易いはずだという勘違いをしていた。恥ずかしい限りである。）

肝心の貢献については、価値ある新しい命題の証明には至らなかったため、「オリジナルの証明よりも簡潔である」という、非常に主観的かつ乱暴な主張をすることになってしまった。この点については、批判は甘んじて受けねばなるまい。実際のところ、プッシュダウンオートマトンの専門家の視点から見たときに、オリジナル（Greibach & Friedman, J.ACM 1980）の証明がどの程度の複雑なものであるかは、当時も今も、とんとわからない。SPDAの定義ひとつを取っても、本論文における定義は Greibach & Friedman の定義よりも良いと思う（例えば、SPDL が RHL の拡張であることが自然に表現されている）が、オートマトンの専門家には Greibach & Friedman から本論文における定義と同じ直観を得られるのかもしれない。（定義を思いつきさえすれば、２つが同じ言語を定めることは自明なのだが。。。）[追記 3 Oct 2014：少し考えた結果、論文中の定義と Greibach & Friedman の定義の間に違いなんて、大してないという結論に至った。]そういった忌憚のない意見は、南出先生（筑波大学）を訪問したときに、研究グループの誰かに伺えばよかったのだが、つい忘れてしまっていた。なお、忌憚のない意見は現在も募集中です。メールでもくれるとありがたいです。

Minamide & Tozawa のアルゴリズムが SPDA に拡張できるという結果は、自明ではないとは思う。この点を強調した論文の流れにした方が良かったのかもしれない。例えば、Minamide & Tozawa のアルゴリズムの紹介、その SPDA への拡張、実装・評価、というような。応用を思いつかないので、評価のサンプルインプットに困ってしまうが。実際の論文は「Minamide & Tozawa よりもすげーぜ！」といった体であり、大変に残念なできである。

ひとつくらい、非自明な帰結について触れておこう。CFL-SDPL包含判定は 2-EXPTIME complete であることが知れらているが、２段の指数関数のうちひとつは、CFL reachability problem の（最短の） witness の長さが exponential であるという事実から従う。より具体的には、次の通りである：

• PDA A と SPDA B が与えられたとする
• SPDA B のスタックを忘却した有限状態オートマトンを B' とする（B' は B の over-approximation になるように取る）
• B' の状態の組（＝ B の状態の組）ごとに、L(A)-reachability を解き、witness を構成する。こうして構成された witness 達の長さの最大値を k とする
• このとき、L(A) ⊆ L(B) は、k に対して指数時間で解ける

余談だが、Colin Sterling が「本論文の技術に inspire された real-time deterministic DPDA の言語同値性判定」のトークをしていて、大変に驚いたし、嬉しかった。この論文で提案した技術も、まったくの無価値というわけではなかったということだろう。それだけが救いである。