TaPL読む４
前回が4/25で眩暈しそう。半年以上前…（2回目）
文脈（あんまりこの言い方好きじゃないけど…）について、最初から記号のリストを作るのは面倒だったので、都度記号を追加する方法をとった。その時に束縛変数と自由変数で分けて行ったが、自由変数のde Bruijnインデックスがころころ変わってほしくないので自由変数はリストの後ろに、束縛変数は直近のものが最小のインデックスを持つのでリストの先頭に付け足すようにした。
少し違うかもしれないが
のローカル変数の考え方がde Bruijnインデックスと似てるような気がして面白かった。
名前付き項に戻すときについては束縛変数を自分で生成する必要があって、Haskellで文字をランダムに選ぶのは面倒に感じたので、de Bruijnインデックスをそのまま文字に変換した。こうすると変数記号に数字を使った場合にremovemane->restorenameの結果が困ったことになるが、一般的に変数に数字は使わないのでいいことにした。
Stateモナドを使うとき、まず状態を受ける関数で書いてみてからdo式に置き換えるようにしてみたが、結果ラムダ式まみれになってしまった。これでいいのか…？
ラムダ計算における代入の構文をどうしようかと思ったけど、代入はラムダ抽象が適用されたような式の簡約に出る操作のことなので、新たに構文を考える必要はなかった。すでに今のパーサーでも混乱してたのでこれ以上複雑にならなくてよかった。
代入における束縛変数の書き換えや変数捕獲の解決として、5章のアルファ変換によるものが出た。前者はde Bruijnを使うと起きない（気がする）が後者の解決としてシフトによる項の付け替えがある。アルファ変換によって束縛変数の名前を変える代わりにシフトの足切りによって束縛変数の名前を（実効的に）入れ替えてる。de Bruijnレベルを採用すると代入時のシフトを考えなくてよさそうだけど、結局ラムダが消費されるときにインデックスをまとめて下げる必要がありそうなのと、束縛変数と自由変数でシフトの扱いを変えないとだめなので、de Bruijnインデックスのほうが楽なのかな（もし逆が採用されてたら逆のことを思ってそう）。
シフトが実質d=1で打ち切り数c=0のものしか使われなかったり、代入も代入先項=0しか興味がないの、後者2つは実装の都合だけど、シフトの任意性はどこかで使うのかな、手間は変わらないけど…と思ったらベータ簡約でシフト-1があった。
7章で代入のシフトを最後にしてるけどこれで効率が変わるの？それともシフトと実装の共通化を図ってるのかな、確かにこうするとTmVarについての変換だけ定めたらあとは自明になるので、項について置換操作として共通化できるのか。後で楽になるらしいけど、25章まで続ける自信がないので放っておこう。
評価の部分が明示的には網羅的でないパターンなので難しかった。Haskellでやってるけど、ガードはあくまでBool式を並べるのでcaseのパターンマッチとうまく並んでくれずきれいにできなかったので、実際にやる手順を想像して手続き的に書いた。
小ステップのほうが今のところ難しいところがなくて楽な気がするけど、大ステップのメリットって何があるのかな。
4章や7章の実装をあまり参考にしないようにしていて、そのためにinfoのような解析用の補助変数を組み込んでいないけど、これは後々問題になるんだろうか。表示にあたってのremovenameで除去した名前の扱いの実装は正直ちょっとよくわかってないけど、せっかくなら導入したrestrorenameを使ったらいいのに。
次から型の話らしい。そういえば本のタイトルは型システム入門でしたね。ラムダ計算入門だと思ってた。
ところで7章終わりに「実装したからといって、理解したとは限らない。」と書いてあった。そんなこと言わないでよ…確かに演習問題を解いてないけど…
