The Power of Negation in Higher-Order Datalog

TL;DR

This paper explores the expressive power of Higher-Order Datalog with negation, revealing how increasing order affects complexity classes under different semantics, and establishing a hierarchy of logical expressiveness.

Contribution

It provides a detailed characterization of Higher-Order Datalog$^ eg$'s expressive power under well-founded and stable model semantics, linking it to complexity classes and demonstrating a hierarchy.

Findings

Higher-Order Datalog$^ eg$ captures k-EXP under well-founded semantics.

It captures co-(k-NEXP) under stable model semantics.

Expressive power increases with order, revealing a hierarchy.

Abstract

We investigate the expressive power of Higher-Order Datalog$^\neg$ under both the well-founded and the stable model semantics, establishing tight connections with complexity classes. We prove that under the well-founded semantics, for all $k\geq 1$, $(k+1)$-Order Datalog$^\neg$ captures k-EXP, a result that holds without explicit ordering of the input database. The proof of this fact can be performed either by using the powerful existential predicate variables of the language or by using partially applied relations and relation enumeration. Furthermore, we demonstrate that this expressive power is retained within a stratified fragment of the language. Under the stable model semantics, we show that $(k+1)$-Order Datalog$^\neg$ captures co-(k-NEXP) using cautious reasoning and k-NEXP using brave reasoning, again with analogous results for the stratified fragment augmented with choice rules. Our results establish a hierarchy of expressive power, highlighting an interesting trade-off between order and non-determinism in the context of higher-order logic programming: increasing the order of programs under the well-founded semantics can surpass the expressive power of lower-order programs under the stable model semantics.