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

難易度 3大学院入試の専門科目の標準レベル大学院数学計算理論・ラムダ計算

型なしラムダ計算を考える。適用は左結合（ $M N L = (M N) L$ ）、抽象は右に最大限のびるものとし、 $α$ 同値な項は同一視する。簡約は $β$ 簡約のみを考える（ $η$ 簡約は考えない）。 $0$ 以上の整数 $n$ に対してチャーチ数を
$c_{n} = λ f . λ x . n 個 f (f (\dots (f x) \dots))$
と定める（ $c_{0} = λ f . λ x . x$ ）。さらに次の項を定める。
$S = λn . λ f . λ x . f (n f x), M = λm . λn . λ f . m (n f),$
$P = λa . λb . λ s . s a b, K = λa . λb . a, K^{'} = λa . λb . b,$
$T = λ p . P (p K^{'}) (S (M (p K) (p K^{'}))) .$
このとき項
$N = c_{2} c_{2} T (P c_{1} c_{1}) K^{'}$
は $β$ 正規形をもち、それはあるチャーチ数 $c_{k}$ に一致する。整数 $k$ を求めよ。

この問題で使うもの

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

ヒント

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

ヒント 1

$c_{n} F X$ が $F$ を $X$ に $n$ 回適用した項に簡約されることを使い、まず $c_{2} c_{2}$ が何回の反復を表すかを調べよう。

ヒント 2

$c_{2} c_{2} \to_{β}^{*} c_{4}$ である。また $P X Y K =_{β} X$ 、 $P X Y K^{'} =_{β} Y$ 、 $S c_{n} =_{β} c_{n + 1}$ 、 $M c_{a} c_{b} =_{β} c_{ab}$ を確かめると、 $T (P c_{a} c_{b}) =_{β} P c_{b} c_{ab + 1}$ がわかる。

ヒント 3

$N =_{β} T^{4} (P c_{1} c_{1}) K^{'}$ となる。組は $(1, 1) \mapsto (1, 2) \mapsto (2, 3) \mapsto \dots$ と変化するので、あと 2 回の更新を計算し、最後に第 2 成分を取り出せばよい。

答えと解説

答えを見る

22

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

解説を読む

以下、 $\to_{β}^{*}$ は $0$ 回以上の $β$ 簡約、 $=_{β}$ は $β$ 同値を表す。 $F^{n} X$ で $n F (F (\dots (F X) \dots))$ を表す。

(1) チャーチ数による反復. 任意の項 $F, X$ に対し
$c_{n} F X \to_{β} (λ x . F^{n} x) X \to_{β} F^{n} X$
である（ $x$ が $F$ に自由に現れないよう束縛変数を取り替えておく）。

(2) $c_{2} c_{2}$ の正規形.
$c_{2} c_{2} \to_{β} λ x . c_{2} (c_{2} x) \to_{β} λ x . λ y . (c_{2} x) ((c_{2} x) y) .$
ここで $c_{2} x \to_{β} λ z . x (x z)$ なので $(c_{2} x) y \to_{β}^{*} x (x y)$ 、さらに $(c_{2} x) (x (x y)) \to_{β}^{*} x (x (x (x y)))$ 。よって
$c_{2} c_{2} \to_{β}^{*} λ x . λ y . x (x (x (x y))) = c_{4} .$
（一般に $c_{m} c_{n} =_{β} c_{n^{m}}$ であり、ここでは $2^{2} = 4$ 。）

したがって $N =_{β} c_{4} T (P c_{1} c_{1}) K^{'}$ で、(1) より
$N =_{β} T^{4} (P c_{1} c_{1}) K^{'} .$

(3) 組と射影. $P X Y \to_{β}^{*} λ s . s X Y$ だから
$P X Y K \to_{β}^{*} K X Y \to_{β}^{*} X, P X Y K^{'} \to_{β}^{*} K^{'} X Y \to_{β}^{*} Y .$

(4) 算術. $S c_{n} \to_{β} λ f . λ x . f (c_{n} f x) \to_{β}^{*} λ f . λ x . f (f^{n} x) = c_{n + 1}$ 。また
$M c_{a} c_{b} \to_{β}^{*} λ f . c_{a} (c_{b} f) \to_{β}^{*} λ f . λ x . (c_{b} f)^{a} x .$
$(c_{b} f) u \to_{β}^{*} f^{b} u$ を内側から $a$ 回使うと $(c_{b} f)^{a} x \to_{β}^{*} f^{ab} x$ となり、 $M c_{a} c_{b} \to_{β}^{*} c_{ab}$ 。

(5) $T$ の働き. (3), (4) より
$T (P c_{a} c_{b}) \to_{β} P (P c_{a} c_{b} K^{'}) (S (M (P c_{a} c_{b} K) (P c_{a} c_{b} K^{'}))) =_{β} P c_{b} (S (M c_{a} c_{b})) =_{β} P c_{b} c_{ab + 1} .$
つまり $T$ は組 $(a, b)$ を $(b, ab + 1)$ に移す。 $=_{β}$ は適用について合同なので、これを繰り返し使える。

(6) 計算. $(1, 1)$ から始めると
$(1, 1) \mapsto (1, 1 \cdot 1 + 1) = (1, 2) \mapsto (2, 1 \cdot 2 + 1) = (2, 3) \mapsto (3, 2 \cdot 3 + 1) = (3, 7) \mapsto (7, 3 \cdot 7 + 1) = (7, 22) .$
よって $T^{4} (P c_{1} c_{1}) =_{β} P c_{7} c_{22}$ であり、(3) より
$N =_{β} P c_{7} c_{22} K^{'} =_{β} c_{22} .$

(7) 正規形. $c_{22}$ は $β$ 正規形である。Church–Rosser の定理より、 $N =_{β} c_{22}$ なら $N$ と $c_{22}$ は共通の簡約先をもち、 $c_{22}$ は正規形なので $N \to_{β}^{*} c_{22}$ 。正規形は（存在すれば）一意なので、 $N$ の $β$ 正規形は $c_{22}$ である。また $n \neq = n^{'}$ なら $c_{n}$ と $c_{n^{'}}$ は $α$ 同値でない異なる正規形なので、 $k$ は一意に決まる。

したがって $k = 22$ 。

別解

$c_{2} c_{2} = λ x . c_{2} (c_{2} x)$ は $c_{4}$ と $β$ 同値（ $c_{m} c_{n} =_{β} c_{n^{m}}$ で $2^{2} = 4$ ）。よって $c_{2} c_{2} T =_{β} T^{4}$ （ $T$ を 4 回適用）。

対 $p = P u v$ （ $u, v$ はチャーチ数）に対し $p K = u$ , $p K^{'} = v$ 。 $M u v = λ f . u (v f)$ は積 $c_{uv}$ 、 $S$ は後者関数。したがって $T (P u v) =_{β} P v c_{1 + uv}$ 、すなわち数の組 $(u, v) \mapsto (v, 1 + uv)$ 。

$(1, 1)$ から 4 回適用する:
- 1 回目: $(1, 1 + 1 \cdot 1) = (1, 2)$
- 2 回目: $(2, 1 + 1 \cdot 2) = (2, 3)$
- 3 回目: $(3, 1 + 2 \cdot 3) = (3, 7)$
- 4 回目: $(7, 1 + 3 \cdot 7) = (7, 22)$

最後に $K^{'}$ を適用すると第 2 成分 $c_{22}$ が得られる。よって $k = 22$ 。
検算: 漸化式 $a_{n + 1} = 1 + a_{n - 1} a_{n}$ （ $a_{0} = a_{1} = 1$ ）で $a_{2} = 2, a_{3} = 3, a_{4} = 7, a_{5} = 22$ となり、一致する。

この問題の確認

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

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

確認の方法について

間違いを報告する

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