正規木文法

理論計算機科学と形式言語理論において、正規木文法は、有向木または項の集合を記述する形式文法である。^[1]正規単語文法は、単一パス木の集合を記述する、特別な種類の正規木文法と見なすことができます。

正規木文法Gはタプルによって定義される

G = ( N , Σ, Z , P )、

どこ

• Nは非終端記号の有限集合であり、
• Σ はNと素な順位付きアルファベット（つまり、その記号が関連するアリティを持つアルファベット）であり、
• Z は開始非終端記号であり、Z ∈ Nであり、
• P はA → tの形式の生成規則の有限集合であり、 A ∈ N かつ t ∈ T Σ ( N ) です。ここで、 T Σ ( N ₎は関連する項代数_、つまりΣ ∪ N内の記号からその引数の数に応じて構成されるすべての木の集合であり、非終端記号はヌル引数とみなされます。

文法G は暗黙的に木の集合を定義します。つまり、規則集合P を使用してZから導出できる木はすべてGによって記述されると言えます。この木の集合はGの言語として知られています。より正式には、集合T _Σ ( N ) 上の関係 ⇒ _Gは次のように定義されます。

木t ₁ ∈ T _Σ ( N )は、コンテキストSと生成規則( A → t ) ∈ Pが存在し、次の条件を満たす場合、1ステップで木t 2 ∈ _T Σ ( _N ) (つまり 、t ₁ ⇒ _G t ₂ )に導出できます。

• t ₁ = S [ A ]であり、
• t ₂ = S [ t ] です。

ここで、コンテキストとは、ちょうど 1 つの穴があるツリーを意味します。Sがそのようなコンテキストである場合、S [ t ] はツリーt をSの穴に埋め込んだ結果を表します。

Gによって生成さ_れる木言語は言語L ( G )={ _t∈TΣ | Z⇒G * t _}である 。

ここで、T _ΣはΣの記号から構成されるすべての木の集合を表し、⇒G _*は⇒Gの連続的な適用を表します。

何らかの正規木文法によって生成された言語は正規木言語と呼ばれます。

G ₁ = ( N ₁ ,Σ ₁ , Z ₁ , P ₁ ) とします。ここで

• N ₁ = { Bool , BList } は非終端記号の集合であり、
• Σ ₁ = { true , false , nil , cons (.,.) } は順位付けされたアルファベットで、引数はダミー引数で示されます（つまり、シンボルcons の引数は 2 です）。
• Z ₁ = BListは最初の非終端記号であり、
• 集合P1_は次の生成規則から構成される。
  • ブール値→ false
  • ブール値→真
  • BList →なし
  • BList →短所( Bool , BList )

文法G ₁からの導出の例は次の通りである。

BList ⇒ cons ( Bool、BList ) ⇒ cons ( false、cons ( Bool、BList )) ⇒ cons ( false、cons ( true、nil ))。

画像は対応する導出ツリーを示しています。これはツリーのツリー (メイン画像) ですが、単語文法の導出ツリーは文字列のツリー (左上の表) です。

G ₁によって生成されるツリー言語は、ブール値のすべての有限リストの集合です。つまり、L ( G _{1 ) は}T _Σ1に等しくなります。文法G _{1は、代数データ型宣言 (}標準 MLプログラミング言語)に対応します。

  データ型 Bool 
    =  false 
    |  true
  データ型 BList 
    =  nil 
    |  Bool * BListのcons    

L ( G1 )の各メンバーは_、 BList型のStandard-ML値に対応します。

別の例として、非終端記号集合と上記のアルファベットを使用し、生成規則集合をP _{2で拡張して、} G ₂ = ( N ₁ , Σ ₁ , BList ₁ , P ₁ ∪ P ₂ )とします。これは、次の生成規則で構成されます。

• BList ₁ →短所( true , BList )
• BList ₁ →短所( false、BList ₁ )

言語L ( G ₂ ) は、少なくとも 1 回はtrue を含むブール値の有限リストすべての集合です。集合L ( G _{2 ) には、標準 ML にも他の関数型言語にも対応する}データ型はありません。これはL ( G ₁ )の適切な部分集合です。次の導出が示すように、 上記の例の用語はL ( G ₂ )にも存在します。

BList ₁ ⇒ cons ( false , BList ₁ ) ⇒ cons ( false , cons ( true , BList )) ⇒ cons ( false , cons ( true , nil ))。

L ₁、L _{2 が}両方とも正規木言語である場合、木集合L ₁ ∩ L ₂、L ₁ ∪ L ₂、およびL ₁ \ L _{2も正規木言語であり、} L ₁ ⊆ L ₂であるかどうか、およびL ₁ = L ₂であるかどうかは決定可能です。

• 正規木文法は正規単語文法の一般化です。
• 正規木言語は、ボトムアップ木オートマトンと非決定性トップダウン木オートマトンによって認識される言語でもある。^[2]
• Rajeev AlurとParthasarathy Madhusudanは、正規二分木言語のサブクラスをネストされた単語と視覚的にプッシュダウンする言語に関連付けました。^{[3] [4]}

正規木文法の応用例には以下のものがあります。

• コンパイラコード生成における命令選択^[5]
• 等式（＝）と集合の帰属関係（∈）のみを述語とする一階論理理論の決定手順[ ^6]
• 数学的集合に関する制約の解決^[7]
• 有限代数（常に正規木言語）に関する一階述語論理で表現可能なすべての真理の集合^[8]
• グラフ検索^[9]

• 集合制約– 正規木文法の一般化
• 木結合文法

• 正規木文法は 1968 年にすでに次のように記述されていました。
  • Brainerd, WS (1968). 「ツリーオートマトン最小化」.情報と制御. 13 (5): 484–491. doi : 10.1016/s0019-9958(68)90917-0 . hdl : 10945/40204 .
  • Thatcher, JW; Wright, JB (1968). 「一般化された有限オートマトン理論と、2 階論理の決定問題への応用」.数学システム理論. 2 (1): 57–81. doi :10.1007/BF01691346. S2CID  31513761.
• ツリー文法に特化した書籍としては、Nivat, Maurice、Podelski, Andreas (1992)、「Tree Automata and Languages . Studies in Computer Science and Artificial Intelligence. Vol. 10. North-Holland」があります。
• 正規木文法のアルゴリズムは、効率重視の観点から、次の文献で説明されています: Aiken, A.; Murphy, B. (1991). 「Implementing Regular Tree Expressions」. ACM Conference on Functional Programming Languages and Computer Architecture . pp. 427–447. CiteSeerX 10.1.1.39.3766 . 
• ツリーから重みへのマッピングが与えられれば、ドナルド・クヌースによるダイクストラの最短経路アルゴリズムの一般化を正規ツリー文法に適用して、各非終端記号について導出可能なツリーの最小重みを計算できます。この情報に基づいて、重みの昇順で言語を列挙するのは簡単です。特に、最小重みが無限の非終端記号は、空の言語を生成します。参照: Knuth, DE (1977). "A Generalization of Dijkstra's Algorithm". Information Processing Letters . 6 (1): 1–5. doi :10.1016/0020-0190(77)90002-3.
• 通常のツリー オートマトンが一般化され、ツリー内の兄弟ノード間の等価性テストが可能になりました。参照: Bogaert, B.、Tison, Sophie (1992)。「ツリー オートマトンにおける直接部分項の等価性および不等性制約」。Proc . 9th STACS . LNCS. Vol. 577. Springer. pp. 161–172。
• より深いノード間の等価性テストを許可すると、決定不能が生じます。参照: Tommasi, M. (1991)。Cousins Germains での Arbres avec Tests d'Égalités を自動化します。ライフイット。