言葉づかい、態度 3: 焦点

computational, computationally, computable を単に「計算的」で修飾するかも知れない。

• 計算的圏＝計算可能圏
• 計算的集合＝計算的圏の対象
• 計算的関数＝計算的圏の射＝計算可能関数

計算的圏は、高々加算な付点集合の圏に埋め込める。さらに、高々加算集合の圏にも埋め込める。

• Cptbl → PtSet_≦ω → Set_≦ω

PtSet_≦ωとSet_≦ωの中間的存在として、PtSet^nons_≦ωは、non-strict mapを許した圏。nons は allow non-strict の意味。

計算的集合の部分集合は、計算可能なものに限定すべき。計算可能＝計算的部分集合は、帰納的加算集合と一致すべき。よって、計算的部分集合＝帰納的加算集合。

計算的集合に、計算的部分集合の束を対応させると、計算的論理の計算的ハイパードクトリンになるだろう。ローヴェアの言葉で言うなら、計算的部分集合が計算的属性代数〈computational attribute algebra〉で統制されればよい。属性代数は、真偽値の代数の一般化。

計算的論理とはあらずもがなな言い方で、通常の論理は暗黙に計算的だろう。暗黙の前提をハッキリさせて、計算的論理と超越的論理の差を見る。

computational/computableの意味でΓを添えることにすると：

• Pow_Γ(X)⊆Pow(X)
• Pow(X) ⊆ Pow_Γ(X) とは限らない。
• Map_Γ(X, Y)⊆Map(X, Y)
• Map(X, Y)⊆Map_Γ(X, Y) とは限らない。

ここで、Map(-, -) = Hom_Set(-, -) = Set(X, Y), Map_Γ(-, -) = Hom_Cptbl(-, -) = Cptbl(X, Y)。

帰納構造、帰納代数

帰納的構成はよく使うが、構成（生成）された後にできる構造の話。

Xが生成された集合、Aが初期集合、c_iがコンストラクタだとする。これらを、(X, A, c₁, ..., c_n) という構造だと考える。次の記法を使う。

• X₀ := A
• X₊ := X＼A

定義より、X = X₀ + X₊。X₀の要素をプリミティブ、X₊の要素をコンポジットと呼ぶ。

(X, A, c₁, ..., c_n)が有限全域帰納構造だとは、次を満たすこと。

1. c_i:X→X は全域写像
2. c_iの余域を Im(c_i)に制限すると双射。
3. c₀:A→X を埋め込みとすると、c₀, c₁, ..., c_n は協力して全射〈jointly serjective〉、あるいは被覆〈covering〉。

C = {c₁, ..., c_n} として、記号的な構造として、A×C^*があり、標準的な全射 A×C^*→X がある。

以上の構造を踏まえて、次のように一般化する。

• コンストラクタc_iが有限とは限らない。1, ..., n ではなくて、いくつかの集合 A₁, ..., A_n でパラメトライズされた無限のコンストラクタを許す。
• コンストラクタの写像が全域とは限らない。
• 代数構造 A×C^* がより複雑なオペラッドになる。

以上のような一般化により、帰納構造を持った代数、帰納構造を持った圏／オペラッドを定義する。