Logica is an open-source logic programming language that compiles to SQL and runs on DuckDB, SQLite, PostgreSQL, and BigQuery. Unlike classic Datalog, it freely combines recursion and aggregation, concisely expressing algorithms from shortest paths to PageRank. This expressiveness raises semantic challenges: aggregates update by replacement rather than accumulation, evaluation depends on rule scheduling, and programs may converge to meaningful results without reaching a fixpoint, placing them outside traditional fixpoint semantics. We address this with Defendant-Opponent (DO) semantics, a stabilization-based framework for nonmonotonic logic programs. Evaluation is modeled as a rewrite system over derivation states, and a ground atom is true if, from every reachable state, some continuation makes the atom persist in all further derivations. This admits two equivalent characterizations: game-theoretically, truth is what a Defendant can defend against any Opponent in a three-turn game; and modally, truth corresponds to []<>[]t in the derivation graph viewed as a Kripke structure, placing nonmonotonic reasoning within S4. DO semantics coincides with least fixpoint semantics for positive Datalog and is compatible with both Well-Founded and Stable Model Semantics. For programs that converge without a fixpoint, ω-limit interpretations give rigorous meaning to iterative computations such as PageRank.
翻译:Logica是一种开源逻辑编程语言,可编译为SQL并在DuckDB、SQLite、PostgreSQL及BigQuery上运行。与经典Datalog不同,Logica自由结合了递归与聚合,能够简洁地表达从最短路径到PageRank的各类算法。这种表达能力引发了语义层面的挑战:聚合通过替换而非累积进行更新,求值结果依赖于规则调度,程序在没有达到不动点的情况下仍可能收敛至有意义的结果,从而超出传统不动点语义的适用范围。为此,我们提出被告-对手(DO)语义——一种针对非单调逻辑程序的稳定化框架。求值过程被建模为基于推导状态的重写系统,当从所有可达状态出发均存在某个延续方案使得原子命题在所有后续推导中持续成立时,该接地原子被视为真。该定义具有两种等价刻画:在博弈论层面,真即被告在三人博弈中能够针对任意对手捍卫的结论;在模态逻辑层面,真对应于将推导图视为克里普克结构时的[]<>[]t公式,从而将非单调推理纳入S4模态系统。DO语义对正Datalog程序与最小不动点语义完全一致,并与良基语义及稳定模型语义兼容。对于收敛于非不动点的程序,ω-极限解释为PageRank等迭代计算提供了严谨的语义基础。