単純型付けと型の数え上げ

単純型付きラムダ計算（チャーチ流）で、閉じた項に型を付けたり型付け可能かを判定したりでき、矢印型を右結合で読める。原子型が $k$ 個で矢印が $n$ 個の型の個数 $C_{n} k^{n + 1}$ のような型の個数を求められる

前提

β 簡約と β 正規形（大学院数学計算理論・ラムダ計算）
カタラン数（大学数学離散数学・組合せ論）

この技能までの道筋（7 技能）

算数中学高校大学大学院

読み込み中…

右端（太枠）がこの技能です。左へドラッグすると、さらに前の前提をさかのぼれます。技能を押すと、そこまでの道筋が光ります。

一覧で見る（前提が先）

β 簡約と β 正規形（大学院数学計算理論・ラムダ計算）
樹形図で数え上げる（算数場合の数）
積の法則と和の法則（算数場合の数）
和の法則・積の法則と樹形図（数学A 場合の数と確率）
順列・円順列・重複順列（数学A 場合の数と確率）
組合せ（数学A 場合の数と確率）
カタラン数（大学数学離散数学・組合せ論）

説明

単純型付きラムダ計算では、原子型（ $α, β, \dots$ ）と矢印 $\to$ から型を作り、各ラムダ項に「どんな入力を受けてどんな出力を返すか」を表す型を付けます。この技能では、チャーチ流（束縛変数に型を書き込む $λ x : σ . M$ の形）の閉じた項に型を付け、型が付かない項を見分け、 $α \to β \to α$ のような矢印型を右結合で正しく読めるようになります。さらに、型の形が二分木であることを使って、原子型が $k$ 個・矢印が $n$ 個の型の個数 $C_{n} k^{n + 1}$ を求められるようになります。

なぜそうしてよいのか

型は次のように帰納的に作ります：原子型は型であり、 $σ, τ$ が型なら $(σ \to τ)$ も型である。括弧を省くときは右結合、つまり $σ \to τ \to ρ$ は $σ \to (τ \to ρ)$ と読みます。これは「 $σ$ を受け取ると『 $τ$ を受け取って $ρ$ を返す関数』を返す」という意味で、2 引数関数を 1 引数ずつ受け取る形に合っています。型付けの規則は 3 つです：(変数) 文脈に $x : σ$ があれば $x : σ$ ；(抽象) 文脈に $x : σ$ を加えて $M : τ$ なら $λ x : σ . M : σ \to τ$ ；(適用) $M : σ \to τ$ かつ $N : σ$ なら $M N : τ$ 。チャーチ流では束縛変数の型が書いてあるので、項の構造を外側からたどれば型は（付くなら）1 つに決まり、適用のところで「関数の入力の型」と「引数の型」が完全に一致するかを確かめれば型付け可能かが判定できます。たとえば $λ x : σ . xx$ では $xx$ に型が付くために $σ = σ \to τ$ が必要ですが、右辺は左辺より矢印が 1 つ多いので決して一致せず、型は付きません。

型の個数を数えるには、型を二分木とみます。矢印 $σ \to τ$ を「左の子 $σ$ 、右の子 $τ$ をもつ内部節点」、原子型を「葉」とすると、型と「葉に原子型の名前を書いた二分木」が 1 対 1 に対応します（括弧の付け方が木の形をちょうど決めるからです）。矢印が $n$ 個の型は内部節点が $n$ 個の二分木で、その形は $C_{n} = \frac{1}{n + 1} (n 2 n)$ 通りです。内部節点 $n$ 個の二分木は葉をちょうど $n + 1$ 個もち、各葉に $k$ 個の原子型から重複を許して 1 つずつ選ぶので $k^{n + 1}$ 通り。積の法則で、矢印 $n$ 個の型は $C_{n} k^{n + 1}$ 個です。

手順

型を読むときは、省かれた括弧を右から補う： $σ_{1} \to σ_{2} \to \dots \to σ_{m} \to ρ = σ_{1} \to (σ_{2} \to (\dots \to (σ_{m} \to ρ)))$
閉じた項の型付けは外側から： $λ x : σ . M$ なら文脈に $x : σ$ を加えて $M$ の型 $τ$ を求め、全体を $σ \to τ$ とする
適用 $M N$ では $M$ の型が $σ \to τ$ の形で、 $N$ の型がちょうど $σ$ であることを確かめ、 $M N : τ$ とする。一致しなければ型は付かない
型を数えるときは、型を「内部節点＝矢印、葉＝原子型」の二分木に直し、矢印の個数 $n$ と原子型の個数 $k$ を確認する
木の形の数 $C_{n} = \frac{1}{n + 1} (n 2 n)$ と葉 $n + 1$ 個へのラベルの付け方 $k^{n + 1}$ を掛けて、個数 $C_{n} k^{n + 1}$ を求める

例題

原子型が $α, β$ の 2 つだけの単純型を考える。型は「原子型は型であり、 $σ, τ$ が型なら $(σ \to τ)$ も型である」として作られるものとし、括弧の付け方が異なる型は異なる型とみなす（例: $(α \to β) \to α$ と $α \to (β \to α)$ は異なる）。矢印 $\to$ をちょうど 3 個含む型の個数を求めよ。

例題の解答

【手順 4】型を二分木に直す。矢印 1 個が内部節点 1 個にあたるので、求めるものは「内部節点が 3 個の二分木で、各葉に $α$ か $β$ を書いたもの」の個数である。原子型は $k = 2$ 個、矢印は $n = 3$ 個。

【手順 5】木の形は $C_{3} = \frac{1}{4} (3 6) = 5$ 通り。実際、括弧を省かずに書くと
$((* \to *) \to *) \to *, (* \to (* \to *)) \to *, (* \to *) \to (* \to *), * \to ((* \to *) \to *), * \to (* \to (* \to *))$
の 5 つである。どの形も葉（ $*$ の位置）は $3 + 1 = 4$ 個あり、それぞれに $α, β$ のどちらかを入れるので $2^{4} = 16$ 通り。積の法則より
$C_{3} \cdot 2^{4} = 5 \cdot 16 = 80.$

答え: $80$

よくある誤り

矢印を左結合で読んでしまう誤り。 $α \to β \to α$ を $(α \to β) \to α$ と読むのは誤りで、正しくは $α \to (β \to α)$ 。たとえば $λ x : α . λ y : β . x$ の型は $α \to β \to α = α \to (β \to α)$ である。
括弧の付け方を数えずに、原子型の並べ方だけ数えてしまう誤り。矢印 $n$ 個の型を $k^{n + 1}$ 個とするのは誤りで、木の形の数を掛けて $C_{n} k^{n + 1}$ が正しい（ $n = 3, k = 2$ なら $16$ ではなく $80$ ）。
カタラン数の添字を葉の個数で取ってしまう誤り。葉が $n + 1$ 個だからといって $C_{n + 1} k^{n + 1}$ とするのは誤りで、木の形の数は内部節点（矢印）の個数 $n$ に対する $C_{n}$ である（ $n = 2$ なら形は $(* \to *) \to *$ と $* \to (* \to *)$ の $C_{2} = 2$ 通り）。
適用で型が「だいたい合えばよい」としてしまう誤り。 $M : σ \to τ$ , $N : σ^{'}$ のとき $M N$ に型が付くのは $σ^{'} = σ$ のときだけ。たとえば $λ x : σ . xx$ は $σ = σ \to τ$ が必要だが、両辺の矢印の個数が異なるので型付け不可能である。

この説明は AI が書き、別の AI が例題を独立に解いて答えを確かめ、説明を一歩ずつ査読しました。

入口の問題

難易度 1（大学院の講義の例題レベル）
互いに異なる $3$ つの原子型 $p, q, r$ をもち、定数をもたない単純型付きラムダ計算（チャーチ流）を考える。型は
$τ ::= p ∣ q ∣ r ∣ (τ \to τ)$
で生成される式とし、括弧の付け方（木としての形）が異なる型や、原子型の並びが異なる型は異なる型とみなす（たとえば $((p \to q) \to r)$ と $(p \to (q \to r))$ は異なる型であり、 $(p \to q)$ と $(q \to p)$ も異なる型である）。
記号 $\to$ をちょうど $3$ 個含む型の個数を求めよ。

この技能を使う問題

この技能の次に学べること

型の住人（η 長 β 正規形）の数え上げ（大学院数学計算理論・ラムダ計算）