木変換器とスタック木変換器の対応

木変換器がスタック木変換器に含まれていることは既に示した．加えて，スタック木変換器 は，木変換器より真に大きい．これは，木変換器のクラスに含まれない木変換を，スタック木変 換器が表現できることを意味する．Stk は，その1つである．木変換器は，定理160より RTL の逆像が RTL で閉じている．しかし，Stk はRTL の逆像が RTL で閉じていない場合がある．

命題 307. Σ ={>⁽⁰⁾} ^{について，}JStk_ΣK⁻¹[{>}]6∈RTL □ 証明. L = JStk_ΣK⁻¹[{>}] とし，L ∈ RTL と仮定する．補題 66 の p_L について，t₁ = Tail^pL(x1)，t2 = Cons(| ⊥,· · ·{z Cons(⊥}

pL個

,Cons(>,Empty))· · ·)) を考える．JStkΣK(t1(t2)) = >

より，t1(t2)∈L である．この時，以下を満たす u1, u2, u3 が存在する．

• t1 =u1(u2(u3))

• height(u₂(u₃))≤p_L

• height(u₂)≥1

• 任意のn∈N ^{について，}u1(uⁿ₂(u3(t2)))∈L

特に，u1(u3(t2)) ∈ L である．ところで，m = height(u2) とすると，u2 = Tail^m(x1) で あり，u1(u3) = Tail^pL−m(x1) ^{である．また，}m ≥ 1 ^より，pL −m < pL であり，つまり JStk_ΣK(u₁(u₃(t₂))) =⊥ 6∈L となるが，これは矛盾．よって，題意は示された． ■ 一般に，Stk によるRTL の逆像は，CFTL になる．このことを示すため，まずスタックシス テムへの逆像が CFTL で閉じていることを示す．

補題 308. ランク付きアルファベット Σ について，以下が成り立つ．

∀L∈ P( ˆT_Σ⊥)∩RTL.stkeval⁻_elm¹[L]∈CFTL

□ 証明. L∈ P( ˆT_Σ⊥)∩RTL について，JMK =L となる FTA M = (Q,Σ_⊥, q₀, R) が存在する．

この時，PDTA M⁰ = (Q⁰,Σ⁰,Γ⁰, q⁰₀, u⁰₀, R⁰) を，以下のように定義する．

Q^{0 def}= Q∪ {qB} ∪ {qstk, qelm} Σ^{0 def}= Σ∪STK¯

Γ^{0 def}= {A⁽⁰⁾,H⁽⁰⁾,T⁽¹⁾} q⁰₀ ^def= q0

u⁰₀ ^def= A

R^{0 def}= {qs(σ(x1, ... ,xn),A) →σ(qs1(x1,A), ... , qsn(xn,A))|σ : (s1, ... , sn)_Σ^˙∪STK s}

∪ {q(σ(x1, ... ,xn),A)→σ(q1(x1,A), ... , qn(xn,A))

|q(σ(x1, ... ,xn))→σ(q1(x1), ... , qn(xn))∈R}

∪ {q(Head(x1),A)→Head(q(x1,H))|q ∈Q}

∪ {q(Head(x₁),A)→Head(q_B(x₁,H)) |q(⊥)→ ⊥ ∈R}

∪ {q(Tail(x₁),H) →Tail(q(x₁,T(H)))|q ∈Q∪ {q_B}}

∪ {q(Tail(x₁),T(z₁))→Tail(q(x₁,T(T(z₁))))|q ∈Q∪ {q_B}}

∪ {q(Cons(x₁,x₂),H)→Cons(q(x₁,A), q_stk(x₂,A))|q ∈Q}

∪ {q(Cons(x₁,x₂),T(z₁))→Cons(q_elm(x₁,A), q(x₂,z₁))|q∈Q∪ {q_B}}

∪ {q_B(Empty,H)→Empty, q_B(Empty,T(z₁))→Empty}

この時，stkeval⁻¹_elm[JMK] =JM⁰K であることは，容易に確認できる． ■ これを元に，一般のランク付き木において，Stk による RTL の逆像が CFTL で閉じている ことを示すことができる．

定理 309. ランク付きアルファベット Σ について，以下が成り立つ．

∀L∈ P( ˆTΣ_⊥)∩RTL.JStkΣK⁻¹[L]∈CFTL

□ 証明. L∈ P( ˆT_Σ⊥)∩RTLについて，JMK =LとなるFTAM = (Q,Σ_⊥, q₀, R)が存在する．こ の時，補題308の PDTAM⁰ = (Q⁰,Σ⁰,Γ⁰, q⁰₀, u⁰₀, R⁰)に対して，M⁰⁰ = (Q⁰⁰,Σ⁰,Γ⁰, q₀⁰⁰, u⁰₀, R⁰⁰) を，以下のように定義する．

Q^{00 def}= Q⁰×SS×SS∪Q⁰×Q⁰ q₀^{00 def}= hq⁰₀,elm,elmi

R^{00 def}= {hq⁰, s, s⁰i(σ(x1, ... ,xn), γ(⃗z))→σ(hq₁⁰, s1, s1i(x1, u1), ... ,hq_n⁰, sn, sni(xn, un))

|s, s⁰ ∈S, σ : (s1, ... , sn)_Σ^˙∪STK s⁰,

q(σ(⃗x), γ(z))→σ(q₁⁰(x₁, u₁), ... , q⁰_n(x_n, u_n))∈R⁰}

∪ {hq₁⁰,elm,elmi(x, γ(⃗z))→ hq⁰₂,elm,stki(x, u)

|q₁⁰(Head(x₁), γ(⃗z))→Head(q₂⁰(x₁, u))∈R⁰}

∪ {hq⁰,stk,stki(x, γ(⃗z))→ hq⁰₁, q⁰₂i(x, u)

|q⁰(Cons(x₁,x₂), γ(⃗z))→Cons(q⁰₁(x₁,A), q₂⁰(x₂, u))∈R⁰}

∪ {hq₁⁰, q₂⁰i(x, γ(⃗z))→ hq⁰₁,stk,elmi(x,A)

|q₂⁰(Empty, γ(⃗z))→Empty∈R⁰} この時，JStk_ΣK⁻¹[JMK] =JM⁰⁰K ^{を示す．これは，}

JStkΣK⁻¹[JMK] = stkproj⁻_elm¹[stkeval⁻_elm¹[JMK]] (∵^定理209)

= stkproj⁻_elm¹[JM⁰K] (∵^補題308)

より，stkproj⁻_elm¹[JM⁰K] =JM⁰⁰K ^{と等しい．さらに，}stkproj⁻_elm¹[JM⁰K] =JM⁰⁰K ^{が成り立つこと}

は容易に確認できる．よって，題意は示された． ■

さて，Stk は命題307より RTL を超える CFTL を逆像に持つことがあるため，木変換器で 表現できるとは限らない．

補題 310. Stk6⊆MTT □

証明. Stk⊆MTT とする．この時，定理160より，

∀L∈ P( ˆT_Σ)∩RTL.JStk_ΣK⁻¹[L]∈RTL

である．つまり，L ^def= {T} ^{について，}Stk⁻_{T¹_(0)}[L] ∈RTL だが，これは命題307に矛盾する．

よって，題意は示された． ■

Stk はスタック木変換器の最下層にあるクラスであるため，ここからスタック木変換器一般に おいて，木変換器より真に大きいことが示された．ところで，Stk は RTL の逆像が CFTL で 閉じていたが，StkTT には CFTL を超える RTLの逆像を持つものが存在する．

定理 311. 以下を満たす JMK: ˆTΣ →Tˆ∆_⊥ ∈StkTT が存在する．

∃L ∈ P( ˆT∆)∩RTL.JMK⁻¹[L]6∈CFTL

□ 証明. 例203の M = (Q,Σ,∆, e, R) について，L = {∧(>,>)} ∈ RTL だが，命題204より，

JMK⁻¹[L] ={aⁿ(bⁿ(cⁿ($)))|n∈N} 6∈CFTL．よって，題意は示された． ■ 一般に，StkTT とStkMTTのRTL の逆像による言語は，Stk のRTLの逆像による言語と，

その言語のTDTT^，MTTでの逆像による言語で特徴付けられる．なぜなら，StkTT^，StkMTT は，TDTT，MTT とStk の合成によって記述できるからである．

補題 312.

• StkTT_ω ⊆TDTT; Stk_ω

• StkMTTω ⊆MTT; Stkω

□ 証明. StkMTT M = (Q,Σ,∆, e, R) について，MTT M₁ = (Q₁,Σ,∆₁, e₁, R₁) を以下のよう に定義する．

Q1 def= Q

∆1

def= ∆∪STK¯ e1

def= e R₁ ^def= R

Q=Q⁽¹⁾，つまり M がStkTT の場合，M₁ はTDTT になる．この時，M₂ = Stk_∆ として，

JMKω =JM1K;JM2Kω を示す．まず，

∀k ∈SS, η1, η2 ∈SFM(∅,∅)k . η1 ⇒M₁ η2 impliesη1 ⇒M η2

で，⇒M₁ は S

k∈SSSFM(∅,∅)k で閉じていることは，η1 に対する構造的帰納法で容易に示せ る．よって，t ∈TˆΣ について，

e[x1 ←t]⇒^∗M nf(⇒M1, e[x1 ←t]) である．ここから，t ∈TˆΣ，m∈N ^{について，}

Head(Tail^m(e[x1 ←t]))⇒^∗M Head(Tail^m(nf(⇒M₁, e[x1 ←t])))

⇒^∗M stkevalelm(Head(Tail^m(JM1K(t))))

=JM2Kω(JM1K(t))(m)

= nf(⇒M,Head(Tail^m(e[x1 ←t])))

=JMKω(t)(m)

である．よって，題意は示された． ■

また，逆の関係も成り立つ．

補題 313.

• TDTT; Stk_ω ⊆StkTT_ω

• MTT; Stkω ⊆StkMTTω

□ 証明. MTT M1 = (Q1,Σ,∆∪STK, e¯ 1, R1) に対して，StkMTT M = (Q,Σ,∆, e, R) を以下 のように定義する．

Q^def= Q1

e ^def= stkproj_stk(e₁)

R^def= {q(σ(⃗x), ⃗y)→stkproj_stk(η)|q(σ(⃗x), ⃗y)→η ∈R}

Q₁ =Q⁽¹⁾₁ ，つまりM₁ がTDTTの場合，M はStkTT になる．この時，M₂ = Stk_∆ として，

JM₁K;JM₂Kω =JMKω を示す．定理202と同様にして，

Head(Tail^m(e[x1 ←t]))⇒^∗M stkproj_elm(Head(Tail^m(nf(⇒M1, e1[x1 ←t]))))

= stkproj_elm(Head(Tail^m(JM1K(t)))) が示せる．ここから，

Head(Tail^m(e[x₁ ←t]))⇒^∗M stkproj_elm(Head(Tail^m(JM₁K(t))))

⇒^∗M stkeval_elm(stkproj_elm(Head(Tail^m(JM₁K(t)))))

=JM₂Kω(JM₁K(t))(m)

= nf(⇒M,Head(Tail^m(e[x₁ ←t])))

=JMKω(t)(m)

も容易に示せる．よって，題意は示された． ■

よって，StkTT，StkMTTは，それぞれTDTT，MTTとStk の合成と同等の表現力を持つ．

定理 314.

• StkTTω = TDTT; Stkω

• StkMTT_ω = MTT; Stk_ω

□

証明. ^補題312^，補題313^より． ■

これは，木変換器の階層が StkTT，StkMTT でも保存されることを示している．しかし，

これは StkATT では成り立たない．なぜなら，StkATT を同様に ATT と Stk に分解した場 合，分解された ATT が巡回する場合があるからである．具体的に例291を考えると，この例を ATT と思った場合は巡回する．一般に，StkATT が ATTと Stk に分解できるかは未解決であ り，本研究では同等ではないと予想している．

予想 315. ATT; Stk⊊StkATT □

ただし，非巡回 StkATT の場合，同様の方法で ATTと Stk に分解できる．

補題 316. StkATTncr,ω ⊆ATT; Stkω □

証明. StkATT M = (A,Σ,∆, a0, ♯, R) について，ATT M1 = (A,Σ,∆∪STK, a¯ 0, ♯, R) を考 える．この時，M2 = Stk∆ として，JMKω =JM1K;JM2Kω は，補題312^{と同様に示せる．} ■

また，逆の関係も成り立つ．

補題 317. ATT; Stkω ⊆StkATTncr,ω □

証明. 定理294と同様に示せる． ■ よって，非巡回 StkATT は，ATT とStk の合成と同等の表現力を持つ．

定理 318. StkATT_ncr,ω = ATT; Stk_ω □

証明. 補題316，補題317より． ■

つまり，予想301^と予想315は同値であり，どちらかが肯定的に解決されればもう一方も肯定 的に解決される．ところで，以上の結果より，StkTT，非巡回 StkATT，StkMTT の間で，部 分関係による階層を為すことを示すことができる．

系 319.

• StkTT_ω ⊆StkATT_ncr,ω

• StkATTncr,ω ⊆StkMTTω

□ 証明. 定理314，定理318，定理152，定理155より． ■ これは，さらに真部分関係に強めることができる．それは，StkTT，非巡回StkATT，StkMTT がそれぞれ TDTT，ATT，MTT と同様の樹高性を持つことによる．これを示すために，まず Stk の樹高性を明らかにする．Stk は入力木のスタックに関する記号を全て評価し，⊥ ^以外は出 力に残さない．それに加え，⊥ 以外に入力木にない記号を生成することはない．よって，一般に 出力木の高さは入力木の高さ以下になる．

定理 320 (Stk の樹高性). ランク付きアルファベット Σ について，以下が成り立つ．

∀t∈Tˆ_Σ∪STK¯ .height(JStkΣK(t))≤height(t)

□ 証明. 定理209より，題意は

∀t ∈Tˆ_Σ∪STK¯ .height(stkeval_elm(stkproj_elm(t)))≤height(t) と等しい．さらに，これは

∀t∈Tˆ_Σ∪STK¯ , m∈N.height(stkeval_elm(stkproj_elm(Head(Tail^m(t)))))≤height(t) から導かれる．なお，系210より，

stkeval_elm(stkproj_elm(Head(Tail⁰(t)))) = stkeval_elm(stkproj_elm(t))

に注意．よって，これを以下のように構造的帰納法で示す．なお，スペースの都合上 height を h，stkeval_elm を f，stkproj_elm を p₁，stkproj_stk を p₂，t 7→ Head(Tail^m(t)) を g_m と略記 する．

IB1 適用不能．

IB2 以下のように場合分けを行う．

• 任意の σ∈Σ⁽⁰⁾ ∪ {⊥}^{について，}t =σ の場合，

h(f(p1(gm(σ)))) =h(f(gm(Cons(σ,Empty))))

=

h(σ) (m= 0) h(⊥) (m≥1)

≤1 =h(σ) より正しい．

• t= Empty の場合，

h(f(p1(gm(Empty)))) =h(f(gm(Empty)))

=h(⊥)

≤1 =h(Empty) より正しい．

IS 以下のように場合分けを行う．

• 任意の n≥1，σ⁽ⁿ⁾ ∈Σ，t1, ... , tn ∈Tˆ_Σ∪STK¯ について，

h(f(p₁(g_m(σ(t₁, ... , t_n))))) =h(f(g_m(Cons(σ(p₁(t₁), ... , p₁(t_n)),Empty))))

=

h(σ(f(p1(t1)), ... , f(p1(tn)))) (m= 0)

h(⊥) (m≥1)

≤1 + max{h(f(p₁(g₀(t_i))))|i∈[n]}

≤1 + max{h(t_i)|i∈[n]} (∵i.h.)

=h(σ(t₁, ... , t_n)) より正しい．

• t1, t2 ∈Tˆ_Σ∪STK¯ について，

h(f(p1(gm(Cons(t1, t2))))) =h(f(gm(Cons(p1(t1), p2(t2)))))

=

h(f(p1(t1))) (m= 0) h(f(p1(gm−1(t2)))) (m≥1)

≤

h(t1) (m= 0)

h(t₂) (m≥1) (∵i.h.)

≤1 + max{h(t_i)|i∈[2]}

=h(Cons(t1, t2)) より正しい．

• t₁ ∈Tˆ_Σ∪STK¯ について，

h(f(p₁(g_m(Head(t₁))))) =h(f(g_m(Cons(Head(p₁(t₁)),Empty))))

=

h(f(p1(g0(t1)))) (m= 0)

h(⊥) (m≥1)

≤

h(t₁) (m= 0)

h(⊥) (m≥1) (∵i.h.)

≤1 +h(t1) =h(Head(t1)) より正しい．

• t₁ ∈Tˆ_Σ∪STK¯ について，

h(f(p1(gm(Tail(t1))))) =h(f(p1(gm+1(t1))))

≤h(t1) (∵i.h.)

≤h(Tail(t1)) より正しい．

■ ここから，定理314を合わせて，StkTT，StkMTTの樹高性が，TDTT，MTT と同様にな ることが示せる．

系 321 (StkTT ^と StkMTT ^の樹高性).

• ^任意のJMK: ˆTΣ →Tˆ∆ ∈StkTT ^{について，}

∃cM ∈N.∀t∈TˆΣ .height(JMK(t))≤cM ·height(t)

• 任意のJMK: ˆT_Σ →Tˆ_∆ ∈StkMTTについて，

∃c_M ∈N.∀t∈Tˆ_Σ .height(JMK(t))≤exp(c_M ·height(t))

がそれぞれ成り立つ． □

証明. それぞれ定理314より，

• JMK=JM₁K;JM₂K ^を満たす JM₁K∈TDTT，JM₂K∈Stk について，定理94のc_M1 に 対してcM

def= cM₁，f ^def= n7→cM₁ ·n

• JMK=JM1K;JM2K ^を満たす JM1K∈MTT^，JM2K∈Stk ^{について，定理}134^のcM1 に 対してc_M ^def= c_M1，f ^def= n7→exp(c_M1 ·n)

とおく．この時，それぞれ任意の t∈TˆΣ について，

height(JMK(t)) = height(JM2K(JM1K(t)))

≤height(JM1K(t)) (∵^定理320)

≤f(height(t))

となる． ■

もちろん，非巡回 StkATT の樹高性についても同様に示せるが，これは定理305と同様の結 果になる．それぞれの樹高性から，StkTT，非巡回 StkATT，StkMTT のクラスについて，逆 の包含関係は成り立たないことが示された．

補題 322.

• StkATTncr 6⊆StkTT

• StkMTT6⊆StkATT_ncr

□

証明. ^{それぞれ，}

• StkATTncr ⊆StkTT

• StkMTT⊆StkATT_ncr が成り立つと仮定する．この時，

• 定理294より，ATT⊆StkATT_ncr ⊆StkTT

• 定理267より，MTT ⊆StkMTT⊆StkATTncr

であり，

• 例99の M について，JMK∈StkTT

• 例135の M について，JMK∈StkATTncr

である．しかし，これはそれぞれ，補題151，補題154と同様に，系321，定理305に矛盾する．

よって，題意は示された． ■

以上から，StkTT，非巡回 StkATT，StkMTT の間で，真の部分関係による階層を為すこと を示すことができる．

定理 323.

• StkTT⊊StkATTncr

• StkATT_ncr ⊊StkMTT

□

証明. 系319，補題322より． ■

推移律から，StkTT は StkMTT より真に小さいことも示された．

系 324. StkTT⊊StkMTT □

証明. 定理323より． ■

系207より，Stk はスタック木変換器の階層において，最下層にあたる．このStk が補題310 より MTT に含まれないことと以上の結果から，以下の関係が導かれる．

補題 325.

• StkTT6⊆TDTT

• StkATT_ncr 6⊆ATT

• StkMTT6⊆MTT

□

証明. それぞれ

• StkTT⊆TDTT

• StkATTncr ⊆ATT

• StkMTT⊆MTT

が成り立つと仮定する．この時，定理323より，

• 系156より，StkTT⊆TDTT⊆MTT

• 定理155より，StkTT ⊆StkATT_ncr ⊆ATT⊆MTT

• StkTT⊆StkMTT⊆MTT

である．また系207より，それぞれ Stk ⊆StkTT ⊆MTT となるが，これは補題310に矛盾す

る．よって，題意は示された． ■

以上より，スタック木変換器は木変換器より真に大きいことが示された．

定理 326.

• TDTT⊊StkTT

• ATT⊊StkATTncr

• MTT⊊StkMTT

□ 証明. 定理202，定理294，定理267，補題325より． ■

また，StkATT_ncr⊆StkATT より，StkATT は ATT より真に大きいことも分かる．

系 327. ATT⊊StkATT □

証明. 定理326より． ■

一般に，定理311に見られるように，スタック木変換器では RTL の逆像が RTL に閉じてい ない木変換を表現できるが，そのようなものは定理160に違反するため木変換器では表現できな い．ただし，RTLの逆像が RTL に閉じている木変換で，木変換器では表現できないが，スタッ ク木変換器では表現できるものが存在するかという問題は，未解決である．予想では，RTL の 逆像が RTL で閉じている木変換で，スタック木変換器で表現できるものは，木変換器でも表現 できる．

予想 328. JMK: ˆT_Σ →Tˆ_∆⊥ ∈StkMTTについて，以下の2条件は同値である．

• JMK∈MTT

• ∀L∈ P( ˆT∆_⊥)∩RTL.JMK⁻¹[L]∈RTL

□ ところで，線形 StkTT が，線形TDTTと Stk に分解できることも，定理314の分解方法を 適用することで示せる．

定理 329. StkTTlu,ω = TDTTlu; Stkω □

証明. M が線形 StkTT の場合，補題312のM1 は線形 TDTT．また，M1 が線形 TDTTの 場合，補題313のM は線形StkTT．よって，題意は示された． ■

ここから，以下が導かれる．

定理 330. 予想163が成り立つならば，JMK : ˆTΣ → Tˆ∆_⊥ ∈ StkTTlu について，以下が成り 立つ．

∀L∈ P( ˆT∆_⊥)∩RTL.JMK⁻¹[L]∈CFTL

□ 証明. 定理329より，JMK=JM1K;JM2K ^を満たす JM1K∈TDTTlu，JM2K∈Stk が存在する．

この時，L ∈ P( ˆT_∆⊥)∩RTL について，定理309より JM₂K⁻¹[L] ∈ CFTL であり，予想163 より JMK⁻¹[L] =JM₁K⁻¹[JM₂K⁻¹[L]]∈CFTL．よって，題意は示された． ■

一般に，スタック木変換器においてRTL の逆像が CFTL に閉じているクラスの一つとして，

線形 StkTT が該当するのではないかと考えている．これは，定理329から，線形 TDTT が定 理309の証明で与えられた文脈自由文法による言語の逆像について，CFTL で閉じていること を意味する．

予想 331. JMK: ˆTΣ →Tˆ∆_⊥ ∈StkTTlu について，以下が成り立つ．

∀L∈ P( ˆT∆_⊥)∩RTL.JMK⁻¹[L]∈CFTL

□

ドキュメント内 スタック機構を持つ木変換器の表現力 (ページ 134-145)