Title

Oct 15, 2008 @ Tohoku Univ.
Macro Tree Transducers
and
Their Complexity
Kazuhiro Inaba
The University of Tokyo
[email protected]
Oct 15, 2008 @ Tohoku Univ.
Macro Tree Transducer
(MTT) とは?
 TreeからTreeへの変換の形式化(の一種)
例
(cons list  snoc list):
SNOC
CONS
B
A
CONS
A
A
SNOC
CONS
NIL
SNOC
NIL
A
B
をMTTで書くと…
2
Oct 15, 2008 @ Tohoku Univ.
MTT とは?
 TreeからTreeへの変換の形式化(の一種)
例
(cons list  snoc list):
f( CONS(x, y) )
f( NIL )


g(y, SNOC(NIL,c(x)))
NIL
g( CONS(x, y), z )
g( NIL,
z )


g(y, SNOC(z, c(x)))
z
c( A )
c( B )


A
B
3
Oct 15, 2008 @ Tohoku Univ.
MTT とは!
制約された一階の関数型言語
 扱うデータ型は
Ranked Tree のみ
 Ranked
Tree =
ラベルから子要素の数が一意に決まるTree
 より正確には、入力木型(TI)と出力木型(TO)
の2種類のTreeのみ
 それぞれの関数の型は、ある n≧0 について
TI * TOn  TO
4
Oct 15, 2008 @ Tohoku Univ.
MTT とは!
制約された一階の関数型言語

それぞれの関数の型は、ある n≧0 について
TI * TOn  TO
 常に、第一引数(入力木)に関して帰納的定義
g( CONS(x, y), z )
g( NIL,
z )


…
…
 第二引数以降は、バラして使うことはできない
(そのまま出力することのみが可能)
5
Oct 15, 2008 @ Tohoku Univ.
≪関数の型≫
TI = Trees over {CONS, NIL, A, B}
TO = Trees over {SNOC, NIL, A, B}
f :: TI  TO
g :: TI * TO  TO ≪常に入力木(第一引数)に
関して帰納的定義≫
c :: TI  TO
f( CONS(x, y) )
f( NIL )


g(y, SNOC(NIL,c(x)))
NIL
g( CONS(x, y), z )
g( NIL,
z )


g(y, SNOC(z, c(x)))
z
c( A )
c( B )


A
B
≪第二引数以降はその
まま出力するだけ≫
6
Oct 15, 2008 @ Tohoku Univ.
これらの制約によって
得られる物は?

種々の性質が決定可能
 停止性
(自明)
 Domain や Range のメンバシップ判定
 Domain や Range の有限性
 “Exact” Type Checking
 変換によるサイズ増加の線形性
 などなど

つまり、MTTで書かれたプログラムなら
これらの性質を機械的に静的検証可能
 XML変換言語の検証のためのモデル
7
Oct 15, 2008 @ Tohoku Univ.
MTTとは?(逆からの眺め)
 有限状態モデルの拡張の歴史…
8
Oct 15, 2008 @ Tohoku Univ.
MTTとは?(逆からの眺め)
「パラメタ」
オートマトン
(= 正規文法)
文脈自由文法
マクロ文法
「文字列→木」
「出力付き」
木オートマトン
(= 正規木文法)
文脈自由木文法
ツリー
トランスデューサ
マクロ ツリー
トランスデューサ
トランスデューサ
9
Oct 15, 2008 @ Tohoku Univ.
これらの拡張によって
得られる物は?

他に知られている木変換モデルを包含する表現力
 Attributed Tree Transducer (Attribute Grammar)
 Pebble Tree Transducer
 Higher-order Macro Tree Transducer
 MSO Tree Translation
…

現実のXML処理言語(XSLT, XQuery, XML-QL,
…) などの「木構造変換部分」を表現できる表現力
[Milo/Suciu/Vianu 00]
10
Oct 15, 2008 @ Tohoku Univ.
Today’s Talk
 MTTの形式的定義
 非決定性
 IO
 MTT
と OI
1個の“Translation Membership” の計算量
 Compressed
 MTT
Representation
の任意有限個の合成の計算量
 Garbage-Free
Form
11
Oct 15, 2008 @ Tohoku Univ.
MTTの形式的定義
 MTT
= (Q, q0, Σ,Δ, R) where
Q
: Rankつき状態集合(関数の集合)
 q0 : 初期状態(main関数)
 Σ : 入力木のRankつきラベル集合
 Δ : 出力木のRankつきラベル集合
 R : 以下の形の変換規則(関数定義)の集合


q(σ(x1, …, xm), y1, … yk )  rhs
rhs ::= yi | δ(rhs, …, rhs) | q(xi, rhs, ..., rhs)
12
Oct 15, 2008 @ Tohoku Univ.
例

Q = {f(1), g(2), c(1)}, q0 = f,
Σ={CONS(2),NIL(0),A(0),B(0)},
Δ={SNOC(2),NIL(0),A(0),B(0)}, R=
f( CONS(x, y) )
f( NIL )


g(y, SNOC(NIL,c(x)))
NIL
g( CONS(x, y), z )
g( NIL, z )


g(y, SNOC(z, c(x)))
z
c( A )
c( B )


A
B
13
Oct 15, 2008 @ Tohoku Univ.
注意! 非決定性 MTT
 例:
S(S(S(…S(Z)…)  A/Bの完全二分木
A
S
or
A
Z
S
A
Z
Z
Z
or
Z
Z
Z
Z
Z
Z
Z
Z
Z
A
Z
Z
B
A
Z
A
or
A
Z
B
B
B
Z
B
or
B
Z
Z
A
or
A
A
Z
A
Z
B
Z
Z
Z
or… (2 more)
14
Oct 15, 2008 @ Tohoku Univ.
注意! 非決定性 MTT
 例:
S(S(S(…S(Z)…)  A/Bの完全二分木
f( S(x) )
f( Z )


g(x, h(x, Z))
Z
g( S(x), y )
g( Z,
y )


g(x, h(x, y))
y
h(
h(
h(
h(




A(y,
B(y,
A(y,
B(y,
S(x),
S(x),
Z,
Z,
y
y
y
y
)
)
)
)
y)
y)
y)
y)
15
Oct 15, 2008 @ Tohoku Univ.
なぜ非決定性が必要?
 MTTの表現力を超える制御フローの近似
<xsl:template name=“h”>
<xsl:choose>
<xsl:when test=“COMPLEX-TEST-EXPRESSION”>
<A> … </A>
</xsl:when>
<xsl:otherwise>
<B> … </B>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
16
Oct 15, 2008 @ Tohoku Univ.
2つの非決定性評価戦略:
IO と OI
 IO
= Inside-Out ≒ Call-by-Value
 ネストした関数適用は「内側から」先に評価
 OI
= Outside-In ≒ Call-by-Name
 ネストした関数適用は「外側から」先に評価
17
Oct 15, 2008 @ Tohoku Univ.
IO と OI

h( Z, y ) 
h( Z, y ) 
IOなら?
h(Z,h(Z,Z)) = h(Z, A(Z,Z)) =
|
| h(Z, B(Z,Z)) =
|

A(y, y)
B(y, y)
A(A(Z,Z),
B(A(Z,Z),
A(B(Z,Z),
B(B(Z,Z),
A(Z,Z))
A(Z,Z))
B(Z,Z))
B(Z,Z))
OIなら?
h(Z,h(Z,Z)) = A(h(Z,Z), h(Z,Z))
= A(A(Z,Z), A(Z,Z))
| A(A(Z,Z), B(Z,Z))
| A(B(Z,Z), A(Z,Z))
| A(B(Z,Z), B(Z,Z))
| B(h(Z,Z), h(Z,Z)) = …|…|…|…
18
Oct 15, 2008 @ Tohoku Univ.
MTT-IO vs MTT-OI

表現力の比較
 MTT-IO
 MTT-IO

⊄ MTT-OI & MTT-OI ⊄ MTT-IO
⊂ MTT-OI2 & MTT-OI ⊂ MTT-IO2
モデルとしての扱いやすさ
 OI
の方が扱いやすい場面が多い
(MTT同士の合成が計算しやすいなどなど)

現実のプログラムの近似モデルとして
 IO

の方がより適切な場面が多い
計算量の比較
 IOの方が低コストなことが多い
19
Oct 15, 2008 @ Tohoku Univ.
ここからの話
 K.
Inaba and S.Maneth, “The
Complexity of Tree Transducer
Output Languages”, To appear in
FSTTCS 2008
http://www.kmonos.net/pub/files/mttout_full.pdf
 MTT(の合成)で表現される変換の
出力木言語 range(MTTk) のメンバ判定
… を中心に。
20
Oct 15, 2008 @ Tohoku Univ.
“Translation Membership” 問題
 変換
τ の変換メンバシップ問題とは
 入力:
二つの木
 出力: 真偽値
a, b
b ∈τ(a)
 この判定に必要な計算量は?
21
Oct 15, 2008 @ Tohoku Univ.
Translation Membership of
Deterministic Total MTT
 O(
|a| + |b| ) time
 τ(a)
を「注意深く」計算しながら b と比較
22
Oct 15, 2008 @ Tohoku Univ.
Translation Membership of
MTT-IO
 O(
|a|・|b|2k+2 ) time
 where
 “Inverse
 τ-1(b)
k = 最大パラメータ数
Type Inference” の応用
はツリーオートマトンで表現できる
∈ τ-1(b) ?” は O(|a|×遷移関数の1回の実
行時間 ) で判定可能
 “a
23
Oct 15, 2008 @ Tohoku Univ.
Translation Membership of
MTT-OI
 |a|+|b|に関して
 NP-complete
 DSPACE(n)
24
Oct 15, 2008 @ Tohoku Univ.
Trn. Mem. of MTT-OI
≪NP-hardness≫
 SAT
からの変換
 入力木
「b(b(…b(c(…c(z)…)…)」に対して、
変数 #b 種類、節数 #c 個の充足可能な
CNF命題論理式を非決定的に出力する
(そして、そのような論理式を全て出力しうる)
MTT-OI が存在する
25
Oct 15, 2008 @ Tohoku Univ.
Trn. Mem. of MTT-OI
≪NP-hardness≫
 これです→
26
Oct 15, 2008 @ Tohoku Univ.
Trn. Mem. of MTT-OI
≪NP & DSPACE(n)≫
 直接示すのは難しい
 計算ステップ数は指数オーダになりうる
f( S(x), y )
f( Z,
y )
 まず、MTT-OI
 Path-linear
 f(x, f(x, y))
 y
の subclass について示す
MTT
 “同じ子供に対する関数適用はネストしない”
MTT
27
Oct 15, 2008 @ Tohoku Univ.
Path-linear MTT?
 Path-linear
MTT
 “同じ子供に対する関数適用はネストしない”
 Tree
Transducer (=パラメタ無しMTT) を含む
 Linear MTT (= 同じ子供に対する関数適用は存在
しない)を含む
 Old
Known Result:
 MTT-OI
⊂ TT ∘ LinMTT ∘ TT
28
Oct 15, 2008 @ Tohoku Univ.
Trn. Mem. of Path-lin MTT-OI
≪NP & DSPACE(n)≫ : Proof
τ を、”+” という特殊なノード
を出力する決定性MTT τd へと変換する
 非決定性MTT
)
)
)
)




A(y,
B(y,
A(y,
B(y,
h( S(x), y )
h( Z,
y )


+(A(y,y), B(y,y))
+(A(y,y), B(y,y))
h(
h(
h(
h(
S(x),
S(x),
Z,
Z,
y
y
y
y
y)
y)
y)
y)
29
Oct 15, 2008 @ Tohoku Univ.
+
S
A
S
+
Z
B
Z
+
+
A
Z
B
Z
A
Z
Z
A
B
Z
Z
+
Z
Z
B
Z
Z
A
Z
Z
B
Z
Z
Z
30
Oct 15, 2008 @ Tohoku Univ.
Trn. Mem. of Path-lin MTT-OI
≪NP & DSPACE(n)≫ : Proof
∈ τ(a)」
if and only if
「τd(a) のそれぞれの “+” ノードを左右ど
ちらかの子でうまく置き換えると b になる」
 「b
τd(a) と b を top-down に再帰的に比較
するだけで判定できる GOOD
|τd(a)| >>>> |a|+|b| かもしれない
τd(a) をマジメに計算はできない BAD
31
Oct 15, 2008 @ Tohoku Univ.
τd(a) と b の比較アルゴリズム
let rec comp(pt, t) =
match (pt, t) with
| (+(pt1, pt2), t) ->
comp(pt1, t) || comp(pt2, t)
| (σ(pt1,pt2,…ptn), σ(t1,t2,…tn) ) ->
comp(pt1,t1) && … && comp(ptn,tn)
| _ ->
false

非決定性計算での時間計算量


height(τd(a)) ・|b|・基本演算の時間
※Path-linearならheight=O(|a|)
決定性計算での空間計算量


max( height(τd(a))), height(b) ) ・ ptとtのノード表現のサイズ
※ pt と t のノード表現から親ノードの表現を計算できれば↑は不要
32
Oct 15, 2008 @ Tohoku Univ.
Trn. Mem. of Path-lin MTT-OI
≪NP & DSPACE(n)≫ : Proof
 τd(a)
の圧縮表現
 τd(a)
の各ノードは、そのノードを生成した瞬
間のτd の「コールスタック」で表現できる
f(
f(
g(
g(
h(
h(
S(x) )
Z )
S(x), y
Z,
y
S(x), y
Z,
y
)
)
)
)






g(x, h(x,
Z
g(x, h(x,
y
+(A(y,y),
+(A(y,y),
+
Z))
y))
B(y,y))
B(y,y))
A
B
<<g>>(x, h(x, Z))
g(x, <<h>>(x, y))
+(<<A>>(y,y), B(y,y))
33
Oct 15, 2008 @ Tohoku Univ.
≦ |a| なので、
τd(a) を O(|a|)サイズに圧縮できた!
 「コールスタック」の高さ
 問題点:

「コールスタック」で表現されたノードの
子ノードや親ノードを得ることは可能か?
その計算量は?
34
Oct 15, 2008 @ Tohoku Univ.

文脈自由木言語によるXML圧縮[BLM08]
 子ノードを得ることは可能
 「色々な条件を満たしていれば」線形時間で可能
linear ならば」
親ノードを得ることが(線形時間で)可能
 「パラメタ変数の使われ方が

[Inaba/Maneth08]
 Path-linear
ならば線形時間で子ノードを計算可能
 Path-linear ならば「コールスタックツリー表現」を使う
ことで、線形時間で親ノードを計算可能
35
Oct 15, 2008 @ Tohoku Univ.

「コールスタックツリー表現」
 基本アイデア
 子ノードを計算できるノード表現χがあれば、
「祖先ノード全部をχで表現したリスト」
で各ノードを表すことにすれば、
子ノードも親ノードも計算もできるようになる
 問題点: サイズがO(|a|)ではなくなる
 追加アイデア
 ノード v のコールスタック表現と、vの子ノードのコールスタッ
ク表現は、「よく似ている」
 『「祖先ノード全部をχで表現したリスト」を共通部分はできる
だけまとめた trie 構造』でノードを表現すればいい
 Path-linear なら O(|a|) サイズになる
36
Oct 15, 2008 @ Tohoku Univ.
おさらい
 Path-linear
MTT の変換メンバシップ判定
は NP かつ DSPACE(n)
 出力木のノードの「コールスタック表現」
 さらに
「コールスタックツリー表現」
37
Oct 15, 2008 @ Tohoku Univ.
Translation Membership of
MTT∘MTT ∘・・・∘MTT
τ = τ1 ;τ2 ; … ;τk とする
(各 τi は path-linear MTT)
 変換を
 基本的なアプローチ
 変換の途中結果
a1∈τ1(a), a2 ∈ τ2(a1), …, b ∈ τk(ak-1)
をすべて推測して、各τiのTrn. Mem.判定に帰
着
38
Oct 15, 2008 @ Tohoku Univ.
Translation Membership of
MTT∘MTT ∘・・・∘MTT
 基本的アプローチを真っ向から実行すると
 Old
b


Known Result:
∈ τ(a) ならば |b|≦ 2^2^|a|
a1∈τ1(a), a2 ∈ τ2(a1), …, b ∈ τk(ak-1) を満たす
ai は、あるとすれば |ai|≦2^2^2^2^2^2^2^…^|a|
探索範囲は有限!
2i
39
Oct 15, 2008 @ Tohoku Univ.
Translation Membership of
MTT∘MTT ∘・・・∘MTT
 基本的アプローチを真っ向から実行する
ことの問題点
 変換の途中結果が大きすぎる
b が実際に大きい場合は、
それでも(計算量的には)問題ない
|a| <<< |ai| >>> |b| なケースが問題

↑こういうケースを除きたい
 最終出力
40
Oct 15, 2008 @ Tohoku Univ.
Theorem
≪Garbage Free Form≫
MTT合成列
τ=
τ1 ; τ2 ; … ; τk
に対し、等価な合成列
τ = γ0 ; γ1 ; γ2 ; … ; γk
で、任意の b∈τ(a) に対し
 任意のPath-linear
a0∈γ0(a),…, ai=γi(ai-1),..., b=ak=γk(ak-1)
|ai-1|/2 < |ai| for all i
を満たす中間結果列 a0,…,ak を
とれるものを構成できる
41
Oct 15, 2008 @ Tohoku Univ.
Garbage Free Form の帰結 (1)

Translation Membership of
MTT∘MTT ∘・・・∘MTT is
 NP-complete
 DSPACE(n)

Proof.
Garbage Free Form に変換してから
「基本的アプローチ」: 変換の途中結果
a0∈γ0(a), a1 ∈ γ1(a0), …, b =ak∈ γk(ak-1)
をすべて推測して、各γiのTrn. Mem.判定に帰着 □
42
Oct 15, 2008 @ Tohoku Univ.
Garbage Free Form の帰結 (2)

range(MTT∘MTT ∘・・・∘MTT) is
 NP-complete
 DSPACE(n)
 i.e., MTTのrangeは文脈依存言語

Proof.
実はGFFの最初の変換γ0のrangeは、正規木言語であ
ることが示せる。変換の途中結果
a0∈γ0(???), a1 ∈ γ1(a0), …, b =ak∈ γk(ak-1)
をすべて推測して、各γiのTrn. Mem.判定 および
range(γ0)のMem判定に帰着 □
43
Oct 15, 2008 @ Tohoku Univ.
Garbage Free Form の帰結 (3)
 range(MTT∘MTT
∘・・・∘MTT) の有限性は
決定可能
 Proof.
GFFなら、range(τ)が有限 iff range(γ0)が有限。
実はGFFの最初の変換γ0のrangeは、正規木言語
であることが示せる。
正規木言語の有限性は決定可能 □
44
Oct 15, 2008 @ Tohoku Univ.
Proof Sketch of
GFF Theorem (1/3)
 最後のMTTを「サイズを減らさない」ものに
変形
…
;τk-1 ; τk
 … ;τ’k-1 ; γk
の繰り返し
(正確には、最後から2番目のMTTを、「最後
のMTTが使わない部分木は生成しない」も
のに変形、の方が近い?)
45
Oct 15, 2008 @ Tohoku Univ.
Proof Sketch of
GFF Theorem (2/3)

サイズを減らす関数3種類
 “Input-deletion”
 そもそも入力の一部分を完全無視

f(σ(x1,…,xm), y1, …, yk )  ∃I : xi が1度も現れない
 “Erasure”
 Leaf

で引数をそのまま出力
f( σ, y1, …, yk )  yi
 “Skipping”


子供が1つのノードで、ただ別の関数を呼ぶだけ
f(σ(x), y1, …, yk )  g(x, y1, …, yk )
46
Oct 15, 2008 @ Tohoku Univ.
Proof Sketch of
GFF Theorem (3/3)
 τk-1
; τk
Erasure, Input-Deletion,
Skipping が起きそうな箇所を
予測して、先に削除しておく
ツリートランスデューサ
 τk-1 ; (E ; I ; S ;γk )
(結合則)
 (τk-1 ; E ; I ; S) ;γk
(MTT-OI はE,I,Sの後ろからの合成に
関して閉じている)
 τ’k-1 ;γk
47
Oct 15, 2008 @ Tohoku Univ.
補足: Combined Complexity
of Translation Membership

DtMTT:
 O(

MTT-IO:
 O(

|M|・|a|・|b|2k+2 )
Path linear MTT-OI:
 O(

|M|・(|a|+|b|) )
|M|・poly(|a|+|b|) )
※ Nondet.
MTT ∘MTT ∘… ∘MTT:

O( 2^2^2^2^…^|M| ・ poly(|a|+|b|) ) ※Nondet.
48
Oct 15, 2008 @ Tohoku Univ.
まとめ

Macro Tree Transducer




“Translation Membership”



制限された関数型言語
オートマトン+ツリー+出力+パラメタ
非決定性。IO / OI
圧縮表現
Garbage Free Form
文献


J. Engelfriet and H. Vogler, “Macro Tree Transducers”,
JCSS(31) 71-146, 1985
K. Inaba and S. Maneth, “The Complexity of Tree
Transducer Output Languages”, To appear in FSTTCS 2008
49