「ラムダ項」、「ラムダ束縛」とも言う

ラムダ計算の項のこと

定義

\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

与えられたラムダ式が、「抽象表現」なのか「作用表現」なのかで解釈の仕方が変わる

たぶん

上のNが「抽象表現」ならば③

つまりN全体がラムダ抽象

上のNが「作用表現」ならば①？

つまり引数zxに関数\lambda z.(\lambda x.yx)を適用している

ということは、そのラムダ式が、どちらを表しているのか常に前提が必要？

わかんねえわ

pp.79-80

関連