Visibly Pushdown Languages and Term Rewriting

Jacques Chabin and Pierre Rety

Abstract :

To combine tree languages with term rewriting, we introduce a new class of tree
languages, that both extends regular languages and restricts context-free languages,
and that is closed under intersection (unlike context-free languages).
To do it, we combine the concept of visibly pushdown language,
with top-down pushdown tree automata, and we get the visibly pushdown tree automata.
Then, we use them to express the sets of descendants for
a sub-class of growing term rewrite systems, and thanks to closure under
intersection, we get that joinability and (restricted) unifiability are decidable.