面白CS論文紹介 1日目ranha |
本記事は、「今年読んだ面白CS論文紹介カレンダー」 の1日目の記事です。
ぼくが今年読んだ論文で面白かったものを勝手に紹介し散らせば、 皆さんの興味をひくものが少なからずある筈だ。 とゆーような狙いがあるわけです。
まぁ面白い論文の紹介が面白いとは限らないですし、 どうなるか知ったものではありませんが。
しかしもう一つ狙いがあります。 それは、面白CS論文紹介カレンダーはまだまだ参加者を募集していますので、 この低レベルエントリを読んで貰って、 気軽に参加出来る事を知ってもらうのも狙いです。
以下紹介に入っていくわけなのですが、 よくよく考えると、 今年は研究(というか実験)の一環で 結構な数の論文をちゃんと読んだりしたので、 面白かったものを全部列挙すると結構な量になってしまいます…。 そこで、とりあえず今回はパーザで統一して取り上げてみようかな〜という。
しかも単にパーザという話ではなくて、 停止して結果を返すパーザ(無限ループしない!!)を強く意識した感じになってしまいました。
title : TRX: A FORMALLY VERIFIED PARSER INTERPRETER authors : Adam Koprowski , Henri Binsztok
タイトルを中心に、概説を述べるならば
(Parsing Expression Grammarsは皆様ご存知でしょうか?)
しかしPEGを解釈するといっても、任意の文法を許可するわけではありません。 具体的な話になりますが、次の文法を考えてください。
expr ::= expr [+] factor / factor (この例は実際 論文にあるものです)
こいつを元に、単純に再帰下降的にパージング (この論文でのPEGのsemanticsは本質的に再帰下降的です) すると明らかに無限ループです。いわゆる「左再帰」になっているというやつですが。
さて、ではどんなPEGを許そうというのでしょうか? そもそも、どんな文法だと嬉しいのでしょうか。 Coqで実装しようと考えると、
こんなところでしょうか。
この2つの条件を満たすようなある種の文法は、 Bryan Fordによって既に提案1されています。 それはwell formed grammarと呼ばれるものです。 このwell formed grammar、文字通りなのですが 素直に帰納法が使えるという意味で構造としてwellなもので、 well formed grammarであれば、左再帰の形になっていないことは証明出来ます。
実際にTRXは、まず与えられた文法がwell formed grammarになっているかどうかを検査して、 もしwell formed grammarならパージングを実行する、という形に成っています。
とはいえ、well formed grammarであるかどうかの検査はそこまで自明なものではありません。 それから、TRXはもう一つの目標に実用的であることを掲げていて、単純なPEGsではなしに、 セマンティックアクション付きのXPEGsというものを定義、形式化しています。
実装が公開されているかどうかは分かりませんが、 これを読めば十分に同じアプローチで実装可能という程度には詳しく説明が書かれていますので、 PEG大好きな皆さんは是非読んでみてください。
どう考えても面白い!! では当然ダメとしてうーんなんでしょう…。
well formed grammarという非常に良い形をした文法を考えれば、 まぁ当然のことながら上手く行くよねという極めてシンプルな考えに基づいている所がキレイかなーと思います。
あとは他の人にとって面白いかどうか分かりませんが、 PEGの本当に基本的なところが頭から最後まで通して読むだけで分かった感じになれる、 とかはお得感結構あるし、何より自分で実装出来るようになるしで面白いよなーみたいなのは。
いわばなんとなくの実装じゃなくて、実際正しい実装をすることが出来るようになるのですよ!?
title : Structurally Recursive Descent Parsing authors : Nils Anders Danielsson , Ulf Norell
スゴイ級に面白い
雰囲気的には、上述のTRXに似ています。つまり、停止するパーザだけを作れるようにしたい。 しかし、この論文ではPEGではなく、parser combinatorを扱うのです。まずここが異なる部分。 (ちなみにparser combinatorについて知らない方は、 是非この機会にMonadic parsing in Haskellを読んでみてください) それから、Agda2で実装しています。
とはいえ、ここでも単純に再帰下降的にパージングしようとしますので、左再帰的な文法は残念ながら扱う事が出来ません。 なので、先のwell formed grammarのように左再帰が無い文法であるかを検査し、それに対する解釈を定義する事になるのですが、 このどちらのアプローチも非常に面白い方法を取っています。
まず左再帰を含むかどうかの検査について。 文法というものは本質的に再帰的であるので、何も変な事をせずにcoinductiveとしてシンプルに定義してしまっています。
(coinductiveといえば、無限ぽい項が作れてしまうという点でinductiveと異なります。 典型的な例ですが、
Inductive List where nil :: List cons :: Int -> List -> List
こう定義したListの型が付くのは、長さが有限の項に限りますが、
CoInductive Stream where nil :: Stream cons :: Int -> List -> List cofixpoint zeros = cons 0 zeros
こうした場合、zerosの様な無限サイズの項も許す(文字通りストリーム!)ようになります)
とはいえ、coinductiveに定義されたパーザは左再帰を許す、すなわち
xseq = xseq >>= (\xs -> char 'x' >>= (\x -> return (xs ++ [x])))
<|> (char 'x' >>= return [x])
このようなパーザが定義出来るようになります。 問題はこのようなパーザを用いて再帰下降的なパージングが(corecursiveに)行われても停止しないという事です。
停止しないパーザだけを作りたいという要求と衝突してしまうわけですが、 論文ではこのようなパーザが構成されないようにしています。
構成されないようにするというのが面白いところで、 これは構成した後に検査するのとは少し違うのですが、 まぁ兎に角その為にIndexというinductiveな型を coinductiveに定義したパーザ型のパラメタとして用います。
codata Parser (Tok : Set) : Index → Set → Set1 where ...
こんな感じ。
このinductiveな型は、左再帰的なパーザの構成を防ぐだけではなくて、 こいつを拠り所にして、必ず停止する解釈を定義してしまうのです。
一粒で二つ美味しい！！
何がってそれはもうこれ全部面白いですよ!! 今書いてても鳥肌が立つぐらいには面白いと思っています。
まずAgda2の使い倒しっぷりが半端ない。尋常でなく使うのが上手い。 well formed grammarになっているかどうか検査するのに相当する部分も、 Agda2自身の型検査器を利用して片付けてしまっています。
これはもうなんていうか、パーザの実装がどうこうという話ではなくて、 Agda2の上手い使い方を垣間みる為だけに読んでも十分価値のあるものだと思います。
ただ、論文の後半の方を読んでもらうと分かるのですが、 実装が比較的楽に片付く一方で、 使う時には色々と問題が生じます。
この辺のトレードオフでさえ面白く感じてしまうのですがなんというか病気っぽいですね…。 実装による千差万別さみたいなものが好きな人は、上述のTRXと合わせて読むと かなり楽しめるのではないかと思います。
title : Derivatives of Regular Expressions author : Janusz A. Brzozowski
正則表現界隈では非常に有名らしいBrzozowskiのDerivatives of Regular Expressionsです。 恥ずかしながら、ぼくは今年はじめて(とある理由から)読むことになったのですが、非常に面白かったです。
それに、色々関連するお話があって、特に(と言いますか、例に依ってと言いますか) Conor McBrideによる Clowns to the Left of me, Jokers to the Right : Dissecting Data Structures2 がまた大変なことになっていて…。これは置いておきます。
正則表現Lにおけるderivate(微分),Dc(L)を、 Lが受理する文字列のうちで、先頭が文字cからはじまるものを headとtailで分けてそのtailの部分を全て集めたもの〜という感じで定義します。
で、これのどの辺が微分になるんですかという話は、 ぼくでは上手い事説明出来そうに無いので入手して読んでもらえれば 良いのではないかと思います。
微分っぽさ以外で何が面白いのかと言うと、ここまでも停止するパーザに関する話を紹介してきましたが、 今度はなんと、与えられた正則表現で、入力となる文字列を受理するか否かを有限時間で判別する関数が、 微分の概念を用いるとCoqやらAgda2で非常に簡単に定義出来る、というものです。
しかもこれ、ただならぬ感じにキレイな等式が微分から導きだされて、 それがそもそも正則表現の構造に対して帰納的に定義されてるのでそれを書けば、 関数の定義が終わるという事になってるわけですよ!!
オートマトンを生成せずにすむという簡潔さも魅力なわけですけど、 ちょっとこれは何がどうなったらこんな事に…という感じです。
前から削って行くという一見単純な概念の奥深さのようなものが垣間見えると思います。 というより、この後2つの応用を読んでもらえれば。
あとは、これがあると良いよなーという性質が結構成り立つのも気持ちいいものです。 例えば、正則表現を微分したものはまた正則表現になるとかですかね。
title : Yacc is dead authors : Matthew Might , David Darais
Brzozowskiのderivative operatorが絡んだ最近の話題と言えばこれをおいてほかには〜。 はい…これ2010年のお話なんですよね。twitterでも非常に盛り上がっていましたが完全に無視していました。
Yaccが生きるとか死ぬとか、そんなことを紹介で言うつもりはありません!!
ここまでの話は、左再帰を含まない文法を扱う話ばかりでしたが、 ここからは任意の文脈自由文法(左再帰も合法)を扱う(扱いたい)話に突入です。
この論文では実行効率についても色々書いていますが、ここでは完全に無視します。
重要な点は2つ。
まず簡単に実装出来ないとダメということについて。 論文中では、未実装の言語で実装を試みた時に、 当該のアルゴリズムが複雑であると、実装にあたっての障害になってしまう。 そのまま結局実装されない、だと元も子もないというくだりがあります。 そんな曖昧な話ではなくて、例えばCoqとかAgda2で実装しようと思ったとしましょう。 この時、アルゴリズムの複雑さは絶望的速度で実装を地獄に追いやるので、簡単であればあるほど嬉しいです…。
任意の文脈自由文法が扱えると良いというのは、 勿論自分で言語を作る際にも役立つと思うのですが、 むしろ既存の文脈自由文法な言語に対するパーザを書こうと思った時に効力が発揮される気がします。
左再帰が扱えない場合、右再帰に変形してどうたらこうたらする必要があるのですが、 そもそもこの変形するという操作における保存性のようなものを言わないといけないわけです。
こと、仕様書が存在する言語に対するパーザを書く際は、 文法をコピペして一切手を加えないぐらいが良いとぼくは思うのですが。
それはさておき。 さてさて、Yacc is deadでは何をどうしているのでしょうか?? まず微分の考えを文脈自由文法に持ち込んでいます。
更にそのまま、パーザコンビネータに対して微分を拡張します (とはいえ、このパーザコンビネータはApplicativeっぽくなってて、 つまりMonadicではないので殆ど素直に文脈自由文法を実行可能にした程度だと思ってもらえれば)。
ここで問題が。文脈自由文法は本質的にrecursiveだとかなんとか先に書きましたが、 素直に微分しようとすると、微分操作が停止しないという問題が出てきます。例えば次の例。
List = (List · {x}) ⋃ {x} とする Dx(List) = Dx((List · {x}) ⋃ {x}) = Dx(List · {x}) ⋃ {є} = Dx(List) · {x} ⋃ {є} {Dx(List)が展開される} = (Dx(List) · {x} ⋃ {є}) · {x} ⋃ {є}
このようになってしまうと微分が停止しません。 エッじゃあどうなってるんですか!?!? パージングはどうするんですか!?!?!?!?
ここで評価戦略がlazyな言語を用いましょうという事ですね。ウオオーーーッ!!!
まぁこれ適当な事を言ってる訳じゃなくて、 この辺で楽に切り上げようと思うと実際lazyな言語を用いるのが楽ですという話です。
実際、著者らはライブラリをScala(でname passingを用いて)と Haskellで実装しています (ただ、あちこちでメモ化をしようとしているので、実装はぱっと見大変な事に成っています。 メモ化するのは当然高速化の為。具体的な計算量の話も論文にあります)。 (参考 : http://www.ucombinator.org/projects/parsing/)
チラッとScheme版もみた記憶があるのですが、 何をしているのかは知りません。 以上!!
正則表現ライブラリとか使うぐらいならパーザコンビネータがっつり書きますし…と思った皆様も、 興味が持てるのではないでしょうか。面白いと思うかどうかは知りませんが。
しかしその他の、例えばCYK parsing algorithmとか GLR parserあたりと比べても、 実装は結構楽になってるんじゃないかと思うのですが。
あとは、なんていうか面白いというか…やられた感は強いですよね。 人間やはり一般化を諦めては成りません。一般化というかこれは転用という感じなのですが。
title : Total Parser Combinators author : Nils Anders Danielsson
ヤバイ級に面白い
Yacc is deadっぽく微分を使って、CoqやAgda2で、 任意の文脈自由文法が扱えるライブラリのようなものを簡単に書けないだろうか、と考えるのは、 ここまでの流れの上では比較的自然なもののように思われます。
そんな皆様にお得なヤバイ級面白い論文が、 Total Parser Combinatorsです。
著者は前述の Structurally Recursive Descent Parsingも書いた Nils Anders Danielssonサンです。実装は当然Agda2!!
Structurally Recursive Descent ParsingはCoqでも 比較的素直に実装出来るような感じなのですが、こっちはそれほど楽ではありません (絶対に出来ないという事は無い気がするんですが…)。
またしてもAgda2を最大限利用している…というか、 mixed induction and coinductionという 型理論的にも面白い 3 4 手法を(比較的)カジュアルに用いて、(かなりの部分の)文脈自由文法を扱える monadic parser combinatorライブラリを作ろうという試みです。
解釈の部分では、確かにBrzozowskiの微分が息づいているのですが、 細かい条件が色々入っているのでかなり気合いを入れなければ読めない感じになっています。
とはいえ、任意の文脈自由文法を扱える、というわけではありません。 以下は論文にもある例なのですが
| p = p | p |
| p′ = p′ >>= λ x → return (f x) |
このようなnon-productiveな例は、 何をどうしたところで文字列をパーズ出来るものではないので認めないようにしています。
ただし、本論分では認めないようにすることが 不当に表現出来る範囲を狭めるものではないということを、 Expressive strengthという定理を証明することで示していることが 大変素晴らしい部分です。
Structurally Recursive Descent Parsingでは、正直な所、 使おうと思った時に実用に堪えられるかというと疑問が残るところがありました。 しかし本作ではその辺も上手い事解決していますし、 何より左再帰が扱えるようになったという所は大きな進歩であるように思います。
このような意味で、中々達成されなかった左再帰が扱えるパーザを作る為に、 どういうものが用いられたか、何故上手くいったのかを想像するワクワクします。 実際この論文はそれらの疑問に多く答えてくれるという意味でも 素晴らしいものでしょう。
特に、mixed induction and conductionの有効活用例を 実践的な例で示したというのも個人的には興味深いです。
積極的に使いたいテクニークですよねこれは…。 Agda2使い必読では。
title : Simple, functional, sound and complete parsing for all context-free grammars author : Tom Ridge
この論文を読んだ人はこんな論文を読んでいます。
Parser Combinators for Ambiguous Left-Recursive Grammars.
http://cs.uwindsor.ca/~hafiz/pub/PADL_PAPER_FINAL.pdf
論文中にも色々説明があるのですが、 いきなり読むと意味不明感が強かったのでオススメ論文を先に読むと雰囲気が分かり易いと思います。 実際、Tom Ridge自身が関連研究の部分で
this work can be taken as proof that the basic approach of Frost et al. is correct.
として書いているので、損は無い筈です。
さて、この論文で用いているアプローチはこれまでのものと一線を画します。 これまでは合法的な文法だけを選りすぐってその後の処理に繋いでましたが、 タイトル通りにall context-free grammarがついに許されるようになりました。
とはいえパージングはこれまで通りに再帰下降的に行っています。 …??? では一体どのようなカラクリで停止性を保証していると言うのでしょうか…???
任意の文法を許すわけですから、実行時に何かしらの基準を用いて 無限ループに向かっている事を察知し切り上げている筈です。
これはその通りで、読んでみると、確かに正しそうだ!! と膝を打つような基準を用いています。 といいますか、本論文はその切り上げが確かに正しいということを証明しているのですが。
答えは論文にありますので、少し考えてみて、突撃してください。
この論文はタイトルに偽りがありませんし、タイトルだけで面白すぎますよ。
ここまでは、本当に上手く行くことが分かっているものだけを対象にして必ず停止することを保証していました。
しかし、ここでは一転。実行させてみてダメそうなら失敗させる。という方向にしています。 ただそのダメそうというのが本質的にダメであるかを示せるかどうかというのは別問題です。 この論文は、実際にsoundnessと(ある種の)completenessを示しているというところが重要でしょう。
しかも(速度はさておきですが)簡単に実用出来そうなところが大変良いです。
別にパーザだけを書くつもりは無かったのですが、 一段落つくところまで書いてみると結構な量に成った感がありますし、 まぁ少なくともパーザなお話というだけですが若干の括りはある気がするので 取りあえずこれで。
パーザを定理証明支援系などで扱おうと思った際に面白いのは、 扱う文法は幾らでもcyclicに、再帰的に書けるものである、というところです。
それが故に、inductiveな方向だけを許そうというのでは上手く行かないことが多々あります。
この問題をどう扱うかというのは、 定理証明系を用いてこれまで通り無限ループしちゃうようなプログラムを、 カジュアルに書けるように成る為の分かり易くて面白い道場のようなものではないかと考えます。
とはいえ、coinductive一辺倒で戦うのが正しいかどうかも分かりません。 適切な道具を使って、もしくは新たに自分が道具を作り出すという事が強く求められます。
ただ一つ、これは割と言えることだとぼくが考えているのは、 従来のプログラミング言語で単純にループだとか再帰だとか言われていたものに対して、 もっとずっと注意深く、繊細になれるという事があります。 単に絶対に停止するというのと、停止しないような呼び出しパスが含まれるというのは大きな違いです。
ひいてはプログラムの構造そのものに、いつのまにか注目している自分がいる事に気付くシーンが 少々ですが、確かにあります。 そこから無理に数学に繋いだりする必要はないと思いますが、 停止するとかしないとか以前の問題に、ここで得た洞察は 通常のプログラムを書く際にもしばしば利用出来ると思うのです。
ぼくはより良いプログラムを書きたいと思っている人間なので、 この様な修行が出来るというのは何にも代え難いものだと 考えます。
This document was translated from LATEX by HEVEA.