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

難易度 3大学院入試の専門科目の標準レベル大学院数学計算理論・ラムダ計算

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

この問題で使うもの

型の住人（η 長 β 正規形）の数え上げ（説明と入口の問題）

この問題を解けるようになるまで（9 技能）

算数中学高校大学大学院

読み込み中…

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

一覧で見る（前提が先）

ヒント

行き詰まったら、上から順に 1 つずつ開いてください。

ヒント 1

$β$ 正規 $η$ 長形の本体 $M$ は型 $o$ の項で、「型 $o$ の変数」「 $f N_{1} N_{2}$ 」「 $G (λ y . N^{'})$ 」のどれかの形になることを確かめ、文脈にある型 $o$ の変数の個数を追跡しよう。

ヒント 2

型 $o$ の変数が $k$ 個ある文脈で $f, G$ の出現回数の和が $n$ の項の個数を $a (n, k)$ とすると、 $a (0, k) = k$ 、 $a (n, k) = a (n - 1, k + 1) + \sum_{i + j = n - 1} a (i, k) a (j, k)$ 。求めるのは $a (4, 0)$ 。

ヒント 3

$a (1, k) = k^{2} + k + 1$ 、 $a (2, 0) = 3$ 、 $a (2, 1) = 13$ 、 $a (2, 2) = 41$ となる。次に $a (3, 1)$ を求め、 $a (4, 0) = a (3, 1) + 2 a (1, 0) a (2, 0)$ を計算する。

答えと解説

答えを見る

82

結果を記録する（このブラウザにだけ保存されます）:

解説を読む

項の形の決定. $β$ 正規形かつ $η$ 長形の項では、型 $o$ の部分項は「頭変数に、その変数の型が要求する個数の引数をすべて与えたもの」であり、矢印型の引数は $λ$ 抽象の形で現れる。本体 $M$ の文脈にある変数は $f : o \to o \to o$ 、 $G : (o \to o) \to o$ と、 $G$ の引数の $λ$ で束縛された型 $o$ の変数たちである。したがって、型 $o$ の項 $N$ は次のどれかである。
- 文脈にある型 $o$ の変数 $x$
- $f N_{1} N_{2}$ （ $N_{1}, N_{2}$ は型 $o$ の項）
- $G (λ y^{o} . N^{'})$ （ $N^{'}$ は $y$ を文脈に加えた型 $o$ の項）

$α$ 同値で同一視するので、各 $λ$ で新しい（互いに異なる）変数が束縛されると考えてよく、変数の選び方は「文脈にある型 $o$ の変数の個数」だけある。

漸化式. 型 $o$ の変数が $k$ 個ある文脈で、 $f, G$ の出現回数の和がちょうど $n$ である型 $o$ の項の個数を $a (n, k)$ とする。上の分類から
$a (0, k) = k, a (n, k) = a (n - 1, k + 1) + i + j = n - 1 \sum a (i, k) a (j, k) (n \geq 1)$
が成り立つ（第 1 項が $G (λ y . N^{'})$ 、第 2 項が $f N_{1} N_{2}$ の場合）。求める個数は $a (4, 0)$ である。

計算.
$a (1, k) = a (0, k + 1) + a (0, k)^{2} = k^{2} + k + 1$ より
$a (1, 0) = 1, a (1, 1) = 3, a (1, 2) = 7, a (1, 3) = 13$ 。

$a (2, k) = a (1, k + 1) + 2 a (0, k) a (1, k)$ より
$a (2, 0) = a (1, 1) + 0 = 3$ 、
$a (2, 1) = a (1, 2) + 2 \cdot 1 \cdot 3 = 7 + 6 = 13$ 、
$a (2, 2) = a (1, 3) + 2 \cdot 2 \cdot 7 = 13 + 28 = 41$ 。

$a (3, 1) = a (2, 2) + 2 a (0, 1) a (2, 1) + a (1, 1)^{2} = 41 + 26 + 9 = 76$ 。

$a (4, 0) = a (3, 1) + (a (0, 0) a (3, 0) + a (1, 0) a (2, 0) + a (2, 0) a (1, 0) + a (3, 0) a (0, 0)) = 76 + (0 + 3 + 3 + 0) = 82$ 。

（確認： $a (2, 0) = 3$ に対応する項は $G (λ x . G (λ y . x))$ 、 $G (λ x . G (λ y . y))$ 、 $G (λ x . f x x)$ の 3 つである。）

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

別解

$f : o \to o \to o$ , $G : (o \to o) \to o$ のもとで、型 $o$ の $β$ 正規 $η$ 長形の項 $M$ は次のいずれかである。
- 文脈中の型 $o$ の変数 $x$ （ $G$ の引数の $λ$ で束縛されたもの）。重み 0。
- $f A B$ （ $A, B$ は型 $o$ の項）。重み $1 + w (A) + w (B)$ 。
- $G (λ x^{o} . N)$ （ $N$ は型 $o$ の項で、文脈に $x$ が 1 つ増える）。重み $1 + w (N)$ 。

ここで重みは $f, G$ の出現回数とする。文脈にある型 $o$ の変数が $n$ 個のとき、重み $k$ の項の個数を $t_{n} (k)$ とおく。生成関数 $T_{n} (z) = \sum_{k} t_{n} (k) z^{k}$ は
$T_{n} = n + z T_{n}^{2} + z T_{n + 1}$
を満たす。これを係数比較して順に計算する。

$t_{n} (0) = n$
$t_{n} (1) = n^{2} + n + 1$
$t_{n} (2) = 2 n t_{n} (1) + t_{n + 1} (1) = 2 n^{3} + 3 n^{2} + 5 n + 3$
$t_{n} (3) = 2 t_{n} (0) t_{n} (2) + t_{n} (1)^{2} + t_{n + 1} (2)$
$t_{n} (4) = 2 t_{n} (0) t_{n} (3) + 2 t_{n} (1) t_{n} (2) + t_{n + 1} (3)$

$t_{0} (4)$ に必要な値は次のとおり。
- $t_{0} (1) = 1$ , $t_{0} (2) = 3$
- $t_{1} (1) = 3$ , $t_{1} (2) = 13$ , $t_{2} (2) = 41$
- $t_{1} (3) = 2 \cdot 1 \cdot 13 + 3^{2} + 41 = 76$

よって
$t_{0} (4) = 2 \cdot 0 \cdot t_{0} (3) + 2 \cdot 1 \cdot 3 + 76 = 82.$

検算: $t_{0} (1) = 1$ （ $G (λ x . x)$ のみ）、 $t_{0} (2) = 3$ （ $G (λ x . f xx)$ , $G (λ x . G (λ y . x))$ , $G (λ x . G (λ y . y))$ ）は直接数え上げと一致した。

答え: 82

この問題の確認

AI が作成した問題です。公開前に次の確認を行いました。

別の AI が答えを見ずに 3 回解き、3 回とも同じ答えになりました
プログラムで答えを計算し直し、一致を確認しました
AI の査読で、条件・解説・表記を確認しました
答えの正しさについて慎重に扱うべき点が見つからなかったため、自動で公開しました

確認の方法について

間違いを報告する

この問題の誤り・分かりにくい点・難易度や学年のずれを知らせる