Automate d'arbres

En informatique théorique, plus précisément en théorie des langages, un automate d'arbre est une machine à états qui prend en entrée un arbre, plutôt qu'une chaîne de caractères pour les automates plus conventionnels, comme les automates finis. Comme pour les automates classiques, les automates d'arbres finis (FTA pour finite tree automata en anglais) peuvent être déterministes ou pas. Suivant la façon dont les automates se « déplacent » sur l'arbre qu'ils traitent, les automates d'arbres peuvent être de deux types : (a) ascendants ; (b) descendants. La distinction est importante, car si les automates non déterministes (ND) ascendants et descendants sont équivalents, les automates déterministes descendants sont strictement moins puissants que leurs homologues déterministes ascendants. En effet, les propriétés d'arbres spécifiées par les automates déterministes descendants ne peuvent dépendre que des propriétés de chemins. Un alphabet gradué (ranked alphabet en anglais) est un alphabet muni d'une fonction qui, à chaque symbole de , associe un entier naturel qui est son arité (le nombre d'arguments qu'elle requiert). On considère les constantes comme des opérateurs nullaires (i.e. d'arité 0). Parfois, l'ensemble des symboles d'arité 0 est partagé en deux sous-ensembles, les constantes et les variables. Un alphabet gradué est donc une signature (ensemble de symboles de constante, de fonction et de relation), considérée comme indépendante de l'algèbre sur laquelle elle agit éventuellement. Étant donné un alphabet gradué , les termes (de base) ou arbres sur sont définis comme suit : Un symbole de d'arité 0 est un terme ; Si est un symbole d'arité , et si sont des termes, alors la suite est un terme ; ce terme est généralement noté ; Tout terme s'obtient, à partir des symboles d'arité 0, par un nombre fini d'applications de la règle précédente. On peut voir un terme comme un arbre. La racine de l'arbre a pour étiquette le symbole , et les enfants de la racine sont les termes . Un terme clos est un terme sans variable.