数据逻辑可表达性：针对一元与守护二阶逻辑的研究 (Datalog-Expressibility for Monadic and Guarded Second-Order Logic)

from arxiv, Some of the results of this article until Section 5 have been announced in a conference paper with the same title in the proceedings of ICALP'21; the results in Section 6 about nested monadic and nested guarded queries were not yet present in the conference version. The article has been accepted for publication in ACM Transactions of Computational Logic

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.

翻译：我们通过存在性卵石游戏刻画了在有限结构上等价于数据逻辑程序的单子二阶逻辑（MSO）语句。同时证明，对于任何可在MSO中表达且在态射下封闭的有限结构类C，以及任意整数l和k，都存在一个Feder和Verdi意义下宽度为(l,k)的规范数据逻辑程序Π。这些刻画同样适用于严格扩展MSO的守护二阶逻辑（GSO）。为证明这些结果，我们展示了每个补集在态射下封闭的GSO类C都是可数范畴结构的约束满足问题（CSP）的有限并集。已知MSO与数据逻辑的交集包含嵌套单子定义查询（Nemodeq）类；类似地，我们证明GSO与数据逻辑的交集包含所有可通过更具表达力的嵌套守护查询语言表达的问题。然而，通过利用我们的结果，可以证明这两种查询语言均无法作为完整刻画，因为我们构造了一个MSO与数据逻辑交集内的查询，其无法用嵌套守护查询表达。