Macro Tree Transducers and Their Complexity

Presentation on theme: "Macro Tree Transducers and Their Complexity"— Presentation transcript:

1 Macro Tree Transducers and Their Complexity
Kazuhiro Inaba The University of Tokyo

2 Macro Tree Transducer (MTT) とは？
TreeからTreeへの変換の形式化（の一種） 例 (cons list  snoc list)： SNOC CONS SNOC A B CONS SNOC A A CONS A NIL NIL B をMTTで書くと…

3 MTT とは？ TreeからTreeへの変換の形式化（の一種） 例 (cons list  snoc list)：
f( CONS(x, y) )  g(y, SNOC(NIL,c(x))) f( NIL )  NIL g( CONS(x, y), z )  g(y, SNOC(z, c(x))) g( NIL, z )  z c( A )  A c( B )  B

4 MTT とは！ 制約された一階の関数型言語 扱うデータ型は Ranked Tree のみ
Ranked Tree = ラベルから子要素の数が一意に決まるTree より正確には、入力木型(TI)と出力木型(TO)の２種類のTreeのみ それぞれの関数の型は、ある n≧0 について TI * TOn  TO

5 MTT とは！ 制約された一階の関数型言語 それぞれの関数の型は、ある n≧0 について TI * TOn  TO
常に、第一引数（入力木）に関して帰納的定義 第二引数以降は、バラして使うことはできない （そのまま出力することのみが可能） g( CONS(x, y), z )  … g( NIL, z )  …

6 ≪関数の型≫ 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) )  g(y, SNOC(NIL,c(x))) f( NIL )  NIL g( CONS(x, y), z )  g(y, SNOC(z, c(x))) g( NIL, z )  z c( A )  A c( B )  B ≪第二引数以降はその 　まま出力するだけ≫

7 これらの制約によって 得られる物は？ 種々の性質が決定可能 つまり、MTTで書かれたプログラムなら これらの性質を機械的に静的検証可能
停止性 （自明） Domain や Range のメンバシップ判定 Domain や Range の有限性 “Exact” Type Checking 変換によるサイズ増加の線形性 などなど つまり、MTTで書かれたプログラムなら これらの性質を機械的に静的検証可能 XML変換言語の検証のためのモデル

8 MTTとは？（逆からの眺め） 有限状態モデルの拡張の歴史…

9 MTTとは？（逆からの眺め） 「パラメタ」 オートマトン （= 正規文法） 文脈自由文法 マクロ文法 「文字列→木」 「出力付き」
木オートマトン （= 正規木文法） 文脈自由木文法 トランスデューサ ツリー トランスデューサ マクロ ツリー トランスデューサ

10 これらの拡張によって 得られる物は？ 他に知られている木変換モデルを包含する表現力
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]

11 Today’s Talk MTTの形式的定義 非決定性 MTT 1個の“Translation Membership” の計算量
IO と OI MTT 1個の“Translation Membership” の計算量 Compressed Representation MTT の任意有限個の合成の計算量 Garbage-Free Form

12 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)

13 例 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) )  g(y, SNOC(NIL,c(x))) f( NIL )  NIL g( CONS(x, y), z )  g(y, SNOC(z, c(x))) g( NIL, z )  z c( A )  A c( B )  B

14 注意！ 非決定性 MTT 例: S(S(S(…S(Z)…)  A/Bの完全二分木 or or or or or or… (2 more)

15 注意！ 非決定性 MTT 例: S(S(S(…S(Z)…)  A/Bの完全二分木 f( S(x) )  g(x, h(x, Z))
f( Z )  Z g( S(x), y )  g(x, h(x, y)) g( Z, y )  y h( S(x), y )  A(y, y) h( S(x), y )  B(y, y) h( Z, y )  A(y, y) h( Z, y )  B(y, y)

16 なぜ非決定性が必要？ 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>

17 2つの非決定性評価戦略: IO と OI IO = Inside-Out ≒ Call-by-Value
ネストした関数適用は「内側から」先に評価 OI = Outside-In ≒ Call-by-Name ネストした関数適用は「外側から」先に評価

18 IO と OI IOなら？ OIなら？ h( Z, y )  A(y, y) h( Z, y )  B(y, y)
h(Z,h(Z,Z)) = h(Z, A(Z,Z)) = A(A(Z,Z), A(Z,Z)) | B(A(Z,Z), A(Z,Z)) | h(Z, B(Z,Z)) = A(B(Z,Z), B(Z,Z)) | B(B(Z,Z), B(Z,Z)) 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)) = …|…|…|…

19 MTT-IO vs MTT-OI 表現力の比較 モデルとしての扱いやすさ 現実のプログラムの近似モデルとして 計算量の比較
MTT-IO ⊄ MTT-OI & MTT-OI ⊄ MTT-IO MTT-IO ⊂ MTT-OI2 & MTT-OI ⊂ MTT-IO2 モデルとしての扱いやすさ OI の方が扱いやすい場面が多い （MTT同士の合成が計算しやすいなどなど） 現実のプログラムの近似モデルとして IO の方がより適切な場面が多い 計算量の比較 IOの方が低コストなことが多い

20 ここからの話 K. Inaba and S.Maneth, “The Complexity of Tree Transducer Output Languages”, To appear in FSTTCS MTT(の合成)で表現される変換の 出力木言語 range(MTTk) のメンバ判定 … を中心に。

21 “Translation Membership” 問題
変換 τ の変換メンバシップ問題とは 入力: 二つの木 a, b 出力: 真偽値 b ∈τ(a) この判定に必要な計算量は？

22 Translation Membership of Deterministic Total MTT
O( |a| + |b| ) time τ(a) を「注意深く」計算しながら b と比較

23 Translation Membership of MTT-IO
O( |a|・|b|2k+2 ) time where k = 最大パラメータ数 “Inverse Type Inference” の応用 τ-1(b) はツリーオートマトンで表現できる “a ∈ τ-1(b) ？” は O(|a|×遷移関数の1回の実行時間 ) で判定可能

24 Translation Membership of MTT-OI
|a|+|b|に関して NP-complete DSPACE(n)

25 Trn. Mem. of MTT-OI ≪NP-hardness≫
SAT からの変換 入力木 「b(b(…b(c(…c(z)…)…)」に対して、 変数 #b 種類、節数 #c 個の充足可能なCNF命題論理式を非決定的に出力する （そして、そのような論理式を全て出力しうる） MTT-OI が存在する

26 Trn. Mem. of MTT-OI ≪NP-hardness≫
これです→

27 Trn. Mem. of MTT-OI ≪NP & DSPACE(n)≫
直接示すのは難しい 計算ステップ数は指数オーダになりうる まず、MTT-OI の subclass について示す Path-linear MTT “同じ子供に対する関数適用はネストしない” MTT f( S(x), y )  f(x, f(x, y)) f( Z, y )  y

28 Path-linear MTT？ Path-linear MTT “同じ子供に対する関数適用はネストしない”
Tree Transducer (=パラメタ無しMTT) を含む Linear MTT (= 同じ子供に対する関数適用は存在しない)を含む Old Known Result: MTT-OI ⊂ TT ∘ LinMTT ∘ TT

29 Trn. Mem. of Path-lin MTT-OI ≪NP & DSPACE(n)≫ : Proof
非決定性MTT τ を、”+” という特殊なノードを出力する決定性MTT τd へと変換する h( S(x), y )  A(y, y) h( S(x), y )  B(y, y) h( Z, y )  A(y, y) h( Z, y )  B(y, y) h( S(x), y )  +(A(y,y), B(y,y)) h( Z, y )  +(A(y,y), B(y,y))

30 + S A B S + + + + A B A B A B A B Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z

31 Trn. Mem. of Path-lin MTT-OI ≪NP & DSPACE(n)≫ : Proof
「b ∈ τ(a)」 if and only if 「τd(a) のそれぞれの “+” ノードを左右どちらかの子でうまく置き換えると b になる」 τd(a) と b を top-down に再帰的に比較するだけで判定できる GOOD |τd(a)| >>>> |a|+|b| かもしれない τd(a) をマジメに計算はできない BAD

32 τ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 のノード表現から親ノードの表現を計算できれば↑は不要

33 Trn. Mem. of Path-lin MTT-OI ≪NP & DSPACE(n)≫ : Proof
τd(a) の圧縮表現 τd(a) の各ノードは、そのノードを生成した瞬間のτd の「コールスタック」で表現できる f( S(x) )  g(x, h(x, Z)) f( Z )  Z g( S(x), y )  g(x, h(x, y)) g( Z, y )  y h( S(x), y )  +(A(y,y), B(y,y)) h( Z, y )  +(A(y,y), B(y,y)) + A B <<g>>(x, h(x, Z)) g(x, <<h>>(x, y)) +(<<A>>(y,y), B(y,y))

34 「コールスタック」の高さ ≦ |a| なので、 τd(a) を O(|a|)サイズに圧縮できた！
問題点： 「コールスタック」で表現されたノードの 子ノードや親ノードを得ることは可能か？ その計算量は？

35 文脈自由木言語によるXML圧縮[BLM08]
子ノードを得ることは可能 「色々な条件を満たしていれば」線形時間で可能 「パラメタ変数の使われ方が linear ならば」 親ノードを得ることが（線形時間で）可能 [Inaba/Maneth08] Path-linear ならば線形時間で子ノードを計算可能 Path-linear ならば「コールスタックツリー表現」を使うことで、線形時間で親ノードを計算可能

36 「コールスタックツリー表現」 基本アイデア 追加アイデア
子ノードを計算できるノード表現χがあれば、 　「祖先ノード全部をχで表現したリスト」 で各ノードを表すことにすれば、 子ノードも親ノードも計算もできるようになる 問題点： サイズがO(|a|)ではなくなる 追加アイデア ノード v のコールスタック表現と、vの子ノードのコールスタック表現は、「よく似ている」 『「祖先ノード全部をχで表現したリスト」を共通部分はできるだけまとめた trie 構造』でノードを表現すればいい Path-linear なら O(|a|) サイズになる

37 おさらい Path-linear MTT の変換メンバシップ判定は NP かつ DSPACE(n) 出力木のノードの「コールスタック表現」
さらに 「コールスタックツリー表現」

38 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.判定に帰着

39 Translation Membership of MTT∘MTT ∘・・・∘MTT
基本的アプローチを真っ向から実行すると Old Known Result: b ∈ τ(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

40 Translation Membership of MTT∘MTT ∘・・・∘MTT
基本的アプローチを真っ向から実行する ことの問題点 変換の途中結果が大きすぎる 最終出力 b が実際に大きい場合は、 それでも（計算量的には）問題ない |a| <<< |ai| >>> |b| なケースが問題 ↑こういうケースを除きたい

41 Theorem ≪Garbage Free Form≫
任意のPath-linear MTT合成列 τ = τ1 ; τ2 ; … ; τk に対し、等価な合成列 τ = γ0 ; γ1 ; γ2 ; … ; γk で、任意の b∈τ(a) に対し a0∈γ0(a),…, ai=γi(ai-1),..., b=ak=γk(ak-1) |ai-1|/2 < |ai| for all i を満たす中間結果列 a0,…,ak を とれるものを構成できる

42 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.判定に帰着 □

43 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判定に帰着 □

44 Garbage Free Form の帰結 (3)
range(MTT∘MTT ∘・・・∘MTT) の有限性は 決定可能 Proof. GFFなら、range(τ)が有限 iff range(γ0)が有限。 実はGFFの最初の変換γ0のrangeは、正規木言語であることが示せる。 正規木言語の有限性は決定可能　□

45 Proof Sketch of GFF Theorem (1/3)
最後のMTTを「サイズを減らさない」ものに変形 … ;τk-1 ; τk … ;τ’k-1 ; γk の繰り返し 　（正確には、最後から2番目のMTTを、「最後のMTTが使わない部分木は生成しない」ものに変形、の方が近い？）

46 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” 子供が１つのノードで、ただ別の関数を呼ぶだけ f(σ(x), y1, …, yk )  g(x, y1, …, yk )

47 Proof Sketch of GFF Theorem (3/3)
Erasure, Input-Deletion, Skipping が起きそうな箇所を予測して、先に削除しておく ツリートランスデューサ τk-1 ; τk  τk-1 ; (E ; I ; S ;γk ) (結合則)  (τk-1 ; E ; I ; S) ;γk (MTT-OI はE,I,Sの後ろからの合成に 関して閉じている)  τ’k-1 ;γk

48 補足: Combined Complexity of Translation Membership
DtMTT: O( |M|・(|a|+|b|) ) MTT-IO: O( |M|・|a|・|b|2k+2 ) Path linear MTT-OI: O( |M|・poly(|a|+|b|) ) ※ Nondet. MTT ∘MTT ∘… ∘MTT: O( 2^2^2^2^…^|M| ・ poly(|a|+|b|) ) ※Nondet.

49 まとめ Macro Tree Transducer “Translation Membership” 文献 制限された関数型言語
オートマトン＋ツリー＋出力＋パラメタ 非決定性。IO / OI “Translation Membership” 圧縮表現 Garbage Free Form 文献 J. Engelfriet and H. Vogler, “Macro Tree Transducers”, JCSS(31) , 1985 K. Inaba and S. Maneth, “The Complexity of Tree Transducer Output Languages”, To appear in FSTTCS 2008