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. 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. 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 t1∈ TΣ(N) can be derived in a single step into a tree t2 ∈ TΣ(N) (in short: t1 ⇒G t2), if there is a context S and a production (A→t) ∈ P such that: t1 = S[A], and t2 = 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) = . 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. Let G1 = (N1,Σ1,Z1,P1), where N1 = {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), Z1 = BList is our starting nonterminal, and the set P1 consists of the following productions: Bool → false Bool → true BList → nil BList → cons(Bool,BList) An example derivation from the grammar G1 is BList ⇒ cons(Bool,BList) ⇒ cons(false,cons(Bool,BList)) ⇒ cons(false,cons(true,nil)).