Algorithmic uses of the Feferman-Vaught theorem (Q598280): Difference between revisions

The author gives a unified presentation, including new results, of how to use the Feferman-Vaught theorem, and new variations thereof, algorithmically in the case of Monadic Second-Order Logic MSOL. The introduction contains a survey of results in the considered direction. The formalism of translation schemes and its associated maps, the semantic transductions and syntactic translations are introduced. Translation schemes unify formalisms due to Tarski, Mostowski and Robinson and clarified by Rabin. A unary map between structures, the fusion, is introduced. It contracts the satisfaction set of a unary predicate to a single point. This operation satisfies a variant of the Feferman-Vaught theorem. In its full generality it is not known to be expressible as a first-order logic transduction. However, several special cases can be expressed in this way. A formalism of MSOL-inductive classes is presented. These are classes of structures built inductively using the disjoint union, quantifier-free transductions, and the fusion operation. It is shown how to construct lookup tables for reduction sequences associated with these operations, and how to use them for linear-time model checking of structures represented as parse trees of inductive classes. The author introduces graph polynomials and defines the class of MSOL-definable graph polynomials. He proves a Feferman-Vaught theorem for MSOL-definable graph polynomials, generalizes known and generates new splitting theorems for graph polynomials, and how they can be used for calculations. Finally the author discusses extensions of MSOL for which the Feferman-Vaught theorem holds as well.