Choice constructs are an important addition to the language of logic programming that greatly increase its modeling capabilities. Their semantics are non-deterministic, in the sense that their might be several interpretations that satisfy a choice construct. In this paper, the semantics of logic programs with choice operators are studied using the recently proposed non-deterministic approximation fixpoint theory . We show that this allows to represent the semantics of Liu, Pontenelli, Son and Trusczczyński and generalize these semantics to the three-valued case. Furthermore, the framework allows us to give a principled account of the diference and similarities between stable model semantics of choice programs and disjunctive logic programs.
objects of study of AFT are (approximating)
operators and their fixpoints . For logic programming for
Logic programming is one of the most popular instance, it was shown that Fitting’s [6] three-valued
declarative formalisms, as it ofers an expressive, immediate consequence operator is an
approximatrule-based modelling language and eficient solvers ing operator of Van Emden and Kowalski’s [7]
twofor knowledge representation. An important part valued immediate consequence operator and that
of this expressiveness comes from choice construct, all major semantics of (normal) logic programming
that allow to state e.g. set constraints in the head of can be derived directly from this approximating
rules. For example, the rule 1 ≤ {, , } ≤ 2 ← operator. Recently, AFT was generalized to also
expresses that if is true, between 1 and 2 atoms capture non-deterministic operators [8] which allow
among , and can be true. Choice constructs for diferent options or choices in their output. It
are non-deterministic, in the sense that there is was shown that many major semantics of
disjuncmore than one way to satisfy their head. For ex- tive logic programming (specifically the weakly
supample, 1 ≤ {, , } ≤ 2 can be satisfied by { }, ported, (partial) stable, and well-founded semantics
{, }, { }, . . .. Formulating semantics for such [9]) are captured by non-deterministic AFT.
non-deterministic rules has proven a challenging In this paper, we commence an operator-based
task [
Approximation fixpoint theory (AFT) [5] is a semantics; (2) it gives immediately rise to a wide vapurely algebraic theory which was shown to unify riety of semantics, such as the three-valued fixpoint the semantics of, among others, logic programming and stable semantics, and the state semantics; (3) default logic and autoepistemic logic. The central it allows to compare these semantics with semantics for other, related formalisms, notably, disjunctive 21st International Workshop on Nonmonotonic Reasoning, logic programs; and (4) allows to use concepts inSeptember 2–4, 2023, Rhodes, Greece vestigated for AFT such as stratification [10]. $ jesse.heyninck@ou.nl (J. Heyninck) This study of choice constructs brings to light that (J. hHtetpysn:i/n/cski)tes.google.com/view/jesseheyninck the stable semantics as they are currently defined 0000-0002-3825-4052 (J. Heyninck) in non-deterministic AFT are too restrictive. This ©Cr2e0a2t3ivCeoCpyormigmhtonfosrLtihciesnpsaepAerttbryibiuttsioaunt4h.o0rsI.nUtesrenapteiromniatlte(dCCunBdeYr leads to the generaliziation of the stable semantics to CPWrEooUrckReshdoinpgs IhStpN:/c1e6u1r3-w-0s.o7r3g 4C.0E).UR Workshop Proceedings (CEUR-WS.org) what we call the constructive stable semantics. We Preorder
Type ≤ ≤ ⪯ ⪯ ⪯
Definition
Element Orders ℘( )
2 ℘( )2 × ℘( )
2 × ℘( )2 ℘(℘( )) × ℘(℘( )) ℘(℘( )) × ℘(℘( )) ℘(℘( ))2 × ℘(℘( ))2
Set-based Orders ( 1, 1) ≤ ( 2, 2) if 1 ⊆ 2 and 1 ⊇ 2 ( 1, 1) ≤ ( 2, 2) if 1 ⊆ 2 and 1 ⊆ 2 ⪯ if for every ∈ there is an ∈ s.t. ⊆ ⪯ if for every ∈ there is an ∈ s.t. ⊆ ( 1, 1) ⪯ ( 2, 2) if 1 ⪯ 2 and 2 ⪯ 1 List of the preorders used in this paper (instantiated for the lattice ⟨ , ⊆⟩). can show that these semantics generalize existing se- 2.1. Disjunctive Logic Programming and and disjunctive logic programs can be explained ex- consider a propositional1 language L, whose atomic study also sheds more light on the foundations of (representing truth), F (falsity), U (unknown), and
In what follows we formulas are denoted by , , (possibly indexed), and that contains the propositional constants T C (contradictory information). The connectives in L include negation ¬, conjunction ∧ and disjunction ∨. Formulas are denoted by , , (again, possibly indexed). Logic programs in L may be divided to diferent kinds as follows: a (propositional) disjunctive logic program set of rules of the form ⋁︀ in L (a dlp in short) is a finite =1 ← , where the head ⋁︀ and the body is a formula in L. A rule is called normal, if its body is a conjunction of literals (i.e., =1 is a non-empty disjunction of atoms, atomic formulas or negated atoms), and its head is atomic. A rule is disjunctively normal if its body is a conjunction of literals and its head is a non-empty disjunction of atoms. We will use these denominations for programs if all rules in the program satisfy the denomination, e.g. a program is normal if all its rules are normal. The set of atoms occurring in a
The semantics of dlps are given in terms of fourvalued interpretations. A four-valued interpretation of a program {T, C} and −C = C. Truth assignments to complex formulas • (, )( ) = ⎪ ⎪ ⎪ ⎧ T ⎪⎨ U
F ⎩ C if ∈ and ∈ , if ̸∈ and ∈ , if ̸∈ and ̸∈ , if ∈ and ̸∈ .
1For simplicity we restrict ourselves to the propositional
case.
mantics for choice programs [
In this section, we recall disjunctive logic proNotational Conventions and Defintiions : To increase logic program is denoted . deterministic operators (Sec. 2.2). gramming and choice programs (Sec. 2.1) and non- are then recursively defined as follows:
Immediate Consequence Operator for dlps = { ⊆ = {Δ | ⋁︀ Δ ← ︀⋃
∈ and (, )( ) = T}, HD ( ) | ∀Δ ∈ HD
( ), ∩ Δ ̸= ∅}.
Immediate Consequence Operator for choice programs { ⊆ ︀⋃ ∈ ( ) dom(hd( )) | ∀ ∈ ( ) : |= hd( )}
Ndao ℐ for disjunctive logic programs = {Δ | ⋁︀ Δ ← ∈ , (, = {Δ | = { 1 ⊆
= (ℐ ︀⋁ Δ ←
︀⋃ ℋ ℐ ℐ , , (, )
(, ) , †(, ) (, )
† (, ), 1 ∩ Δ ̸= ∅} († ∈ {, }), Ndao ℐ for choice programs , (, ), ∩ dom( ) ∈ sat( )} († ∈ {, }), program obtained by replacing in every rule in of the form 1 ∨ . . . ∨ a negated literal ¬ (1 ≤
) is a three-valued stable model of if it is a
Choice constructs have been studif ⊆ and
⊆ . quence operator for normal programs [11] is defined
An extension to dlps of the immediate conse- where dom ⊆
set of atoms
pared by two order relations: the information order , ied in several works on logic programming [
choice atom relative to a as an expression
= (dom, sat) and sat ⊆ ℘(dom). Intuitively, dom as follows: , we define: Definition 1 (Immediate Consquence operator for dlps). Given a dlp and a two-valued interpretation • HD ( )
= and (, )( ) = T}. • IC ( ) = { HD ( ), ∩ Δ ̸= ∅}.
{Δ ⊆ | ︀⋁ Δ ←
∈ ︀⋃ HD ( ) | ∀Δ
Thus, IC ( ) consists of sets of atoms that occur in activated rule heads, each sets contains at least one representative from every disjuncts of a rule in ℒ , rule
whose body is satisfied by . Denoting by ℘( ) the powerset of , IC is an operator on the lattice ⟨℘( ), ⊆⟩. ∈ , 2An overview of other semantics for dlps can be found in
previous work on non-deterministic AFT [8]. for any choice rules, and it is normal respectively monotone imation fixpoint theory as introduced by Denecker, ⊆ ′ ⊆ . A choice program is a set of Arieli and Bogaerts 2022, which generalizes approxif all of the rules are normal respectively all the Marek and Truszczyński (2000) to non-deterministic heads of rules are monotone.
operators, i.e. operators which map elements of a
We now recall the supported model-semantics [
the lattice ⟨℘( ), ⊆⟩. is denoted by ( ). from Definition 1 is a non-deterministic operator on operator IC
over ⟨ , ⊆⟩ for dlps). We recall the necessary details on non-deterministic AFT, referring to the original paper [8] for more details and explanations. ∈ is
A non-deterministic operator on ℒ is a function ( ). The operator IC : ℘( ) → ℘(℘( )) is some 1, 2, 1, 2 ⊆ ℒ , 1 × 1 ⪯ ⊆ defined as: { ⊆ sets of lattice elements, one needs a way to compare them, such as the Smyth order and the Hoare order .
Let Then: ∈ ∈ = ⟨ℒ , ≤⟩ be a lattice, and let ,
⪯ such that if for every
≤ ; and there is a ∈ such that
∈ ℘(ℒ ).
there is an ∈ ⪯ if for every ≤ . Given
2 × 2 if 1; and 1 × 1 ⪯ 2 × 2 1 ⪯
2 and 2 ⪯ if 1 ⪯ 2 and 2 ⪯ 1 : ℒ : ℒ
2 jection operator defined by (, and similarly for (, ) = (,
Let ator = ⟨ℒ , ≤⟩ 2be a lattice.
2 → ℒ , we denote by the pro
Given an oper) = (, )2.
An oper
)1, is called a nondeterministic approximating operator (ndao, for short), if it is ⪯ -monotonic (i.e. ( 1, 1) ≤ ( 2, 2)
implies ( 1, 1) ⪯ ( 2, 2)), and is exact (i.e., for every ∈ ℒ , 3Notice that we slightly abuse notation and write (, ) ∈ ) to abbreviate
∈ ( ( )(, ))2, i.e. is a lower bound ))1 and ∈ generated by ( )(, ) and is an upper bound generated by
∈ ℒ | ∈ ′)}. The stais a computation for satisfies the following principles: Convergence : ∞ ∈ IC ( ∞) Persistence of reasons : There is a sequence of
if 0 = ∅ and the sequence We now recall the definition of a computation: Definition 2.
A sequence of sets of atoms ⟨ ⟩∞=0 ator → ℘(ℒ ) ∖∅ × ℘(ℒ )∖∅ ⊆ +1, ⊆ ( ) and +1 ∈ IC programs ⟨ ⟩∞=0 such that for every ≥ 0, sistent pairs (, ( −1) with ∈ IC ′ ( −1).
Revision For every >
0, there is some ′ ⊆ Persistence of beliefs ⊆ +1 for every ≥ 0.
A set is a LPST-answer set if there is a computation for
whose result is . {, that {,
} of ({, Example 1. Consider the program ≤ 2 ← ¬ ; ← ; ← }.
We see = {
1 ≤ ℒ | and {, } ⊆ ⋃︀ } ) = ). {, ∈ ({, } } is also a LPST-answer set
) dom(hd( )) (since a computation for : ⟨∅, { }, {, }⟩. of . This is seen by observing that the following is (,
We now recall basic notions from non-deterministic approximation fixpoint theory (AFT) by Heyinck, } is a supported model, as it is a model (for any ∈ ℒ ) ( )( ) = { • ℋ • ℋ , (, , (, tive logic programs: given an interpretation (,
), ) should satisfy all choice constructs for ← ∈ has a body
that is made ∈ true by (, ) (and similarly for ℐ more formal detail, first, we define the activated by Heyninck et al (2022) and can be immediately obtained once an ndao is formulated. Due to space
that approximates the immediate consequence operator IC . The idea of designing approximation limitations, these semantics are not discussed here. operators for rules using choice constructs in rules ℐ behaves as follows for = { ∨ ← ¬ }:
HD • For any interpretation (, ) for which ̸∈ ,
) = {{, }} and thus ℐ { ⊆ dom( ) | ∀ second stable fixpoint of ℐ . (∅, {, }) is a fixpoint of ℐ
that is not stable.
The operator ℐ to fixpoints of ℐ [8]. tics of dlps: In general, (total) stable fixpoints of
correspond to (total) stable models of
and weakly supported models of ℐ [
[
In order to apply non-deterministic AFT to obtain
semantics for choice programs, the first task is to
formulate an non-deterministic approximation operator
from the literature [
, -operator based on heads that occur in rules , ( }, { }) = {{ }, {, }} × {{ }, {, }} as
It should be noticed that this operator is not well-defined for every program: {, }
←}.
Example 4. Let
For this program, no sets satisfying = {
1 < {, } < 2 ←; 2 < not defined (for any , both choice constructs exist, and thus ℐ ⊆ ). deterministic approximation operator approximating interpretation (, ), we say that: ∈ ℋ As 2 ∩ ︀⋃ {dom( ) | , ( 2, 2) and thus dom( ) ∩ 2 ∈ sat( ).
∈ , ( 1, 1)( ) ∈ ∈ ℋ ← as ℐ monotonicity. ⪯ -monotonicity follows from sym
⊆ 2, this concludes the proof of ⪯ metry and [8, Lemma 3]. Exactness is immediate, there is a rule ,
We now turn to the study of the semantics for choice
programs obtained on the basis of our approxima- fixpoints) of ℐ
:
models of
coincide with pre-fixpoints (respectively
tion operator ℐ
, which we will see give a natural
four-valued generalisation of the supported model
semantics by [
A first insight is that exact fixpoints of
incide with the supported models of Liu et al [
Proposition 2. Let a normal constraint program model of . be given. Then ∈ ℐ ,
(, ) if is a supported IC ,
isfies and thus ∈ IC ,
∈ IC , co- a three-valued supported model of . As for ev
Proof. For the ⇒-direction, suppose that (, ) is ︀⋃ ery atoms to choice constructs. Other notions will be 4In some works, these models have been called weakly supinvestigated in future work.
ported models [
This non-correspondence between pre-fixpoints and models does not hold due to the non-monotonic nature of choice constructs: for monotone choice constructs the correspondence holds: Proposition 4. Let some normal choice program with monotone choice constructs be given. Then
(, ) is a model of if ℐ is not a satisfactory generalisation of the ideas underlying the stable semantics for normal logic programs. If we take one step back, we can explain the choice for minimal fixpoints, and their shortcomings in the context of choice constructs, in stable non-deterministic operators as defined by Heyninck, Arieli and Bogaerts [8] as follows. For deterministic operators, the stable version of an approximation operator ifxpoints of (., ).
is defined as the glb of
For deterministic operators over finite lattices, the minimal fixpoint of is identical to the glb of fixpoints of (., ), and it is also identical to the fixpoint obtained by iterating (., )
We now move to the stable semantics.
We first consider the stable semantics as defined by Heyninck, Arieli and Bogaerts [8].
There, the stable ifxpoints of operator based on (., ). The usefulness of the stable was defined as the
≤ -minimal semantics as defined by Heyninck, Arieli and Bogaerts is demonstrated by the characterisation of the (partial) stable model semantics for disjunctive logic programs. However, for choice constructs, the selection of minimal fixpoints might be overly strong: Example 6. Consider the program {,
} ≤ 2 ←}. Intuitively, this rule allows to choose between one and two among and . The stable = {
1 ≤ version of IC behaves as follows:
(IC , )( ) = {{ }, { }} for any ⊆ This means that this program has two stable fixpoints according to the intuitive reading of , {, of IC : { } and { }. This is clearly undesirable, as
} should be allowed as a stable interpretation as well (notice this is also an LPST-answer set). inck, Arieli and Bogaerts [8], the glb of fixpoints of (., ) is often too weak (e.g. for the program from Example 6 we get { } ∩ { } ∩ {, as the glb of fixpoints. However, this still leaves
} = ∅ an alternative choice: namely looking at fixpoints erator as follows: Definition 5. structive lower bound operator is defined as:
Given an ndao , the complete con
We can now define the constructive complete op- Corollary 1. For any ndao , if (, ) ∈ ( )(, ) ( )( ) = { ∈ (, ) | ∃ 0, .., ∈ wfs( (., ))} (, ) ∈ ( )(, ).
We illustrate the constructive stable semantics coincide (see also [8, Proposition 11]). lattices, all notions of complete and stable operator (., ) and (, . ) are downward closed and ⪯ monotonic, (
)( ) ̸= ∅ and ( )( ) ̸= ∅. then (, ) ∈ (
)(, ) tion 5, Proof. If (, ) ∈ ( )(, ) then with Proposi
∈ ( )( ) and ∈ ( )( ) and thus
The fact that constructive stable operators generalize (minimality-based) stable operators means we can also obtain results on the well-definedness of constructive stable operators on the basis of the insights on (minimality-based) stabel operators [8].
Proposition 6. For any ndao and , ∈ ℒ s.t.
Example 7. Let allow for +1 of Definition 4, quence according to ℐ have no way of deriving just from the program . of ( ):
= {{, } = 2 ←}. If we would ⪯ ( ) in the second condition ∅, { } would be a well-founded se, (., ) (for any ⊆ {, } )
Thus, what appears to be a change to the semantics of [8] on first sight, can be seen as a mere generalization of these semantics. From the above
Proposition 5, it follows immediately that the set of }}. However, we fixpoints of ( ) is a subset of the set of fixpoints The complete constructive upper bound operator is defined analogously, and the constructive stable operator is defined as ( tor to the constructive stable operator is the ≤ minimality of stable fixpoints [ 8, Proposition 14].
This can be seen by observing that in Example 8, might be non-≤ -minimal fixpoints of (ℐ can now show the proposition. Indeed, since ⪯ -monotonic, with [8, Lemma 3], (., ) is ⪯
is monotonic. The Proposition follows from †. 6The generalisation of this result to innfiite lattices is left for future work. Proposition 7. Let a normal choice program given. tics coincide for disjunctive logic programs and their conversion into choice rules. In other words, the point in a very exact way to the diference between disjunctive logic programs and choice programs: the diference is not in how the constructs of disjunction and choice atoms are treated (i.e. when they ′=1 ¬ ′ ∈ . Clearly, should be made true or false), but rather in how which follows from +1 tence of beliefs is immediate. Revision follows from ∈ ℐ ( , ).
Persisremains to be shown is that +1 ∩dom( ) ∈ sat( ), tions, typically (e.g. in the most popular solvers ′=1 ¬ ′ ) = T as well. What the stable semantics is constructed: for disjunc← 1, . . . , implies ∈ for every = 1, . . . ,
and ′ ̸∈ (as for every ′ = 1, . . . , ′, which implies ′ ̸∈
⊆ ) for every ′ = 1, . . . , ′ and thus according to persiste nc′e of reasons. Thus, for every
( , ) for some ′ ⊆ ( ) ← ∈ ′, ( , )( ) = T implies (,
)( ) = T, which means also ( , )( ) = T. Furthermore, by definition of +1, for every satisfied by +1. Thus, +1 ∈ ℐ ← , ∈ ∖ ( , ).
′, is
according to [
This also gives an answer to the question of how to combine disjunctions and choice constructs in structs, but one has to make a choice as to which stable semantics are used: either one preserves the minimality of answer sets as in disjunctive logic proby using the constructive stable semantics. In this context, it is perhaps interesting to note that the constructive stable semantics still coincides with the standard stable semantics for normal logic programs.
In that case, all stable models are minimal.
In this paper, we studied the semantics of choice programs in the framework of non-deterministic approximation fixpoint theory.
One of the main
insights was that stable operators based on
minimality rule out intuitive acceptable models, which
lead us to formulate the constructive stable
semanset semantics defined by Liu et al [
the relation between stable semantics for disjunctive logic programs and choice programs. We first show that the operator for disjunctive logic programs is a special case of the operator for choice programs. In more technical detail, for a disjunctive logic program , we define
D2C( ) = { 1 ≤ Δ
← | } . In other words, we replace every disjunction Δ
← ∈ ︀⋁ of Δ is true (recall ℐ is defined in Example 2).
Proposition 8. For any disjunctive logic program ,
by the constraint that requires at least one element ture on logic programming [
To the best of our knowledge, this is the first application of AFT to the semantics of choice programs. As our semantics basically generalize the (2022).
341–355.
Nonsemantics of Liu et al [
The study undertaken in this paper is subject to several restrictions: we assume finite programs, in the body, and assume ℐ
) ̸= ∅ for every consistent interpretation. In future work, we will generalize our results beyond these assumptions.
Recursive aggregates in disjunctive logic programs: Semantics and complexity, in: Proceedings of JELIA’04, volume 3229 of Lecture Notes in 212. characterization of aggregates in answer set programming, Theory and Practice of Logic proximations, stable operators, well-founded ifxpoints and applications in nonmonotonic reasoning, in: Logic-based Artificial Intelligence, volume 597 of Engineering and Computer Sci2 (1985) 295–312. mantics of predicate logic as a programming language, Journal of the ACM (JACM) 23 with
external