An Algorithm for Comparing Deterministic Regular Tree Grammars

An algorithm to decide inclusion for languages defined by deterministic regular tree grammars is presented. The algorithm is shown to run in polynomial time based on the number of constructors, constructor arity, and number of non-terminals. Correctness proofs are included. 1 Regular tree grammars A regular tree grammar, G, is a grammar for constructing trees. Formally, G = (C; N;P;S) where: 1. C is a finite, non-empty set of constructors. Each constructor c n is of arity n. Constants are 0-arity constructors. 2. N is a finite, non-empty set of non-terminals where N " C = ;. 3. P is a finite set of productions of the form A ! c n (X 1 ; : : : ; X n ) where A is a non-terminal, c n is a constructor, and each X i is a non-terminal. If the constructor is a constant, then we write c 0 as a shorthand for c 0 (). 4. S is a special element of N called the start symbol. A regular tree is constructed from a regular tree grammar in the following manner: 1. If A is a non-terminal, th..