プログラム意味論スレッド

λ式のバッカス記法による定義
　ｘ∈Ｕ {変数全体}
　Ｅ∈Λ {λ式全体}
とするとき、
　Ｅ ::＝ ｘ｜(Ｅ0 Ｅ1)｜(λｘ.Ｅ)

関数適用　(ＭＮ)
　Ｍが関数、Ｎが引数
関数抽象　(λｘ.Ｍ)
　束縛変数ｘによるＭのλ抽象

定義：部分λ式集合 sub(Ｅ)
(１) Ｅが変数x　→　{x}
(２) Ｅが(ＭＮ)　→　sub(Ｍ)∪sub(Ｎ)∪{Ｅ}
(３) Ｅが(λx．Ｍ)　→　sub(Ｍ)∪{Ｅ}

部分式　〜　sub(Ｅ) の元
xのＥにおける出現　〜　部分式であること
束縛された出現　〜　zが(λz．Ｍ)の中に出現するとき
自由な出現 〜　束縛されていない出現
閉式　〜　自由な出現をもたないλ式

Ｍで自由なxの出現をすべてＮでおきかえたものを
Subst[x>N] Ｍ、と書く。

定義：α変換
yがＱに部分式としても束縛変数としても出現しないとき
Ｅ=(λx．Ｑ)で、Ｆ=(λｙ．Subst[x>y] Ｑ)のとき、
ＥはＦにα変換可能であるといい、Ｅ{α}>Ｆと書く。

定義：β変換
Ｒで自由に出現するどの変数もＱで束縛されないとき
Ｅ=((λx．Ｑ)Ｒ)で、Ｆ=Subst[x>Ｒ] Ｑのとき、
ＥはＦにβ変換可能であるといい、Ｅ{β}>Ｆと書く。

α変換は関数の仮引数を形式的に変更すること、
β変換は関数の仮引数に実引数を代入すること
に対応する。

((λx．Ｑ)Ｒ)の形のλ式をβ基とよぶ。

つまらないんだけど、いつまで続けるの？

理解すれば面白くなりますよん。ではでは。