Macro Tree Transducer の 型検査アルゴリズム

Presentation on theme: "Macro Tree Transducer の 型検査アルゴリズム"— Presentation transcript:

1 Macro Tree Transducer の 型検査アルゴリズム
POPLミーティング 2006/05/31 稲葉 一浩

2 Introduction XML変換言語 型チェック Macro Tree Transducer
XMLからXML（木構造から木構造）への変換に特化した専用言語 型チェック 専用言語の特徴を使って、λ計算やMLなどの一般的な型検査よりも詳細な検査ができる（可能性がある）。 Macro Tree Transducer 木構造変換の形式化のひとつ

3 発表のながれ いろいろと定義 型チェック MTTの型検査アルゴリズム 参考資料 Tree Tree Automaton
Macro Tree Transducer 型チェック Forward type inference Inverse type inference MTTの型検査アルゴリズム 参考資料

4 定義 : Tree ランクつきアルファベット Σ上のTreeを以下で帰納的に定義 Σ = {σ1, σ2, ..., σn }
rank : Σ → Nat Σ上のTreeを以下で帰納的に定義 t ::= σ1 ( t1, ..., trank(σ1) ) | σ2 ( t1, ..., trank(σ2) ) | σn ( t1, ..., trank(σn) )

5 例 : Tree c c b a a a Σ = { a, b, c } rank(a)=0, rank(b)=1, rank(c)=2
c(c(a,a), b(a)) c c b a a a

6 定義 : 決定性Tree Automaton A B C D E トップダウン ボトムアップ {Q, q0, F, δ, Σ}
δσ : Q → Qrank(σ) ボトムアップ {Q, F, δ, Σ} δσ : Qrank(σ) → Q q2 ∈F? A q3 q1 B C q1 q2 D E

7 Tree Automaton と Regularity
「決定性ボトムアップツリーオートマトンの受理する木の集合」というのは、非常によい性質を持っている Regular (正規) 等価なさまざまな定式化 Regular Tree Grammar, MSO, ... 木構造に対する「型」として一般的によく使われている → 本発表では、木の「型」はツリーオートマトンで与えることにする。

8 Macro Tree Transducer (MTT)
Treeを入力としてTreeを出力するもの トップダウンツリーオートマトン ＋ 出力付き ＋ アキュムレータ付き

9 定義 : MTT {Q, q0, Σ, Δ, ξ} Q : 状態集合 q0 : 始状態 ∈ Q Σ : 入力木のアルファベット
Δ : 出力木のアルファベット ξ : 変換規則

10 定義 : MTT : 変換規則 ξ : 以下の形の「変換規則」の集合 q ∈ Q σ ∈ Σ, n=rank(σ)
関数名 引数（Σ上の木） 引数（Δ上の木） mはq毎に固定 q(σ(x1,...,xn) )( y1, ..., ym ) ⇒ (Δ ∪ q(xi) ∪ yj) 上のTree 関数の値

11 例1 : MTT 入力 Σ= {a, c} rank(a)=2, rank(c)=0 出力 Δ= {a, b, c} rank(b)=2
q0( a(x,y) )() ⇒ a( q1(x)(), q1(y)() ) q0( c() )() ⇒ c() q1( a(x,y) )() ⇒ b( q0(x)(), q0(y)() ) q1( c() )() ⇒ c()

12 例2 : MTT 入力 Σ = {a,b,c} rank(a)=(b)=1, (c)=0 出力 Δ = {a,c}
q0( a(x) )() ⇒ a( q0(x)() ) q0( b(x) )() ⇒ q0(x)() q0( c() )() ⇒ c()

13 例3 : MTT 入力 Σ = {a,b,c} rank(a)=(b)=1, (c)=0 出力 Δ = {a,b,c}
q0( a(x) )() ⇒ q1(x)( a(q2(x)()) ) q0( b(x) )() ⇒ q1(x)( b(q2(x)()) ) q0( c() )() ⇒ c() q1( a(x) )(y) ⇒ q1(x)( a(y) ) q1( b(x) )(y) ⇒ q1(x)( b(y) ) q1( c() )(y) ⇒ y q2( a(x) )() => q2(x)() q2( b(x) )() => q2(x)() q2( c() )() => c() q2( d() )() => d()

14 MTTの表現力 １個だと「そこそこ」 有限個のMTTを組み合わせることで、かなり実用的な変換言語と同等の記述力
TL [Manethら, 2005] : ３個のMTT k-pebble tree transducer : k+1個のMTT higher order tree transducer : k個のMTT

15 問題：「型検査」 入力Treeの型 （RI） =ツリーオートマトン 変換プログラム(τ) =MTT
出力Treeの型 （RO） =ツリーオートマトン forall x. (x : RI ⇒ τ(x) : RO) ???

16 Forward Type Inference
入力の型 RI と変換MTT τ から、 実際に出力されうる木の型 RO’ を計算 RO’ ⊆ RO ならOK ダメ MTTはRegularityを保存しない コピー q(a(x))() ⇒ b(q(x), q(x))

17 Inverse Type Inference
出力の型 RO と変換MTT τ から、 入力として受け取れる木の型 RI’ を計算 RI ⊆ RI’ なら OK 大丈夫！ MTTの逆変換はRegularityを保存する！

18 アルゴリズム 出力型を表すオートマトン RO 変換MTT τ から、入力として取り得る木の型を表すオートマトン RI’ を構築する
RI ⊆ RI’ の判定アルゴリズムは既知なのでOK

19 RI’の構築 RO = {P, Pf, Δ, β} τ = {Q, q0, Σ, Δ, ξ}
RI’ = {D, Df, Σ, α} where D = { d | d : Q→(Pm→P) } Df= { d | d(q0)(())∈Pf }

20 RI’の構築 RI’ = {D, Df, Σ, α} where D = { d | d : Q→(Pm→P) } Df= { d | d(q0)(())∈Pf } ルートのノード x が状態 d∈Df になる if and only if その木を変換 q0(x) すると、 出力木の状態は Pf に入る が成立するように遷移関数を定める

21 RI’の構築 RI’ = {D, Df, Σ, α} where D = { d | d : Q→(Pm→P) } Df= { d | d(q0)(())∈Pf } 入力木のノード x が状態 d になる if and only if そのノード以下の部分木を変換 q(x,ys) すると、出力木の状態は d(q)(β(ys)) になる が常に成立するように遷移関数を定める

22 MTTの変換規則 RI’ = {D, Df, Σ, α} where D = { d | d : Q→(Pm→P) } Df= { d | d(q0)(())∈Pf } 関数名 引数（Σ上の木） 引数（Δ上の木） mはq毎に固定 q0(σ(x1,...,xn) )( y1, ..., ym ) ⇒ a( q1(x2)(y1,y3), q2(x4)(), c ) 関数の値

23 具体例 : “b”を削除するMTT q( a(x) )() ⇒ a( q(x)() ) q( b(x) )() ⇒ q(x)()
入力 Σ = {a,b,c} rank(a)=(b)=1, (c)=0 出力 Δ = {a,c} Q = {q} 入力型 b*c 出力型 c　　とすると型検査が通ることを確認 q( a(x) )() ⇒ a( q(x)() ) q( b(x) )() ⇒ q(x)() q( c() )() ⇒ c()

24 具体例 : “b”を削除 出力型 c のオートマトン {P,Pf,Δ,β} 変換を表すMTT {Q,q,Σ,Δ,ξ} β(c)() = p0
β(a)(p) = p1 Pf = {p0} P = {p0,p1} q( a(x) )() ⇒ a( q(x)() ) q( b(x) )() ⇒ q(x)() q( c() )() ⇒ c()

25 参考資料 “A Comparison of Pebble Tree Transducers with Macro Tree Transducers”, Joost Engelfriet and Sebastian Maneth, 2003 “XML Type Checking Using High-Level Tree Transducer”, Akihiko Tozawa, 2006

26 おわり