Weighted Tree Automata -- May it be a little more?

TL;DR

This work presents a comprehensive, proof-rich development of weighted tree automata (wta) over strong bimonoids, unifying automata-theoretic and universal-algebraic perspectives. It clarifies two distinct semantics for wta—the run semantics $[ abla run]$ and the initial-algebra semantics $[ abla init]$—and analyzes when they coincide (e.g., under bottom-up-determinism or semiring conditions) or diverge. The book builds a broad framework: preliminaries on algebras, lattices, and semimodules; detailed structures for nested polynomials and free strong bimonoids; representations of trees, tree grammars, and matrices; and a wide range of results including pumping lemmas, normal forms, determinization, and connections to weighted context-free/regular tree grammars and weighted MSO logic. It also develops decomposition results, monoid-representation characterizations, and dual viewpoints via fta-hypergraphs, yielding a robust theory with deep connections to formal languages, algebra, and logic. The work advances both foundational theory and potential applications in areas such as natural language processing, by delivering rigorous tools for analyzing and transforming weighted tree languages over diverse weight structures.

Abstract

This is a book on weighted tree automata. We present the basic definitions and some of the important results in a coherent form with full proofs. The concept of weighted tree automata is part of Automata Theory and it touches the area of Universal Algebra. It originated from two sources: weighted string automata and finite-state tree automata.

Figures (104)

• Figure 1: Overview of the models of automata and models of grammars which occur in this book. Their relationship is expressed by arrows. For every pair $(X,Y)$ of models, if $X \rightarrow Y$, then $Y$ is a special case of $X$, and if $X \leftrightarrow Y$, then $X$ and $Y$ are equivalent. wta: weighted tree automaton wcfg: weighted context-free grammar wsa: weighted string automaton wrtg: weighted regular tree grammar fta: finite-state tree automaton cfg: context-free grammar fsa: finite-state string automaton wpb: weighted projective bimorphism $\Sigma$, $\Psi$: ranked alphabets $\Gamma$: alphabet $\mathsf{B}$: strong bimonoid rhs: right-hand side
• Figure 2: A finite part of the Hasse diagram for $A = (\mathbb{N} \times \mathbb{N})$ and $(n_1,n_2) \le (k_1,k_2)$ if $n_1 \le k_1$ and $n_2 \le k_2$.
• Figure 3: The Venn diagram (left) and the Euler diagram (right) for $U = \{a,b,c\}$ and $A = \{\{a\}, \{a,b\}, \{b,c\}\}$.
• Figure 4: Illustration of the index $i(b)$ and the period $p(b)$ of $b$ (cf. fulkosvog19).
• Figure 5: (a) Example of an expression over the operations $\oplus$ and $\otimes$ and unit elements $\mathbb{0}$ and $\mathbb{1}$ of $\mathsf{B}$ and the variables $x_1,x_2,x_3$; each of the three dashed ellipses stands for a maximal pattern of $\oplus$-occurrences or a maximal pattern of $\otimes$-occurrences; and (b) the corresponding nested polynomial where each nontrivial finite multiset $M$ is denoted by a pair in square brackets with the vertical list of $(\mathrm{value} \mapsto \mathrm{multiplicity})$-relationships of $M$ inside (where the unit element $\mathbb{0}$ is disregarded), and each nontrivial finite sequence $(c_1,\ldots,c_n)$ is presented by itself (except that the unit element $\mathbb{1}$ is disregarded).

Theorems & Definitions (837)

• Lemma 2.5.2
• proof
• Lemma 2.5.3
• proof
• Corollary 2.5.4
• proof
• Corollary 2.5.5
• proof
• Corollary 2.5.6
• proof