Semantical evaluations as monadic second-order compatible structure transformations

Abstract

A transformation of structures τ is monadic second-order compatible (MS-compatible) if every monadicsec ond-order property P can be effectively rewritten into a monadic second-order property Q such that, for every structure S, if T is the transformed structure τ (S), then P(T) holds iff Q(S) holds. We will review Monadic Second-order definable transductions (MS-transductions): they are MS-compatible transformations of a particular form, i.e., defined by monadicsec ond-order (MS) formulas. The unfolding of a directed graph into a tree is an MS-compatible transformation that is not an MS-transduction. The MS-compatibility of various transformations of semantical interest follows. We will present three main cases and discuss applications and open problems.