Diamonds Are Forever: Stabilization Semantics for Unrestricted Aggregation and Recursion in Logica

Abstract

Logica is an open-source logic programming language that compiles to SQL and runs on platforms including DuckDB, SQLite, PostgreSQL, and BigQuery. Unlike classic Datalog, Logica permits the free combination of recursion and aggregation, enabling concise formulations of algorithms from shortest paths to PageRank. This expressiveness introduces fundamental semantic challenges: aggregate predicates are updated by replacement rather than accumulation, evaluation is sensitive to rule scheduling, and programs may converge to meaningful results without ever reaching a fixpoint, placing them outside the scope of traditional fixpoint semantics. We address these challenges with Defendant-Opponent (DO) semantics , a stabilization-based framework for nonmonotonic logic programs. Program evaluation is modeled as a rewrite system over derivation states. A ground atom is true if, from every reachable state, there exists a continuation after which the atom persists in all further derivations. This notion admits two equivalent characterizations: (1) game-theoretically, truth is what a Defendant can defend against any Opponent in a three-turn derivation game; and (2) modally, a formula

is a theorem precisely when the condition

white medium square lozenge white medium square t ◻ ◊ ◻ t $\Box \mkern 1.33mu{\LARGE \Diamond }\Box \mkern 1.33mu\,t$

holds in the derivation graph viewed as a Kripke structure. We show that DO semantics coincides with classic least fixpoint semantics for positive Datalog programs and is compatible with both the Well-Founded Semantics (the two never disagree on definite answers) and the Stable Model Semantics (every stable model is a DO interpretation). For programs that converge without reaching a fixpoint, we introduce

omega ω $\omega$

-limit interpretations, giving rigorous meaning to iterative computations such as PageRank. DO semantics thus offers a coherent framework that complements existing logic programming semantics while supporting recursive aggregation.