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
© Copyright 2025 ExpyDoc