SECCONハッカソンで正規言語の話をしてきた

つくばでの

エキサイティングな1日半が終了しました。記憶に新しいうちに記事に。

ハッカソンについて

「2日という短い時間制限」な状況でのプログラミング・イベント、時間制限がある状況でのプログラミングは嫌いなのですが、 先日公開したRANSの応用について考える良い機会と思い参加しました。声をかけてくれた実行委員 @takesako さんに感謝。

さて、僕は「正規言語とパスワード生成」というタイトルでハッカソンの期間で

  • URL(任意)と秘密正規表現(自分で選ぶ: 固定)からオリジナルなパスワードを自動でつくる仕組み
  • RANSの Python wrapper (using SWIG)

を作り、なんとか発表にこぎつけました。RANSについて次の記事あたりで紹介したいと思います。

RANS(C++) Python wrapper の作成には SWIG を使いました。とても便利なツールですぐ wrapper が動いたので、資料作りに時間をかけれたのが嬉しい。 プレゼン資料はSpeaker Deck に挙げておきました。

セキュリティばりばりな方からマジで非常に面白い着眼点・アイディアを得られたりしました。最初はネタ扱いでしたがかなり面白いかもしれません。考えてみる。

CTFについて

ハッカソンとCTFは別室で並列に行われていたので、終始感染していたわけではありませんでしたが、学生さんたちがもくもくと問題を解いている姿は<del>少し引きました</del>すごかったです。 結果はつくば勢の1,2フィニッシュと流石な感じでした。

最後に

SECCONに参加して嬉しかったことTOP3を列挙します

  1. @ucq 君が人間であることを確かめれた(「ボット」「概念」「情報思念体」と思っていました。割りとまじで)
  2. @super_rti 伯爵(まじ)に謁見できた
  3. ちぃちゃん.ぺろぺろ.jp正規表現.ぺろぺろ.jp が取得できた。これは @ym405nm さんの ぺろぺろ.jp というサービス。

@super_rti 伯爵は一見ネタキャラっぽいですが、未来の部屋(音声認識で荷電制御)Regexp::Assemble for PHP, sexyhook 等いろいろハイレベルなことをやってるスーパーハッカーでした。「//コメント至上主義」怖い。

ハッカソンで一緒に行動させて頂いた @suma90h, @ucq, @super_rti, @ym405nm, @takuho_kay (敬称略)。 皆さん非常に濃ゆくて面白いメンバーで夜の議論も大いに盛り上がりました。楽しかった。 #そして筑波の夜は更けていく

サイボウズ・ラボユースっていいよね!

この記事はサイボウズ・ラボユースの紹介記事です.

サイボウズ・ラボ 中谷さん(@shuyo)の記事「 サイボウズ・ラボユースって知ってる?」を引用する形で,ラボユース生視としての所感を基に書いてみました.

サイボウズ・ラボユースとは

サイボウズ・ラボユース

今後の研究開発の発展と世界に通用する日本の若手エンジニア育成のため、有望な中高生、大学生を集めた「サイ ボウズ・ラボユース」を設立することといたしました。

ラボに採択された学生さんは,スーパー技術者集団サイボウズ・ラボの支援を受けながら,自分の好きなプロジェクトを進めていきます. 近く ラボユース最終成果報告会 にて,僕を含む第一期メンバーの成果報告が行われます.

僕は「世界最速の正規表現JITエンジンの実装」というタイトルで,ユースでの一年間,開発してきた正規表現エンジンのお話をします. プロジェクトの成果物である正規表現エンジン Regen(レーゲン)は githubにて公開 しています.

ユースの中身

ユースに採択された学生は,サイボウズ・ラボで,つまりラボメンバーの近くで開発に勤しみます.

サイボウズ・ラボユースって知ってる?

サイボウズ・ラボユースで「何をやってもらう」か。 実は設問がすでに間違っている。ラボユースは「やってもらう」ところではなく、自分から「やりたいこと」をやるところ。 サイボウズ・ラボはなんというか放置プレイが得意な会社で、何も言わないと何も言われない面があったわけだが、ラボユースもその血を脈々と受け継いでいる。

基本的には,ユース生から議論を持ち込んで,ラボメンバー勢がそれに全力で応じるという感じです.そして,ユース生は議論を糧に開発を行います!

特に僕の場合は,サイボウズ・ラボ 光成さん(@herumi)にx86最適化周りでと〜ても多くのモノを叩きこんで貰いました. また,「正規表現」というテーマについても,数学や言語について深い知識を持つメンバーさん達と興味深い議論が絶えませんでし た(数学は共通言語ですね :-) ).

サイボウズ・ラボユースって知ってる?

それぞれが深い専門知識を持つ幅広いメンバーが集まっており、少し頭を悩ませるような問題でも一緒に考えればだいたい解決 への道が見えてくる。ブレストとかすれば、分野横断したいろいろなアイデアがきっと出てくる。若干手前味噌だがw

長い期間,ラボメンバーさん達と近い距離で(それこそ一緒にランチを取りながら),議論ができます.僕自身日々の議論から得たものは多く, ,それを学会発表(学生奨励賞受賞)という形にすることもできました.

口頭以外での議論や情報共有は,サイボウズLive (Web上のコミュニケーションツール)上で行われます.ここでは,プロジェクトを 横断したユース生同士の議論も盛り上がりました.

宣伝

この記事では僕のプロジェクト「世界最速の正規表現JITエンジンの実装」について内容には触れませんでした. 先にも述べたとおり,3/26(月)秋葉原での ラボユース最終成果報告会 にて詳細な報告が行われるので,是非聞きに来て下さい. プロジェクトはザラッと

  • 桐井祐樹「Ruby・Raccを使用した言語処理系の日本語プログラミング化」
  • 新屋良磨「世界最速の正規表現JITエンジンの実装」@sinya8282
  • 林 拓人「型システムの拡張と型推論」
  • 鈴木勇介「世界で一番仕様に忠実なJavaScript処理系の作成」
  • 粟本真一「現役高校生の考えるクラウドOSの設計と実装」

という感じになっています. (「世界」を冠したタイトルが2つもある! :-) )

どれも面白く,志の高いプロジェクトです.

個人的には鈴木くんの発表が楽しみで仕方がない.彼は凄い(笑),もちろんプロジェクトも.

二期生の募集も

また,成果報告会ではラボユース二期生の募集説明会も行われます.やりたいテーマを持った学生さんは,参加の一択ですね. 改めて見てみると,第一期メンバーは比較的低レイヤーなプロジェクトが多い!第二期はどんなプロジェクトが揃うんでしょうか.

さぁ,この記事を読んだ学生さんは今すぐ参加登録 をするんだ!

正規表現でSATを(完全に)解こう!

SATを解きましょう

Augurio Buonanno! 正規表現でやってみたシリーズ第一弾(?)です. SATを解きましょう. → 充足可能性問題

変数の組み合わせ to 正規表現

まず正規表現で問題を扱うには, 対象を文字列にエンコードしなおす必要があります.

X1,X2,…Xnなn個数の変数を真を1, 偽を0と解釈して並べると

/[01]{n}/ #これは(0|1),「0または1」のn回繰り返し

で変数の組み合わせを表現できますね. つまりn文字の2進列に対して

  • n番目の文字が1<->Xnは真
  • n番目の文字が0<->Xnは偽

とするわけです. よしよし, 変数の組み合わせは攻略しました. あとは論理式を正規表現に直せれば良いわけです.

論理式 to 正規表現

Wikipediaにある具体例を標的にしましょう.

まず第一節目について考えてみます. X1かX2が真な節. 正規表現でも or, ∨ (= |) が使えるので

/(1[01]|[01]1)/

と書くことができます. そうですよね, この正規表現にマッチする文字列は

  • 11
  • 10
  • 01

ですね. この節だけ限定して考えればこの文字列は論理式を満たす変数の組み合わせ「X1かX2が真」です!!

問題は and, ∧ です. しかし and 演算(どちらの正規表現にもマッチする)は正規表現の能力を超えていないので認めちゃいましょう. そうすると先の論理式全体は, 正規表現

/(1[01]|[01]1)&(1[01]|[01]0)&(0[01]|[01]0)/

と記述できます. ね, 簡単でしょ?

この「正規表現にマッチする全文字列」は, 先の「論理式を充足する変数の組み合わせ」に一対一対応します.

実質, 変数の組み合わせを文字列にエンコードした時点で仕事は終わっちゃいました ;-)

正規表現 to 受理文字列

理屈だけ納得してもつまらないですよね. 「どこが”完全”に解いてるの?」「普通の正規表現には’&’無いじゃん!」みたいな.

ということで宣伝にもなっちゃいますが, 僕の作ってる正規表現エンジン Regen ではなんと

  • 正規表現にマッチするテキストの生成
  • &, !(not), &&(xor) 演算

に対応しています.

Regen 内の正規表現ツール recon で上述の正規表現(論理式)にマッチする文字列を全列挙してみましょう.

SHINYA% ./recon -E -t '(1[01]|[01]1)&(1[01]|[01]0)&(0[01]|[01]0)'
10
SHINYA%

10はX1が真, X2が偽なので上述の論理式を充足しますね! 充足不可能な式は?

当然なにも出力しません.

SHINYA% ./recon -E -t '(1[01]|[01]1)&(0[01]|[01]1)&(1[01]|[01]0)&(0[01]|[01]0)'
SHINYA%

生成するテキストは正規表現が受理する全文字列(後述)なので, 充足する変数の組み合わせを全列挙してくれます.

SHINYA% ./recon -E -t '(1[01]|[01]1)'
01
10
11
SHINYA%

正規表現, 楽しいですね :-)

補足

正規表現でのand

形式言語的な意味での拡張正規表現(Extended Regular Expression)は, 正規表現に’&’(積集合演算)と’!'(否定演算)が使えます.この拡張正規表現は正規表現の能力は超えません(記述の複雑さは変わりますが). 否定の正規表現の話題はshibuya.pmでも発表しました. 否定とorさえあればandもできますね.

Regenについて

この記事で紹介したツールは Regen をインストールすると使えます(ちなみに「レーゲン」と読みます. ドイツ語カッコいい.). githubから取ってきて使ってやって下さい.まだ色々実装が足りないので資料など皆無(コマンドのヘルプすら!)ですが,

% git clone git@github.com:sinya8282/Regen.git
% cd Regen/src
% make recon REGEN_ENABLE_PARALLEL=no REGEN_ENABLE_XBYAK=no
% ./recon -h
USAGE: regen [OPTIONS]* PATTERN
Regex selection and interpretation:
  -E   PATTERN is an extended regular expression(&,!,&&,||,,,)
  -f   obtain PATTERN from FILE
Output control:
  -t   generate acceptable strings
  -d   generate DFA graph (Dot language)
  -m   minimizing DFA
%

という風に, 今回紹介した生成系は使え(ま|るはずで)す.

(‘-E’ オプションは拡張演算子on, ‘-t’で受理文字列のモード)

他の機能やオプションも説明したいですが, それは次の機会で…(手抜き)

全文字列の列挙?

説明中では「正規表現にマッチする全文字列を列挙」と書きましたが, これは嘘です.例えば

/a*/

みたいなKleene閉包が使われる正規表現は

"", "a", "aa", "aaa",...

と無限の文字列にマッチしうるので, 全列挙は不可能です.

じゃあ, どうするか? (無限はむりでも数を限定すればなんとかなりそうです.)

この辺りは面白い話なので是非次の記事辺りで説明したいと思います!

後方参照でSATを解く

ここでは完全にpureな正規表現でもSATを解けることを紹介しました.調べてみるとPerlなどでお馴染みの後方参照を使って解く方法も解説されてました. まめめも: 後方参照のある正規表現の能力(ただし, 後方参照使うと非正規表現ですよ!)正規表現でSATを解く, 思いついた時にはいかにもありそうなネタと思っていましたが, 検索した範囲で見当たらなかったので記事にしました.正規表現, 楽しいですね :-)

追記

会場で @shinh さんに「Perlなら先読み(?=)あるから/R1&R2/みたいな正規表現は/(?=R1)R2/でいけるよね.」というアドバイスをお受けしました. なるほど.
今回のSATの例も先読みを使えば「SATを充足する変数組み合わせを受理する正規表現」は記述できます.
ちなみに Perlな正規表現の受理文字列生成とかできる module とかあるんでしょうか? (全文字列を生成して通す, というアプローチでなく)
Perlでの先読みは(実装は)オートマトン的ではなく, 再帰を使って実装されています(と思う). ゆえに「先読みってオートマトン理論的にどうなの?」というお話もありますが, このあたりも非常に面白い話なので次回の記事あたりでまとめたいと思います.

たらいまわし関数の停止性

たらいよ, とまれ!

Curry-Howardの対応について調べてたはずなのに, なぜかこの記事 によってたらいまわし関数に興味が出たので.

f(x,y,z) =
 if x <= y then y
           else f(f(x-1,y,z), f(y-1,z,x), f(z-1,x,y))

これがたらい回し関数, 竹内関数とも(あの竹内先生?).

 

場合分けでいけそう?

f(x, y, z) について, 「最小の引数」について場合分け.

case1
x <= y, z 

  1. x <= y なので y を返して停止.
case2
y <= x, z ∧ not case1
fで再帰. それぞれの引数についてさらに考える. 

  1. f(x-1, y, z) : は, x-1=y となる場合 case1(停止). それ以外は case2に帰着.
  2. f(y-1, z, x) : は, y-1 が最も小さい値なのでcase1(停止)
  3. f(z-1, x, y) : は, z-1=y となる場合 case1(停止), それ以外は case3に帰着.
case3
z <= x, y ∧ not case1 ∧ not case2
fで再帰. それぞれの引数についてさらに考える. 

  1. f(x-1, y, z) : は, x-1=z となる場合 case1(停止). それ以外は case3に帰着.
  2. f(y-1, z, x) : は, y-1=z となる場合 case1(停止). それ以外は case2に帰着.
  3. f(z-1, x, y) : は, z-1 が最も小さい値なのでcase1(停止).

 

case2, case3 でそれぞれ帰着が再帰しちゃってる. このままだとだめ.

ただ, case2, case3 の停止性が自分自身に帰着してる場合は停止する, というのも case2-1とcase3-1両方でxの値は常に減少, なのでいつかは x<=y,z を満たし case1(停止) に帰着.

ここまでは割と楽勝, 厄介なのは case2, case3 の相互再帰する場合. むむむ,,, そうだ図を書いてみよう. せっかくホワイトボード買ったんだし ;-)

tarai_args_flow

おぉ, case2のy, case3のz は相互再帰において単に交換しあってるだけでそれぞれ値が不変ではないか!!
かつcase2,3におけるxは常に減少しつづける(再帰が往復して-1)ので, 有限回の相互再帰呼び出しで case2, case3 は x <= y,z に辿り着きcase1(停止)に帰着する.

 

 

停止性が証明できた?

恐らく, これでどのような計算木も網羅して停止することを証明したと思う. 思うのですが.. (思っちゃだめ..?) 間違ってたら ツッコミ お願いします. というかそのためのブログ :-)

追記 たらいは止まってなかった.

コメントにてつっこみがあり, 一番外側の f の停止性を示さなきゃだめでしょと. その通りだ…
ということで再思考中….

 

 

 

なにやら

皆さん一般化して考えたり, Coq を使って証明してたりする感じ. 面白い. ふーん, 一般化たらいは止まらないのか.

証明が知りたいのでとりあえず元論文を読みます.

Shibuya.pm 〜夏の正規表現祭り〜 で好きなこと喋ってきた.

夏だ祭りだ正規表現だ!!

ということで, 行ってきました Shibuya.pm @ mixi

僕はありがたくも「正規表現の限界」とLT・宣伝で「僕の考えた世界最強の正規表現エンジン」と2つの枠で発表させてもらいました.

「正規表現の限界」の方は, 割と皆さん面白いと行ってくれて本当に嬉しかった. 発表するまで「こんなの当たり前じゃん」とか「誰得」とか切り捨てられないかな… とかネガティブループしてたんですが, 発表してみるとやっぱり楽しかった.

計算量だとかアルゴリズム詳細とかは末尾の資料を参照してください. つっこみがあれば修正したいです.

というかつっこみがなくても修正しなくちゃな… チラッと触れて説明してないところ多いし :-)

メモメモ

以下, 心に残った言葉, 印象深かったことをメモ

最後に, 懇親会でこれを聞けて嬉しかった

「キャプチャ"する"括弧こそ特別な表記にすべきじゃないですか?」と @ さんに聞いたら, 「Perlの父 Larry もそこは後悔している」みたいなことを聞けて少しスッキリした. ダンさんも聞きまくったらしいw #shibuyapm
@sinya8282
Ryoma SHINYA

 
Better Tag Cloud