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)).