# Regular tree grammar

In theoretical computer science and formal language theory, a regular tree grammar is a formal grammar that describes a set of directed trees, or terms. A regular word grammar can be seen as a special kind of regular tree grammar, describing a set of single-path trees.

## Definition

A regular tree grammar G is defined by the tuple
G = (N, Σ, Z, P),
where
* N is a finite set of nonterminals,
* Σ is a ranked alphabet (i.e., an alphabet whose symbols have an associated arity) disjoint from N,
* Z is the starting nonterminal, with Z ∈ N, and
* P is a finite set of productions of the form A → t, with A ∈ N, and t ∈ T$_Σ$(N), where T$_Σ$(N) is the associated term algebra, i.e. the set of all trees composed from symbols in Σ ∪ N according to their arities, where nonterminals are considered nullary.

## 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. More formally, the relation ⇒$_G$ on the set T$_Σ$(N) is defined as follows:
A tree t$_1$∈ T$_Σ$(N) can be derived in a single step into a tree t$_2$ ∈ T$_Σ$(N) (in short: t$_1$ ⇒$_G$ t$_2$), if there is a context S and a production (A→t) ∈ P such that:
* t$_1$ = S[A], and
* t$_2$ = 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$_1$ = (N$_1$,Σ$_1$,Z$_1$,P$_1$), where
* N$_1$ = {Bool, BList } is our set of nonterminals,
* Σ$_1$ = { true, false, nil, cons(.,.) } is our ranked alphabet, arities indicated by dummy arguments (i.e. the symbol cons has arity 2),
* Z$_1$ = BList is our starting nonterminal, and
* the set P$_1$ consists of the following productions:
** Bool → false
** Bool → true
** BList → nil
** BList → cons(Bool,BList)
An example derivation from the grammar G$_1$ 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$_1$ is the set of all finite lists of boolean values, that is, L(G$_1$) happens to equal T$_{Σ1}$. The grammar G$_1$ corresponds to the algebraic data type declarations (in the Standard ML programming language):
Every member of L(G$_1$) corresponds to a Standard-ML value of type BList.
For another example, let G$_2$ = (N$_1$, Σ$_1$, BList$_1$, P$_1$ ∪ P$_2$), using the nonterminal set and the alphabet from above, but extending the production set by P$_2$, consisting of the following productions:
* BList$_1$ → cons(true,BList)
* BList$_1$ → cons(false,BList$_1$)
The language L(G$_2$) is the set of all finite lists of boolean values that contain true at least once. The set L(G$_2$) has no datatype counterpart in Standard ML, nor in any other functional language. It is a proper subset of L(G$_1$). The above example term happens to be in L(G$_2$), too, as the following derivation shows:
BList$_1$ ⇒ cons(false,BList$_1$) ⇒ cons(false,cons(true,BList)) ⇒ cons(false,cons(true,nil)).

## Language properties

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

## 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