Regular cost functions. I: Logic and algebra over words (Q2846575)

Consider functions mapping (finite) words over an alphabet to natural numbers or the value \(\infty\). Two such functions \(f\) and \(g\) are equivalent if, for all sets \(X\) of words, \(f\) restricted to \(X\) is bounded iff \(g\) restricted to \(X\) is bounded. A \textit{cost function} is an equivalence class of this relation. This can be seen as a generalization of the theory of formal languages by identifying a language \(L\) with the function mapping each element of \(L\) to \(0\) and each other word to \(\infty\). Cost automata are finite automata that can count (with possible resets) the number of occurrences of a special state during the run on a word. Regularity now means that the cost function can be computed by a cost automaton. This notion can equivalently be stated in terms of certain closure operations or in algebraic terms making use of so-called stabilization monoids. The content of the present paper is a characterization of regular cost functions using ``cost monadic logic'', the extension of monadic second-order logic by the ability to express that a certain monadic variable has cardinality bounded by some non-negative integer.