Regular tree grammar

Derivation of trees

The grammar G implicitly defines a set of trees: any tree that can be derived from Z using the rule set P is said to be described by G. This set of trees is known as the language of G. Formally, the relation ⇒_G on the set T_Σ(N) is defined as follows:

A tree t₁∈ T_Σ(N) can be derived in a single step into a tree t₂ ∈ T_Σ(N) (in short: t₁ ⇒_G t₂), if there is a context S and a production (A→t) ∈ P such that:

• t₁ = S[A], and
• t₂ = S[t].

Here, a context means a tree with exactly one hole in it; if S is such a context, S[t] denotes the result of filling the tree t into the hole of S.

The tree language generated by G is the language L(G) = { t ∈ T_Σ | Z ⇒_G* t }.

Here, T_Σ denotes the set of all trees composed from symbols of Σ, while ⇒_G* denotes successive applications of ⇒_G.

A language generated by some regular tree grammar is called a regular tree language.

Examples

Let G₁ = (N₁,Σ₁,Z₁,P₁), where

• N₁ = {Bool, BList } is our set of nonterminals,
• Σ₁ = { true, false, nil, cons(.,.) } is our ranked alphabet, arities indicated by dummy arguments (i.e. the symbol cons has arity 2),
• Z₁ = BList is our starting nonterminal, and
• the set P₁ consists of the following productions:
  • Bool → false
  • Bool → true
  • BList → nil
  • BList → cons(Bool,BList)

An example derivation from the grammar G₁ is

BList ⇒ cons(Bool,BList) ⇒ cons(false,cons(Bool,BList)) ⇒ cons(false,cons(true,nil)).

The image shows the corresponding derivation tree; it is a tree of trees (main picture), whereas a derivation tree in word grammars is a tree of strings (upper left table).

The tree language generated by G₁ is the set of all finite lists of boolean values, that is, L(G₁) happens to equal T_Σ1. The grammar G₁ corresponds to the algebraic data type declarations (in the Standard ML programming language):

<span id="mwvQ"></span><span class="kr" id="mwvg">datatype</span> <span class="kt" id="mwvw">Bool</span> <span class="p" id="mwwA">=</span> <span class="nc" id="mwwQ">false</span> <span class="p" id="mwwg">|</span> <span class="nc" id="mwww">true</span> <span class="kr" id="mwxA">datatype</span> <span class="kt" id="mwxQ">BList</span> <span class="p" id="mwxg">=</span> <span class="nc" id="mwxw">nil</span> <span class="p" id="mwyA">|</span> <span class="nc" id="mwyQ">cons</span> <span class="kr" id="mwyg">of</span> <span class="n" id="mwyw">Bool</span> <span class="n" id="mwzA">*</span> <span class="n" id="mwzQ">BList</span>

Every member of L(G₁) corresponds to a Standard-ML value of type BList.

For another example, let G₂ = (N₁, Σ₁, BList₁, P₁ ∪ P₂), using the nonterminal set and the alphabet from above, but extending the production set by P₂, consisting of the following productions:

• BList₁ → cons(true,BList)
• BList₁ → cons(false,BList₁)

The language L(G₂) is the set of all finite lists of boolean values that contain true at least once. The set L(G₂) has no datatype counterpart in Standard ML, nor in any other functional language. It is a proper subset of L(G₁). The above example term happens to be in L(G₂), too, as the following derivation shows:

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

Language properties

If L₁, L₂ both are regular tree languages, then the tree sets L₁ ∩ L₂, L₁ ∪ L₂, and L₁ \ L₂ are also regular tree languages, and it is decidable whether L₁ ⊆ L₂, and whether L₁ = L₂.

Alternative characterizations and relation to other formal languages

• Regular tree grammars are a generalization of regular word grammars.
• The regular tree languages are also the languages recognized by bottom-up tree automata and nondeterministic top-down tree automata.
• Rajeev Alur and Parthasarathy Madhusudan related a subclass of regular binary tree languages to nested words and visibly pushdown languages.

Applications

Applications of regular tree grammars include:

• Instruction selection in compiler code generation
• A decision procedure for the first-order logic theory of formulas over equality (=) and set membership (∈) as the only predicates
• Solving constraints about mathematical sets
• The set of all truths expressible in first-order logic about a finite algebra (which is always a regular tree language)
• Graph-search