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

$\eta$ 長 $\beta$ 正規形の形. 型 $A_1\to \cdots \to A_k\to p$（$p$ は原子型）の $\eta$ 長 $\beta$ 正規形は
$$\lambda z_1\cdots z_k.w{N}_1\cdots N_m$$
の形で、頭部 $w$ は文脈中の変数、$w$ の型は $B_1\to \cdots \to B_m\to p$（結果がちょうど $p$ になるまで完全に適用する）、各 $N_j$ は型 $B_j$ の $\eta$ 長 $\beta$ 正規形である。したがって住人の個数は、文脈ごとに「各原子型の項の個数」を数えればよい。

外側の抽象. $T$ の住人は
$$\lambda Fghxy.M,F:(a\to b)\to (a\to b)\to c,g:a\to a\to b,h:b\to c,x,y:a$$
で、$M$ は文脈 $\Gamma =\{F,g,h,x,y\}$ での型 $c$ の $\eta$ 長 $\beta$ 正規形である。

各原子型を作れる変数. 結果の型が $c$ のものは $F,h$、$b$ のものは $g$、$a$ のものは $a$ 型の変数だけである。$b$ や $c$ の項から $a$ の項を作る変数はないので、数え上げは有限で終わる。

(1) 頭部が $h$ の場合. $M=hN$、$N$ は $\Gamma$ での型 $b$ の項。$N=gst$ で $s,t$ は型 $a$ の項、すなわち $\Gamma$ の $a$ 型変数 $x,y$ のいずれか。よって $2\cdot 2=4$ 通り。

(2) 頭部が $F$ の場合. $M=F{P}_1{P}_2$ で、$P_1,P_2$ は型 $a\to b$ の $\eta$ 長形なので $P_1=\lambda u.M_1$、$P_2=\lambda v.M_2$ と書ける。$M_1$ は文脈 $\Gamma \cup \{u:a\}$ での型 $b$ の項で、$M_1=gst$、$s,t\in \{x,y,u\}$ なので $3\cdot 3=9$ 通り。同様に $M_2$ も文脈 $\Gamma \cup \{v:a\}$ で $9$ 通り（$u$ は $P_2$ の中では使えない）。よって $9\cdot 9=81$ 通り。

頭部が $g,x,y$ のときは結果の型が $c$ にならないので、これで全部である。また異なる選び方は異なる正規形を与える。

したがって住人の個数は
$$4+81=85.$$

住人は $\lambda FGHxy.M$（$M:c$）の形。文脈は $F:(a\to b)\to (a\to b)\to c$, $G:a\to a\to b$, $H:b\to c$, $x,y:a$。

$\eta$ 長形では、型 $c$ の項は頭変数が最終的に $c$ を返す変数で始まる。そのような変数は $F$ と $H$ のみ。

型 $a$ の項: 返り値が $a$ の関数型の変数はなく、$a$ は原子型なので、$a$ 型の変数そのものだけ。文脈に $a$ 型の変数が $k$ 個あれば項は $k$ 個。
型 $b$ の項: 返り値が $b$ である変数は $G$ のみ（$F,H$ は $c$ を返す）。よって $G{A}_1{A}_2$（$A_i$ は $a$ 型の項）で、$k^2$ 個。

場合分け:
1. 頭が $H$: $H{M}^{\prime }$、$M^{\prime }:b$。文脈の $a$ 型変数は $x,y$ の 2 個なので $2^2=4$ 個。
2. 頭が $F$: $FPQ$、$P,Q:a\to b$。長形では $P=\lambda u.N$（$N:b$）で、文脈の $a$ 型変数は $x,y,u$ の 3 個なので $N$ は $3^2=9$ 個。$Q$ も同様に 9 個。よって $9\cdot 9=81$ 個。

合計 $4+81=85$。
検算: $a$ 型項と $b$ 型項の生成規則に他の可能性（たとえば $b$ 型の変数や $a$ を返す関数）がないことを確かめた。