第１１回。前回から２１日です。３週間。
「週刊型システム入門」くらいになると嬉しいんですけどね。難しいですね。
６章「項の名無し表現」、後半です。
～前回のあらすじ～
「変数の名前、ダブるとわけわかんなくなるね」
「なので、変数の名前の付け方決めまーす」（変数および項の「標準の」表現を考える← やりたいこと）
「ていうか変数にわざわざ名前を付けません」（変数の出現を、名前を介して参照するのではなく～(略)）
「ラムダに対応した番号で呼ぶことにします」
「そんでこの記法をつかった項に関して、こんな定義ができます」（わかってない）
T を、以下の条件を満たす集合の最小の族 {T0,T1,T2,...} とする。
(1) 0≤k0 ならば λ.t1∈Tn−1
(3) t1∈Tn かつ t2∈Tn ならば (t1t2)∈Tn
各 Tn の要素を n 項と呼ぶ。
というかんじでした。（わかってない）
復習
復習というか、ほとんど訂正かもしれないんですけど。
上の定義の件です。書籍中で定義 6.1.2ですね。
前回からフワっと考えたり見直したりしていたんですが、
どうやら上の定義は、「項に含まれる自由変数の数」にフォーカスしたものなようでした。
n: 自由変数の数(種類)
Tn: n 種類の自由変数を持つ項が取りうる値のパターン(式の形)(T2とかT3とかそれぞれに複数の形がある)
定義の式や文字を、勝手に書き下すと、こうなりました。
(1) 項
kの自由変数が０～ｎ個だったら、同じ形の項がTnに含まれる
（根本的な定義）
(2) 項t1がTnに含まれて、かつｎが０より大きい値だったら、λ.t1はTn-1に含まれる
（λ によって 1 つの自由変数が束縛されるため？）（今回採用の記法では、束縛対象でない変数はいない？）
(3)t1がTn内、t2もTn内に含まれるとき、(t1 t2)はTnに含まれる
（横に値が増えても自由変数の種類は増えないため）
ええ。自分でも思いました。「3週間経ってまだハテナあるじゃねえか」
とりあえず今のところ、これで進もうと思います。
前回の自分の発言に従う形。という。ことで。
※前回の発言→「続き読んでるウチに簡単な話に思えてくるんスよ」
自由変数の扱い方
モチベーションこのあたり。↓
例として
λx.y xを名無し項として表現することを考える。
xの扱い方は既にわかっているが、yについては束縛子が見つからず、
したがってこの変数がどれだけ「遠く」なりうるのかわからず、どの数を割り振ればいいのかわからない。
これは確かに問題です。
自分はまた 「えー、じゃあ番号とか言わずにアルファベットのままにしたら良くない？」 とか思ってしまう訳ですが、
たぶんそうはいかんのでしょうね。決めたいのは文法でなくて、論理なのだよワトソン君。数字とアルファベットでは次元が違うだろう。みたいな話だと思います。
で、その方法のアイデアがなんも沸かないところ、ノータイムで例を出してくれます。
「ルールを先に決めちゃって、その数字使おか」とのこと。じゃあアルファベット使うってルールでもいいの？（手のひら大回転）（そうはいかない）
例として、次の名前付け文脈を用いることを考える。
Γ = x -> 4
y -> 3
z -> 2
a -> 1
b -> 0
すると、
x (y z)は4 (3 2)と表現される。
λw. y wはλ. 4 0と表現される。
λw.λa.xはλ.λ.6と表現される。
？？？？ｗｗｗ？？ｗ？？？？？？？ｗ？？？？？？？？？ｗｗｗｗｗｗｗｗｗｗ
１行目以外なんも解んねえやどうすんだこれ
一つずつ行きましょう。まず。
すると、
x (y z)は4 (3 2)と表現される。
これはいいですね。たぶん。上に並んだΓとそれぞれ同じ値です。
ぶっちゃけ実質アルファベットじゃんとかガンマの並びどっから出したとか適当でいいのかとか思いますけど
λw. y wはλ. 4 0と表現される。
「あーうんwが束縛変数だから0になって、そんでyｇａ・・・アァ゛！？
なんだこれ誤植では？とか思ってしまうレベルなんですが。これは何。
何をどう数えたらyが4になるんだろう・・・わからない・・・・・・・・
v,w,x,y,z,a,bでwが0なのにあわせて数えたりしてもyが4にはならん・・・恨めしい・・・。
ていうかどう考えてもアルファベットの並びなんか関係なくあるべきなんですよ。
上のガンマはあくまでただの例と考えるとして、何かが絶対におかしい・・・。
わからんすぎてググりました。
http://ryna4c2e.hatenablog.com/entry/20141023/1414077068
https://bellbind.hatenadiary.org/entry/20071129/1196309781
・・・やっぱ４じゃなくない・・・・・・？
（そして方法論的には、書いてある「自由変数は括られた λ の数+1 から付ける」みたいなやつだと超納得）
λw.λa.xはλ.λ.6と表現される。
はいわかりません。 1 つ前と同じ話だと思うのでそりゃそうなんですけど。
なんだろうこれ、λw.λa.xで言ったら、
「x？ あー(引数リストに無いから)知らん奴だな、1，2(0，1？)は席埋まってるから・・・あー、3 でも 4 でも 6 でも良いや」
とかだったりしますか？ それだとそう書けぶちのめすぞつらいですね・・・つらい・・・。
とりあえず、上に挙げた 2 ブログで当然のように話している
「自由変数は λ の数より多くする」だけだと思っておきます。いきなりフリーダムされるのは・・・つらい・・・。
シフトと代入
さて、式の書き方が定まってきたなというところで、式のイジり方を考えるようです。
(代入のためには、)「シフト」と呼ばれる補助的な操作が一つ要る。
とのことです。さっきググったページで見たやつだ！（やめろ）
しかし、どうやら書籍上に具体例がなくてつらいので、次の「評価」に行って具体的な話を見ましょう。手を動かして理解するんだ。
評価
というわけで具体例。
(λ.1 0 2) (λ.0)を簡約すると、0 (λ.0) 1//1 (λ.0) 2ではない
こんなん。代入先の1，2の値が減ってますね。
要は、「代入とかして式の形(λ の数)が変わると変数の相対位置も当然変わるので、ちゃんと調整しましょうね」の意。
なんだか簡約作業がまたひとつ面倒になるということですね。とはいえ、規則的にできる様子です。
それを表すやたらテキストに起こしにくい式↓がありました。（画像）
これを日本語で読むと、
１．
(λ.t12) v2の簡約は、
２．t12の中の 0 を「v2の全て(0 以上)の変数に 1 を足した項」に置き換え、
３．全て(0 以上)の変数に 1 を引いたもの
となります。
日本語の通りにさっきの例(λ.1 0 2) (λ.0) -> 0 (λ.0) 1を操作してみると、答えが一致するかと思います。
この手順が、今回 6 章で取り入れた「項の名無し表現」de Bruijn index（ド・ブラン インデックス）を用いた、
ラムダ式表現の取り扱い方でした。
ヨッシャア次は実装だぜ！！！！！！！！！
おわり
さて今回は話が進みました。よかった。6 章をなんとか乗り越えることができました。（なお演習回答ゼロ）
ただ、反省を述べると、「今思うと第１０回の存在意義がほぼ無くなってない・・・？」という問題が浮上しています。ひどい。
要するに、第１０回でずっと喋っていた定義6.1.2.の答えは全部今回のほうにあるんですよね。どうしよう、なんか修正するとか注意書き入れるとかしたほうがいいかな。
ログとしては残したい気持ちがあるんですけど。まあまた見直しですね。今日はおやすみなさい。（日曜 26 時前）
ではまた、次回です。
