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

住人をもつための条件. 次の主張を型の構成に関する帰納法で示す。

> 任意の型 $A$ について、「$A$ が住人をもつ」か「型 $A\to o$ と型 $o\to A$ がともに住人をもつ」のどちらか一方がちょうど成り立つ。

まず、両方が同時に成り立つことはない。もし $M:A$ と $h:A\to o$ が閉じた項なら $hM$ は型 $o$ の閉じた項になるが、単純型付きラムダ計算は強正規化性をもつので、その $\beta$ 正規形は型 $o$ の閉じた正規形である。閉じた正規形は抽象 $\lambda x.N$ の形か、変数を先頭にもつ $x{N}_1\cdots N_k$ の形だが、前者の型は矢印型であり、後者は閉じていないので、型 $o$ の閉じた正規形は存在しない。よって $o$ は住人をもたず、矛盾。

少なくとも一方が成り立つことを帰納法で示す。$A=o$ のときは $\lambda x.x$ が $o\to o$ の住人なので後者が成り立つ。$A=B\to C$ のとき、帰納法の仮定を $B,C$ に使う。
- $C$ が住人 $M$ をもつ場合: $\lambda b.M$ が $A$ の住人。
- $C$ が住人をもたず、$B$ も住人をもたない場合: 閉じた項 $h_B:B\to o$ と $k_C:o\to C$ があるので、$\lambda b.k_C(h_{B}b)$ が $A$ の住人。
- $C$ が住人をもたず、$B$ が住人 $N$ をもつ場合: 閉じた項 $h_C:C\to o$, $k_C:o\to C$ を使うと、$\lambda u.h_C(uN):A\to o$、$\lambda y.\lambda b.k_{C}y:o\to A$ となり後者が成り立つ。

以上より、次がわかる。
$$B\to C\text{ が住人をもつ}⟺C\text{ が住人をもつ、または }B\text{ が住人をもたない}.$$
つまり、$o$ を「偽」、住人をもつことを「真」と読むと、$\to$ は含意の真理値表に従う。

数え上げ. 矢印を $n$ 個含む型（葉が $n+1$ 個の二分木）全体の個数はカタラン数 $C_n=\frac{1}{n+1}\left(\genfrac{}{}{0ex}{}{2n}{n}\right)$ である。そのうち住人をもつもの・もたないものの個数を $T_n,F_n$ とする（$T_n+F_n=C_n$）。$B\to C$ が住人をもたないのは「$B$ が住人をもち、$C$ が住人をもたない」ときに限るので、$B$ の矢印の個数を $i$、$C$ の矢印の個数を $j$（$i+j=n-1$）として
$$F_0=1,F_n=\sum _{i+j=n-1}{T}_i{F}_j(n\ge 1).$$

• $n=0$: $C_0=1$, $F_0=1$, $T_0=0$
• $n=1$: $F_1=T_0{F}_0=0$, $T_1=1-0=1$
• $n=2$: $F_2=T_0{F}_1+T_1{F}_0=0+1=1$, $T_2=2-1=1$
• $n=3$: $F_3=T_0{F}_2+T_1{F}_1+T_2{F}_0=0+0+1=1$, $T_3=5-1=4$
• $n=4$: $F_4=T_0{F}_3+T_1{F}_2+T_2{F}_1+T_3{F}_0=0+1+0+4=5$, $T_4=14-5=9$
• $n=5$: $F_5=T_0{F}_4+T_1{F}_3+T_2{F}_2+T_3{F}_1+T_4{F}_0=0+1+1+0+9=11$, $T_5=42-11=31$

したがって求める個数は $31$ である。

カリー・ハワード対応により、型が住人をもつことは、その型を含意のみの直観主義命題論理の論理式（命題変数は $o$ だけ）とみて証明可能であることと同値である。

命題変数が 1 つ $p$ のとき、含意のみの論理式は直観主義論理で $p$ か $\top$（$=p\to p$）のどちらかと同値になる。実際 $\top \to X\equiv X$、$X\to \top \equiv \top$、$p\to p\equiv \top$、$(p\to p)\to p\equiv p$ より、$A\to B$ の値は
- $B$ の値が $p$ かつ $A$ の値が $\top$ のとき $p$
- それ以外（$B$ が $\top$、または $A$ も $B$ も $p$）のとき $\top$
である。住人をもつ型 $=$ 値が $\top$ の型。

矢印をちょうど $n$ 個含む型の総数は、カタラン数 $c_n=1,1,2,5,14,42$（$n=0,\dots ,5$）。値が $p$（住人をもたない）の個数を $u_n$、住人をもつ個数を $h_n=c_n-u_n$ とする。$u_0=1$（型 $o$）、$n\ge 1$ では $u_n={\sum }_{i+j=n-1}{h}_i{u}_j$（$A$ が住人をもち、$B$ が住人をもたない場合）。

• $n=0$: $u_0=1,h_0=0$
• $n=1$: $u_1=h_0{u}_0=0,h_1=1$
• $n=2$: $u_2=h_0{u}_1+h_1{u}_0=1,h_2=1$
• $n=3$: $u_3=h_0{u}_2+h_1{u}_1+h_2{u}_0=0+0+1=1,h_3=4$
• $n=4$: $u_4=h_0{u}_3+h_1{u}_2+h_2{u}_1+h_3{u}_0=0+1+0+4=5,h_4=9$
• $n=5$: $u_5=h_0{u}_4+h_1{u}_3+h_2{u}_2+h_3{u}_1+h_4{u}_0=0+1+1+0+9=11,h_5=42-11=31$

検算: $n=2$ で住人をもたない型は $(o\to o)\to o$ のみ（$o\to o\to o$ は $\lambda x.\lambda y.x$ が住人）で $u_2=1$ に合う。$n=3$ では $((o\to o)\to o)\to o$ のみが住人をもたない（ここで $((o\to o)\to o)\to o$ の $A=(o\to o)\to o$ が値 $p$ なので $\top$ …）ように見えるが、定義どおり $A$ が住人をもち $B=o$ の型 $(o\to o)\to o$ を $A$ とした $o\to$ ではなく、$A=(o\to o)$、$B=(o\to o)\to o$ すなわち $(o\to o)\to ((o\to o)\to o)$ が唯一の住人をもたない型で、$u_3=1$。

よって求める個数は $31$。