帰納的に自由な集合

集合X上に次のような構造を考える。

1. Xの部分集合I
2. X→Xである写像s1, s2, ..., sN （N≧1）

s1, ..., SN を任意に結合した写像を移動（move）と呼ぶことにし、その全体をMove(X)とする。一方、Σ = {s1, ..., SN}として、クリーネ・スターΣ^*を作る。すると、Σ^*→Move(X)という写像が定義できる。これは、構文的な項の意味写像と考えてよい。

次の条件を考える。

1. Iは有限集合である。
2. すべての移動m:X→Xは単射である。
3. Σ^*→Move(X) は単射である。
4. eval:Move(X)×X→X は全車である。

Σ^*I = I + ΣI + ΣΣI + ... とすると、上の条件は、XがΣ^*Iと同型なことを示す。別な言い方をすると、Xは次の再帰的定義で定義される。

1. IはXの元である。
2. xがXの元なら、s1(x), s2(x), ..., sN(x) はXの元である。
3. 以上で出来た元だけがXの元である。

XはIとΣ決まるから(I, Σ) と書いてもよい。仮にこのような集合を帰納的に自由な集合と呼んでおこう、なぜなら(I, Σ)で自由生成されているから。Σが空のときも許すと、すべての有限集合は帰納的に自由である。有限ではなく、もっとも簡単な帰納的自由集合はN = ({0}, {suc})となる。

帰納的自由集合に実効的な同値関係を入れて割った集合や、実効的な述語で定義される部分集合は帰納的と言っていいと思うが、「実効的」の定義をしなくてはならない。もう少し考えねば。