ラムダ抽象
λ-abstraction
「ラムダ項」、「ラムダ束縛」とも言う
定義
$ \mathcal{V}を可算無限個の変数の集合とする
$ \lambda項の集合$ \Lambdaを以下を満たす最小の集合とする
$ x\in\mathcal{V}\Rightarrow x\in\Lambda
変数もラムダ抽象である
$ M,N\in\Lambda\Rightarrow(MN)\in\Lambda
作用した結果もラムダ抽象である
この$ (MN)のことを「作用表現」という
$ M \in \Lambda, x \in \mathcal{V} \Rightarrow(\lambda x . M) \in \Lambda
抽象化したものもラムダ抽象である
この$ (\lambda x . M)を「抽象化表現」という
ラムダ抽象に対する操作は2つだけ
作用
関数適用のこと
$ M Nとあるときに、「引数$ Nに、関数$ Mを適用する」と見る
つまり、値が主導
抽象化
関数定義のこと
値$ Mを返す関数$ \lambda x.Mを作ることで、$ Mを$ xで抽象化した、と見る
略記の解釈
作用は左結合
$ M_1M_2M_3とあれば、$ (M_1M_2)M_3
例えば$ \lambda x.\lambda y.x y xとあるとき、
xyxは(x y) xであり
x yは「関数x」を「y」に適用している
つまり、引数に取るものは値とは限らない
抽象はできるだけ右に伸ばして読む
参考
記号の優先順位がわからない
$ N\equiv\lambda z.(\lambda x.yx)zxとあるとき、以下のどれ？
「抽象$ \lambda z.B」の$ Bにはどこまで含まれる？
①$ (\lambda x.yz)
②$ (\lambda x.yz)z
③$ (\lambda x.yz)zx
与えられたラムダ式が、「抽象表現」なのか「作用表現」なのかで解釈の仕方が変わる
たぶんmrsekut.icon
上の$ Nが「抽象表現」ならば③
つまり$ N全体がラムダ抽象
上の$ Nが「作用表現」ならば①？
つまり引数$ zxに関数$ \lambda z.(\lambda x.yx)を適用している
ということは、そのラムダ式が、どちらを表しているのか常に前提が必要？
わかんねえわmrsekut.icon
『(理論)12 計算モデルの基礎理論』.icon pp.79-80
関連