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

型の個数. 矢印数 $3$ の型は、葉が $4$ 個の二分木の形（カタラン数 $C_3=5$ 通り）と、葉への $a,b$ の割り当て（$2^4=16$ 通り）で決まる。したがって全部で $80$ 個ある。葉を左から $X,Y,Z,W\in \{a,b\}$ とすると、$5$ つの形は次のとおりである。
$$\text{(S1)}X\to Y\to Z\to W,\text{(S2)}X\to (Y\to Z)\to W,\text{(S3)}(X\to Y)\to Z\to W,$$
$$\text{(S4)}(X\to Y\to Z)\to W,\text{(S5)}((X\to Y)\to Z)\to W.$$

長形の構造. $\eta$ 長 $\beta$ 正規形の項は $\lambda \vec{x}.y{N}_1\cdots N_m$ の形をしている。ここで本体は原子型をもち、頭部 $y$ は変数である。したがって住人を数えるには、すべての引数を $\lambda$ で受け取ったあと、文脈の変数を頭部とする原子型の項を数えればよい。項は有限なので、再帰的な数え上げでは最小解をとる。

以下では $W=a$ の場合を数える。$a$ と $b$ を入れ替える対称性があるので、最後に $2$ 倍する。

(S1) 文脈は $x:X,y:Y,z:Z$ で、すべて原子型である。本体は型 $W$ の変数でなければならないので、住人の個数は $X,Y,Z$ のうち $W$ に等しいものの個数になる。ちょうど $1$ つになるのは $3$ 通り、$2$ 倍して $6$ 個。

(S2) 文脈は $x:X,g:Y\to Z$ である。原子型 $T$ の項の個数を $t(T)$ とすると、
$$t(T)=[X=T]+[Z=T]t(Y)$$
となる。$W=a$ のとき $(X,Y,Z)$ ごとに調べる。
- $Z=b$ のとき $t(a)=[X=a]$ である。$(a,a,b),(a,b,b)$ で $1$、$(b,a,b),(b,b,b)$ で $0$。
- $Z=a,Y=b$ のとき $t(b)=[X=b]$ なので $t(a)=[X=a]+[X=b]=1$ である。$(a,b,a),(b,b,a)$ で $1$。
- $Z=a,Y=a$ のとき $t(a)=[X=a]+t(a)$ である。$X=a$ なら $x,gx,g(gx),\dots$ と無限個。$X=b$ なら最小解は $0$。

よって住人がちょうど $1$ つのものは $4$ 通り、$2$ 倍して $8$ 個。

(S3) 文脈は $f:X\to Y,z:Z$ で、$t(T)=[Z=T]+[Y=T]t(X)$ となる。$W=a$ のとき $(X,Y,Z)$ ごとに調べる。
- $Z=a,Y=b$ のとき $t(a)=1$ である（$2$ 通り）。
- $Z=a,Y=a$ のとき、$X=a$ なら無限個。$X=b$ なら $t(b)=0$ なので $t(a)=1$。
- $Z=b,Y=b$ のとき $0$。
- $Z=b,Y=a$ のとき $t(a)=t(X)$ である。$X=b$ なら $t(b)=1$ で $1$。$X=a$ なら最小解は $0$。

よってちょうど $1$ つのものは $4$ 通り、$2$ 倍して $8$ 個。

(S4) 文脈は $f:X\to Y\to Z$ だけで、原子型の変数がない。型 $W$ の項は $f{N}_1{N}_2$ の形しかなく、$N_1:X$ もまた $f$ の適用でなければならない。これは無限に後退するので有限の項はできず、住人は $0$ 個である。

(S5) 文脈は $F:(X\to Y)\to Z$ である。本体は $F(\lambda x^X.N)$ の形しかないので $Z=W=a$ が必要であり、$N$ は型 $Y$ の項である。
- $Y=b(\ne Z)$ のとき、$N$ は変数 $x$ のみなので $X=b$ が必要である。$(b,b,a)$ で住人は $\lambda F.F(\lambda x.x)$ の $1$ つ。$(a,b,a)$ では $0$。
- $Y=a=Z$ のとき、$X=a$ なら無限個。$X=b$ なら $N=F(\lambda x^{\prime }.N^{\prime })$ が無限に続くので $0$。

よってちょうど $1$ つのものは $1$ 通り、$2$ 倍して $2$ 個。

合計. 住人をちょうど $1$ つもつ型の個数は
$$6+8+8+0+2=24.$$

矢印数 3 の型は、木の形が $C_3=5$ 通り、原子型の配置が $2^4=16$ 通りで、全部で $80$ 個ある。これを最上位の引数の個数 $n$ で分け、それぞれ $\beta$ 正規形かつ $\eta$ 長形の住人を数える。型の末尾の原子型を $c$ とする。住人の本体は、文脈中の変数 $x:{\sigma }_1\to \cdots \to {\sigma }_k\to c$ を頭にとり、各 ${\sigma }_j$ の住人を引数に適用した形になる。

$n=3$（型 $A_1\to A_2\to A_3\to c$、各 $A_i$ は原子型）: 住人は、$A_i=c$ となる $i$ ごとに 1 つ ($\lambda x_1{x}_2{x}_3.x_i$) である。ちょうど 1 つになるのは、$A_1,A_2,A_3$ のうち $c$ に等しいものがちょうど 1 つのときで、$c$ の選び方 2 通り、位置 3 通り、残りは $c$ でない原子型に定まるので $2\cdot 3=6$ 個。

$n=2$（型 $(p\to q)\to r\to c$ と $r\to (p\to q)\to c$）: どちらも文脈は $f:p\to q,x:r$ で同じなので、住人の数も同じである。原子型 $e$ の項の個数を $t(e)$ とおくと $t(e)=[r=e]+[q=e]t(p)$ となる（$[\cdot ]$ は成り立てば 1、成り立たなければ 0）。
- $q\ne c$ のとき: $t(c)=[r=c]$。ちょうど 1 つになるのは $r=c$ のときで、$(p,c)$ の選び方より 4 型。
- $q=c,p=c$ のとき: $r=c$ なら $x,fx,ffx,\dots$ と無限個、$r\ne c$ なら 0 個。
- $q=c,p\ne c$ のとき: $t(c)=[r=c]+[r=p]=1$ となり、$c$ と $r$ の選び方より 4 型。

合計は 1 つの形あたり 8 型、2 つの形で 16 型。

$n=1$（型 ${\tau }_1\to c$、${\tau }_1$ の矢印数は 2）:
- ${\tau }_1=p\to q\to d$: 原子型の変数が文脈にないので、項を作るたびに引数の住人がさらに必要になり、住人は 0 個。
- ${\tau }_1=(p\to q)\to d$: 住人をもつには $d=c$ が必要。$q=c$ のときは、$p=c$ なら無限個、$p\ne c$ なら 0 個。$q\ne c$ のときは $p=q$ のときだけ住人 $\lambda x.x(\lambda y.y)$ がちょうど 1 つ。型は $((q\to q)\to c)\to c$（$q\ne c$）で、$c$ の選び方より 2 型。

合計: $6+16+2=24$。

検算として、型の総数は $16+32+32=80$ となり、場合分けは漏れなく重複もない。