A Unifying Framework for Semiring-Based Constraint Logic Programming With Negation

1 Introduction

Constraint logic programming (CLP) facilitates solving problems requiring the consideration of constraints, and is wellestablished as a fruitful formalism over the last decades. To further increase its expressivity, its language has been extended to take into account information about a problem domain of a more quantitative nature, e.g. by allowing fuzzy constraint satisfaction or taking into account scores or penalties. Due to the wide variety of such possible extensions, several works have sought to unify these approaches using the algebraic concept of a semiring [Bistarelli et al., 2001; Khamis et al., 2023]. Even though these works represent a big step forward in terms of unification, they introduce their own assumptions on semirings, which makes it hard to compare these unifying approaches. Furthermore, they restrict attention to positive logic programs, i.e. programs consisting of rules without negation in the body. This is unfortunate, as it is well-known from e.g. answer set programming that negation increases both the conceptual and computational expressivity. However, it also introduces non-monotonicity of the corresponding immediate consequence operator, leading to intricacies in the definition of semantics.

Approximation fixpoint theory (AFT) [Denecker et al., 2001] is a unifying framework for the definition and study of semantics of non-monotonic formalisms. It is a purely algebraic theory which was shown to unify the semantics of, among others, logic programming, default logic, and autoepistemic logic. Due to the algebraic constructions defined in AFT, it often suffices to define a so-called approximating operator to derive a whole class of well-behaved semantics, including the so-called stable and well-founded semantics.

In this paper, we apply AFT to unify and generalize existing approaches to semiring-based constraint logic programming. In more detail, the contributions of this paper are the following: (1) we unify the approaches of [Bistarelli et al., 2001; Khamis et al., 2023] in the framework of AFT, making clear the different assumptions used in these approaches and how they affect the behaviour of the corresponding semantics, (2) we generalize the language of semiring-based constraint logic programming to allow for negation in the body of rules, and (3) use AFT to define and study semantics for such programs, introducing among others the stable and well-founded semantics, and show how they generalize both existing approaches to (positive) SCLPs and normal logic programs (nlps).

Outline of the Paper: In Section 2 we provide background on lattice theory, AFT and semirings. Section 3 considers properties of semirings and derived orders. Section 4 reconstructs existing semantics for SCLPs with lifted assumptions, and in Section 5, we introduce the syntax and semantics of negation, whereas in Section 6 the semantics for programs with negation are studied. We conclude with regard to related work in Section 7.

2 General Background

In this section, we introduce the necessary preliminaries on lattice theory (Section 2.1), approximation fixpoint theory (Section 2.2) and semirings (Section 2.3).

2.1 Lattice Theory

A partially ordered set (poset) L is an ordered pair ⟨L,≤⟩, where ≤⊆ L × L is a reflexive, antisymmetric and transitive relation. Given a poset L = ⟨L,≤⟩ with S ⊆ L, A lower bound (resp. upper bound) of S is an element x ∈ L such that x ≤ s (resp. s ≤ x) for all s ∈ S. A lower bound y of S is the unique greatest lower bound (glb) of S, denoted ∧ S, if for every lower bound x of S in L we have that x ≤ y, and similarly for the least upper bound (lub). We also denote x ∧ y by ∧{x, y} and x ∨ y by ∨{x, y}.

A lattice is a partially ordered set such that each pair of elements has a greatest lower bound and a least upper bound. A lattice is bounded if there are ⊥,⊤ ∈ L such that for any x ∈ L, ⊥ ≤ x ≤ ⊤ holds, and it is complete if every subset of L has a greatest lower bound and a least upper bound. ⊥≤ denotes a complete lattice's least element, and ⊤≤ its greatest element. While every complete lattice is a bounded lattice, it should be noted that the converse is not true [Blyth, 2005].

We will study operators O : L → L, which are ≤- monotone if for all x ≤ y we have that O(x) ≤ O(y), and ≤-antimonotone if for all x ≤ y we have that O(y) ≤ O(x). 1 This work also concerns commutative binary operators O : L × L → L. Such operators are called (anti)monotone if they are monotone (resp. antimonotone) in either operand. That is, we fix one operand at a time and consider the (anti)monotonicity of x ↦→ O(x, y) and y ↦→ O(x, y) separately. An element x ∈ L is a prefixpoint of O if O(x) ≤ x, a fixpoint of O if O(x) = x, and a postfixpoint of O if x ≤ O(x). Should it exist, lfp≤(O) denotes the ≤-least fixpoint of O. 2

Thanks to Theorem 5.1 of Cousot and Cousot [Cousot and Cousot, 1979], we have a constructive characterization of this least fixpoint [Tarski, 1955]. For this characterization, we first define the ordinal powers of a function O : L → L by defining O0 (x) = x, Oα+1 (x) = O(Oα(x)) for a successor ordinal α, and Oα(x) = ∨β<α Oβ (x) for a limit ordinal α. The least fixpoint of a monotone operator on a complete lattice can be constructed by applying its ordinal powers starting from ⊥≤:

Theorem 1 ([Cousot and Cousot, 1979]). Given a complete lattice L = ⟨L, ≤⟩ and a ≤-monotone operator O : L → L, there is an ordinal α such that Oα(⊥≤) is the least fixpoint of O, which coincides with O's least prefixpoint.

2.2 Approximation Fixpoint Theory

In this section, we recall approximation fixpoint theory (AFT) [Denecker et al., 2001], which offers techniques for approximating the fixpoints of a possibly non-monotonic operator.

Given a lattice L = ⟨L,≤⟩, a bilattice is the structure L2 = ⟨L2 ,≤p,≤v⟩, where L2 = L × L, and for every x1, y1, x2, y2 ∈ L, (x1, y1)≤p(x2, y2) if x1 ≤ x2 and y2 ≤ y1, and (x1, y1)≤v(x2, y2) if x1 ≤ x2 and y1 ≤ y2. Intuitively, bilattice elements (x, y) ∈ L2 approximate elements in the interval [x, y] = {z ∈ L : x ≤ z ≤ y}. If x ≤ y, we call (x, y) consistent, and Lc is the set of all consistent pairs. We call elements (x, x) ∈ Lc exact, and note that the set of all exact elements constitutes an embedding of L in L2 . We also use projection functions (x, y)1 = x and (x, y)2 = y.

An operator O : L2 → L2 is an approximator of O : L → L if it is ≤p-monotone and, for any x ∈ L, O(x, x) = (O(x), O(x)). Approximating operators O can be thought of as combinations of two separate operators (O(·, ·))1 and (O(·, ·))2 calculating, respectively, a lower and upper bound for the value of the approximated operator O. We denote (O(·, ·))1 and (O(·, ·))2 as Ol(x, y) and Ou(x, y) respectively. Specifically, we have Ol(·, y) = λx. Ol(x, y) (i.e., Ol(·, y)(x) = Ol(x, y)) and Ou(x, ·) = λy. Ou(x, y).

1 When the ordering clear, we simply say O is (anti)monotone.

2 If the ordering is clear, we simply write lfp(O).

Given a complete lattice ⟨L, ≤⟩ and an approximating operator O : L2 → L2 , the stable operator for O is S(O)(x, y) = (lfp(Ol(·, y)), lfp(Ou(x, ·))). For any ≤p-monotone operator O on L2 , the fixpoints of S(O) are ≤v-minimal fixpoints of O [Denecker et al., 2001]. Also, Ol(·, y) and Ou(x, ·) are ≤-monotone operators -guaranteeing S(O) is well-defined, and S(O) is ≤p-monotone [Denecker et al., 2001].

Given an approximating operator O : L2 → L2 . (x, y) is: the Kripke-Kleene (KK) fixpoint of O if (x, y) = lfp≤p (O); a stable fixpoint of O if (x, y) = S(O)(x, y); the well-founded (WF) fixpoint of O if (x, y) = lfp≤p (S(O)).

A lattice operator may permit multiple approximating operators, but Denecker et al. 2004 define the most precise approximating operator Ou approximating an operator O, called the ultimate approximator of O. In more detail, given a complete lattice L = ⟨L,≤⟩, and O : L → L, the ultimate approximator of O, Ou : Lc → Lc is defined by Ou (x, y) = (∧ O([x, y]), ∨ O([x, y])).

2.3 Semirings

In this section we recall the necessary preliminaries on semirings, which we will use as the range of interpretations of logic programs. A monoid is a tuple M = ⟨L, ◦, e⟩ such that ◦ : L × L → L is a binary, associative operator on L; and we have for any x ∈ L that e ◦ x = x = x ◦ e-e is the identity element of ◦. If ◦ is commutative, we call M a commutative monoid. If ⟨L,≤⟩ is a poset s.t. ◦ is ≤-monotone, M is ordered by ≤, and if for every x ∈ L we have that e ≤ x, it is positively ordered.

A commutative monoid M = ⟨L, ◦, e⟩ is equipped with a 'sum' operation⃝I for finite index sets I such that: ⃝i∈∅xi = e; ⃝i∈{j}xi = xj; ⃝i∈{j,k}xi = xj ◦ xk for j ̸= k; and ⃝j∈J ⃝i∈Ij xi =⃝i∈Ixi if ⋃j∈J Ij = I and Ij ∩ Ij ′ = ∅ for j ̸= j ′ . If the sum operation ⃝I is well-defined for any infinite index set I, M is a complete monoid. 3

A semiring is a tuple S = ⟨L,+,×, 0, 1⟩, such that: ⟨L,+, 0⟩ is a commutative monoid, with + being called the additive operator; ⟨L,×, 1⟩ is a monoid, with × being called the multiplicative operator; we have for any x ∈ L that x×0 = 0 = 0×x-i.e. 0 is the absorbing element of ×; and we have for any x, y, z ∈ L that x×(y+z) = (x×y)+(x×z) and (y + z) × x = (y × x) + (z × x)-i.e. × left- and rightdistributes over +. Sum (∑) and product (∏) denote the sum operation of + and × respectively. We identify six specific classes of semirings:

1. If ⟨L,×, 1⟩ is a commutativemonoid, S is a commutative semiring.
2. If x + x = x holds for any x ∈ L, S is an idempotent semiring.
3. If S is a commutative idempotent semiring, and we have for any x ∈ L that x + 1 = 1 = 1 + x-i.e. 1 is the

3 Bijective indexings are left implicit. E.g. ⃝{x1, . . . , xn} = x1 ◦ . . . ◦ xn and ⃝(x1, x2, . . .) = x1 ◦ x2 ◦ . . . (if it is defined).

absorbing element of +-then S is a constraint-based semiring (c-semiring) [Bistarelli et al., 2001].

1. S is a complete semiring if ⟨L,+, 0⟩ is a complete monoid, and it holds that ∑i∈I (x × xi) = x × (∑i∈I xi) and ∑i∈I (xi × x) = (∑i∈I xi) × x.
2. If ⟨L,+, 0⟩ and ⟨L,×, 1⟩ are ordered by poset ⟨L,≤⟩, S is ordered by ⟨L, ≤⟩.
3. If ⟨L,+, 0⟩ is positively ordered by the poset ⟨L,≤⟩ and ⟨L,×, 1⟩ is ordered by ⟨L,≤⟩, then S is positively ordered by ⟨L, ≤⟩.

Note. Hereafter, unless otherwise specified, S = ⟨L, +, ×, 0, 1⟩ is assumed to be a commutative semiring. Some examples of commutative semirings are:

• S = ⟨F, +, ·, 0, 1⟩, for F ∈ {N, Z, Q, R};
• P(A) = ⟨2A, ⋃, ⋂, ∅,A⟩, the power set semiring ;
• B = ⟨{true, false}, ∨, ∧, false, true⟩, the Boolean semiring;
• F = ⟨[0, 1],max,min, 0, 1⟩, the fuzzy semiring;
• N∞ = ⟨N ⋃{∞}, +, ·, 0, 1⟩, where n + ∞ = ∞ for all n and m · ∞ = ∞ for all m ̸= 0 - the semiring of natural numbers lifted to infinity.

3 Families of Semirings and Their Orderings

In Section 2.1, we saw a constructive definition for the least fixpoint of a monotone operator on a complete lattice, and, in Section 2.2, we saw that such constructions are widely used in AFT. In the following sections, we will use such constructions again to define the semantics of our semiringbased formalism. For this, we will require complete lattices that order our semirings. Some semirings of interest have standard orderings that happen to be complete lattices-for example, the Boolean semiring B forms a complete lattice under false < true and the power set semiring P(A) forms a complete lattice under set inclusion. Such orderings are not readily apparent for all semirings, however. We therefore investigate a "semiring-agnostic" ordering and look for conditions under which this ordering forms a complete lattice. This ordering, found throughout the literature [Green et al., 2007; Khamis et al., 2024; Hannula, 2023], is the natural order.

Definition 1. For any x, y ∈ L, we say x≤N y if there exists a z ∈ L such that x + z = y. When ≤N is a partial order, we call it the natural order. A semiring ⟨L, +, ×, 0, 1⟩ for which ⟨L, ≤N⟩ is a partial order is called naturally ordered.

Not all semirings are naturally ordered. When semirings allow for additive inverses, the ordering is not antisymmetric. In all other cases, the ordering is a partial order.

Lemma 1. S is naturally ordered if and only if it contains no elements x and -x s.t. x ̸= 0 and x + (-x) = 0.

Our additive and multiplicative operators are monotone for naturally ordered semirings.

Lemma 2. If S is naturally ordered, it is ordered by ≤N.

A complete lattice of semiring elements must be bounded. For naturally ordered semirings, the element 0 is the least element bounding our lattice from below.

Lemma 3. If S is naturally ordered, ⊥≤N = 0.

While all naturally ordered semirings are bounded from below by 0, they are not generally bounded from above. A straightforward example of this is the whole number semiring N, for which the natural order coincides with the usual ordering and which extends infinitely upwards. Naturally, this also means not all naturally ordered semirings form a complete lattice. In fact, a naturally ordered semiring has a maximal element if and only if said element is absorbing for +.

Lemma 4. If S is naturally ordered, ⊤≤N = x ∈ L if and only if x is absorbing for +.

Bistarelli et al. 2001 propose an ordering specific to csemirings which forms a complete lattice under certain circumstances.

Definition 2. Let S be a c-semiring. For any a, b ∈ L, we define the c-semiring order as a≤C b if a + b = b.

We treat ≤C as if it were defined for any (non-c-)semiring and find it to be a specific case of the natural order.

Lemma 5. For idempotent S and a, b ∈ L: a≤N b iff a≤C b.

Not only do ≤N and ≤C coincide whenever S is idempotent-in this case they are also always a partial order. This, of course, also means that idempotent semirings do not permit additive inverses.

Lemma 6. If S is idempotent, it is naturally ordered.

Bistarelli et al. [1997] show how ≤N can form a complete lattice for c-semirings by first showing that + and ∨ coincide, then showing that any set that has the ∨ also has the ∧, and finally combining these two facts to get that any set has both the ∨ and ∧. However, this reasoning relies on the assumption that the sum is defined for any (infinite) set of c-semiring elements. This assumption does not hold for every c-semiring, as shown in Appendix A.1. We also find that a complete csemiring is a stronger assumption than necessary to obtain these results. Indeed, we find the same results for complete idempotent semirings with a greatest element ⊤≤N .

Lemma 7. If S is a complete idempotent semiring s.t. ⊤≤N exists, then ⟨L,≤N⟩ is a complete lattice.

Completeness of a semiring, by itself, is not sufficient to guarantee a complete lattice of semiring elements.

Lemma 8. Not every complete semiring gives rise to a complete lattice under the natural order.

Other examples of a semiring inducing a complete lattice under the natural order are N∞ and ⟨[0, 1], +, ·, 0, 1⟩.

4 Semiring-based Constraint Logic Programming

We begin our study of semiring-based constraint logic programming, limiting ourselves to the positive fragment of the full formalism that will be presented in Section 5. In essence, this special case is a simplified account of semiring-based constraint logic programs as introduced by Bistarelli et al. 2001, in which we exclude variables and functions from our language, leaving such extensions for future work. On the other hand, we lift their assumption of c-semirings and consider general semirings.

Definition 3. Given a semiring S = ⟨L,+,×, 0, 1⟩ and a set of atoms A, generalized atoms are defined as atoms and semiring values. A clause is an expression of the form H : -B1, . . . ,Bn where H, the head of the clause, is an atom and each Bi appearing in the (possibly empty) body of the clause is a generalized atom. A positive semiring-based constraint logic program for S (PSCLP(S), for short 4 ), is a set of clauses. AP denotes the atoms used in PSCLP(S) P.

Notice that Datalog programs [Ceri et al., 1989] are a special case of PSCLPs, namely the programs PSCLP(B).

Example 1. We consider the following program P (adapted from [Bistarelli et al., 2001]) as a running example.

c1: solution(a) :- path(a,b). c2: solution(a) :- path(a,c). c3: path(a,b) :- mass_transit(a). c4: path(a,c) :- car(a). c5: mass_transit(a) :- train(a). c6: train(a) :- 2. c7: car(a) :- 3.

The semiring over which P is defined, from which the integer values in the program stem, is the optimization semiring O = ⟨N ⋃{∞}, min, +, ∞, 0⟩. This semiring allows us to optimize over constraints, by assigning each constraint an integer representing the cost of the connection it models, combining constraints by summing their costs, and comparing constraints using the minimum operator. We order the semiring with the complete lattice ⟨N ⋃{∞},≥⟩-higher costs are 'lesser than' lower costs.

The clauses c6 and c7 describe the costs associated with travelling by train or car respectively. c5 tells us that train travel is a form of mass transit. Since mass_transit(a) is only defined by c5, the cost of using mass transit will only depend on the cost of travelling by train. The clauses c3 and c4 inform us that mass transit and car travel each allow us to take a different path, and that the costs associated with following these paths will depend on the cost of using their corresponding mode of transport. Finally, the clauses c1 and c2 tell us that either path constitutes a solution to our problem, and that we must compare the costs of either path to obtain the optimal solution to our problem.

The semantics of PSCLPs is given in terms of interpretations that assign semiring values to formulas, essentially generalizing classical interpretations by allowing any semiring value as truth value instead of just the Boolean ones.

Definition 4. An interpretation I of some PSCLP P based on a semiring S = ⟨L, +, ×, 0, 1⟩ is a mapping I : AP → L. We extend interpretations to semiring element x ∈ L by I(x) = x, to conjunctions of formulas (inductively) by I(A, B) = I(A)× I(B), and to empty conjunctions by I(∅) = 1.

Note. Hereafter, unless otherwise specified, we assume that ⟨L,≤⟩ is a partial order, and that P is a PSCLP(S).

We endow the set of P's interpretations ISP with an ordering that respects the partial order of semiring elements.

4 We write PSCLP when the semiring is clear or unimportant.

Definition 5. The partial order of interpretations ⟨ISP ,⪯⟩ is derived from ⟨L, ≤⟩ such that for any I1, I2 ∈ ISP , I1 ⪯ I2 if I1(x) ≤ I2(x) for any atom x ∈ AP .

When ⟨L,≤⟩ is a complete lattice, so is ⟨ISP ,⪯⟩. We now introduce the notion of model for PSCLPs.

Definition 6. I ∈ ISP is a semiring model of P if it holds for every H ∈ AP that ∑{∏ni=1 I(Bi) | H : - B1, . . . , Bn ∈ P} ≤ I(H). MSP denotes the set of semiring models of P .

This notion of model deviates slightly from the traditional notion of model. The traditional notion of model requires only that the head of each clause be interpreted as no lesser than the clause's body-considering every clause independently. Our notion of model instead considers all clauses defining an atom in unison, requiring that said atom be interpreted as no lesser than the sum of these clauses' bodies. The difference between these notions stems from the fact that the operators used traditionally for the comparison between clauses (like ∨ or max) are idempotent, while the additive operators used for this purpose in our framework are not necessarily. In this way, our notion of model treats semirings more seriously as a structure for evaluation. 5

Example 2. We illustrate which interpretations are semiring models of our running example program. For interpretation I ∈ ISP to be a semiring model of P , we require that:

• 3 ≥ I(car(a)) and 2 ≥ I(train(a));
• I(train(a)) ≥ I(mass transit(a));
• I(car(a)) ≥ I(path(a, c));
• I(mass transit(a)) ≥ I(path(a, b)); and
• min{I(path(a, c)), I(path(a, b))} ≥ I(solution(a)).

Given all the interpretations of a PSCLP, we would like to select a single unique model as the representative one. In logic programming, this representative model is the minimal model [Lloyd, 1987], obtained as the intersection of each model's sets of true atoms. Intuitively, this model minimizes truth ascription while still satisfying all clauses. In other words, it makes true what must be true and nothing else. Here, we follow a similar approach but require a generalization of the notion of model intersection.

Definition 7. Given a complete lattice ⟨L, ≤⟩ and A ∈ AP , we define the model intersection of M ⊆ MSP as ⋂ M(A) = ∧{I(A)| I ∈ M}.

Lemma 9. If S is ordered by a complete lattice ⟨L,≤⟩ and M ⊆ MSP , ⋂ M is a semiring model for PSCLP(S) P .

We obtain the minimal semiring model by intersecting MSP .

Definition 8. The minimal semiring model of PSCLP P is M sP = ⋂ MSP . M sP is the model-theoretic semantics of P .

Example 3. For our running example, the minimal semiring model gives us the following.

• M sP (car(a)) = 3 and M sP (train(a)) = 2;
• M sP (mass transit(a)) = 2;

5 We defer an investigation of the differences between these notions of model to Appendix A.2.

• M sP (path(a, c)) = 3;
• M sP (path(a, b)) = 2; and
• M sP (solution(a)) = 2.

The model-theoretic semantics of a PSCLP lacks a constructive definition. We therefore work toward an equivalent fixpoint semantics that does have a constructive definition, based on an extension of the well-known immediate consequence operator from Datalog to PSCLPs.

The fixpoint semantics of a PSCLP is defined as the least fixpoint of this immediate consequence operator. This fixpoint can be constructed if TP is monotone on a complete lattice.

Lemma 7 now gives us sufficient conditions for the existence of a constructive definition of our fixpoint semantics.

Corollary 1. If S is ordered by the complete lattice ⟨L,≤⟩ (e.g. when S is a complete idempotent semiring s.t. ⊤≤N exists), there is an ordinal α such that TPα(⊥⪯) is the least fixpoint of TP, which coincides with TP's least prefixpoint.

Example 4. We illustrate TP on the program from Example 1. The immediate consequence operator is instantiated as TP(I)(H) = min{∑ni=1 I(Bi)|H : - B1, . . . , Bn ∈ P}. The bottom interpretation ⊥⪯ for this semiring maps each semiring element to itself and each atom to the bottom element ∞.

In view of Corollary 1, we obtain lfp(TP) stepwise as illustrated in Table 1. A fixpoint is reached at I4, as TP(I4) = I4.

To show the equivalence between our model-theoretic semantics and our fixpoint semantics, we require that the prefixpoints of TP coincide with the semiring models of P .

Lemma 11. Let S be ordered by the complete lattice ⟨L,≤⟩. I ∈ ISP is a semiring model of PSCLP(S) P iff TP(I) ⪯ I.

From here, we obtain the equivalence between the minimal semiring model of P and the least fixpoint of TP.

Lemma 12. Let S be ordered by the complete lattice ⟨L,≤⟩. For PSCLP(S) P , M sP = lfp(TP).

5 Generalized Negation for Semiring-based Constraint Logic Programming

As presented up until this point, our formalism can only represent positive expressions. We can express that one may use mass transit if there is an available train connection, but we would have no good way to express that cycling is a good alternative if it is not raining. We now extend our formalism with a notion of negation so that negative expressions may also be represented. This notion of negation will follow the idea of negation as failure [Clark, 1977], where the negation of an atom may be derived if the atom itself is not derivable.

Definition 10. Given a semiring S = ⟨L, +, ×, 0, 1⟩ and a set of atoms A, negated atoms are defined as not a where a ∈ A. Atoms or their negation are referred to as literals, and generalized atoms are literals or semiring elements. A normal semiring-based constraint logic program based on S (NSCLP(S) for short 6 ) is a set of normal clauses of the form H : - B1, . . . , Bn where H, the head, is an atom and each Bi appearing in the (possibly empty) body is a generalized atom.

Normal logic programs, of course, interpret true and false as each other's negation. We generalize negation in normal logic programs with a notion of negation similar to that used in G¨odel logics [G¨odel, 1932], also used in the semiring-based formalism of Eiter and Kiesel [Eiter and Kiesel, 2020b]. Here we make use of 1 and 0, the neutral and absorbing elements of the multiplicative operator ×; if an atom is interpreted with 0and it would thus nullify the interpretation of any conjunction it appears in-we interpret its negation as 1, leaving the interpretation of the further conjunction unaffected. Meanwhile, if an atom is interpreted as anything other than 0-and it would thus not nullify the interpretation of the conjunction it appears in-we interpret its negation as 0, nullifying the interpretation of any conjunction it appears in. Take, e.g. I4 from Example 3. We have I4(not car(a)) = ∞, as I4(car(a)) = 3 ̸= ∞. Meanwhile, for rain(a)-an atom without a clause defining it-we have I4(not rain(a)) = 0, as I4(rain(a)) = ∞. This notion of negation generalizes negation as known from nlps while making only minimal assumptions on the semiring. Note. A semiring permits only a single absorbing element for ×-namely 0; for any ×-absorbing element a, we have that a × 0 = a = 0 = 0 × a.

Definition 11. An interpretation I (Def. 4) is extended to negated literals by I(not a) = {1 if I(a) = 0 0 otherwise .

As is well-known from normal logic programs, introducing negation leads to non-monotonicity of the TP-operator:

Example 5. Consider the NSCLP(B) P = {a : - not b}, where true > false as usual. Now consider two interpretations I1 = {a : true, b : true} and I2 = {b : false, b : false}. We see that I2 ⪯ I1. Applying TP we get TP(I1)(a) = I1(not b) = false, TP(I2)(a) = I2(not b) = true, and TP(I1)(b) = false = TP(I2)(b). Note that, because there is no predicate defining b, the value assigned by TP to b is false-the neutral element for ∨ resulting from summation over an empty set-under either interpretation. Comparing the values assigned to a and b now shows that I2 ⪯ I1 but TP(I2) ⪯̸ TP(I1).

Naturally, this behaviour means that previous results relying on the assumed ≤-monotonicity of + and × cannot be presumed to hold for NSCLPs. Most importantly, the nonmonotonicity of TP means that we can no longer use Theorem 1 to construct its least fixpoint. In the following sections, we will circumvent this behaviour by means of AFT.

6 We write NSCLP when the semiring is clear or unimportant.

6 Normal Semiring-based Constraint Logic Programming in Approximation Fixpoint Theory

In the previous section, we saw that we can no longer derive the monotonicity of our immediate consequence operator from the monotonicity of + and ×. This left us without a constructive definition of the least fixpoint semantics for our program. In this section, we capture our framework in AFT by approximating the immediate consequence operator, thus bestowing NSCLPs with the semantic notions recalled in Section 2.2. Note. Hereafter, unless otherwise specified, we assume that ⟨L, ≤⟩ is a complete lattice. Note that, by extension, ⟨ISP , ⪯⟩ is assumed to be a complete lattice as well.

6.1 Approximating the Immediate Consequence Operator

We first consider the most precise, ultimate, approximator T u P of the immediate consequence operator TP.

While the ultimate approximator is the most precise approximator, its evaluation is rather costly-requiring the evaluation of TP for every interpretation in the input approximation, prior to identifying the glb and lub. This typically results in a higher computational complexity [Denecker et al., 2004]. For this reason we also introduce another approximator which is not necessarily as precise, but is more economical to use.

For this second approximator, we generalize the four-valued operator originally introduced by [Fitting, 2002]. Recall that consistent approximations (Il, Iu) ∈ IScP have a lower bound Il-which is most conservative in its interpretation-and an upper bound Iu-which is most generous in its interpretations. In other words, for any atom A ∈ AP , Il(A) is the lowest value of any I(A) with I ∈ [Il, Iu] and Iu(a) the highest. Now, to approximate TP, we find a new lower bound taking the same sum-product as we would when evaluating TP but-instead of considering a single interpretation-we evaluate generalized atoms without negation using Il (yielding the most conservative values) and evaluate negated atoms using Iu (nullifying whenever possible). The new upper bound is found the same way, switching Il and Iu. This way of approximating TP relies on the additional assumption that 0 lies at the bottom of our semiring ordering, such that nullifying an expression cannot increase its value; this way, using the given upper bound to evaluate negated literals results in lesser values and vice versa.

Definition 13. Let I1, I2 ∈ ISP ; H ∈ AP ; T fPl (I1, I2)(H) = ∑{∏ni=1 I′ (I1, I2)(Bi)|H : -B1, . . . ,Bn ∈ P}; and I′ (I1, I2)(Bi) = {I2(Bi) if Bi is of the form notF I1(Bi) otherwise .

We define T fP (I1, I2) = (I3, I4) s.t. for all A ∈ AP , I3(A) = T fPl (I1, I2)(A) and I4(A) = T fPl (I2, I1)(A).

It follows immediately from the results from [Denecker et al., 2004, Theorem 5.6] that T u P is an approximator of TP.

Somewhat surprisingly, T fP is not generally ≤p-monotone: Example 6. We present an example wherein T fP is not ≤pmonotone.

Take the semiring Z = ⟨Z∪{-∞, +∞}, +, ·, 0, 1⟩ consisting of the integers with positive and negative infinity, ordered by ≤ as usual. Consider an NSCLP(Z) consisting of a single clause p : - not q, r. Now consider two approximations A1 = (I1, I2) and A2 = (I1, I3) where I1 = {p : -1, q : -1, r : -1}, I2 = {p : 1, q : 1, r : 1}, and I3 = {p : 0, q : 0, r : 0}. We see that A1 ≤p A2. We now apply T fP to A1 and A2 and get T fP (A1) = ({p : 0, q : 0, r : 0}, {p : 0, q : 0, r : 0}) and T fP (A2) = ({p : -1, q : 0, r : 0}, {p : 0, q : 0, r : 0}). Even though A2 is more precise than A1, we do not have that T fP (A1)≤p T fP (A2); in fact, T fP (A1) is strictly more precise than T fP (A2). T fP is not ≤p-monotone for this NSCLP. The reason for this failure of ≤p-monotonicity is that the upper bound of A2 being lower (i.e. more precise) than that of A1 (namely 0 instead of 1 for every atom) causes not q in the rule body to evaluate to 1, which in turn "allows" the truth value of r to determine the truth value of p. However, as this "positive" influence of r means that p attains the negative value I1(r) = -1, we obtain a new lower bound for p that is negative and thus lower than the new lower bound obtained in view of A1. Thus, T fP will not behave as an approximator when applied to semirings that have elements below the 0-element. Working out the same example for T u P , we get T u P (A1) = ({p : -1, q : 0, r : 0}, {p : 1, q : 0, r : 0}) and T u P (A2) = ({p : -1, q : 0, r : 0}, {p : 0, q : 0, r : 0}). Here we do have that T u P (A1) ≤p T u P (A2). This is no coincidence, as T u P is guaranteed to be an approximator [Denecker et al., 2004].

Whenever the additive and multiplicative operators are monotone and 0 is the minimum element of the semiring ordering, T fP is an approximator of TP:

Lemma 13. T fP is an approximator of TP if and only if S is positively ordered by the complete lattice ⟨L, ≤⟩.

We can now construct the KK fixpoints of our two approximators, to approximate all the fixpoints of TP, thus generalizing the semantics from PSCLPs to NSCLPs:

Corollary 2. There is an ordinal α such that T u P α(⊥≤p ) = lfp≤p (T u P ). If S is positively ordered by the complete lattice ⟨L,≤⟩, the same holds for T fP .

Note. If lfp≤p (T u P ) and lfp≤p (T fP ) are exact, TP has only a single fixpoint. This is the case in particular if P is positive.

Example 7. We illustrate the use of an approximator by constructing the KK fixpoint of T fP for our running example, extended with three additional clauses to incorporate negation.

That is, P = {c1, . . . , c10} with:

c8: solution(a) :- path(a,d). c9: path(a,d) :- bicycle(a).

c10: bicycle(a) :- 1, not rain(a). T fPl is instantiated as T fPl (I1, I2)(H) = min{∑ni=1 I′ (I1, I2)(Bi)|H : -B1, . . . ,Bn ∈ P}. Table 2

shows the application of the corresponding T fP , starting from ⊥≤p , to construct the KK fixpoint A4.

6.2 Stable Semantics for Normal Semiring-based Constraint Logic Programs

KK fixpoints of T u P and T fP approximate all fixpoints of TP, but might sanction self-supporting reasoning:

Example 8. Consider an NSCLP(B) P consisting of two clauses: p : - not q and q : - q. Applying T fP gives us T fP (⊥≤p ) = ({p : false, q : false}, {p : true, q : true}) = ⊥≤p ; thus ⊥≤p is the KK fixpoint of T fP , which means that q stays undecided because of the self-supporting rule q : - q, which also keeps p undecided (in view of p : - not q).

The only reason for making q true in the upper bound of the KK fixpoint in the example above is the fact that q was made true in the upper bound of the least precise approximation. This type of "because-I-said-so" reasoning is avoided by using the stable operator and its ≤p-least fixpoint-the WF fixpoint, which we study in this section.

We first observe these operators are well-defined:

Corollary 3. For any (I1, I2) ∈ IScP there are ordinals α and β such that (∧ TP([·, I2]))α(⊥⪯) = lfp(T u P l (·, I2)), (∨ TP([I1, ·]))β (⊥⪯) = lfp(T u P u (I1, ·)), and the stable operator for T u P is S(T u P )(I1, I2) = (lfp(T u P l (·, I2)), lfp(T u P u (I1, ·))). The same holds for T fP if S is positively ordered by ⟨L, ≤⟩.

The fixpoints of these stable operators, called the stable fixpoints of T u P and T fP respectively, are ≤v-minimal fixpoints of their respective bilattice operator (this is an immediate corollary of Theorem 4 of [Denecker et al., 2001]) and they generalize the WF and stable model semantics known from normal logic programs (see Theorem 2).

We can now also construct the well-founded fixpoints of our two stable operators. These fixpoints approximate all stable fixpoints of their respective bilattice operators.

Corollary 4. There is an ordinal α such that S(T u P )α(⊥≤p ) = lfp≤p (S(T u P )). If S is positively ordered by ⟨L,≤⟩, the same is true for T fP .

Example 9. To illustrate the use of the stable operator, we apply S(T fP ) to the program presented in Example 8 We first construct the WF fixpoint, by repeatedly applying S(T fP ), starting from ⊥≤p . Denoting interpretations as sets of true atoms, we get the following. First, ⊥≤p = (∅, {p, q}). Then, S(T fP )((∅, {p, q})) = ({p}, {p}) since lfp(T fPl (·, {p, q})) = {p} and lfp(T fPl (·, ∅)) = {p}. Finally, S(T fP )({p}, {p}) = ({p}, {p}) so ({p}, {p}) is the WF fixpoint of T fP . Since this WF fixpoint is exact, we also know it to be the only stable fixpoint of T fP .

Finally, since our operators generalize those known from normal logic programming, and AFT has been shown to faithfully capture all the main semantics from nlp [Pelov et al., 2007], we faithfully generalize these main semantics:

Theorem 2. Given an NSCLP(B), the following hold: (1) (I1, I2) is a stable fixpoint of T fP iff it is a partial stable model according to [Przymusinski, 1990]; (2) (I1, I2) is the WF fixpoint of T fP iff it is the WF model according to [Przymusinski, 1990]; (3) (I1, I2) is a stable fixpoint of T u P iff it is a partial stable model according to [Denecker et al., 2004]; (4) (I1, I2) is the WF fixpoint of T u P iff it is the WF model according to [Denecker et al., 2004].

7 Conclusion, in view of RelatedWork

We have unified existing semantics [Bistarelli et al., 2001; Khamis et al., 2023] for PSCLPs in this paper, and generalized the syntax and semantics to allow for default negation on the basis of AFT, resulting in a family of well-behaved semantics that also generalizes the well-known semantics for nlps. To our best knowledge only a few other approaches combine semirings and logic programming, which we discuss now.

Firstly, Eiter and Kiesel 2020a provide a framework that captures many approaches to answer set programs taking into account algebraic constraints. In this work, terms (like a in train(a)) are allowed to be interpreted using semiring values and operations. However, while terms are assigned semiring values, formulas are still interpreted in a discrete way, by assigning the neutral element of × if it is true while assigning the neutral element of the + if it is true. Thus, they use a different interpretation of formulas, where semirings are seen as oracles to evaluate the constraints. [Eiter and Kiesel, 2020a] show that a host of different systems, e.g. integrations of satisfaction modulo theories into ASP [Cabalar et al., 2020b; Cabalar et al., 2020a], can be captured within their framework, and the differences described above also apply to such systems.

Secondly, there is work combining logic programs with semirings in generalizations of model-counting [Derkinderen et al., 2024; Kimmig et al., 2017]. Such works differ from ours in that their semantics are obtained by assigning every discrete or Boolean interpretation of a logic program a semiring value, generalizing the ProbLog semantics [Raedt et al., 2007], whereas we use semiring values to build our interpretations.

Future work includes computational complexity, implementations, and applying AFT-based notions such as stratification [Vennekens et al., 2004], conditional independence [Heyninck, 2024] and non-determinism [Heyninck et al., 2024].