型の住人（η 長 β 正規形）の数え上げ

型 $A_{1} \to \dots \to A_{n} \to a$ の η 長 β 正規形の閉じた項を、仮定 $x_{i} : A_{i}$ のうち結論が $a$ のものを頭に選び引数を再帰的に埋める形で場合分けし、 $((a \to b) \to (a \to b) \to c) \to \dots \to c$ のような型の住人の個数を求められる

前提

単純型付けと型の数え上げ（大学院数学計算理論・ラムダ計算）

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

算数中学高校大学大学院

読み込み中…

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

一覧で見る（前提が先）

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

説明

単純型付きラムダ計算で、与えられた型をもつ閉じた項（型の住人）が「本質的に何通りあるか」を数えます。項を η 長 β 正規形という決まった形にそろえると、項は「どの仮定を頭に使うか」と「その引数をどう埋めるか」の選択の列で表され、樹形図と積・和の法則で数えられます。型を命題とみたときの証明の数え上げに当たり、型の構造の理解や、型から項が 1 つに決まるか（プログラムの一意性）の判定に使います。

なぜそうしてよいのか

β 正規形の項を考えます。項が $λ$ 抽象なら中身を見ます。 $λ$ 抽象でないなら、それは適用 $h M_{1} \dots M_{k}$ を左から展開した形で、頭 $h$ は $λ$ 抽象ではありえません（ $λ$ 抽象に引数を適用すると β 基になってしまうため）。頭は適用でもないので、頭は変数です。したがって β 正規形はいつも $λ x_{1} \dots x_{m} . y M_{1} \dots M_{k}$ （ $y$ は変数、各 $M_{j}$ も β 正規形）の形をしています。

さらに η 長（η-long）とは、「矢印型の項は必ず $λ$ で包み、変数の適用は原子型になるまで引数を全部与える」という約束です。たとえば $g : a \to b$ をそのまま引数に渡さず $λ z . g z$ と書きます。この約束のもとでは、型 $A_{1} \to \dots \to A_{n} \to a$ （ $a$ は原子型）の項は必ず $λ x_{1} : A_{1} \dots x_{n} : A_{n} . y M_{1} \dots M_{k}$ となり、頭 $y$ はそのとき使える変数のうち型が $B_{1} \to \dots \to B_{k} \to a$ （結論がちょうど $a$ ）のもの、 $M_{j}$ は型 $B_{j}$ の η 長 β 正規形です。どの閉じた項も βη 変換でちょうど 1 つの η 長 β 正規形（束縛変数の名前の付け替えを除く）に移ることが知られているので、この形の項を数えればよく、形が違えば別の住人です。

この形は「ゴール（いま作るべき型）」と「文脈（使える変数）」の組で再帰的に決まります。ゴールが矢印型なら引数を文脈に足して結論の原子型をゴールにし、原子型 $a$ なら結論が $a$ の変数を頭に選んで、その引数の型を新しいゴールにします。選び方は頭ごとに和、引数ごとに積で数えます。頭の候補がなければその分岐は $0$ 通りです。無限個になるかどうかには注意が要ります。ある（文脈, ゴール） $S$ から分岐をたどって、同じゴールで文脈の型が少なくとも元と同じだけそろった組に戻ってくる（循環する）とします。この循環をいくらでも重ねられるのは、(i) 循環の途中で埋めるほかの引数がすべて住人をもち、(ii) $S$ 自身に住人が少なくとも 1 つある（循環を止める「基底」がある）ときに限ります。このとき循環を $0, 1, 2, \dots$ 回重ねた項がすべて別の住人になって無限個です。基底がなければ循環は永久に終わらず、項は 1 つも完成しません。たとえば $(a \to a) \to a$ では、ゴール $a$ の頭の候補は $f : a \to a$ だけで、その引数のゴールがまた $a$ になります。 $f (f (f \dots))$ は有限の項にならないので、住人は $0$ 個です。

手順

型を右結合で $A_{1} \to \dots \to A_{n} \to a$ （ $a$ は原子型）と読み、仮定 $x_{1} : A_{1}, \dots, x_{n} : A_{n}$ を文脈に入れる。ゴールは原子型 $a$
文脈の変数のうち、結論（矢印の一番右）がゴールの原子型と一致するものを頭の候補としてすべて挙げる。候補がなければ $0$ 通り
各候補 $y : B_{1} \to \dots \to B_{k} \to a$ について、引数 $M_{1}, \dots, M_{k}$ のゴールを $B_{1}, \dots, B_{k}$ とする。 $B_{j}$ が矢印型なら、その仮定を新しい変数として文脈に足してから（ $λ$ で包んで）同じ手順を再帰的に行う
頭の選び方ごとの個数は引数の個数の積、全体は頭の候補にわたる和: $N (Γ, a) = \sum_{y} \prod_{j} N (Γ_{j}, B_{j})$
同じゴール（文脈の型は元以上）に戻る循環があるときは、循環の途中のほかの引数がすべて住人をもち、かつそのゴールに循環を使わない住人が少なくとも 1 つあるときに限り無限個と判定する。基底がなければその分岐は $0$ 個（例: $(a \to a) \to a$ は $0$ 個）

例題

原子型 $a, b, c$ について、型 $((a \to b) \to c) \to (a \to b) \to (a \to b) \to a \to c$ をもつ閉じた η 長 β 正規形の項の個数を求めよ。

例題の解答

【手順 1】右結合で読むと、仮定は $F : (a \to b) \to c$ , $g : a \to b$ , $h : a \to b$ , $x : a$ で、ゴールは $c$ 。

【手順 2】結論が $c$ の変数は $F$ だけ。よって項は $λ F g h x . F M$ の形。

【手順 3】 $M$ のゴールは $a \to b$ で矢印型なので、新しい変数 $z : a$ を文脈に足して $M = λ z . P$ , $P : b$ とする。文脈は $F, g, h, x, z$ 。
- $P$ （ゴール $b$ ）の頭の候補（手順 2）: 結論が $b$ の変数は $g$ と $h$ の 2 つ。
- どちらも引数は型 $a$ を 1 つとる。ゴール $a$ の頭の候補は $x$ と $z$ の 2 つで、どちらも引数なし（ $a$ は原子型）。

【手順 4】 $P$ の個数は、頭 $g$ の場合 $2$ 、頭 $h$ の場合 $2$ で、和は $2 + 2 = 4$ 。 $F$ の引数は $M$ の 1 つなので、全体は $1 \times 4 = 4$ 。

【手順 5】たどった分岐のゴールは $c \to (a \to b) \to b \to a$ と進むだけで、同じゴールに戻る循環はないので有限。住人は
$λ F g h x . F (λ z . g x)$ , $λ F g h x . F (λ z . g z)$ , $λ F g h x . F (λ z . h x)$ , $λ F g h x . F (λ z . h z)$ の $4$ 個。

答え: $4$

よくある誤り

η 長でない項を別に数えてしまう誤り（例: 上の例で $λ F g h x . F g$ を 5 個目とする）。 $F g$ は η 長形 $F (λ z . g z)$ と βη 同値なので同じ住人。正しくは η 長形だけを数える。
内側の $λ$ で入った変数を文脈に入れ忘れる誤り（例: 上の例で $F (λ z . g □)$ の $□ : a$ に $x$ だけを入れて 1 通りとし、全体を 2（頭が $g, h$ ） $\times 1 = 2$ 個とする）。正しくは $z : a$ も使えるので $□$ は $x, z$ の 2 通りで、全体は 2（頭が $g, h$ ） $\times 2 = 4$ 個。
結論の原子型ではなく型全体で頭を選んでしまう誤り（例: ゴール $b$ に対して $g : a \to b$ は型が $b$ でないから使えないとする）。正しくは結論が $b$ なら頭にでき、足りない引数 $a$ を新たなゴールとして埋める。
循環があれば必ず無限個、または循環を 1 回で打ち切って有限個と数える誤り。 $(a \to a) \to a \to a$ では基底 $x$ があるので $λ f x . f^{n} x$ （ $n \geq 0$ ）がすべて住人で無限個（ $λ f x . x$ と $λ f x . f x$ の 2 個ではない）。一方 $(a \to a) \to a$ では基底がないので住人は $0$ 個（無限個ではない）。

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

入口の問題

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

型の住人（η 長 β 正規形）の数え上げ

前提

説明

なぜそうしてよいのか

手順

例題

よくある誤り

入口の問題

この技能を使う問題