カテゴリー : Programming

プログラミング言語Grassは正規表現と相性が良い – RANSによるプログラム列挙

僕のポスター「正規言語の列挙:プログラミングへの応用」はこんな感じです.テックちゃんが右上に居るのがポイント!(ぉぃ http://t.co/CNgcCsxo9t
@sinya8282
Ryoma Sin'ya

PPL2013でポスター発表をしてました.

失礼ながらPPLは規模の小さい学会だと思ってたので,実際参加してみて各方面のガチ勢が多かったのが嬉しびっくりでした.

 

さて

PPLでのポスターでも話したネタですが,プログラミング「Grass」の話をしたいと思います.もちろん正規表現ぽい話.

Grassは”W”,”w”,”v”の三文字のみでプログラムを書けるチューリング完全な言語です.イカれてますよね :-)

さて,この言語Grassですが,文法はもちろんきちんと定義されていて

  • app ::= W+ w+
  • abs ::= w+app*
  • prog ::= abs | prog v abs | prog v app*
といったシンプルな文法となっています.

正規表現!!

この文法はBNFで記述されていますが,実は線形文法で書けます.つまり「正規表現で書ける」.
w([vw]*(W+w)*)*
が構文的に正しいGrassのプログラムを表現する正規表現です.シンプルですね.
プログラムの列挙
さて,RANSと言う僕が開発しているソフトウェアがあります.これは正規表現と数を食わせて「長さ–辞書順でその数に対応する受理文字列を返す」というものです.その逆もできます.
凄い点は「文字列から数は線形時間で,数から文字列は準線形時間で計算できる」
さて,プログラミング言語Grassの構文は正規表現で書けます.では,プログラムと数の対応をいくつか列挙してみましょう.

Hello, world

% cat hello.www
wwvwwwWWWwwWwwWWWWwvwWWwwwWwwvwWwwwWwwvwWWwWWWWWwvwWWWwwwwWWWWwWWWWw
WWWWWWwWWWWWWWwWWWWWWWwWWWWWWWWwWwwwwwwwwvwWWWwwwwwWWWWWwWWWWWwWWWWW
WWwWWWWWWWWwWWWWWWWWWwWwwwwwwwvwWWWWwwwwwwWWWWWWwWWWWWWwWWWWWWWwWWWW
WWWWWwWWWWWWWWWwWwwwwwwwvwWWWWWwwwwwwwWWWWWWWwWWWWWWWWwWWWWWWWWwWWWW
WWWWWWwWWWWWWWWWWwWwwwwwwwvwWWWWWWWwwwwwwwwWWWWWWWWwWWWWWWWWWwWWWWWW
WWWwWWWWWWWWWWWwWwwwwwwvwWWWWWWWWwwwwwwwwwWWWWWWWWwWWWWWWWWWwWWWWWWW
WWWWwWWWWWWWWWWWwWWWWWWWWWWWWWwWwwwwwwwvwWWWWWWWWwwwwwwwwwwWWWWWWWWW
wWWWWWWWWWWwWWWWWWWWWWWwWWWWWWWWWWWWWwWwwwwwwvwWWWWWWWWWWwwwwwwwwwww
WWWWWWWWWWwWWWWWWWWWWWwWWWWWWWWWWWWWwWwwwwwvwWWWWWWWWWWwwwwwwwwwwwwW
WWWWWWWWWWWwWWWWWWWWWWWWWwWWWWWWWWWWWWWWwWWWWWWWWWWWWWWwWWWWWWWWWWWW
WWWWwWwwwwwwwvwWWWWWWWWWWwwwwwwwwwwwwwwwwwWwwwwwwwwwwwwwwwwwwwWWWwww
wwwwwwwwwwwwwwwwWwwWWWWWWWWWWWWWWWWWWWWwvwWWwwwwWWWwwwwwwwwwwWWWWwww
wwwwwwwWWWWWwwwwwwwwwwwwwWWWWWWwwwwwwwWWWWWWWwwwwwwwwwwwWWWWWWWWwwww
wwwwwwwwwwwwwwwwwwvwWWWWWWWWWWWWWWWWwwwwwwwWwwvwWWWWwwwwwwwWWWWWwwwW
WWWWWwwwwwwwWWWWWWWwwwwwwwwWWWWWWWWwwwwwwwwwwwwwwWWWWWWWWWwwwwwwwwww
wwwwvwWWwWWWWWw
これは「Hello, world」を出力するGrassプログラムです(こちらから拝借しました).イカれてますよね.
このプログラムはGrassの文法的に「何番目」のプログラムなのでしょうか?RANSがあればお気軽に計算出来ます.
% cat hello.www | rans 'w([vw]*(W+w)*)*' --tovalue
16276174481634706127730787006880531370466380062973401969614529593658
83958803429956101907280299748822841594957446604850712567590269550047
04442396791176156604038955035748328503682524926066804754823248092598
88431440137005387911828231622152001940020161961290610781750518034051
89101265159339318336722855919281300746470264479856011884839769266736
50505379491629371259037681514934225197925358244649970308443675866436
6464026061342507810037583

などという10進数400桁以上の巨大な数が出てきます.ちなみにRANSは凄いので0.1秒程度でこの数が求まります.

百億番目のGrassプログラム

では逆に,「キリの良い数」に対応するプログラムを生成してみましょう.
「百億番目のGrassプログラム」は何か?簡単です.
% echo '10000000000' | rans 'w([vw]*(W+w)*)*'
wwWwvWWwwwwvwvwvWwvwWwwvv
さて,これは何を出力するプログラムでしょうか?実は
% echo '10000000000' | rans 'w([vw]*(W+w)*)*' > hoge.www
% ./yagi.rb hoge.www
w
なんと!「w」を!出力するプログラムなんです!
「百億番目のプログラムがwを出力する」なんて,Grass凄い.どこまで草を生やすんだ.
(yagi.rbはrubyによるGrass処理系実装です.まめめもさんから拝借しました.)

ちなみに

PPLではGrassの開発者である上野先生が参加されていて,この記事に相当する話をしたら.
え,文法は正規なんですねwww これは面白いwww
などという予想外の反応をされました.「文法が正規なのは意図してなかったのかよ」というオチです.面白いですね.
チューリング完全なプログラミング言語で,文法が正規言語のクラスなモノなんて恐らく他にあまり無い?と思うので,Grassは正規表現と相性が良いと言ってOKでしょう(ぇ

RANS使いましょう

このように,RANSを使えば色々なことができます.今回はGrassという面白いネタを扱いました.
ソースコードも公開していますので,皆さんも是非RANSを使ってみて下さい.

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

たらいよ, とまれ!

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 を使って証明してたりする感じ. 面白い. ふーん, 一般化たらいは止まらないのか.

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

C++ 始めました.

色々な事情から

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

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

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

ということで

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

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

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

 

こんな感じ

C++積んでみた

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

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

おいおい”入門”だぜ?

ってことで:-)

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

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

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

 

SICP Reading #20 [3.1 ~ 3.2.3] 局所の入れ物としてのフレーム

院試/学会が無事終了したということでSICP勉強会再開.
2章の残りをまとめるのがメンドクサイのでそのまま3章に突入するなど :-p

環境/フレーム

SICPで定義されるScheme処理系では, 式の評価に必要な変数(名前)と値の対応を格納してる環境という構造があり, 環境はさらにフレームで構成される.

たとえば, 式

(define (square x)
        (* x x))

を実行した時の環境を考えてみると.

のような図で説明することができるとのこと(SICP表記とはちょっと変えてるけど).

(define (square x)
  (* x x))

をもうちょっと詳しく考えてみると, これは

(define square
  (lambda (x)
     (* x x)))

の syntax-sugar なので, すなわち.

defineは

現在のフレームに 名前と値 の対応を書き込む.

lambdaは

関数のオブジェクト(クロージャ)を返す. オブジェクトはlambda 実行持の環境の参照を持つ.

lambda 実行時の環境への参照を持つというのがミソで, これがすなわちレキシカルクロージャーってことかな.

内部定義とかでは, このフレームが連鎖してくとのこと.

ここまでわかれば, 問題も楽勝.

問題 3.10

手続き make-withdraw が以下のように与えれた場合.

(define (make-withdraw initial-amount)
  (let ((balance initial-amount))
    (lambda (amount)
      (if (>= balance amount)
          (begin (set! balance (- balance amount))
                 balance)
          "Insufficient founds"))))

次の式を実行した時の環境構造を示せというもの.

(define W1 (make-withdraw 100))
(W1 50)
(define W2 (make-withdraw 100))

まず

make-withdraw の定義文の syntax-sugar を剥ぎ取る!! (わかりやすくね.)

let は ((lambda でクロージャを作って) 適用する) syntax-sugar.

(let ((<var> <exp>)) <body>)

((lambda (<var>) body) <exp>)

また, define の syntax-sugar も剥ぎとると, make-withdraw の定義は

(define make-withdraw
  (lambda (initial-amount)
    ((lambda (balance)
       (lambda (amount)
         (if (>= balance amount)
             (begin
               (set! balance (- balance amount))
               balance)
             "Insufficient funds")))
     initial-amount)))

となる.

(lambda (initial-amount) ~~) が実行されると, 大域環境を環境に持ったクロージャが返る. それに対して defineで make-withdraw という名前で環境に書き込む. この時点での環境構造を図で表すとこんな感じ.

lambda と define のここの役割がわかれば, 簡単.
この調子で問題をといてみる.

W1を定義

微妙に説明してなかったけど, 関数オブジェクトに引数を与えるということは, 引数に対応するフレームを追加し, 関数オブジェクトのコード本体を実行するということなので, initial-amount が載ってるフレームが新規に作成される.

ここで

make-withdraw に対応した関数オブジェクトのコード部分

((lambda (balance)
       (lambda (amount)
             <body>)))
     initial-amount)

では, 度のlambda が実行される. しかも, 1度目のlambda は名前がつけられないまま適用される!! (その結果として評価されるべきlambda 式が返る)

結果を図にしてみる.

ここで,

  • フレームE1は, (make-withdraw 100)という関数実行持に作られたフレーム
  • フレームE2は,名前もつけられないまま実行された (lambda (balance) ) を initial-balance を引数で実行した時に作成されたフレーム
  • (W1 50) を実行してみる

    (W1 50)を実行すると, W1に対応する関数オブジェクトのコード内部で, (set! balance ~) によって balance の値を書き換えるる. ここで, 「balance の値を書き換える」とは, フレームをたどって, balance に対応する値を書き換えるということなので, 結果は

    と, 構造は変わらず, フレームE2の balance の値が変更される.

    W2を定義

    ここで, もうひとつの講座オブジェクト W2 を作るとどうなるのか? と言う問題.

    (define W2 (make-withdraw 100))

    W2を上記の式で定義すると, W1と同様のプロセスを辿る. ここで重要なのは, 生成されるフレーム(環境)は別ということ.

    図で注目する点として,

    1. W1, W2 の関数オブジェクトは, それぞれ異なる環境への参照を持ってる.
    2. W1, W2 の関数オブジェクトは, コード部を共有してる.

    1点目が, W1, W2をそれぞれ別のオブジェクトとして扱える基礎となってるのは言うまでもないですね.
    2点目に関しては, SICP 「処理系の実装による」と注記されていた. (この辺は5章でやるのかな?)

    今回は

    Scheme の実行モデル, クロージャ, 再代入…. いろいろ開眼した気がする.
    *複雑なので図にミスあるかも >< 指摘, 訂正大歓迎です.

Python で Turing-Machine シミュレーター

僕が今読んでいる計算理論の基礎では Turing-Machine が登場してきます.

Turing-Machineによるアルゴリズムは, 非直感的で, 人間が記述や動作のシミュレーションをするのは骨が折れます(まじで). ということで, Turing-Machine のシミュレーターを Python でサクッと実装してみました.

コード

 

動かしてみる

“0” が 2の乗数個分続く文字列(ex: “0”, “00”, “0000”..)を認識するTuring-Machineを作成してみます. 遷移関数は Python の辞書で手抜き :-p

def is_power_of_two_of_0(str, dump):
delta = {'q1':{'_':('qreject','R'),'x':('qreject','R'),'0':('q2','_','R')},
'q2':{'_':('qaccept','R'),'x':('q2','R'),'0':('q3','x','R')},
'q3':{'_':('q5','L'),'x':('q3','R'),'0':('q4','R')},
'q4':{'_':('qreject','R'),'x':('q4','R'),'0':('q3','x','R')},
'q5':{'_':('q2','R'),'x':('q5','L'),'0':('q5','L')}}
turing_machine = TM(delta, 'q1', 'qaccept', 'qreject')
turing_machine.dump = dump
return turing_machine.does_accept(str)

これを実行してみると,

&gt;&gt;&gt; import turing_machine
&gt;&gt;&gt; turing_machine.is_power_of_two_of_0("0000", True)
'q1'0000
_'q2'000
_x'q3'00
_x0'q4'0
_x0x'q3'_
_x0'q5'x_
_x'q5'0x_
_'q5'x0x_
'q5'_x0x_
_'q2'x0x_
_x'q2'0x_
_xx'q3'x_
_xxx'q3'_
_xx'q5'x_
_x'q5'xx_
_'q5'xxx_
'q5'_xxx_
_'q2'xxx_
_x'q2'xx_
_xx'q2'x_
_xxx'q2'_
_xxx_'qaccept'_
True

ちゃんと認識されてますね(良かった).

Twitter の TL上でbrainfu*k処理系を実装するのがが流行ってるっぽいので, 自分も一枚噛んでみようかなぁと思ってたり. とりあえず Turing-Machine シミュレーターから実装してみたのでした.

 
Better Tag Cloud