木変換の逆正規性保存
On Inverse Regularity Preservation
稲葉 一浩（国立情報学研究所）

木変換とは？
Treeを受け取り
rdfchantitle

itemdatef
プログラム

link

Treeを返す
html
headbodymeta

h1 p（XML処理、コンパイラ、…）

div木変換とは？

おことわり
今日は、簡単のため文字列変換で例示します逆正規性保存とは？
【定義】
f が逆正規性保存 (IRP) ⇔∀L:正規言語. f-1(L)={t | f(t)∈L}も正規f-1(L)正規fL
正規例：dup(x) = xx
dup-1( a*b*) = a*|b*発表内容
MTT*という言語のプログラムは全て逆正規性保存 [EngVog85]

MTT* ⊆ IRP
この包含は proper だろうか？

MTT*⊊IRP or MTT*=IRP ?
*Today’s Talk+

背景：IRPの応用例 @ XML
型チェック

f :: L1 → L2 ？

f– 入力の型(=スキーマ)(= 正規言語) L1– 出力の型(=スキーマ)(= 正規言語) L2– XML変換プログラム

IRPなら計算可能!

-1
fの型が正しい ⇔ f(L1)⊆L2 ⇔ L1⊆f (L2)

なぜ逆方向？
• 順正規性保存(FRP) 「∀L:正規. {f(t) | t∈L}も正規」を考えないのは何故か？
– 理由１： よくある関数は FRP であるよりは IRP である方が多い傾向にある (例えば dup)
– 理由２： 型エラーが起きたときに、IRPで型チェックをする方が良いエラー理由を表示しやすい• 「型エラー 」＝ 「L1⊆f-1(L2) が成り立たない」 ＝「 f-1(L2)に入らないのにL1に入る反例 t がある」＝「その木 t を入力したときに、型が合わない結果になってしまう！」という、実際にエラーを起こす入力例を提示できる– あとはこの入力を使ってステップ実行デバッグするなり出力を計算して眺めてみるなり…

• FRP では「型エラー 」 ＝ 「f(L1)⊆L2 が成り立たない」 ＝ 「 L2 に入らないのにf (L1)に入る反例 t がある」 ＝「なにか下手な入力を入れると、こんなまずい出力がでちゃうよ！」という、エラー時の出力例を提示– じっと睨んで、こんなのが出てしまう理由を推測する位しかできない現実の(XML処理)言語は…

当然、IRPとは限らない制限された言語を考える
XSLT, XQuery, …
MTT*

IRP

＝「この範囲の言語機能だけ使って書けば、完全な型チェックができますよ」＝「範囲外なら、この範囲の機能で近似して、近似的な型チェック」

制限された言語を考える
XSLT, XQuery, …
MTT*

PTT*

IRP

ATT*
TBY*
MM*MFT*＝「この範囲の言語機能だけ使って書けば、完全な型チェックができますよ」＝「範囲外なら、この範囲の機能で近似して、近似的な型チェック」

それぞれのカバー範囲は？
XSLT, XQuery, …

IRP
MTT* = PTT*
= ATT* = TBY* = …
「IRPに入りつつ十分表現力もある木変換言語」の既存の提案は、すべて表現力が一致する！

Q: 実はIRPも一致するのでは…？

=IRP?

MTT* = PTT*
= ATT* = TBY* = …

Q: 実はIRPも一致するのでは…？

The Answer is No!

=IRP?

MTT* = PTT*
= ATT* = TBY* = …

証明 (1)
文字列を超指数的に長くする関数n2^^ntower( “a..a” ) = “aa…aa”
where 2^^0 = 1, 2^^(n+1) = 22^^n

は MTT* で表現できない [EngVog85]∵ 「MTT*≒構造再帰と関数合成のみで書ける木変換」
では指数的増加しか書けない証明 (2.1)
tower 関数は IRP である
つまり ∀L:正規. {x |tower(x)∈L} も正規∀L: 正規aaaa a

出力文字はaしかないのでa aaa

L = { an | n≡r1 or … or n≡rk mod m } の形(※ただし有限個の違いは除く)証明 (2.2)
L = { an | n≡r1 , …, rk mod m } について{x | tower{x}∈L}= {an | 2^^n ≡r1, … ,rn mod m} は正規？
Yes! 2^^n mod m は、(※有限個のnを除き) 定数
なのでこの集合は(※有限個を除き)全体集合か空集合– m が奇素数 → フェルマーの小定理より
2^^n+1 ＝ 2^(2^^n) ≡ 2^(2^^n mod m-1) ＝ 2^定数–m=2→ 常に0 なので定数– m が合成数 → 中国剰余定理より素数に帰着まとめ示したこと

MTT* ⊊ IRP
未解決問題：towerより現実的な例はあるか？

MTT*∩LSI ⊊ IRP∩LSI？
※ LSI = Linear Size Increasei.e., exists c > 0, forall t, size(f(t)) ≦ c size(t)参考文献“Regularity Preserving Functions”[Kosaraju74] [Seiferas&McNaughton76, Kozen96, Zhang99]– f : N  N が Regularity Preservingとは「∀L:正規言語. {x |∃y. f(|x|)=|y| & xy∈L}も正規」– “Inverse” という形容はないが、本質的にAlphabet１種類の文字列変換の IRP と同値– RP iff f is “ultimately periodic“ modulo any n∈N– 接尾辞以外の除去への拡張等 [Matos06, Berstel et al., 06]• (2010/03/11 追記)
tower が IRP であることも [Berstel et al., 06] に書いてありました！
http://dx.doi.org/10.1016/j.tcs.2005.11.034

MTT*とは [Engelfriet&Vogler85](for MTT*∩LSI, see [Engelfriet&Maneth03])

MTT = 木の上の(相互)構造再帰＋ 累積変数
- 型 Tree(Σ) × Tree(Δ)k  Tree(Δ) の関数の集まり

MTT* = 有限個のMTTの合成
MTT ::= FUN … FUN
FUN ::= f(A(x1,…,xn), y1,…,yk) → RHS
RHS ::= C( RHS, … , RHS )| f(xi, RHS, …, RHS) | yi例：

start( A(x1) )→ double( x1, double(x1, E) )double( A(x1), y1) → double( x1, double(x1, y1) )double( B, y1 )→ C( y1, y1 )

主補題の証明 (mで帰納法)∀m∃km ∀n≧km. (2^^km ≡ 2^^n mod m)– m = 1: km=0 とすると以降全て ≡0 mod m– m = 2: km=1 とすると以降全て ≡0 mod m– m = p (奇素数):• フェルマーの小定理から 2p-1 ≡ 1 mod p より
• 2^^n+1 = 22^^n≡2(2^^n % p-1) mod p である• 帰納法の仮定より n≧kp-1以上で 2^^n % p-1 は定数• ゆえに kp = kp-1 + 1 とすれば題意を満たす– m = a b (合成数, a,b は互素):• 中国剰余定理より、二数が mod a, mod b で等しければmod ab でも等しいゆえに km = max(ka, kb) と取ればよい証明: tower∈IRP• L⊆a* を正規言語とする– Folklore: （決定性オートマトンの構造より）• L は Lf ∪ (Lr / Lb) という形。ただし• Lf , Lb は有限集合• Lr ={an | n%m∈{r1,…,rk}} for some m & r1, …, rk＜m– 逆写像の集合論的性質より• tower-1(L) = tower-1(Lf) ∪ (tower-1(Lr) / tower-1(Lb))– tower は単射なので、有限集合の逆像は有限集合• tower-1(Lf) と tower-1(Lb) は有限。よって正規言語– 主補題より• tower-1(Lr) = L1 ∪ L2
• L1 = {an | n＜km, f(an)∈L} 有限なので正規• L2 = {an | n≧km} if 2^^km%m∈{r1,…,rk} or L2 = Φ いずれにせよ正規– 正規言語は ∪ と / で閉じているので、tower-1(L) も正規

証明: tower∉MTT*• Theorem 3.24 of [EngVog85]– f ∈ MTT ⇒ ∃c. ∀s. len(f(s)) ≦ clen(s)– 証明はSentential Formと入力sに関する帰納法• MTT* = MTT の有限合成で書ける変換– tower = f1▫f2 ▫ … ▫ fk∈MTT* (where fi∈MTT) とせよ– 先ほどの定理から• ∃c1,c2,…,ck .∀s . len(tower(s))≦ck^(ck-1^…(c1^len(s))…)• ^^ は任意の指数関数より速く増加する– 証明は以下をkに関する帰納法で∀k≧1∀q>0 ∀r∃m∈Nat ∀ n≧m .
q・ 2^^n ≧ ck^(ck-1^…(c1^n)…)• ゆえに矛盾