祝・第１０回。（セルフ祝辞）
メイドインアビスの更新が先か本シリーズの更新が先かという様相を呈していましたが、
なんとかこちらに軍配が上がるようです。やっていきましょう。
かいせつ：
メイドインアビスというwebコミックが存在します。
もとより連載半不定期・ゆっくり目の更新頻度の作品ですが、
直近のアニメ化・映画化等の都合からか、現在は輪をかけて本編の更新が滞っている状況にあります。
本記事の記載日2019年07月07日時点での最新51話の更新日が3月30日なため、
本シリーズの前回更新が3月10日であったことと対比して発言をしています。
初手真顔解説芸だよ。
こんにちは、こんばんは。
型システム入門です。Type and Prolgamming Languageです。お久しぶりです。
さて、長らく日が空きました。その中での出来事を紹介しますが、
↑こんなん言ってたら
↑こんなん降ってきた
以上です。
では。第６章「項の名無し表現」です。
～これまでのあらすじ～
定義 5.3.5 代入 [x -> s]x = s [x -> s]y = y // y != x の場合 [x -> s](λy.t1) = λy.[x -> s]t1 // y != x かつ yがsの自由変数に含まれない場合 [x -> s](t1 t2) = ([x -> s]t1 [x -> s]t2)
「代入が出来るようになったで！」
せやな。
項の名無し表現
やりたいこと：「ここまでやったラムダ項、名前ダブるとダルくない？」
あ、なんか脇の問題だ・・・（不穏発言）
「え～～なんかもっと型の捌き方みたいの（何それ）教えてよ～！！」とか言い出しそうですが、
「本題をさっさと進めたい」みたいな気持ちになったら負けですね。そう、これは学問・・・。
で、戻りますが、今回の章は
「識別子を見て『この名前知ってんな』となるロジックを正確に実装をしようぜ」
というのが論の展開方針だと思っています。たぶんそう。
ちなみに１ページめくった時の感想を先に書くと、
「いや理屈知らんけど『じゃあ全部アドレスで指定しますわ』みたいなノリじゃあかんのか？ できるのかしらんけど」
みたいのです。それで済んだらこの本はいらねえ。
君だけの表現方法を選ぼう！
で、名前をダブらせないための方法というのは、いくらか考えられうるようです。はえー世の中の学者かしこいんやな
書籍内では方法が5つ挙がっていて、その中での3つ目が採用されます。内容はこんなん。
(3) 名前を変更する必要がない、変数および項の「標準の」表現を考える
ちなみに他の方法には「(5) もう変数なんつーモンを使うんはやめようや」とかいう(たぶん)過激な方法もありました。名前がどうとかいうレベルの話じゃない。SFの「老いがつらいから肉体を手放そう」みたいなやつだ。
とにかく(3)の方法を採用すると、こんなこと↓になるようです。
原文
変数の出現を、名前を介して参照するのではなく、束縛子を直接指すことによって項を表現するのである。
これは、名前の付いた変数を自然数に置き換えることで達成できる。
自然数 k は、「それを囲む k 番目の λ によって束縛される変数」を意味する。
例えば、通常の項 λx.x は名無し項 λ.0 に対応する。λx.λy. x (y x)は、 λ.λ. 1 (0 1)に対応する。
λ.λ.0
と書くと"内側"=右側のλに対応する変数を返すような関数に意味的に対応していて、
λ.λ.1
と書くと"外側"=左側のλに対応する変数を返すような関数に意味的に対応している
「いやそれ読めんの？」（第一印象）
・いや単純に数数えんのしんどそう
・ラムダの中にラムダいる時どうすんの？
・ラムダ切り抜く範囲？スコープ変えた時？とか上手くいくの？（いきそうではある）
・そういや厳密にはラムダに対して引数は１つなんだっけ(なので複雑度が増しても連番だけで対応が絞り込める)
・はじめ言った「じゃあアドレス指定で」ってもしかして正解なんか？
・ウダウダ良いはしたけどとりあえず成立しそうなのはわかる気がせんでもない
と。
そんで、コンパイラ書き勢はこの採番結果を「静的距離」っていうみたいです。そのニュアンスはわかる（気がする）。
ちなみにこの後「えーじゃあこっから項は数字で表すの？」というと全くそんなことはない。
なんやねんこの例。ちなみに僕はこの数字の表現のほうがわかりやすいとおもいます。
ちなみに「それ読めんの？」はどうやら少し正しいようで、上で引用した部分の手前にはこうあります。
de Bruijnのアイディアとは、読みやすさを犠牲にすれば、項の表現はもっと単純にできるというものであった。変数の出現を、名前を介して参照するのではなく、束縛子を直接指すことによって項を表現するのである。
※de Bruijnのアイディア：(3) の方法のこと
じゃあちょっと定義してみよっか^^
形式的には、名無し項の構文は通常の項の構文（定義5.3.1）とほとんど同じように定義する。
唯一の違いは、各項が自由変数を幾つ含みうるかについて丁寧な追跡が必要になることである。すなわち、自由変数を全く含まない項（0項と呼ばれる）の集合、
高々一つの自由変数を含む項（1項と呼ばれる）の集合、などを区別する。
Tを、以下の条件を満たす集合の最小の族{T0,T1,T2,...}とする。(1)
0≤k<nならばk∈Tn
(2)t1∈Tnかつn>0ならばλ.t1∈Tn−1
(3)t1∈Tnかつt2∈Tnならば(t1t2)∈Tn
ふえぇ・・・わかんないよお・・・
数学弱者たる僕がこの記述から読み取れた気がすることを文字にしますと、
「いろんな項をあつめた集合がおるんやけど、距離が
n以下やったら集合のサイズがnん時にはその項が含まれてるはずやで」
みたいな感じです。自分でも何を言っているのかわからない。
「100より小さい自然数は1～100に含まれてんで」みたいな雰囲気を感じています。あたりまえ体操再生待ったなし。
ああ、ちゃんと言うとなんか逆なんですかね。「1～100」のほうを求めるのがモチベーションですもんねこれ。（定義されているのは{T0,...}のほう）
であれば、こうですか。
「距離が
n以下のときに出てくる項の集合の最小のやつ、Tってことにするわ」
何が嬉しいのかはわからんがさっきよりは実のあることを言っている気がします。ウオオ。
そして(2)を改めて見て思ったのが、なんかこれ3章でやったdepth()に近くない？？という話なのですが、
3章を学習していた当時の記事を確認したところ
「流し読みました。」じゃないんだよ。（身から出た錆）
そして「深さっぽくない？」とは思っているものの、実は
(2)
t1∈Tnかつn>0ならばλ.t1∈Tn−1じゃなくて
(2)t1∈Tnかつn>0ならばλ.t1∈Tn+1な気がするな・・・？（わからん）
とかの感覚もあったりします。ラムダ増やしたら浅くなるんか？え？なんで？みたいな。
つまり、「t1がTnの中にあって、t1 = λ.t2とかの時 t2 が Tn-1 の中にあるよ」って話ならわかるんですけど。なんか逆なんですかね。わからん。
こまかい謎は点在しているんですが、
「目の前にあるなんらかの式が定まった時に考えなきゃいけない範囲」が定義されたんか・・・？と思っています。
それはつまり、さっきの
・ラムダ切り抜く範囲？スコープ変えた時？とか上手くいくの？（いきそうではある）
とかを解決する概念・・・か・・・？という感想。
具体的には、「ここまで値とっといたら目の前に来たこの式は表現できるな」の指標な気がします。
という感じで、なんとなく定義を読んだ感じになりました。
ぶっちゃけ前述の通り「これ読み方あってんの？」のレベルなんですが、
こういうのはだいたい話さえフワっと覚えといたら続き読んでるウチに簡単な話に思えてくるんスよ（暴言）
そしてその「続き」は、また次回であります。第１０回、ここまで。
おわり
ええと、今回は
「名前がぶつかってしんどい」
「ちょっとルールきめて連番で名前つけよか」
「なんか何が嬉しいのかわからん定義でてきた」
という話でした。（強引）
次回またアルファベットに数字を予約（？）したりとかわけわからんことを言い出すんですが、
がんばってやっていきましょう。ちなみに今回の内容は冊子上で2ページ弱です。
ではまた次回。フワっと覚えとかないといけない。
