型無しλ計算 - Internet Explorer 2.0

型無しλ計算

メモ　

評価の順番について

TaPLではこれを採用

簡単に言えばλ抽象の中で簡約をすることはできない

$ \lambda z. \mathrm{id}(z)は$ \lambda z.zにすることはできない

論理演算を次のようにλ式で表すことができる

$ \top := \lambda t. \lambda f.t

$ \bot := \lambda t.\lambda f. f

$ \mathrm{test} := \lambda b. \lambda v \lambda w. bvw

$ \land := \lambda b. \lambda c. b c \bot

$ \lor := \lambda b.\lambda c.b \top c

$ \lnot := \lambda b.b \bot \top

ただし$ b,c = \top, \bot

2組のペアを$ \mathrm{test}と同じ形式で

$ \mathrm{pair} := \lambda f.\lambda s.\lambda b. bfs

ただし$ b = \top,\bot

$ \mathrm{fst} := \lambda p. p \top

$ \mathrm{snd} := \lambda p. p \bot

$ pは$ \text{pair}

Church数$ c_0, c_1\dots c_n

$ c_0 := \lambda s.\lambda z. z

$ c_1 := \lambda s.\lambda z. s z

$ c_2 := \lambda s.\lambda. s(sz)

$ c_n := \lambda s.\lambda z. s(s(\cdots(s z)\cdots))

$ sは何らかの関数，$ zはゼロを指す

以下$ m,nはChurch数

$ \mathrm{plus} := \lambda m.\lambda n.\lambda s.\lambda z.ms(nsz)

$ \mathrm{times} := \lambda m.\lambda n.\lambda s.\lambda z.m(\mathrm{plus}(n))c_0

$ c_0に$ +nを$ m回するのイメージ

$ \mathrm{pow} := \lambda m.\lambda n.\lambda s.\lambda z.m(\mathrm{times}(n))c_1

ただし$ n^m

$ c_1に$ \times nを$ m回するのイメージ

後者関数$ \mathrm{suc}

前者関数