β 簡約と β 正規形

型なしラムダ項の自由変数・束縛変数を見分け、捕獲を避けた代入 $M [x := N]$ を行い、 $(λ x . M) N \to_{β} M [x := N]$ をくり返して項の β 正規形を求められる（正規形をもたない $Ω = (λ x . xx) (λ x . xx)$ も判定できる）

前提

中学までに習ったことだけで始められます。

説明

型なしラムダ計算では、関数の適用 $(λ x . M) N$ を「本体 $M$ の中の $x$ を $N$ で置き換える」ことで計算します。この一歩を β 簡約といい、これ以上 β 簡約できない項を β 正規形といいます。この技能を身につけると、ラムダ項を機械的に計算して最終的な形（β 正規形）を求めたり、 $Ω = (λ x . xx) (λ x . xx)$ のように計算がいつまでも終わらない項を見分けたりできます。チャーチ数による算術の計算や、プログラムの意味を調べる場面の基本操作です。

なぜそうしてよいのか

ラムダ項は、変数 $x$ 、抽象 $λ x . M$ （「 $x$ を受け取って $M$ を返す関数」）、適用 $M N$ （「 $M$ に $N$ を渡す」）の 3 種類から作られます。 $λ x . M$ の中の $x$ は $λ x$ に束縛されていて（束縛変数）、その名前に意味はありません。 $λ x . x$ と $λ y . y$ は同じ関数です（名前の付け替えを α 変換といい、α 変換で移り合う項は同じとみなします）。一方、どの $λ$ にも束縛されていない変数は自由変数で、外から与えられる値を表します。例えば $λ x . x y$ では $x$ が束縛変数、 $y$ が自由変数です。

関数 $λ x . M$ に $N$ を渡したら、「 $M$ の中の（自由に現れる） $x$ を $N$ に置き換えたもの」になるはずです。これが $(λ x . M) N \to_{β} M [x := N]$ です。ただし素朴に文字を置き換えると意味が変わることがあります。 $λ y . x$ は「何を受け取っても $x$ を返す関数」ですが、 $x$ に $y$ を代入して $λ y . y$ にすると恒等関数になってしまいます。外から来た自由変数 $y$ が、内側の $λ y$ に「捕獲」されたためです。そこで、代入する前に内側の束縛変数を新しい名前に付け替え、 $(λ y . x) [x := y] = (λ z . x) [x := y] = λ z . y$ とします。これが捕獲を避けた代入で、こうすれば束縛変数の名前に意味がないという原則と矛盾しません。

項の中に $(λ x . M) N$ の形の部分（β 基、レデックスという）が残っている限り β 簡約を続けられ、1 つも残らなくなった項が β 正規形です。β 正規形は、どの順序で簡約しても（たどり着けるなら）α 変換を除いて 1 つに決まることが知られています（チャーチ–ロッサーの定理）。ただし、どう簡約してもたどり着けない項もあります。 $Ω = (λ x . xx) (λ x . xx)$ を 1 回 β 簡約すると、 $xx$ の 2 つの $x$ に $λ x . xx$ を入れて $(λ x . xx) (λ x . xx) = Ω$ に戻ります。 $Ω$ の中にある β 基はこれ 1 つだけなので、どう簡約しても $Ω$ から抜け出せず、 $Ω$ は β 正規形をもちません。

手順

項の構造を読む。適用は左結合（ $M N P = (M N) P$ ）、 $λ$ の本体はできるだけ右まで伸びる（ $λ x . M N = λ x . (M N)$ ）という約束で括弧を補う
各変数が束縛変数か自由変数かを見分ける。代入で捕獲が起こりそうなら、内側の束縛変数を新しい名前に付け替えておく（α 変換）
$(λ x . M) N$ の形の部分（β 基）を 1 つ選ぶ。迷ったら最も左外側のものを選ぶ（正規形があれば必ずたどり着ける選び方）
$M$ の中の自由な $x$ だけを $N$ に置き換え、 $(λ x . M) N$ を $M [x := N]$ に書き換える
β 基がなくなるまで 3・4 をくり返す。β 基がなくなればそれが β 正規形。簡約しても同じ形の項に戻るなど終わらないことがわかれば、正規形をもたないと判定する

例題

自然数 $n (n \geq 0)$ に対し、チャーチ数を $n = λ f . λ x . n 個 f (f (\dots (f x) \dots))$ と定める（例: $0 = λ f . λ x . x$ 、 $2 = λ f . λ x . f (f x)$ ）。 $S = λm . λ f . λ x . f (m f x)$ とするとき、項 $S 2$ の β 正規形はあるチャーチ数 $k$ になる。 $k$ を求めよ。

例題の解答

（手順 1） $S 2 = (λm . λ f . λ x . f (m f x)) (λ f . λ x . f (f x))$ で、 $m f x = (m f) x$ と読む。

（手順 2） $2$ の中の $f, x$ は $2$ 自身の $λ$ に束縛されていて、外の $S$ の $f, x$ とは別物である。混同を避けるため $2 = λ g . λ y . g (g y)$ と名前を付け替える。 $2$ には自由変数がないので、代入で捕獲は起こらない。

（手順 3・4）いちばん外側の β 基で $m := λ g . λ y . g (g y)$ と代入する:
$S 2 \to_{β} λ f . λ x . f ((λ g . λ y . g (g y)) f x) .$
（手順 5 → 3・4）まだ β 基 $(λ g . λ y . g (g y)) f$ が残るので、 $g := f$ と代入する（ $f$ は内側の $λ y$ に捕獲されない）:
$\to_{β} λ f . λ x . f ((λ y . f (f y)) x) .$
さらに β 基 $(λ y . f (f y)) x$ で $y := x$ と代入する:
$\to_{β} λ f . λ x . f (f (f x)) .$
（手順 5）この項には $(λ \dots) N$ の形の部分がないので β 正規形である。これは $f$ が 3 個並んだ $3$ なので、 $k = 3$ 。

答え: $3$

よくある誤り

捕獲を気にせず文字を置き換えてしまう誤り。 $(λ x . λ y . x) y \to_{β} λ y . y$ とするのは誤りで、正しくは内側の $y$ を付け替えて $(λ x . λ z . x) y \to_{β} λ z . y$ （定数関数のまま）
束縛されている $x$ まで置き換えてしまう誤り。 $(x (λ x . x)) [x := N] = N (λ x . N)$ ではなく、正しくは内側の $x$ は $λ x$ に束縛されているので $N (λ x . x)$
結合の約束を取り違える誤り。 $λ x . x y$ を $(λ x . x) y$ と読んで $y$ に簡約してしまうが、正しくは $λ x . (x y)$ で、すでに β 正規形。また $x y z$ は $x (y z)$ ではなく $(x y) z$
$Ω = (λ x . xx) (λ x . xx)$ を簡約すると $xx$ の形になって止まると考える誤り。正しくは $(xx) [x := λ x . xx] = (λ x . xx) (λ x . xx)$ で $Ω$ に戻り、β 正規形をもたない

この説明は AI が書き、別の AI が例題を独立に解いて答えを確かめ、説明を一歩ずつ査読しました。

入口の問題

難易度 1（大学院の講義の例題レベル）
型なしラムダ計算を考える。適用は左結合（ $M N L = (M N) L$ ）、抽象は右に最大限のびるものとし、 $α$ 同値な項は同一視する。簡約は $β$ 簡約のみを考える（ $η$ 簡約は考えない）。 $y, z, w$ は変数とする。
項
$M = (λ x . λ y . x y) (λ z . z y)$
の $β$ 正規形として正しいものを、次のア〜オから 1 つ選べ。
ア　 $λ y . y y$
イ　 $λ w . w y$
ウ　 $λ w . y w$
エ　 $y$
オ　 $M$ は $β$ 正規形をもたない

この技能を使う問題

この技能の次に学べること

チャーチ数と対による計算（大学院数学計算理論・ラムダ計算）
単純型付けと型の数え上げ（大学院数学計算理論・ラムダ計算）