Subrecursive inaccessible ordinal と Equational derivation vs. computation について

角田法也（熊本大・工）^{∗}

1998 年 6 月 26 日

Recursive functions を増加度によって分類する。 α ∈ Ω を countable tree ordinal （下を参照）として、次をみたす increasing functions の列 {f_{β} : N → N | β ≺ α} を scale と呼ぼう。

β ≺ γ ⇒ ∃k ∀x ≥ k (f_{β}(x) < f_{γ}(x)). Tree ordinals Ω は次のように再帰的に定義される。

(i) 0 ∈ Ω, (ii) if α ∈ Ω, then α + 1 ∈ Ω, (iii) if α : N → Ω, then α ∈ Ω. （(iii) のとき、 α は limit と呼ばれ、 α = sup α_{x} （但し α_{x} は関数 α の x での値）と書かれる。また、列 < α_{x} >_{x∈N} は

fundamental sequence for α と呼ばれる。）また、 sub-tree partial ordering ≺ は次の推移閉包で定義される。

(i) α ≺ α + 1, (ii) λ_{x} ≺ λ for a limit λ. 以下に出てくる関数の階層が scale となるために、 fundamental sequence に次の条件を付けたものを structured tree ordinal

(α ∈ Ω^{S}）と呼ぶ。

∀limit λ ⪯ α ∀n (λ_{n} + 1 ⪯_{n+1} λ_{n+1}) （但し ≺_{n} は次の推移閉包で定義される： (i) α ≺_{n} α + 1, (ii) λ_{n} ≺_{n} λ for a limit λ.）

例： Fast-growing (F -scale) F_{0}(x) = x + 1, F_{α+1}(x) = F_{α}^{x+1}(x)(= F_{α}(⋯ (F_{α}(x)) ⋯)), F_{λ}(x) = F_{λ_{x}}(x) for a limit λ.

例： ϵ_{0} までの fundamental sequences.

(C.N.F) (ω^{α_{1}} + ⋯ + ω^{α_{m}})_{x} = ω^{α_{1}} + ⋯ + (ω^{α_{m}})_{x} (for α_{1} ≥ ⋯ ≥ α_{m}). β: limit⇒ (ω^{β})_{x} = ω^{β_{x}}, (ω^{β+1})_{x} = ω^{β} · (x + 1). (β + 1)_{x} = β, 0_{x} = 0.

例： F_{ω}(x) = F_{x+1}(x) ≈ Ackermann function.

例： Hardy (H-scale) H_{0}(x) = x, H_{α+1}(x) = H_{α}(x + 1), H_{λ}(x) = H_{λ_{x}}(x).

性質 H_{α+β}(x) = H_{α}(H_{β}(x)) から次の性質が導かれる。

H_{ω^{α}}(x) = F_{α}(x) .

この性質から、 (ϵ_{0})_{n} = ω^{ω^{·^{·^{ω}}}} （n 個の ω）とすると、 scale の性質から、 F_{ϵ_{0}}(x) = F_{(ϵ_{0})_{x}}(x) = H_{(ϵ_{0})_{x+1}}(x) ≤ H_{(ϵ_{0})_{x+1}}(x+1) = H_{ϵ_{0}}(x + 1) となって、次の性質が導かれる。（左側の不等式は明らか。）

H_{ϵ_{0}}(x) < F_{ϵ_{0}}(x) ≤ H_{ϵ_{0}}(x + 1) .

（これは ϵ_{0} が F -scale と H-scale の不動点になっていることを意味する。）

例： Slow-growing (G-scale) G_{0}(x) = x, G_{α+1}(x) = G_{α}(x) + 1, G_{λ}(x) = G_{λ_{x}}(x).

上と同様に F -scale と G-scale の不動点を求めたい。すなわち次の性質：

G_{α}(x) < F_{α}(x) ≤ G_{α}(x + 1)

をもつ α を subrecursive inaccessible と呼び、 mimimal な s-inaccessible を作ることを考えよう。

定義： Ω_{n} 拡張 tree ordinals （Ω_{0} = N）は次のように再帰的に定義される。 (i) 0 ∈ Ω_{n}, (ii) if α ∈ Ω_{n}, then α + 1 ∈ Ω_{n}, (iii) if α : Ω_{k} → Ω_{n} (for k < n), then sup_{Ω_{k}} α_{γ} ∈ Ω_{n}.

∗kadota@cs.kumamoto-u.ac.jp

定義： φ_{α} : Ω_{n} → Ω_{n}(α ∈ Ω_{n+1}): 拡張 F-scale:

(i) φ_{0}(β) = β + 1, (ii) φ_{α+1}(β) = φ_{α}^{1+β}(β), (iii) φ_{λ}(β) = sup_{γ∈Ω_{k}} φ_{λ[γ]}(β), (iv) φ_{Λ}(β) = φ_{Λ[β]}(β).

（但し、 ψ^{0}(·) = ·, ψ^{δ+1}(·) = ψ(ψ^{δ}(·)), ψ^{λ}(·) = sup_{γ∈Ω_{k}} ψ^{λ[γ]}(·).)

定義： Terms T_{n}: (i) 0, 1, w_{0}, w_{1}, ⋯, w_{n−1} ∈ T_{n}. (w_{k} = sup_{γ∈Ω_{k}} γ を意味する。 )

(ii) if α ∈ T_{n+1}, β, γ ∈ T_{n}, then φ_{α}^{γ}(β) ∈ Ω.

定理： (Collapsing) Fix x ∈ N, α ∈ T_{2}, β ∈ T_{1} のとき、

G_{φ_{α}(β)}(x) = F_{cα}(G_{β}(x))

（特に G_{φ_{α}(w_{0})} = F_{cα} が成立（β = w_{0} とすると w_{0}[x] = x だから）。

（但し、 collapsing c(= c_{x}) は c0 = 0, c1 = 1, cw_{k+1} = w_{k}, c(φ_{α}^{γ}(β) = φ_{cα}^{cγ}(cβ) で定義される。）

例： (2^{2^{·^{·^{2}}}} } (x 2s) ≈) F_{3}(x) = G_{φ_{3}(w_{0})}, hence |φ_{3}(w_{0})| = ϵ_{0}.

(F_{ϵ_{0}} ≈) F_{φ_{3}(w_{0})} = G_{φ_{φ_{3}(w_{1})}(w_{0})}, hence |φ_{φ_{3}(w_{1})}(w_{0})| = |ID_{1}|

⋮

τ =^{def} sup_{n} φ_{φ_{··_{φ_{3}(wn)}··}(w_{1})}(w_{0}). Then

G_{τ} (x) < F_{τ} (x) ≤ G_{τ} (x)

This ordinal τ is minimal subrecursive inaccessible. |τ| = |ID_{<ω}| = |Π_{1}^{1} − CA_{0}|

・問題点： scale になっているか。 OK. Structuredness が成立（Kadota). ・ unique か。 Fund. seq. の system を「ほんの少しだけ」変えると、 G_{ϵ_{0}} ≈ F_{ϵ_{0}} などがでる（Weiermann). ・利点： Cichon による fund. seq を使って、 ProvRec(PA)≪ F_{ϵ_{0}} 等の結果を直接・簡明に示すことができる（Weiermann). ・ Wainer の問題意識：「Proof」と「Computation」の関係を示す。

（Equational derivation vs. computation (by Handley-Wainer))

（Fund. seq. の system を扱いやすくするため、 α[n] を次のような ordinal の有限集合とする。

α[0] ⊂ α[1] ⊂ α[2] ⊂ ⋯ ⊂ ∪_{n}α[n] s. t. (i) 0 ∈ α[n], (ii) if β + 1 ∈ α[n], then β ∈ α[n], (iii) if β ∈ α[n], then β + 1 ∈ α[n + 1].）

Kleene’s Equation Calculus (Herbrand-Gödel-Kleene-style recursive definitions) による recursive function の計算に uniformly に ordinal を assign する。

E: rewrite system とし、 rewrite rule 一回の適用を t ⇒_{E} u, 0 回を含めた有限回適用を t ⇒^{∗}_{E} u.

次の (P),(S),(E),(C) から n : N ⊢_{E}^{α} t = m を導く。この意味は ”from input≤ n, we can derive that t has value m within ordinal bound α.” である。これに対応して、次の (P),(S),(E) から（(C) を使わずに）導くことを n : N ⊧_{E}^{α} t = m と書くことにする。

(P) \overline{n : N ⊢_{E}^{α} ⌈m⌉ = m} (for m ≤ n + 1)

(S) \frac{n : N ⊢_{E}^{β} t = m}{n : N ⊢_{E}^{α} S(t) = m} (β ∈ α[n])

(E) If t ⇒_{E} r then \frac{n : N ⊢_{E}^{β} r = m}{n : N ⊢_{E}^{α} t = m} (β ∈ α[n])

(C) If w(x) is a term, then \frac{n : N ⊢_{E}^{β_{0}} t = k k : N ⊢_{E}^{β_{1}} w(⌈k⌉) = m}{n : N ⊢_{E}^{α} w(t) = m} (β_{0}, β_{1} ∈ α[n])

定理： If n : N ⊢_{E}^{α} t = m, then m ≤ B_{α}(n).

（但し、 B-scale: B_{0}(x) = x + 1, B_{α+1}(x) = B_{α}^{2}(x), B_{λ}(x) = B_{λ[x]}(x) ）

（証明のポイント： (C) の場合、左側の式から k ≤ B_{β_{0}}(n)、右側の式から m ≤ B_{β_{1}}(k) が導かれているとき、 m ≤ B_{β_{1}}(B_{β_{0}}(n) ≤ B_{β}^{2}(n) = B_{β+1}(n) となる。）性質： B_{ω·α} = F_{α} （但し、 F_{α+1} の定義を F_{α+1}(x) = F_{α}^{2^{x+1}}(x) と修正したとき。）

命題： Suppose tree T justifies n : N ⊢_{E}^{α} t = m. It follows that Height(T) ≤ B_{α}(n).

命題： Suppose reduction sequence D justifies n : N ⊧_{E}^{α} t = m. It follows that Height(D)(= Length(D)) ≤ G_{α}(n).

定義： P(α) = {φ : N^{k} → N | for some β < α, E, f, max(n⃗) : N ⊢_{E}^{β} f(⌈n⃗⌉) = φ(n⃗)}, D(α) = {φ : N^{k} → N | for some β < α, E, f, max(n⃗) : N ⊧_{E}^{β} f(⌈n⃗⌉) = φ(n⃗)},

定理： P(ω · α) = D(α^{+}).

（但し、 α に対する α^{+} は、 F_{α} ≈ G_{α^{+}} となる tree ordinal のこと。）

例： P(ω · 2) = D(ϵ_{0}) = E^{3} (Grzegorczyk hier.).

P(ω · n) = D(φ_{n}(w_{0})) = E^{n+1}.

P(ω · ω) = D(φ_{w_{1}}(w_{0})) = PrimRec.

P(ω · (ω + 1)) = D(φ_{w_{1}+1}(w_{0})(= Γ_{0})) =^{?} ElemRec in Ackermann.(Weiermann)

P(ω · ϵ_{0}) = D(φ_{ϵ_{w_{1}} +1}(w_{0})) = ProvRec(PA).

⋮

参考文献 [1] S.S. Wainer, Slow growing versus fast growing, J. Symbolic Logic 54, 1989, 608-614.

[2] S.S. Wainer, Hierarchies of provably computable functions, in P. Petkov (Ed.) Mathematical Logic, Plenum Press 1990, 211-220.

[3] N. Kadota, On Wainer’s notation for a minimal subrecursive inaccessible ordinal, Math. Logic Quarterly 39, 1993, 217-227.

[4] W.G. Handley and S.S. Wainer, Equational derivation vs. computation, APAL 70, 1994, 17-49.

[5] S.S. Wainer, The hierarchy of terminating recursive programs over N, in D. Leivant (Ed.) Logic and Computational Complexity, Springer Lect. Notes in Computer Science 960, 1995, 281-299.

[6] S.S. Wainer, Accessible segments of the fast growing hierarchy, in J.A. Makowsky, E.V. Ravve (Eds.) Logic Colloquium ’95, Springer Lect. Notes in Logic 11, 1998, 339-348.

————————————

[7] E.A. Cichon and A. Weiermann, Term rewriting theory for the primitive recursive functions, APAL 83, 1997, 199-223.

[8] A. Beckmann and A. Weiermann, A term rewriting characterization of the polytime functions and related complexity classes, Arch. Math. Logic 36, 1996, 11-30.

————————————

[9] T. Arai, Consistency proof via pointwise induction, Arch. Math. Logic 37, 1998, 149-165 (([10] T. Arai, Variations on a theme by Weiermann, to appear (JSL).)) 未見

[11] A. Weiermann, Sometimes slow growing is fast growing, APAL 90, 1997, 91-99.

[12] A. Weiermann, How to characterize provably total functions by local predicativity, J. Symbolic Logic 61, 1996, 52-69. ———————————–

[13] A.J. Heaton and S.S. Wainer, Axioms for subrecursion theories, in S.B. Cooper, T.A. Slaman, S.S. Wainer (Eds.) Computability, Enumerability, Unsolvability, London Math. Soc. Lect. Notes 224, Cambridge U.P., 1996, 123-138.

[14] L. Kristiansen, A jump operator on honest subrecursive degrees, Arch. Math. Logic 37, 1998, 105-125. (([15] H. Simmons, A density property of the primitive recursive degrees, Technical Report Series UMCS-93-1-1, Depart-

ment of Computer Science, University of Manchester 1993.)) 未見