Under consideration for publication in Theory and Practice of Logic Programming

1

arXiv:cs/0509024v2 [cs.LO] 15 May 2006

Well-founded and Stable Semantics of Logic Programs with Aggregates

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

submitted 1 November 2005; revised 14 April 2006; accepted 4 May 2006

Abstract

In this paper, we present a framework for the semantics and the computation of aggregates in the context of logic programming. In our study, an aggregate can be an arbitrary interpreted second order predicate or function. We de?ne extensions of the Kripke-Kleene, the well-founded and the stable semantics for aggregate programs. The semantics is based on the concept of a three-valued immediate consequence operator of an aggregate program. Such an operator approximates the standard two-valued immediate consequence operator of the program, and induces a unique Kripke-Kleene model, a unique well-founded model and a collection of stable models. We study di?erent ways of de?ning such operators and thus obtain a framework of semantics, o?ering di?erent trade-o?s between precision and tractability. In particular, we investigate conditions on the operator that guarantee that the computation of the three types of semantics remains on the same level as for logic programs without aggregates. Other results show that, in practice, even e?cient threevalued immediate consequence operators which are very low in the precision hierarchy, still provide optimal precision. KEYWORDS: Logic Programming, Aggregates.

1 Introduction This paper is a study of the semantics of an extension of logic programming with aggregates. Aggregates are speci?c second order functions or predicates ranging over sets. Standard examples are the minimum of a subset of a partially ordered domain, the cardinality of a set, the sum, the product and the average of a ?nite set of integers or reals, etc. Aggregates play an important role in di?erent areas. They are used and studied extensively in the context of databases (confer the group-by statement). They were introduced in the context of logic programming as declarative variants of the set of and bag of procedures (Kemp and Stuckey 1991; Mumick et al. 1990). Recently, they were introduced in the context of two extensions of logic programming, Answer Set Programming (Simons et al. 2002) and Abductive Logic Programming (Van Nu?elen and Denecker 2000). Aggregates commonly show up in human expert knowledge and expressions of computational problems. For instance: ? the query for the average result of students for some exam; ? the property that the capacity of a room should exceed the number of students attending the course that takes place in that room;

2

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe ? the cardinality constraint that a lecturer should not teach more than 6 courses; ? the property or constraint that the sum of the capacities of available power generators in some electricity factory should exceed some given lower bound;

These examples show that aggregates are important to express many forms of human expert knowledge and computational problems in a direct and natural way. For this reason, aggregates likely will be part of computational logics and the languages of future knowledge based systems. We will study the semantics of sets of rules of the form A←? where A is an atomic formula and ? a logic expression possibly containing aggregate formulas. Such rule sets are a core part in logic programming and extensions such as abductive logic programming and extended logic programming, the sublogic of answer set programming. Rule sets occur also as de?nitions of intensional predicates in deductive databases and as inductive de?nitions in the logic ID-logic, an extension of classical logic with generalized, non-monotone inductive de?nitions (Denecker 2000). Thus, the results of our study can be applied in the context of all these logics. In the context of logic programming, several extensions with aggregates were proposed for subclasses of the formalism that we consider here, in particular for monotone aggregate programs (Mumick et al. 1990; Ross and Sagiv 1997) and strati?ed aggregate programs (Dell’Armi et al. 2003; Mumick et al. 1990). Our work extends such proposals in two ways. First, we consider more general rule sets with arbitrary recursion over aggregates. Second, we develop a framework of semantics including extensions of the three main semantics that have been used in logic programming: Kripke-Kleene semantics (i.e., three-valued completion semantics) (Fitting 1985), stable semantics (Gelfond and Lifschitz 1988) and the well-founded semantics (Van Gelder et al. 1991). The foundation of our work is the algebraic theory of approximating operators (Denecker et al. 2000; Denecker et al. 2004). Approximation theory is a ?xpoint theory of non-monotone lattice operators. With any lattice operator O : L → L, it associates a family of approximating operators A : L2 → L2 on the product lattice L2 . The ?xpoint theory associates with every approximating operator A di?erent types of ?xpoints: a Kripke-Kleene ?xpoint and a well-founded ?xpoint, both in the bilattice L2 and a set of A-stable ?xpoints of O in the lattice L. In (Denecker et al. 2000) it was shown that the three-valued Fitting operator ΦP (Fitting 1985) is an approximation of the immediate consequence operator TP of a logic program P and that the di?erent types of ?xpoints of ΦP corresponds to the Kripke-Kleene, the well-founded and the stable models of P . In (Denecker et al. 2004), the class of approximations of O was further investigated. The collection of approximations of a lattice operator O is ordered by a precision order. More precise approximations have a more precise Kripke-Kleene and well-founded ?xpoint, and have more stable ?xpoints. It was shown that O has

Well-founded and Stable Semantics of Logic Programs with Aggregates

3

a most precise approximation, called the ultimate approximation of O which has the most precise semantics. In the context of logic programming, approximation theory induces a family of Kripke-Kleene, a family of well-founded and a family of stable semantics, generated by the class of approximations of the immediate consequence operator TP . Basically, each family formalizes similar intuitions but in di?erent degrees of precision. In (Denecker et al. 2004), the ultimate and the standard versions of these semantics are investigated. It follows from the general theory that the ultimate versions of the semantics are more precise than the standard semantics. Also, ultimate semantics have elegant semantic properties which do not always hold for the standard semantics based on the Fitting operator. For instance, substituting a rule body B by a formula B ′ which is equivalent with B in classical logic, is equivalence preserving1 in the ultimate semantics but not in the standard semantics. Also, the ultimate wellfounded model of a program with a monotone TP is the least ?xpoint of TP . On the negative side, applying the ultimate approximation is computationally harder, and it was shown that computing the three types of ultimate semantics for propositional programs is one level higher in the polynomial hierarchy than the standard versions of the same semantics. It was also shown that for important classes of logic programs, standard and ultimate semantics coincide. In fact, it seems that both semantics only di?er for programs containing a recursively de?ned predicate p whose de?nition also uses reasoning by cases of the form (p ∧ . . . ) ∨ (?p ∧ . . . ). In practice, such programs seem to be rare (we are unaware of any practical program with this feature). Thus, the standard semantics based on the Fitting operator and the ultimate semantics based on the ultimate approximation are two very close points in the hierarchy of semantics induced by approximation theory and represent di?erent trade-o?s between precision and complexity. In this work we apply the approximation theory in the context of rule sets with aggregate expressions. We extend the two-valued immediate consequence operator TP for aggregate programs, de?ne several di?erent approximating operators of it and study the semantics obtained from them. One operator is the ultimate approximation of TP . The three types of ultimate semantics obtained from this operator extend the corresponding ultimate semantics for logic programs. They also have the same attractive semantical properties and the high computational complexity. So, we also study extensions of the standard Kripke-Kleene, well-founded and stable semantics of logic programs. To achieve this, we propose the concept of a three-valued aggregate relation approximating a given aggregate relation. We use this concept to de?ne an extension of the Fitting operator ΦP to the case of programs with aggregates. Since an aggregate relation is approximated by a class of three-valued aggregate relations, we obtain a sub-family of approximations of TP , all of which coincide with the Fitting operator ΦP in case P does not contain aggregate expressions. Just as in the case of logic programming without aggregates, the di?erent semantics based on the di?erent approximation operators represent close points in

1

In the sense of having the same set of models.

4

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

the hierarchy of semantics induced by approximation theory and provide di?erent trade-o?s between precision and complexity. 2 Fixpoint Theory of Monotone and Non-monotone Operators We now present the necessary background on Approximation Theory. For more information we refer to (Denecker et al. 2004). A structure L, ≤ is a poset if ≤ is a re?exive, asymmetric and transitive binary relation on L. A poset L, ≤ is a chain if ≤ is a total order, i.e., for each x, y ∈ L, either x ≤ y or y ≤ x. Sometimes, when the order relation ≤ is clear from the context we denote a poset simply with its domain L. A poset L, ≤ is chain-complete if each chain S ? L has a least upper bound lub(S ) in L. Since the empty set is a chain, a chain-complete poset has a least element ⊥. A poset L, ≤ is a complete lattice if each subset S of L has a least upper bound lub(S ) and a greatest lower bound glb(S ) in L. In particular, L has a least element ⊥ and a largest element ?. A complete lattice is chain-complete. An operator O : L → L on a poset L, ≤ is ≤-monotone if for each x, y ∈ L, x ≤ y implies O(x) ≤ O(y ). A monotone operator O on a chain-complete poset L, ≤ has a least ?xpoint lfp(O). This ?xpoint can be constructively computed as a sequence of powers of O de?ned as follows: O ↑0 (x) = x O ↑α+1 (x) = O(O ↑α (x)) O ↑λ (x) = lub({O ↑α (x) | α < λ}) for a limit ordinal λ Proposition 2.1 If O : L → L is a monotone operator and L is a chain-complete poset then there exists an ordinal α such that O ↑α (⊥) = lfp(O). The least such ordinal is called the closure ordinal of O and is denoted by ∞. Approximation theory is an extension of the above ?xpoint theory to the case of arbitrary (non-monotone) lattice operators O. The following basic concepts are needed. Given a complete lattice L, ≤ , its bilattice is the structure L2 , ≤, ≤p where for all x, y, x′ , y ′ ∈ L, (x, y ) ≤ (x′ , y ′ ) (x, y ) ≤p (x′ , y ′ ) if and only if x ≤ x′ and y ≤ y ′ if and only if x ≤ x′ and y ′ ≤ y

The order ≤ on L2 is called the product order, while ≤p is called the precision order. Both orders are complete lattice orders on L2 . We are interested only in a subset of L2 . A pair (x, y ) is consistent if x ≤ y and exact if x = y . The set of consistent pairs is denoted by Lc . A basic intuition in approximation theory is that a consistent pair (x, y ) approximates an element by a lower and an upper bound. Hence, (x, y ) approximates any element in the interval [x, y ] = {z ∈ L | x ≤ z ≤ y }. More precise pairs approximate

Well-founded and Stable Semantics of Logic Programs with Aggregates

5

fewer elements: (x, y ) ≤p (x1 , y1 ) implies [x, y ] ? [x1 , y1 ]. Pairs (x, x) are called exact because they approximate a single element x. The set of exact pairs represents the embedding of L in Lc . The product order is a complete lattice order on Lc while ≤p is chain-complete on Lc . Hence, any ≤-monotone or ≤p -monotone operator on Lc has a least ?xpoint in the ≤ or ≤p order. Notice also that (⊥, ?) is the ≤p -least element of Lc while the ≤p -maximal elements of Lc are precisely the set of exact elements. Example 2.1 Consider the lattice T WO = {f , t} of classical truth values ordered as f < t. We denote the set T WOc of consistent approximations of T WO with T HREE . ?, ? The set T HREE corresponds to the set of truth values {? f, u t} used in threevalued logic. The exact pairs (f , f ) and (t, t), called false and true correspond to ? , called unde?ned. The product the values ? f and ? t, while (f , t) corresponds to u ? <? order on T HREE corresponds to the truth order ? f <u t. The precision order ? ? ? <p t, and is sometimes called the ? <p f , u on T HREE corresponds to the order u knowledge order. We can de?ne logical connectives in T HREE in the following way. Conjunction ∧ and disjunction ∨ of two elements are de?ned as the greatest lower bound and the least upper bound with respect to the product order ≤. The negation operator ? =u ? . The is de?ned as ?(x, y ) = (?y, ?x). In particular, ?? f =? t, ?? t=? f , and ?u truth tables of the connectives ∧, ∨, and ? are the same as in Kleene’s strong three-valued logic. De?nition 2.1 (Approximating Operator ) Let O : L → L be an operator on a complete lattice L, ≤ . We say that A : Lc → Lc is an approximating operator of O if the following conditions are satis?ed: ? A extends O, i.e., A(x, x) = (O(x), O(x)) for every x ∈ L; ? A is ≤p -monotone. We denote the projections of an approximating operator A : Lc → Lc on the ?rst and second components with A1 and A2 , i.e., if A(x, y ) = (u, v ) then A1 (x, y ) = u and A2 (x, y ) = v . There is a simple and natural intuition behind the concept of an approximating operator A. Any tuple (x, y ) ∈ Lc can be viewed as a non-empty interval [x, y ] = {z | x ≤ z ≤ y }. It is easy to see that for any z ∈ [x, y ], A(x, y ) ≤p A(z, z ) = (O(z ), O(z )) which means that the set O([x, y ]) = {O(z ) | z ∈ [x, y ]} is a subset of the interval A(x, y ). Hence, A1 (x, y ) is a lower estimate and A2 (x, y ) is an upper estimate to O(z ), for each z in [x, y ]. The ≤p -monotonicity of A guarantees that A has a least ?xpoint called the Kripke-Kleene ?xpoint of A and denoted by KK (A). This ?xpoint approximates all ?xpoints of O, i.e., if x = O(x) then KK (A) ≤p (x, x). Next we de?ne the stable and well-founded ?xpoints of A. With a ?xed element b ∈ L, we can associate an operator A1 (·, b) mapping any x ∈ [⊥, b] to A1 (x, b). The operator A1 (·, b) is monotone but as a function from [⊥, b] to L, in general it is not

6

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

internal in [⊥, b]. Similarly, for a ?xed element a ∈ L, the operator A2 (a, ·) : [a, ?] → L is monotone, but in general is not internal in [a, ?]. De?nition 2.2 Let L, ≤ be a complete lattice. The upper stable operator St↑ A : L → L is de?ned as

2 St↑ A (a) = glb({x ∈ [a, ?] : A (a, x) ≤ x})

and the lower stable operator St↓ A : L → L is de?ned as:

1 St↓ A (b) = glb({x ∈ [⊥, b] : A (x, b) ≤ x}).

The upper stable operator maps a lattice element a to the greatest lower bound of the set of pre-?xpoints of A2 (a, ·). If A2 (a, ·) is internal in [a, ?] then due to its monotonicity, St↑ A (a) is its least ?xpoint. The lower stable operator maps a lattice element b to the greatest lower bound of the set of pre-?xpoints of A1 (·, b). This set 1 may be empty, in which case St↓ A (b) = ?. However, if A (·, b) is internal in [⊥, b], ↓ then StA (b) is its least ?xpoint. De?nition 2.3 The stable revision operator S tA : L2 → L2 where L, ≤ is a complete lattice is de?ned as follows:

↑ S tA (a, b) = (St↓ A (b), StA (a)).

In general, the stable revision operator is not internal in the set Lc . However, there is a subclass of Lc on which this operator has very nice properties. It is de?ned as the intersection of the following subclasses: ? A pair (a, b) ∈ Lc is A-reliable, if (a, b) ≤p A(a, b). ? A pair (a, b) ∈ Lc is A-prudent, if a ≤ St↓ A (b). It is easy to see that if (a, b) is A-reliable, then the operators A1 (·, b) and A2 (a, ·) are internal in their domain. On the other hand, if (a, b) is A-prudent, we can guarantee that a is a safe underestimate of all ?xpoints below b of the operator O. Intuitively, the stable revision operator implements two quite di?erent approximation processes, one to re?ne the upper estimate b and one to re?ne the lower estimate a. Given a current upper estimate b, we compute a new lower estimate by an iterative process x0 = ⊥, x1 = A1 (x0 , b), . . . , xi+1 = A1 (xi , b), . . . until a ?xpoint is reached. In each stage, we use A to approximate O([xi , b]) from below, i.e., by setting xi+1 := A1 (xi , b) ≤ O(z ), for each z ∈ [xi , b]. It is easy to see that each computed xi is a lower estimate to each ?xpoint of O below b, and the limit St↓ A (b) is the best lower bound we can obtain through A to the set of these ?xpoints. On the other hand, the re?ned upper estimate is computed as a limit of the sequence y0 = a, y1 = A2 (a, y0 ), . . . , yi+1 = A2 (a, yi ), . . . . The goal is to eliminate non-minimal, non-reachable ?xpoints of O above the current lower estimate a. Assuming that a ≤ O(a)(= A2 (a, a) = y1 ), all points in [a, O(a)] are considered reachable. On the next level, also points in O([a, O(a)]) above a are of interest, and we can approximate these points from above by computing A2 (a, y1 ) = y2 . This

Well-founded and Stable Semantics of Logic Programs with Aggregates

7

process is continued until the ?xpoint St↑ A (a) is reached and this ?xpoint is taken as the new upper bound. In (Denecker et al. 2004), it was shown that the set Lrp of pairs that are A-reliable and A-prudent contains (⊥, ?), is chain-complete, and the stable revision operator is an internal, ≤p -monotone operator in Lrp . It follows that this operator has a least ?xpoint, called the well-founded ?xpoint of A and denoted by W F (A). All consistent ?xpoints of S tA are A-reliable and A-prudent. They are called stable ?xpoints of A and they are ≤-minimal ?xpoints of A. The subset of exact stable ?xpoints is denoted by ST (A). Exact stable ?xpoints can be characterized alternatively as follows: x ∈ L is an exact stable ?xpoint if and only if O(x) = x and lfp(A1 (·, x)) = x. We have the following lemma. Lemma 2.1 A stable ?xpoint of A is a minimal pre-?xpoint of O. The inverse however is not true: not every minimal pre-?xpoint of O is a stable ?xpoint of A. Proof Let x be a stable ?xpoint of A and y a pre-?xpoint of O such that y ≤ x. By antimonotonicity of A1 in the second argument, it holds that A1 (y, x) ≤ A1 (y, y ) = O(y ) ≤ y . Hence, y is a pre-?xpoint of A1 (·, x) and since x is the least ?xpoint of this monotone operator, this implies that x ≤ y . In general, a lattice operator O : L → L may have many approximating operators. For any pair A, B of approximations of O, we de?ne A ≤p B if and only if for each (x, y ) ∈ Lc , A(x, y ) ≤p B (x, y ). The following result about the relationship between the di?erent classes of ?xpoints of A and B was proven in (Denecker et al. 2004). Theorem 2.1 If A ≤p B , then KK (A) ≤p KK (B ), W F (A) ≤p W F (B ) and ST (A) ? ST (B ). So, more precise approximating operators lead to more precise Kripke-Kleene and Well-founded ?xpoints, and to more exact stable ?xpoints. It turns out that O has a most precise approximation UO called the ultimate approximation of O. It is de?ned as: UO (x, y ) = (glb(O([x, y ])), lub(O([x, y ]))) where O([x, y ]) = {O(z ) | z ∈ [x, y ]}. The Kripke-Kleene, stable and well-founded ?xpoints of UO are called the ultimate Kripke-Kleene, ultimate stable and ultimate well-founded ?xpoints of O. Theorem 2.2 (Denecker et al. 2004) The ultimate Kripke-Kleene and ultimate well-founded ?xpoint of O is the most precise of all Kripke-Kleene and well-founded ?xpoints of all approximations of O. The set of ultimate exact stable ?xpoints includes all exact stable ?xpoints of all approximations A of O. A special case arises when O is monotone.

8

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

Theorem 2.3 (Denecker et al. 2004) If O is monotone, then for every (x, y ) ∈ Lc , UO (x, y ) = (O(x), O(y )) and its ultimate well-founded ?xpoint is exact and is the least ?xpoint of O. In (Denecker et al. 2000), it was shown that the Kripke-Kleene, the well-founded and the stable semantics of a logic program P correspond to Kripke-Kleene, wellfounded and exact stable ?xpoints of the three-valued immediate consequence operator ΦP of P de?ned by Fitting (1985). In (Denecker et al. 2003), analogous results were obtained in the context of default and autoepistemic logic. This shows that approximation theory formalizes an important non-monotonic principle. 3 Aggregates 3.1 Aggregate Functions and Relations In this text, an aggregate is understood as a second-order n-ary function or relation having at least one set argument. For simplicity, we assume that n = 1 in case of aggregate functions and n = 2 in case of aggregate relations. We denote the powerset of a set D with ?(D). De?nition 3.1 (Aggregate Functions and Relations ) Let D1 and D2 be domains. An aggregate function is any function f : ?(D1 ) → D2 . An aggregate relation is any relation r ? ?(D1 ) × D2 . We use f to denote an aggregate function and r to denote an aggregate relation. Although many aggregates are functions, for uniformity and convenience sake, our theory below is developed for aggregate relations. If an aggregate function f is used in a context which requires an aggregate relation, f is understood as its graph Gf which is the aggregate relation de?ned as Gf = {(S, d) | f(S ) = d}. We now de?ne a number of standard aggregate functions and relations which we study in this paper. We start with aggregate relations in the context of a poset D, ≤ : De?nition 3.2 ? glb ? ?(D) × D - de?ned as {(S, d) | S ∈ ?(D) and d = glb(S )}. ? lub ? ?(D) × D - de?ned as {(S, d) | S ∈ ?(D) and d = lub(S )}. ? lb ? ?(D) × D - de?ned as {(S, d) | ?x ∈ S, d ≤ x}. ? ub ? ?(D) × D - de?ned as {(S, d) | ?x ∈ S, x ≤ d}. ? min ? ?(D) × D - de?ned as {(S, d) | d is a minimal element of S }. ? max ? ?(D) × D - de?ned as {(S, d) | d is a maximal element of S }. The aggregate relations glb and lub are (graphs of) partial aggregate functions. If D, ≤ is a complete lattice then glb and lub are (graphs of) total aggregate functions. If D, ≤ is a totally ordered set then min and max represent partial functions. If in addition D is ?nite then min and max represent total functions and min = glb and max = lub. Next, we de?ne aggregate functions on ?nite sets of numbers. Below, we assume that D is an arbitrary domain and D′ is a Cartesian product D1 × · · ·× Dn in which D1 is the set of real numbers R. Also, we denote the set of all ?nite subsets of a domain D by ?F (D).

Well-founded and Stable Semantics of Logic Programs with Aggregates De?nition 3.3 ? card : ?F (D) → N de?ned as card(S ) = |S |, the cardinality of S ; ? sum : ?F (D′ ) → R de?ned as sum(S ) = ? prod : ?F (D′ ) → R de?ned as prod(S ) = x1 ; x1 ;

(x1 ,...,xn )∈S

9

(x1 ,...,xn )∈S

? avg ? ?F (D′ ) × R (Average) - the graph of a partial aggregate function de?ned only for non-empty sets as (S, d) ∈ avg if d = sum(S )/card(S ). In the de?nition of sum, prod and avg, only the ?rst element of a tuple is used to compute the value. The reason to introduce the other arguments is to be able to count one number multiple times. That is, a set S ? R × D2 × · · · × Dn represents a multiset of real numbers. For example, when counting the total capacity of a building consisting of di?erent rooms, we need to count the capacity of a room as many times as there are rooms with that capacity. All these aggregate functions have no natural extensions to in?nite sets. However, their graphs Gf can be considered as aggregate relations on arbitrary sets — containing only tuples (S, d) for which S is ?nite. In this paper, we will focus only on aggregates with one set argument but our theory can be extended easily to the more general case. An example of an aggregate relation with two set arguments is the generalized quanti?er most ? ?(D) × ?(D) where most(A, B ) expresses that most A’s are B’s. The relation most is de?ned as the set of all pairs of sets (A, B ) such that card(A ∩ B ) > card(A \ B ).

3.2 Derived Aggregate Relations In this section we show how to obtain new aggregate relations by composition of existing aggregates with other relations. De?nition 3.4 The composition of an aggregate relation r ? ?(D1 ) × D2 with a binary relation P ? D2 × D3 is the aggregate relation rP ? ?(D1 ) × D3 de?ned as: rP = {(S, d) | ?d′ ∈ D2 : (S, d′ ) ∈ r and (d′ , d) ∈ P }. The composition of an aggregate function f : ?(D1 ) → D2 with a binary relation P ? D2 × D3 is the aggregate relation fP ? ?(D1 ) × D3 de?ned as: fP = {(S, d) | (f(S ), d) ∈ P }. Typically, the binary relation P is some partial order relation on the domain D2 . For example, the card≥ aggregate relation is obtained as the composition of the card aggregate function with the ≥ relation on N and contains all pairs (S, n) such that card(S ) ≥ n. An aggregate relation can also be composed with a relation on sets. We consider only one instance of this sort of composition.

10

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

De?nition 3.5 The subset aggregate of an aggregate relation r ? ?(D1 ) × D2 is the aggregate r? ? ?(D1 ) × D2 de?ned as: r? = {(S, d) | ?S ′ : (S ′ , d) ∈ r ∧ S ′ ? S }. For an aggregate function f, f? denotes the subset aggregate of the graph of f. As an example, card? (S, d) holds if for some subset S ′ ? S , card(S ′ ) = d. In this case, the two derived aggregates card? and card≥ are identical. This is because there exists a subset S ′ ? S such that card(S ′ ) = d if and only if card(S ) ≥ d. 3.3 Monotone and Anti-monotone Aggregates We de?ne two di?erent notions of monotonicity of aggregates, one for functions and one for relations, and then show how they are related. De?nition 3.6 Let D2 , ≤ be a poset and f : ?(D1 ) → D2 an aggregate function. We say that f is: ? monotone if S1 ? S2 implies f(S1 ) ≤ f(S2 ); ? anti-monotone if S1 ? S2 implies f(S1 ) ≥ f(S2 ). The next two propositions list standard aggregate functions which are monotone or anti-monotone with respect to some partial order. Proposition 3.1 Let D, ≤ be a complete lattice. The aggregate function glb : ?(D) → D is antimonotone with respect to ≤ and the aggregate function lub : ?(D) → D is monotone with respect to ≤. Proof Standard result from lattice theory (Davey and Pristley 1990, Lemma 2.22). In Table 1 we use the following notation for subsets of real numbers: R+ for the set of non-negative numbers, R? for the set of non-positive numbers, R[1,∞) for the set of numbers in the interval [1, ∞), and R[0,1) for the set of numbers in the interval [0, 1). Proposition 3.2 Let D be a Cartesian product D1 × · · · × Dn where n ≥ 1. The aggregate functions in Table 1 from ?F (D), the set of ?nite subsets of D, to the poset D′ , ≤ are monotone when D1 is as given in the table. Proof Follows immediately from well-known properties of real numbers. Monotonicity and anti-monotonicity of an aggregate relation are de?ned in the following way.

Well-founded and Stable Semantics of Logic Programs with Aggregates

aggregate card sum sum prod prod D1 arbitrary R+ R? R[1,∞) R[0,1) D′ , ≤ N, ≤ R+ , ≤ R? , ≥ R[1,∞) , ≤ R[0,1) , ≥

11

Table 1. Monotone aggregate functions on ?nite sets De?nition 3.7 Let r ? ?(D1 ) × D2 be an aggregate relation. We say that r is: ? monotone if (S1 , d) ∈ r and S1 ? S2 implies (S2 , d) ∈ r; ? anti-monotone if (S2 , d) ∈ r and S1 ? S2 implies (S1 , d) ∈ r. The next proposition summarizes the (anti-)monotonicity properties of the aggregate relations de?ned in De?nition 3.2. Proposition 3.3 The aggregate relations lb, ub ? ?(D) × D on a poset D, ≤ are anti-monotone. All other relations de?ned in De?nition 3.2 are neither a monotone nor an antimonotone. We point out that the graph of a monotone aggregate function is not a monotone aggregate relation according to De?nition 3.7. For example, lub is a monotone aggregate function but its graph is not a monotone aggregate relation. Instead, the composition of an aggregate function f with the inverse of the order with respect to which it is monotone results in a monotone aggregate relation. Proposition 3.4 Let f : ?(D1 ) → D2 be an aggregate function which is monotone with respect to a partial order relation ≤ on D2 . Then f≥ and f> are monotone aggregate relations and f≤ and f< are anti-monotone aggregate relations. Proof f≥ : Consider two sets S1 and S2 such that S1 ? S2 ? D1 and an element d ∈ D2 . Suppose that f≥ (S1 , d) holds. By de?nition of f≥ this is equivalent to f(S1 ) ≥ d. Since f is monotone we also have that f(S1 ) ≤ f(S2 ). So, we can conclude f(S2 ) ≥ d which is equivalent to f≥ (S2 , d). The monotonicity of f> and the anti-monotonicity of f≤ and f< can be proven in a similar fashion. As an application of this result we have that the aggregate relations card≥ and card> are monotone since the aggregate function card is monotone with respect to ≤. Forming the subset aggregate of any aggregate relation always results in a monotone aggregate relation.

12

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

Proposition 3.5 Let r ? ?(D1 ) × D2 be an arbitrary aggregate relation. 1. r? is a monotone aggregate relation. 2. If r is a monotone aggregate relation then r? = r.

4 First-order Logic with Aggregates We introduce aggregates in the context of many-sorted ?rst-order logic. A sort symbol (or simply sort) s denotes some sub-domain of the domain of discourse. A product type s1 × · · · × sn represents the product of the domains represented by the sorts s1 , . . . , sn and a set type {s} represents the set of all sets of elements of sort s. De?nition 4.1 (Aggregate Signature ) An aggregate signature Σ is a tuple S ; F ; P ; A where ? ? ? ? S is a set of sorts; F is a set of sorted function symbols f : s1 × · · · × sn → w where n ≥ 0; P is a set of sorted predicate symbols p : s1 × · · · × sn where n ≥ 0; A is a set of sorted aggregate symbols r : {s1 × · · · × sn } × w where n ≥ 1.

We use Sort(Σ), F unc(Σ), P red(Σ), and Aggr(Σ) to denote the sets S , F , P , and A of Σ. We call a function symbol of the form f : → w a constant. An aggregate symbol r : {s1 × · · · × sn } × w denotes an aggregate relation between sets of type s1 × · · · × sn and objects of sort w. Of course, Aggr(Σ) may contain many instances of the same type of aggregate relation but with di?erent sorts. For each sort s, we assume an in?nite set Vs of variables of sort s disjoint from the constants in F unc(Σ). We denote variables, predicate symbols and function symbols with small letters and constants with capital letters. De?nition 4.2 (Terms and atoms ) Let Σ be an aggregate signature. For every sort s ∈ S , we de?ne the set of terms of type s by induction: ? a variable x ∈ Vs of sort s is a term of type s; ? if f : s1 × · · · × sn → w ∈ F unc(Σ) and t1 , . . . , tn are terms of type s1 , . . . , sn respectively, then f (t1 , . . . , tn ) is a term of type w. An atom has the form p(t1 , . . . , tn ) where p : s1 × · · · × sn ∈ P red(Σ) is a predicate symbol and t1 , . . . , tn are terms of types s1 , . . . , sn respectively. For a ?xed aggregate signature Σ we de?ne the notions of set expressions, aggregate atoms and formulas of the logic by simultaneous induction.

Well-founded and Stable Semantics of Logic Programs with Aggregates

13

De?nition 4.3 A set expression of type {s1 ×· · ·× sn } has the form {(x1 , . . . , xn ) | ?} where ? is an aggregate formula called the condition of the expression and for each i = 1, . . . , n, xi is a variable of sort si . An aggregate atom has the form r(s, t) where r : {s1 × · · · × sn } × w ∈ Aggr(Σ) is an aggregate symbol, s is a set expression of type {s1 × · · · × sn }, and t is a term of type w. An aggregate formula is an atom, an aggregate atom, or an expression of the form ??, ? ∧ ψ , ? ∨ ψ , ?x? and ?x? where ? and ψ are aggregate formulas and x a variable. We also use ? ? ψ as an abbreviation for ? ∨ ?ψ . The set of aggregate formulas over Σ is denoted by Laggr . Σ We illustrate the syntax of aggregate formulas with an example of modeling power plant maintenance. Example 4.1 (Power Plant Maintenance ) A power plant has a number of power generators called units which have to be scheduled for maintenance. There is a restriction on the total capacity of the units in maintenance. Consider the following aggregate signature: Σ = {u, w, nat}; {M ax : nat}; {capacity : u × nat, maint : u × w × w}; {sum : {nat × u} × nat} . The sort u is interpreted with units and the sort w with weeks. The predicate capacity (u, c) represents that a unit u has a capacity c. The predicate maint(u, s, e) speci?es that unit u is in maintenance during the period starting at time point s (inclusive) and ending at time point e (exclusive). The following aggregate formula expresses that the total capacity of the units in maintenance during a week, should not exceed a value M ax: ?w sum≤ ({(c, u) | ?s?e(maint(u, s, e) ∧ s ≤ w < e ∧ capacity (u, c))}, M ax). In this formula the sum aggregate computes the sum of all capacities c of units u that are in maintenance during week w. Note that each capacity c is counted as many times as there are units u with capacity c. A positive literal is an atom p(t1 , . . . , tn ) and a negative literal is the negation of an atom ?p(t1 , . . . , tn ). An occurrence of a variable x in an aggregate formula ψ is bounded if it occurs in a subformula ?x? or ?x? of ψ or in a set expression {(x1 , . . . , x, . . . , xn ) | ?} in ψ . An occurrence of x in ψ is free if it is not bounded. The set of free variables of ψ , denoted by F ree(ψ ), is the set of all variables with at least one free occurrence in ψ . Terms and formulas without variables are called ground and those without free variables are called closed. Now, we de?ne the semantics of the logic. Let Σ be an aggregate signature. De?nition 4.4 (Structure ) A Σ-structure D consists of the following:

14

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe ? for each sort s ∈ S a domain sD ; ? for each function symbol f : s1 × · · · × sn → w ∈ F unc(Σ) a function

D D f D : sD 1 × · · · × sn → w ;

? for each predicate symbol p : s1 × · · · × sn ∈ P red(Σ) a relation

D p D ? sD 1 × · · · × sn .

? for each aggregate symbol r : {s1 × · · · × sn } × w ∈ Aggr(Σ) an aggregate D D relation rD ? ?(sD 1 × · · · × sn ) × w . Consider a Σ-formula ?(x1 , . . . , xn ) with free variables x1 , . . . , xn of sorts s1 , . . . , sn , D respectively and let d1 , . . . , dn be elements of sD 1 , . . . , sn , respectively. Then, ?(d1 , . . . , dn ) denotes the formula obtained by substituting di for each free occurrence of xi in ?. So, we consider domain elements as new constants of the respective sorts. We denote this enlarged signature with Σ(D) and the corresponding set of formulas with Laggr Σ(D ) . De?nition 4.5 The value t D of a ground term t for a Σ-structure D is de?ned inductively as follows: ? if t is a domain element d, then t D = d; ? if t is a constant c, then t D = cD ; ? if t is a term f (t1 , . . . , tn ), then t D = f D ( t1

D, . . . ,

tn

D ).

In the following de?nition and in the rest of the paper we often treat a relation R ? D as a function R : D → {f , t} de?ned as R(d) = t if and only if d ∈ R for an element d ∈ D. De?nition 4.6 (Truth function ) Given is a Σ-structure D. We de?ne the value {x | ?} D of a set expression {x | ?} and the truth value HD (ψ ) of an aggregate formula ψ by simultaneous induction. The value {(x1 , . . . , xn ) | ?(x1 , . . . , xn )} D of a set expression is the set

D {(d1 , . . . , dn ) ∈ sD 1 × · · · × sn | HD (?(d1 , . . . , dn )) = t}

The truth function HD (·) : Laggr Σ(D ) → T WO for closed aggregate formulas is de?ned in the following way: HD (p(t1 , . . . , tn )) HD (r({x | ?}, t)) HD (??) HD (? ∨ ψ ) HD (? ∧ ψ ) HD (?x?(x)) HD (?xψ (x)) = p D ( t1 D , . . . , tn = rD ( {x | ?} D , t = ?HD (?) = HD (?) ∨ HD (ψ ) = HD (?) ∧ HD (ψ ) = d∈sD HD (?(d)) = d∈sD HD (ψ (d))

D) D)

(where s the sort of x) (where s the sort of x)

We de?ne D |= ? if HD (?) = t. When D |= ? we call D a model of ?. The relation |= is called the truth relation or the satis?ability relation. When the structure D

Well-founded and Stable Semantics of Logic Programs with Aggregates

15

is clear from the context, we drop the subscript D from the valuation function · and truth function H. We illustrate the use of ?rst-order logic with aggregates to formalize the wellknown magic square problem. Example 4.2 (Magic Square ) Given is a n × n grid which has to be ?lled with the integer numbers from 1 to n2 such that the sum of the numbers in all rows, columns, and two diagonals is equal to the same number M (n), known as the magic constant: n(n2 + 1) 2 Consider the following aggregate signature: M (n) = Σ = {pos, nat}; {+ : nat × nat → nat, ? : nat × nat → nat, / : nat × nat → nat, Dim : nat, M c : nat, f : pos × pos → nat}; ?; {sum : {nat} × nat} The sort pos represents the positions of the table and the sort nat the values of the table. The function symbol f speci?es the number in the corresponding row and column, the constant Dim gives the dimension of the grid, and the constant M c gives the magic number. The problem is modeled by the following theory T : M c = Dim ? (Dim ? Dim + 1)/2 ?x?y (1 ≤ f (x, y ) ≤ Dim ? Dim) ?x1 ?x2 ?y1 ?y2 (f (x1 , y1 ) = f (x2 , y2 ) → x1 = x2 ∧ y1 = y2 ) ?y sum({z | ?x(z = f (x, y ))}, M c) ?x sum({z | ?y (z = f (x, y ))}, M c) sum({z | ?x(z = f (x, x))}, M c) sum({z | ?x(z = f (x, Dim + 1 ? x))}, M c) Consider any structure D such that DimD = n ∈ N, posD = {1, . . . , n} and natD = N. Then D is a model of T if and only if f D speci?es a solution for the magic square problem of dimension n. 5 Aggregate Programs In this section, we de?ne the syntax of aggregate programs and introduce a basic semantical tool, the TP operator. Given are an aggregate signature Σ and a set of sorted predicate symbols Π. We call the symbols from Σ pre-de?ned or interpreted while those from Π de?ned. With Σ(Π) we denote the aggregate signature consisting of both sets of symbols. From now until the end of this paper, we will assume a ?xed aggregate signature Σ and a Σ-structure D interpreting the pre-de?ned symbols. Remark 1 Some of the pre-de?ned symbols are interpreted on standard domains like:

16

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe ? sort symbols nat, int, real interpreted by the sets of natural, integer and real numbers respectively; ? the standard function symbols +, ?, ?, . . . on these sorts interpreted as the corresponding operations on numbers; ? the standard predicate symbols =, ≤, . . . on these sorts interpreted as the corresponding relations on numbers; ? all aggregate symbols de?ned in Section 3.1: card, min, max, sum, . . . .

Other interpreted symbols may be domain-speci?c. In the context of logic programming, the interpretation of the set Sd ? Sort(Σ) of domain-speci?c sorts and the set Fd ? F unc(Σ) of domain-speci?c function symbols is normally given by the free term algebra generated by Fd . The interpretations sD of all sorts s ∈ Sd and the interpretation f D of all function symbols f : s1 × · · · × sn → s ∈ Fd are de?ned by simultaneous induction as follows:

D D ? If t1 ∈ sD 1 , . . . , tn ∈ sn , then f (t1 , . . . , tn ) ∈ s . D D D ? If t1 ∈ s1 , . . . , tn ∈ sn , then f (t1 , . . . , tn ) = f (t1 , . . . , tn ).

In case there is only one domain-speci?c sort, the free term algebra corresponds to the Herbrand pre-interpretation, i.e., the Herbrand universe and the Herbrand interpretation of function symbols. The value of domain speci?c pre-de?ned predicate symbols may be de?ned by an extensional database on the domain of D. A Σ(Π)-aggregate rule r is of the form A←? where A is an atom of a de?ned predicate and ? is a Σ(Π)-aggregate formula. Note that ? may contain universal quanti?ers. The atom A is called the head of the rule and the formula ? the body. We use body (r) to denote the body ? of r. A Σ(Π)aggregate program is a (possibly in?nite) set of aggregate rules. A normal aggregate program is an aggregate program in which the bodies of all rules are conjunctions of literals and aggregate atoms. Now, we introduce the basic semantical constructs. The D-base baseD (Π) of Π is de?ned as baseD (Π) = {p(d1 , . . . , dn ) | p : s1 × · · · × sn ∈ Π, and

D d1 ∈ sD 1 , . . . , dn ∈ sn }.

The semantics of an aggregate program will be de?ned in the collection of Σ(Π)structures extending D. For each subset I of baseD (Π), we de?ne the Σ(Π)-structure D(I ) extending D such that for every atom A ∈ baseD (Π): HD(I ) (A) = t if and only if A ∈ I . Clearly, this is a one-to-one correspondence between the subsets of baseD (Π) and Σ(Π)-extensions of D. In the rest of the paper, we exploit this correspondence and use subsets of baseD (Π), called interpretations, to represent Σ(Π)-extensions of D. Sometimes, we also view an interpretation I as a mapping I : baseD → T WO. An interpretation I is a model of an aggregate program P if I is a model of the

Well-founded and Stable Semantics of Logic Programs with Aggregates

17

?rst-order theory obtained from P by turning every rule A ← ? into an implication ?x(A ? ?) where x are the free variables of A and ?. The set I = ?(baseD (Π)) forms a complete lattice under the subset order ?. This order extends to Σ(Π)-structures as follows: D(I ) ≤ D(J ) if and only if I ? J . We introduce the following notation. For any closed de?ned atom A = p(t1 , . . . , tn ), A D denotes the atom p( t1 D , . . . , tn D ) ∈ baseD (Π). De?nition 5.1 The instantiation of a program P over a structure D is de?ned as the set instD (P ) of all closed rules A ← ? such that: ? there exists a rule A′ ← ?′ ∈ P with free variables x1 , . . . , xm of sorts s1 , . . . , sm , and D ? there exist domain elements d1 ∈ sD 1 , . . . , dm ∈ sm , and ′ ? A = A (d1 , . . . , dm ) D and ? ? = ?′ (d1 , . . . , dm ). Note that the body of a rule in the instantiation of an aggregate program is a closed formula containing domain elements. We now de?ne the two-valued immediate consequence operator of an aggregate program P . De?nition 5.2 aggr The two-valued immediate consequence operator TP, D : I → I of an aggregate program P is de?ned as:

aggr = ?}. TP, D (I ) = {A | A ← ? ∈ instD (P ) and D (I ) |

This operator extends the TP operator for normal logic programs de?ned by van Emden and Kowalski (1976). As for standard logic programs we have a correspondence between models of an aggr aggregate program P and pre-?xpoints of TP, D . Proposition 5.1 An interpretation I is a model of an aggregate program P if and only if I is a aggr aggr pre-?xpoint of TP, D , i.e., TP,D (I ) ≤ I . Proof The proof is straightforward extension of the proof for standard logic programs.

De?nition 5.3 An interpretation I is a supported model of an aggregate program P extending D aggr if I is a ?xpoint of TP, D . Although the supported model semantics is generally considered to be a weak semantics there are problems with aggregates for which it is the appropriate semantics. One such example is the Party Invitation problem (Ross and Sagiv 1997).

18

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

Example 5.1 (Party Invitation ) A number of people are invited to a party. A person p will accept the invitation if and only if at least k of his (her) friends also accept the invitation. Consider the following aggregate signature: Σ = {person, nat}; {A : person, B : person}; {thr : person × nat, f riend : person × person}; {card : {person} × nat} and let Π = {accept : person}. Here f riend(x, y ) means that y is a friend of x and thr(x, t) gives the lower bound t on the number of friends of x. The problem can be modeled by the following single rule: accept(x) ← thr(x, t) ∧ card≥ ({y | f riend(x, y ) ∧ accept(y )}, t). Consider an instance of the problem with two friends, say A and B . Each one of them accepts the invitation if and only if the other one accepts as well. This is represented by the Σ-structure D in which personD = {A, B } and in which f riendD and thrD are given by the following table: f riend(A, B ). f riend(B, A). thr(A, 1). thr(B, 1).

The aggregate program has two supported models in which accept is ? and {A, B } respectively. The second solution is not minimal but it is a correct solution to the problem. In reality, A and B may communicate with each other about their decisions to attend the party. Several other examples for which the supported model semantics is appropriate, including an elaborated version of the Party Invitation problem, can be found in (Pelov 2004). It is worth noting that each of these examples can also be expressed in ?rst order logic with aggregates using the completion of the aggregate program. 5.1 De?nite Aggregate Programs In the context of logic programming, de?nite logic programs are negation free logic programs. A de?nite program P characterizes a monotone TP operator and its intended semantics is the least ?xpoint of TP . In this section, we extend the notion of de?nite program to programs with aggregates. We de?ne the notions of positive, negative, and neutral aggregate formulas. This de?nition is not entirely syntactic, but also depends on the monotonicity or antimonotonicity of aggregate symbols appearing in the formula. We can do that because aggregate symbols always have a ?xed interpretation given by the structure D. De?nition 5.4 An occurrence of a predicate P (resp. a formula ψ ) in an aggregate formula ? is neutral if it occurs in the condition θ of an aggregate atom r({x | θ}, t) in ? such

Well-founded and Stable Semantics of Logic Programs with Aggregates

19

that rD is neither monotone nor anti-monotone aggregate relation. Otherwise, the occurrence of P (resp. ψ ) is positive if the number of negations and aggregate atoms interpreted with an anti-monotone aggregate relation above P (resp. ψ ) is even and negative if the number of negations and aggregate atoms interpreted with an anti-monotone aggregate relation above P (resp. ψ ) is odd. De?nition 5.5 (Positive and Negative Aggregate Formulas ) An aggregate formula ? is positive if no de?ned predicate occurs negatively or neutrally in ?. An aggregate formula ? is negative if no de?ned predicate occurs positively or neutrally in ?. We note that in the above de?nition the polarity of pre-de?ned symbols does not matter. Moreover, if a formula does not contain de?ned atoms then it is both positive and negative. If the formula ? is an aggregate atom of the form r({x | ?}, t) there are three cases in which it can be positive. The ?rst one is when rD is a monotone aggregate relation and ? is a positive formula. The second case is when rD is an anti-monotone aggregate relation and ? is a negative formula. The third one is when rD is arbitrary and ? does not contain de?ned predicates. Similarly, the aggregate atom r({x | ?}, t) is negative if rD is a monotone aggregate relation and ? is negative, rD is an anti-monotone aggregate relation and ? is positive, or rD is an arbitrary aggregate relation and ? does not contain de?ned symbols. The main property of positive (resp. negative) aggregate formulas is that their satis?ability is monotone (resp. anti-monotone) for a given structure D. Proposition 5.2 Let D be a Σ-structure and ψ be a closed Σ(Π)-aggregate formula (possibly containing domain elements). For any pair I ? J ∈ baseD (Π), it holds that: ? if ψ is positive then D(I ) |= ψ implies D(J ) |= ψ ; ? if ψ is negative then D(J ) |= ψ implies D(I ) |= ψ . Proof The proof is by induction on the structure of ψ . For positive and negative formulas without aggregates this property is a standard result in the theory of ?rst-order logic. We consider only the case when ψ is an aggregate atom r({x | ?(x)}, t) without free variables. Let SI = {x | ?(x)} D(I ) and SJ = {x | ?(x)} D(J ) . First, let ψ be a positive aggregate atom. We distinguish three cases. 1. rD is a monotone aggregate relation and ?(x) is a positive formula. For every wellsorted tuple d, ?(d) is a positive formula as well. By the induction hypothesis, we have that D(I ) |= ?(d) implies D(J ) |= ?(d). Consequently, SI ? SJ . Finally, because rD is a monotone aggregate relation, (SI , t D ) ∈ rD implies (SJ , t D ) ∈ rD . Thus, D(I ) |= ψ implies D(J ) |= ψ . 2. rD is an anti-monotone aggregate relation and ?(x) is a negative formula. By the induction hypothesis, for every appropriate tuple d of domain elements assigned to x, we have D(J ) |= ?(d) implies D(I ) |= ?(d). Consequently, SJ ? SI . Finally, because rD is an anti-monotone aggregate relation, (SI , t D ) ∈ rD implies (SJ , t D ) ∈ rD . Thus, D(I ) |= ψ implies D(J ) |= ψ .

20

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

3. If ? contains no de?ned predicates, then D(I ) |= ψ if and only if D(J ) |= ψ if and only if D |= ψ . The proof of anti-monotonicity of negative aggregate atoms is similar and is omitted. We point out that the class of positive (resp. negative) formulas are a strict subset of the class for which the satis?ability relation is monotone (resp. anti-monotone). For example the formula p ∨ ?p is a tautology and hence it is monotone, however it is neither positive nor negative. De?nition 5.6 A de?nite aggregate program is an aggregate program such that the bodies of all rules are positive aggregate formulas. The class of de?nite aggregate programs is an extension of the class of de?nite logic programs and has a monotone immediate consequence operator. Theorem 5.1 aggr If P is a de?nite aggregate program then TP, D is monotone. Proof Follows immediately from Proposition 5.2. De?nition 5.7 We de?ne the least ?xpoint model of a de?nite Σ(Π)-aggregate program P extending aggr D as the least ?xpoint of its immediate consequence operator TP, D . A well-known example that can be modeled as a de?nite aggregate program, is the Company Control problem (Kemp and Stuckey 1991; Mumick et al. 1990; Ross and Sagiv 1997; Van Gelder 1992). Example 5.2 (Company Control ) Given is a set of companies which own shares in each other. The problem is to decide if a company x has a controlling interest in a company y . This is the case when x owns (directly or through intermediate companies controlled by x) more than 50% of the stock of y . To model the problem we use the following aggregate signature: Σ = {c, s}; ?; {owns stock : c × c × s}; {sum : {s × c} × s} . The sort c represents companies and the sort s represents fractions of shares and is interpreted over the real interval [0..1]. The de?ned predicates are Π = {controls : c × c}. The predicate owns stock (x, y, s) means that a company x owns a fraction s of the stock of a company y and controls(x, y ) means that x controls y . The problem is modeled by the aggregate program consisting of the following rule: controls(x, y ) ← sum> ({(s, z ) | (x = z ∨ controls(x, z ))∧ owns stock (z, y, s)}, 0.5).

Well-founded and Stable Semantics of Logic Programs with Aggregates

21

For numbers in the interval [0..1], the sum aggregate function is monotone with respect to ≥. Consequently, by Proposition 3.4, sum> is a monotone aggregate relation. Further, the formula in the aggregate atom is a positive formula, so the aggregate atom in the last rule is monotone. Since none of the bodies contain aggr negation this is a de?nite aggregate program with a monotone TP, D operator which has a least ?xpoint I .

aggr We will now show that the least ?xpoint of TP, D corresponds to the solution to the company control problem. We start by giving a more precise de?nition of the control relation. Let sh(a, b) be a function which returns the fraction of shares of a company a in a company b or 0 if a does not have shares in b. We de?ne for every n ∈ N the level n control binary relation, denoted by C n , by induction on n as follows:

? C 0 = ?, i.e., no company has level 0 control of another company; ? C n+1 = {(a, b) | sh(a, b) + (a,c)∈C n sh(c, b) > 0.5} for n ≥ 0, i.e., a has a level n + 1 control over company b if the sum of the shares of a in b together with the shares of the companies which a has level n control in b is more than 50%. Clearly, C n is an increasing sequence of relations. We de?ne the controls relation between companies C as C = n≥0 C n , i.e., a company a controls a company b if, for some n ≥ 0, (a, b) ∈ C n . Proposition 5.3 aggr controlslfp(TP,D ) = C . Proof aggr n In = C n. Let In = TP, D ↑ (?) for n ≥ 0. We will prove for each n ≥ 0 that controls Clearly, it follows from this that controlslfp(TP,D ) = C . For n = 0, controlsI0 is empty and is equal to C n . For n > 0, assume that controlsIi = C i for i = 0, . . . , n ? 1. Fix two companies a and b and consider the value of the instance of the set expression: S = {(s, z ) | (a = z ∨ controls(a, z )) ∧ owns stock (z, b, s)} It is easy to see that if controlsIn?1 = C n?1 then S = {(s, c) | (a, c) ∈ C n?1 and c contains s shares in b} ∪ S1 where S1 = {(s, a)} if a has s shares in b and S1 = ? otherwise. It is straightforward then to see that controlsIn contains (a, b) if and only if (a, b) ∈ C n . Example 5.3 (Borel Sets ) Let R be the set of real numbers. Borel sets are de?ned by the following monotone inductive de?nition: ? any open set of real numbers is a Borel set; ? for any countable set C of Borel sets, C and C are Borel sets;

In?1 .

aggr

22

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe ? if B is a Borel set then R ? B is a Borel set.

To model this de?nition as an aggregate program consider the following aggregate signature:

ω Σ = {s}; {compl : s → s}; {open : s}; {glbω ? , lub? : {s} × s} .

The Σ-structure D interprets the sort s with the set ?(R) of all subsets of the real numbers, the predicate open is interpreted with the set of open sets, and the function compl is interpreted as set complement: complD (S ) = R ? S . The aggregate relations glbω and lubω are the restrictions of glb and lub to countable input sets, i.e., for any set R of sets of real numbers and set S of real numbers, (R, S ) ∈ glbω ω if and only if |R| ≤ ω and S = R. The aggregate relations glbω ? and lub? ω ω are obtained by forming the subset aggregates of glb and lub respectively (see De?nition 3.5). Then glbω ? (R, S ) holds if S is the intersection of some countable subset of R. Likewise lubω ? (R, S ) holds if S is the union of some countable subset of R. The program de?ning Borel sets de?nes a single de?ned predicate borel : s and contains the following rules: borel(S ) ← open(S ). borel(compl(S )) ← borel(S ).

ω borel(S ) ← glbω ? ({B | borel (B )}, S ) ∨ lub? ({B | borel (B )}, S ).

Each of these rules is the formal representation of one of the rules in the inductive ω de?nition of Borel sets. Since glbω ? and lub? are monotone aggregate relations (Proposition 3.5) this is a de?nite aggregate program and it de?nes a monotone aggr operator TP, D . Consequently, the set of Borel sets is the least set of sets closed under the rules of the inductive de?nition and this corresponds exactly to the least aggr aggr ?xpoint of TP, D . Thus, borel (d) ∈ lfp(TP,D ) if and only if d is a Borel set. 5.2 Strati?ed Aggregate programs The important class of strati?ed aggregate programs was already considered by several authors (Mumick et al. 1990; Dell’Armi et al. 2003; Faber et al. 2004). It is a natural extension of the concept of strati?ed logic program (Apt et al. 1988) where aggregates are treated as negative literals. De?nition 5.8 An aggregate program P is strati?ed if for each de?ned predicate p, there is a unique natural number p > 0 called the level of p such that if q occurs positively in the body B of a rule with head p, then q ≤ p and if q occurs negatively in B or in an aggregate atom, then q < p . The level P of P is the maximum of the levels of the de?ned predicates. For each level i, let Pi be the set of all rules with a predicate of level i in the head and Πi the set of de?ned predicates of level i. De?ne for each i ≥ 0, Σi = Σ ∪ 1≤j ≤i Πj .

Well-founded and Stable Semantics of Logic Programs with Aggregates

23

Assume i ≥ 1 and ?x an arbitrary Σi?1 -structure D′ extending D. Notice that all predicates of Πi occur only positively in bodies of Pi . Consequently, Pi is a aggr de?nite aggregate program and has a monotone TP ′ operator. Note that it does i ,D not matter whether the aggregates in Pi are monotone or non-monotone, since they do not contain predicates of Πi . De?nition 5.9 The standard model of an aggregate program P extending D is the interpretation I = 1≤i≤ P Ii where the set {Ii | 1 ≤ i ≤ P } is de?ned by the following (?nite) induction: D0 = D;

aggr Ii = lfp(TP ); i ,Di?1

Di = D(

1≤j ≤i

Ij ).

The aggregate program in the following example is a strati?ed aggregate program. Example 5.4 (Shortest Path ) Consider the signature of directed weighted graphs Σ = {n, w}; ?; {edge : n × n × w}; {min : {w} × w} . A Σ-structure D interprets the sort n with a set of nodes, and the sort w, representing weights, with some set of real numbers wD ? R. The graph is de?ned by the relation edgeD where (a, b, w) ∈ edgeD represents an edge from a to b with weight w. Consider the following formulation of the problem of ?nding the weight of the shortest path between two nodes which can be found in (Van Gelder 1992, Example 4.1). sp(x, y, w) ← min({c | cp(x, y, c)}, w). cp(x, y, c) ← edge(x, y, c). cp(x, y, c1 + c2 ) ← cp(x, z, c1 ) ∧ edge(z, y, c2). The aggregate relation min is neither monotone nor anti-monotone, so the aggregate atom min(. . .) in the ?rst rule is neutral. Consequently, the program is not de?nite. However, the program is strati?ed. The ?rst stratum which de?nes the cp/3 predicate is a de?nite logic program. The predicate cp/3 represents the transitive closure of the graph: cp(a, b, w) is true in the least model of Pcp if and only if there is a path between a and b with weight w. The second stratum contains only the de?nition of sp/3 and sp(a, b, w) is true in the standard model of the program if and only if a shortest path between a and b exists and has weight w. 6 Ultimate Semantics for Aggregate Programs We start our study of the semantics of general aggregate programs with a brief investigation of the semantics generated by the ultimate approximating opera-

24

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

aggr aggr tor UP, D of TP,D . This semantics of aggregate programs was ?rst studied by Denecker et al. (2001).

De?nition 6.1 aggr aggr c c The ultimate approximating operator UP, D : I → I of TP,D : I → I is de?ned as:

aggr UP, D (I1 , I2 ) = ( aggr TP, D (I ), aggr TP, D (I ) ). I ∈[I1 ,I2 ] I ∈[I1 ,I2 ]

De?nition 6.2 The ultimate Kripke-Kleene model, the ultimate well-founded model, and the set of ultimate stable models of an aggregate program P are de?ned as the Kripke-Kleene, aggr the well-founded, and the set of exact stable ?xpoints of the UP, D operator. Example 6.1 Consider the following program with Herbrand universe {0, 1}: p(0) ← card({x|p(x)}, 1). Observe that this program has two supported models: ? and {p(0)}. Also, this is not a de?nite aggregate program and its immediate consequence operator is nonmonotone as can be seen from:

aggr TP, D ({p(0)}) = {p(0)}, aggr TP, D ({p(0), p(1)}) = ?.

Let us construct the well-founded ?xpoint. We start from the pair (⊥, ?). The new upper and lower bounds are obtained by applying the stable revision operator of De?nition 2.3 on (⊥, ?) = (?, {p(0), p(1)}). The new upper bound is the least aggr 2 ?xpoint of (UP, D ) (?, ·). It is easy to see that :

aggr 2 aggr (UP, D ) (?, ?) = TP,D (?) = ?.

It follows that ? is a ?xpoint of this operator; it is obviously the least ?xpoint. aggr 1 Likewise, the new lower bound is the least ?xpoint of (UP, D ) (·, {p(0), p(1)}). This is ? as well, since:

aggr 1 (UP, D ) (?, {p(0), p(1)}) = ?;

Consequently, the well-founded ?xpoint is (?, ?). This represents the two-valued interpretation ? and this is also the unique ultimate stable model of this program. The ultimate Kripke-Kleene model can be computed in two computation steps:

aggr 1 aggr 2 (UP, D ) (?, {p(0), p(1)}) = ?; (UP,D ) (?, {p(0), p(1)}) = {p(0)} aggr 1 aggr 2 (UP,D ) (?, {p(0)}) = ?; (UP, D ) (?, {p(0)}) = {p(0)}.

The model is the three-valued interpretation {p(0)u } = (?, {p(0)}). We obtain the following corollary to Theorem 2.3 and Theorem 5.1.

Well-founded and Stable Semantics of Logic Programs with Aggregates

25

Corollary 6.1 aggr If TP, D is monotone, then the ultimate well-founded ?xpoint of P is the least aggr ?xpoint of TP, D and the unique ultimate stable ?xpoint of P . If P is a de?nite aggregate program, then its ultimate well-founded model and unique ultimate stable model is the least ?xpoint model of P . It follows that both the ultimate well-founded and the ultimate stable semantics correctly model the company control program in Example 5.2 and the Borel sets program in Example 5.3. Later, we will also show a similar result to Corollary 6.1 for strati?ed programs: if P is a strati?ed program then its ultimate well-founded and unique ultimate stable model coincide with the standard model of P . Hence, the ultimate semantics also models correctly the shortest path program in Example 5.4. Two aggregate programs with the same immediate consequence operator are equivalent under ultimate semantics. Since substituting formulas in rule bodies by equivalent formulas preserves the operator, this operation is equivalence preserving. Proposition 6.1 Let P and P ′ be aggregate programs such that P ′ is obtained by substituting a formula ?′ for a formula ? in the body of a rule of P . If ?(? ≡ ?′ ) is satis?ed in all aggr aggr ′ two-valued Σ(Π)-extensions D(I ) of D, then TP, D = TP ′ ,D and P and P have the same ultimate Kripke-Kleene model, the same ultimate well-founded model, and the same set of ultimate stable models. Another result about the set of ultimate stable models is that they are always minimal models. In fact, we can prove such result for the set of stable models aggr associated with any approximating operator of TP, D . Proposition 6.2 aggr Let P be an aggregate program and A be an approximating operator of TP, D . Each stable model of A is a minimal model of P . Proof aggr By Lemma 2.1, every stable model of A is a minimal pre-?xpoint of TP, D and by aggr Proposition 5.1, the pre-?xpoints of TP,D are exactly the models of P . The nice semantical properties of ultimate semantics come at a computational price. Even for programs without aggregates, computing the ultimate well-founded model is co-NP-hard and deciding the existence of a two-valued ultimate stable model is Σp 2 -complete (Denecker et al. 2004). For this reason, we will study weaker aggr semantics based on less precise approximations of TP, D . 7 Extending the Standard Well-founded and Stable Semantics The goal of this section is to extend the Kripke-Kleene (Fitting 1985), well-founded (Van Gelder et al. 1991) and stable (Gelfond and Lifschitz 1988) semantics of normal logic programming. According to Approximation Theory (Denecker et al. 2000) these three semantics can be obtained from the three-valued immediate consequence

26

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

operator ΦP de?ned by Fitting (1985). In particular, the collection of three-valued interpretations corresponds to the set Lc of consistent pairs of the lattice L of two-valued interpretations. The operator ΦP is an approximation on this set, it approximates the TP operator and its stable and well-founded ?xpoints correspond to the stable and well-founded models of P . By extending ΦP to the class of aggregate programs, we will be able to obtain well-founded and stable semantics which extend those of logic programs without aggregates. To extend the Fitting operator for aggregate programs, we must be able to evaluate the aggregate formulas in three-valued interpretations. For this reason we introduce the concept of a three-valued structure. It is similar to standard structures, except that predicates are assigned three-valued relations and aggregate symbols are assigned three-valued aggregate relations. Because the value of a set expression in a three-valued structure can be a three-valued set, three-valued aggregates take three-valued sets as argument. We ?rst illustrate these points with an example. Example 7.1 We denote a three-valued set by indexing its certain elements with ? t and its possible ? ? t u ? = {1? ? . Let us ?x the three-valued set S elements with u , 2 ? , 3t , 5u }. A three-valued aggregate C ard of the cardinality aggregate card is a mapping from pairs of three-valued sets and natural numbers to T HREE . In case of the set ?, correct values for the set S ? are the following: S ? n) = u ? , for all n ∈ {2, 3, 4} C ard(S, ? ? C ard(S, n) = f , for all natural numbers n ∈ {2, 3, 4} ? has between two and four elements. This speci?es that the set approximated by S Similarly, correct values in case of card≥ are as follows: ? ? n) = ? t, for all n ∈ {0, 1, 2} ? C ard≥ (S, ? ? , for all n ∈ {3, 4} C ard≥ (S, n) = u ? ? n) = ? C ard(S, f , for all natural numbers n ∈ {0, . . . , 4}

? certainly has more than zero, one This speci?es that each set approximated by S and two elements, and has possibly more than three or four elements, but de?nitely ? has not more than ?ve elements or more. A weaker but still correct value for S would be: ? ? 0) = ? t, ? C ard≥ (S, ? ? , for all n ∈ {1, 2, 3, 4, 5, 6} C ard≥ (S, n) = u ? ? n) = ? C ard(S, f , for all natural numbers n > 6 ? has certainly more than 0 elements, which speci?es that the set approximated by S possibly more than one to six elements and certainly not more than 7 elements or more.

We now formalize the notions of three-valued aggregate relations and structures. De?nition 7.1 (Three-valued Aggregate Relations ) A three-valued aggregate relation is a function R : ?(D1 )c × D2 → T HREE which satis?es:

Well-founded and Stable Semantics of Logic Programs with Aggregates

27

?1 , S ?2 ∈ ?(D1 )c and for ? ≤p -monotonicity: for every pair of three-valued sets S ? ? ? ? every d ∈ D2 , if S1 ≤p S2 then R(S1 , d) ≤p R(S2 , d); ? exactness: for every exact (two-valued) set S ∈ ?(D1 ) and for every d ∈ D2 , R((S, S ), d) ∈ T WO. The concept of a three-valued aggregate relation is very similar to approximating operators (De?nition 2.1). Remark 2 The de?nition has a straightforward extension to aggregates with multiple set arguments by requiring ≤p -monotonicity and exactness conditions for all set arguments. A three-valued aggregate relation R approximates an aggregate relation r if for each set S ∈ ?(D1 ) and for each d ∈ D2 , R((S, S ), d) = r(S, d). Due to the exactness condition, a three-valued aggregate relation approximates exactly one aggregate relation. Recall that T HREE = T WOc . It follows that a three-valued aggregate relation R : ?(D1 )c × D2 → T HREE is completely determined by the pair (R1 , R2 ) of its projections on the ?rst and second component. These projections are relations R1 , R2 ? ?(D1 )c × D2 such that R1 ? R2 and R1 , R2 coincide on two-valued sets2 . We will frequently de?ne a three-valued aggregate relation R by de?ning R1 and R2 separately. De?nition 7.2 (Three-valued Structure ) ? consists of the folLet Σ be an aggregate signature. A three-valued Σ-structure D lowing: ? for each sort s ∈ S a domain sD ; ? for each function symbol f : s1 × · · · × sn → w ∈ F unc(Σ) a function

D D f D : sD 1 × · · · × sn → w ; ? ? ? ? ?

? for each predicate symbol p : s1 × · · · × sn ∈ P red(Σ) a three-valued relation

D p D : sD 1 × · · · × sn → T HREE . ? ? ?

? for each aggregate symbol r : {s1 × · · · × sn } × w ∈ Aggr(Σ) a three-valued aggregate relation

c D c D rD : ?((sD 1 ) × · · · × (sn ) ) × w → T HREE . ? ? ? ?

? approximates a Σ-structure D if for each predicate A three-valued Σ-structure D ? ? D D symbol p, p approximates p and for each aggregate symbol r, rD approximates rD . Now we de?ne a precision order between three-valued aggregate relations and structures.

2

Equivalently, R1 , R2 are functions ?(D1 )c × D2 → T WO which coincide on two-valued sets and such that R1 ≤ R2 .

28

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

De?nition 7.3 For all three-valued aggregate relations R1 , R2 : ?(D1 )c × D2 → T HREE , de?ne ? d) ≤p R2 (S, ? d) for every three-valued set S ? ∈ ?(D1 )c and R1 ≤p R2 if R1 (S, domain element d ∈ D2 . ?2 if D ?1 and D ?2 ? 1 and D ?2 , de?ne D ? 1 ≤p D For all three-valued Σ-structures D have the same domain, the same interpretations of sort and function symbols, for ? ? each predicate symbol p ∈ P red(Σ), pD1 ≤p pD2 and for each aggregate symbol ?2 ?1 D D r ∈ Aggr(Σ), r ≤p r . It is straightforward to see that if R1 ≤p R2 and R2 approximates an aggregate relation r then R1 also approximates r. De?nition 7.4 (Three-valued valuation and truth functions ) ? be a three-valued Σ-structure. We de?ne the Let Σ be an aggregate signature and D three-valued valuation function · D ? for set expressions and the three-valued truth function HD ? for aggregate formulas by simultaneous induction. Let {(x1 , . . . , xn ) | ?(x1 , . . . , xn )} be a set expression of type {s1 × · · · × sn }. The ? value {(x1 , . . . , xn ) | ?} D ? is the three-valued set S de?ned as: ?(d1 , . . . , dn ) = H ? (?(d1 , . . . , dn )) S D

D for every (d1 , . . . , dn ) ∈ sD 1 × · · · × sn . aggr The three-valued truth function for ?rst-order aggregate formulas HD ? (·) : LΣ(D ?) → T HREE is de?ned as in De?nition 4.6 using the three-valued operations ∧, ∨, and ? as de?ned in Example 2.1. ? ?

Next, we show that the three-valued truth function HD ? is monotone with respect to the precision order ≤p on three-valued interpretations. Proposition 7.1 ?2 then for every Σ-aggregate ?1 and D ? 2 be three-valued Σ-structures. If D ? 1 ≤p D Let D ( ? ). ( ? ) ≤ H formula ?, HD ?2 ?1 p D Proof The proof is by a standard induction argument on the size of ?. For aggregate atoms it follows from the ≤p -monotonicity of the three-valued aggregate relations. Another proposition shows the correspondence between three-valued and twovalued truth functions. If all predicate symbols have two-valued interpretations then evaluating an aggregate formula in a three-valued structure results in a twovalued truth value. Proposition 7.2 ? be a three-valued structure which approximates Let D be a Σ-structure and D ? D. For every aggregate formula ? such that pD is two-valued for all predicates p appearing in ?, HD ? (?) = (HD (?), HD (?)).

Well-founded and Stable Semantics of Logic Programs with Aggregates

29

Proof The proof is by a standard induction argument on the size of ?. For aggregate atoms it follows from the exactness condition of the three-valued aggregate relations. In the sequel we will consider only three-valued structures for which only the interpretation of the de?ned predicates Π and the aggregates is three-valued while the interpretation of the pre-de?ned predicates is two-valued. Such structures are ? (I ?) where I ?: base ? (Π) → T HREE gives the (three-valued) interpredenoted by D D tation of the predicates in Π. We now extend De?nition 5.2 of the immediate consequence operator for aggregate programs to the three-valued case. De?nition 7.5 c c The three-valued immediate consequence operator Φaggr ? : I → I for an aggregate P,D ? to a three-valued interpretation program P maps any three-valued interpretation I aggr ? ′ ? I =Φ (I ) such that for each ground de?ned atom A ∈ base ? (Π):

? P,D D

?′ (A) = I

{HD ? (I ?) (?) | A ← ? ∈ instD ? (P )}.

?′ is the greatest of all truth values of Or, the truth value of a de?ned atom A in I bodies of rule instances with A in the head. Proposition 7.3 ? is a three-valued structure approximating D then Φaggr is an approximating If D ? P,D aggr operator of TP, . D Proof Follows from Proposition 7.1 and Proposition 7.2. De?nition 7.6 ? , the D ? -Kripke-Kleene model, the D ? -well-founded Given a three-valued structure D ? model and the set of D-stable models of an aggregate program P are de?ned as the Kripke-Kleene, well-founded and the set of exact stable ?xpoints of the Φaggr ? P,D operator. Example 7.2 Reconsider the program of Example 6.1 with Herbrand universe {0, 1}: p(0) ← card({x|p(x)}, 1). We will show that, for an appropriate value of the three-valued aggregate, its standard well-founded model is identical to its ultimate well-founded model. To compute stable and well-founded models, we need to choose a three-valued aggregate C ard approximating card. Let us assume that

? u ? = (f , t) C ard({0u , 1 ? }, 1) = C ard((?, {0, 1}), 1) = u ? ? = (f , t). C ard({0u }, 1) = C ard((?, {0}), 1) = u

30

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

Then the following assignments can be computed easily:

aggr 1 ? ? 1 u u (Φaggr ? ) ({p(0) , p(1) }) = (ΦP,D ? ) ((?, {p(0), p(1)})) = ?; P,D ? ? 2 u u (Φaggr ? ) ({p(0) , p(1) }) P,D aggr 1 ? u (ΦP,D ? ) ({p(0) }) aggr 2 ? u (ΦP,D ? ) ({p(0) }) 2 f f (Φaggr ? ) ({p(0) , p(1) }) P,D ? ? 2 = (Φaggr ? ) ((?, ?)) P,D

= ?; = {p(0)}; = ?; = {p(0)}.

= = =

2 (Φaggr ? ) ((?, {p(0), p(1)})) P,D aggr 1 (ΦP,D ? ) ((?, {p(0)})) 2 (Φaggr ? ) ((?, {p(0)})) P,D

aggr These assignments are the same as for the ultimate approximation UP, D . It follows ? -well-founded model and the unique D ? -stable model that the empty set ? is the D ? ? -Kripke-Kleene model. of this program and {p(0)u } is the D

For logic programs without aggregates each Φaggr ? operator coincides with the P,D operator ΦP de?ned by Fitting (1985). So, the well-founded and stable semantics of aggregate programs is an extension of the well-founded and stable semantics of normal logic programs. ? and, in parNotice that the semantics of an aggregate program P depends on D ticular, on the choice of the three-valued aggregates. This means that we still have a family of di?erent semantics. This family can be ordered by precision. Not surprisingly, using more precise three-valued aggregates leads to more precise semantics. The following proposition is a straightforward consequence of Proposition 7.1. Proposition 7.4 ?1 and D ?2 and for every three-valued For every pair of three-valued Σ-structures D aggr ?2 then Φ ? ? ?, if D ? 1 ≤p D interpretation I ? 2 (I ). ? (I ) ≤p ΦP,D P,D

1

So, by Theorem 2.1 we obtain the following result. Theorem 7.1 ? 1 and D ?2 be two three-valued Σ-structures Let P be an aggregate program and D ? 2 . Then: ? 1 ≤p D such that D ? 1 -Kripke-Kleene model of P is less precise (in the ≤p order) than the ? the D ? D2 -Kripke-Kleene model of P ; ?1 -well-founded model of P is less precise (in the ≤p order) than the ? the D ? 2 -well-founded model of P ; D ?1 -stable model is a D ?2 -stable model. ? every D The semantics that we have de?ned in this section do not satisfy all the strong declarative properties of the ultimate semantics de?ned in the previous section. For ? -well-founded model of an aggregate program with monotone imexample, the D mediate consequence operator is not necessarily its least ?xpoint. E.g. the program {p ← p ∨ ?p.} has a constant, hence monotone TP with least ?xpoint {p}, but in its well-founded model p is unknown. Also, substituting a formula for an equivalent formula in a rule body is not in general equivalence preserving. E.g. substituting true for p ∨ ?p in the above program does not preserve equivalence. However, some interesting properties still hold.

Well-founded and Stable Semantics of Logic Programs with Aggregates

31

Proposition 7.5 Let P and P ′ be aggregate programs such that P ′ is obtained by substituting an aggregate formula ?′ for an aggregate formula ? in the body of a rule of P . If ? , then P and P ′ are ?(? ≡ ?′ ) is satis?ed in all three-valued Σ(Π)-extensions of D ? -Kripke-Kleene, D ? -well-founded and D ? -stable semantics. equivalent under the D Proof Follows from the fact that P and P ′ have the same three-valued immediate consequence operators. The three-valued equivalence condition in this proposition is strictly stronger than the two-valued equivalence condition in Proposition 6.1. For example true and p ∨ ?p are equivalent in two-valued semantics but not in three-valued. Another important property is that in case of a strati?ed aggregate program P , ? -well-founded semantics and D ? -stable semantics coincide with the standard the D semantics as de?ned in Section 5.2, and it does not matter how the aggregate ?. relations are approximated by D Theorem 7.2 Let P be a strati?ed Σ(Π)-aggregate program. For any three-valued Σ-structure ? approximating D, the D ? -well-founded model is two-valued and is equal to the D ? -stable model of P . standard model of P extending D and to the unique D The proof of this result depends on the following lemma. Lemma 7.1 Let ? be a closed Σ(Π)-aggregate formula such that predicates of Π do not occur ? be a three-valued Σ-structure in an aggregate atom. Let D be a Σ-structure and D which is two-valued on all predicates in Σ and approximates D. Then for any three-valued interpretation (I1 , I2 ), if the predicates in Π occur only positively in ? then HD ? (I1 ,I2 ) (?) = (HD (I1 ) (?), HD (I2 ) (?)) and if the predicates in Π occur only negatively in ? then HD ? (I1 ,I2 ) (?) = (HD (I2 ) (?), HD (I1 ) (?)). Proof By simultaneous induction on the structure of ?. We give only the case when the predicates of Π occur only positively in ?. The proof of the other case is symmetric. ? For a pre-de?ned atom p(t1 , . . . , tn ): HD ? (I1 ,I2 ) (p(t1 , . . . , tn )) = HD ? (p(t1 , . . . , tn )) = (HD (p(t1 , . . . , tn )), HD (p(t1 , . . . , tn ))). ? For a user de?ned atom p(t1 , . . . , tn ): HD ? (I1 ,I2 ) (p(t1 , . . . , tn )) = (I1 , I2 )(p( t1 = (I1 (p( t1

D, . . . ,

tn

D ))

D, . . . ,

tn

D )), I2 (p(

t1

D, . . . ,

tn

D )))

= (HD(I1 ) (p(t1 , . . . , tn )), HD(I2 ) (p(t1 , . . . , tn ))).

32

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

? For a formula with negation ??: HD ? (I1 ,I2 ) (??) = ?HD ? (I1 ,I2 ) (?) = ?(HD(I2 ) (?), HD(I1 ) (?)) = (?HD(I1 ) (?), ?HD(I2 ) (?)) = (HD(I1 ) (??), HD(I2 ) (??)) ? For a conjunction ? ∧ ψ : HD ? (I1 ,I2 ) (? ∧ ψ ) = HD ? (I1 ,I2 ) (?) ∧ HD ? (I1 ,I2 ) (ψ ) = (HD(I1 ) (?), HD(I2 ) (?)) ∧ (HD(I1 ) (ψ ), HD(I2 ) (ψ )) = (HD(I1 ) (?) ∧ HD(I1 ) (ψ ), HD(I2 ) (?) ∧ HD(I2 ) (ψ )) = (HD(I1 ) (? ∧ ψ ), HD(I2 ) (? ∧ ψ )). ? The proofs for formulas of the form ? ∨ ψ , ?x?, and ?x? are analogous. ? Let r({x | ?}, t) be an aggregate atom. Since ? contains only pre-de?ned predicate symbols from Σ then HD ? (r({x | ?}, t)). ? (I1 ,I2 ) (r({x | ?}, t)) = HD ? of all predicate symbols is two-valued we Moreover, since the interpretation by D have (by Proposition 7.2): HD ? (r({x | ?}, t)) = (HD (r({x | ?}, t)), HD (r({x | ?}, t))). by De?nition 7.4 by the induction hypothesis by de?nition of ? by De?nition 4.6.

Proof of Theorem 7.2 (Sketch) Let P be strati?ed by the level mapping . , and let Πi be the predicates of level i, Pi the set of rules of P with head in Πi . Given an interpretation I ∈ I , let us de?ne I |i as the restriction of I to the predicates of Πi , and I |≤i and I |<i as the restriction of I to the predicates of j<i Πj . We extend these notations also to threej ≤i Πj , respectively those of valued interpretations. It is easy to see that for every i = 1, . . . , P and every ?J ? ∈ I c , if I ?|≤i = J ?|≤i , then I,

aggr ? ? Φaggr ? (I )|≤i = ΦP,D ? (J )|≤i . P,D

? ∈ Ic: Moreover, for every I

aggr ? Φaggr ? (I ?| ? (I )|i = ΦP ,D P,D

i <i )

?|i ). (I

? is the well-founded It follows from Corollary 3.12 in (Vennekens et al. 2006) that I aggr ? ?xpoint of ΦP,D ? if and only if for every i = 1, . . . , P , I |i is the well-founded aggr ?xpoint of ΦP ,D ? (I ?|<i ) . i The next step is to prove by induction that for every i = 1, . . . , P , the well?|i of Φaggr founded ?xpoint I ? (I ?|<i ) is equal to (I |i , I |i ) where I is the standard model Pi ,D ? -well-founded model I ? of P is equal to the standard of P . This will show that the D

Well-founded and Stable Semantics of Logic Programs with Aggregates

33

?|<i = (I |<i , I |<i ). Let Σi?1 = Σ ∪ model I of P . Fix i and assume that I j<i Πj , ′ ′ ′ ′ ′ ? ? ? ? ? D = D(I |<i ) and D = D (I |<i ). Notice that D approximates D and D is two?|<i is a two-valued interpretation). Using valued on all predicates of Σi?1 (because I Lemma 7.1 we can show that for any three-valued Πi -interpretation (I1 , I2 ),

aggr aggr 1 2 Φaggr ? ′ (I1 , I2 ) = (TPi ,D ′ (I ), TPi ,D ′ (I )). P ,D

i

aggr By Theorem 2.3 it follows that Φaggr ? ′ is also the ultimate approximation of TPi ,D ′ . Pi ,D ? ′ -well-founded model of Pi is equal to the ultimate well-founded model of So, the D aggr Pi extending D′ and, by Corollary 6.1, to the least ?xpoint of TP ′. i ,D aggr Since the Φaggr ? operators are less precise than the ultimate approximation UP,D P,D we have the following corollary of Theorems 2.1 and 7.2.

Corollary 7.1 For a strati?ed program P , the ultimate well-founded model is two-valued and is equal to the unique ultimate stable model and to the standard model of P . In the next sections we de?ne several di?erent three-valued aggregate relations and study the semantics obtained from the corresponding Φaggr ? operator. P,D 7.1 Trivial Approximating Aggregates As a ?rst example of a three-valued aggregate relation, we consider the least precise approximation of an aggregate. In the sequel, it will be convenient to view an aggregate relation both as a subset of ?(D1 ) × D2 and as a function from ?(D1 ) × D2 to T WO . De?nition 7.7 (Trivial Approximating Aggregate ) Let r ? ?(D1 ) × D2 be an aggregate relation. The trivial approximating aggregate triv (r) : ?(D1 )c × D2 → T HREE of r is de?ned as follows: triv (r)((S1 , S2 ), d) = (f , t) (r(S1 , d), r(S1 , d)) if S1 = S2 if S1 = S2

Proposition 7.6 For every aggregate relation r, triv (r) is a three-valued aggregate relation and triv (r) approximates r. For a (two-valued) structure D we de?ne triv (D) as the three-valued structure in which every aggregate relation r is interpreted with triv (r). When D is clear from the context we simply use triv . As mentioned earlier, the trivial approximating aggregate is the least precise three-valued aggregate relation. Proposition 7.7 Let r be an aggregate relation. For every three-valued aggregate relation R of r, triv (r) ≤p R. The trivial approximating aggregates are very imprecise. Nevertheless, by Theorem 7.2, they su?ce to model the semantics of the important class of strati?ed aggregate programs.

34

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

Corollary 7.2 Let P be a strati?ed aggregate program. The triv -well-founded model of P is twovalued and is equal to the standard model of P and the unique triv -stable model of P . This corollary shows that even the weakest instance of the well-founded and stable semantics su?ces to de?ne the standard model approach for strati?ed aggregate programs. 7.2 Ultimate Approximating Aggregate In this section we investigate the instance of the Φaggr operator in which aggreP gate symbols are interpreted with the most precise three-valued aggregate relation, called the ultimate approximating aggregate. This three-valued aggregate relation is de?ned for all aggregate relations in a uniform way using a construction similar to that of ultimate approximations. De?nition 7.8 (Ultimate Approximating Aggregate ) Let r ? ?(D1 ) × D2 be an aggregate relation. The ultimate approximating aggregate of r is a three-valued aggregate relation ult(r) : ?(D1 )c × D2 → T HREE de?ned as: ult(r)1 ((S1 , S2 ), d) = t if and only if ?S ∈ [S1 , S2 ] : (S, d) ∈ r ult(r)2 ((S1 , S2 ), d) = t if and only if ?S ∈ [S1 , S2 ] : (S, d) ∈ r Proposition 7.8 For every aggregate relation r, ult(r) is a three-valued aggregate relation and ult(r) approximates r. For a structure D we de?ne ult(D) as the three-valued structure in which every aggregate relation r is interpreted with ult(r). When D is clear from the context we simply use ult. The ultimate approximating aggregate ult(r) is the most precise in the ≤p -order among all possible three-valued aggregate relations. Proposition 7.9 Let r be an aggregate relation. For every three-valued aggregate relation R which approximates r, R ≤p ult(r).

aggr So, Φaggr ? operators and by P,ult is the most precise operator in the family of ΦP,D Proposition 7.1, the ult-well-founded and the ult-stable semantics are the most precise semantics of aggregate programs in this family. Of course, these semantics are still weaker than the ultimate well-founded and ultimate stable semantics from Section 6. Recall that for the program {p ← p ∨ ?p.}, p is true in the ultimate wellfounded model but unknown in the ult-well-founded model. An aggregate program showing similar behavior is given in the following example.

Well-founded and Stable Semantics of Logic Programs with Aggregates Example 7.3 Consider the following program with Herbrand universe {0, 1, 2, 3}: p(x) ← card≤ ({x|p(x)}, 1) ∨ card≥ ({x|p(x)}, 2).

35

Note that the body is a tautology in 2-valued logic. Therefore, in the ultimate semantics, this program is equivalent with: p(x) ← t In the ultimate Kripke-Kleene, well-founded and unique stable model, p is true for all domain elements. On the other hand, in the ult-well-founded model, each ? and the program has no ult-stable model. This can be seen atom p(i) has value u ?, for every as follows. First, we observe that for each three-valued interpretation I aggr 2 ? aggr ? two-valued I approximated by I , (ΦP,ult ) (I ) is an upper bound of TP, D (I ) = aggr 2 {p(0), . . . , p(3)} = ?. Hence, (ΦP,ult ) is a constant operator and maps each three? to {p(0), . . . , p(3)}. On the other hand, it is easy to see that valued interpretation I ? ? ? = {0u ? 1) and ult(card≥ )1 (S, ? 2) for the three-valued set S , . . . , 3u }, ult(card≤ )1 (S, ? approximates sets with strictly more than one element and are both false, since S other sets with strictly less than two elements. Therefore,

aggr 1 ? ? 1 u u (Φaggr P,ult ) ({p(0) , . . . , p(3) }) = (ΦP,ult ) (?, {p(0), . . . , p(3)}) = ?. 1 Hence, ? is the least ?xpoint of (Φaggr P,ult ) (·, {p(0), . . . , p(3)}) and {p(0), . . . , p(3)} is aggr 2 the least ?xpoint of (ΦP,ult ) (?, ·). It follows that the ult-well-founded ?xpoint is ? ? {p(0)u , . . . , p(3)u } = (?, {p(0), . . . , p(3)}).

As for the stable semantics, any ult-stable ?xpoint is also a supported ?xpoint, and the only supported ?xpoint is {p(0), . . . , p(3)}. However, the least ?xpoint of 1 (Φaggr P,ult ) (·, {p(0), . . . , p(3)}) is not {p(0), . . . , p(3)} but ?. Hence, there are no ultstable ?xpoints. Now we look at characterizations of the ultimate approximating aggregate of some common aggregate functions. Such characterizations are useful for several purposes. First of all, they can be used in an implementation of the semantics. Second, they can be used for complexity analysis of the semantics. For monotone and anti-monotone aggregates the truth value can be computed directly on the boundary multisets. Proposition 7.10 Let r : ?(D1 ) × D2 be a monotone aggregate relation. Then ((S1 , S2 ), d) ∈ ult(r)1 if and only if (S1 , d) ∈ r and ((S1 , S2 ), d) ∈ ult(r)2 if and only if (S2 , d) ∈ r. Proposition 7.11 Let r : ?(D1 ) × D2 be an anti-monotone aggregate relation. Then ((S1 , S2 ), d) ∈ ult(r)1 if and only if (S2 , d) ∈ r and ((S1 , S2 ), d) ∈ ult(r)2 if and only if (S1 , d) ∈ r. Next, we look at extrema aggregates, possibly de?ned on in?nite sets.

36

r

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

((S1 , S2 ), d) ∈ ult(r)1 i? d ∈ S1 ∧ min(S2 , d) d ∈ S1 ∧ max(S2 , d) glb(S1 , d) ∧ glb(S2 , d) lub(S1 , d) ∧ lub(S2 , d) ((S1 , S2 ), d) ∈ ult(r)2 i? d ∈ S2 ∧ ??d′ ∈ S1 : d′ < d d ∈ S2 ∧ ??d′ ∈ S1 : d′ > d glb(S1 ∪ (S2 ∩ [d, ?]), d) lub(S1 ∪ (S2 ∩ [⊥, d]), d)

min max glb lub

Table 2. Characterization of ultimate approximating aggregates of extrema aggregates. Proposition 7.12 The characterizations in Table 2 are correct. Next, look at the aggregate functions card, sum and prod de?ned on ?nite sets. Proposition 7.13 (ult(card)) For every three-valued set (S1 , S2 ) and element d: ((S1 , S2 ), d) ∈ ult(card)1 if and only if |S1 | = d = |S2 | ((S1 , S2 ), d) ∈ ult(card)2 if and only if |S1 | ≤ d ≤ |S2 | Proposition 7.14 (ult(sum) and ult(prod)) For every three-valued set (S1 , S2 ) and element d: ((S1 , S2 ), d) ∈ ult(sum)1 i? sum(S1 , d) ∧ ?(x1 , . . . , xn ) ∈ S2 \ S1 : x1 = 0 ((S1 , S2 ), d) ∈ ult(sum)2 i? ?S ′ ? S2 \ S1 : sum(S1 ∪ S ′ , d) ((S1 , S2 ), d) ∈ ult(prod)1 i? prod(S1 , d)∧ (d = 0 ∨ ?(x1 , . . . , xn ) ∈ S2 \ S1 : x1 = 1) ((S1 , S2 ), d) ∈ ult(prod) i? ?S ′ ? S2 \ S1 : prod(S1 ∪ S ′ , d). Proof The proof is straightforward and uses only basic properties of numbers. Note that the de?nition of ult(sum)2 and ult(prod)2 is simply a reformulation of the original de?nition of ult. In fact, Pelov (2004) shows that the complexity of computing ult(sum)2 and ult(prod)2 is NP-complete so it is unlikely that any e?cient algorithms can be found. Finally, we look at combined aggregate relations of the form f≥ and f≤ where f : ?F (D1 ) → D2 is an aggregate function on ?nite sets and ≤ is a total order on D2 . For all three aggregate functions card, sum, and prod we can give e?cient algorithms for ult(f≥ )1 and ult(f≥ )2 . We start with the following general result. Let minf , maxf : ?F (D1 )c → ?F (D1 ) be functions which for a given ?nite three-valued set (S1 , S2 ) return a set S ∈ [S1 , S2 ] such that f(S ) is minimal (resp. maximal) over the set [S1 , S2 ], i.e., ?S ′ ∈ [S1 , S2 ] : f(minf (S1 , S2 )) ≤ f(S ′ ) ?S ′ ∈ [S1 , S2 ] : f(maxf (S1 , S2 )) ≥ f(S ′ ).

2

Well-founded and Stable Semantics of Logic Programs with Aggregates

37

Note that for a given aggregate function f and a three-valued set (S1 , S2 ) there may be more than one set in the interval [S1 , S2 ] with a minimal value of f. For example minsum (?, {0}) can return either ? or {0}. The values of ult(f≤ ) and ult(f≥ ) can be computed using the minf and maxf functions in the following way. Proposition 7.15 Let f : ?F (D1 ) → D2 be an aggregate function and ≤ be a total order on D2 . Then: ((S1 , S2 ), d) ∈ ult(f≥ )1 if and only if f(minf (S1 , S2 )) ≥ d ((S1 , S2 ), d) ∈ ult(f≥ )2 if and only if f(maxf (S1 , S2 )) ≥ d and similarly for ult(f≤ ): ((S1 , S2 ), d) ∈ ult(f≤ )1 if and only if f(maxf (S1 , S2 )) ≤ d ((S1 , S2 ), d) ∈ ult(f≤ )2 if and only if f(minf (S1 , S2 )) ≤ d. Proof First note that, since {f(S ) | S ∈ [S1 , S2 ]} is a ?nite totally ordered set, it always has a minimal and a maximal element. We give the proof for ult(f≥ )1 : ((S1 , S2 ), d) ∈ ult(f≥ )1 ??S ∈ [S1 , S2 ] : (S, d) ∈ f≥ ??S ∈ [S1 , S2 ] : f(S ) ≥ d ??x ∈ {f(S ) | S ∈ [S1 , S2 ]} : x ≥ d ?f(minf (S1 , S2 )) ≥ d. The proofs of the other cases are analogous. So, to decide the ?rst and second components of ult(f≥ )((S1 , S2 ), d) we need to compute the values minf (S1 , S2 ) and maxf (S1 , S2 ). First, we show how to compute these two functions for any monotone or anti-monotone aggregate function. Proposition 7.16 If f is a monotone aggregate function with respect to ≤ then minf (S1 , S2 ) = S1 and maxf (S1 , S2 ) = S2 . If f is an anti-monotone aggregate function with respect to ≤ then minf (S1 , S2 ) = S2 and maxf (S1 , S2 ) = S1 . This proposition can be applied to all aggregate functions listed in Table 1. For aggregate functions which are non-monotone the idea is to partition the under and over-estimate of the input three-valued set to subsets on which the aggregate function is monotone or anti-monotone. Then we combine the sets on which the function is monotone to obtain minf and the sets on which it is anti-monotone to obtain maxf . We illustrate this idea for the sum and prod aggregate functions. Below, S + denotes the set {(x1 , . . . , xn ) ∈ S | x1 ≥ 0} and S ? denotes the set {(x1 , . . . , xn ) ∈ S | x1 < 0}.

38

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

Proposition 7.17 For every three-valued set (S1 , S2 ):

+ ? minsum (S1 , S2 ) = S1 ∪ S2 ? + maxsum (S1 , S2 ) = S1 ∪ S2 .

Proof Clearly the set S ′ ∈ [S1 , S2 ] with minimal sum is obtained by taking S1 and all tuples with negative numbers from S2 \ S1 , that is

+ ? ? ? + ? minsum (S1 , S2 ) = S1 ∪ (S2 \ S1 )? = S1 ∪ S1 ∪ (S2 \ S1 ) = S1 ∪ S2 .

The aggregate function prod is non-monotone for sets with arbitrary real numbers as ?rst argument but is monotone for sets with the ?rst argument in the interval [1, ∞) and anti-monotone for sets with the ?rst argument in the interval [0, 1]. So, for prod on non-negative real numbers we can give a similar algorithm as for sum in Proposition 7.17. Below, S [1,∞) denotes the set {(x1 , . . . , xn ) ∈ S | x1 ∈ [1, ∞)} and S [0,1) denotes the set {(x1 , . . . , xn ) ∈ S | x1 ∈ [0, 1)}. Proposition 7.18 + For the aggregate function prodR : ?F (R+ ) → R+ , minprodR+ (S1 , S2 ) = S1

[1,∞) [0,1)

∪ S2 ∪ S2

[0,1)

maxprodR+ (S1 , S2 ) = S1

[1,∞)

.

The algorithms for prod on the entire set of real numbers are more complicated and can be found in (Pelov 2004). As an application of the ult-well-founded semantics we consider a recursive formulation of the shortest path problem. Example 7.4 (Shortest Path ) Consider the following formulation of the problem of ?nding the shortest path (Van Gelder 1992, Example 4.1): sp(x, y, w) ← min({c | cp(x, y, c)}, w). cp(x, y, c) ← edge(x, y, c). cp(x, y, c1 + c2 ) ← sp(x, z, c1 ) ∧ edge(z, y, c2 ). The only di?erence between this program and the formulation of the shortest path in Example 5.4 is that we have replaced the cp predicate in the body of the second clause of cp with the sp predicate. We have incorporated the knowledge that any shortest path of length n + 1 must be an extension of a shortest path of length n. This fact is the basis of Dijkstra’s algorithm. However, the program is no longer strati?ed because the sp/3 predicate depends on itself through the min aggregate relation which is non-monotone. It turns out the above program is only correct under certain conditions on the graph.

Well-founded and Stable Semantics of Logic Programs with Aggregates

39

Proposition 7.19 Let edgeD be a graph with the property that for any pair of nodes a and b, if there is a path from a to b, there is a shortest path from a to b. In the ult-well-founded model of the shortest path program from Example 7.4 an atom sp(a, b, w) is: ? true if a shortest path between a and b exists and has weight w; ? false otherwise. The proof of the proposition and a deeper analysis of this program is given in Appendix A. There are several types of graphs for which we can show that when there is a path from one node to another, there is a shortest path between these nodes: acyclic ?nite graphs, ?nite graphs with non-negative weights and in?nite graphs with weights in N0 . It follows from Proposition 7.19 that for these types of graphs, the programs in Example 5.4 and Example 7.4 are equivalent. There are also types of graphs which do not satisfy the condition. Connected nodes without shortest path can occur if there is a cycle with a negative weight between the two nodes. It can also occur in in?nite graphs. An example of such a graph is {(0, n + 2, 1), (n + 2, 1, 1/n + 2) | n ∈ N}; although there are an in?nite number of paths from 0 to 1, there is no shortest path between 0 and 1 (see Ross and Sagiv (1997) for another example). In the appendix, we show that in such graphs, the well-founded model may be three-valued or may even contain erroneous true sp(a, b, w) atoms, i.e., there are paths between a and b with strictly less weight than w. We conclude the section on ultimate approximating aggregates by showing that for de?nite aggregate programs, the ult-well-founded and ult-stable semantics are aggr equal to the least ?xpoint of the TP, D which we de?ned in Section 5.1. The key to the proof of this result is the following lemma. Lemma 7.2 ? = ult(D) and let (I1 , I2 ) be a three-valued interpretation. If ? is a closed Let D positive aggregate formula then HD ? (I1 ,I2 ) (?) = (HD (I1 ) (?), HD (I2 ) (?)). If ? is a closed negative aggregate formula then HD ? (I1 ,I2 ) (?) = (HD (I2 ) (?), HD (I1 ) (?)). Proof The proof extends that of Lemma 7.1 with several new cases when ? is an aggregate atom r({x | ψ }, t), ψ contains de?ned predicates and rD is either a monotone or an anti-monotone aggregate relation. We consider only the case when rD is a monotone aggregate relation and ψ is a positive aggregate formula. The other three cases (rD monotone and ψ negative and rD anti-monotone and ψ positive or negative) are symmetric. First, note that since ψ (x) is a positive formula then for every tuple of domain elements d, ψ (d) is also positive. So, H(I1 ,I2 ) (ψ (d)) = (HI1 (ψ (d)), HI2 (ψ (d))) and consequently {x | ψ }

? (I1 ,I2 ) D

= ( {x | ψ }

D (I1 ) ,

{x | ψ }

D (I2 ) ).

40 We have:

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

HD ? (I1 ,I2 ) (r({x | ψ }, t)) = ult(r)( {x | ψ } = ult(r)(( {x | ψ }

(by Proposition 7.10) = (r( {x | ψ }

? (I1 ,I2 ) , D D (I1 ) ,

t )

D (I2 ) ),

{x | ψ }

t ) t ))

D (I1 ) ,

t ), r( {x | ψ }

D (I2 ) ,

= (HD(I1 ) (r({x | ψ }, t)), HD(I2 ) (r({x | ψ }, t))).

Theorem 7.3 Let P be a de?nite aggregate program. Then P has a two-valued ult-well-founded aggr model (M, M ) which is also the single ult-stable model. Moreover M = lfp(TP, D ). Proof From Lemma 7.2 follows that if P is a positive aggregate program then

aggr aggr Φaggr P,ult (I1 , I2 ) = (TP,D (I1 ), TP,D (I2 )). aggr By Theorem 2.3 follows that Φaggr P,ult is also the ultimate approximation of TP,D . So, the ult-well-founded model of P is equal to the ultimate well-founded model of P aggr extending D and, by Corollary 6.1, to the least ?xpoint of TP, D .

7.3 Bound Approximating Aggregate The ultimate approximating aggregates have the disadvantage that they may have a higher complexity than the aggregate relations which they approximate. We already mentioned that the complexity of ult(sum)2 and ult(prod)2 is NP-complete (Pelov 2004) while the complexity of sum and prod is polynomial. In this section we de?ne a less precise approximating operator for aggregate functions that are de?ned on totally ordered ?nite sets of numbers. De?nition 7.9 Let f : ?F (D1 ) → D2 be an aggregate function and D2 , ≤ be a totally ordered set. The bound approximating aggregate bnd(f) : ?F (D1 )c × D2 → T HREE is de?ned as follows ((S1 , S2 ), d) ∈ bnd(f)1 if and only if f(minf (S1 , S2 )) = d = f(maxf (S1 , S2 )) ((S1 , S2 ), d) ∈ bnd(f)2 if and only if f(minf (S1 , S2 )) ≤ d ≤ f(maxf (S1 , S2 )). Note that by using Proposition 7.15, the de?nition of bnd(f) is equivalent to ult(f≥ ) ∧ ult(f≤ ) where ∧ is the greatest lower bound in T HREE with respect to the ≤ order (see Example 2.1). Proposition 7.20 Let f : ?F (D1 ) → D2 be an aggregate function and D2 , ≤ be a totally ordered set. Then bnd(f) is a three-valued aggregate relation of f. It is interesting to see how bnd(f) compares to ult(f). We ?rst show that the ?rst components of the two three-valued aggregate relations are always equal.

Well-founded and Stable Semantics of Logic Programs with Aggregates

41

Proposition 7.21 Let f : ?F (D1 ) → D2 be an aggregate function and ≤ a total order on D2 . Then bnd(f)1 = ult(f)1 . However, for most aggregate functions, bnd(f) can be less precise than ult(f), i.e., bnd(f) <p ult(f) because bnd(f)2 > ult(f)2 . Example 7.5 The pair ((?, {1, 3}), 2) is not in the relation ult(sum)2 because there is no set S ∈ [?, {1, 3}] such that sum(S ) = 2. On the other hand ((?, {1, 3}), 2) ∈ bnd(sum)2 because b1 = sum(minsum (?, {1, 3})) = sum(?) = 0, b2 = sum(maxsum (?, {1, 3})) = sum({1, 3}) = 4, and b1 ≤ 2 ≤ b2 . So, ult(sum)2 ? bnd(sum)2 and consequently bnd(sum) <p ult(sum). 7.4 On the Complexity In this section we prove a simple complexity result. A full analysis of the complexity of model generation for aggregate programs is beyond the scope of this paper but we show that, despite the second order nature of aggregates, model generation for aggregate programs may remain tractable under an appropriate choice of the three valued aggregates. The type of computational problem considered here is the model extension problem (Mitchell and Ternovska 2005): given a signature Σ(Π), an aggregate program ? which is two-valued on all prediP based on Σ(Π) and an input Σ-structure D cates and three-valued on aggregate symbols, compute the Kripke-Kleene model, the well-founded model or an exact stable model. Informally, we are interested here in the complexity for instances of these problems with ?xed P , ?xed Σ(Π), and “?xed” interpretation of the aggregate symbols in Aggr(Σ) and for varying but ?nite input Σ \ Aggr(Σ)-structures Do . The problem with this intuition is that the ? interpretation rD of a given aggregate symbol r in this class is of course not really ?xed: it varies with the input structure Do . We are interested in classes of problems where for example the sum predicate is systematically interpreted by its ultimate approximating aggregate, but evidently, the sum aggregate relation and its ultimate approximating aggregate depend on the domain of the input structure Do . To circumvent this problem, we introduce the following concepts. Let us ?x an aggregate program P based on signature Σ(Π). Consider the class C of two-valued structures of Σ \ Aggr(Σ) with a ?nite domain (i.e., with ?nite domains for every sort s). We assume a given function X from C to the class of Σ-structures such that for each Do ∈ C , X (Do ) extends Do with three-valued aggregates R for each aggregate symbol r ∈ Aggr(Σ). Moreover, we assume that for each aggregate symbol r ∈ Aggr(Σ), there are two Turing machines which, for (an appropriate encoding of) arbitrary Do ∈ C and arbitrary well-typed pair (S, d) consisting of a

42

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

? and a domain element d, compute respectively (rX (Do ) )1 (S, ? d) three-valued set S X (D o ) 2 ? and (r ) (S, d). Let X (C ) be the image class of C under the function X . The main result of this section is that if each three-valued aggregate R ∈ Aggr(Σ) is polynomially computable in the size of the domain of the input structure, i.e., if for arbitrary Do , ? and d, the Turing machines associated to R can compute (rX (Do ) )1 (S, ? d) and S X (D o ) 2 ? (r ) (S, d) in polynomial time in the size of the domain of Do (i.e., the total number of elements in all domains sDo of all sorts s), then the following holds: Theorem 7.4 ? deciding if an atom A is true in the Kripke-Kleene model of a program P extending a structure in the class X (C ) is in P; ? deciding if an atom A is true in the well-founded model of a program P extending a structure in the class X (C ) is in P; ? deciding the existence of an exact stable model of a program P extending a structure in the class X (C ) is in NP. Note that, in the common case, computing the value of an aggregate is polynomial ? (of a ?xed type s1 × · · · × sn ). Then, since in the size of the input three-valued set S the number of elements in such a set is bounded by a polynomial in the size of the domain of Do , computing the value of the aggregate is certainly polynomial in the size of the domain of the input structure Do . Proof Let L be a (?nite) lattice and A an approximation operator on Lc . Suppose that n is the length of the longest chain in L. The computation of the Kripke-Kleene and well-founded ?xpoint of A and the test whether a lattice element is an exact stable ?xpoint of A is done by monotone ?xpoint computations. It is easy to see that the number of applications of A to compute its Kripke-Kleene ?xpoint is bound by n. Also testing whether a lattice element is an exact stable ?xpoint of A requires at most n applications of A. Because the computation of the well-founded ?xpoint involves an embedded ?xpoint computation, its computation takes at most n2 applications of A. Let us now consider a model extension problem for ?xed P, Σ(Π) and aggregate extension function X . Given an input Σ \ Aggr(Σ)-structure Do , the lattice in which the computations take place is the power-set lattice I = ?(baseDo (Π)). The maximal chain length in this lattice is the number of facts, i.e., the cardinality of baseDo (Π). This number is polynomial in the size of the domain of Do . It follows then that all we need to prove to obtain the desired complexity results is that for ? ∈ I , we can compute Φaggr ? any given pair J P,X (Do ) (J ) in polynomial time in the size of the domain. ? From De?nition 7.5, it follows that Φaggr P,X (Do ) (J ) corresponds to computing the truth value of the bodies of all rule instances A ← ? ∈ inst(P ). It is clear that the number of rule instances is polynomial in the size of the domain of Do . Therefore, all we need to prove is that for an arbitrary aggregate formula ?[x] with free variables ?, for arbitrary Do ∈ C and tuple d of domain x, the truth value of ?[x/d] in J elements, can be computed in polynomial time in the domain size of Do .

Well-founded and Stable Semantics of Logic Programs with Aggregates

43

In case ? is a ?rst order formula, the polynomial computability of its truth value with respect to a three-valued structure is proven by induction on the structure of ?. We need to extend this proof with the additional case that ? is an aggregate atom. Computing the truth value of an aggregate atom r(s, d) requires ?rstly, ?, to evaluate the contained set expression s and compute its three-valued set S X (D o ) 1 ? X (D o ) 2 ? and secondly, to evaluate the truth value of (R ) (S, d) or (R ) (S, d). It follows straightforwardly from the induction hypothesis that the ?rst task can be done in polynomial time in the domain size of Do , whereas the second task is polynomial by assumption. Our main motivation for developing the semantic framework of this section was the high complexity of the ultimate well-founded and stable semantics as de?ned in Section 6. This result shows that under appropriate choice of the three-valued aggregates, we indeed obtain weaker but tractable Kripke-Kleene and well-founded semantics. The above theorem is subject to a strong limitation, in particular the restriction to ?nite structures. Many of the interesting applications of aggregates (including the company control and the shortest path problem) contain integer or real numbered domains. Frequently used aggregates such as sum and card range over these in?nite domains. Clearly, in the context of in?nite domains, only strong syntactical conditions on the form of rules can guarantee termination or tractability of the model generation process. But this is the case whether the program contains aggregate expressions or not. To discover such conditions is an important topic for future research but it is beyond the scope of this paper to investigate this issue.

7.5 Summary of the results In this and the previous section, we have introduced a family of Kripke-Kleene, a family of stable and a family of well-founded semantics for aggregate programs, parameterized by the approximation operator. We introduced also a sub-family of these semantics, obtained by extending the standard three-valued Fitting operator with di?erent three-valued aggregates. We presented two generic ways for deriving a three-valued aggregate from a given (two-valued) aggregate relation, called the trivial and the ultimate three-valued aggregate. All instances in each of the three families are consistent with each other. In particular, when one instance of the Kripke-Kleene or well-founded semantics infers that a literal is true, there is no instance in which this literal is false and any more precise instance of the same semantics will infer the same literal. Also, a model in one instance of the stable semantics is also a model in each more precise instance of the stable semantics. This shows that all instances of each of the three families of semantics basically formalize the same intuitions but with di?erent degree of precision, with the semantics based on the ultimate operator as the most precise. However, for several important subclasses of aggregate programs, optimal precision is reached using weaker approximations. As a general rule, when the well-founded model of one approximation is two-valued, then it coincides with the well-founded and unique

44

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

stable model of each more precise approximation. In Theorem 7.3 and Corollary 6.1, we proved that for de?nite aggregate programs, the least ?xpoint semantics, the ult-well-founded, ult-stable, the ultimate well-founded and the ultimate stable semantics all coincide. One example is the Company Control Example 5.2. For strati?ed aggregate programs, Theorem 7.2 showed that the standard model, the triv -well-founded and triv -stable model and the ultimate well-founded and stable model all coincide. This class was illustrated by the ?rst Shortest Path Example 7.4. In case of the second Shortest Path Example 7.4, Proposition 7.19 showed that (under some weak conditions) the ult-well-founded model is two-valued. This raises the question of what a good choice of the semantics is and how we can exploit our results to build an e?ective reasoning system for aggregate programs. Just as for standard logic programming, the family of semantics of aggregate programs o?ers a trade-o? between precision versus complexity. Therefore, choosing the “right” semantics is a pragmatic matter and the relevant question is what degree of precision is required for the applications that one has in mind. In the case of logic programs without aggregates, the standard and the ultimate semantics only di?er for programs with a rare combination of reasoning by cases and recursion, as in {p ← p ∨ ?p}. We are not aware of a single non-arti?cial example of a logic program, appearing in the literature, which shows this behaviour. This means that, de facto, the standard and the ultimate semantics coincide and the ultimate semantics can be computed using the more e?cient Fitting operator. In case of aggregate programs, the situation seems even better. It must be admitted that applications of recursion over aggregates in the literature are quite rare. We believe that this is not a coincidence. Indeed, aggregates provide a rather powerful way to avoid recursion. In a language without aggregates, the means to compute the value of some aggregate of a set of objects (e.g., cardinality, sum, minimum or maximum, . . . ) is often by using recursion over the potential elements of the set (Van Gelder 1992). By allowing aggregates in the language, such applications of recursion can be avoided. Recall that for strati?ed aggregates programs even the triv -stable and triv -well-founded semantics are su?ciently precise. As for the applications of recursion over aggregates in this paper, the Party Invitation program of Example 5.1 is to be interpreted under the supported model semantics, whereas for the second Shortest Path Example 7.4 and the Company Control Example 5.2, the ult-well-founded model is the correct solution. In summary, we believe that extensions of the standard semantics with polynomially computable three-valued aggregates, provide su?cient precision for almost all practical applications. This is the case for the ultimate approximating aggregates of card, min, max and the bound approximating aggregates of sum and prod (Pelov 2004). To us, it seems that the most suitable approximation for being incorporated in model generation or query systems for aggregate programs, is the extension of the Fitting operator with those three-valued aggregates.

Well-founded and Stable Semantics of Logic Programs with Aggregates 8 Related Work

45

Aggregate relations are closely related to generalized quanti?ers (Lindstr¨ om 1966). An example of a generalized quanti?er is most(A, B ), de?ned on page 9, which expresses that most elements of set A belong to set B . Clearly, this relation can be viewed as a binary aggregate relation with two set arguments. Standardly, the notion of generalized quanti?er is formalized in a slightly more involved way than as a second order predicate in an arbitrary domain. Instead the concept is formalized as a class of structures closed under isomorphism. For example, most could be formalized as the class of all structures consisting of a domain D and a binary relation M ? ?(D) × ?(D) consisting of all pairs (A, B ) such that A is ?nite and more than half of the elements of A belong to B . In this way, a domain independent characterization of the generalized quanti?er is obtained. Aggregates could be formalized similarly. For example, the cardinality aggregate could be formalized as the class of all structures consisting of a domain D and a binary relation C ? ?(D) × N containing all tuples (S, n) such that S is a subset of D containing n elements. An extensive study of generalized quanti?ers in three-valued logic is done by van Eijck (1996). The notion of a super-valuation interpretation of a generalized quanti?er, as de?ned there, coincides with our notion of ultimate approximating aggregate of the corresponding aggregate relation. In the context of logic programming, many di?erent approaches to aggregates have been proposed. Below, we discuss a selection of them. The class of monotonic aggregate programs (Mumick et al. 1990) is very similar to the class of de?nite aggregate programs. A monotonic program is a program in which every rule is monotonic. A monotonic rule is a rule r such that I |= body (r) and I ? J implies J |= body (r) for any pair of interpretations I and J . Although this is a semantic de?nition of monotonicity, the authors introduce a su?cient syntactic condition for monotonicity of a rule. Essentially, an aggregate atom can appear only in formulas of the form ?z r({x | q (x)}, z ) ∧ p(z, t) (1)

where p is a pre-de?ned relation. Moreover, the satis?ability of this formula must be monotone. In our syntax (1) can be expressed as the aggregate atom rP ({x | q (x)}, t) (2)

using the derived aggregate relation rP . Then, the condition that the satis?ability of (1) is monotone is equivalent to the condition that rP is a monotone aggregate relation (and consequently (2) is a positive aggregate atom). The notion of positive aggregate atoms is simpler and, in our opinion, more natural than the condition of monotonic literals of (Mumick et al. 1990). A common approach to extend the stable semantics of general logic programs with negation to aggregate programs was to treat aggregate literals as negative literals when computing the program reduct (Kemp and Stuckey 1991; Gelfond 2002; Elkabani et al. 2004). Such semantics is relatively easy to de?ne and the de?nition also extends to answer sets of disjunctive logic programs. However, it has been

46

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

shown that this semantics accepts non-minimal models and does not model correctly some problems with recursion over aggregation, for example the Company Controls program from Example 5.2 (Pelov 2004, Section 4.3.3). For aggregate programs containing only negative aggregate literals it has been shown (Pelov et al. 2004) that the set of ult-stables models is the same as the set of stable models de?ned by the above authors. A more elaborate de?nition of a stable semantics was given by (Simons et al. 2002) for programs with weight constraints and implemented by the well-known smodels system. In our language, weight constraints correspond to aggregate atoms build with the sum≤ and sum≥ aggregate relations. An extensive comparison between the ult-stable semantics and the stable semantics of weight constraints can be found in (Pelov et al. 2004; Pelov 2004) and will not be repeated here. A novel feature of the language of weight constraints was that it allows weight constraints to be present also in the head of the rules. This approach have been further developed in di?erent directions. One line of research was to consider di?erent variations and extensions of weight constraints like abstract constraints (Marek and Truszczy? nski 2004), monotone cardinality atoms (Marek et al. 2004) or set constraints (Marek and Remmel 2004). Such constraint atoms correspond in a natural way to aggregate atoms. The stable semantics of these extensions is also de?ned in terms of lattice operators. However, since constraint atoms are allowed in the heads of rules, the operators become non-deterministic and the algebraic theory is quite di?erent than the approximation theory we used in this work. However, all the semantics agree on the class of de?nite aggregate programs and its least model semantics. The equivalent of a de?nite logic program in (Marek and Remmel 2004) is called a Horn SC-logic programs and such programs are also characterized by a unique model which is the least ?xpoint of a aggr deterministic monotone operator SP which is the equivalent of our TP, D operator. Another extension of the language of weight constraint atoms is to considers arbitrary propositional formulas containing arbitrary aggregate atoms (both in the head and in the body of the rule) (Ferraris 2005). The answer set semantics for such ? -stable semantics which we de?ned. propositional formulas is di?erent than the D The main reason is that the semantics of (Ferraris 2005) is based on the logic of ? -stable semantics are based on here-and-there (Lifschitz et al. 2001) while the D Kleene’s strong three-valued logic T HREE . The simplest example of the di?erence between the two logics is that ??p is equivalent to p in T HREE while it is not in the logic of here-and-there. As a consequence, the program consisting of the single rule p ← ??p is a de?nite program according to De?nition 5.6 because ??p is a positive (aggregate) formula. So, all our semantics assign to this program the model ? On the other hand, it has two models ? and {p} according to the answer set semantics of (Lifschitz et al. 2001; Ferraris 2005). This di?erence also manifests for aggregate formulas. For example, it is easy to see that the aggregate formulas ?sum= (s, t) and sum(s, t) have the same three-valued truth value for any interpretation of sum with a three-valued aggregate relation while they are not equivalent under the semantics of (Ferraris 2005). Another proposal for a stable semantics of disjunctive logic programs extended with aggregates was given in (Faber et al. 2004). In the sequel we investigate in

Well-founded and Stable Semantics of Logic Programs with Aggregates

47

? -stable semore detail the relationship with this semantics to the family of D mantics de?ned earlier. First, we recall the de?nitions of the stable semantics of (Faber et al. 2004). De?nition 8.1 (Faber et al. 2004) The reduct P I of an aggregate program P with respect to an interpretation I is a program obtained from inst(P ) by deleting all rules in which a literal or an aggregate atom in the body is false in I . An interpretation I is a FLP-stable model of P if I is a minimal model of P I . In one direction we can show the following result. Proposition 8.1 ? , if an interpreFor any aggregate program P and for any three-valued structure D ? -stable model of P then I is a FLP-stable model of P . tation I is an D Proof ? -stable model I is also a D ? -stable model of P I . It will then We will show that any D aggr follow from Lemma 2.1, that I is a minimal pre-?xpoint of TP I ,D . Since the preaggr I ?xpoints of TP I ,D are exactly the models of P , this will imply that I is a minimal model of P I and hence, I is a FLP-stable model of P . We start by showing

aggr 1 1 ?J ? I : (Φaggr ? ) (J, I ) = (ΦP,D ? ) (J, I ). P I ,D

(*)

aggr 1 1 This will imply that lfp((Φaggr ? ) (·, I )) = lfp((ΦP,D ? ) (·, I )) = I , so I will be a P I ,D

stable model of P I . To show (*) we only need to look at the rules r ∈ P ? P I and 1 show that HD ? (J,I ) (body (r)) = f . The de?nition of reduct implies that for such a ?. rule HD(I ) (body (r)) = f where D is the (two-valued) structure approximated by D We also have that (J, I ) ≤p (I, I ) which implies that

1 1 HD ? (I,I ) (body (r)) = HD (I ) (body (r)) = f ? (J,I ) (body (r)) ≤ HD 1 So, HD ? (J,I ) (body (r)) = f .

The next example gives a program for which the two semantics disagree. Example 8.1 Consider the following aggregate program P : r ← card= ({x | p(x)}, 1). p(A) ← r. p(B ) ← r. p(A) ← p(B ). p(B ) ← p(A). The program has only one model M = {r, p(A), p(B )}. This is also a FLP-stable model because P M = P and M is also a minimal model of P . However, the program does not have an ultimate total stable model and, consequently, it does not have a total stable model for any less precise approximating operator.

48

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

To illuminate what is going on in this example, let us make the following observation. In the context of the Herbrand universe {A, B }, the aggregate atom card= ({x | p(x)}, 1) expresses that p has either zero or two elements. Or, in each two-valued Herbrand interpretation this atom is equivalent to (?p(A) ∧ ?p(B )) ∨ (p(A) ∧ p(B )). (3)

In fact, if we interpret card= by the ultimate approximating aggregate, then a simple case analysis shows that, in each three-valued Herbrand interpretation, the truth values of the aggregate atom and of the formula (3) are identical3 . It follows that the program P and the program obtained by substituting the rules r ← ?p(A) ∧ ?p(B ). r ← p(A) ∧ p(B ). for the ?rst rule in P , have identical three-valued immediate consequence operators and hence, have identical stable models4 . The second program is a standard logic program and it is easy to see that it has no stable models. In particular, if we compute the reduct under M = {r, p(A), p(B )}, only the second new rule remains and together with the rest of the rules the least model is ?. Thus M is not a stable model of the translated program. The above example illustrates a natural principle of the semantics de?ned in our framework. Substituting an aggregate atom by an aggregate free formula which is equivalent with respect to two-valued semantics, preserves ultimate well-founded and ultimate stable models. Substituting an aggregate atom by an aggregate free formula which is equivalent with respect to three-valued semantics preserves the standard well-founded and stable semantics. As shown by the example, this natural principle is not satis?ed by the semantics de?ned in (Faber et al. 2004). This is a fundamental weakness of this semantics. Finally, we mention another recent work on de?ning a stable semantics of aggregates (Son and Pontelli 2007). As shown in that paper, the semantics de?ned there coincides with the ult-stable semantics and provides an interesting di?erent formalization for this semantics. 9 Conclusions and Future Work In this paper we presented a systematic extension of all major semantics of logic programs to aggregate programs: the least ?xpoint semantics (van Emden and Kowalski 1976), the standard model of strati?ed programs (Apt et al. 1988), the supported model semantics (Apt et al. 1988), the Kripke-Kleene semantics (Fitting 1985), the stable model semantics (Gelfond and Lifschitz 1988), the well-founded semantics (Van Gelder et al. 1991),

3 4

The three-valued equivalence of ult(card= ) and (3) is an application of a general transformation of ultimate approximations of aggregate atoms to formulas (Pelov 2004, Section 5.3.6). Stronger, both three-valued and two-valued immediate consequence operators coincide, and hence, all semantics of the two programs based on these operators coincide, including ultKripke-Kleene, ult-stable and ult-well-founded semantics.

Well-founded and Stable Semantics of Logic Programs with Aggregates

49

and the ultimate stable and ultimate well-founded semantics (Denecker et al. 2004). The extension of the stable and well-founded semantics is not unique but is parameterized by how aggregate relations are extended to three-valued relations on three-valued sets. We studied three instances of these semantics. Two of them are the least precise (called triv ) and the most precise (called ult) in this family and they are de?ned in a uniform way for all aggregate relations. The third instance (called bnd) is de?ned only for aggregate functions on totally ordered sets. For some aggregates, most notably sum and prod the bnd-semantics is strictly less precise than the ult semantics. Although, we did not present here a full complexity analysis, the advantage of the bnd-semantics over the ult-semantics is that it has a lower complexity (Pelov 2004). We also showed that all important properties and relationships of the original semantics are preserved in the extension. For example, a strati?ed aggregate program ? -well-founded model which is equal to the unique D ? -stable P has a two-valued D ? of model of P and the standard model of P for any three-valued interpretation D the aggregate relations. A similar result for a de?nite aggregate program P is that the ult-well-founded model is equal to the unique ult-stable model and the least ?xpoint model of P . Another important property of all stable semantics which we de?ne is that stable models are always minimal models.

References

Apt, K. R., Blair, H. A., and Walker, A. 1988. Towards a theory of declarative knowledge. In Foundations of Deductive Databases and Logic Programming, J. Minker, Ed. Morgan Kaufmann, Chapter 2, 89–148. Davey, B. A. and Pristley, H. A. 1990. Introduction to Lattices and Order. Cambridge University Press. Dell’Armi, T., Faber, W., Ielpa, G., Leone, N., and Pfeifer, G. 2003. Aggregate functions in disjunctive logic programming: Semantics, complexity, and implementation in DLV. In 18th International Joint Conference on Arti?cial Intelligence. Morgan Kaufmann, 847–852. Denecker, M. 2000. Extending classical logic with inductive de?nitions. In 1st International Conference on Computational Logic. Lecture Notes in Arti?cial Intelligence, vol. 1861. Springer, 703–717. ? ski, M. 2000. Approximating operators, Denecker, M., Marek, V., and Truszczyn stable operators, well-founded ?xpoints and applications in non-monotonic reasoning. In Logic-based Arti?cial Intelligence, J. Minker, Ed. Kluwer Academic Publishers, 127– 144. ? ski, M. 2003. Uniform semantic treatment Denecker, M., Marek, V., and Truszczyn of default and autoepistemic logics. Arti?cial Intelligence 143, 1, 79–122. ? ski, M. 2004. Ultimate approximations and Denecker, M., Marek, V., and Truszczyn its application in nonmonotonic knowledge representation. Information and Computation 192, 1, 84–121. Denecker, M., Pelov, N., and Bruynooghe, M. 2001. Ultimate well-founded and stable model semantics for logic programs with aggregates. In 17th International Conference on Logic Programming. LNCS, vol. 2237. Springer, 212–226. Elkabani, I., Pontelli, E., and Son, T. C. 2004. Smodels with CLP and its applica-

50

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

tions: A simple and e?ective approach to aggregates in ASP. In International Conference on Logic Programming. 73–89. Faber, W., Leone, N., and Pfeifer, G. 2004. Recursive aggregates in disjunctive logic programs: Semantics and complexity. In 9th European Conference on Arti?cial Intelligence (JELIA). LNCS, vol. 3229. Springer, 200–212. Ferraris, P. 2005. Answer sets for propositional theories. In 8th International Conference on Logic Programming and Nonmonotonic Reasoning. LNCS, vol. 3662. Springer, 119– 131. Fitting, M. 1985. A Kripke-Kleene semantics for logic programs. Journal of Logic Programming 2, 4, 295–312. Gelfond, M. 2002. Representing knowledge in A-Prolog. In Computational Logic: Logic Programming and Beyond, Essays in Honour of Robert A. Kowalski, Part II, A. C. Kakas and F. Sadri, Eds. LNCS, vol. 2408. Springer, 413–451. Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming. In Logic Programming, Proc. of the 5th International Conference and Symposium. MIT Press, 1070–1080. Kemp, D. B. and Stuckey, P. J. 1991. Semantics of logic programs with aggregates. In International Logic Programming Symposium. MIT Press, 387–401. Lifschitz, V., Pearce, D., and Valverde, A. 2001. Strongly equivalent logic programs. ACM Transactions on Computational Logic 2, 4, 526–541. ¨ m, P. 1966. First order predicate logic with generalized quanti?ers. Theoria 32, Lindstro 186–195. ¨ , I., and Truszczyn ? ski, M. 2004. Logic programs with monoMarek, V., Niemela tone cardinality atoms. In 7th International Conference on Logic Programming and Nonmonotonic Reasoning. LNCS, vol. 2923. Springer, 155–166. Marek, V. and Remmel, J. 2004. Set constraints in logic programming. In 7th International Conference on Logic Programming and Nonmonotonic Reasoning. LNCS, vol. 2923. Springer, 167–179. ? ski, M. 2004. Logic programs with abstract constraint Marek, V. W. and Truszczyn atoms. In National Conference on Arti?cial Intelligence. AAAI Press / The MIT Press, 86–91. Mitchell, D. and Ternovska, E. 2005. A framework for representing and solving NPsearch problems. In Proc. of the National Conference on Arti?cial Intelligence. 430–435. Mumick, I. S., Pirahesh, H., and Ramakrishnan, R. 1990. The magic of duplicates and aggregates. In 16th International Conference on Very Large Data Bases. Morgan Kaufmann, 264–277. Pelov, N. 2004. Semantics of logic programs with aggregates. Ph.D. thesis, K.U.Leuven. Pelov, N., Denecker, M., and Bruynooghe, M. 2004. Partial stable semantics for logic programs with aggregates. In 7th International Conference on Logic Programming and Nonmonotonic Reasoning. LNCS, vol. 2923. Springer, 207–219. Ross, K. A. and Sagiv, Y. 1997. Monotonic aggregation in deductive databases. Journal of Computer and System Sciences 54, 1, 79–97. ¨ , I., and Soininen, T. 2002. Extending and implementing the stable Simons, P., Niemela model semantics. Arti?cial Intelligence 138, 1–2, 181–234. Son, T. C. and Pontelli, E. 2007. A constructive semantic characterization of aggregates in answer set programming. Theory and Practice of Logic Programming . Accepted as a Technical Note. van Eijck, J. 1996. Quanti?ers and partiallity. In Quanti?ers, Logic, and Language, J. van der Does and J. van Eijck, Eds. CSLI, 105–144.

Well-founded and Stable Semantics of Logic Programs with Aggregates

51

van Emden, M. H. and Kowalski, R. A. 1976. The semantics of predicate logic as a programming language. Journal of the ACM 23, 4, 733–742. Van Gelder, A. 1992. The well-founded semantics of aggregation. In 11th ACM Symposium on Principles of Database Systems. ACM Press, 127–138. Van Gelder, A., Ross, K. A., and Schlipf, J. S. 1991. The well-founded semantics for general logic programs. Journal of the ACM 38, 3, 620–650. Van Nuffelen, B. and Denecker, M. 2000. Problem solving in ID-logic with aggregates: some experiments. In 8th International Workshop on Nonmonotonic Reasoning, special track on Abductive Reasoning. Vennekens, J., Gilis, D., and Denecker, M. 2006. Splitting an operator: Algrebraic modularity results for logics with ?xpoint semantics. ACM Transactions on Computational Logic . Accepted.

Appendix A Proof of the Shortest Path Theorem Before proving Proposition 7.19, we ?rst introduce some concepts. We de?ne the length of a path as its number of edges. We de?ne a partial function sp(., .) as follows: sp(a, b) is de?ned if and only if there is a shortest path from a to b and sp(a, b) = w where w is the weight of the shortest path. Note that it is possible that there is a path from a to b while there is not a shortest path. E.g., consider the graph with edges {(a, a, ?1), (a, b, 1)}. It has no shortest paths. Proposition 7.19 Let edgeD be a graph with the property that for any pair of nodes a and b, if there is a path from a to b, there is a shortest path from a to b. In the ult-well-founded model of the shortest path program from Example 7.4 an atom sp(a, b, w) is: ? true if a shortest path between a and b exists and has weight w; ? false otherwise. Proof We will compute the ult-well-founded model of P by an alternating ?xpoint computation using the sequences (In )n∈N and (Jn )n∈N which are de?ned by mutual induction: ? I0 = ⊥; 2 ? Jn = St↑ ΦP (In ) = lfp(ΦP (In , ·)); 1 ? In = St↓ ΦP (Jn?1 ) = lfp(ΦP (·, Jn?1 )). We now construct this sequence until we reach a ?xpoint. 1. We show that J0 = lfp(Φ2 P (⊥, ·)) = C ∪ S where C = {cp(a, b, w) | there is a path from a to b with weight w } S = {sp(a, b, w) | there is a path from a to b with weight w }.

aggr In the ?rst iteration Φ2 P (⊥, ⊥) = TP,D (⊥) = C1 where

C1 = {cp(a, b, w) | edge(a, b, w) ∈ edgeD }.

52

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

In the next iteration, the value of cp/3 will not change because the value of sp/3 has not changed. On the other hand cp/3 has changed, so sp/3 will change now. First, let us compute the value of the set expression for values a and b: {c | cp(a, b, c)}

D (⊥,C1 )

= (?, Wab )

where Wa,b = {w | (a, b, w) ∈ edge }. i.e., there is a path between a and b of length 1. According to Table 2 in Section 7.2, it holds that ult(min)2 ((?, Wab ), x) is true for all x ∈ Wab . So, we obtain Φ2 P (⊥, C1 ) = C1 ∪ S1 where S1 = {sp(a, b, w) | edge(a, b, w) ∈ edgeD }. Continuing this process we can show by induction that for every positive integer number n > 0 we have Φ2 P (⊥, ·) ↑ (2n ? 1) =

1≤i≤n

Ci ∪

1≤i<n

Si Si

1≤i≤n

Φ2 P (⊥, ·) ↑ (2n) =

1≤i≤n

Ci ∪

where Ci = {cp(a, b, w) | there is a path from a to b of length i and weight w } Si = {sp(a, b, w) | there is a path from a to b of length i and weight w }. At the ?rst limit ordinal ω we have Φ2 P (⊥, ·) ↑ ω =

i∈N

Ci ∪

i∈N

Si = C ∪ S.

Hence, after this ?rst step, we have computed in J0 all possible path weights between any two pairs of points a and b. 2. Next we show that I1 = lfp(Φ1 P (·, C ∪ S )) = CE ∪ SP where: SP = {sp(a, b, w) | there is a shortest path from a to b of weight w } CE = {cp(a, b, w) | (a, b, w) ∈ edgeD or ?c, w1 : sp(a, c, w1 ) ∈ SP and (c, b, w ? w1 ) ∈ edgeD } De?ne also the following sets for every i > 1: SPi = {sp(a, b, w) | there is a shortest path from a to b of length i and weight w } CEi = {cp(a, b, w) | (a, b, w) ∈ edgeD or i > 1 and ?c, w1 : sp(a, c, w1 ) ∈ SPi?1 and (c, b, w ? w1 ) ∈ edgeD } Note that SP = i∈N SPi and CE = For the ?rst iteration we verify that

i∈N

CEi .

Φ1 P (⊥, C ∪ S ) = C1 = CE1 . To see why this is the case, we compute the value of the set expression: {c | cp(a, b, c)} where Aab = {w | there is a path from a to b of length w }.

(⊥,C ∪S )

= (?, Aab )

Well-founded and Stable Semantics of Logic Programs with Aggregates

53

Further, ult(min)1 ((?, Aab ), w) is false for every weight w (see Table 2 of Section 7.2). So, the interpretation of sp/3 will be the empty set. The interpretation of cp/3 will be the same as the edge relation. Hence we obtain the set CE1 . On the next iteration only the value of sp/3 will change. We have {c | cp(a, b, c)}

(CE1 ,C ∪S )

= (Wab , Aab )

and ((Wab , Aab ), w) ∈ ult(M in)1 if w ∈ Wab and the shortest path between a and b has weight w. So Φ1 P (CE1 , C ∪ S ) = CE1 ∪ SP1 . On the next iteration, the cp/3 relation becomes the composition of SP1 with the edgeD relation: Φ1 P (CE1 ∪ SP1 , C ∪ S ) = CE1 ∪ CE2 ∪ SP1 . In the next step we compute CE1 ∪ CE2 ∪ SP1 ∪ SP2 , i.e., we obtain all shortest paths of at most length 2. Continuing this process we obtain a ?xpoint which is Φ1 P (CE ∪ SP, C ∪ S ) = CE ∪ SP. At this stage, we have found all shortest paths. 2 3. Next, we show that J1 = lfp(Φ2 P (CE ∪ SP, ·)) = CE ∪ SP , i.e., ΦP (CE ∪ SP, CE ∪ SP ) = CE ∪ SP . It is straightforward to verify that cp(a, b, w) ∈ Φ2 P (CE ∪ SP, CE ∪ SP ) if and only if cp(a, b, w) ∈ CE . As for sp(a, b, w), we ?rst have to consider the value of the set expression {c | cp(a, b, c)} where Bab = Wab ∪ {w | ?c, w1 : sp(a, c, w1 ) ∈ SP ∧ (c, b, w ? w1 ) ∈ edgeD }. Either there is no path from a to b, in which case Bab is empty, and its minimum unde?ned. In this case, no sp(a, b, w) atom is derived. Or, there is a path from a to b. Then by the assumption of the proposition, there is a shortest path from a to b, say with weight w. This minimal path is either an edge from a to b or it is an extension of a shortest path from a to some vertex c. In both cases, w belongs to the set Bab and is its least element. In this case, sp(a, b, w) is derived. Hence Φ2 P (CE ∪ SP, CE ∪ SP ) = CE ∪ SP. 4. Since J1 = I1 , it follows that I2 = J1 = I1 and that we have reached a ?xpoint which is the two-valued ult-well-founded model that was to be proven.

(CE ∪SP,CE ∪SP )

= (Bab , Bab )

The following example shows that the condition in the proposition is essential for the proof. Example A.1

54

Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

Consider the following graph {(a, a, ?1), (a, b, 0)}. It is easy to see that there are no shortest paths because of the cycle in a. Hence, SP = ?. We compute the ult-well-founded model of P by an alternating ?xpoint computation. The ?rst three steps are exactly as in the proof. Things only change in the computation of J1 . For this step, the proof exploited the fact that all connected pairs have a shortest path, but this assumption does not hold anymore. We have: ? I0 = ⊥. ? J0 = {sp(a, a, ?n ? 1), sp(a, b, ?n), cp(a, a, ?n ? 1), cp(a, b, ?n) | n ∈ N}. This describes all paths in the graph. ? I1 = CE ∪ SP = {cp(a, a, ?1), cp(a, b, 0)}. Indeed, since there are no shortest paths in this graph, the set SP is empty and CE is just a copy of the edge relation. ? J1 = lfp(Φ2 P (CE, ·)). The computation is entirely similar to the ?xpoint computation of J0 (see the proof of the proposition). De?ne Ci = {cp(a, a, ?n ? 1), cp(a, b, ?n) | n ∈ [0, i]} Si = {sp(a, a, ?n), sp(a, b, ?n + 1) | n ∈ [0, i[}. Note that CE = C0 ∪ S0 . First, we compute Φ2 P (CE, CE ). Since there are no true sp atoms, the computed cp atoms correspond to the edges. Hence, cp remains unchanged. As for sp, its rule derives the atoms sp(a, a, ?1) and sp(a, b, 0), i.e., we obtain C0 ∪ S1 . In the next iteration, since cp did not change, sp remains unaltered. Now cp is extended by composing S1 with the edge relation. We obtain C1 . In the next iteration, cp remain identical, and now sp will be extended to obtain S2 . In general we have the same ?xpoint computation as for J0 except that we start at CE rather than at ⊥. It holds that Φ2 P (CE, ·) ↑ (2n) = Cn ∪ Sn Φ2 P (CE, ·) ↑ (2n + 1) = Cn ∪ Sn+1 The limit of this sequence, J1 , is equal to J0 . Therefore, I2 will be equal to I1 , so we reached the well-founded ?xpoint which is (I1 , J0 ). Since I1 = J0 , this is a three-valued model. For example, for each negative integer n, the atom sp(a, b, n) is unknown.