Twitter: @kinaba
via 住井さん で、 ML Workshop の採択論文リストが出てることを知りました。 "Many holes in Hindley-Milner" (複数穴あり Zipper 的なものをMLで扱う話、穴の個数を型情報に含めるための加算できる自然数表現を差分リストで、 っていう技が面白かった) と "Unrestricted call-by-value recursion" （call-by-value で再帰的な (ループした) データ定義を実現する手法、これで、フルの call-by-need セマンティクスがなくてもそっち方面で使われてる テクニックをいくらか持ってこれるよ）というのだけ読んでみた。 他の併設ワークショップ の論文リストも 揃ってきてるみたいですね。 個人的に WGP の "Concepts =? Type Classes" がすごく気になる。 C++0x の concept と Haskell の型クラスの共通点と違うところを分析するという。気になる。
なんだか最近論文日記になっちゃってるなあ。どうしたものか。
（[Day 2-3'] [Day 1] の続き） 特に面白かったのはタイトルを <strong>で強調 してあります。 これで終わりです。
"Deterministic Pushdown Automata and Unary Languages" 文字の種類が１種類だと正規表現と文脈自由言語は表せるパターンに差がない、という話があるのですが、 そうは言っても、表現力には違いがあって、文脈自由言語で書いた方が指数^2倍短く書ける言語、みたいな のが存在することが知られています。文字の種類の制限を無くすと、DFAを文脈自由文法にもっていくと、 指数どころかどんな計算可能関数を持ってきてもそれ倍くらい短く書ける例が作れてしまうらしい。 一方で、DFAを決定性文脈自由文法（決定性プッシュダウンオートマトンで書けるCFG）だと、 文字の種類の制限を外しても二重指数関数倍くらいで爆発は収まるらしい。さて、決定性かつ文字の種類が １種類だとどうなるでしょうか、というのがこの論文のテーマ。普通の指数関数倍らしい。
"The number of runs in Sturmian words" 「長さnの 0/1 文字列の中に"繰り返し列"（定義がちょっとややこしい）が最大何個あるか問題」 というのが局地的に今大変ホットらしく。何年か前に最大でも O(n) 個であることがわかって、 それから O(n) の定数係数を求める争いが激化、0.9なんとかn個よりは多く 1.0何とかn個よりは少ない （細かい数値は忘れたけどnを挟む形）と言う結果が現在のところ最先端で、地図の四色問題みたいな計算機に よる列挙スタイルの証明で日々激戦が繰り広げられているという。 この研究は、任意の文字列ではなくて、Sturmian words という特殊な形式の文字列では何個あるかを求めたもの。 Sturmian words というのはフィボナッチ拡張版みたいなもので、自然数の列 [a,b,c] に対応する Sturmian word は、s1="0" s2="1" s3=s2^a.s1 s4=s3^b.s2 s5=s4^c.s3 の s5。[1,1,1,1,1] とかだと5番目のフィボナッチword。 この特殊な構造を元に、このパターンに当てはまる文字列ではピッタリ 0.8n が個数の上限なことを証明したとのこと。 Subword Automaton (ある単語の部分列のみ＆すべてにマッチするオートマトン) を作ってその構造について 考えるという方針を強調されていました。
"Learning Regular Languages Using Nondeterministic Finite Automata" マッチして欲しい文字列の例と、して欲しくない文字列の例から学習してNFAを作るアルゴリズム。 全然知らない方面の話なので既存手法の話から面白かった。「まず正の例で trie を作って、負の例に マッチしない範囲で状態と状態をひたすらマージする」のがこれまでのNFA学習法らしい。 今回の話は正の例と負の例をインターリーブさせながら学習する感じでした。
Invited Talk は Petrinet の話。寝てました。
"Games for Temporal Logics on Trees" CTL の一般化バージョンの表現力をゲームで特徴づける話。 よくありそうだったけどどの辺が新しいのかよくわからんかった…。
[PDF] "Composed Bisimulation for Tree Automata" Best Paper 賞受賞。 Bottom-upツリーNFAの最小化…を完全にやるとコストが大きいのでそこそこ小さくするアルゴリズム。 オートマトンのサイズ削減というのは、要は、いかにして全く同じ言語（文字列／木）を受理する 複数の状態を見つけるか（見つけたらそれをマージするのは簡単）なわけですが、文字列の場合 状態の Bisimulation を使う方法が 計算量的に比較的お手軽なことが知られていて、これをツリーに応用してみる話です。 downward bisimulation (同じ部分木集合を受理する、という同値関係) と、 upward bisimulation (同じコンテキスト(部分木を取り除いた残り)に必ず現れる、という同値関係) を 使ってこれを合成することでうまく行くとかなんとか。
[PDF] "Progressive Solutions to FSM Equations" 入力と出力がある有限状態マシンSが２つのコンポーネントAとXの合成でできてることがわかっていて、 SとAの入出力仕様が完全にわかっているときXを求めるという問題があるらしく。 条件を満たす最大の X を求める計算法はすでにあったのだけど、これは デッドロックしない（無限ε遷移にはまらない）ような最大の X を求める方法だそうだ。
最後に "New Ideas and Open Problems" セッションがありました。未解決問題を交換しあったり、 こういう方向に研究進めてみるといいんじゃない？オートマトン業界的に、みたいな意見交換などなど。
色々話がありましたが、 Smoothness が 話題になってて（きっとICALPからの直輸入だと思う）確かにこれは面白そうでした。 指数実行時間をもたらすような最悪ケースが特異点のような形になっていて、 ちょっと最悪ケースの形を変えたような近傍ケースでは軒並み高速に動くような アルゴリズムだと、要は最悪ケース周りの計算量の変化が「急」だと、最悪はともかく実際は速かったり、 そこが「滑らか/smooth」だと、実際にも最悪に近いケースにつかまりやすかったり…… というのが直感的な理解らしい。１日目最後の、「Brzozowski のアルゴリズムは最悪指数なはずなのに 実際は速い」みたいなのをこれで理論づけられないか？等々。 他には、今回のCIAAで何回 Hopcroft って出てきたよっていうくらい最小化アルゴリズムが人気だけれど、 決定化と違って、最小化は実際には最小でなくても小さければいいという応用はとても多いわけで、 「最小の2倍以内のサイズにはする」みたいな近似アルゴリズムってこの分野全然ないよね誰かやれよ、 みたいな。「無くはない、近似まで考えても効率を上げるのは全然無理という結果がなんかの問題で出てた」 と言ってる人もいた。
30KB 超えてしまった…。 LNCS 読める人は http://dx.doi.org/10.1007/978-3-540-70844-5 から論文PDFが手に入ります。 何個かはタイトルぐぐれば見つかるかも。（※追記：見つけた分のリンクを追加）
（[Day 1] の続き） 特に面白かったのはタイトルを <strong>で強調 してあります。
Invited Talk は "Language Decompositions, Primality, and Trajectory-Based Operations"。 1問 $300 の賞金付きの Open Problem 3題！ 正規言語の素因数分解みたいなのを考えます。r1 = /ab|a/ にマッチする文字列は、 r2=/a/ にマッチする文字列と r3=/b?/ にマッチする文字列の結合になってます。 逆に、r2にマッチする文字列とr3にマッチする文字列の結合は、必ずr1にマッチします。 つまり、r1 = r2 r3 と"因数分解"できると考えることができます。 一方で、r4 = /ab|ba/ をそういう風に分解することはできません。つまり r4 は"素数"。 あ、もちろん r5=// と空文字列にのみマッチする文字列を使うと r4 = r4 r5 なんですが、 普通の数の素因数分解するときに 1 を考えないのと同じで、この話では // は素数に数えないことにします。 未解決問題１：正規表現/NFA/DFAが"素数"かどうか判定する効率的なアルゴリズムはあるか？ （ただしこれは賞金無し）。 ところで、正規表現の場合、"素因数分解" は一意とは限りません。 例として、/a|aa|aaa/ = /a?/ /a?/ /a?/ と /a|aa|aaa/ = /a?/ /(aa)?/ という２通りの分解がありえます。 /(aa)?/ = /a?/ /a?/ ではないのに注意。/(aa)?/ は"素数"です。 未解決問題２：正規表現には必ず"素因数分解"が存在するか？ "素数"でなければ定義上"因数分解"はできるので、結局のところ「いくら分解しても"素因数"の結合にならないような 無限に分解するしかない正規表現は存在するか？」という問いになります。 あとは、"Trajectory" という概念を使ったこの話の一般化。Trajectory とは文字 0 と 1 上の正規言語のことで、 「正規言語 r と r' の Trajectory t によるシャッフル」を、「r,r',t にマッチする文字列をそれぞれ適当に 取ってきて、tの0の所にrから取ってきた文字列を埋めて、1の所にr'から取ってきた文字列を埋める処理」で定義。 さっきの文字列の結合は t=/0*1*/ によるシャッフルということになります。/(01)*/ や /[01]*/ みたいな シャッフルもあれば、もっと変態的な混ぜ方も考えられる、と。この一般シャッフルでの分解可能性の判定 に関する問題が残りの賞金付き問題でした。
ひとひねりあるパターン検索のセッション。
[PDF] "Automata-theoretic Analysis of Bit-split Languages for Packet Scanning" Snort みたいな侵入検知の並列化。 要は検知パターン（ASCII上の Aho-Corasick オートマトン）を bit 毎にバラして 8 並列で嬉しいという。愚直にバラすとマッチしない はずのものまで検出してしまうところもちゃんとどうにかなっている、という話だったらしいんですが、 主にそもそも /a*/ ってどう素因数分解するんだ等を考えていてちゃんと聞けてません(汗
"Pattern Matching in DCA Coded Text" 圧縮した文字列に対して圧縮したまま検索かけるよー系のお話。 反辞書 による圧縮データに対してのアルゴリズムらしい。 主に /a*/ = /a?/ /(a(aa)*)?/ で合ってるだろうか等を考えていて（以下略
"A Run-Time Efficient Implementation of Compressed Pattern Matching" 発表者が物凄い理由で不在につきピンチヒッター。 こちらも圧縮した文字列に対して圧縮したまま検索かけるよー系のお話。 truncation-free な collage-system というものになってる圧縮法（LZ78 や BPE が入る、LZ77 は入らない） + prefix符号（ハフマンとか）な圧縮に対してのアルゴリズムらしい。 BPE っぽい系統の圧縮法に応用されてたような感じだったのだけど、これ compress コマンドの圧縮に対しては使えるんじゃないのかな。あれって LZW + 何だっけ。
Invited Talk は 確率文脈自由文法 方面の話だった気がしますが、再帰的なマルコフモデルがどうとか、 自分の発表の１つ前なんて集中できるわけがないのでした。 どういう文脈だったか覚えてないんですが、 「入力：自然数d1,d2,...,dn,k、出力：Σ(√di)≦k かどうか」 の判定問題が NP かどうかすらわかっていない、PSPACE に入ることは最近証明された、 という話が面白かった。続いてトランスデューサーセッション。
[PDF] "Multi-Return Macro Tree Transducers" 元々の始まりはコンパイラ方面の話だと思うんですけど、Macro Tree Transducer (MTT) というものがあります。 コンパイラの定式化の基本は Knuth の属性文法 (Attribute Grammar / AG) があって、あれは典型的には synthesized 属性は「戻り値」、inherited 属性は「引数」 で実装されることになるんですけど、 実際問題として実装がそうなるんだったら、いっそ「引数と戻り値つきで木構造を再帰的にtop-downトラバースする 相互再帰関数群」というモデルを最初から考えちゃえばどうよ？というのが MTT、たぶん。適当言ってるかもしれない。 最近はコンパイラよりも、 一般に関数型言語のfoldっぽい再帰関数の合成による最適化やら、XSLTみたいな木変換言語の解析やらの モデルとして使われていると思う。 んで、MTT では別々のsynthesized属性は別々の関数にして、各関数の戻り値は一つという形の 定式化になってるんですが、これは多値（と厳密に言っていいのかどうか微妙ですが）を返せる定式化にしておくと 幾つか嬉しい性質が得られるよ、というお話。
"On Complexity of Two Dimensional Languages Generated By Transducers" セルオートマトンみたいなので初期パターンから始めて絵ができていくようなのを Transducer の繰り返し適用として定式化して、出てくる絵のエントロピーがどうとかという話だったように 思いますが気が抜けてて全然聞いていないのでした。やばいちゃんと聞けてない発表多すぎる。
[arXiv] "3-way Composition of Weighted Finite-State Transducers" １日目の Tree-Series と同じで、変換規則に重みを付けた Transducer の話。今回は文字列。 ３個の Transducer を合成して １個の Transducer にしたいシチュエーションが結構あるらしいんですが、 既存の２個の合成アルゴリズムで T1・T2・T3 = (T1・T2)・T3 で計算すると、(T1・T2) が巨大にふくれて それから T3 で一気にフィルタして小さくなるようなパターン（もしくは T1・(T2・T3) でも同様）を避けたくて、 一気に 3-way 合成するアルゴリズムを作りましたというお話。 基本的には３つのtransducerの状態を組にしたproduct constructionなんだけど、詳しくはよく 理解できてないのですがε遷移のループができると単純なproduct constructionでは間違いになるらしく、 そういうループを消すε-filterというテクニックの3-way版がメインの内容らしい。
無限なセッション。
"Testing whether a binary and prolongeable regular language L is geometrical or not on the minimal deterministic automaton of pref(L)" Geometrical 言語というのは、二次元平面上の格子点の原点を含む集合で表される言語。 {(0,0), (0,1), (1,0), (1,1), (1,2)} は {"", "x", "y", "xy", "yx", "xyy", "yxy"} を表す感じ。 含まれる格子点をたどって右上方向に進んで行ったときのxとyの列が文字列、という。3次元以上の Geometrical 言語もあるけれど今回の対象は2次元。prefix-closed な言語の DFA が与えられたときに、 それが Geometrical かどうかを判定するアルゴリズム、とのこと。DFAの状態を２次元平面上にマップしていって、 最左と最右パスを通って変な風に交わらないか判定するとかそんな感じでした。
[PDF] "Computing Convex Hulls by Automaton Iteration" 死ぬほど感動した。 いや実際どのくらい実用に耐える速度で動くのかは知らないんですけど。 これは自分で一度この手のエンジンを組んでみて感覚をつかむ必要がある！！と思いました。 自然数をビット列と見なすと、ある種の自然数の集合は、正規表現やDFAで表現できます。 「偶数全体の集合」なら /(1[01]*)?0/ こんなの。「16以上31以下」/1[01]{4}/。 適当なエンコードをすることで、自然数のペアやタプル等も表現可能。 オートマトンで表現した自然数に対してどういう演算ができるかというと、自由に使えるのは足し算と 不等号での比較くらい。一般の掛け算は無理（正規言語にならないので）。 要はPresburger算術です。 ところで、自然数の場合有限列ですが、無限列を受理するオートマトンも60年近く前から考えられています。 この Büchi automaton をちょっと制限したものを使うことで、ビットの無限列…実数や、その集合、ペア、タプル等も無限精度で表現できます。 そして、この集合を表現するオートマトンから、等価な線形不等式系を得る多項式時間アルゴリズムが 2005年に発見されている、と、 ここまでが背景。「この表現を使って n次元 凸法 を求めるアルゴリズム」というのがこの論文の肝になります。→→ 1: 元となる点の集合をSとしてオートマトンで表現 2: S に入ってる点同士の中点を全部 S に追加。つまり S = {(v1+v2)/2 | v1,v2∈S}。 これを無限に繰り返した極限 S∞ はオートマトンで表現可能 3: 一般に閉包はこのオートマトン表現で計算できるので S∞ の閉包 C∞ も表現可能 4: C∞ が凸包 ←← わかりやすすぎる。 3次元凸法を分割統治で計算するアルゴリズムを理解しようとして３回くらい挫折した身としては これはヤバいと言わざるを得ない。
"Automated Compositional Reasoning of Intuitionistically Closed Regular Properties" これも Büchi automaton の応用の話。モデル検査の際に最弱事前条件を求めるかなにかの処理が必要になって、 制限を入れない Büchi automaton だと補集合の計算が難しいので考えてみた、というお話。 普通の正規言語というのは、文字列の有限集合とandとorとnotと結合と*演算で閉じた（正規言語にそれらの演算を 加えてもまた正規言語になる）最小の言語クラス、という定式化がなされていて、要するにブール代数で 閉じたクラスということになっています。これを Heyting代数 で閉じたクラスというものを考えてみるとどうなるか、という。 ブール代数が古典論理に対応するのに対してHeyting代数は直観主義論理に対応しているわけで、 計算しやすさという面ではなかなか良い感じになるらしい。
（[Day 3''-4]に続く）
これ 行ってきました。未来の自分のために勢いでほぼ全部メモっておきますが、 細かい話読んでも面白くないと思うので、適当にスルーしてください。 特に面白かったのはタイトルを <strong>で強調 してあります。 あと一応軽く用語集。
Invited Talk は、NFA の計算量が今熱い！というお話でした。 DFA なら解き方がよく知られている問題（最小化、同値判定 etc）も NFA では異様に難しかったりするとか、NFA と DFA の表現力の差（最小DFAと最小NFAのサイズの差 etc） はどんなものか、とか色々色々。んで、そのあと第１セッションのはじまりはじまり。
[PDF] "Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata" ツリーNFAの性質を調べる効率的なアルゴリズムの話。 Universality というのは、どんなツリーにもマッチするオートマトンかどうかのチェック。 文字列でいうと、要は正規表現 /.*/ と等価かどうかのチェック。 もちろんDFAに変換すれば楽勝なんですけどその変換自体が最悪O(2^n)なので、 非決定性のまま直接やれるならやりたい。 文字列で説明すると、基本的には、S0={{q0}} :: 入力読む前のNFAの状態の可能性を全列挙 S1={{δ(q,a)|q∈s} | s∈S0, a∈Σ} :: １文字以下読んだ後の状態の可能性を全列挙、 ……みたいに繰り返してって受理状態集合 F と交わらない集合が Si にでてきたらそこで試合終了 Universal ではありませんでした、という方式。Si の中に s⊆t な s と t が両方入ってたら s の方だけ 考えれば十分なので、Si は互いに包含関係のない要素同士のあつまり（= antichain）だけ考えればよいことに 注意するとわりと良い感じに動くらしい。Inclusion は QA×2^QB 上の antichain を考えると同様。 ツリーに適用する場合は bottom-up で。top-down は難しい。
"A Translation from the HTML DTD into a Regular Hedge Grammar" XHTML じゃなくて HTML だと閉じタグ省略したりできるので、 PHP をプログラム解析して 出力の形式の正しさ を検査したい的に考えると XML と違って面倒なのですけど、 そのタグ省略規則まで含めて HTML DTD を形式的に扱いやすい形にもって行きましたという話。 テクニカルには、DTD の定義する木構造のタグ省略無し版を生成する文法の上に 消せるタグを非決定的に消す transducer を走らせて計算。
[PDF] "Tree-Series-to-Tree-Series Transformations" 重みつき Tree Transducer というものを考えたい。機械翻訳をtreeからtreeへの変換としてモデル化して、 各翻訳規則に「正しそう度」を載せておいて、最終的に、使った全規則の「正しそう度」を合算した値が 一番大きい物を選ぶとかなんとか。tree から tree集合への変換だけを考える範囲ではその「重み／正しそう度」は 数学的に言えば Semiring (半環) でありさえすれば いいんだけど、たまにtreeの無限集合を入力として出力を考えたいことがあって、その場合Semiring上での無限和が ちゃんと取れるという制限を加えないといけなくなってうっとおしい。そこで逆に、扱いにくいタイプの無限和が 出てこないような重み付き Transducer だけを考えるというアプローチが考えられるわけですけどそれは どういう Transducer か。結論は、"deletion" と "replication" と呼ばれる種類の形の変換規則がなければいい、 ということだそうな。 自分もこの前書いた論文で、用途は違うけど、その２つ（ともう１つ）の形の 変換規則が大変邪魔なのでどうにかする的なことをやってたので面白かった。
続いて第２セッション。古典中の古典のようなアルゴリズムでもまだまだ考えるべきところは多いらしい。
"Hopcroft's Minimization Technique: Queues or Stacks?" DFA の無駄を無くして最小の DFA を作るアルゴリズムとして Hopcroft さんが考えた O(n log n) の方法が あります。最初は「受理状態は全部同じ」「受理状態じゃない状態も全部同じ」ものと見なしておいて、 一文字読んだあとの遷移を調べて全部同じだとマズいことがわかったら同じとみなした集合を適宜分割して いく…というアルゴリズムなんですが、分割基準を適用する順番をキューで管理するかスタックで管理するか 実装に自由度があって、どっちがいいんだろうね、というお話。 扱う文字が一種類しかないような特殊な場合だとスタックなら実は O(n) になることと、キューだと最悪ケース n log n になるような場合が実際あることを証明。だからスタックの方がいいんじゃね？ってのはまあ早計 ですけどもそんな感じです、みたいな発表でした。
"Five Determinization Algorithms" NFA を DFA 化（した上でできるだけ状態数最小化）するアルゴリズム５題。 「A: 状態集合を状態と見なしてDFA作成」 → 「A': さらに Hopcroft's Algorithm」が基本パターンですが、 これをどうにかしたい。特に最小化は意外と重いので、いきなり小さいDFAを作れる決定化アルゴリズムとか欲しい。 まずは「B: 新しい状態集合SをDFAの状態として付け加えるまえに一息入れて、Sに足しても状態としての意味は 変わらないような集合を全部入れたS'を作ってからDFAの状態とする案」これをマジメにやるといきなり 最小DFAが出るんだけど、SからS'を計算するのは超しんどいので、「C: S'の近似S''で我慢する案」などを考える。 あるいは「D: 状態(頂点)の集合ではなく遷移(辺)の集合をDFAの状態とする」という構築法。 あと、最初のanti-chainの話ででてきたのと似たようなアイデアで、 「E: 極大集合だか極小集合だかのみを考える"compress"法」。 できるDFAのサイズはおおよそ A > D >> C > E = D+E > B=A' で、計算時間は (他) >>> E > D+E みたいな雰囲気。
"Hyper-Minimization in O(n^2) time" もとの DFA と同じ文字列を受理するという性質を保ちつつ DFA の状態数を最小にするのが普通の Minimization (O(n log n)) ですが、それでもまだメモリが足りない時とかのために、 「もとの DFA と受理結果が変わっちゃうような文字列はたかだか有限個」で状態数最小の DFA を構築するハイパーミニマイゼーション！ 有限個くらい違っても大して困んなくない？ という話ではなく、 有限種類の文字列しか受理しない DFA に対しては "Cover Automaton" という効率的な表現が知られている らしく、それと合わせて使うとお得だとか。 方法は、xor で product construction。つまり、元の DFA の状態集合を Q 受理集合を F とすると 状態集合 Q×Q 受理集合 {(q,p) | q∈F xor p∈F } の DFA を考える。 このxorオートマトンの状態(q,p)が有限種類の文字列しか受理しない ⇔ 元の状態 q が受理する言語と p が受理する言語の差は有限、なので p と q がマージできるという判定に使える。終了。xor かっこいい。 このアルゴリズムはproductを取る時点で O(n^2) 確定なんだけど、もっと効率よく、たとえば Hopcroft のと同じで O(n log n) にならないか？という辺りは未解決問題。xor状態の有限性判定とマージ処理を 遅延実行しながら一気にやると計算量減らせそうな気がしてしばらく考えてたのですけど、ちょっとわからんですね。
怪しげなマシーン大集合セッション。
"Persistent Computation of Turing Machines" 著者不在につき発表なしー。タイトルには凄い惹かれるものがあるのであとで論文読まないと。
"Finite Eilenberg Machines" オートマトンやトランスデューサーやプッシュダウンオートマトンを表現できる 汎用的な枠組み "Finite Eilenberg Machine" を扱うフレームワークを OCaml で作ったよ、 というお話。要は、有限状態間のラベルとしてある種の制約を満たした関数を任意に割り当てられる モジュール。計算を関数の合成で表現して結果を返してくれる。Coq で色々証明していた。Coq やらないとなあ…
[PDF] "Antimirov and Mosses's Rewrite System Revisited" 正規表現と正規表現の等価性判定アルゴリズム。古典的な方法は、 「NFA作る→DFA作る→Hopcroft's Minimizaion→グラフの同型判定」です。 一方、同じくらいの古典として 正規表現を微分する スタイルというのがあって、そっち方面の流れで「99.9..% の信頼度で同型性を保証」 みたいなアルゴリズムを開発実装実験してみた、という話だったと思います。xor 考えててあまり聞いていなかった。 計算量のオーダーとしては Hopcroft の O(n log n) vs 他みんな指数時間なんだけど、実際実験してみると Brzozowski 系統のアルゴリズムは基本的にほぼ線形で走ってるように見える、速い、とのこと。 ここでも槍玉に挙がる人気者の Hopcroft。 DFAをMinimizeしないで直接同値性判定するアルゴリズムが存在[Hopcroft,Karp?]してるのを論文書いた後 に知ったので実験してみたけどそれよりも若干速いよーと言っていた。
ポスターセッション。
"Combination of Context-Free Grammars and Tree Automata for Unranked and Ranked Trees" Regular Hedge Grammar (DTD みたいに子要素の列を正規表現で表すタイプの木文法) を拡張して Context-Free Hedge Grammar を考えてみるテスト。XML を文字列として表すと Context-Free Hedge Grammar の出力文字列は Context-Free に収まるらしい。面白げ。 そして発表にあった予想の反例作れるんじゃないか？と思って延々考えてたので他のを全くポスター発表 まったくチェックしてないのであった。反例は作れたのですけどすかさず南出先生に それKnuth と突っ込まれてしかも Knuth の例の方がずっとシンプルでした Knuth は偉大。
（[Day 2-3'] [Day 3''-4] に続く）
明日から Conference on Implementation and Application of Automata というのに行ってきます。 正規表現の実装の話なんかでよくでてくる オートマトン に関係した話を４日間ひたすら繰り広げる学会であります。 今までプログラミング言語の学会にしか参加したことがなかったので、ちょっと違う世界で楽しみ。 てか、面白そうな発表が多すぎてヤバい。
"3 not problem"
を読んで、長いこと考えて解けなかったので Ruby で全探索して答えを出してから意味を考えたら、
確かに要は3は2ビットで表現できるということ
になってました。感動。
ほとんど答えなヒントな答えをコメントアウト <!--
気力が尽きてたらやらないつもりでしたが大丈夫そうなので、明後日の Google Code Jam 2008 も参加しようと思います。練習問題見る限りでは ICPC や TopCoder 的な問題なのかな。 ただし言語は自由、Mathematica や Excel を使いたければ使うのも自由、ライブラリを 使うのも遠慮無く、というスタイル。よっしゃ頑張ろう。
ルール見た感じGoogle関係者は参加しないのかーそれはちょっと残念。
おわったーぜんぜんだめだー。去年で言うとRNA出すのに30時間かかる処理系が作れましたレベル。
今回の問題は、「山あり谷あり火星人ありの地形の上を走る無人探査用の車を制御するプログラムを書いて、 上手く基地まで誘導してあげてね」というものでした。タイムリミットがあるのでアクセルベタ踏みで行きたいけれど、 スピード出し過ぎると曲がれずにクレーターに落っこちるなどなど。いいバランスの問題で面白かった！ 以下考えたことの流れ。
とりあえずライトニング部門用に速攻で実装できそうな方法として考えたのは、「homeや山やクレーターや 火星人それぞれからの距離の逆二乗に適当な係数をかけた値の総和が低い方にひたすら向かう」。 要するに、home からは引力、その他障害物からは斥力が働いていると考えたときの力の向きに沿ってできる限り 進もうとする方法。「沿って進もうとする」というのは、具体的には、今の向きより力の向きが左向きなら l 右向きなら r、＆、前向きなら a 後ろ向きなら b を送るというだけ。実装めちゃくちゃ簡単です。 これで small_scatter.wrld は行けるんですが、spiral.wrld みたいに障害物が密集している地帯に 外から突入しないといけないパターンだと、この引力斥力モデルでは外向きに斥力の方が強くなってしまって、 home に近づけないことが発覚。 そこで、「斥力は home と物体を結ぶ直線に垂直な方向にのみ発生する」ようにして、 外向きに押し出されないように調整。確かこれのバリエーションで spiral をおおむね抜けられるようになったので、 ライトニングにはそれで提出したんだったと思う。サーバーがバージョンアップすると全然 home に行けなくなったりしてわりとどうしようもない感じ。
んで、その後どうする…と考えたのですが、「マジメに経路プランを考えて適切なタイミングで命令を飛ばす」 みたいなのは加速度係数と摩擦係数とハンドルの回転速度の推定をした上で幾何的な計算ないし数値積分をしつつ ネットワーク遅延を考慮しながら非同期通信してあとタイマーでミリ秒単位でタイミング計ったりしないと いけなさそうで面倒だなーと思ってしまったので（ここら辺のやる気のなさからしてどうしようもない）、 上記の方針の延長線上を行くことに決定。 各 "T" メッセージが届いた時点（だいたい100msに一回）で、 怪しげな力の場を設定してその地点に働く力を決めて、その都度ローカルに方針を決定。 結局、色んな要素に力ベクトルを計算させて それを足し合わせて方向を決める感じ…つまり 議会制弾幕回避機関 が劣化したみたいなのになりました。最終的には Hickie (homeを目指す) と Boomkn (進行方向にあるBoulderを 避ける) と Claire (進行方向にあるCraterを避ける) と Martin (火星人を避ける) と Oberon (homeを通り 過ぎちゃったときに思いっきりブレーキかける) 5人の合議制。 あとは千鳥足状態にならないようバランスとる人やら、数百ミリ秒以内にクレーターに突っ込むことが 予測される行動はすべてキャンセルさせる人やらなんとなく障害物の多い方向を嫌う人やらを 作っては消し作っては消ししていました。
まあ、home へ向かう理由は引力だけなので、長い壁や迷路を作られると完全にお手上げです。 というか、そもそも普通のマップでも全然安定してhomeに帰れないまま終わってしまいました。 いまだに spiral ですら結構死ぬという。むずかしい…。 明日他のみんなのコードを読んで修行しよう。
ICFP コンテストちゅう。 OMeta/JS で行こうと準備してたのですけども、 パターンマッチの使い所など一つも見いだせない感じだったので結局ただの JavaScript でやってます。 問題の舞台が火星なので、DigitalMars の言語を使う人は頑張り所なのではないかと思います頑張ってください！
問題内容は、2003年の車制御コンテストをマップ非公開にして、あと制御しやすくして、 ちゃんとプログラムで解きやすくした感じですかね。 とりあえず、とっさに思いついた方法で spiral や small_scatter ならまあまあの精度で home に帰れるのが最初の10時間くらいでできたんですが、そっから24時間何も進んでいないのが現状です。 300行弱。まあまあの精度で帰るというのも、自分が組んだはずのアルゴリズムから推測されるのと 全然違う行動を取って帰ってくるのでちょっともうこれはどうしたものか。
もう少しシビアにタイミング読んで命令送ったりしたいんですが、ちょっと手元の マシンでは VMWare が重すぎて、変にこれに合わせてしまうと実機で酷いことになりそうで怖くてできない。 あと VMWare とホストでファイル共有する方法がどうもうまくいかなかったので、 ホストでコード直す → 外のsvnレポジトリにインターネット経由でチェックイン → VMWareの中からチェックアウト → 中で実行、という、１回のテストランにかかる時間が長くてしんどい。
さてそろそろコーディング再開…
計算するだけが式じゃないぜ。
package Yuno;
import static Yuno.Yuno.Hi.*;
import static Yuno.Yuno.Da.*;
import static Yuno.Yuno.Ma.*;
public class Yuno
{
static int myprint(String s)
{ System.out.print(s); return 1; }
static class Hi { static int 来週も見てくださいね = myprint("来週も見てくださいね！\n"); }
static class Da { static int X = myprint("×365 "); }
static class Ma { static int _ = myprint("スケッチ"); }
static class Ri { static int X = myprint("ひだまり"); }
public static void main(String[] arg) {
boolean Hi_Da_Ma=Ri.
X / _ / X < 来週も見てくださいね;
}
}
演算子オーバーロードのない Java だと / や < の評価の際に何か別の処理をさせるのは java.lang.instrument 辺りまで持ち出す大技に なっちゃうと思いますので、ここは変数 X や _ を評価する際に別のコードを走らせてみました。
Java のクラスのロード/初期化（特にここでは、staticフィールドの値セット）は、
プログラム起動時に一気に行われるわけではなく、「最初にそのクラスが使われる時」に行われます。
このコードの場合、Ri. X が評価されるときに Ri がロードされて、
_ が評価されるときに Ma がロードされて…、という順番でクラスがロードされます。
（細かい仕様はよく知らないので、実装依存かもしれません。）
（追記：調べました。
12.4.1 When Initialization Occurs によると初期化は immediately before
the first occurrence of
... A static field declared by T is used and the field is
not a constant variable
ということで、ちゃんと実装非依存で成り立つようです。）
追記： id:t_yano さんのバージョン。 なるほど assert と : を使って "文字列" をそこに置けるようにするのは上手いですね！ 自分のは、「来週も見てくださいね」がソースコード上に３回も 出てきてしまってるのが自分でどうも気に入らない…。それを言うと昨日のD版なんか無茶苦茶なんですが…。
これは何かというと
X / _ / X < ... っていうAAの形で書くというだけの遊びだと思いますよ、たぶん！ 私もよくわからんけど。 あと最初の人は単にゆのっちを描きたかっただけかもしらんですけど。 「たったそれだけ」なはずなのに、例えば 水島さんの Scala 版 は恐ろしいほどスカラスカラしてる（ _ が無名関数を楽に書くための placeholder で困ったところを implicit conversion を使って回避！）し、 sumim さんの Squeak Smalltalk 版 は「_ が代入と同じ」という特徴を、スキャナの作業用テーブルを言語の中から書き換えるという、 ああこれは Smalltalk だなぁというダイナミックな手段で解決するし、 ranha さんの Haskell 版 は、知らない人には ghc って cpp 通したりできるのかよ！みたいな発見があると思う。 自分の Java 版も、「クラス初期化のタイミングは本当に最初の使用のギリギリ直前になってる」 という Java ならでは…というほどでもないかもしれないけど割と Java チックな特徴を盛り込んだつもりです。 という感じで、各言語各様の特徴と変態的な解決策を楽しむといいんじゃないかなーという。
via 水島さん他。 ref. cho45のブックマーク > ゆの in language
import std.stdio;
class 来週も見てくださいね () {
static:
ひだまり opDiv (スケッチ X) { write(typeof(X).stringof); return typeof(return).init; }
スケッチ opDiv_r (ひだまり X) { write(typeof(X).stringof); return typeof(return).init; }
来週も見てくださいね opCall() { write(typeof(X).stringof); return typeof(return).init; }
int opCmp(X)(X X) { write(typeof(X).stringof); return typeof(return).init; }
}
class ひだまり : 来週も見てくださいね! (){}
class スケッチ : ひだまり {}
class x365 : スケッチ {}
alias ひだまり _ ; x365 X;
int main(){ return
/////////////////////////////////////////////////////////////////
X / _ / X < 来週も見てくださいね!
/////////////////////////////////////////////////////////////////
()();}
盛大に間違えようとして間違いきれなかった感がありますがポイントは
あ、D でも普通にやろうと思えば普通にできますので、その辺りは誤解なきように…。
西サモアの日が変わるまでが7月7日です って明示されてるとありがたいですよね。僕たちの七夕はまだ始まったばかりだ！！！ 通ればインドで id:wpw さんとウハウハしてきます。いや通ればっていうか、書き終わるんでしょうかこれ。
全然関係ないんですが Nine open problems for conjunctive and Boolean grammars というのを最近知って、問題がわりとわかりやすかったので思わず考えてしまっています。 いわゆる文脈自由文法は、文字列と文字列の結合と論理和 | だけで記述する文法ですが、 それに & を足した Conjunctive Grammar と、さらに否定 ! を足した Boolean Grammar の表現力はいかほどか、というもの。
一つすでに解かれている問題は、文字が１種類だけの場合「正規表現で書けるパターン」
と「Conjuctive Grammarで書けるパターン」の表現力は一致するか？というもの。
文脈自由文法の場合は正規表現と一致することが知られています。例えば
A → 'a' A 'a' | 'a' は要するに「奇数個の'a'」で、これは a(aa)*
みたいに正規表現でも書ける。正規表現より文脈自由文法が強いのは要は括弧の対応関係みたいなのが
とれるからなんですが、文字が１種類だけで単に文字数だけの問題になると、そういう差がつけられなくなる。
一方で、Boolean Grammar まで強めると楽勝で正規表現で書けないパターンが作れるらしく、
さてそれでは中間の Conjunctive Grammar はどうでしょう、という問題ですね。
答えは「正規表現じゃ書けないパターンは、作れる」らしい。
締め切り１日前なので現実逃避日記です。
くるるさんのを見ながら まとめるつもり一切なく考えたことを垂れ流してみる。
・前の記事では単純な型付きの関数型言語をなんとなく前提に表示的意味論を説明しましたが、 表示的意味論が素敵にカオスになっていくのは型無しλ計算を相手にしたときで…
・fix(G) の定義に fix(G) を使ってる問題は、型無し言語なら定義からfixを消すことができて、
function fix2(G){
return (function(x){ return G(function(y){return (x(x))(y)} })(
function(x){ return G(function(y){return (x(x))(y)} }
)
} // 実は適当に書いたので合ってるか自信ない
いわゆる call-by-value 版 Y コンビネータとかいうヤツですが。
これでプログラマなら完全に再帰が消えたので安心という気分になれる可能性もありますが、
Axiom of Foundation 人間には、たぶんより一層キモさが明確になってるかもしれません。
何がキモいってこれ → x(x)。関数 x の値域に x 自身が入ってきている。これは大変です。
・形無しλ式に表示的意味を与えたい。さて、形無しλ式で表せる数学的オブジェクト全体の 集合を D とする。する、っていうか、 まずそもそもその D ってどういう集合だよって問題がでてきて、D は D の中に "DからDへの関数" …を全て含むことはできないので "DからDへの計算可能な関数" …を全て含んでいる（正確にはそういう 集合を単射で埋め込める）でないといけない。そういう謎集合Dと"計算可能な関数"とその埋め込みと…を 考えたのが Scott さんという人であり、その辺が領域理論の面白いところであり。
・なんかイメージ的には Lowenheim-Skolem により可算モデルがあるはずなのに "非可算集合の存在" は証明できちゃうよ、みたいなイメージが。 fix や fix2 は外から見ると中では有り得ないことをしているような感じがするけど、 中（計算可能な世界 / D）から見える範囲では fix や fix2 は機能している。 そういう意味では…どうなるんだろう。
・すごい適当なことを言った気がするぞ俺。
・話が飛びますけど計算量の話で Uniformity ってありますよね。あれも何か帰納法がどこで回ってるか微妙で微妙という感覚があって いっつもこの辺りの問題と近いような遠いような風に思えてしまう。
・Forcing って Scott Domain に似てるのか！ Forcing を今度こそ理解する会を次回開催するときはちょっと気にかけてみよう。
ICFP (会議の方) の Accepted Papers が出てるのに気づきました。
とりあえず "Report on the Tenth ICFP Programming Contest"
って去年のコンテストの
主催者レポート、ってそれはどう ICFP の Paper になるんだろ。
"Efficient nondestructive equality checking for trees and graphs"
が気になる。
R6RS の equals? を循環アリでもちゃんと止めるための巧い手法ということらしい。
"Write it Recursively: A Generic Framework for Optimal Path Queries"
あ、森畑さん松崎さんだ。おめでとーございます。
"Ynot: Reasoning with the Awkward Squad"
は副作用も扱える Coq らしくて気になっているんだけど
全然調べられてないなあ。
…という辺りがパッと見気になりました。