チャーチ数と対による計算

型なしラムダ計算を考える。適用は左結合（$MNL=(MN)L$）、抽象は右に最大限のびるものとし、$\alpha$ 同値な項は同一視する。簡約は $\beta$ 簡約のみを考える。$0$ 以上の整数 $n$ に対してチャーチ数を
$$c_n=\lambda f.\lambda x.f^{n}x(f^{0}x=x,f^{n+1}x=f(f^{n}x))$$
と定め、対と射影を
$$P=\lambda a.\lambda b.\lambda z.zab,{\pi }_1=\lambda a.\lambda b.a,{\pi }_2=\lambda a.\lambda b.b$$
と定める。さらに
$$G=\lambda p.P(p{\pi }_2)(c_2(p{\pi }_1))$$
とおき、項
$$M=c_{3}G(P{c}_2{c}_3){\pi }_2$$
を考える。$M$ の $\beta$ 正規形はあるチャーチ数 $c_k$ である。$k$ を求めよ。

型なしラムダ計算を考える。適用は左結合（$MNL=(MN)L$）、抽象は右に最大限のびるものとし、$\alpha$ 同値な項は同一視する。簡約は $\beta$ 簡約のみを考える（$\eta$ 簡約は考えない）。$0$ 以上の整数 $n$ に対してチャーチ数を $$c_n=\lambda f.\lambda x.\underset{n\text{ 個}}{\underbrace{f(f(\cdots (f}}x)\cdots ))$$ と定め（$c_0=\lambda f.\lambda x.x$）、項 $P$ を $$P=\lambda m.\lambda n.\lambda f.\lambda x.m(nf)(mfx)$$ と定める。項 $$N=P(c_2{c}_3)c_2$$ は $\beta$ 正規形をもち、それはあるチャーチ数 $c_k$ に一致する。$k$ を求めよ。

型なしラムダ計算を考える。適用は左結合（$MNL=(MN)L$）、抽象は右に最大限のびるものとし、$\alpha$ 同値な項は同一視する。簡約は $\beta$ 簡約のみを考える。$0$ 以上の整数 $n$ に対してチャーチ数を
$$c_n=\lambda f.\lambda x.\underset{n\text{個}}{\underbrace{f(f(\cdots (f}}x)\cdots ))$$
と定め、右辺の本体を $f^{n}x$ と書く（$f^{0}x=x$）。

項
$$M=(c_3{c}_2)(c_2{c}_3)$$
は $\beta$ 正規形をもち、その正規形は、ある $0$ 以上の整数 $k$ に対して $\lambda f.\lambda x.f^{k}x$ と $\alpha$ 同値になる。この $k$ を求めよ。

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

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

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

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

型なしラムダ計算を考える。適用は左結合（$MNL=(MN)L$）、抽象は右に最大限のびるものとし、$\alpha$ 同値な項は同一視する。簡約は $\beta$ 簡約のみを考える（$\eta$ 簡約は考えない）。$0$ 以上の整数 $n$ に対してチャーチ数を
$$c_n=\lambda f.\lambda x.\underset{n\text{個}}{\underbrace{f(f(\cdots (f}}x)\cdots ))$$
で定める。

正規順序戦略とは、各ステップで、項に含まれる $\beta$ 基（$(\lambda v.P)Q$ の形の部分項）のうち最も左外側にあるもの（項を文字列として書いたときに、その $\beta$ 基の先頭が最も左にあるもの）を 1 回だけ縮約する戦略である。

項 $c_3{c}_2$ から出発して正規順序戦略で $\beta$ 簡約を繰り返すと、有限回で $\beta$ 正規形に到達する。正規形に到達するまでに行われる $\beta$ 簡約の回数（ステップ数）を求めよ。

型なしラムダ計算を考える。適用は左結合（$MNL=(MN)L$）、抽象は右に最大限のびるものとし、$\alpha$ 同値な項は同一視する。簡約は $\beta$ 簡約のみを考える（$\eta$ 簡約は考えない）。$0$ 以上の整数 $n$ に対してチャーチ数を
$$c_n=\lambda f.\lambda x.\underset{n\text{個}}{\underbrace{f(f(\cdots (f}}x)\cdots ))$$
と定める（$c_0=\lambda f.\lambda x.x$）。さらに次の項を定める。
$$S=\lambda n.\lambda f.\lambda x.f(nfx),M=\lambda m.\lambda n.\lambda f.m(nf),$$
$$P=\lambda a.\lambda b.\lambda s.sab,K=\lambda a.\lambda b.a,K^{\prime }=\lambda a.\lambda b.b,$$
$$T=\lambda p.P(p{K}^{\prime })(S(M(pK)(p{K}^{\prime }))).$$
このとき項
$$N=c_2{c}_{2}T(P{c}_1{c}_1)K^{\prime }$$
は $\beta$ 正規形をもち、それはあるチャーチ数 $c_k$ に一致する。整数 $k$ を求めよ。

型なしラムダ計算を考える。適用は左結合（$MNL=(MN)L$）とし、$\alpha$ 同値な項は同一視する。$0$ 以上の整数 $n$ に対してチャーチ数を
$$c_n=\lambda f.\lambda x.\underset{n\text{ 個}}{\underbrace{f(f(\cdots (f}}x)\cdots ))$$
で定める。さらに
$$P=\lambda a.\lambda b.\lambda z.zab,{\pi }_2=\lambda p.p(\lambda a.\lambda b.b),$$
$$F=\lambda p.p(\lambda a.\lambda b.Pb(ab))$$
とおき、
$$M={\pi }_2(c_{3}F(P{c}_2{c}_2))$$
とする。$M$ は $\beta$ 正規形をもち、それはあるチャーチ数 $c_k$ に一致する。$k$ を求めよ。