Complexity and Expressiveness of Models of XML Translations 東京大学大学院 情報理工学系研究科 コンピュータ科学専攻 細谷研究室 稲葉 一浩 背景 XML処理プログラムの さまざまな性質を静的に検証したい 例： 「想定される全ての入力に対し、エラー状態に陥らず処理 を完了する」 例： 「問題のある出力（型エラー、スクリプトインジェクション等） を決して出さない」 どうやって？ 諸性質を決定可能な抽象化されたモデルによって プログラムを表現/近似し、そのモデルで性質を検証 XSLT, XQuery, XDuce, E4X 等 のプログラム 「モデル」 検証 木構造変換のモデル 検証のためのモデルに望まれる性質 高い表現力 より多くのプログラムを、より高精度に近似可能 種々の検証問題の決定可能性 プログラムからのモデル構築の容易さ 歴史 Syntax-Directed Translation [Irons 1960] Attribute Grammar [Knuth 1968] (Attributed Tree Transducer) [Fülöp 1981] Top-down/Bottom-up Tree Transducer [Thatcher&Wright 1970] Tree-Walking Transducer [Aho&Ullman 1980] Macro Tree Transducer [Engelfriet 1980, CourFrZ 1982] MSO-Definable Tree Translation [Courcelle 1994] Pebble Tree Transducer [Milo&Suciu&Vianu 2003] Macro Tree Transducer (MTT) の長所 高い表現力 前ページのモデルは全てMTT、もしくはその合成でシミュレート可能 現実のXML処理言語のよいモデル化として使われている XML-QL, (“expressive fragment of”) XSLT [MSV00], DTL [MBPS05], ... 多くの性質が決定可能 全域性 Emptiness Domain/Range のメンバシップ Range の有限性 “Exact” な型検査 … MTT の短所 多くの性質が決定可能 → しかし、具体的な計算量が未知の問題が多い 変換メンバシップ 出力言語のメンバシップ 出力言語の有限性 … 合成に関する閉包性が非常に弱い MTTと他の変換の合成は、一般にはMTTで表現できない なぜ「合成」が重要か？ 木構造処理プログラムは複数の処理の組み合 モデル わせで記述されることが多い M = M1 ; M2 ; … ; Mk XMLDBへのクエリ 出力用に整形 Syntax Sugar の展開 最適化 別形式で出力, etc 合成が可能であれば、「処理それぞれに対応す るモデルを個別に計算したのち、合成」で全体の モデルMk モデルM2 モデルM1 モデルが構築可能 処理１ 入力 処理２ 処理k ・・・・ 出力 なぜ「合成」が重要か？ なぜ全体を「ひとつの」モデルで表現したいか？ （「MTT k 個の合成」という表現に対して 静的検証を行えばよいのでは？？） “k個の合成” に対する静的検証アルゴリズムは、 “MTT1個” に対する静的検証と比較して、一般に 複雑である 効率的な実装がMTT1個の場合のみ。k個への拡張は困難な例 など (e.g. Exact Type Checking [Maneth&Perst&Seidl 2007, Frisch&Hosoya 2007], Specialization [Matsuda&Fu&Takeichi 2009], etc) 計算量が大きい (P vs NP, EXPTIME, …) 本研究の貢献 MTTの拡張 ‘Multi-Return MTT’ を提案 MTTにはない、合成に関する良い閉包性 DT ； mrMTT ； DtT ⊆ mrMTT MTT同様の決定可能性と、より高い表現力を持つ MTTとその合成に関する計算量の研究 結果 出力言語のメンバシップ判定: DSPACE(n) かつ NP完全 変換メンバシップ判定: PTIME (1個), DSPACE(n) かつ NP完全 (合成) キーアイデア MTTの合成に伴う計算量の指数爆発を押さえるための 汎用性のある技法 “Garbage-Free Form” を証明 発表の流れ MTTの概要 Contribution 1 合成可能性に優れたモデル “Multi-Return MTT” Contribution 2 MTT1つの “変換メンバシップ問題” の計算量 Contribution 3 MTT合成列の計算量: “Garbage-Free Form” RHS ::= F( RHS, … , RHS ) | q(xi, RHS, …, RHS) | yi MTT とは start( A(x1) ) → double( x1, double(x1, E) ) double( A(x1), y1) → double( x1, double(x1, y1) ) double( B, y1 ) → F( y1, y1 ) double( B, y1 ) → G( y1, y1 ) Tree(Σ) から Tree(Δ) への変換を表すMTT ＝ 型 Tree(Σ) × Tree(Δ)k Tree(Δ) の関数の集まり 第一引数（＝入力木）に関して帰納的に定義される 第一引数のラベルによって分岐 関数適用は、現在のノードの直接の子ノードに対してのみ可能 第２、第３、…引数(Accumulation Parameters)に対しては、 ラベルを見たり子ノードを得たりできない 各関数は、出力木１つを返す 非決定性MTT 非決定性の使われかた 「条件を満たす任意のノード１つ」のような 非決定的なクエリの表現 MTTの表現力を超える制御フローの近似 double( B, y1 ) = if complicated_condition then F( y1, y1 ) else G( y1, y1 ) double( B, y1 ) → F( y1, y1 ) double( B, y1 ) → G( y1, y1 ) 2つの評価戦略: IO と OI double( A(x1), y1) → double( x1, double(x2, y1) ) double( B, y1 ) → F( y1, y1 ) double( B, y1 ) → G( y1, y1 ) IO (inside-out / call-by-value)： 引数を評価してから関数呼び出し start(A(B)) double( B, double(B, E) ) double( B, F(E, E) ) F( F(E,E), F(E,E) ) or G( F(E,E), F(E,E) ) or double( B, G(E, E) ) F( G(E, E), G(E, E) ) or G( G(E, E), G(E, E) ) 2つの評価戦略: IO と OI double( A(x1), y1) → double( x1, double(x2, y1) ) double( B, y1 ) → F( y1, y1 ) double( B, y1 ) → G( y1, y1 ) OI (outside-in / call-by-name)： 引数を評価せずに先に関数呼び出し start(A(B)) double( B, double(B, E) F( double(B, E), double(B, E) ) F( F(E,E), double(B, E) ) F( F( F( G(E,E), double(B, E) ) F( F( G( double(B, E), double(B, E) ) G( F(E,E), double(B, E) ) G( G( G( G(E,E), double(B, E) ) G( G( ) F(E,E), F(E,E), G(E,E), G(E,E), F(E,E) G(E,E) F(E,E) G(E,E) ) ) !! ) !! ) F(E,E), F(E,E), G(E,E), G(E,E), F(E,E) G(E,E) F(E,E) G(E,E) ) ) !! ) !! ) IO or OI? なぜ二つの評価戦略を考えるのか？ IO は一般に、OIより良い近似となる // f(A(x)) if ≪complex_choice≫ then e1 else e2 nondet_f( A(x) ) e1 IO でのみ nondet_f( A(x) ) e2 左右の木が 常に等しい start( A(x) ) dup(x, nondet_f(x)) dup( A(x), y ) B(y, y) OI MTTの合成はIO MTTの合成より良い性質を持つ （後述） “Garbage-Free Form” は、 OIでのみ構成法が得られている MTTIO ⊆ MTTOI;MTTOI && MTTOI⊆MTTIO;MTTIO Contribution 1 [Published at PLAN-X08 and CIAA08] 合成可能性に優れたモデル “Multi-Return MTT” 木構造変換モデルの階層 [EV85] DT ; MTTOI ⊆ MTTOI [OurWork] MTTOI ; LT ⊆ MTTOI [EV85] LHOM ; MTTIO ⊈ MTTIO [OurWork] MTTIO ; LDtT ⊈ MTTIO [OurWork] MTTOI ; DtT ⊈ MTTOI MTTOI MTTIO [Fül81] DtT ; ATTR ⊈ ATTR mrMTTIO [Our Work] DT ; mrMTTIO ⊆ mrMTTIO mrMTTIO ; DtT ⊆ mrMTTIO [Fül81] DtT ; DATTR ⊈ DATTR ATTR [Fül81] DATTR ; DtT ⊆ DATTR [Eng77] TR ; TR ⊈ TR [Cou94] MSOTT ; MSOTT ⊆ MSOTT [Eng77] TR ; DTR ⊆ TR DTR ; TR ⊆ TR [Bak79] B ; B ⊈ B DATTR TR MSOTT [Eng77] DTR ; DTR ⊆ DTR [Rou70] DtT ; DtT ⊆ DtT [Bak79] B ; LB ⊆ B DB ; B ⊆ B B [Eng77] LTR ; LTR ⊆ LTR DTR LTR = LB DtT [Bak79] DB ; DB ⊆ DB DB Multi-Return MTT f( ROOT(x) ) → let (z1, z2) = g( x, NIL ) in QUERY( z1, z2 ) g( A(x), y1, y2 ) → let (z1, z2) = g( x, y1, y2 ) in (CONS(copy(x), z1), z2) → let (z1, z2) = g( x, y1, y2 ) in (z1, CONS(copy(x), z2)) → (y1, y2) g( B(x), y1, y2 ) g( L, y1, y2 ) 特徴 LET ::= let (z1,…,zn) = q(xi, TR, …, TR) in RHS ::= LET* (TR, …, TR) TR ::= δ(TR, …, TR) | yi | zi 各関数は、複数の出力木からなる組を返す “let” 構文により、返値の組を分解して使う 右からの合成 MTTIO ; DtT ⊈ MTTIO [Our Work] 合成をMTTで表現できなくなる後処理の例 （以下の規則を再帰的に適用）: L R mrMTTIO ; DtT ⊆ mrMTTIO [Our Work] DtT = “deterministic, total, and top-down” 累積引数を使わずtop-downの再帰で書ける全域関数 右からの合成（証明の概要） mrMTTIO ; DtT ⊆ mrMTTIO 基本アイディア：mrMTT の関数 f と DtT の関数 g 各々に ついて、合成関数 <f;g> を作る 非決定性の処理に Multi-Return が必要。例： mrMTT の関数 f( A(x) ) A( nondet(x) ) DtT の関数 g( A(x) ) B( g1(x), g2(x) ) × 間違い <f;g>( A(x) ) = g(f(A(x)) = g(A(nondet(x)) = B( g1(nondet(x)), g2(nondet(x)) ) = B( <nondet;g1>(x), <nondet;g2>(x) ) ○ 正解 <nondet;g1/g2>(…) (nondet(x)にg1とg2を適用した結果のペア) <f;g>( A(x) ) let (z1,z2) = <nondet;g1/g2>(x) in B( z1, z2 ) 左からの合成 DtT ; MTTIO ⊈ MTTIO [Engelfriet&Vogler 1985] 合成をMTTで表現できなくなる前処理の例 （ルートに１つノードを追加）: X DT ; mrMTTIO ⊆ mrMTTIO [Our Work] DT = “deterministic and top-down” 累積引数を使わずtop-downの再帰で書ける関数 左からの合成（証明の概要） DT ; mrMTTIO ⊆ mrMTTIO 基本アイディア： 同様に合成関数 <f;g> を作る 非決定性ルールのインライン展開にletが必要 DTの関数 f(L) A(L) mrMTTの関数 g(A(x)) h(x, nondet) h(L, y) B(y, y) × 間違い <f;g>(L) = g(f(L)) = g(A(L)) = h(L, nondet) = B( nondet, nondet ) ○ 正解 <f;g>(L) let z = nondet in B(z, z) 関連研究 (左合成可能な MTTIO の拡張) T ; YIELD [Engelfriet&Vogler 1985] MTTIO を簡単な変換モデルの合成で特徴付けようと する際にベースとなったクラス (MTTIO = res-T ; YIELD) HMTT [Maneth&Nakano 2008] Macro Tree Transducer with Holes : “穴”の空いた木 と、穴への木の挿入操作を持つMTT MTTIO ; YIELD ⊆ HMTTIO 【本研究の特徴】 右からの合成にも 対応している MTTIO ⊊ T;YIELD=HTT=1-mrMTT ⊊ HMTT ⊊ mrMTT 関連研究 (Multi-Return) Multi Bottom-up Tree Transducer [Fülöp&Kühnemann&Vogler 2004] Top-down 変換の Bottom-up 変換での 特徴付け MTTOI mrMTTIO MTTIO ATTR MSOTT TR 【本研究の特徴】 DTR = mrDB “Multi-Return” の 合成可能性への応用 DtT DATTR B LTR = LB DB Contribution 2 [Published at PLAN-X09] MTT1つ の “変換メンバシップ問題” の計算量 変換メンバシップ問題とは 変換 τ の “変換メンバシップ問題” とは: 入力: 二つのツリー s と t 出力: (s , t ) ∈ τ ? s ？ τ t 変換メンバシップ問題とは Assertion のチェック assert( run_my_xslt( load_xml(“test-in.xml”) ) == load_xml(“test-out.xml”) ); 「左辺を計算して右辺と比較」より高速に判定可能か？ 非決定性MTTの場合は？ MTTの計算は指数ステップ（以上）かかることがあるが、 それよりも効率的に変換メンバシップを解けるか？ 外部からの副作用（ランダムな選択、グローバルオプション等） を非決定性でモデル化した場合、「指定の出力を出す Configurationはあるか？」を問う より複雑な判定問題の部分問題 （後述）出力言語メンバシップ判定問題 本研究で得られた結果 MTTOI NP完全, DSPACE(n) 系: MTTIO;MTTIO NP-hard MTTIO とその拡張 多項式時間 Multi-Return 系: DT* ; mrMTT ; DtT* 多項式時間 Regular+(Dis)equality look-ahead f( A(x1,x2) ) s.t. x1≡x2 → C( f(x1) ) f( A(x1,x2) ) s.t. x1 has even number of nodes → D( f(x1), f(x2) ) f( A(x1,x2) ) otherwise → E( f(x1), f(x2) ) 変換メンバシップの計算量: MTTOI MTTOI の変換メンバシップは NP-hard [Our Work] 3-SAT からの還元で証明 2つの自然数(n,m)をエンコードした入力木から、節数n、 変数m種のSATisfiable論理式を全て生成するMTTが存在 e.g., A 2 clauses ∨ ∨ A B 3 variables ∧ x1 x2 τ x2 x3 ∧ or B ∨ B ￢ x2 Z x1 x3 x1 ∨ x3 x1 x2 ￢ x3 変換メンバシップの計算量: MTTOI MTTOIの変換メンバシップは NP, DSPACE(n) [OurWork] 文脈自由文法による圧縮 出力集合 τ(s) は、|s| に比例するサイズの文脈自由木文法 で表現可能 [Maneth&Busatto 2004] ∈ S t τ(s) 圧縮表現上での木のなぞり (up, 1stchild, nextSibling) を効 率的に実行可能なクラス path-linear MTTOI の発見 [OurWork] 変換メンバシップの計算量: MTTIO MTTIOの変換メンバシップは PTIME [OurWork] (最大でk引数のMTTの場合, O(n2k+2)) Inverse Type Inference [EV85, MSV03] の応用 逆像 τ-1(t) は指数サイズ 2|t| のオートマトンで受理できる 正規言語である S ∈ t τ-1(t) オートマトンの構築を、sに対するrunに必要になった部分 のみlazyに行うことで、多項式時間での実行が可能 変換メンバシップの計算量: mrMTTIO mrMTTIOの変換メンバシップは PTIME [OurWork] (最大でk引数d返値のMTTの場合, O(n2k+2d)) MTTIO に対するアルゴリズム（Inverse Type Inference） の straightforward な拡張 系: DT ; MTTIO ; DtT の変換メンバシップも PTIME 【mrMTTの有効性の一例】 Inverse Type Inference×3 の遅延実行でPTIMEアルゴリズムを得るのは 困難 （Inv. Type Inf. の実行にはオートマトン全体の情報が必要なため） mrMTTIO で表現すれば、Inverse Type Inference ×1 の適用となりTrivial!! 関連研究 (変換メンバシップ問題の計算量) Top-down Tree Transducer [Baker 1978] 非決定性あり、Accumulation Parameter なし DSPACE(n) ( O(n4) [Our Work]) Total Deterministic MTT [Maneth 2002] 非決定性なし、 Accumulation Parameter あり DTIME(n) 【本研究の特徴】 より表現力の高いクラスを対象としている （非決定性と Acc. Param. を合わせて初めて 発生する組み合わせ爆発の解決） Contribution 3 [Published at FSTTCS08] “Garbage-Free Form” による MTT合成列の計算量の研究 変換メンバシップの計算量: MTT* τ = τ1 ; τ2 ; τ3 ; … ; τk where τi∈ MTTIO ∪ MTTOI の変換メンバシップ問題の計算量は？ 既にわかっていること 少なくとも、NP-hard MTTIO* = MTTOI* = mrMTTIO* [EV85, Our Work] 基本アプローチ: Generate & Test 変換の中間木構造 s1, …, sk-1 を推測 MTT1つ1つの変換メンバシップを判定 (s,s1)∈τ1, (s1,s2)∈τ2, …, (sk-1, t) ∈τk 全て成り立てば、 (s,t) ∈ τ1 ; … ; τk 成り立たなければ別の s1, …, sk-1 を試す s τk ∈ τ2 ∈ τ1 s1 ∈ s2 Sk-1 t 基本アプローチ: Generate & Test 変換の中間木構造 s1, …, sk-1 を推測 MTT1つ1つの変換メンバシップを判定 (s,s1)∈τ1, (s1,s2)∈τ2, …, (sk-1, t) ∈τk 全て成り立てば、 (s,t) ∈ τ1 ; … ; τk 成り立たなければ別の s1, …, sk-1 を試す s 2n Good News もし∀n.|sn| < O(|s|+|t|) な ら、このアルゴリズムは NP/DSPACE(n) s1 ∈ τk ∈ τ2 ∈ τ1 Good News τ(s) は有限なので、 s1,…,sk-1の候補は有限 停止性の保証 Bad News |sn|=O(2^2^..2^2^|s|) s2 Sk-1 t [Our Work] “Garbage-Free Form” of MTTOI* 任意のMTTIO/OI 合成列 τ = τ1 ;τ2 ;τ3 ; … ; τk に対して、等価な MTTOI の合成列 τ = μ1 ; μ2 ; μ3 ; … ; μ2k+1 で、 μ2 ～ μ2k+1 は nondeleting, (i.e., |in|/2≦|out|) なものを構成可能 （※ μ1 ; μ2 ; μ3 ; … ; μ2k+1 は最終出力と比べて無駄に巨大な 中間構造を作らない(Garbage-Free)計算が可能） Nondeleting と Garbage-Free の関係 「|s|+|t| より大きい中間木構造がある いずれかの変換 τn がdeleting」 τ1 τ2 τk s2 s Sk-1 t s1 よって、「すべての変換がnondeleting 中間構造のサイズ < O(|s|+|t|)」 Garbage Free Form (証明概略) “Deletion” のくくり出し τ1 ; τ2 ＝ τ1 ; (D2 ; μ2) ＝ (τ1 ; D2) ; μ2 ＝ ρ1 ; μ2 ＝ D1 ; μ1 ; μ2 τ2 を、不要な入力を 削除する変換 D2 と、 nondeleting な μ2 へ分解 結合則 τ1 と D2 の合成 （MTTOI でのみ可能） 同様に Garbage-Free Form の応用 [Our Work] 変換メンバシップ 出力言語のメンバシップ判定 （変換τ、入力型 Sで決まる出力集合τ(S) に対し、 木 t が含まれるか t∈τ(S) ？） NP完全、DSPACE(n) NP完全、DSPACE(n) 非決定性計算 （変換τ、入力木sに対し、τ(s)に属す木 t を１つ計算） |s|+|t| に関して NP、DSPACE(n) [Future Work] PTIME? 関連研究 (Garbage-Free Form) Top-down Tree Transducers [Baker 1978] 非決定性あり、Accumulation Parameter なし Total Deterministic MTT [Maneth 2002] 非決定性なし、 Accumulation Parameter あり 【本研究の特徴】 - より表現力の高いクラスを対象としている。 - 非決定性と Acc. Param. の組み合わせで生じる 新種のdeletion を分離する手法の提案。 （MTT のSyntax的な拡張 MTTCF を導入することで、 inline展開等のプログラム変換を可能とし、分離を実現） f( A(x) ) dup( x, mayDelete(x) ) dup( A(x), y ) B( y, y ) [Our Work] DSPACE(n), NP完全 関連研究 （Level-n文法 [Damm82] のメンバシップ） [Kuroda64] = NSPACE(n) 文脈依存文法 [Maneth02] DSPACE(n) DtMTT* の出力言語 [Asveld81] PTIME MTTOI* の出力言語 Level-n IO文法 Level-n OI文法 ？ Level-2 IO文法 Level-2 OI文法 ？ IO マクロ文法 = L1-IO文法 OIマクロ文法 = L1-OI文法 (CYK) PTIME 文脈自由文法 = Level 0文法 [Aho68] NSPACE(n) [Rounds73] NP完全 Conclusion まとめ（本研究の貢献） “Multi-Return MTT” の提案 DtT (Accumulation Parameterを使わずにtop-downの再帰で 記述できる全域関数) との合成に関して閉じたクラス MTTおよびその合成に関する計算量の研究 “変換メンバシップ” IO MTT (およびその幾つかの拡張) 1つの場合多項式時間 OI MTT (またはMTTの合成列) の場合NP完全 / DSPACE(n) “Garbage-Free Form” 任意のMTT合成列を無駄な中間構造を作らないよう変形 “変換メンバシップ”、”出力言語のメンバシップ” の 計算量 NP完全/DSPACE(n) を証明 将来の研究課題 (1) Garbage-Free Form のさらなる応用・拡張 非決定性計算: 入力木 s 、変換 τ から t ∈ τ(s) を「どれか一つ」 取り出すのに必要は計算量は？ 予想： PTIME 現在のGFFは、中間木構造である「τi(si) の要素」のサイズ を押さえている。これを拡張し、|τi(si)| の無駄を消す必要 がある。 range(τi) ⊆ dom(τi+1) という条件を加えたGFF 将来の研究課題 (2) 変換メンバシップ等の実用的な実装 推測 変換の中間木構造 s1, …, sk-1 を MTT1つ1つの変換メンバシップを判定 (s,s1)∈τ1, (s1,s2)∈τ2, …, (sk-1, t) ∈τk 全て成り立てば、 (s,t) ∈ τ1 ; … ; τk 成り立たなければ別の s1, …, sk-1 を試す NPやDSPACE(n)の全探索でs1, …, sk-1を探す 非現実的 現実のプログラムでは s1, …, sk-1 のかなりの部分が 決定的に定まる 実用的な実装の可能性 発表論文 博士論文に含まれている研究 Kazuhiro Inaba and Haruo Hosoya, “Mulit-Return Macro Tree Transducers”, Workshop on Programming Language Techniques for XML (PLAN-X 2008) Kazuhiro Inaba, Haruo Hosoya, and Sebastian Maneth, “Multi-Return Macro Tree Transducers”, International Conference on Implementation and Application of Automata (CIAA 2008) Kazuhiro Inaba and Sebastian Maneth, “The Complexity of Tree Transducer Output Languages”, Foundation of Software Technologies and Theoretical Computer Science (FSTTCS 2008) Kazuhiro Inaba and Sebastian Maneth, “The Complexity of Translation Membership for Macro Tree Transducers”, Workshop on Programming Language Techniques for XML (PLAN-X 2009) その他 Kazuhiro Inaba and Haruo Hosoya, “XML Transformation Language Based on Monadic Second-Order Logic”, Workshop on Programming Language Techniques for XML (PLAN-X 2007)
© Copyright 2024 ExpyDoc
