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

原子型として $o$ ただ 1 つをもち、定数をもたない単純型付きラムダ計算（チャーチ流）を考える。型は $$\tau ::=o\mid (\tau \to \tau )$$ で生成される式とし、括弧の付け方（木としての形）が異なる型は異なる型とみなす。型 $\tau$ が住人をもつとは、型 $\tau$ の閉じた項（自由変数をもたない項）が存在することをいう。

矢印 $\to$ をちょうど $5$ 個含む型（したがって $o$ をちょうど $6$ 個含む型）のうち、住人をもつものの個数を求めよ。

互いに異なる $2$ つの原子型 $a,b$ をもち、定数をもたない単純型付きラムダ計算（チャーチ流）を考える。型は
$$\tau ::=a\mid b\mid (\tau \to \tau )$$
で生成される式とする。括弧の付け方（木としての形）または原子型の配置が異なる型は、異なる型とみなす。$\to$ は右結合とし、型に現れる $\to$ の個数をその型の矢印数とよぶ。

型 $\tau$ の住人とは、型 $\tau$ をもつ閉項であって、$\beta$ 正規形かつ $\eta$ 長形（long normal form）であるもののこととする。住人は $\alpha$ 同値なものを同一視して数える。

矢印数がちょうど $3$ である型のうち、住人をちょうど $1$ つだけもつ型の個数を求めよ。

原子型を $o$ ただ 1 つだけもつ単純型付きラムダ計算（チャーチ流、定数なし）を考える。型は
$$\tau ::=o\mid (\tau \to \tau )$$
で生成されるものとし、括弧の付け方が異なる型は異なる型とみなす（たとえば $(o\to o)\to o$ と $o\to (o\to o)$ は異なる型である）。型 $\tau$ に含まれる記号 $\to$ の個数を $\tau$ の矢印の個数という。

型 $\tau$ をもつ閉じた項（自由変数をもたない項）が少なくとも 1 つ存在するとき、$\tau$ は住人をもつという。矢印の個数がちょうど $6$ である型のうち、住人をもつものの個数を求めよ。

互いに異なる $2$ つの原子型 $a,b$ をもち、定数をもたない単純型付きラムダ計算（チャーチ流）を考える。矢印型は右結合（$A\to B\to C=A\to (B\to C)$）とし、$\alpha$ 同値な項は同一視する。型
$$T=(a\to a\to b)\to (a\to b)\to a\to a\to b$$
をもつ閉じた項で、η 長 β 正規形であるものの個数を求めよ。

原子型を $o$ ただ 1 つだけもつ単純型付きラムダ計算（チャーチ流、定数なし）を考える。矢印型は右結合（$A\to B\to C=A\to (B\to C)$）とし、$\alpha$ 同値な項は同一視する。型
$$\tau =(o\to o\to o)\to ((o\to o)\to o)\to o$$
の閉じた項で、$\beta$ 正規形かつ $\eta$ 長形（$\beta$-normal $\eta$-long form）であるものは、ある項 $M$ を用いて $\lambda f^{o\to o\to o}.\lambda G^{(o\to o)\to o}.M$ の形に書ける。このような項のうち、$M$ の中に変数 $f$ と $G$ が合わせてちょうど $4$ 回出現するもの（$f$ の出現回数と $G$ の出現回数の和が $4$）の個数を求めよ。