Datalog-Expressibility for Monadic and Guarded Second-Order Logic

TL;DR

This paper characterizes which Monadic and Guarded Second-order Logic sentences over finite structures can be expressed as Datalog programs, establishing connections with pebble games, CSPs, and query expressiveness.

Contribution

It provides a logical and combinatorial characterization of MSO and GSO sentences equivalent to Datalog, extending known results and introducing new canonical program constructions.

Findings

Characterization of MSO sentences equivalent to Datalog via pebble games

Existence of canonical Datalog programs for MSO classes closed under homomorphisms

Demonstration that certain queries in MSO∩Datalog are not expressible in nested guarded queries

Abstract

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.