This paper contributes to the mathematical foundations of logic programming by introducing and studying the sequential composition of answer set programs. On the semantic side, we show that the immediate consequence operator of a program can be represented via composition, which allows us to compute the least model semantics of Horn programs without any explicit reference to operators. As a result, we can characterize answer sets algebraically, which further provides an algebraic characterization of strong and uniform equivalence which is appealing. This bridges the conceptual gap between the syntax and semantics of an answer set program in a mathematically satisfactory way. The so-obtained algebraization of answer set programming allows us to transfer algebraic concepts into the ASP-setting which we demonstrate by introducing the index and period of an answer set program as an algebraic measure of its cyclicality. The technical part of the paper ends with a brief section introducing the algebraically inspired novel class of aperiodic answer set programs strictly containing the acyclic ones. In a broader sense, this paper is a first step towards an algebra of answer set programs and in the future we plan to lift the methods of this paper to wider classes of programs, most importantly to higher-order and disjunctive programs and extensions thereof.
翻译:本文通过引入并研究答案集程序的顺序复合,为逻辑程序的数学基础做出了贡献。在语义层面,我们证明了程序的直接后果算子可以通过复合运算表示,这使得我们能够在不显式引用算子的情况下计算Horn程序的最小模型语义。由此,我们可以从代数角度刻画答案集,进而为强等价与一致等价提供具有吸引力的代数表征。这以数学上令人满意的方式弥合了答案集程序语法与语义之间的概念鸿沟。所获得的答案集编程代数化使我们能够将代数概念迁移至ASP框架中,我们通过引入答案集程序的指数与周期作为其循环性的代数度量来展示这一点。本文的技术部分以简要介绍一类受代数启发的新型非周期答案集程序作为结束,该类程序严格包含非循环程序。从更广泛的意义上说,本文是迈向答案集程序代数的第一步,未来我们计划将本文方法推广至更广泛的程序类别,尤其是高阶程序、析取程序及其扩展。