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

難易度 4大学院入試の難問レベル大学院数学計算理論・ラムダ計算

型なしラムダ計算を考える。適用は左結合（ $M N L = (M N) L$ ）とし、 $α$ 同値な項は同一視する。 $0$ 以上の整数 $n$ に対してチャーチ数を
$c_{n} = λ f . λ x . n 個 f (f (\dots (f x) \dots))$
で定める。さらに
$P = λa . λb . λ z . z a b, π_{2} = λ p . p (λa . λb . b),$
$F = λ p . p (λa . λb . P b (a b))$
とおき、
$M = π_{2} (c_{3} F (P c_{2} c_{2}))$
とする。 $M$ は $β$ 正規形をもち、それはあるチャーチ数 $c_{k}$ に一致する。 $k$ を求めよ。

この問題で使うもの

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

ヒント

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

ヒント 1

$F$ を対 $P A B$ に適用すると何になるかをまず調べ、 $c_{3} F X$ が $F$ の 3 回適用 $F (F (F X))$ に等しいことを使いましょう。

ヒント 2

$F (P A B) =_{β} P B (A B)$ です。さらにチャーチ数どうしの適用 $c_{m} c_{n}$ がどのチャーチ数になるかを、合成 $c_{a} (c_{b} g) =_{β} c_{ab} g$ から求めます。

ヒント 3

$c_{m} c_{n} =_{β} c_{n^{m}}$ です。対は $⟨ c_{2}, c_{2} ⟩ \mapsto ⟨ c_{2}, c_{4} ⟩ \mapsto ⟨ c_{4}, c_{16} ⟩ \mapsto \dots$ と変化します。

答えと解説

答えを見る

65536

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

解説を読む

以下 $=_{β}$ は $β$ 同値を表す。チャーチ–ロッサーの定理より、 $M =_{β} c_{k}$ が示せれば、 $c_{k}$ は $β$ 正規形なので $M$ の $β$ 正規形は $c_{k}$ である。

補題 1（合成）. 任意の項 $g$ と $a, b \geq 0$ について $c_{a} (c_{b} g) =_{β} c_{ab} g$ 。

実際 $c_{b} g =_{β} λ x . g^{b} x$ （ $g^{b} x$ は $g$ を $b$ 回適用した項）なので、 $c_{a} (c_{b} g) =_{β} λ y . (c_{b} g)^{a} y =_{β} λ y . g^{ab} y =_{β} c_{ab} g$ 。

補題 2（適用はべき乗）. $m \geq 1, n \geq 0$ について $c_{m} c_{n} =_{β} c_{n^{m}}$ 。

$c_{m} c_{n} =_{β} λ x . c_{n} (c_{n} (\dots (c_{n} x) \dots))$ （ $c_{n}$ が $m$ 個）。補題 1 を内側から繰り返し使うと $c_{n} (\dots (c_{n} x)) =_{β} c_{n^{m}} x$ となるので、 $c_{m} c_{n} =_{β} λ x . c_{n^{m}} x =_{β} λ x . λ y . x^{n^{m}} y = c_{n^{m}}$ 。

$F$ の働き. 任意の項 $A, B$ について
$F (P A B) \to_{β} P A B (λa . λb . P b (a b)) ↠_{β} (λa . λb . P b (a b)) A B ↠_{β} P B (A B) .$
つまり $F$ は対 $⟨ A, B ⟩$ を $⟨ B, A B ⟩$ に移す。また $π_{2} (P A B) =_{β} B$ である。

計算. $c_{3} F X =_{β} F (F (F X))$ であるから、 $X = P c_{2} c_{2}$ から順に $F$ を 3 回適用する。補題 2 により $c_{a} c_{b} =_{β} c_{b^{a}}$ を用いる。
- 1 回目: $P c_{2} c_{2} \mapsto P c_{2} (c_{2} c_{2}) =_{β} P c_{2} c_{4}$ （ $2^{2} = 4$ ）
- 2 回目: $P c_{2} c_{4} \mapsto P c_{4} (c_{2} c_{4}) =_{β} P c_{4} c_{16}$ （ $4^{2} = 16$ ）
- 3 回目: $P c_{4} c_{16} \mapsto P c_{16} (c_{4} c_{16}) =_{β} P c_{16} c_{65536}$ （ $1 6^{4} = 65536$ ）

したがって $M =_{β} π_{2} (P c_{16} c_{65536}) =_{β} c_{65536}$ となり、 $k = 65536$ である。

別解

$P a b$ は組 $(a, b)$ を表し、 $(P a b) s \to_{β} s a b$ 。 $π_{2}$ は組の第 2 成分を取り出す。

$F$ の働き: $F (P a b) \to (P a b) (λa . λb . P b (a b)) \to P b (a b)$ 。すなわち $F : (a, b) \mapsto (b, a b)$ 。

チャーチ数について $c_{i} c_{j} = λ x . c_{j}^{i} x = c_{j^{i}}$ （ $c_{i} c_{j} x \to c_{j} (c_{j} (\dots (c_{j} x)))$ 、 $c_{j}$ を $i$ 回合成すると $x$ に $f$ を $j^{i}$ 回かける。 $i = 0$ のとき $c_{0} c_{j} = λ x . x = c_{1} = c_{j^{0}}$ ）。よって $F : (c_{i}, c_{j}) \mapsto (c_{j}, c_{j^{i}})$ 。

$c_{3} F (P c_{2} c_{2})$ は $F$ を 3 回適用する。
- 初期: $(2, 2)$
- 1 回目: $(2, 2^{2}) = (2, 4)$
- 2 回目: $(4, 4^{2}) = (4, 16)$
- 3 回目: $(16, 1 6^{4}) = (16, 65536)$

$π_{2}$ で第 2 成分を取り出して $c_{65536}$ 。つまり $k = 65536 = 2^{16}$ 。

検算: 第 2 成分の列 $2, 4, 16, 65536$ は $b_{t + 1} = b_{t}^{b_{t - 1}}$ （ $b_{0} = b_{1} = 2$ から始め、 $b_{2} = 2^{2} = 4$ , $b_{3} = 4^{2} = 16$ , $b_{4} = 1 6^{4} = 65536$ ）に一致する。 $1 6^{4} = 2^{16} = 65536$ 。

この問題の確認

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

別の AI が答えを見ずに 3 回解き、3 回とも同じ答えになりました
プログラムで答えを計算し直し、一致を確認しました
AI の査読で、条件・解説・表記を確認しました
答えの正しさについて慎重に扱うべき点が見つからなかったため、自動で公開しました

確認の方法について

間違いを報告する

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