ツリーオートマトンとは、状態マシンの一種です。ツリーオートマトンでは、従来の状態マシンの 文字列ではなく、ツリー構造を扱います。
以下の記事では、木の正規言語に対応する分岐木オートマトンについて扱います。
古典的なオートマトンと同様に、有限木オートマトン (FTA) は決定論的オートマトンにも非決定論的オートマトンにもなり得ます。オートマトンが入力木を処理する方法に応じて、有限木オートマトンには (a) ボトムアップ、(b) トップダウンの 2 つのタイプがあります。これは重要な問題です。非決定論的 (ND) トップダウン木オートマトンと ND ボトムアップ木オートマトンが表現力において同等であるにもかかわらず、決定論的トップダウン木オートマトンが決定論的ボトムアップ木オートマトンよりも明らかに劣っているのは、決定論的トップダウン木オートマトンによって指定される木プロパティがパス プロパティにのみ依存するためです (決定論的ボトムアップ木オートマトンは ND 木オートマトンと同じくらい強力です)。
定義
F上のボトムアップ有限木オートマトンがタプル ( Q , F , Q f , Δ ) として定義されます。ここで、Qは状態の集合、Fはランク付けされたアルファベット(つまり、シンボルが関連付けられたアリティを持つアルファベット)、Q f ⊆ Qは最終状態の集合、 Δ は n 項 f ∈ F 、 q、q i ∈ Q 、およびサブツリーを表すx i変数に対して、 f ( q 1 ( x 1 ), ... , q n ( x n )) → q ( f ( x 1 ,..., x n ) )という形式の遷移規則の集合です。つまり、 Δ のメンバーは、子ノードのルートが状態であるノードから、ルートが状態であるノードへの書き換え規則です。したがって、ノードの状態は、その子ノードの状態から推測されます。
n =0、つまり定数記号fの場合、上記の遷移規則の定義はf () → q ( f () となります。多くの場合、空の括弧は便宜上省略されます:f → q ( f )。定数記号(葉)のこれらの遷移規則は状態を必要としないため、明示的に定義された初期状態は必要ありません。ボトムアップのツリーオートマトンがF上の基底項で実行され、すべての葉から同時に開始して上方に移動し、各サブ項にQからの実行状態を関連付けます。項のルートがQ fからの受理状態に関連付けられている場合、項は受理されます。[1]
F上のトップダウン有限木オートマトンがタプル ( Q , F , Q i , Δ ) として定義され、ボトムアップ木オートマトンとの相違点が 2 つあります。まず、初期状態の集合であるQ i ⊆ QがQ fに置き換わります。次に、遷移規則が逆になります: q ( f ( x 1 ,..., x n )) → f ( q 1 ( x 1 ),..., q n ( x n ) )、ここでn元f ∈ F、q、q i ∈ Q、およびサブツリーを表すx i変数。つまり、 Δ のメンバーは、ここでは、ルートが状態であるノードから、子のルートが状態であるノードへの書き換え規則です。トップダウン オートマトンでは、ルートの初期状態のいくつかから始まり、木の枝に沿って下方に移動し、実行に沿って状態を各サブタームに帰納的に関連付けます。すべての枝をこのように通過できれば、その木は受け入れられます。[2]
ツリーオートマトンが決定性(略してDFTA)と呼ばれるのは、Δの2つのルールが同じ左側を持たない場合です。そうでない場合は非決定性(NFTA)と呼ばれます。[3]非決定性トップダウンツリーオートマトンには、非決定性ボトムアップツリーオートマトンと同じ表現力があります。[4]遷移規則は単純に逆になり、最終状態が初期状態になります。
対照的に、決定性トップダウンツリーオートマトン[5]は、ボトムアップのものほど強力ではありません。これは、決定性ツリーオートマトンでは、2つの遷移ルールが同じ左側を持たないためです。ツリーオートマトンの場合、遷移ルールは書き換えルールであり、トップダウンの場合は、左側は親ノードになります。その結果、決定性トップダウンツリーオートマトンでは、すべてのブランチで真であるツリープロパティのみをテストできます。これは、各子ブランチに書き込む状態の選択が、子ブランチの内容を知らずに親ノードで決定されるためです。
無限木オートマトンではトップダウンオートマトンを無限木に拡張し、2つの後継者を持つモナド2階理論であるS2Sの決定可能性を証明するために使用できます。有限木オートマトン(トップダウンの場合は非決定性)はWS2Sに十分です。[6]
例
ブールリストを受け入れるボトムアップオートマトン
FとQの要素を色分けして区別し、ランク付けされたアルファベットF ={ false、true、nil、cons (.,.) } を使用し、cons のアリティが2で、その他のすべてのシンボルのアリティが0である場合、ブール値のすべての有限リストの集合を受け入れるボトムアップのツリーオートマトンを ( Q、F、Q f、 Δ ) として定義できます。ここで、 Q = { Bool、BList }、Q f = { BList }、および Δ は次の規則で構成されます。
この例では、規則は各項にボトムアップ方式で型を割り当てるものとして直感的に理解できます。たとえば、規則 (4) は「項cons ( x 1、x 2 ) はBList型を持ち、x 1とx 2 はそれぞれBool型とBList型である」と読むことができます。受け入れ可能な例の実行は次のとおりです。
正規木文法#例に示されている、オートマトンに対応する正規木文法からの同じ用語の導出を参照してください。
拒否の例の実行は
直感的には、これはcons ( false、true )という項が適切に型付けされていないことに相当します。
2進表記で3の倍数を受け入れるトップダウンオートマトン
この例では、上記と同じ色付けを使用して、ツリー オートマトンが通常の文字列オートマトンを一般化する方法を示します。図に示す有限決定性文字列オートマトンでは、3 の倍数を表す 2 進数字の文字列がすべて受け入れられます。決定性有限オートマトン#形式定義の概念を使用すると、次のように定義されます。
- 状態の集合Qは{ S 0 , S 1 , S 2 }であり、
- 入力アルファベットは{ 0,1 }であり、
- 初期状態はS 0であり、
- 最終状態の集合は{ S0 }であり、
- 遷移は表の列(B)に示されているとおりです。
ツリーオートマトン設定では、入力アルファベットが変更され、0と1 のシンボルは両方とも単項になり、ツリーの葉にはnilなどのヌルシンボルが使用されます。たとえば、文字列オートマトン設定のバイナリ文字列「110」は、ツリーオートマトン設定の項「1 ( 1 ( 0 ( nil ))) 」に対応します。このようにして、文字列をツリー、つまり項に一般化できます。バイナリ文字列表記の 3 の倍数に対応するすべての項のセットを受け入れるトップダウンの有限ツリーオートマトンが次のように定義されます。
- 状態の集合Qは{ S 0、S 1、S 2 }のままであり、
- 入力アルファベットの順位は{ 0,1,nil }で、 Arity ( 0 ) = Arity ( 1 )=1、Arity ( nil ) =0となる。
- 初期状態の集合は{ S 0 }であり、
- 遷移は表の列(C)に示されているとおりです。
たとえば、ツリー「1 ( 1 ( 0 ( nil ))) 」は、次のツリーオートマトンの実行によって受け入れられます。
対照的に、項「1 ( 0 ( nil )) 」は、次の非受理オートマトン実行につながります。
オートマトンの実行を開始するための初期状態はS 0以外にないため、用語「1 ( 0 ( nil )) 」はツリーオートマトンでは受け入れられません。
比較のために、表の列 (A) と列 (D) には、それぞれ(右) 正規 (文字列) 文法と正規木文法が示されています。これらは、それぞれ対応するオートマトンと同じ言語を受け入れます。
プロパティ
認識性
ボトムアップ オートマトンの場合、tから始まりq ( t )で終わる縮約が存在する場合、基底項t (つまりツリー) が受け入れられます。ここで、 q は最終状態です。トップダウン オートマトンの場合、 q ( t ) から始まりtで終わる縮約が存在する場合、基底項tが受け入れられます。ここで、q は初期状態です。
ツリーオートマトンAによって受け入れられる、または認識されるツリー言語L ( A )は、 Aによって受け入れられるすべての基底用語の集合です。基底用語の集合は、それを受け入れるツリーオートマトンが存在する場合に認識可能です。
線形(つまり、アリティ保存)木準同型性は認識可能性を保存します。[7]
完全性と削減
非決定性有限木オートマトンが完全であるとは、すべての可能な記号状態の組み合わせに対して利用可能な遷移規則が少なくとも1つ存在する場合です。状態qは、tからq ( t )への縮小が存在する基底項tが存在する場合にアクセスできます。NFTAは、そのすべての状態にアクセス可能である場合に縮小されます。[8]
ポンピング補題
認識可能な木構造言語Lにおける十分に大きい[9]基底項tは垂直に3分割することができ[10]、中間部分を任意に繰り返しても(「ポンピング」しても)、結果の項はLに保持される。[11] [12]
上記の例のブール値のすべての有限リストの言語では、高さの制限k =2を超えるすべての項は、 consの出現を含む必要があるため、ポンピングできます。たとえば、
すべてその言語に属します。
閉鎖
認識可能な木言語のクラスは、和集合、相補集合、交差集合に関して閉じている。[13]
マイヒル・ネローデ定理
ランク付けされたアルファベットF上のすべての木の集合上の合同性は、すべての f ∈ Fに対して、u 1 ≡ v 1かつ ... かつu n ≡ v nであればf ( u 1 ,..., u n ) ≡ f ( v 1 ,..., v n )となるような同値関係です。同値類の数が有限であれば、それは有限インデックスです。
与えられた木言語Lに対して、各コンテキストCに対してC [ u ] ∈ L ≡ C [ v ] ∈ Lであれば、u ≡ L vによって合同性を定義できます。
ツリーオートマトンにおけるマイヒル・ネローデ定理は、次の3つの文が同値であることを述べている。[14]
- Lは認識可能なツリー言語です
- Lは有限指数の合同の同値類の和集合である。
- 関係≡Lは有限指数の合同である
参照
- クールセルの定理- グラフに関するアルゴリズム的メタ定理を証明するためのツリーオートマトン応用
- ツリー トランスデューサ-ワード トランスデューサがワード オートマトンを拡張するのと同じ方法でツリーオートマトンを拡張します。
- 交代木オートマトン
- 無限木オートマトン
注記
- ^ Comon et al. 2008、セクション1.1、p.20。
- ^ Comon et al. 2008、セクション1.6、p.38。
- ^ Comon et al. 2008、セクション1.1、p.23。
- ^ コモンら。 2008年、宗派。 1.6、定理 1.6.1、p. 38.
- ^ 厳密に言えば、決定論的トップダウンオートマトンがComon et al. (2008) によって定義されていないが、そこで使用されている(セクション1.6、命題1.6.2、p. 38)。それらはパスが閉じた木言語のクラスを受け入れる(セクション1.8、演習1.6、p. 43-44)。
- ^ Morawietz, Frank; Cornell, Tom (1997-07-07). 「オートマトンによる制約の表現」。計算言語学協会第35回年次会議議事録 - ACL '98/ EACL '98。米国: 計算言語学協会。pp. 468–475。doi :10.3115/976909.979677。
- ^ Comon et al. (2008, sect. 1.4, theorem 1.4.3, p. 31-32) のツリー準同型性の概念は、記事「ツリー準同型性」の概念よりも一般的です。
- ^ Comon et al. 2008、セクション1.1、p.23-24。
- ^ 正式には、高さ( t ) > k、ただしk > 0はtではなくLのみに依存する
- ^ 形式的には、コンテキストC [.]、非自明なコンテキストC′ [.] 、およびt = C [ C′ [ u ]]となる基底項u が存在する。「コンテキスト」C [.] は、1 つの穴を持つツリー (または、それに応じて、1 つの変数が 1 回出現する項) である。ツリーが穴ノードのみで構成される場合 (または、それに応じて、項が変数のみである場合)、コンテキストは「自明」であると呼ばれる。表記C [ t ] は、ツリーt をC [.]の穴に挿入した結果(または、それに応じて、変数をtにインスタンス化した結果) を意味する。Comon ら 2008、p. 17 に正式な定義が示されている。
- ^ 正式には、C [ C′ n [ u ]] ∈ L ( n ≥ 0の場合)。C n [.]という表記は、 C [.]をn個重ね合わせた結果を意味します(Comon et al. 2008、p. 17 を参照)。
- ^ Comon et al. 2008、セクション1.2、p.29。
- ^ コモンら。 2008年、宗派。 1.3、定理 1.3.1、p. 30.
- ^ Comon et al. 2008、セクション1.5、p .36。
参考文献
- コモン、ヒューバート。マックス・ドーシェ。ギルロン、レミ。ジャックマール、フィレンツェ;ルギエズ、デニス。レーディング、クリストフ。ティソン、ソフィー。マーク・トンマシ(2008年11月)。ツリー オートマトンの技術と応用。2014 年2 月 11 日に取得。
- 細谷 治夫 (2010 年 11 月 4 日)。XML処理の基礎: ツリーオートマトンアプローチ。ケンブリッジ大学出版局。ISBN 978-1-139-49236-2。
- ゲセグ、フェレンツ;スタインビー、マグナス (1984)。 「ツリーオートマトン」。arXiv : 1509.06233 [cs.FL]。
- Engelfriet, Joost (1975). 「ツリーオートマトンとツリー文法」. arXiv : 1510.02036 [cs.FL].
外部リンク
実装
- Grappa - ランク付けおよびランク付けされていないツリーオートマトンライブラリ (OCaml)
- Timbuk - 到達可能性分析とツリーオートマトン計算のためのツール (OCaml)
- LETHAL - 有限木とヘッジオートマトンを扱うためのライブラリ (Java)
- マシンチェックされたツリーオートマトンライブラリ (Isabelle [OCaml、SML、Haskell])
- VATA - 非決定性ツリーオートマトンを効率的に操作するためのライブラリ (C++)
