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

1. カリー・ハワード対応への言い換え。 単純型付きラムダ計算で型 $\tau$ が住人をもつことは、$\tau$ を命題変数 $o$ だけからなる含意 $\to$ だけの論理式とみたとき、$\tau$ が直観主義命題論理（含意のみの断片）で証明可能であることと同値である。

2. 1 変数の含意論理式の分類。 矢印の個数についての帰納法で、すべての型 $\tau$ は次のどちらか一方を満たすことを示す。
- (T) $\tau$ は証明可能（住人をもつ）
- (F) $\tau$ と $o$ は互いに導ける（$\tau ⊢o$ かつ $o⊢\tau$）

$\tau =o$ は (F)。$\tau =A\to B$ とし、$A,B$ について主張が成り立つとする。
- $B$ が (T) のとき：$B$ の証明から $A\to B$ が証明できるので (T)。
- $B$ が (F) で $A$ が (F) のとき：$A⊢o⊢B$ より $⊢A\to B$ なので (T)。
- $B$ が (F) で $A$ が (T) のとき：$A\to B$ と（証明可能な）$A$ から $B$、したがって $o$ が導ける。逆に $o$ から $B$ が導けるので $A\to B$ も導ける。よって (F)。

さらに $o$ 自身は証明可能でない（古典論理で $o$ を偽とする付値で偽になり、直観主義で証明可能な式は古典的にも恒真だから）。(F) の型は $o$ と同値なので証明不能である。したがって (T) と (F) は排反で、
$$A\to B\text{が (F)}⟺A\text{が (T) かつ}B\text{が (F)}$$
が成り立つ。これは「$o$ を偽として古典的に真理値を計算し、真になる型がちょうど住人をもつ型である」ということでもある。

3. 個数の漸化式。 矢印の個数が $n$ の型の総数は、内部節点 $n$ 個の二分木の個数であるカタラン数 $C_n$ である（$C_0,\dots ,C_6=1,1,2,5,14,42,132$）。住人をもつものの個数を $T_n$、もたないものの個数を $F_n$ とすると、$T_n+F_n=C_n$、$T_0=0,F_0=1$ で、$A\to B$ の $A,B$ の矢印の個数を $i,j(i+j=n-1)$ として
$$F_n=\sum _{i=0}^{n-1}{T}_i{F}_{n-1-i}(n\ge 1).$$

順に計算する。
- $F_1=T_0{F}_0=0$、$T_1=1-0=1$
- $F_2=T_0{F}_1+T_1{F}_0=0+1=1$、$T_2=2-1=1$
- $F_3=T_0{F}_2+T_1{F}_1+T_2{F}_0=0+0+1=1$、$T_3=5-1=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$
- $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$
- $F_6=T_0{F}_5+T_1{F}_4+T_2{F}_3+T_3{F}_2+T_4{F}_1+T_5{F}_0=0+5+1+4+0+31=41$、$T_6=132-41=91$

（確認：$n=2$ では $o\to o\to o$ が住人 $\lambda x^o.\lambda y^o.x$ をもち、$(o\to o)\to o$ は住人をもたないので $T_2=1$。$n=3$ では $(o\to o\to o)\to o$ だけが住人をもたず $T_3=4$ で、漸化式と一致する。）

よって求める個数は $91$ である。

型を含意論理式とみなす（カリー・ハワード対応）。閉じた項が存在することは、含意だけの直観主義論理（最小論理）で証明可能であることと同値。

【1 変数の場合の簡約】 原子が $o$ だけのとき、すべての型は直観主義的に $o$ か $\top :=o\to o$ のどちらかと同値である。実際、同値は $\to$ について合同なので、帰納的に $A\to B$ を調べればよい。$B\equiv \top$ なら $A\to B\equiv \top$。$B\equiv o$ のとき、$A\equiv \top$ なら $A\to B\equiv o$、$A\equiv o$ なら $A\to B\equiv o\to o\equiv \top$。$o$ は証明可能でない（住人がない）ので、型が住人をもつことは $\top$ と同値であることと同じ。

この規則は $o$ を偽、$\top$ を真とみなした古典的な真理値計算と一致する（$A\to B$ が偽になるのは $A$ が真で $B$ が偽のときだけ）。よって、住人をもつ型の個数は、$o$ を偽としたとき真になる型の個数に等しい。

【数え上げ】 矢印の個数 6 の型は $o$ を 7 個含む二分木で、全部で Catalan 数 $C_6=132$ 個。$n$ 個の $o$ をもつ型のうち偽になるものの個数を $F_n$、真になるものを $T_n$、全体を $c_n$（$c_n=1,1,2,5,14,42,132$）とする。$A\to B$ が偽になるのは $A$ が真かつ $B$ が偽のときだけなので
$F_n={\sum }_{i+j=n}{T}_i{F}_j,T_n=c_n-F_n$。
$F_1=1,T_1=0$
$F_2=T_1{F}_1=0,T_2=1$
$F_3=T_1{F}_2+T_2{F}_1=1,T_3=1$
$F_4=T_1{F}_3+T_2{F}_2+T_3{F}_1=1,T_4=4$
$F_5=T_2{F}_3+T_3{F}_2+T_4{F}_1=1+0+4=5,T_5=9$
$F_6=T_2{F}_4+T_3{F}_3+T_4{F}_2+T_5{F}_1=1+1+0+9=11,T_6=31$
$F_7=T_2{F}_5+T_3{F}_4+T_4{F}_3+T_5{F}_2+T_6{F}_1=5+1+4+0+31=41,T_7=132-41=91$。

検算: 矢印 2 個（$n=3$）では $o\to (o\to o)$ のみ住人をもち $T_3=1$。矢印 3 個（$n=4$）では 5 個の型のうち偽になるのは $((o\to o)\to o)\to o$ ではなく $(o\to (o\to o))\to o$ の 1 個だけで、$T_4=4$ と合う。

したがって答えは 91。