第５章型無しラムダ計算、３節形式的議論。
この節苦手なんですよね。形式的議論シリーズ。
この節、いつも「お前何言ってんだ」感が強い。（暴言）
クソお久しぶりの更新です。
2月は更新がゼロでした。ヒエッ・・・。
では。
〜これまでのあらすじ〜
「はえ〜ラムダの計算いろいろできるんやな」 「けどここまでのは文字に式入れんの繰り返しただけやで」 「リアル数字とかも入れれんねんで」 「リアル真偽値とも組み合わせられんねんで」 「特殊な構造でさらに意味をみいだせんねんで（？）（再帰のことを言っています）」
こんなん？（浮き足立ってきた）
それで今回は、
「これまで君らが遊んできたその式のパズル、ちゃんと定義洗ってみよか」
です。
ちなみに、
「ちゃんと定義を洗う」行為は
先述の「この節苦手なんですよね」に直結しており、
ぶっちゃけ細かい話全然わからんからカットしたいし、
むしろどうせ全然理解できねえから雰囲気で畳むべきでは
とか思っています。どう考えても丸ごと一ヶ月更新が空いた理由の一つ。
というわけで、書籍内では色々問題提起とミスリードと解決と順序がありますが、ここは一旦結論から投げ込みましょう。
〜型無しラムダ計算の定義〜
構文
t ::=
x // 変数
λx.t // ラムダ抽象
t t // 関数適用
v ::=
λx.t // ラムダ抽象値
-----
評価 // <> ←このやつは書籍内だともうちょい違う記法です
<t1 -> t1'>: t1 t2 -> t'1 t2 // <t1をt1'に簡約できる時>〜的な
<t2 -> t2'>: v1 t2 -> v1 t2'
(λx.t12) v2 -> [x -> v2]t12
最後の奴・・・何・・・？ ※最後の奴：[x -> v2]t12
いきなり出てきて焦りました。書いてる自分も焦りました。
話が逸れ気味になりますが経緯をお話ししておくと、
今記事を書いている３週間くらい前にこの結論の部分の前の「全然理解できねえ部分」を読み進めており、
その部分で[a -> b]この記法を見ていたものの、あまりの無理解ぶりにまんまと意味を忘れており、
「結論からピックアップしたらエエ感じに進むんちゃうか！？」と楽をして進めようとした今になって面食らう、というのが経緯です。
そして書きながら読み戻して冷静を取り戻しました。引用しましょう。P42。
ここで[x -> t2]t12 は、「t12の中のxの自由な出現をすべてt2で置き換えることによって得られる項」を意味する
らしいです。（他人事じゃないんだよ）
たとえば[x -> v2]t12であれば、
「項t12において、xをv2に代入する」と読めます。（そのはず）
（書籍内だと矢印の形が少し簡約のやつと違うんですが置いておきたい）（わかってない）
そんな感じで、戻ってみましょう。
(λx.t12) v2 -> [x -> v2]t12
「たしかに。」
t12の中身が全くの謎なのが意味不明ポイントでしたね。ハァーー数学ゥーーって感じです。どんな感じだ。（抽象化が完全な感じですよ）（伝われ）
いや完全に主観の感想なんですけど、たぶんわかんないサイドで共有される感想はこのへんなんじゃないかな。当ブログは手探りで学問をやっています。
で。
この定義は今回の結論なので、少し逆向きに進んでいきますと、(λx.t12) v2 -> [x -> v2]t12これを安心して書くための努力が数ページに渡って記されているわけですね。
色々仮説や慣習、たとえば「同じ形の式だったら文字入れ替えてもよくない？」(俺はずっとそう思ってるよ)っていうのをきちんと認めたりして、大変な定義を記載していたりするんですね。この５章３節では、次に書く定義を整えるまでに、3種類の仮定をし、どれも「この場合に矛盾が出る」と否定をしてきました。どうせなので書いておきましょう。
定義 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)
そう、「代入の定義」。
「代入の定義」。
いやどんだけ気難しいんだよ数学。
「必要なのはわかるんですけどね、いやそれ・・・うん・・・いや大変ですね・・・ほんと・・・ですよね・・・」みたいな気持ちですよ僕は。「理学というのはそういうもんだよ」を受け入れる気持ちが未だに整ってないの大丈夫か。
いやむしろ逆に、プログラム書く時なんかは「必要なのはわかるんですけどね」の塊なはずなので、自分をコンピュータだと思って読む気持ちとかが大事なのかもしれませんね。（？）（まあ実際そうだよね）（コンピュータがわかるのは数学だよ）（プログラミングは問題を数学で記述可能な内容に書き下すことだよ）（みたいな）（どっかで聞きかじったような）（受け売り）
オチたのかオチてないのか全くわからない散文になりましたが、
たぶん５章３節の内容はだいたい以上です。細かい演習何もしてないや。
とにかく、式の形で型無しラムダ計算が定義できまして、
遂に次の６章ではまた実装のターンです。やってやった。これを楽しみにこの本を開いている。
⇧後日追記：と思ったら実装のターンは7章でした。解散。
というわけで、まあまあ以上です。正直今回の記事は中身が無さすぎる気がする。終わってみれば、初めから定義置いて終了でもよかった。それくらいには「仮説を立てては否定する」のターンが辛かった。何か書かなければいけないような内容に感じていた。結果がこれだよ。
それではまた次がいつになるかわかりませんが、というか次の更新がTAPL記事になるかわかりませんが、今回もありがとうございました、また次回！
