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

互いに異なる 3 つの原子型 $a,b,c$ をもつ単純型付きラムダ計算（チャーチ流、定数なし）を考える。矢印型は右結合（$A\to B\to C=A\to (B\to C)$）とし、$\alpha$ 同値な項は同一視する。型 $A$ の閉じた項のうち、$\beta$ 正規形かつ $\eta$ 長形（$\eta$-long form）であるものを $A$ の住人とよぶ。（住人は、型 $A$ の閉じた項の $\beta \eta$ 同値類と 1 対 1 に対応する。）

型
$$T=((a\to b)\to (a\to b)\to c)\to (a\to a\to b)\to (b\to c)\to a\to a\to c$$
の住人の個数を求めよ。

互いに異なる $3$ つの原子型 $p,q,r$ をもち、定数をもたない単純型付きラムダ計算（チャーチ流）を考える。型は
$$\tau ::=p\mid q\mid r\mid (\tau \to \tau )$$
で生成される式とし、括弧の付け方（木としての形）が異なる型や、原子型の並びが異なる型は異なる型とみなす（たとえば $((p\to q)\to r)$ と $(p\to (q\to r))$ は異なる型であり、$(p\to q)$ と $(q\to p)$ も異なる型である）。

記号 $\to$ をちょうど $3$ 個含む型の個数を求めよ。

互いに異なる $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 つだけもつ単純型付きラムダ計算（チャーチ流、定数なし）を考える。矢印型は右結合（$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$）の個数を求めよ。

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

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