計算理論・ラムダ計算の問題

難易度 2大学院の講義の演習問題レベル証明問題大学院数学計算理論・ラムダ計算

型なしラムダ計算を考え、項は $α$ 同値なものを同一視する。適用 $M N$ は $M$ を関数、 $N$ を引数とする適用を表し、適用は左結合とする（ $M N P = (M N) P$ ）。代入 $M [z := N]$ は変数の捕獲を起こさない代入（必要なら束縛変数を付け替える）とする。 $\to_{β}$ を 1 ステップの $β$ 簡約（任意の部分項で行ってよい）、 $↠_{β}$ をその反射推移閉包とする。 $β$ 基（ $(λ z . P) Q$ の形の部分項）を含まない項を $β$ 正規形といい、 $M ↠_{β} N$ となる $β$ 正規形 $N$ を $M$ の $β$ 正規形という。

項 $F, X$ と $0$ 以上の整数 $k$ に対して $F^{0} X = X$ , $F^{k + 1} X = F (F^{k} X)$ と定め、 $0$ 以上の整数 $k$ のチャーチ数を
$c_{k} = λ f . λ x . f^{k} x$
とする（ $f$ , $x$ は異なる変数）。さらに、互いに異なる変数 $a, f, x$ を用いて
$S = λa . λ f . λ x . a f (a f (f x))$
と定める。

チャーチ・ロッサーの定理（したがって、ある項が $β$ 正規形をもつならそれは一意であること）は用いてよい。

$n$ を $0$ 以上の整数とするとき、項 $c_{n} S c_{0}$ の $β$ 正規形が $c_{2^{n} - 1}$ であることを証明せよ。

この問題で使うもの

β 簡約と β 正規形（説明と入口の問題）
チャーチ数と対による計算（説明と入口の問題）

ヒント

行き詰まったら、上から順に 1 つずつ開いてください。

ヒント 1

$c_{n} S c_{0} ↠_{β} c_{2^{n} - 1}$ を示し、チャーチ数が $β$ 正規形であることと正規形の一意性で結論します。まず $S$ がチャーチ数に対してどんな数を返すかを調べましょう。

ヒント 2

鍵になるのは、任意の項 $F, X$ について $c_{m} F X ↠_{β} F^{m} X$ となることと、 $S c_{m} ↠_{β} c_{2 m + 1}$ となることです。 $F^{k} (F^{j} X) = F^{k + j} X$ も使います。

ヒント 3

$S c_{m} \to_{β} λ f . λ x . c_{m} f (c_{m} f (f x))$ の内側を、内側の $c_{m} f (f x)$ から順に簡約すると $f$ が何回並ぶかを数えます。そのあと $c_{n} S c_{0} ↠_{β} S^{n} c_{0}$ とし、 $S^{k} c_{0}$ を $k$ に関する帰納法で調べます。

採点の観点と模範解答

自分で証明を書いてから、採点の観点で見比べてください。

採点の観点を見る

任意の項 $F, X$ について $c_{m} F X ↠_{β} F^{m} X$ を、束縛変数の付け替えで変数の捕獲を避けて示している（2 点）
$S c_{m} \to_{β} λ f . λ x . c_{m} f (c_{m} f (f x))$ から、内側の項を文脈の中で順に簡約し $f^{m + 1} x$ 、 $f^{2 m + 1} x$ を得て $S c_{m} ↠_{β} c_{2 m + 1}$ を導いている（3 点）
$S^{k} c_{0} ↠_{β} c_{2^{k} - 1}$ を、 $2 (2^{k} - 1) + 1 = 2^{k + 1} - 1$ を使って $k$ に関する帰納法で示している（2 点）
$c_{n} S c_{0} ↠_{β} S^{n} c_{0}$ と合わせて $c_{n} S c_{0} ↠_{β} c_{2^{n} - 1}$ を得ている（1 点）
チャーチ数が $β$ 基を含まない（適用の関数部分がすべて変数 $f$ ）ことを示し、チャーチ・ロッサーの定理による正規形の一意性から結論している（2 点）

結果を記録する（このブラウザにだけ保存されます）:

模範解答を読む

示すことは 2 つある: (A) $c_{n} S c_{0} ↠_{β} c_{2^{n} - 1}$ 、(B) $c_{2^{n} - 1}$ が $β$ 正規形であること。この 2 つが示されれば、 $c_{2^{n} - 1}$ は $c_{n} S c_{0}$ の $β$ 正規形の 1 つであり、正規形の一意性（チャーチ・ロッサーの定理から従う）により、それが $c_{n} S c_{0}$ の $β$ 正規形である。

以下、 $β$ 簡約が任意の部分項で行えること（文脈について閉じていること）を使う。すなわち $M ↠_{β} M^{'}$ ならば $P M ↠_{β} P M^{'}$ , $M P ↠_{β} M^{'} P$ , $λ z . M ↠_{β} λ z . M^{'}$ である（1 ステップごとに文脈の中で同じ簡約をすればよい）。また $c_{k}$ と $S$ は自由変数をもたない閉項である。

補題 0. 項 $F, X$ と $k, j \geq 0$ に対し $F^{k} (F^{j} X) = F^{k + j} X$ （構文的に等しい）。

証明. $k$ に関する帰納法。 $k = 0$ では両辺とも $F^{j} X$ 。 $k$ で成り立てば $F^{k + 1} (F^{j} X) = F (F^{k} (F^{j} X)) = F (F^{k + j} X) = F^{k + j + 1} X$ 。 $□$

補題 1. 任意の $m \geq 0$ と任意の項 $F, X$ に対し $c_{m} F X ↠_{β} F^{m} X$ 。

証明. 項は $α$ 同値なものを同一視するので、 $c_{m} = λ f . λ y . f^{m} y$ と書いてよい。ここで $y$ は $F$ に自由に現れない変数で、 $f$ と異なるものにとる。 $β$ 簡約の定義より
$c_{m} F \to_{β} (λ y . f^{m} y) [f := F] = λ y . F^{m} y$
である（ $y$ は $F$ に自由に現れないので、束縛変数 $y$ による捕獲は起こらない。また $f^{m} y$ の中で $f$ を $F$ に置き換えると $F^{m} y$ になることは $m$ に関する帰納法で直ちにわかる）。文脈閉包により $c_{m} F X \to_{β} (λ y . F^{m} y) X$ 。さらに
$(λ y . F^{m} y) X \to_{β} (F^{m} y) [y := X] = (F [y := X])^{m} X = F^{m} X$
である。ここで 2 つ目の等号は、代入が適用の各部分に分配されること（ $m$ に関する帰納法）により、3 つ目の等号は $y$ が $F$ に自由に現れないので $F [y := X] = F$ となることによる。合わせて $c_{m} F X ↠_{β} F^{m} X$ （ $m = 0$ のときは $c_{0} F X \to_{β} (λ y . y) X \to_{β} X = F^{0} X$ で、同じ議論に含まれる）。 $□$

補題 2. 任意の $m \geq 0$ に対し $S c_{m} ↠_{β} c_{2 m + 1}$ 。

証明. $c_{m}$ は閉項なので、代入 $[a := c_{m}]$ で変数の捕獲は起こらず
$S c_{m} \to_{β} λ f . λ x . c_{m} f (c_{m} f (f x)) .$
内側の部分項について、補題 1（ $F = f$ , $X = f x$ ）と補題 0 より
$c_{m} f (f x) ↠_{β} f^{m} (f x) = f^{m} (f^{1} x) = f^{m + 1} x .$
これを引数の位置で使うと $c_{m} f (c_{m} f (f x)) ↠_{β} c_{m} f (f^{m + 1} x)$ であり、再び補題 1（ $F = f$ , $X = f^{m + 1} x$ ）と補題 0 より
$c_{m} f (f^{m + 1} x) ↠_{β} f^{m} (f^{m + 1} x) = f^{2 m + 1} x .$
$λ f . λ x .$ の内側で簡約できるので
$S c_{m} ↠_{β} λ f . λ x . f^{2 m + 1} x = c_{2 m + 1} . □$

補題 3. 任意の $k \geq 0$ に対し $S^{k} c_{0} ↠_{β} c_{2^{k} - 1}$ 。

証明. $k$ に関する帰納法。 $k = 0$ では $S^{0} c_{0} = c_{0} = c_{2^{0} - 1}$ （反射性）。 $S^{k} c_{0} ↠_{β} c_{2^{k} - 1}$ を仮定すると、文脈閉包と補題 2（ $m = 2^{k} - 1 \geq 0$ ）より
$S^{k + 1} c_{0} = S (S^{k} c_{0}) ↠_{β} S c_{2^{k} - 1} ↠_{β} c_{2 (2^{k} - 1) + 1} = c_{2^{k + 1} - 1} . □$

(A) の証明. 補題 1（ $m = n$ , $F = S$ , $X = c_{0}$ ）より $c_{n} S c_{0} ↠_{β} S^{n} c_{0}$ であり、補題 3（ $k = n$ ）より $S^{n} c_{0} ↠_{β} c_{2^{n} - 1}$ 。推移性より $c_{n} S c_{0} ↠_{β} c_{2^{n} - 1}$ 。

(B) の証明. $c_{k} = λ f . λ x . f^{k} x$ の部分項は、 $c_{k}$ 自身、 $λ x . f^{k} x$ 、 $f^{j} x$ （ $0 \leq j \leq k$ ）、および変数 $f$ である。このうち適用の形をしているのは $f^{j} x = f (f^{j - 1} x)$ （ $1 \leq j \leq k$ ）だけで、その関数部分は変数 $f$ であり $λ$ 抽象ではない。よって $c_{k}$ は $β$ 基を含まず、 $β$ 正規形である。特に $c_{2^{n} - 1}$ は $β$ 正規形である。

結論. (A) より $c_{n} S c_{0} ↠_{β} c_{2^{n} - 1}$ 、(B) より $c_{2^{n} - 1}$ は $β$ 正規形である。チャーチ・ロッサーの定理より $β$ 正規形は一意なので、任意の $n \geq 0$ に対して $c_{n} S c_{0}$ の $β$ 正規形は $c_{2^{n} - 1}$ である。 $■$

この問題の確認

AI が作成した問題です。公開前に次の確認を行いました。

別の AI が模範解答を見ずに 3 回証明を試み、3 回証明できました
2 つの AI が独立に、模範解答の証明を 1 ステップずつ確かめました
AI の査読で、条件・解説・表記を確認しました
答えの正しさについて慎重に扱うべき点が見つからなかったため、自動で公開しました

確認の方法について

間違いを報告する

この問題の誤り・分かりにくい点・難易度や学年のずれを知らせる