2020-03-08

De Bruijn index, 壁を越えて新たな壁へ

昨日の記事で述べた2つの問題はどちらも解決したが、さらに新しい壁にぶつかった。

De Bruijn indexの代入処理

ラムダ式の評価を進めるにあたり代入処理が最も重要である。通常の記法では M[x:=N]と書き、これはM中に現れるフリー変数xをNで置き換えるという意味である。例えば、

(f x (g x))[x:=0] = f 0 (f 0)

となる。同様のことがDe Bruijn index記法でも可能である。が、ちょっと直感的でない。M[s]と書き、sは無限になりうる数列N1.N2.N3...の総称である。その定義は、小文字のnをindexとすると

n[N1.N2....Nn...] = Nn
(M1 M2)[s] = (M1[s])(M2[s])
(\ M)[s] = (\ M[1.1[s'].2[s'].3[s']...])
  where s' = s↑1

ここでs↑1はシフトと呼ばれる処理で大雑把に言うとindexを1増やす操作を表す。定義は以下で与えられる:

s↑1 = 2[s].3[s].4[s]....

n[s]がsのn番目の要素を取る働きをするので、s↑1はsから最初の要素を落とした数列に相当する。

これを頑張ってHaskellに実装した。

ClosedでないTermとDe Bruijn index

フリー変数を持つラムダ式をDe Bruijn index記法に変換するのはちょっとむずかしい。フリー変数は勝手に名前を変えるわけには行かないからだ。しかし、De Bruijn indexには名前がない。Abstractionの数より大きな数を持たせればフリー変数を参照したことになるため、何番目のフリー変数がどの名前だったかという情報を追加で返すことにした。また、逆変換時はその情報を使ってフリー変数を復元することにした。

その結果「De Bruijin index->通常の記法->De Bruijin index」の変換はうまく行くようになったが、「通常の記法->De Bruijin index->通常の記法」の変換は失敗する場合が生まれた。次はこれを修正したい。

AtCoderがトレンドに

全く関係のない話題だが、競プロのAtCoderに関する単語がツイッターのトレンドに入っていた。僕は個人の興味関心に合わせたトレンドを無効化しているはずなのだが、こんなプログラマーしか喜ばないような話題が本当に他のツイッターユーザーにも表示されているんだろうか？？？