クラッシュなんとか

http://partake.in/events/15125a4e-2c15-4f68-b4a6-32899eb3f91d

οcαmlクラッシュ，会場を取りあえず銀座6丁目のルノアールとして，まぁ開催は確定という形になりました．
（ネット使いたいので，会場が変わる可能性はあるのですがそれにしても常識の範囲内で都内です）

で，少し広めの部屋をとって最小8人最大14人ということになっていて，あと4人は参加して貰えないと飲料代が〜というのありますし，是非参加してくださいませ！

クラッシュシリーズn弾

タイトル通りですが，クラッシュシリーズn弾，
恐らく8月の26日，日曜日で日付がかなり決定に近い暫定となりましたので，こっちにも書きます．

http://partake.in/events/15125a4e-2c15-4f68-b4a6-32899eb3f91d

今回はοcαmlです．

また，例に依ってクラッシュチャレンジ中はググりまくっているので，
インターネッツ出来て良い所がある，
もしくはうちでやると良い，という大変ありがたい情報がありましたら，コメントなどで教えて頂けると幸いです．

アレがチューリング完全になるかどうか

まず決定性2PDSから決定的Turing machineに変形する

2テープTuring machine(TM)への変形が殆ど明らかな気がするので，そこから1テープTMにすれば良いと思いますが．

直接1テープTMにするならば次のようになるのかなーと思います．

まず与えられた2本のスタック(これを便宜上スタック1,スタック2と呼びます)を1本のテープにしなければなりませんが，これは2本のスタックのトップとトップをくっつけるようにし，1本にします．この時，TMのヘッドはスタック2のトップ相当部を指すようにします．

以後，2PDS上のスタックの変化を，このTM上のテープの変化で摸倣していくことになります．この摸倣の中で「だいたい」不変なのは，テープ上のヘッドより左側というのがスタック1に対応していて，ヘッド含む右側というのがスタック2に対応しているということです．

さて，決定性2PDSの遷移の定義というのは，2本のスタックトップのアルファベットの組と，その時点での状態に基づくものになっているというのは良いとしまして．「2本のスタックトップの組」となっていますが，勿論1テープTMでは同時に2つのマスから読むことは出来ません．ヘッドがそもそも1つしかないですし．

まず簡単な例として，2PDS上の遷移で，「スタックトップを見て状態は変えるけどスタックはどちらも変化しない」場合を考えます．
はじめにアルファベットの組による場合分けをTM上でどうするかということを考えます．とはいえこれは全く明らかな方法があって，今ヘッドがいるのがスタック2のトップなわけですから，そのセルを読んで得たアルファベット毎の補助ステートへと遷移し，その際ヘッドを左に動かします．この時のヘッドが指すのはスタック1のトップなわけですから，そのセルを読めば，各々のスタックトップのアルファベットをみたことと同じになるわけで，あとは2PDS側の遷移にならって状態を遷移させれば良いわけです．この時，同時にヘッドを右に動かします．

(先ほど上で「だいたい」不変だと言ったのはこの補助ステートに突入する部分で，ヘッドを左に動かしてしまっているので条件が崩れてしまっているのが分かると思います．ただまぁこの補助ステートに突入するみたいなことが，アトミックにみると無視出来てしまって，外から観測出来るのが，2PDSに対応するTM上の状態に留まっている時だけだと考えるようにすると，条件が保たれていることが分かります．)

以上が2PDS側でのスタックを全く変化させない場合の遷移の摸倣でした．
しかし一般には2PDS側では，各々のスタックトップアルファベットがpopされる，もしくはアルファベットの有限列がpushされることが独立に起こりえます．ということは，TM側で状態を遷移させる前に，こちらもテープを弄ってあげなければいけません．とはいえ，テープはまずスタック1に対応する変形を行い，スタック2に対応する変形を逐次に行えば良いわけですから，
1.ヘッドの指す1文字削除を削除しつつ全体をcompactionする
2.ヘッドの指す位置に文字列を挿入
する2つが出来ればどうとでもなります．でまぁこの1と2の操作というのはTM上のルーチンとして書けますからおk．

従って，2PDS上での全ての遷移をTM上で摸倣することが出来ます．

決定性TMから決定性2PDSへの変形(参考 : オートマトン 言語理論 計算理論II[第2版]の定理8.13)

こちらも割と簡単に出来て．
TMのテープから2本スタックを作る必要がありますが，スタック1を空，スタック2にテープの左端がトップ側にくるようにしてコピーします．
この時2つのスタックが果たす役割というのは．
・スタック1がテープ上のヘッドより左の部分テープ
・スタック2がテープ上のヘッド含む右の部分テープ
となっています．
TMの遷移は，セルを読んで左に動く or 右に動く or 動かずそのセルを書き換えるの3択としても一般性を失いませんから，この各々を2PDS側で摸倣出来るかというかという話に成ります．
まずセルを読んで左に動くのはスタック1のトップをスタック2にpushすれば良いですし，右に動くのはスタック2のトップをスタック1にpushすれば良い話です．動かずにそのセルを書き換えるのはスタック1を触らずにスタック2のトップを差し替えれば良いわけでこれは2PDSの通常の操作になります．

というわけで，TM上での全ての遷移を2PDS上で摸倣することが出来ます．

勿論実際にはテープ上の左方向に無限に続く空白と，右方向に無限に続く空白を考えなければならないのでここまで単純な話ではありませんが，両スタックの底(なので適当に底を表す印をアルファベットに追加して，かつ置いておく必要がある)が見えたら，スタック1の底にたどり着いたら，テープで捉え直すと，ここより左に無限に空白が続いている，スタック2の底にたどり着いたら，テープで捉え直すと，ここより右に無限に空白が続いていると解釈してあげればまぁ上手く行くんじゃないですかね…

StackLangから決定性2PDSへの変形

同じことですけどStackLangから決定性2PDSへコンパイルしましょうという話ですが．
2PDSの1つのスタックを，StackLangのデータスタックにしてあげて，もう1つのスタックを継続スタックというかコールスタックというか…として対応させれば出来る気がします．

TMからStackLangへの変形

今回は，与えられた半無限テープ(semi infinite)を持つTMからStackLangへのプログラムへの変形をしたいと思います．

TMのテープをデータスタックにコピーして来て，でこれまただいたい，データスタックに入っているのがヘッド含む右の部分テープに対応していると考えて．TMから2PDSにする時に書いたように，データスタックが空(というか底印だけが積まれている状態)の時は，TMとしてみるとヘッドの右側には空白が無限に続いていることを表しているとしましょう．

TM上の状態を，StackLangにおける関数に対応させて，状態遷移を関数呼出しに対応させてみます．
で，TM上のヘッドを右に動かす行為をデータスタックのpopに対応させるとすれば，popしたアルファベットはどこに行ってしまうのでしょうか，というのが問題でしょう．
ここをどうとも出来ないと，TM上のヘッドを左に動かすことがにっちもさっちも行きません．

popしたアルファベットを何らかの形で記憶させておかなければなりませんが，StackLangには局所変数すらありません．
しかし，アルファベットが高々有限なわけですから変数を使うまでもなく，場合分けを駆使すれば「何をpopしたのか」が分かります．

つまり

S1(){
  switch( top() ){
  case A:{
    pop(); // (1)
    S2();
   ...
  }
  ...
}

という形にしておけば，(1)でpopされたものがアルファベットAであったことがstate2から戻って来た時に分かっています．やんわりとですがpopされてきた列が，実行の足跡にふんわりと対応しているような気がしないでもありません．

ではヘッドを左に動かすということはどうすれば良いのでしょうか．ある状態S2から別の状態S3に変えつつ，ヘッドを左に動かすわけですが，とはいえS2にはpopされたものは残っていません．

S2(){
  switch( top() ){
  case X:{
    /* ヘッドを左に動かすのに対応した操作をしたい */
    /* でも何をpopしたのか俺は分からん */
    ...
  }
  ...
  }
  ...
}

困ったとなる．取りあえず，次はS3に行きたいという情報(継続)をスタックにpushしてreturnする．

S2(){
  switch( top() ){
  case X:{
    push(S3);
    return;
  }
  ...
  }
  ...
}

さて，戻って来たるはS1の(2)である．

S1(){
  switch( top() ){
  case A:{
    pop(); // (1)
    S2();
    //(2)
    ...
  }
  ...
}

もともとreturnしてきたのはデータスタックにpopしたものを復活させることだったのだから，さっさと戻してあげる．ただまぁ継続が積まれていることに注意して．

S1(){
  switch( top() ){
  case A:{
    pop();
    S2();
    switch( top() ){
    case S3:{
      pop();
      push(A);
      S3();
      //(4)
    }
    ...
    }//end of continuation switch
  }
　case X:{/* これはヘッド位置を変えず，書き換えする場合 */
    pop();
    push(X');
    S4();
  }
  ...
  }//end of alphabet switch
}

とすれば良い．S3に遷移して更に1つ左にヘッドを動かすという事に成った時も，先と同様にS3から(4)にやってくるがこれはそのままS1からのreturnを引き起こす．
別の言い方をすればS3がS1で末尾再帰呼出しになっているわけなので，S3の中からS1のcall siteへjumpするわけで，その(つまりS3の)継続をcallする際には，矢張り，ヘッドは正しく1つ分左に進む．

あとはmain関数をどう実装するか，ですけど

final1(){
  push(◎);
}

main(){
  switch( top() ){
  case A:{
    ...
  }
  ...
  case ◎:{ return; }
  }
  main();
}

のような形に成っていて，この◎は，TMの受理状態に対応する関数(上ではその一つとしてfinal1)の中でこのアルファベットをpushして後はひたすら戻って計算を終了させようというつもりなわけです．

まぁなんか元の設定では停止してかつスタックが空のときなど言っていましたが，別にfinal1の中でスタックを空にすれば済む話なので簡単の為に◎を使いました．

大雑把には上の様な感じで，あとの細々としたところを詰めていけば，与えられた半無限テープを持つTMからStackLangのプログラムを作れたということになっていそうです．

pop + 関数呼出しがヘッドを1つ右に動かすことに対応していて，なので1つ左に動かす操作を上手く行う為にこの関数呼出しは「非」末尾再帰になっています．
末尾再帰になっている時は，ヘッドを動かしません．なので，1つ左に動かすというのがcall先からのjumpになり，まぁなんか上手い事行く様なえーと図があった方が良いなあ．

適当に考えた言語での受理について

先日twitterに

このようなことを書きました．

若干数反応を頂けたのですが，その時は何も考えてなかったのでうんともすんとも言えなかったのです．どうせCFL程度だろとかは思っていたのですが．
しかし，研究室に持ち込んでなんか上手い証明方法とかあるんですかねーなど尋ねたところ，いやこれCFLではないでしょうというヒントを貰ったのでニコニコ動画みながらグダグダ書いたのを取りあえずメモ代わりに書いておきます．

まずDCFLでない例

ウィキピディア（http://en.wikipedia.org/wiki/Deterministic_context-free_language）によると，

For example, the language of even-length palindromes on the alphabet of 0 and 1 has the simple, unambiguous grammar S → 0S0 | 1S1 | ε, but it cannot be parsed by a deterministic push down automaton.

とまぁそうなっているので実際にこの例を受理出来ればよいという話で．

type stack = Bottom | Push of (char * stack)

let stack_from_list l =
  List.fold_right (fun e acc -> Push (e , acc)) l (Push ('Z',Bottom))

let entire = ref (stack_from_list ['a';'b';'a';'a'])

let pop () =
  match !entire with
    | Push (c ,rest) -> entire := rest

let push c = entire := Push (c , !entire)

let top () =
  match !entire with
    | Push (c,_) -> c

let other = function
  | 'a' -> 'b'
  | 'b' -> 'a'

(*
  stackの底の印Zのすぐ上に c があればそれを削除
  もしc以外が存在すれば yabai
  底の印Zが最初から見えていても yabai
*)
let rec del_char (c:char) =
  if top () = 'Z'
  then failwith "yabai"
  else if top () = c
  then
    begin
      pop ();
      if top () <> 'Z'
      then begin
	del_char c;
	push c
      end
      else () (* 1つ先読みして底が見えればそれだけが取り除かれ再構築される *)
    end
  else if top () = other c
  then
    begin
      pop ();
      del_char c;
      push (other c)
    end

let del_a () = del_char 'a'
let del_b () = del_char 'b'

let rec f () =
  if top () = 'a'
  then
    begin
      pop ();
      del_a ();
      f ();
    end
  else if top () = 'b'
  then
    begin
      pop ();
      del_b ();
      f ();
    end
  else if top () = 'Z'
  then ()
  else failwith "yabasugi"

なんかまぁデロデロとこんな感じで書けました．別に証明とかはしてないですが，fを実行すると偶数長回文になっている時だけに，終了後スタックが空（底目印Zだけが積まれている）状況になる気がします．

やっていることは簡単で，スタックトップからボトムに向かって下って行くわけですが，その下る時に，スタックトップの文字と同じ文字がボトム（底Zのすぐ上）に在れば削り，無ければその時点で例外を投げちゃう．
削った後にトップをポップして，底目印Zが見えてくるまでこれを続ける…という具合でうまく行きそう．

CFLでない例

次にCFLでない例として有名な言語{a^n b^n c^n}を受理させます．

type stack = Bottom | Push of (char * stack)

let stack_from_list l =
  List.fold_right (fun e acc -> Push (e , acc)) l (Push ('Z',Bottom))

let entire = ref (stack_from_list ['a';'a';'b';'b';'c';'c'])

let pop () =
  match !entire with
    | Push (c ,rest) -> entire := rest

let push c = entire := Push (c , !entire)

let top () =
  match !entire with
    | Push (c,_) -> c

(*
  スタックトップからみて行って，c2に一致するアルファベットがあれば
  それをc1で置き換える
*)
let rec replace_char c1 c2 =
  if top () = c2
  then begin
    pop ();
    push c1;
  end
  else
    let a = top () in
    pop ();
    replace_char c1 c2;
    push a

(*
  fでは，スタックトップからaの連続している間，底に向かう．
  その間，aをpopしつつ，最も近くにあるbをyで置き換える．
*)
let rec f () =
  if top () = 'a'
  then begin
    pop ();
    replace_char 'y' 'b';
    f ();
  end
  else ()

(*
  yとして置き換わっていないbがあるかどうか調べる．
  これがあるということは，aの連続している長さよりも
  多い数bが存在しているので，例外を投げる
*)
let rec check_b () =
  if top () = 'b'
  then failwith "check_b find b"
  else if top () = 'Z'
  then ()
  else
    let a = top () in
    pop ();
    check_b ();
    push a

(*
  スタックに残っている物が，y^n c^nの形になっているかを
  調べるだけ．
*)
let rec g () =
  if top () = 'y'
  then begin
    pop ();
    g () ;
    if top () = 'c'
    then pop ()
    else failwith "fail in g"
  end
  else if top () = 'c'
  then ()
  else failwith "fail in g"

let main () =
  f ();
  check_b ();
  g ();
  if top () = 'Z'
  then print_endline "accept"
  else print_endline "reject"

やることというのは，a^n b^nというのがスタックのトップ側に出て来ているかを調べて，ボトム側にb^n c^nがあるかどうかを調べるという2段構えのようなものになっています．雰囲気としては{a^n b^n c^m}と{a^n b^m c^m}のintersectionを取る感じなのかなー．それはともかく．

まず関数fでスタックトップからボトムにaが連続する間くだっていくわけですが，その際に最もトップ側にあるbをアルファベットyで置き換えるようにします．
次に，check_b関数でスタックにbが残っているか，つまりyに置き換わっていないbが存在するかを調べます．これはまぁaの連続する出現長とbの出現長が一致しているかを調べているわけです．
で，その後はy^m c^mがスタックトップ側に残っているかどうかを関数gで調べるという手筈です．

すごい適当に書いたので

あとで書き直そう

1から10までの和

メモ

C言語にtimetravel機構がある時（あと実行開始時のスタックトップ位置が予知出来ていれば），const値からの複数回読み込みを許すならば55ぐらいは計算出来そうだぞみたいなことをBoost.Tsukubaの間やっていたのでした．

const struct tuple p = f();

のところはまぁ分かると思いますが，constと字面上（syntaxでは）書いていますけど実行時にはN回のpへの代入が発生していてまぁconstはやはり見掛け倒しだ（極論）

timetravelとか言ってますけど，スタックをコピーしておいてそこまで巻き戻ると言った方が良いのかなんというのか…．
もとは限定継続っぽいのを馴染みよい形で入れればなんとかなるんじゃないかという発想があってだらだら書いてたのですが，結局ぐちゃぐちゃになってしまって全然良く無いですね．あんまそこにとらわれないで，これとこれを使えば上手い事いくからこれとこれが欲しいみたいなゴリ押しストーリーでも良かったかもしれない．