ランク付き木から文字列への決定性ストリーム変換器の表現力

1731095 Alur D’Antoni (STTsur ) STTsur STTsur STTsur (MSOTT) STTsur (SRTST) SRTST

(yDTR) yDTR yDTR

SRTST yDTR

yDTR SRTST SRTST yDTR

SRTST yDTR yDTR

30

: 1731095

:

:

:

: 2019

3

14

Alur D’Antoni (STTsur) STTsur STTsur (MSOTT) STTsur (SRTST) SRTST (yDTR_{) yDT}R yDTR SRTST yDTR SRTST yDTR _yDTR _SRTST

1 1 1.1 . . . 1 1.2 . . . 3 1.3 . . . 3 2 5 2.1 . . . 5 2.2 . . . 7 3 10 4 13 4.1 . . . 13 4.2 . . . 15 5 SRTST yDTR ₂₀ 5.1 yDTR _{SRTST . . . 20} 5.2 yDTR SRTST . . . 23 5.3 SRTST yDTR _{. . . 25} 5.4 SRTST yDTR _{. . . 29} 5.5 . . . 34 6 35 6.1 . . . 35 6.2 . . . 36 7 39 40 41

1

1.1

(

) [24, 16, 15, 13, 10, 20]

Alur D’Antoni (streaming tree

transducer with single-use-restriction STTsur) [2] *1 STTsur

(visibly pushdown automaton) (streaming string

transducer ) [3, 14, 2] / (call/return) STTsur ( ) STTsur STTsur (single-use-restriction) STTsur

(monadic second order definable tree transducer MSOTT) [2]

MSOTT [11] STTsur

[2]

books book The Art of Computer Programming D.E.Knuth empty toJSON =====_⇒ [ {

title:"The Art of Computer Programming", author:"D.E.Knuth" } ] 1.1 JSON ⟨books ⟨book

⟨The Art of Computer Programming⟩ ⟨D.E.Knuth⟩

book_⟩ ⟨empty⟩ books_⟩

1.2

(deterministic streaming ranked-tree-to-string

transducer SRTST) SRTST ( )

STTsur

SRTST 1.1

1.2 SRTST

(deterministic top-down tree-to-string transducer yDT) *2 _yDT

1.1 toJSON

yDT

toJSON (t) = [books(t)]

books(books(x1, x2)) ={info(x1)}rest(x2)

books(empty) = ε

rest(books(x1, x2)) = ,{info(x1)}rest(x2)

rest(empty) = ε

info(book(x1, x2)) = title:"id (x1)",author:"id (x2)"

yDT (regular look-ahead )

(deterministic top-down tree-to-string transducer with regular look-ahead yDTR) [9]

1.1 toJSON yDTR toJSON′

toJSON′(t) = [] if t = empty

toJSON′(t) = [books′(t)]

books′(books(x1, x2)) ={info(x1)} if x2 = empty

books′(books(x1, x2)) ={info(x1)},books′(x2)

t = empty x2 = empty toJSON′

( toJSON ) yDT yDTR yDT

yDTR _[22] yDTR yDTR SRTST ( )

1.2

SRTST yDTR _SRTST yDTR yDTR SRTST yDTR SRTST

1.3

2 3

4 5 yDTR _SRTST SRTST SRTST yDTR yDTR ₆ SRTST yDTR ₇

2

(BTA) ∅ 0 N {1, . . . , n} [n] n = 0 [n] =_∅ S S |S| S S′ S S′ S_{\ S}′ S _{⊆ S}′ S′ S′\ S S! ∆ k k-∆k k = 0 ∆k () k- t i ti k- t |t| k k- t ∈ ∆k _{d ∈ ∆ k- d k +} 1-(t1, . . . , tk, d) t|| d ∆ k ∆≤k = !k_i=0∆i A B f f : A ⇀ B f Dom(f )

2.1

∆ ∆ w1, . . . , wn w1· · · wn ∆ 0 ε u = u1· · · un v = v1· · · vm ‘·’ u· v = u1· · · unv1· · · vm ‘·’ uv ∆ ∆∗ ∆∗ L Σ Σ rankΣ : Σ → N (Σ, rankΣ) k σ σ(k) Σ k Σ(k) Σ k Σ(>k) _{X = {x} 1, x2, . . .} k _{∈ N} Xk ={x1, . . . , xk} k = 0 Xk =∅ 1. Σ TΣ σ(n) ∈ Σ t1, . . . , tn ∈ TΣ σ(t1, . . . , tn)∈ TΣ ! e _{∈ Σ}(0) _{e() ∈ T} Σ e

f f b a f a b 2.1 f(f(b,a),f(a,b))

⟨f ⟨f ⟨b b⟩ ⟨a a⟩ f⟩ ⟨f ⟨a a⟩ ⟨b b⟩ f⟩ f⟩

2.2 ⌊f(b,a),f(a,b)⌋ Σ Σˆ σ _{∈ Σ} ⟨σ σ⟩ ( Σ =ˆ !_σ∈Σ"⟨σ#∪"σ⟩#)*1 ˆ Σ σ _{∈ Σ ⟨σ} σ_⟩ σ (well-matched ) σ ∈ Σ ⟨σ σ⟩ (well-formed ) 1. Σ ={f(2)_{, a}(0)_{, b}(0)_} t = f(f(b,a),f(a,b))∈ TΣ TΣ 2.1 t′ 0 b _TΣ t′ = f(b(a),f(b,a))̸∈ TΣ

⟨f ⟨b b⟩ ⟨a a⟩ f⟩ ⟨f ⟨a a⟩ ⟨b b⟩ f⟩ f⟩ (2.1)

⟨f ⟨f ⟨b b⟩ ⟨a b⟩ f⟩ ⟨f ⟨a a⟩ ⟨b b⟩ f⟩ (2.2)

⟨f ⟨a a⟩ ⟨b b⟩ ⟨a a⟩ f⟩ (2.3)

(2.1) f_⟩ (2.2) _⟨a b_⟩ (2.3) 2 f Σ ! *1 _{call/internal/return 3} call/return

Σ 2. ⌊−⌋ : TΣ → ˆΣ∗ t = σ(t1, . . . , tn)∈ TΣ ⌊t⌋ = ⟨σ ⌊t1⌋ · · · ⌊tn⌋ σ⟩ ! TΣ ⌊TΣ⌋ ⌊TΣ⌋

e _{∈ Σ}(0) _{⟨e e⟩ (= ⌊e⌋) ⟨e⟩}

3. _{⌈−⌉ : ⌊T}Σ⌋ → TΣ w =⟨σ(n) _w 1· · · wn σ(n)⟩ ∈ ⌊TΣ⌋ ⌈w⌉ = σ(⌈w1⌉, . . . , ⌈wn⌉) w1, . . . , wn ∈ ⌊TΣ⌋ ! ⌊−⌋ ⌈−⌉ t ∈ TΣ t = ⌈⌊t⌋⌉ w_{∈ ⌊T}Σ⌋ w =⌊⌈w⌉⌋ 2. 1 Σ =_{f(2)_{, a}(0)_{, b}(0)_{} f(f(b,a),f(a,b))} w w =⌊f(f(b,a),f(a,b))⌋

=⟨f ⟨f ⟨b b⟩ ⟨a a⟩ f⟩ ⟨f ⟨a a⟩ ⟨b b⟩ f⟩ f⟩ =⟨f ⟨f ⟨b⟩ ⟨a⟩ f⟩ ⟨f ⟨a⟩ ⟨b⟩ f⟩ f⟩ ∈ ⌊TΣ⌋

w 2.2

w′ _⌊TΣ⌋

w′ =_{⟨f ⟨b b⟩ ⟨a a⟩ f⟩ ⟨f ⟨a a⟩ ⟨b b⟩ f⟩ ̸∈ ⌊T}Σ⌋

w′ f(b,a) f(a,b) !

2.2

(BTA) BTA

BTA BTA

4. (non-deterministic bottom-up tree automaton BTA) (Π, Σ, θ) • Π • Σ • θ : Σ(n)_{× Π}n _{→ 2}Π _! BTA A = (Π, Σ, θ) θ θ :ˆ TΣ → 2Π σ(t1, . . . , tn)∈ TΣ ˆ θ(σ(t1, . . . , tn)) = $ π1∈ˆθ(t1),...,πn∈ˆθ(tn) θ(σ, π1, . . . , πn) π ∈ Π t ∈ TΣ π ∈ ˆθ(t) π t π LA(π) ={t ∈ TΣ | π ∈ ˆθ(t)} A L(π) π ∈ Π π A BTA π _{∈ Π L(π) ̸= ∅} σ(n) _{∈ Σ π} 1, . . . , πn ∈ Π θ(σ, π1, . . . , πn) 1

(determinisitc bottom-up tree autoamton DBTA) DBTA

t _{∈ T}Σ |ˆθ(t)| ≤ 1 θ(t) =ˆ {π} π θ(t) =ˆ ∅ DBTA θ Σ(n) _{× Π}n _Π ˆ θ(t) = ∅ ⊥ ̸∈ Π t _{∈ T}Σ t DBTA {LA(π) | A = (Π, Σ, θ) : DBTA, π ∈ Π} BTA {LA(π) | A = (Π, Σ, θ) : BTA, π ∈ Π} BTA [7] A = (Σ, Π, θ) A′ = (Σ, Π′, θ′) BTA A A′ A⊗ A′ _{A⊗ A}′ _{= (Σ, Π× Π}′_{, θ} A⊗A′) σ(n) ∈ Σ (π1, π1′), . . . , (πn, π′n)∈ Π × Π′ θ_A⊗A′(σ, (π₁, π₁′), . . . , (π_n, π_n′)) ={(π, π′)∈ Π × Π′ | π ∈ θ(σ, π1, . . . , πn)∧ π′ ∈ θ(σ, π1′, . . . , πn′)} (π, π′)∈ Π×Π′ _L A⊗A′((π, π′)) =L_A(π)∩L_A′(π′) 3. BTA A = (Π, Σ, θ) Π = {πa, πb} Σ = {f(2), a(0), b(0)} θ θ(f, π1, π2) ={π1}, θ(a, ()) ={πa}, θ(b, ()) ={πb}.

f f b a f a b {πb} {πb} {πb} {πa} {πa} {πa} {πb} 2.3 BTA σ(n) _{∈ Σ π} 1, . . . , πn ∈ Π |θ(σ, π1, . . . , πn)| = 1 A DBTA L(πa) a L(πb) b θ(a) =ˆ {πa} ˆθ(b) = {πb} a_{∈ L(π}a) b∈ L(πb) f(b,a), f(a,b) ∈ TΣ ˆ θ(f(b,a)) = $ π1∈ˆθ(b),π2∈ˆθ(a) θ(f, π1, π2) =_{πb}, ˆ θ(f(a,b)) = $ π1∈ˆθ(a),π2∈ˆθ(b) θ(f, π1, π2) =_{πa}.

f(b,a) ∈ L(πb) f(a,b) ∈ L(πa) f(f(b,a),f(a,b)) ∈

L(πb) ˆ θ(f(f(b,a),f(a,b))) = $ π1∈ˆθ(f(b,a)),π2∈ˆθ(f(a,b)) θ(f, π1, π2) ={πb}. ˆ θ(f(f(b,a),f(a,b))) 2.3 !

3

(yDTR₎

yDTR _{(yDT) (regular}

look-ahead ) yDT yDTR 5. ( ) Q ∆ Xn (n ∈ N) RhsQ,∆(Xn) τ ::= ε | aτ | q(xi)τ a∈ ∆ q ∈ Q i ∈ [n] q(xi) (q, xi) ! RhsQ,∆(Xn) yDTR τ ∈ RhsQ,∆(Xn) τ q(xi) q(xi)∈ τ yDTR _{[12, 18] DBTA} SRTST yDTR BTA BTA BTA

6. (deterministic top-down

tree-to-string transducer with regular look-ahead, yDTR) (Q, Σ, ∆, Init, R, Π, θ) • Q • Σ • ∆ • (Π, Σ, θ) BTA • Init ⊆ RhsQ,∆(X1)× Π (τ, π)_{̸= (τ}′, π′)_{∈ Init L(π) ∩ L(π}′) = _∅ (Π, Σ, θ) (τ, π)∈ Init π τ Init(π) • R ⊆ !_n∈N(Q_{× Σ}(n) _{× Rhs} Q,∆(Xn)× Πn)

q(σ(x1, . . . , xn))→ τ ⟨π1, . . . , πn⟩ q ∈ Q σ(n) _{∈ Σ τ ∈ Rhs} Q,∆(Xn) π1, . . . , πn ∈ Π rank(σ) = 0 σ() σ _⟨⟩ (q, σ, τ, (π1, . . . , πn)) ̸= (q, σ, τ′, (π′1, . . . , πn′))∈ R i∈ [n] πi ̸= π′i L(πi)∩ L(πi′) =∅ (Π, Σ, θ) q ∈ Q σ(n) _{∈ Σ π} 1, . . . , πn ∈ Π (q, σ, π1, . . . , πn)- π = (π1, . . . , πn) ∈ Πn (q, σ, π1, . . . , πn) (q, σ, π) (q, σ, π)-(q, σ, π)∈ R (q, σ, π)- τ rhs(q, σ, π) ! M = (Q, Σ, ∆, Init, R, Π, θ) yDTR q ∈ Q !q"M : TΣ ⇀ ∆∗ τ ∈ RhsQ,∆(Xn) !τ"M : TΣn ⇀ ∆∗ σ(t1, . . . , tn) ∈ TΣ π1, . . . , πn ∈ Π t1 ∈ L(π1), . . . , tn ∈ L(πn) (q, σ, π1, . . . , πn )-!q"M(σ(t1, . . . , tn)) =!rhs(q, σ, π1, . . . , πn)"M(t1, . . . , tn) ( π′₁, . . . , π′_n R rhs(q, σ, π1, . . . , πn) = rhs(q, σ, π1′, . . . , πn′) ) !τ"M :TΣn ⇀ ∆∗ !ε"M(t1, . . . , tn) = ε !aτ"M(t1, . . . , tn) = a!τ"M(t1, . . . , tn) !q′_(x i)τ"_M(t1, . . . , tn) =!q′"_M(ti)· !τ"_M(t1, . . . , tn) a _{∈ ∆ q}′ _{∈ Q x}i ∈ Xn M _{!M" : T}Σ ⇀ ∆∗ t∈ TΣ π _{∈ Π} t _{∈ L(π) !M" (t) = !Init(π)"M}(t) π (Init π ) _!M" Dom(M ) _!q"M Dom(q) 4. 3 Π θ yDTR M = (Q, Σ, ∆, Init, R, Π, θ) Q = {q} Σ = {f(2)_{, a}(0)_{, b}(0)_{} ∆ = {a, b} Init = {(q(x} 1), πa), (q(x1), πb)} R q(f(x1, x2))→ q(x1)q(x2) ⟨πa, πa⟩, q(f(x1, x2))→ q(x2)q(x1) ⟨πb, πa⟩, q(a) → a, q(f(x1, x2))→ q(x1)q(x2) ⟨πa, πb⟩, q(f(x1, x2))→ q(x2)q(x1) ⟨πb, πb⟩, q(b) → b.

!M" b f(f(b,a),f(a,b))

!M" (f(f(b,a),f(a,b))) = abab

!M" (f(f(b,a),f(a,b))) = !Init(πb)"_M(f(f(b,a),f(a,b)))

=_!q(x1)"M(f(f(b,a),f(a,b))) =_!q"M(f(f(b,a),f(a,b))) =_{!rhs(q, f, ⟨π}b, πa⟩)"_M(f(b,a), f(a,b)) =_!q(x2)q(x1)"M(f(b,a), f(a,b)) =_!q"M(f(a,b))_!q"M(f(b,a)) =_{!rhs(q, f, ⟨π}a, πb⟩)"_M(f(a,b))!rhs(q, f, ⟨πb, πa⟩)"_M(f(b,a)) =_!q(x1)q(x2)"M(a, b)!q(x2)q(x1)"M(b, a) =_!q"M(a)_!q"M(b)_!q"M(a)_!q"M(b) = abab ! M = (Q, Σ, ∆, Init, R, Π, θ) yDTR A = (Σ, Π, θ) M

Dom(M ) _⊆ !_{(τ,π)∈InitL}A(π) yDTR Dom(M ) BTA

Dom(M ) = LA0(π0) A0 = (Σ, Π0, θ0)

BTA LA⊗A0(π0) = LA(π) ∩ Dom(M)

A′ = (Σ, Π_{× Π}0, θ′) def= A⊗ A0 yDTR M′ = (Q, Σ, ∆, Init′, R′, Π× Π0, θ′)

Init′ =_{{(τ, (π, π}0))| (τ, π) ∈ Init} R′ q(σ(x1, . . . , xn))→ rhs(q, σ, π1, . . . , πn) ⟨(π1, π′1), . . . , (πn, π′n)⟩ !M" = !M′_" Dom(M′) = % (τ′_,π′_)∈Init′ LA′(π′) (3.1) yDTR _{(3.1) Dom(q)} Dom(q) = % (q,σ,π)∈R {σ(t1, . . . , tn)| t1 ∈ L(π1), . . . , tn ∈ L(πn)}

4

(SRTST) SRTST Alur D’Antoni (STTsur) SRTST SRTST

4.1

SRTST ( ) Γ ∆ Γ ∆∗ _(evaluation) Γ ∆ E(Γ, ∆) Γ ∆ E ::= ε _{| aE | γE} a ∈ ∆ γ ∈ Γ E(Γ, ∆) α : Γ → ∆∗ _{E(Γ, ∆) ∆}∗ _{e ∈ E(Γ, ∆)} e γ α(γ) ∆ eα Γ Γ′ ∆ Γ E(Γ′, ∆) (assignment) ρ : Γ→ E(Γ′_{, ∆)} ρ = [γ1 := e1, . . . , γn := en] Γ ={γ1, . . . , γn} ei = ρ(γi)∈ E(Γ′, ∆) γ γ := γ Γ Γ′ _∆

A(Γ, Γ′_{, ∆) ρ : Γ → E(Γ}′_{, ∆)}

E(Γ, ∆) E(Γ′, ∆) e_{∈ E(Γ, ∆)} e γ

ρ(γ) Γ′ ∆ eρ _{A(Γ, Γ}′, ∆) Γ′ =∅ α ∈ A(Γ, Γ′_{, ∆) Γ ∆}∗ ρ1 : Γ1 → E(Γ′1, ∆) ρ2 : Γ2 → E(Γ′2, ∆) Γ1 Γ′₁ ∪ Γ′ 2 ρ1ρ2 γ ∈ Γ1 ρ1(γ) ∈ E(Γ′1, ∆) γ₁′ ∈ Γ′ 1 ∩ Γ2 ρ2(γ1′) ∈ E(Γ′2, ∆) γ1′ ∈ Γ′1 \ Γ2 E(Γ′_{1 ∪ Γ}′₂, ∆) (ρ1ρ2)(γ) ρ1 : Γ1 → E(Γ, ∆) ρ2 : Γ2 → E(Γ, ∆) Γ1∩ Γ2 =∅ ρ15 ρ2 Γ15 Γ2 E(Γ, ∆) ( ) ρ15 ρ2 = [γ1 := ρ1(γ1), . . . , γn := ρ1(γn), γ1′ := ρ2(γ1′), . . . , γm′ := ρ2(γm′ )] Γ1 ={γ1, . . . , γn} Γ2 ={γ1′, . . . , γm′ }

5. Γ = {γ1, γ2} ∆ = {a, b} α = [γ1 := ab, γ2 := ba] ∈ A(Γ, ∅, ∆)

ρ1 = [γ1 := γ1γ2, γ2 := γ1b] ∈ A(Γ, Γ, ∆) ρ1α = ⎡ ⎣γ1 := ab_()*+ γ1 ba ()*+ γ2 , γ2 := ab_()*+ γ1 b ⎤ ⎦ ρ2 = [γ1 := aγ1γ2b, γ2 := γ2γ1] ρ2ρ1α = ρ2(ρ1α) = ρ2[γ1 := abba, γ2 := abb] = ⎡ ⎣γ1 := a abba_{( )* +} γ1 abb ()*+ γ2 b, γ2 := abb_()*+ γ2 abba ( )* + γ1 ⎤ ⎦ (ρ2ρ1)α = ⎡ ⎢ ⎣γ1 := a γ1γ2 ()*+ γ1 b γ1b ()*+ γ2 , γ2 := γ1b ()*+ γ2 γ1γ2 ()*+ γ1 ⎤ ⎥ ⎦ α = ⎡ ⎣γ1 := a ab_()*+ γ1 ba ()*+ γ2 b ab_()*+ γ2 bb, γ1 := ab_()*+ γ1 b ab_()*+ γ1 ba ()*+ γ2 ⎤ ⎦ !

4.2

7. (deterministic streaming ranked-tree-to-string transducer, SRTST) (S, Σ, ∆, P, s0, Γ, F, δc, δr, ρc, ρr) • S • Σ • ∆ • P • s0 ∈ S • Γ • F : S ⇀ E(Γ, ∆) • δc : S× Σ → S × P • δr : S× P × Σ → S • ρc : S× Σ → A(Γ, Γ, ∆) • ρr : S× P × Σ → A(Γ, Γ 5 Γp, ∆) Γp Γ∩ Γp =∅ γ _{∈ Γ} γp ∈ Γp ! Γ Γ ∆ Γ Γ∪ Γp ∆ β γp ∈ Γp β(γ)

Φ = S× (P × A(Γ, ∅, ∆))∗ _{× A(Γ, ∅, ∆) Φ SRTST (configuration)}

(s, Λ, α) _{∈ Φ} s Λ α αε = [γ := ε]γ∈Γ SRTST δ : Φ× ˆΣ ⇀ Φ (s0, ε, αε) a ∈ ˆΣ δ(_{−, a)} b _{∈ Σ} a = _⟨b (s, Λ, α) δ((s, Λ, α), a) = (s′, (p, α′)Λ, αε) • s′ _{p δ} c(s, b) = (s′, p) • (p, α′_{)Λ Λ (p, α}′₎ α′ = ρc(s, b)α α′ ρc(s, b) γ ∈ Γ

(s, α) =⟨σ⇒ (s′, [γ := ε]_γ∈Γ) .. . (p, ρc(s, σ)α) .. . Λ (p, ρc(s, σ)α)Λ 4.1 (s, α) (s′, ρr(s, p, σ) [γp := β(γ)]_γ∈Γα) σ⟩ =⇒ (p, β) .. . ... (p, β)Λ Λ 4.2 α(γ) 4.1 b_{∈ Σ} a = b_⟩ (s, (p, β)Λ, α) δ((s, (p, β)Λ, α), a) = (s′, Λ, α′) • s′ _δ r(s, p, b) = s′ • Λ (p, β)Λ (p, β) • α′ = ρr(s, p, b)βpα βp = [γp := β(γ)]_γ∈Γ α′ ρr(s, p, b) γp ∈ Γp β(γ) γ _{∈ Γ} α(γ) 4.2 SRTST T a _{∈ ˆ}Σ c c′ c=_⇒a T c′ c′ = δ(c, a) T c=⇒ ca ′ _{c 0 c}′ c =_⇒∗ _c′ _{δ Σ}ˆ∗ _δˆ _{w∈ ˆΣ}∗ c c′ c =w_⇒T c′ c′ = ˆδ(c, w) T !T " : ⌊TΣ⌋ ⇀ ∆∗ w ∈ ⌊TΣ⌋

ˆ δ((s0, ε, αε), w) = (s, ε, α) F (s) !T " (w) !T " (w) = F (s)α !T " Dom(T ) 6. 4 yDTR _{SRTST T = (S, Σ, ∆, P, s} 0, Γ, F, δc, δr, ρc, ρr) SRTST S = {s?, sa, sb} Σ = {f(2), a(0), b(0)} ∆ = {a, b} P ={p?, pa, pb} s0 = s? Γ = {γ} δc σ ∈ Σ h ∈ {a, b, ?} δc(sh, σ) = (s?, ph) δr s∈ S σ ∈ Σ δr(s, pa, σ) = sa, δr(sa, p?, σ) = sa, δr(s?, p?, a) = sa, δr(s, pb, σ) = sb, δr(sb, p?, σ) = sb, δr(s?, p?, b) = sb. ρc s∈ S ρc(s?, a) = [γ := a] , ρc(sa, a) = [γ := γa] , ρc(sa, b) = [γ := γb] , ρc(s, f) = [γ := γ] , ρc(s?, b) = [γ := b] , ρc(sb, a) = [γ := aγ] , ρc(sb, b) = [γ := bγ] ρr s∈ S ρr(s, p?, a) = [γ := γp] , ρr(s, pa, f) = [γ := γpγ] , ρr(s, p?, f) = [γ := γ] , ρr(s, p?, b) = [γ := γp] , ρr(s, pb, f) = [γ := γγp] . s ∈ S F (s) = γ f(f(b,a),f(a,b))) T #−$

(s?,#$ , αε ) ⟨f =_{⇒ (s}?,#(p?, αε)$ , αε ) ⟨f =⇒ (s?,#(p?, αε)(p?, αε)$ , αε ) ⟨b =_{⇒ (s}?,#(p?, [γ := b])(p?, αε)(p?, αε)$ , αε ) b⟩ =⇒ (sb,#(p?, αε)(p?, αε)$ , [γ := b] ) (4.1) ⟨a =_{⇒ (s}?,#(pb, [γ := ab])(p?, αε)(p?, αε)$ , αε ) a⟩ =⇒ (sb,#(p?, αε)(p?, αε)$ , [γ := ab] ) f⟩ =_{⇒ (s}b,#(p?, αε)$ , [γ := ab] ) ⟨f =_{⇒ (s}?,#(pb, [γ := ab])(p?, αε)$ , αε ) ⟨a =⇒ (s?,#(p?, [γ := a])(pb, [γ := ab])(p?, αε)$ , αε ) a⟩ =_{⇒ (s}a,#(pb, [γ := ab])(p?, αε)$ , [γ := a] ) ⟨b =⇒ (s?,#(pa, [γ := ab])(pb, [γ := ab])(p?, αε)$, αε ) b⟩ =_{⇒ (s}a,#(pb, [γ := ab])(p?, αε)$ , [γ := ab] ) (4.2) f⟩ =⇒ (sb,#(p?, αε)$ , [γ := abab]) f⟩ =_{⇒ (s}b,#$ , [γ := abab]) F (sb) = γ !T " (f(f(b,a),f(a,b))) = abab (4.1) ⟨a 4.3 (4.2) f⟩ 4.4 4.3 4.4 ==a/ρ⇒ a∈ ˆΣ ρ !

(sb, [γ := b]) =======⟨a/[γ:=aγ]⇒ (s?, [γ := ε]) (p?, [γ := ε]) (p?, [γ := ε]) (p?, [γ := ab]) (p?, [γ := ε]) (p?, [γ := ε]) γ γ ε 4.3 ( (4.1)) (sa, [γ := ab]) _=======f⟩/[γ:=γγp⇒] (sb, [γ := abab]) (pb, [γ := ab]) (p?, [γ := ε]) (p?, [γ := ε]) γ γ γp ( ) γ 4.4 ( (4.2))

5 SRTST

yDT

R

5.1 SRTST yDTR _{5.3 yDT}R SRTST 5.5 SRTST

5.1 yDT

R

SRTST

yDTR _{SRTST SRTST} (bottom-up) SRTST SRTST s _{∈ S σ ∈ Σ} δc(s, σ) = (s′, p) s′ = s0 ρc(s, σ) = [γ := γ]γ∈Γ SRTST 1. M yDTR t ∈ Dom(M) !M" (t) = !T " (⌊t⌋) SRTST T !

. M = (Q, Σ, ∆, Init, R, Π, θ) yDTR (Σ, Π, θ) DBTA

t _{∈ Dom(M) !M" (t) = !T " (⌊t⌋)} SRTST T = (S, Σ, ∆, P, s0, Γ, F, δc, δr, ρc, ρr) m = max({1} ∪ {rank(σ) | σ ∈ Σ}) S = Π≤m Γ = Q× Xm P = Π≤m s0 = () δc σ(n) _{∈ Σ π ∈ S} δc(π, σ) = ((), π) δr σ(n) ∈ Σ π ∈ Πn π′ ∈ Π≤m−1 δr(π, π′, σ) = π′|| θ(σ, π) ρc π ∈ S σ ∈ Σ ρc(π, σ) = [γ := γ]_γ∈Γ ρr σ(n) ∈ Σ π ∈ Πn π′ ∈ Π≤m−1 ρr(π, π′, σ) = 0 q(x_|π′_|+1) :=U(q, σ, π)1 q∈Q5 [q(xk) := q(xk)p]q∈Q, xk∈X_|π′|

U : Q × Σ(n)_{× Π}n _{→ E(Γ, ∆)} U(q, σ, π) = 2 rhs(q, σ, π) (q, σ, π)-ε U xl∈ Xm\ X_|π′_|+1 q(xl) [q(xl) := q(xl)]_{q∈Q, xl∈Xm\X|π′|+1} F (τ, π)_{∈ Init} F ((π)) = τ ρr (q, σ, π)- q(x|π′_|+1) ε yDTR (3.1) t _{∈ T}Σ (q, σ, π)- t ̸∈ Dom(M) t ̸∈ !(τ,π)∈Init L(π) (q, σ, π)- t ∈ L(π′) π′ F ⌊t⌋ !τ"M q(x_|π′_|+1) ε yDTR SRTST SRTST SRTST 7. 4 yDTR _{M SRTST T 1} T = (S, Σ, ∆, P, s0, Γ, F, δc, δr, ρc, ρr) S P Γ S =_{{(), (π}a), (πb), (πa, πa), (πa, πb), (πb, πb), (πb, πa)} = Π≤2, P ={(), (πa), (πb), (πa, πa), (πa, πb), (πb, πb), (πb, πa)} = Π≤2, Γ ={q(x1), q(x2)} = Q× X2. s0 = () δc σ ∈ Σ δc((), σ) = ((), ()), δc((πa), σ) = ((), (πa)), δc((πb), σ) = ((), (πb)). π ∈ Π2 _⌊T Σ⌋ π δr π ∈ Π δr((), () , a) = (πa), δr((πa, π), () , f) = (πa), δr((), () , b) = (πb), δr((πb, π), () , f) = (πb), δr((), (πa), a) = (πa, πa), δr((πa, π), (πa), f) = (πa, πa), δr((), (πa), b) = (πa, πb), δr((πb, π), (πa), f) = (πa, πb), δr((), (πb), a) = (πb, πa), δr((πa, π), (πb), f) = (πb, πa), δr((), (πb), b) = (πb, πb), δr((πb, π), (πb), f) = (πb, πb)

δr ρc s ∈ S σ ∈ Σ ρc(s, σ) = [γ := γ]γ∈Γ ρr π1, π2 ∈ Π ρr(() , () , a) = [q(x1) := a] , ρr(() , () , b) = [q(x1) := b] , ρr(() , (π1), a) = [q(x2) := a, q(x1) := q(x1)p] , ρr(() , (π1), b) = [q(x2) := b, q(x1) := q(x1)p] , ρr((πa, π1), () , f) = [q(x1) := q(x1)q(x2)] , ρr((πb, π1), () , f) = [q(x1) := q(x2)q(x1)] , ρr((πa, π1), (π2), f) = [q(x2) := q(x1)q(x2), q(x1) := q(x1)p] , ρr((πb, π1), (π2), f) = [q(x2) := q(x2)q(x1), q(x1) := q(x1)p] . F ((πa)) = q(x1) F ((πb)) = q(x1) T f(f(b,a),f(a,b)) (() ,_#$ , αε ) ⟨f =_{⇒ (()} ,_{#((), α}ε)$ , αε ) ⟨f =_{⇒ (()} ,_{#((), α}ε)((), αε)$ , αε ) ⟨b =⇒ (() ,_{#((), α}ε)((), αε)((), αε)$ , αε ) b⟩ =_{⇒ ((π}b) ,#((), αε)((), αε)$ , [q(x1) := b] ) ⟨a =⇒ (() ,_#((πb), [q(x1) := b])((), αε)((), αε)$ , αε ) a⟩ =_{⇒ ((π}b, πa),#((), αε)((), αε)$ , [q(x2) := a, q(x1) := b] ) f⟩ =⇒ ((πb) ,#((), αε)$ , [q(x1) := ab] ) ⟨f =_{⇒ (()} ,_#((πb), [q(x1) := ab])((), αε)$ , αε ) ⟨a =_{⇒ (()} ,_{#((), α}ε)((πb), [q(x1) := ab])((), αε)$ , αε ) a⟩ =⇒ ((πa) ,#((πb), [q(x1) := ab])((), αε)$ , [q(x1) := a] ) ⟨b =_{⇒ (()} ,_#((πa), [q(x1) := a])((πb), [q(x1) := ab])((), αε)$, αε ) b⟩ =⇒ ((πa, πb),#((πb), [q(x1) := ab])((), αε)$ , [q(x2) := b, q(x1) := a] ) f⟩ =_{⇒ ((π}b, πa),#((), αε)$ , [q(x2) := ab, q(x1) := ab]) f⟩ =⇒ ((πb) ,#$ , [q(x1) := abab] )

F (πb) = q(x1) !T " (f(f(b,a),f(a,b))) = abab !

5.2 yDT

R

SRTST

5.1 SRTST yDTR yDTR yDTR _{M = (Q, Σ, ∆, Init, R, Π, θ) 1} SRTST T = (S, Σ, ∆, P, s0, Γ, F, δc, δr, ρc, ρr) 2. t ∈ TΣ π ∈ Π δ((π, Λ, α),⌊t⌋) = (π || ˆθ(t), Λ, α′) ! . t t1, . . . , tn ∈ TΣ π1 = ˆθ(t1), . . . , πn = ˆθ(tn) i ∈ [n] δ((πi, Λi, αi),⌊ti⌋) = (πi|| ˆθ(ti), Λi, α′i) t = σ(t1, . . . , tn)∈ TΣ δ((π, Λ, α),⌊t⌋) (π, Λ, α)===⟨σ_{⇒ ((), (π, α)Λ, α}0) ⌊t1⌋ ==⇒ ((π1), (π, α)Λ, α1) ==⇒∗ · · · ⌊tn⌋ ===_{⇒ ((π}1, . . . , πn), (π, α)Λ, αn) σ⟩ ===_{⇒ (π || θ(σ, π}1, . . . , πn), Λ, α′) (Σ, Π, θ) DBTA θ(σ(tˆ 1, . . . , tn)) = θ(σ, ˆθ(t1), . . . , ˆθ(tn)) = θ(σ, π1, . . . , πn) δ((π, Λ, α),⌊t⌋) = (π || ˆθ(t), Λ, α′) 3. T M ! . (3.1) Dom(M ) = 3_{(τ,π)∈Init L(π)} 2 t _{∈ T}Σ δ(((), ε, α0),⌊t⌋) = ((ˆθ(t)), ε, α) 1 Init ⌊t⌋ ∈ Dom(T ) ⇐⇒ (ˆθ(t)) ∈ Dom(F ) ⇐⇒ (τ, ˆθ(t)) ∈ Init ⇐⇒ t ∈ Dom(M) 4. yDTR M = (Q, Σ, ∆, Init, R, Π, θ) τ ∈ RhsQ,∆(Xn) t1. . . , tn ∈ TΣ q(xi)∈ τ ti∈ Dom(q) !τ"M(t1, . . . , tn) = τ [q(xi) :=!q"M(ti)]q(xi)∈τ

! . t τ 5. m = max({1} ∪ {rank(σ) | σ ∈ Σ}) t = σ(t1, . . . , tn) ∈ TΣ π _{∈ Π}≤m−1 _{δ((π, Λ, α),⌊t⌋) = (π}′_{, Λ, α}′₎ α′ =0q(x_|π|+1) :=_!q"M(t)1_q∈Q5 [q(xi) := α(q(xi))]_{q∈Q, xi∈X|π|} !q"M(t) !q"M(t) = ε ! . t t1, . . . , tn ∈ TΣ i ∈ [n] δ((πi, Λi, αi),⌊ti⌋) = (π′i, Λi, α′i) α′ =0q(x_|πi|+1) :=_!q"M(ti) 1 q∈Q5 [q(xj) := αi(q(xj))]q∈Q,xj∈X_|πi| σ(n) _{∈ Σ δ((π, Λ, α),⌊σ(t} 1, . . . , tn)⌋) = (π′, Λ, α′) T (π, Λ, α) ⟨σ ===⇒ ((), (π, ρc(π, σ)α)Λ, α0) ⌊t1⌋ ==_{⇒ ((π}′′₁), (π, ρc(π, σ)α)Λ, [q(x1) :=!q"_M(t1)]_q∈Q5 [q(x) := ε]_{q∈Q, x∈Xm\X1}) ==⇒∗ · · · ⌊tn⌋ ===_{⇒ (π}′′, (π, ρc(π, σ)α)Λ, [q(xi) :=!q"M(ti)]_{q∈Q, xi∈Xn} 5 [q(x) := ε]q∈Q, x∈Xm\Xn) σ⟩ ===⇒ (π′, Λ, ρr(π′′, π, σ)β([q(xi) :=!q"M(ti)]_{q∈Q, xi∈Xn} 5 [q(x) := ε]q∈Q, x∈Xm\Xn)) π′′ = (π₁′′, . . . , π′′_n) β = [γp := γρc(π, σ)α]_γ∈Γ = [γp := α(γ)]_γ∈Γ α′(q(x_|π|+1)) α′(q(x_|π|+1)) = q(x_|π|+1)ρr(π′′, π, σ)β([q(xi) :=!q"_M(ti)]_{q∈Q, xi∈Xn} 5 [q(x) := ε]_{q∈Q, x∈Xm\Xn}) = q(x_|π|+1)(0q(x_|π|+1) :=U(q, σ, π′′)1_q∈Q5 [q(xk) := q(xk)p]_{q∈Q, xk∈X} |π′|) β([q(xi) :=!q"M(ti)]_{q∈Q,xi∈Xn} 5 [q(x) := ε]q∈Q, x∈Xm\Xn) =_{U(q, σ, π}′′)β([q(xi) :=!q"_M(ti)]_{q∈Q, xi∈Xn} 5 [q(x) := ε]_{q∈Q, x∈Xm\Xn}) σ(t1, . . . , tn)̸∈ Dom(q) α′(q(x_|π|+1)) = εβ([q(xi) :=!q"_M(ti)]_{q∈Q, xi∈Xn} 5 [q(x) := ε]_{q∈Q, x∈Xm\Xn}) = ε

t∈ Dom(q) (q, σ, π′′ )-α′(q(x_|π|+1)) = rhs(q, σ, π′′)β([q(xi) :=!q"_M(ti)]_{q∈Q, xi∈Xn}5 [q(x) := ε]_{q∈Q, x∈Xm\Xn}) = rhs(q, σ, π′′) [γp := α(γ)]_γ∈Γ([q(xi) :=!q"_M(ti)]_{q∈Q, xi∈Xn} 5 [q(x) := ε]_{q∈Q, x∈Xm\Xn}) = rhs(q, σ, π′′) [q(xi) :=!q"_M(ti)]_{q∈Q, xi∈Xn} 2 t1 ∈ L(π1′′), . . . , tn ∈ L(πn′′) 4 α′(q(x_|π|+1)) = rhs(q, σ, π′′) [q(xi) :=!q"_M(ti)]_{q∈Q, xi∈Xn} =_{!rhs(q, σ, π}′′)_"M(t1, . . . , tn) =_!q"M(σ(t1, . . . , tn)) q ∈ Q xj ∈ X|π| α′(q(xj)) = α(q(xj)) α′(q(xj)) α′(q(xj)) = q(xj)(0q(x|π|+1) :=U(q, σ, π′′)1_q∈Q5 [q(xk) := q(xk)p]_{q∈Q, x∈X} |π′|) β([q(xi) :=!q"_M(ti)]_{q∈Q, xi∈Xn}5 [q(x) := ε]_{q∈Q, x∈Xm\Xn}) = q(xj)pβ([q(xi) :=!q"M(ti)]_{q∈Q, xi∈Xn}5 [q(x) := ε]q∈Q, x∈Xm\Xn) = q(xj)p[γp := α(γ)]_γ∈Γ([q(xi) :=!q"_M(ti)]_{q∈Q, xi∈Xn} 5 [q(x) := ε]_{q∈Q, x∈Xm\Xn}) = α(q(xj))([q(xi) :=!q"_M(ti)]_{q∈Q, xi∈Xn}5 [q(x) := ε]_{q∈Q, x∈Xm\Xn}) = α(q(xj)) α′ =0q(x_|π|+1) :=_!q"M(t)1_q∈Q5[q(xi) := α(q(xi))]_{q∈Q,xi∈X|π|} 6. t _{∈ Dom(M) !M" (t) = !T " (⌊t⌋)} ! . 3 Dom(M ) = Dom(T ) 5 t _{∈ T}Σ δ(((), ε, α0)) = ((ˆθ(t)), ε, α) α = [q(x1) :=!q"M(t)]q∈Q !T " (⌊t⌋) = F ((ˆθ(t)))α = Init(ˆθ(t)) [q(x1) :=!q"_M(t)]_q∈Q =%Init(ˆθ(t))& M(t) =_{!M" (t)}

5.3 SRTST

yDT

R SRTST yDTR

7. T SRTST w∈ Dom(T ) !T " (w) = !M" (⌈w⌉)

yDTR _{M !}

. T = (S, Σ, ∆, P, s0, Γ, F, δc, δr, ρc, ρr) SRTST w ∈ Dom(T )

!T " (w) = !M" (⌈w⌉) yDTR _{M = (Q, Σ, ∆, Init, R, Π, θ)}

(sc, σ(n), sr), (sc₁, σ1, s1r), . . . , (scn, σn, srn)∈ S × Σ(>0)× S vst

vst (valid state transition)

vst((sc, σ(n), sr), (sc₁, σ1, sr1), . . . , (scn, σn, srn)) = ∃s1, . . . , sn ∈ S. ∃p, p1, . . . , pn ∈ P. (_{∀j ∈ [n]. δ}c(scj, σj) = (sj, pj))∧ (_{∀j ∈ [n − 1]. δ}r(srj, pj, σj) = scj+1)∧ δc(sc, σ) = (sc1, p)∧ δr(srn, pn, σn) = sr vst (sc, σ(n), sr), (sc₁, σ1, sr1), . . . , (scn, σn, srn)∈ S × Σ × S T sc ⟨σ=_{⇒ s}c₁ ==⟨σ_{⇒ s}1 1 =⇒∗ sr1 σ1⟩ ==_{⇒ · · · =⇒}∗ sc_n ==⟨σ_{⇒ s}n n =⇒∗ srn σn⟩ ==_{⇒ s}r σ⟩=_{⇒ s}′ vst M Π i _{∈ N} Πi i = 0 Π0 π = (sc_{, e, s}r_{)∈ S×Σ}(0)_{×S p∈ P δ} c(sc, e) = (sr, p) sc e sr Π0 ={(sc, e, sr)∈ S×Σ(0)×S | δc(sc, e) = (sr, p)} Π0 T sc ⟨e=_{⇒ s}r e⟩=_{⇒ s}′ Πi Πi Πi−1 vst Π_i−1 Πi = Π0∪ {(sc, σ(n), sr)_{∈ S × Σ × S | ∃π}1, . . . , πn∈ Πi−1. vst((sc, σ, sr), π1, . . . , πn)} (5.1) Πi Π0 ⊆ Π1 ⊆ · · · ⊆ Πm−1 = Πm ⊆ S × Σ × S S Σ Πm = Πm−1 m_{∈ N} m Π = Πm

e ∈ Σ(0) _{θ(e) ={(s}c_{, e, s}r_{)∈ Π} σ ∈ Σ}(>0) _π 1, . . . , πn ∈ Π θ(σ(n), π1, . . . , πn) ={(sc, σ, sr)∈ Π | vst((sc, σ, sr), π1, . . . , πn)} Q = S × S × Γ π = (sc, σ(n), sr) ∈ Π γ ∈ Γ (sc, σ, sr)∈ θ(σ, π1, . . . , πn) π1, . . . , πn ∈ Π (sc, sr, γ)(σ(x1, . . . , xn))→ W((sc, σ, sr), π1, . . . , πn, γ) ⟨π1, . . . , πn⟩ W Πn+1 × Γ RhsQ,∆(Xn) W(π, π1, . . . , πn, γ) = γαrn(βnc 5 ηn)· · · αr1(β1c5 η1)αΓε ∈ RhsQ,∆(Xn) π1 = (sc1, σ1, sr1), . . . , πn = (scn, σn, srn) s1, . . . , sn ∈ S i _{∈ [n]} δc(sci, σi) = (si, p) ηi ηi = [γ := (sci, sri, γ)(xi)]_γ∈Γ αr_i = ρr(sri, pi, σ) βic = [γp := ρc(sci, σ)(γ)]_γ∈Γ αΓ ε = [γ := ε]γ∈Γ Init = $ σ∈Σ {(F (s′′)αr(sr₀, p, σ)(βc(σ)5 η(σ, sr0))αΓε, (s0, σ, sr0))| (s0, σ, sr0)∈ Π. ∃s′, s′′ ∈ S. ∃p ∈ P. δc(s0, σ) = (s′, p)∧ δr(sr0, p, σ) = s′′∧ s′′ ∈ Dom(F )} αr_(sr 0, p, σ) = ρr(sr0, p, σ) βc(σ) = [γp := ρc(s0, σ)(γ)]_γ∈Γ η(σ, sr0) = [γ := (s0, sr0, γ)(x1)]_γ∈Γ αΓε = [γ := ε]γ∈Γ SRTST yDTR yDTR 8. 6 SRTST T yDTR _{M 7} M = (Q, Σ, ∆, Init, R, Π, θ) yDTR _{Q = S× Σ × S} (5.1) Πi Π0 ={(s?, a, s?), (s?, b, s?), (sa, a, s?), (sa, b, s?), (sb, a, s?), (sb, b, s?)} Π1 = Π0∪ {(s?, f, sa), (s?, f, sb), (sa, f, sa), (sa, f, sb), (sb, f, sa), (sb, f, sb)} Π2 = Π1∪ {(s?, f, sa), (s?, f, sb), (sa, f, sa), (sa, f, sb), (sb, f, sa), (sb, f, sb)} = Π1

Π = Π2 θ θ(a) =_{(s?, a, s?), (sa, a, s?), (sb, a, s?)}, θ(b) =_{(s?, b, s?), (sa, b, s?), (sb, b, s?)}, θ(f, (s?, a, s?), (sa, a, s?)) ={(s?, f, sa), (sa, f, sa), (sb, f, sa)}, θ(f, (s?, a, s?), (sa, b, s?)) ={(s?, f, sa), (sa, f, sa), (sb, f, sa)}, θ(f, (s?, a, s?), (sa, f, sa)) ={(s?, f, sa), (sa, f, sa), (sb, f, sa)}, θ(f, (s?, a, s?), (sb, f, s?)) ={(s?, f, sa), (sa, f, sa), (sb, f, sa)}, θ(f, (s?, b, s?), (sb, a, s?)) ={(s?, f, sb), (sa, f, sb), (sb, f, sb)}, θ(f, (s?, b, s?), (sb, b, s?)) ={(s?, f, sb), (sa, f, sb), (sb, f, sb)}, θ(f, (s?, b, s?), (sb, f, sa)) ={(s?, f, sb), (sa, f, sb), (sb, f, sb)}, θ(f, (s?, b, s?), (sb, f, s?)) ={(s?, f, sb), (sa, f, sb), (sb, f, sb)}, θ(f, (s?, f, sa), (sa, a, s?)) ={(s?, f, sa), (sa, f, sa), (sb, f, sa)}, θ(f, (s?, f, sb), (sb, a, s?)) ={(s?, f, sb), (sa, f, sb), (sb, f, sb)}, θ(f, (s?, f, sa), (sa, b, s?)) ={(s?, f, sa), (sa, f, sa), (sb, f, sa)}, θ(f, (s?, f, sb), (sb, b, s?)) ={(s?, f, sb), (sa, f, sb), (sb, f, sb)}, θ(f, (s?, f, sa), (sa, f, sa)) ={(s?, f, sa), (sa, f, sa), (sb, f, sa)}, θ(f, (s?, f, sa), (sa, f, sb)) ={(s?, f, sa), (sa, f, sa), (sb, f, sa)}, θ(f, (s?, f, sb), (sb, f, sa)) ={(s?, f, sb), (sa, f, sb), (sb, f, sb)}, θ(f, (s?, f, sb), (sb, f, sb)) ={(s?, f, sb), (sa, f, sb), (sb, f, sb)}. R s_{∈ S} (s, sa, γ)(f(x1, x2))→ aa ⟨(s?, a, s?), (sa, a, s?)⟩, (s, sa, γ)(f(x1, x2))→ ab ⟨(s?, a, s?), (sa, b, s?)⟩, (s, sb, γ)(f(x1, x2))→ ab ⟨(s?, b, s?), (sb, a, s?)⟩, (s, sb, γ)(f(x1, x2))→ bb ⟨(s?, b, s?), (sb, b, s?)⟩, (s, sa, γ)(f(x1, x2))→ (s?, sa, γ)(x1)a ⟨(s?, f, sa), (sa, a, s?)⟩, (s, sa, γ)(f(x1, x2))→ (s?, sa, γ)(x1)b ⟨(s?, f, sa), (sa, b, s?)⟩, (s, sb, γ)(f(x1, x2))→ a(s?, sa, γ)(x1) ⟨(s?, f, sb), (sb, a, s?)⟩, (s, sb, γ)(f(x1, x2))→ b(s?, sa, γ)(x1) ⟨(s?, f, sb), (sb, b, s?)⟩, (s, sa, γ)(f(x1, x2))→ (s?, sa, γ)(x1)(sa, sa, γ)(x2) ⟨(s?, f, sa), (sa, f, sa)⟩, (s, sa, γ)(f(x1, x2))→ (s?, sa, γ)(x1)(sa, sb, γ)(x2) ⟨(s?, f, sa), (sa, f, sb)⟩, (s, sb, γ)(f(x1, x2))→ (sb, sa, γ)(x2)(s?, sb, γ)(x1) ⟨(s?, f, sb), (sb, f, sa)⟩, (s, sb, γ)(f(x1, x2))→ (sb, sb, γ)(x2)(s?, sb, γ)(x1) ⟨(s?, f, sb), (sb, f, sb)⟩. Init ={⟨a, (s?, a, s?)⟩, ⟨b, (s?, b, s?)⟩, ⟨(s?, sa, γ)(x1), (s?, f, sa)⟩, ⟨(s?, sb, γ)(x1), (s?, f, sb)⟩}

M f(f(b,a),f(a,b)) (Σ, Π, θ) f(f(b,a),f(a,b)) ˆ θ(a) ={(s?, a, s?), (sa, a, s?), (sb, a, s?)} ˆ θ(b) =_{(s?, b, s?), (sa, b, s?), (sb, b, s?)} ˆ θ(f(a,b)) =_{(s?, f, sa), (sa, f, sa), (sb, f, sb)} ˆ θ(f(b,a)) ={(s?, f, sb), (sa, f, sa), (sb, f, sb)} ˆ θ(f(f(b,a),f(a,b))) ={(s?, f, sb), (sa, f, sb), (sb, f, sb)} !M" (f(f(b,a),f(a,b))) !M" (f(f(b,a),f(a,b))) = abab

!M" (f(f(b,a),f(a,b))) = !Init((s?, f, sb))" (f(f(b,a),f(a,b)))

=_!(s?, sb, γ)(x1)" (f(f(b,a),f(a,b))) =_!(s?, sb, γ)" (f(f(b,a),f(a,b))) =_!rhs((s?, sb, γ), f,⟨(s?, f, sb), (sb, f, sa)⟩)" (f(b,a), f(a,b)) =_!(sb, sa, γ)(x2)(sa, sb, γ)(x1)" (f(b,a), f(a,b)) =_!(sb, sa, γ)" (f(a,b)) !(sa, sb, γ)" (f(b,a)) =_!rhs((sb, sa, γ), f,⟨(s?, a, s?), (sa, b, s?)⟩)" (a, b) !rhs((sa, sb, γ), f,⟨(s?, b, s?), (sb, a, s?)⟩)" (b, a)

=_{!ab" (a, b) !ab" (b, a)}

= abab !

5.4 SRTST

yDT

R 5.3 yDTR SRTST SRTST SRTST T = (S, Σ, ∆, P, s0, Γ, F, δc, δr, ρc, ρr) 7 yDTR M = (Q, Σ, ∆, Init, R, Π, θ) 8. σ(t1, . . . , tn)∈ TΣ (sc, Λ, α)=⟨σ⇒ (s′, (p, α′)Λ, α′)==⌊t1⇒ · · ·⌋ ⌊tn⌋ ===⇒ (sr_{, (p, α}′_{)Λ, α}′′₎₌σ_{⇒ (s}⟩ ′′_{, Λ, α}′′₎ (sc_{, σ, s}r_{)∈ Π σ(t} 1, . . . , tn)∈ L((sc, σ, sr)) ! . Π θ 9. M T !

. 8 Init σ(t1, . . . , tn)∈ TΣ ⟨σ ⌊t1⌋ · · · ⌊tn⌋ σ⟩ ∈ Dom(T ) ⇐⇒ (s0, ε, αε)=⟨σ⇒T (s′, (p, αε), α) ⌊t 1⌋···⌊tn⌋ ======_⇒T (sr0, αε, α)=σ⟩⇒T (s′′, ε, α′)∧ s′′ ∈ Dom(F ) ⇐⇒ δc(s0, σ) = (s′, p)∧ δr(s0r, p, σ) = s′′∧ s′′ ∈ Dom(F ) ∧ t ∈ L((s0, σ, sr0)) ⇐⇒ (τ, (s0, σ, sr0))∈ Init ∧ t ∈ L((s0, σ, sr0)) ⇐⇒ ⌈⟨σ ⌊t1⌋ · · · ⌊tn⌋ σ⟩⌉ ∈ Dom(M) ⇐⇒ σ(t1, . . . , tn)∈ Dom(M) ρ1 ∈ A(Γ1, Γ′1, ∆) ρ2 ∈ A(Γ2, Γ2′, ∆) Γ1∩ Γ2 = ∅ Γ′1∩ Γ2 = ∅ ρ1ρ2 = [γ1 := ρ1(γ1)]_γ1∈Γ1[γ2 := ρ2(γ′)]_γ2∈Γ2 = 4 γ := 2 ρ1(γ) (γ ∈ Γ1 ) γ (γ _{∈ Γ}2 ) 5 γ∈Γ1+Γ2 4 γ := 2 γ (γ ∈ Γ′ 1 ) ρ2(γ) (γ ∈ Γ2 ) 5 γ∈Γ′ 1+Γ2 = 4 γ := 2 ρ1(γ) [γ′ := γ′]_γ′_∈Γ′ 1 (γ ∈ Γ1 ) γ [γ′ := ρ2(γ)]γ′_∈Γ2 (γ ∈ Γ2 ) 5 γ∈Γ1+Γ2 = 4 γ := 2 ρ1(γ) (γ ∈ Γ1 ) ρ2(γ) (γ ∈ Γ2 ) 5 γ∈Γ1+Γ2 = ρ15 ρ2 ρ′_{1 ∈ A(Γ}1, Γ′1, ∆) α ∈ A(Γ′1,∅, ∆) ρ15 ρ2 = ρ1ρ2 = [γ1 := γ1ρ′1α]γ1∈Γ1ρ2 = ([γ1 := ρ′1(γ1)]_γ1∈Γ1α)ρ2 = ([γ1 := ρ′1(γ1)]γ1∈Γ1 5 ρ2)α = (ρ′_{15 ρ}2)α ρr _{∈ A(Γ, Γ ∪ Γ} p, ∆) ρc ∈ A(Γ, Γ, ∆) α∈ A(Γ, ∅, ∆) α′ _{∈ A(Γ, ∅, ∆)} ρr[γp := γρcα]_γ∈Γα′ = ρr[γp := γρcα]_γ∈Γ[γ := ψγ]_γ∈Γ[ψγ := α′(γ)]_γ∈Γ ψγ ∈ E(ΨΓ, ∆) γ Γ∩ ΨΓ = ∅ [γp := γρcα]_γ∈Γ ∈ A(Γp,∅, ∆) [γ := ψγ]_γ ∈ A(Γ, ΨΓ, ∆) Γp∩ Γ = ∅ ∅ ∩ ΨΓ =∅ Γ ∩ ΨΓ=∅ ρr[γp := γρcα]_γ∈Γα′ = ρr([γp := γρcα]_γ∈Γ5 [γ := ψγ]_γ∈Γ) [ψγ := α′(γ)]_γ∈Γ = ρr(([γp := ρc(γ)]_γ∈Γ5 [γ := ψγ]_γ∈Γ)α) [ψγ := α′(γ)]_γ∈Γ

ρr, [γp := ρc(γ)]_γ∈Γ5 [γ := ψγ]_γ∈Γ ∈ A(Γ ∪ Γp, Γ5 Ψγ, ∆) ρr[γp := γρcα]_γ∈Γα′ = ρr([γp := ρc(γ)]_γ∈Γ5 [γ := ψγ]_γ∈Γ)α [ψγ := α′(γ)]_γ∈Γ SRTST ψ_{∈ A(Ψ, ∅, ∆) α ∈ A(Γ, Γ}′_{, ∆) Γ∩ Ψ = ∅ Γ}′_{∩ Ψ = ∅} αρ = ρα SRTST 10. σ1 t1, . . . , σn tn ∈ TΣ i∈ [n] (sc_i, Λ, αi) ⟨σ i ===========⇒ (s′i, (pi, ρ(sci, σi)α)Λ′, αε) ⌊ti 1⌋···⌊t_{i rank(σi)}⌋ ============⇒ (sri, (s′i, (pi, ρ(sci, σi)α)Λ, α′i) σi⟩ ===========_{⇒ (s}′′_i, Λ, α′′_i) δ((sc_{, Λ, α),⟨σ ⌊σ} 1 t1⌋ · · · ⌊σn tn⌋) = (sr, Λ′, α′) α′ = αr_n(β_nc 5 ηn)· · · αr1(β1c5 η1)αΓε ⎛ ⎝ % i∈[n] [(sc_i, sr_i, γ)(xi) := α′i(γ)]γ∈Γ ⎞ ⎠ i ∈ [n] αr_i = ρr(sri, pi, σi) βci = [γp := ρc(sci, σi)]_γ∈Γ ηi = [γ := (sc i, sri, γ)(xi)]_γ∈Γ ! . t1 = σ1 t1, . . . , tn= σn tn w1 =⌊t11⌋ · · · ⌊t1n⌋ δ((sc, Λ, α), ⟨σ ⟨σ1 w1 σ1⟩) (sc, Λ, α)=⟨σ_{⇒ (s}c₁, (p, ρc(sc, σ)α)Λ, αε) ⟨σ1 ==⇒ (s′1, (p1, ρc(s1c, σ)αε)(p, ρc(sc, σ)α)Λ, αε) w1 ==_{⇒ (s}r₁, (p1, ρc(s1c, σ)αε)(p, ρc(sc, σ)α)Λ, α1) σ1⟩ ==_{⇒ (s}c₂, (p, ρc(sc, σ)α)Λ, ρr(sr1, p1, σ1) [γp := ρc(sc1, σ1)αε]_γ∈Γα1) ρr(sr1, p1, σ1) [γp := ρc(sc1, σ1)αε]_γ∈Γα1 ρr(sr1, p1, σ1) [γp := ρc(sc1, σ1)αε]_γ∈Γα1 = ρr(sr1, p1, σ1) [γp := ρc(sc1, σ1)αε]_γ∈Γ[γ := (sr1, sr1, γ)(x1)]γ∈Γ[(sc1, sr1, γ)(x1) := α1(γ)]γ∈Γ = αr₁([γp := ρc(sc1, σ1)]_γ∈Γ5 [γ := (sc1, sr1, γ)(x1)]_γ∈Γ)αΓε [(sc1, sr1, γ)(x1) := α1(γ)]_γ∈Γ = αr₁(β₁c_{5 η}1)αεΓ[(sc1, sr1, γ)(x1) := α1(γ)]_γ∈Γ

αr₁ = ρr(sr1, p1, σ1) β1c = [γp := ρc(sc1, σ1)]_γ∈Γ η1 = [γ := (s c 1, sr1, γ)(x1)]_γ∈Γ αΓε = [γ := ε]_γ∈Γ (sc, Λ, α)=========⟨σ ⟨σ1 w1 σ1⇒ (s⟩ c2, (p, ρc(sc, σ)α)Λ, αr1(βc15 η1)αΓε [(sc1, sr1, γ)(x1) := α1(γ)]γ∈Γ) δ((sc, Λ, α),⟨σ ⌊t1⌋ · · · ⌊tn⌋) (sc, Λ, α)===⟨σ_{⇒ (s}c₁, (p, ρc(sc, σ)α)Λ, αε) ⌊t1⌋ ==_{⇒ (s}c₂, (p, ρc(sc, σ)α)Λ, αr1(β1c5 η1) [(sc1, sr1, γ)(x1) := α1(γ)]_γ∈ΓαΓε) ⌊t2⌋ ==_{⇒ · · ·} ⌊tn⌋ ===⇒ (scn, ρc(sc, σ)α)Λ, αrn(βnc 5 ηn) [(scn, srn, γ)(xn) := αn(γ)]_γ∈Γ· · · αr₁(β₁c5 η1) [(sc1, sr1, γ)(x1) := α1(γ)]_γ∈ΓαΓε) αr_n(β_nc _{5 η}n) [(snc, srn, γ)(xn) := αn(γ)]_γ∈Γ· · · αr1(β1c 5 η1) [(sc1, sr1, γ)(x1) := α1(γ)]_γ∈ΓαεΓ = αr_n(β_nc _{5 η}n)· · · αr1(β1c5 η1)αΓε [(sc₁, sr₁, γ)(x1) := α1(γ)]_γ∈Γ· · · [(scn, srn, γ)(xn) := αn(γ)]_γ∈Γ = αr_n(β_nc 5 ηn)· · · αr1(β1c5 η1)αΓε ⎛ ⎝ % i∈[n] [(sc_i, sr_i, γ)(xi) := αi(γ)]γ∈Γ ⎞ ⎠ 11. t = σ(t1, . . . , tn)∈ TΣ (sc, Λ, α)=⟨σ_{⇒ (s}′, (p, ρc(sc, σ)α)Λ, αε) ⌊t 1⌋···⌊tn⌋ ======_{⇒ (s}r, (p, ρc(sc, σ)α)Λ, α′) σ⟩ =_{⇒ (s}′′, Λ, α′′) γ _{∈ Γ !(s}c_{, s}r_{, γ)"} M(t) = α′(γ) ! . t1 = σ1 t1, . . . , tn = σn tn ∈ TΣ i∈ [n] (sc_i, Λi, αi) ⟨σ i ========_{⇒ (s}′_i, (pi, ρc(sci, σi)α)Λ, αε) ⌊ti 1⌋···⌊ti n⌋ ========_{⇒ (s}r_i, (pi, ρc(sic, σi)αi)Λi, α′i) σi⟩ ========⇒ (s′′i, Λi, α′′i) γ ∈ Γ !(sc i, sri, γ)"M(t) = α′i(γ) t = σ(t1, . . . , tn) δ((sc, Λ, α),⌊t⌋) (sc, Λ, α)=⟨σ⇒ (s′, (p, ρc(sc, σ)α)Λ, αε)======⌊t1⌋···⌊tn⇒ (s⌋ r, (p, ρc(sc, σ)α)Λ, α′) σ⟩ =⇒ (s′′, Λ, α′′)

10 α′ = αr_n(β_nc _{5 η}n)· · · αr1(β1c5 η1)αΓε ⎛ ⎝ % i∈[n] [(sc_i, sr_i, γ)(xi) := α′i(γ)]γ∈Γ ⎞ ⎠ α′ = αr_n(β_nc _{5 η}n)· · · αr1(β1c5 η1)αΓε ⎛ ⎝% i∈[n] [(sc_i, sr_i, γ)(xi) :=!(sic, sri, γ)"M(ti)]_γ∈Γ ⎞ ⎠ 8 t1 ∈ L((sc1, σ1, sr1)), . . . , tn∈ L((scn, σn, srn)) γ ∈ Γ α′(γ) = rhs((sc, sr, γ), σ, π1, . . . , πn) ⎛ ⎝ % i∈[n] [(sc_i, sr_i, γ)(xi) :=!(sic, sri, γ)"M(ti)]γ∈Γ ⎞ ⎠ π1 = (sc1, σ1, sr1), . . . , πn = (scn, σn, srn) 4 α′(γ) =_!rhs((sc, sr, γ), σ, π1, . . . , πn)"M(t1, . . . , tn) =_!(sc, sr, γ)_"M(σ(t1, . . . , tn)) =!(sc, sr, γ)"M(t) 12. w ∈ Dom(T ) !T " (w) = !M" (⌈w⌉) ! . t =⌈w⌉ t = σ(t1, . . . , tn) (s0, ε, αε)=⟨σ⇒ (s′, (p, αε)Λ, αε)======⌊t1⌋···⌊tn⇒ (s⌋ r0, (p, αε)Λ, α′) σ⟩ =⇒ (s′′, ε, α′′)

w_{∈ Dom(T )} s′′ _{∈ Dom(F ) 9 t ∈ Dom(M)}

!T " (w) !T " (w) = F (s′′)α′′ = F (s′′)ρr(sr0, p, σ) [γp := γρc(s0, σ)αε]_γ∈Γα′ = F (s′′)ρr(sr0, p, σ) [γp := γρc(s0, σ)αε]_γ∈Γ[γ := (s0, sr0, γ)(x1)]_γ∈Γ[(s0, sr0, γ) := α′(γ)]γ∈Γ = F (s′′)ρr(sr0, p, σ)([γp := ρc(s0, σ)(γ)]_γ∈Γ5 η(sr0, σ))αΓε [(s0, sr0, γ) := α′(γ)]γ∈Γ = F (s′′)αr(sr₀, p, σ)(βc(σ)_{5 η(s}r₀, σ))αΓ_ε [(s0, sr0, γ)(x1) := α′(γ)]_γ∈Γ αr _βc _{η α}Γ ε αr(sr0, p, σ) = ρr(sr0, p, σ) βc(σ) = [γp := ρc(s0, σ)(γ)]_γ∈Γ η(sr₀, σ) = [γ := (s0, sr0, γ)(x1)]γ∈Γ αΓε = [γ := ε]γ∈Γ !T " (w) = F (s′′)αr(sr₀, p, σ)(β(σ)_{5 η(s}r₀, σ))αΓ_ε [(s0, sr0, γ)(x1) := α′(γ)]_γ∈Γ

11 !T " (w) = F (s′′)αr(sr₀, p, σ)(β(σ)5 η(sr 0, σ))αΓε [(s0, sr0, γ)(x1) :=!(s0, sr0, γ)"M(t)]γ∈Γ !M" (t) 4 !M" (t) = !Init(π)"M(t) ='F (s′′)αr(sr₀, p, σ)(β(σ)_{5 η(s}r₀, σ))αΓ_ε(_M(t) = F (s′′)αr(sr₀, p, σ)(β(σ)5 η(sr0, σ))αΓε [(s0, sr0, γ)(x1) :=!(s0, sr0, γ)"M(t)]γ∈Γ !T " (⌊t⌋) = !M" (t)

5.5

5.1 yDTR _{SRTST 5.3 SRTST} yDTR _{1 7} 1. SRTST yDTR _! 7 SRTST yDTR _yDTR [22] 2. SRTST ! 7 1 3. SRTST T SRTST T′ ! . 7 T yDTR _{M 1 M} SRTST T′ 1. SRTST SRTST !

6

Alur D’Antoni SRTST

(streaming tree-to-string transducer with single-use-restriction SRTSTsur)

SRTST yDTR

6.1

4 SRTST [2] ( ) SRTST (STTsur) E(Γ, ∆) (conflict relation) η X γ γ′ 8. Γ η ∆ e _{∈ E(Γ, ∆)} e η 1. e γ 2. η(γ, γ′) e γ γ′ ! 9. Γ Γ′ η ∆ ρ 1. ρ(γ) η 2. η(γ1, γ2) ρ(γ1) γ1′ ρ(γ2) γ2′ η(γ1′, γ2′) ! Γ Γ′ η ∆ _{A(Γ, Γ}′, η, ∆) 10. (deterministic

streaming ranked-tree-to-string transducer with single-use-restriction SRTSTsur)

• S Σ ∆ P s0 Γ F δc δr SRTST

• F : S → E(Γ, ∆) F (q) η

• ρc : Q× Σ → A(Γ, Γ, η, ∆)

• ρr : Q× P × Σ → A(Γ, Γ ∪ Γp, η, ∆) !

SRTSTsur SRTST

(monadic second order definable tree-to-string transducer MSOTST) [2] MSOTST

(deterministic finite copying top-down tree-to-string transducer yDT_fc) [10]

6.2

2010 (copyless streaming string transducer SSTcl) [4]

Alur Cern´ˇ y δ : S_{× Σ → A(Γ, Γ, ∆)}

s ∈ S σ ∈ Σ γ ∈ Γ {δ(s, σ)(γ′_{) | γ}′ _{∈ Γ}}

γ

SSTcl

(monadic second order logic definable string transducer, MSOST)

[1] MSOST SSTcl

[11] (copyful streaming string transducer SST)

HDT0L (deterministic 0-context lindenmayer systems with tables and with an

additional homomorphism) [14] HDT0L

[8, 21, 17] SST

(deterministic nested word to word transducer dN2W) [23] dN2W SRTST dN2W

[23]

yDT (sequential yDT

yDT) yDT xi

x1, . . . , xn yDT yDT dN2W

yDT_{seq dN2W} yDTR_seq

yDT_fc

yDTR_fc MSOTST SRTSTsur

yDT yDTR _SRTST [23] [10] [2] 6.1 SSTcl MSOST SST HDT0L STTsur MSOTST STT [1] [14] [2] 6.2 ( )

(linear yDT yDT) yDT xi yDT yDT dN2W [6] yDT [5] yDT Seidl [22] yDT

(determinisitc tree-to-word macro transducer yDMT)

6.1 6.2

yDTR SRTST

(deterministic macro tree

transdcuer MTT) [13] MTTR MSOTT

[10] STTsur MTT

[18]

(macro forest

trans-ducer ) [19]

7

(SRTST) (yDTR₎ SRTST SRTST SRTST ( ) STT STT

(deterministic streaming ranked-tree transducer SRTT)

yDTR SRTST yDTR_fc SRTST

SRTST yDTR_fc

SRTSTsur SRTST STT

[1] Rajeev Alur and Pavol ˇCern´y. Expressiveness of streaming string transducers. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1–12. Schloss Dagstuhl–Leibniz-Zentrum f¨ur Informatik, 2010.

[2] Rajeev Alur and Loris D’Antoni. Streaming tree transducers. J. ACM, 64(5):31:1– 31:55, August 2017.

[3] Rajeev Alur and P. Madhusudan. Visibly pushdown languages. In Proceedings of the Thirty-sixth Annual ACM Symposium on Theory of Computing, STOC ’04, pages 202– 211. ACM, 2004.

[4] Rajeev Alur and Pavol ˇCern´y. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’11, pages 599–610. ACM, 2011.

[5] Adrien Boiret. Normal form on linear tree-to-word transducers. In Language and Automata Theory and Applications, pages 439–451. Springer International Publishing, 2016.

[6] Adrien Boiret and Raphaela Palenta. Deciding equivalence of linear tree-to-word trans-ducers in polynomial time. In Developments in Language Theory, pages 355–367. Springer Berlin Heidelberg, 2016.

[7] H. Comon, M. Dauchet, R. Gilleron, C. L¨oding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications, 2007.

[8] K. Culik and J. Karhum¨aki. A New Proof for the D0L Sequence Equivalence Problem and its Implications, pages 63–74. Springer Berlin Heidelberg, 1986.

[9] Joost Engelfriet. Top-down tree transducers with regular look-ahead. Mathematical systems theory, 10(1):289–303, Dec 1976.

[10] Joost Engelfriet and Sebastian Maneth. Macro tree transducers, attribute grammars, and MSO definable tree translations. Information and Computation, 154(1):34 – 91, 1999.

[11] Joost Engelfriet and Sebastian Maneth. The equivalence problem for deterministic mso tree transducers is decidable. Information Processing Letters, 100(5):206 – 212, 2006. [12] Joost Engelfriet, Sebastian Maneth, and Helmut Seidl. How to remove the look-ahead

of top-down tree transducers. In Arseny M. Shur and Mikhail V. Volkov, editors, Developments in Language Theory, pages 103–115. Springer International Publishing, 2014.

[13] Joost Engelfriet and Heiko Vogler. Macro tree transducers. Journal of Computer and System Sciences, 31(1):71 – 146, 1985.

[14] Emmanuel Filiot and Pierre-Alain Reynier. Copyful streaming string transducers. In Reachability Problems, pages 75–86. Springer International Publishing, 2017.

[15] Zoltan Fulop and H. Vogler. Syntax-Directed Semantics: Formal Models Based on Tree Transducers. Springer-Verlag, 1st edition, 1998.

[16] Zolt´an F¨ul¨op and Heiko Vogler. Attributed Tree Transducers, pages 137–171. Springer Berlin Heidelberg, 1998.

[17] Juha Honkala. A short solution for the HDT0L sequence equivalence problem. Theo-retical Computer Science, 244(1):267 – 270, 2000.

[18] Sebastian Maneth. A survey on decidable equivalence problems for tree transducers. International Journal of Foundations of Computer Science, 26(08):1069–1100, 2015. [19] Keisuke Nakano and Shin-Cheng Mu. A pushdown machine for recursive XML

pro-cessing. In Programming Languages and Systems, pages 340–356. Springer Berlin Hei-delberg, 2006.

[20] Thomas Perst and Helmut Seidl. Macro forest transducers. Information Processing Letters, 89(3):141 – 149, 2004.

[21] Keijo Ruohonen. Equivalence Problems for Regular sets of Word Morphisms, pages 393–401. Springer Berlin Heidelberg, 1986.

[22] Helmut Seidl, Sebastian Maneth, and Gregor Kemper. Equivalence of deterministic top-down tree-to-string transducers is decidable. J. ACM, 65(4):21:1–21:30, April 2018. [23] S(lawomir Staworko, Gr´egoire Laurence, Aur´elien Lemay, and Joachim Niehren.

Equiv-alence of deterministic nested word to word transducers. In Fundamentals of Compu-tation Theory, pages 310–322. Springer Berlin Heidelberg, 2009.

[24] James W. Thatcher. Generalized2 _{sequential machine maps. Journal of Computer and}