Feature automata and recognizable sets of feature trees

Abstract

Feature trees generalize first-order trees whereby argument positions become keywords (“features”) from an infinite symbol set F. Constructor symbols can occur with any argument positions, in any finite number. Feature trees are used to model flexible records; the assumption on the infiniteness of F accounts for dynamic record field updates. We develop a universal algebra framework for feature trees. We introduce the classical set-defining notions: automata, regular expressions and equational systems, and show that they coincide. This extension of the regular theory of trees requires new notions and proofs. Roughly, a feature automaton reads a feature tree in two directions: along its branches and along the fan-out of each node. We illustrate the practical motivation of our regular theory of feature trees by pointing out an application on the programming language LIFE.