■

久しぶりに高橋正子の計算論の第２章「λ計算の基礎」最初の方の数ページを読んだ。
λ計算ってとどのつまり何よ？　って事なんだけど、少し分かった

λ"計算"ってのは、まず以下の定義に基づき再帰的に定義される"λ式"

1. 変数 x0, x1, x2, ...はλ式である
2. Mがλ式でxが変数のとき (λx.M)はλ式である
3. MとNがλ式のとき (MN)はλ式である

と、そのλ式に対して以下で定義されるβ変換（簡約）

(λx.M)N → M[x:=N]
M → N ⇒ λx. M → λx.N, MP → NP, PM → PN
※β変換 「」を「→」と略記している

を繰り返し行うこと！
これだけ！！
まーα変換（変数名は変えてもいいよ）とかあるけど、本質的なところはβ変換のみと考えても良さそう。

ようは"計算" ≡ "β変換" と思っていい

一般的な感覚で言うところの計算（＋やら−やら微分やら）はλ計算の世界では"β変換"を繰り返すだけ。

だからチャーチ数とか (zero ≡ (λf x.x), one ≡ (λf x. f(x)),...)に対する四則演算等は
全てβ変換のみ（とα変換も）繰り返し自然数を定義した各々のλ式に等しくなるかどうかを見ているので決して等号「＝」で結んではだめ。

succ ≡ λ n f x. f(n f x)

ていう演算が定義されていて
zero succ one
というλ式を"計算"したい時は

zero succ one
  → (λ f x. x) (λ n f x. f(n f x)) (λ f x. f x)
  → (λ f x. f x)  ※ 最左のλ式をβ変換
  = one

って感じでβ変換の矢印で式を書く必要がある。

ちなみに括弧が無ければβ変換するのはどこからでも構わない。

(λ n f x. f(n f x)) (λ f x. f x)

を先にβ変換してもいい。

β変換はどこから変換するかによってぜんぜん違うλ式が生成される。
でも最終的に一致するものを「等しい」と言う
1 + 2 = 1 + 3 - 3 + 2 = 1 + 2 = 3
みたいなモン
（λ計算における等しいって言葉の定義をしてないのでここでは感覚的）

β変換を繰り返してλ式が収束（無限に続かず有限に落ち着く）するλ式を正規形って言う。
Church-Rossarの定理ってのは、あるλ式に正規形が存在するならその正規形は一つしか無い　って事

正規形を持たないλ式も存在して、そんなλ式は無限に計算が終わらない

(λ x. xxx)(λ x. xxx)
みたいなλ式がそれ。
こいつを常に左の二つのλ式でβ変換していくと

(λ x. xxx)(λ x. xxx)
(λ x. xxx)(λ x. xxx)(λ x. xxx)
(λ x. xxx)(λ x. xxx)(λ x. xxx)(λ x. xxx)
...

って感じで無限に計算が終わらない。