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

たらいよ, とまれ!

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

C++ 始めました.

色々な事情から

C++製の正規表現エンジンを書くことになりました.

(実を言うと大学3年の時に, 学科のプロジェクトで3D格闘ゲームを作成したことがあるんですが,, そいつは *C++*製, ライブラリにOpenSceneGraph を使っていました. 規模的には3000行ぐらい.

とりあえず C++ の知識やデザパタ, エフェスタ(effective style) に関してなんにも知らない.

ということで

技術書に頼ることにしました. といってもまるっきり素人向けだと読むのがたるいし時間も勿体無いので

  • 各言語共通ではなく, C++ に特化した良書
  • TL上の C++er さんたちが推してる良書
  • C++ の仕組みが分かる良書

に絞って選んだつもり(しらんけど.

 

こんな感じ

C++積んでみた

C++はピアソン・エデュケーション一強?

ここらへん に比べると「まだまだ積み込みが甘い!」と言われそうですが,

おいおい”入門”だぜ?

ってことで:-)

エンジンの実装と並行して読み進めるのが良いか, ある程度読んで実装に進むのが良いか…

とりあえずは C++製エンジンのRE2 のコードやら上の本等読み進めて行く感じで. (大丈夫か?

Russ Cox 先生なら素晴らしいコードに仕上がってるはず!!!

 

PCREは無限の括弧の対応が取れる ~ 再帰も、ネストも、あるんだよ.

追記
ご指摘があり, どうやらPCREはPerl互換正規表現エンジン実装の1つに過ぎないということでタイトルは正確には「Perlの正規表現は無限の括弧の対応が取れる」かもしれません.

こんなの絶対おかしいよ

はい. PCRE すごいです.

僕が正規表現と戯れ始めたのはちょうど1年前. その時, 最初に @shinji_kono 先生に賜った 言葉が

正規表現は たかが 括弧の対応が取れないんですよ.

もうちょっと正確にいうと, 正規表現では

  • (a)
  • (((a)))
  • ((aaa)((bbb)((cc)(d))))
  • (()(()())()(()))()()

のような任意のネストを認めた開き括弧と閉じ括弧の対応がとれない.

というのも, 開き括弧を読み取った時点で, それに対応する閉じ括弧が現れるまで開き括弧の個数 を覚えて置かなければならないからです. 正規表現は 有限 オートマトンで認識できる言語しか表現できないので, 任意個(無限)の括弧に対応した 有限 オートマトンは作れないという話ですね. (もっと強力なプッシュダウン・オートマトン なら可能ですが.)

 

 

ところが

タイトルの通り, PCREさんだとそれが可能です(Perl 5.10からだそうです).

 

(?R)

という構文が正規表現に拡張機能として導入されており, これは パターン全体 を表現するそうです. つまり,

パターンの内部にそのパターン自身を埋め込める

はい. 再帰ですね. PCRE の manual では,

This PCRE pattern solves the nested parentheses problem (assume the PCRE_EXTENDED option is set
so that white space is ignored):

\( ( [^()]++ | (?R) )* \)

という正規表現が紹介されており, この正規表現は空白を無視すると

  • まず, 開括弧にマッチ
  • 続いて
    • 括弧以外の文字列にマッチ(++は貪欲なマッチングで, バックトラックを行わない. これもPerl5.10からの新機能)
    • もしくは, 全体のパターンにマッチ(再帰).

の0回以上の繰り返し.

  • 最後に閉括弧にマッチ.

短いのに恐ろしい記述力ですね. (てか初見じゃ意味不

これで 括弧のネストに対応できる! 再帰で! 1

 

つまり

正規表現2パーサーが書ける じゃないか! と, 思ったら 404 Blog Not Found で既に紹介されていました. (さすが正規表現フェチ ;-)

perl – parser書くならgoto

こちらは (??{ code }) という正規表現にコードを埋め込む, 動的正規表現という機能を使ってますね.

正規表現好きということなら, Perlの正規表現はしっかりチェックしないといけないなぁ. (強烈…)

http://perldoc.jp/docs/perl/5.10.0/perlreref.pod

 

 

おまけ

今日はじめて知ったんですが,

% man pcrepattern

とすると, PCRE の syntax manual が読めます(OS X だと標準で pcre が入ってます). これは便利. というかこれで今回の再帰構文も知りました.

ちゃんと読んでみよっと.

 

 

Footnotes:

1 もちろん 無限 というのは記述力的にという意味で, 実際はスタックの制限で再帰マッチングにはかぎりがあるのですが. (ツッコムのは野暮です:-p

2 もちろん,PCREの拡張を使って.pureな正規表現ではないですね.

 

 

サイボウズ・ラボユースに採択されました.

【サイボウズ・ラボユース】第一期メンバー募集〆切は来週の月曜日4/18です!応募手順も簡単にしましたのでぜひtryしてみてください。http://labs.cybozu.co.jp/recruit/youth.html
@takesako
TAKESAKO

採択されました:-o

内容は 正規表現エンジンの実装,高速化 ということで.

もちろん, プロジェクトの成果は公開していく方針です. まだユースでの開発は始まっていませんが, 現段階での成果物は regen という名前でgooglecodeで公開しています.

  • Regen/gengrep
  • Regen は正規表現コンパイラ,ジェネレータです. 現状では正規表現からC言語やDOT言語で記述されたソースコードを出力することができます.
  • Regen で生成したコードを基盤とした GNU grep ライクな テキストファイル検索が使用可能です. gengrep.py というスクリプトが grep フロントエンドです.
  • Regen はUTF-8なマルチバイト文字列の正規表現検索に対応しています.

とりあえず

  • うれしい! うれしい!
  • 積極的に行動しプログラマーとして成長していきたい
  • 成果を出してユースに貢献したい
  • とりあえず C++ 勉強しなきゃ <- ぇ
  •  

     

    経緯

    eXtreme HAGO LT という沖縄でのイベントで, 僕の卒論成果としての正規表現エンジン/grepの発表(自慢)をしました. -> (ust : 25分ぐらいから僕の発表です. 絶妙のタイミングで僕のBOSSが途中入場してきたりして盛り上がりましたw)

    発表資料を公開 していたら @takesako さんが興味を持ってくれ, 「そのネタでラボユースに応募してみては?」 と. 4月から東京に出てきた僕にとっては最高の誘いだったので応募した感じです. (イベントには参加するものですね ;-)

     

     

    これから

    今現在実装されている正規表現エンジン/grep について

    • 機能拡張
    • 性能向上
    • どのようなケースで役に立つものを作るか?

    といった事を 真剣 に考えて, 開発を行っていきます. (もれなく @herumi さんの熱血指導がついてきてくれるそうです.

     

    開発以外でも

    サイボウズはスーパーハッカーの巣窟 です. そんなメンバーさん達とtechな会話ができると思うと胸が熱くなります. 仕事を邪魔しない程度に絡んでいけたらなぁ, と思います.

    話のネタも考えておかなくちゃ:-p

     

    おまけ

    サイボウズのキャラクター, ボウズマンとの記念撮影.

     
    Better Tag Cloud