We characterise the sentences in Monadic Second-order Logic (MSO) that are over finite structures equivalent to a Datalog program, in terms of an existential pebble game. We also show that for every class C of finite structures that can be expressed in MSO and is closed under homomorphisms, and for all integers l,k, there exists a canonical Datalog program Pi of width (l,k) in the sense of Feder and Verdi. The same characterisations also hold for Guarded Second-order Logic (GSO), which properly extends MSO. To prove our results, we show that every class C in GSO whose complement is closed under homomorphisms is a finite union of constraint satisfaction problems (CSPs) of countably categorical structures. The intersection of MSO and Datalog is known to contain the class of nested monadically defined queries (Nemodeq); likewise, we show that the intersection of GSO and Datalog contains all problems that can be expressed by the more expressive language of nested guarded queries. Yet, by exploiting our results, we can show that neither of the two query languages can serve as a characterization, as we exhibit a query in the intersection of MSO and Datalog that is not expressible in nested guarded queries.

翻译：我们通过存在性卵石游戏刻画了在有限结构上等价于Datalog程序的一元二阶逻辑（MSO）语句。同时证明：对于任何可在MSO中表达且在同态下封闭的有限结构类C，以及任意整数l,k，总存在Feder与Verdi意义下宽度为(l,k)的规范Datalog程序Π。该刻画同样适用于严格扩展MSO的守卫二阶逻辑（GSO）。为证明结论，我们首先论证：任何补集在同态下封闭的GSO类C，均可表示为可数范畴结构的约束满足问题（CSP）之有限并。已知MSO与Datalog的交集包含嵌套一元可定义查询类（Nemodeq）；类似地，我们证明GSO与Datalog的交集包含所有可通过表达能力更强的嵌套守卫查询语言表达的问题。然而，基于所得结论可进一步证明：这两种查询语言均无法构成完全刻画——我们构造了一个属于MSO与Datalog交集却无法用嵌套守卫查询表达的查询实例。