Table of Contents
Fetching ...

Sequential composition of answer set programs

Christian Antić

TL;DR

This work develops an algebraic foundation for answer set programming by introducing sequential composition of ASPs. It shows that the space of all answer set programs forms a finite unital magma under composition with unit $1$, enabling an algebraic interpretation of semantic operators and equivalences. By defining auxiliary constructions like $tf$, $\overline{P}$, and $P^{\lor}$, the authors connect syntax and semantics, and they further identify a restricted Krom-Horn subclass that forms an idempotent semiring. The paper also develops concepts of index and period to measure cyclicality, constructs aperiodic programs, and outlines rich future directions including higher-order, disjunctive extensions, and program synthesis within this algebraic framework.

Abstract

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.

Sequential composition of answer set programs

TL;DR

This work develops an algebraic foundation for answer set programming by introducing sequential composition of ASPs. It shows that the space of all answer set programs forms a finite unital magma under composition with unit , enabling an algebraic interpretation of semantic operators and equivalences. By defining auxiliary constructions like , , and , the authors connect syntax and semantics, and they further identify a restricted Krom-Horn subclass that forms an idempotent semiring. The paper also develops concepts of index and period to measure cyclicality, constructs aperiodic programs, and outlines rich future directions including higher-order, disjunctive extensions, and program synthesis within this algebraic framework.

Abstract

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.

Paper Structure

This paper contains 36 sections, 29 theorems, 202 equations.

Key Result

Theorem 1

Let $H$ be a Horn program and let $P$ be an answer set program.

Theorems & Definitions (64)

  • Theorem 1
  • Definition 3
  • Example 4
  • Example 5
  • Definition 6
  • Theorem 7
  • proof
  • Definition 8
  • Theorem 11
  • proof
  • ...and 54 more