Symbolic Weighted Language Models, Quantitative Parsing and Verification over Infinite Alphabets

We study properties and relationship between three classes of quantitative language models computing over infinite input alphabets: Symbolic Weighted Automata (swA) at the joint between Symbolic Automata (sA) and Weighted Automata (wA), as well as Transducers (swT) and Visibly Pushdown (sw-VPA) variants. Like sA, swA deal with large or infinite input alphabets, and like wA, they output a weight value in a semiring domain. The transitions of swA are labeled by functions from an infinite alphabet into the weight domain. This generalizes sA, whose transitions are guarded by Boolean predicates overs symbols in an infinite alphabet, and also wA, whose transitions are labeled by constant weight values, and which deal only with finite alphabets. We present a Bar-Hillel Perles Shamir construction of a swA computing a swT-defined distance between a swA input language and a word, some closure results and a polynomial best-search algorithm for sw-VPA. These results are applied to solve a variant of parsing over infinite alphabets.