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

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

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

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

例 : 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

定義 : 決定性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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 に入る が成立するように遷移関数を定める

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)) になる が常に成立するように遷移関数を定める

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 ) 関数の値

具体例 : “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()

具体例 : “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()

参考資料 “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

おわり