チューリングマシンと同等の計算能力を持つことが偉大ではないですか？では、ラムダ計算は「虚無生兩極、兩極生四象、四象生八卦」を実現できます。チャーチに感謝します、最終的に我々は世界の万物を手に入れました。

ラムダ計算（またはλ計算）は、関数の定義、実装、再帰を研究するための形式定義システムであり、関数型プログラミング言語の計算モデルでもあります。

定義

ラムダ式は次の要素から構成されます：

  • 変数： v1, v2, . . .
  • 記号：λ および .
  • 括弧：( および )

合法なλ式 <expression> は以下のように再帰的に定義されます：

  • <expression> = <variable> | <function> | <application>
  • <function> = λ <variable>.<expression>
  • <application> = (<expression> <expression>)

λ式の表記法

ラムダ式 M と N に対して、

  • 最外層の括弧は省略可能で、(M N) は M N と表記できます。
  • (λx. M) という式は 関数抽象 と呼ばれ、これは関数の定義を示しています。関数の引数は変数x、関数本体はM、関数名は無名です。これはf(x)=Mと考えることができ、無名であることは関数名fが存在せず、xがMにマッピングされるプロセスのみが存在することを意味します。
  • 関数適用は左結合で行われます： M N P は (M N) P を意味します。
  • λ式は貪欲に拡張されます： λ x. M N は (λ x.M N) を意味し、 (λ x. M) N ではありません。
  • λ式のシーケンス：λ x λ y λ z. N は λ x y z . N と省略可能です。

λ式における自由変数と束縛変数

関数抽象演算子 λ は、関数抽象の本体に現れる任意の変数を束縛できます。変数がλ式のスコープ内にある場合、その変数は束縛されています。そうでなければ、その変数は自由です。

例えば、式 λ y . x x y において、yはλによって束縛された変数ですが、xは自由変数です。

一連の自由変数からなるλ式Mは FV(M) として表現でき、次のように再帰的に定義されます：

  • FV( x ) = {x}、ここでxは自由変数です。
  • FV ( λ x . M ) = FV ( M ) - {x}
  • FV ( M N ) = FV ( M ) ∪ FV ( N )

自由変数を含まないλ式は閉じた式と呼ばれます。

簡約方法

α変換

これはシンボルの置換を表します。特に意味はありませんが、簡約中にシンボル名が衝突した場合、シンボルをリネームすることができます。ただし、α変換は現在のスコープ内でのみ有効です。例えば、λ x x. x は λy x. x に変換できますが、λy x.y に変換することはできません。なぜなら、名前自体はλ式において重要ではないからです。

置換：E[V:=E']は変数VをE'で置換できることを意味し、E'がE内で自由である場合に適用されます。

例えば (λx. y)[y:=x]の結果が(λx. x)になるのは誤りです。なぜなら、xがλの下で束縛されているからです。正しい方法は、α変換を用いて (λz. y)[y:=x] とし、(λz.x) を得ることです。

β簡約

これは関数適用の考え方を表現しています。

式(M N)は、関数MをNに適用することを意味します。つまり、Nを引数として関数Mに渡し、Mの中でMの束縛変数として扱います。上記の定義を用いると、β簡約 (λ v. m) n は m[v:=n] と表現できます。

例えば、関数λ x. (+ x 2)が存在し、+操作がすでに実装されている場合、(λ x. (+ x 2)) 3の結果は(+ 3 2)=5となります。

η変換

これは「外延性」の考え方を表現しています。

もし二つの関数が等価であるならば、それらはすべての引数に対して一致する結果を返さなければなりません。つまり、これら二つの関数に対して、β簡約やα変換を行うと一致するλ式が得られます。

0から世界万物へ

さて、λ計算で遊び始めることができます。忘れてはいけないのは、上記の内容以外には何も持っていないということです、「数」という概念を含めて。

まず、自然数の定義です：

0:= λ f x. f
1:= λ f x. f x
2:= λ f x. f (f x)
3:= λ f x. f (f (f x))
n:= λ f x. f^n x

自然数nの表現は、関数fを引数にn回適用した結果としてのラムダ式であることがわかります。自然数の全域を得るために、現在の自然数nに1を加えるためのINCプロセスを定義できます：

INC:=λ n f x. f (n f x)

同様に、加法PLUS m nプロセスは、関数をm回適用し、さらにn回適用する、つまりm+n回の結果と考えることができます：

PLUS:=λ m n f x. n f (m f x)

もちろん、INCを利用してPLUSを定義することもでき、mに1を加えるプロセスをn回行う結果と考えることができます：

PLUS:=λ m n. n INC m

例えば、(PLUS 2 3)を求めるプロセスは以下の通りです：

(PLUS 2 3)
(PLUS 2 3):= (((λ m n f x. n f (m f x)) 2 ) 3)
:= ((λ m n f x. n f (m f x)) (λ f x. f (f x)) (λ f x. f (f (f x))))
    ここで、(m f x) [m:=λ f x. f (f x)]
    → (λ f x. f (f x)) f x
    → (λ x. f' (f' x)[f':= f] ) x
    → λ x. f (f x) x
    → f (f x')[x':=x]
    → f (f x)
∴ (2 f x) := f (f x)
∴ PLUS 2 3 := (λ n f x. n f (f (f x))) (λ f x. f (f (f x)))
   ここで (n f)[n := λ f x. f (f (f x))]
    → (λ f x. f (f (f x))) f
    → (λ x. f' (f' (f' x)))[f':=f]
    → (λ x. f (f (f x)))
∴ PLUS 2 3 := (λ f x. (λ x. f (f (f x))) (f (f x)))
∵ (λ x. f (f (f x))) (f (f x))
    → f' (f' (f

' x'))[x' := (f (f x))]
    → f' (f' (f' (f (f x))))
    ∵ f は λ 下の束縛変数
    ∴ f'== f;
∴ PLUS 2 3 := f (f (f (f (f x)))) ＝ 5

同様にして、他の算術演算および論理演算を定義することもできます。

再度チャーチに感謝します、この世界を構築してくれたことに。

附：SICP 練習 2.6 の答え:

(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))
(define (add n m)
  (lambda (f) (lambda (x) ((n f) ((m f) x))))