Tree grammars

Terms will be viewed as rooted, ordered, node-labeled trees in the obvious way. All inner nodes carry (non-nullary) operators from Σ,while leaf nodes carry nullary operators or symbols from the alphabet Α. A term/tree with variables is called a tree pattern. A tree containing a designated occurence of a subtree t is denoted C[...t...].

A tree language over Σ is a subset of T_Σ. Tree languages are described by tree grammars, which can be defined in analogy to the Chomsky hierachy of string grammars. Here we use regular tree grammars originally studied in [Brae69]. In [GS88] they were redefined to specify term languages over some signature. Our further specialization so far lies solely in the distinguished role of Α.

Definition (Tree grammar over Σ and Α):

A regular tree grammar

**G**over Σ and Α is given by- a set V of nonterminal symbols
- a designated nonterminal symbol Ax called the axiom
- a set P of productions of the form v -> t, where v ∈ V and t ∈ T_Σ(V)

**L(v)**= {t ∈ T_Σ | v ->* t}, the language of G is**L(G)**= L(Ax).
For convenience, we add a lexical level to the grammar concept, allowing strings from A* in place of single symbols. By convention, achar denotes an arbitrary character, char c a specific character c, string an arbitrary string and empty the empty input. Also for brevity, we allow syntactic conditions associated with righthand sides.