■

ド・ブラン・インデックス

引き続きTAPLを読んでます。 TAPL*1のuntyped*2の実装でムツカシイところは、ド・ブラン・インデックスでした。

6章に詳しくかいてありますが、名前ではなくて環境中の何番目にあるかを持つ事で、宣言していない変数の参照をチェックしつつ、コンパイラが環境をスタック上に取る場合のアドレス計算も出来ます。

その代わり、ソースを読むのが難しくなります。

SECDマシン*3のコンパイル結果はこういう事だったんだなぁと思いました。

(6 2 NIL 3 (1 (0.0) 2 NIL 14 8 (2 NIL 9) (2 NIL 1 
    (0.0) 11 13 1 (1.5) 4 1 (0.0) 10 11 13 9) 5) 13 3 
  (1 (0.0) 2 NIL 14 8 (2 NIL 9) (2 NIL 1 (0.0) 11 13 1 
    (1.4) 4 1 (0.0) 10 10 13 9) 5) 13 3 
:
:
  (2 NIL 2 (4 21) 13 2 NIL 13 1 (0.0) 13 1 (1.1) 4 5) 13 3 
  (1 (0.0) 5) 7 4 21)

SECDマニアのHendersonのコンパイラから引用

untypedの実装で

x\;
(\a. x) (\a. a);

は、(\a. x) (\a. a)のままとかだと、自由変数って感じがわからないじゃないかぁとか。思いました。 値の定義には、関数しかないので、間違いではないと思うのですが。そこで、バインドされた変数も値ってことにして改造して見ればOKってことでバインドされてる、されてると思えます。

fulluntyped*4ででは、変数を複数バインディングして、先にバインディングした値を参照するとContextの長さが変わってるのでエラーになるのは、shiftし忘れだそうです。で、見事に引っかかってしまいました。なるほど。

色々不具合っぽい事が起きた方が、勉強になるんだろうなぁ。

ラムダ計算には詳しくないので、de bruijnインデックス化しないで、タプルとか突っ込んだバージョンを作って見るとより理解が深まると思います。

そこで、de bruijn化されていないラムダ計算を探してみるというか、作ってみれば良いんだなと思います。

型システム入門 −プログラミング言語と型の理論−

*1:TAPL: http://www.amazon.co.jp/exec/obidos/ASIN/4274069117/amazon0ab-22/ref=nosim/

*2:untyped: https://github.com/ilya-klyuchnikov/tapl-scala/tree/master/src/main/scala/tapl/untyped

*3:SECD Mania: http://skelet.ludost.net/sec/index.html

*4:fulluntyped: https://github.com/ilya-klyuchnikov/tapl-scala/tree/master/src/main/scala/tapl/fulluntyped