Macro Tree Transducers and Their Complexity Kazuhiro Inaba The University of Tokyo kinaba@is.s.u-tokyo.ac.jp

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で書くと…

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

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

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

≪関数の型≫ 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 ≪第二引数以降はその 　まま出力するだけ≫

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

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

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

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

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

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)

例 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

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

注意！ 非決定性 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)

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

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

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)) = …|…|…|…

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の方が低コストなことが多い

ここからの話 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) のメンバ判定 … を中心に。

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

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

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

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

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

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

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

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

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

+ 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

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

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

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

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

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

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

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

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

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

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

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 を とれるものを構成できる

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

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

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

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

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 )

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

補足: 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.

まとめ Macro Tree Transducer “Translation Membership” 文献 制限された関数型言語 オートマトン＋ツリー＋出力＋パラメタ 非決定性。IO / OI “Translation Membership” 圧縮表現 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