Evaluation order and nontermination in query languages
Explores how evaluation order impacts nontermination in Datalog and SQL query languages, comparing strategies like naive, semi-naive, and top-down evaluation, and noting that recursive queries can cause infinite loops despite theoretical termination guarantees.
Background
Datalog is a declarative logic programming language used in databases, static analysis, and knowledge representation. Unlike SQL, Datalog is widely believed to always terminate. This post challenges that assumption, showing that termination depends on **evaluation order**: how the engine schedules rule evaluation. Top-down (Prolog-style) evaluation can loop forever on certain recursive rules, while bottom-up evaluation always terminates but can be slower. Modern Datalog engines (Soufflé, Datomic, Flix) often mix strategies for performance, meaning real-world queries may sometimes not terminate. The post traces this to classic results in logic programming (the "occur check" and "negation-as-failure").