propositionApProposition

# Operator-based semantics for choice programs: is choosing losing? (full
version)

Jesse Heyninck
Open Universiteit, the Netherlands
University of Cape Town, South-Africa

###### Abstract

Choice constructs are an important part of the language of logic programming,
yet the study of their semantics has been a challenging task. So far, only
two-valued semantics have been studied, and the different proposals for such
semantics have not been compared in a principled way. In this paper, an
operator-based framework allow for the definition and comparison of different
semantics in a principled way is proposed.

##  1 Introduction

Logic programming is one of the most popular declarative formalisms, as it
offers an expressive, rule-based modelling language and efficient solvers for
knowledge representation. An important part of this expressiveness comes from
_choice constructs_ [Simons et al., 2002], that allow to state e.g. set
constraints in the body or head of rules, and are, among others, part of the
ASP-Core-2 standard [Calimeri et al., 2012]. For example, the rule
$1\\{p,q,r\\}2\leftarrow s.$ expresses that if $s$ is true, between 1 and 2
atoms among $p$, $q$ and $r$ are true. Choice constructs are non-
deterministic, in the sense that there is more than one way to satisfy them.
For example, $1\\{p,q,r\\}2$ can be satisfied by $\\{p\\}$, $\\{p,q\\}$,
$\\{r\\}$, $\ldots$. Formulating semantics for such non-deterministic rules
has proven a challenging task [Liu et al., 2010; Marek and Remmel, 2004; Faber
et al., 2004; Son and Pontelli, 2007]: several semantics have been proposed
but no unifying framework for defining and comparing these semantics exists.
Furthermore, attention has been restricted to two-valued semantics, in
contradistinction to many other dialects for logic programming for which
three- or four-valued semantics have been proposed. Moreover, many proposed
semantics only allow for choice constructs in the body, but not in the head.
Finally, relations with the non-deterministic construct disjunction remain
unclear.

In this paper, a unifying framework for the definition and study of semantics
for logic programs with choice constructs in the head and body is provided.
This framework is based on immediate consequence operators, which are also
useful for the design of explanatory tools and provide foundations for solvers
[Kaminski and Schaub, 2023; Eiter and Geibinger, 2023]. The contributions of
this paper are the following: (1) we show how the famework of non-
deterministic approximation fixpoint theory (AFT) [Heyninck et al., 2024] can
be used to define a wide variety of supported and stable semantics for choice
logic programs, (2) we introduce the constructive stable fixpoints, allowing
to (3) generalize many existing semantics for choice programs, (4) compare
these semantics by introducing postulates, (5) provide a principled comparison
with disjunctive logic programs.

Outline of the Paper: In Section 2, the background on choice programs and non-
deterministic approximation fixpoint theory is given. In Section 3,
approximation operators for choice programs are defined. In Section 4, we
study the resulting supported semantics. In Section 5, we define stable
semantics and show representation results, while giving a postulate-based
study in Section 6. In Section 7, we relate choice constructs and
disjunctions. Related work and a conclusion follows in Sections 8 and 9.

Relation with Previous Work: This paper extends this previous work Heyninck
[2023] by also considering choice construct in the body, which gives rise to
different possible approximators, and comparing these operators using the
notion of groundedness.

##  2 Background and Preliminaries

We recall choice programs and non-deterministic AFT.

###  2.1 Choice Rules and Programs

A _choice atom_ (relative to a set of atoms $\mathscr{A}$) is an expression
$C=(\mathsf{dom},\mathsf{sat})$ where $\mathsf{dom}\subseteq\mathscr{A}$ and
$\mathsf{sat}\subseteq\wp(\mathsf{dom})$. Intuitively, $\mathsf{dom}$ denotes
the _domain_ of $C$, i.e. the atoms relevant for the evaluation of $C$,
whereas $\mathsf{sat}$ is the set of _satisfiers_ of $C$. We also denote, for
$C=(\mathsf{dom},\mathsf{sat})$, $\mathsf{dom}$ by $\mathsf{dom}(C)$ and
$\mathsf{sat}$ by $\mathsf{sat}(C)$. For a concrete example, consider
$1\\{p,q,r\\}2$ which intuitively states that between 1 and 2 of the atoms
$p$, $q$ and $r$ have to be true, corresponds to the choice atom
$(\\{p,q,r\\},\\{\\{p\\},\\{q\\},\\{r\\},\\{p,q\\},\\{p,r\\},\\{q,r\\}\\})$
(notice that $\\{p,q,r\\}$ is the domain and not a satisfier). For such choice
atoms, we assume the domain and satisfiers are clear and can be left implicit
(and similarly for constructs such as $\\{p,q\\}=1$ or $\\{p,q\\}\neq 1$).

A _choice rule_ has the form $C\leftarrow C_{1},\ldots,C_{n}$ where
$C,C_{1},\ldots,C_{n}$ are choice atoms. $C$ is called the _head_ (denoted
$\mathsf{hd}(r)$) and $C_{1},\ldots,C_{n}$ the _body_. If $C_{i}$ is a literal
(i.e. $C_{i}=(\\{\alpha\\},\\{\\{\alpha\\}\\})$, abbreviated by $\alpha$, or
$C_{i}=(\\{\alpha\\},\\{\emptyset\\})$, abbreviated by $\lnot\alpha$) for
every $i=1,\ldots,n$, we call it a _normal choice rule_. If $C$ is an atom, we
call $r$ an _aggregate rule_. A _choice program_ is a set of choice rules, and
is called normal[aggregate] if all of the rules are so. A choice atom $C$ is
_monotone_ if $\mathsf{dom}(C)\cap x\in\mathsf{sat}(C)$ implies
$\mathsf{dom}(C)\cap x^{\prime}\in\mathsf{sat}(C)$ for any $x\subseteq
x^{\prime}\subseteq\mathscr{A}$, and it is _convex_ if for any s.t.
$x\subseteq y\subseteq\mathscr{A}$, $\mathsf{dom}(C)\cap x\in\mathsf{sat}(C)$
and $\mathsf{dom}(C)\cap y\in\mathsf{sat}(C)$, $\mathsf{dom}(C)\cap
z\in\mathsf{sat}(C)$ for any $x\subseteq z\subseteq y$.

Following Liu et al. [2010], a set $x\subseteq\mathscr{A}$ _satisfies_ a
choice atom $C$ if $\mathsf{dom}(C)\cap x\in{\sf sat}(C)$. An interpretation
$x$ satisfies a rule $r$ if $x$ satisfies the head of $r$ or does not satisfy
some choice atom in the body of $r$. $x$ is a _model_ of $\mathscr{P}$ if it
satisfies every rule in $\mathscr{P}$. A rule $r\in\mathscr{P}$ is _$x$
-applicable_ if $x$ satisfies the body of $r$, and the set of $x$-applicable
rules in $\mathscr{P}$ is denoted by $\mathscr{P}(x)$. $x\subseteq\mathscr{A}$
is a _supported model_ of $\mathscr{P}$ if it is a model and
$x\subseteq\bigcup_{r\in\mathscr{P}(x)}\mathsf{dom}(\mathsf{hd}(r))$. For some
$x\subseteq\mathscr{A}$, let
$\mathit{HD}_{\mathscr{P}}(x)=\\{\mathsf{hd}(r)\mid r\in\mathscr{P}(x)\\}$ and
$\mathit{IC}_{\mathscr{P}}(x)=$

$\\{z\subseteq\bigcup_{C\in\mathit{HD}_{\mathscr{P}}(x)}\mathsf{dom}(C)\mid\forall
C\in\mathit{HD}_{\mathscr{P}}(x):z(C)={\sf T}\\}$

######  Example 1.

Consider the program $\mathscr{P}=\\{1\\{p,q\\}2\leftarrow\\{p,q\\}\neq 1\\}$.
The choice atoms behave as follows:

| $\emptyset$ | $\\{p\\}$ | $\\{q\\}$ | $\\{p,q\\}$
---|---|---|---|---
$1\\{p,q\\}2$ | ${\sf F}$ | ${\sf T}$ | ${\sf T}$ | ${\sf T}$
$\\{p,q\\}\neq 1$ | ${\sf T}$ | ${\sf F}$ | ${\sf F}$ | ${\sf T}$

This means that
$\mathit{IC}_{\mathscr{P}}(\emptyset)=\mathit{IC}_{\mathscr{P}}(\\{p,q\\})=\\{\\{p\\},\\{q\\},\\{p,q\\}\\}$,
whereas
$\mathit{IC}_{\mathscr{P}}(\\{p\\})=\mathit{IC}_{\mathscr{P}}(\\{q\\})=\\{\emptyset\\}$.
The models of $\mathscr{P}$ are $\\{p\\}$, $\\{q\\}$ and $\\{p,q\\}$, and only
$\\{p,q\\}$ is supported.

###  2.2 Approximation Fixpoint Theory

We first recall some basic algebraic notions. A _lattice_ is a partially
ordered set (poset) $\langle\mathscr{L},\leq\rangle$ s.t. for every
$x,y\in\mathscr{L}$, a least upper bound $x\sqcup y$ and a greatest lower
bound $x\sqcap y$ exist. A lattice is _complete_ if every
$X\subseteq\mathscr{L}$ has a least upper bound $\bigsqcup X$ and a greatest
lower bound $\bigsqcap X$. $\bigsqcup\mathscr{L}$ is denoted by $\top$ and
$\bigsqcap\mathscr{L}$ is denoted by $\bot$. A function $f:X\rightarrow Y$
from a poset $\langle X,\leq_{1}\rangle$ to a poset $\langle
Y,\leq_{2}\rangle$ is _monotonic_ if $x_{1}\leq_{1}x_{2}$ implies
$f(x_{1})\leq_{2}f(x_{2})$, and $x\in X$ is a _fixpoint_ of $f$ if $x=f(x)$ We
define the ordinal powers of a function $f:X\rightarrow X$ as $f^{0}(x)=x$,
$f^{\alpha+1}(x)=f(f^{\alpha}(x))$ for a successor ordinal $\alpha$, and
$f^{\alpha}(x)=\bigsqcup_{\beta<\alpha}\\!f^{\beta}(x)$ for a limit ordinal
$\alpha$. The following notation will be used: $[x,y]=\\{z\mid x\leq z\leq
y\\}$. We say a pair $(x,y)$ is consistent if $x\leq y$ and total if $x=y$.

We now recall basic notions from non-deterministic approximation fixpoint
theory (AFT) by Heyninck et al. [2024], which generalizes approximation
fixpoint theory as introduced by Denecker et al. [2000] to non-deterministic
operators. We refer to the original paper [Heyninck et al., 2024] for more
details.

The basic idea behind non-deterministic approximation operators is that we
approximate a non-deterministic operator $O$ by generating, for a given lower
bound $x$ and upper bound $y$ that approximates $z$, a set of lower bounds
$\\{x_{1},x_{2},\ldots\\}$ and a set of upper bounds
$\\{y_{1},y_{2},\ldots\\}$ that under- respectively over-approximate
$O(z)=\\{z_{1},z_{2},\ldots\\}$. Formally, a non-deterministic operator on
$\mathscr{L}$ is a function
$O:\mathscr{L}\rightarrow\wp(\mathscr{L})\setminus\\{\emptyset\\}$. For
example, the operator $\mathit{IC}_{\mathscr{P}}$ is a non-deterministic
operator on the lattice ${\langle\wp(\mathscr{A}),\subseteq\rangle}$. As the
ranges of non-deterministic operators are sets of lattice elements, one needs
a way to compare them, such as the Smyth order and the Hoare order. Let
$L={\langle\mathscr{L},\leq\rangle}$ be a lattice, and let
$X,Y\in\wp(\mathscr{L})$. Then: $X\preceq^{S}_{L}Y$ if for every $y\in Y$
there is an $x\in X$ such that $x\leq y$; and $X\preceq^{H}_{L}Y$ if for every
$x\in X$ there is a $y\in Y$ such that $x\leq y$. Given some
$X_{1},X_{2},Y_{1},Y_{2}\subseteq\mathscr{L}$, $X_{1}\times
Y_{1}\preceq^{A}_{i}X_{2}\times Y_{2}$ iff $X_{1}\preceq^{S}_{L}X_{2}$ and
$Y_{2}\preceq^{H}_{L}Y_{1}$; and $X_{1}\times Y_{1}\preceq^{S}_{t}X_{2}\times
Y_{2}$ iff $X_{1}\preceq^{S}_{L}X_{2}$ and $Y_{2}\preceq^{S}_{L}Y_{1}$. The
main orders, instantiated for the lattice of interest for this paper,
$\langle\mathscr{A},\subseteq\rangle$ are recalled in Table 1.

Let $L={\langle\mathscr{L},\leq\rangle}$ be a lattice. Given an operator
$\mathscr{O}:\mathscr{L}^{2}\rightarrow\mathscr{L}^{2}$, we denote by
$\mathscr{O}_{l}$ the projection operator defined by
$\mathscr{O}_{l}(x,y)=\mathscr{O}(x,y)_{1}$, and similarly for
$\mathscr{O}_{u}(x,y)=\mathscr{O}(x,y)_{2}$. An operator
$\mathscr{O}:\mathscr{L}^{2}\rightarrow\wp(\mathscr{L}){\setminus\emptyset}\times\wp(\mathscr{L}){\setminus\emptyset}$
is called a non-deterministic approximating operator (ndao, for short), if it
is $\preceq^{A}_{i}$-monotonic (i.e. $(x_{1},y_{1})\leq_{i}(x_{2},y_{2})$
implies $\mathscr{O}(x_{1},y_{1})\preceq^{A}_{i}\mathscr{O}(x_{2},y_{2})$),
and is _exact_ (i.e., for every $x\in\mathscr{L}$,
$\mathscr{O}(x,x)=(\mathscr{O}_{l}(x,x),\mathscr{O}_{l}(x,x))$). $(x,y)$ is a
fixpoint of $\mathscr{O}$ if $x\in\mathscr{O}_{l}(x,y)$ and
$y\in\mathscr{O}_{u}(x,y)$. A non-deterministic operator
$O:\mathscr{L}\rightarrow\wp(\mathscr{L})$ is _downward closed_ if for every
sequence $X=\\{x_{\epsilon}\\}_{\epsilon<\alpha}$ of elements in $\mathscr{L}$
such that: (1) for every $\epsilon<\alpha$,
$O(x_{\epsilon})\preceq^{S}_{L}\\{x_{\epsilon}\\}$, and (2) for every
$\epsilon<\epsilon^{\prime}<\alpha$, $x_{\epsilon^{\prime}}<x_{\epsilon}$, it
holds that $O(\bigsqcap X)\preceq^{S}_{L}\bigsqcap X$. We also introduce the
following generalisation of an approximation operator, as it will allow us to
capture some further existing semantics.

######  Definition 1.

An operator
$\mathscr{O}:\mathscr{L}^{2}\rightarrow\wp(\mathscr{L}){\setminus\emptyset}\times\wp(\mathscr{L}){\setminus\emptyset}$
is a semi-ndao iff: (1) it is exact, (2) $\mathscr{O}_{l}(\cdot,y)$ is
$\preceq^{S}_{L}$-monotonic for any $y\in\mathscr{L}$, and (3)
$\mathscr{O}_{u}(x,\cdot)$ is $\preceq^{H}_{L}$-anti-monotonic for any
$x\in\mathscr{L}$.

Any ndao is a semi-ndao (cf. Lemma 1 by Heyninck et al. [2024]). A (semi-)ndao
$\mathscr{O}$ _approximates_ an operator $O$ if $\mathscr{O}_{l}(x,x)=O(x,x)$
for every $x\in\mathscr{L}$.

We recall now stable operators (given an ndao $\mathscr{O}$). The _complete
lower stable operator_ is defined by (for any $y\in\mathscr{L}$)
$C(\mathscr{O}_{l})(y)\ =\\{x\in\mathscr{L}\mid x\in\mathscr{O}_{l}(x,y)\mbox{
and }\lnot\exists x^{\prime}<x:x^{\prime}\in\mathscr{O}_{l}(x^{\prime},y)\\}$.
The _complete upper stable operator_ is defined by (for any $x\in\mathscr{L}$)
$C(\mathscr{O}_{u})(x)\ =\ \\{y\in\mathscr{L}\mid
y\in\mathscr{O}_{u}(x,y)\mbox{ and }\lnot\exists
y^{\prime}<y:y^{\prime}\in\mathscr{O}_{u}(x,y^{\prime})\\}$. The _stable
operator_ is given by:
$S(\mathscr{O})(x,y)=(C(\mathscr{O}_{l})(y),C(\mathscr{O}_{u})(x))$. $(x,y)$
is a _stable fixpoint_ of $\mathscr{O}$ if $(x,y)\in S(\mathscr{O})(x,y)$.

Other semantics (e.g. well-founded state, Kripke-Kleene fixpoints and state
and semi-equilibrium semantics) have been defined ([Heyninck et al., 2024;
Heyninck and Bogaerts, 2023]) and can be immediately obtained once an ndao is
formulated. Due to space limitations, they are not discussed or studied here.

##  3 Approximation Operators for Choice Programs

The central task is to define non-deterministic approximations of the
immediate consequence operator $\mathit{IC}_{\mathscr{P}}$. As is usual, we
conceive of pairs of sets of atoms $(x,y)$ as _four-valued interpretations_ ,
where atoms in $x$ are _true_ whereas those in $y$ are _not false_. Thus,
assuming $x\subseteq y$, $(x,y)$ represents an approximation of some set
$z\in[x,y]$. The basic idea behind all the operators defined below is the
same: given an input interpretation $(x,y)$, we determine a set of rules that
are to be taken into account when constructing the new lower (respectively
upper bound), and then take as new lower (respectively upper bounds) the
interpretations that make true the heads of all these rules. As is well-known
already in the case for aggregate programs, there are various ways to give
formal substance to this idea. We will consider four operators inspired by
previous work on aggregate or choice programs, namely $\mathscr{IC}^{\sf
GZ}_{\mathscr{P}}$ [Gelfond and Zhang, 2014], $\mathscr{IC}^{\sf
MR}_{\mathscr{P}}$ [Marek and Remmel, 2004], $\mathscr{IC}^{\sf
LPST}_{\mathscr{P}}$ [Liu et al., 2010], and
$\mathscr{IC}^{\mathscr{U}}_{\mathscr{P}}$ [Heyninck and Bogaerts, 2023]. The
study of further operators is left for future work. Intuitively, the ${\sf
GZ}$-operator takes into account only rules of satisfied bodies whose domain
remains unchanged in $x$ and $y$. The lower bound of the ${\sf LPST}$-operator
takes into account heads of rules whose body is true in every interpretation
between $x$ and $y$, whereas the upper bound collects the results of applying
$\mathit{IC}_{\mathscr{P}}$ to every “non-false” interpretation (i.e. every
member of $[x,y]$). The lower bound of the ${\sf MR}$-operator looks at all
rules whose body is satisfied by the upper bound $y$ and by some subset of the
lower bound $x$, whereas its upper bound is identical to the ${\sf
LPST}$-operator upper bound. The $\mathscr{U}$-operator, finally, has as a
lower and upper bound the ${\sf LPST}$-operator upper bound. Given a choice
program $\mathscr{P}$ and pair of sets of atoms $(x,y)$, let:

$\displaystyle\mathscr{HD}^{{\sf GZ},l}_{\mathscr{P}}(x,y)=\\{C\mid\exists
C\leftarrow C_{1},\ldots,C_{i}\in\mathscr{P},\forall i=1\ldots n:$
$\displaystyle\hskip
71.13188ptx\cap\mathsf{dom}(C_{i})=y\cap\mathsf{dom}(C_{i})\in\mathsf{sat}(C_{i})\\},$
$\displaystyle\mathscr{HD}^{{\sf LPST},l}_{\mathscr{P}}(x,y)=\\{C\mid\exists
C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P},\forall i=1\ldots n:$
$\displaystyle\hskip 71.13188pt\forall z\in[x,y]:z(C_{i})={\sf T}\\},$
$\displaystyle\mathscr{HD}^{{\sf MR},l}_{\mathscr{P}}(x,y)=\\{C\mid\exists
C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P},\exists z\subseteq x:$
$\displaystyle\hskip 71.13188pt\forall i=1\ldots n:y(C_{i})={\sf T}\mbox{ and
}z(C_{i})={\sf T}\\},$

We then define (for ${\sf x}\in\\{{\sf LPST},{\sf MR},{\sf GZ}\\}$) the lower
bound operators by $\mathscr{IC}^{{\sf x},l}(x,y)=$

$\displaystyle\\{z\subseteq\bigcup_{C\in\mathscr{HD}^{{\sf
x},l}_{\mathscr{P}}(x,y)}\mathsf{dom}(C)\mid\forall C\in\mathscr{HD}^{{\sf
x},l}_{\mathscr{P}}(x,y):z\cap{\mathsf{dom}(C)\in\mathsf{sat}(C)}\\}$

Furthermore, we define (for $\dagger\in\\{{\sf MR},{\sf
LPST},\mathscr{U}\\}$):

$\displaystyle\mathscr{IC}^{\mathscr{U},l}_{\mathscr{P}}(x,y)$
$\displaystyle=\mathscr{IC}^{\dagger,u}_{\mathscr{P}}(x,y)$
$\displaystyle=\bigcup_{x\subseteq z\subseteq y}\mathit{IC}_{\mathscr{P}}(z)$

whereas $\mathscr{IC}^{{\sf GZ},u}_{\mathscr{P}}(x,y)=\mathscr{IC}^{{\sf
GZ},l}_{\mathscr{P}}(x,y)$. Finally, we define (for ${\sf x}\in\\{{\sf
LPST},{\sf MR},{\sf GZ},\mathscr{U}\\}$):

$\mathscr{IC}^{{\sf x}}(x,y)=(\mathscr{IC}^{{\sf x},l}(x,y),\mathscr{IC}^{{\sf
x},u}(x,y)).$

We also provide a handy summary of all operators in Table 2.

Preorder | Type | Definition
---|---|---
Element Orders
$\leq_{i}$ | $\wp(\mathscr{A})^{2}\times\wp(\mathscr{A})^{2}$ |  $(x_{1},y_{1})\leq_{i}(x_{2},y_{2})$ iff $x_{1}\subseteq x_{2}$ and $y_{1}\supseteq y_{2}$
$\leq_{t}$ | $\wp(\mathscr{A})^{2}\times\wp(\mathscr{A})^{2}$ |  $(x_{1},y_{1})\leq_{t}(x_{2},y_{2})$ iff $x_{1}\subseteq x_{2}$ and $y_{1}\subseteq y_{2}$
Set-based Orders
$\preceq^{S}_{L}$ | $\wp(\wp(\mathscr{A}))\times\wp(\wp(\mathscr{A}))$ |  $X\preceq^{S}_{L}Y$ iff for every $y\in Y$ there is an $x\in X$ s.t. $x\subseteq y$
$\preceq^{H}_{L}$ | $\wp(\wp(\mathscr{A}))\times\wp(\wp(\mathscr{A}))$ |  $X\preceq^{H}_{L}Y$ iff for every $x\in X$ there is an $y\in Y$ s.t. $x\subseteq y$
$\preceq^{A}_{i}$ | $\wp(\wp(\mathscr{A}))^{2}\times\wp(\wp(\mathscr{A}))^{2}$ |  $(X_{1},Y_{1})\preceq_{i}^{A}(X_{2},Y_{2})$ iff $X_{1}\preceq^{S}_{L}X_{2}$ and $Y_{2}\preceq^{H}_{L}Y_{1}$
Table 1: List of the preorders used in this paper (instantiated for the
lattice $\langle\mathscr{A},\subseteq\rangle$). Immediate Consequence Operator
for choice programs
---
$\mathscr{P}(x)=$ | $\\{C\leftarrow C_{1},\ldots,C_{i}\in\mathscr{P}\mid\forall i=1\ldots n:x\cap\mathsf{dom}(C_{i})\in\mathsf{sat}(C_{i})\\}$
$\mathit{HD}_{\mathscr{P}}(x)=$ | $\\{\mathsf{hd}(r)\mid r\in\mathscr{P}(x)\\}$
$\mathit{IC}_{\mathscr{P}}=$ | $\\{z\subseteq\bigcup_{C\in\mathit{HD}_{\mathscr{P}}(x)}\mathsf{dom}(C)\mid\forall C\in\mathit{HD}_{\mathscr{P}}(x):z(\mathsf{hd}(r))={\sf T}\\}$
Ndao based on Gelfond and Zhang [2014]
$\mathscr{HD}^{{\sf GZ},l}_{\mathscr{P}}(x,y)=$ | $\\{C\mid\exists C\leftarrow C_{1},\ldots,C_{i}\in\mathscr{P},\forall i=1\ldots n:x\cap\mathsf{dom}(C_{i})=y\cap\mathsf{dom}(C_{i})\in\mathsf{sat}(C_{i})\\}$
$\mathscr{IC}^{{\sf GZ},l}(x,y)=$ | $\\{z\subseteq\bigcup_{C\in\mathscr{HD}^{{\sf GZ},l}_{\mathscr{P}}(x,y)}\mathsf{dom}(C)\mid\forall C\in\mathscr{HD}^{{\sf GZ},l}_{\mathscr{P}}(x,y):z\cap{\mathsf{dom}(C)\in\mathsf{sat}(C)}\\}$
$\mathscr{IC}^{{\sf GZ},u}(x,y)=$ | $\mathscr{IC}^{{\sf GZ},l}(x,y)$
$\mathscr{IC}^{\sf GZ}(x,y)=$ | $(\mathscr{IC}^{{\sf GZ},l}(x,y),\mathscr{IC}^{{\sf GZ},u}(x,y))$
Ultimate Ndao for choice programs
$\mathscr{IC}^{\mathscr{U},l}_{\mathscr{P}}(x,y)=$ | $\bigcup_{x\subseteq z\subseteq z}\mathit{IC}_{\mathscr{P}}(z)$
$\mathscr{IC}^{\mathscr{U}}(x,y)=$ | $(\mathscr{IC}^{\mathscr{U},l}(x,y),\mathscr{IC}^{\mathscr{U},l}(x,y))$
Ndao based on Liu et al. [2010]
$\mathscr{HD}^{{\sf LPST},l}_{\mathscr{P}}(x,y)=$ | $\\{C\mid\exists C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P},i=1\ldots n:\forall z\in[x,y]:z(C_{i})={\sf T}\\},$
$\mathscr{IC}^{{\sf LPST},l}(x,y)=$ | $\\{z\subseteq\bigcup_{C\in\mathscr{HD}^{{\sf LPST},l}_{\mathscr{P}}(x,y)}\mathsf{dom}(C)\mid\forall C\in\mathscr{HD}^{{\sf LPST},l}_{\mathscr{P}}(x,y):z\cap{\mathsf{dom}(C)\in\mathsf{sat}(C)}\\}$
$\mathscr{IC}^{{\sf LPST},u}(x,y)=$ | $\mathscr{IC}^{\mathscr{U},l}(x,y)$
$\mathscr{IC}^{\sf LPST}(x,y)=$ | $(\mathscr{IC}^{{\sf LPST},l}(x,y),\mathscr{IC}^{{\sf LPST},u}(x,y))$
Ndao based on Marek and Remmel [2004]
$\mathscr{HD}^{{\sf MR},l}_{\mathscr{P}}(x,y)=$ | $\\{C\mid\exists C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P},\exists z\subseteq x:\forall i=1\ldots n:y(C_{i})={\sf T}\mbox{ and }\ z(C_{i})={\sf T}\\}$
$\mathscr{IC}^{{\sf MR},l}(x,y)=$ | $\\{z\subseteq\bigcup_{C\in\mathscr{HD}^{{\sf MR},l}_{\mathscr{P}}(x,y)}\mathsf{dom}(C)\mid\forall C\in\mathscr{HD}^{{\sf MR},l}_{\mathscr{P}}(x,y):z\cap{\mathsf{dom}(C)\in\mathsf{sat}(C)}\\}$
$\mathscr{IC}^{{\sf MR},u}(x,y)=$ | $\mathscr{IC}^{\mathscr{U},l}(x,y)$
$\mathscr{IC}^{\sf MR}(x,y)=$ | $(\mathscr{IC}^{{\sf MR},l}(x,y),\mathscr{IC}^{{\sf MR},u}(x,y))$
Table 2: Concrete Operators for dlps and choice programs

We first illustrate the behaviour of these operators:

######  Example 2.

Consider again $\mathscr{P}$ from Example 1. We will consider the three-valued
interpretation $(\\{p\\},\\{p,q\\})$. We observe that:

  * •

$\mathscr{IC}^{{\sf
MR},l}_{\mathscr{P}}(\\{p\\},\\{p,q\\})=\\{\\{p\\},\\{q\\},\\{p,q\\}\\}$,

  * •

$\mathscr{IC}^{{\sf
LPST},l}_{\mathscr{P}}(\\{p\\},\\{p,q\\})=\mathscr{IC}^{{\sf
GZ},\dagger}_{\mathscr{P}}(\\{p\\},\\{p,q\\})=\\{\emptyset\\}$ (for
$\dagger=l,u$), and

  * •

$\mathscr{IC}^{\mathscr{U},l}_{\mathscr{P}}(\\{p\\},\\{p,q\\})=\mathscr{IC}^{\mathscr{U},u}_{\mathscr{P}}(\\{p\\},\\{p,q\\}=\\{\emptyset,\\{p\\},\\{q\\},\\{p,q\\}\\}$.

Thus, $(\\{p\\},\\{p,q\\})$ is a fixpoint of the ${\sf MR}$\- and
$\mathscr{U}$-operators, but not of the ${\sf LPST}$ and ${\sf GZ}$-operators.

Unsurprisingly, these ndaos are not well-defined for every program (inevitably
so, as this already holds for $\mathit{IC}_{\mathscr{P}}$):

######  Example 3.

Let $\mathscr{P}=\\{\\{p,q\\}\neq 2\leftarrow;\\{p,q\\}=2\leftarrow\\}$. For
this program, no set satisfying both heads exists, and thus $\mathscr{IC}^{\sf
x}_{\mathscr{P}}(x,y)$ is not defined (for any $x,y\subseteq\mathscr{A}$).

We therefore making the following

Assumption: We restrict attention to programs for which
$\mathscr{IC}_{\mathscr{P}}^{{\sf x},\dagger}(x,y)\neq\emptyset$ for any
$x,y\subseteq\mathscr{A}$, ${\sf x}\in\\{{\sf LPST},{\sf MR},{\sf
GZ},\mathscr{U}\\}$ and $\dagger\in\\{l,u\\}$.

All operators are (semi-)approximators of $\mathit{IC}_{\mathscr{P}}$:111Proof
of all results in the paper, as well as additional results can be found in the
appendix. $\mathscr{IC}^{\sf LPST}_{\mathscr{P}}$ and $\mathscr{IC}^{\sf
MR}_{\mathscr{P}}$ are ndaos for $\mathit{IC}_{\mathscr{P}}$.
$\mathscr{IC}^{\sf MR}_{\mathscr{P}}$ is a semi-ndao for
$\mathit{IC}_{\mathscr{P}}$. $\mathscr{IC}^{\sf GZ}_{\mathscr{P}}$ is an ndao
for $\mathit{IC}_{\mathscr{P}}$ when restricted to consistent inputs. Consider
an arbitrary but fixed choice program $\mathscr{P}$.

${\sf x}=\mathscr{U}$

Follows from Proposition 1 by Heyninck and Bogaerts [2023].

${\sf x}={\sf LPST}$

For _$\preceq^{A}_{i}$ -monotonicity_, consider some
$(x_{1},y_{1})\leq_{i}(x_{2},y_{2})$. We first show that $\dagger$:
$\mathscr{HD}^{l,{\sf
LPST}}_{\mathscr{P}}(x_{1},y_{1})\subseteq\mathscr{HD}^{l,{\sf
LPST}}_{\mathscr{P}}(x_{2},y_{2})$ Suppose that $C\in\mathscr{HD}^{l,{\sf
LPST}}_{\mathscr{P}}(x_{1},y_{1})$, i.e. there is some $C\leftarrow
C_{1},\ldots,C_{n}\in\mathscr{P}$ s.t. for every $z\in[x_{1},y_{1}]$ and every
$i=1,\ldots,n$, $z(C_{i})={\sf T}$. Then, since
$[x_{2},y_{2}]\subseteq[x_{1},y_{1}]$, it also holds that for every
$z\in[x_{2},y_{2}]$ and every $i=1,\ldots,n$, $z(C_{i})={\sf T}$. We have thus
shown that $\mathscr{HD}^{l,{\sf
LPST}}_{\mathscr{P}}(x_{1},y_{1})\subseteq\mathscr{HD}^{l,{\sf
LPST}}_{\mathscr{P}}(x_{2},y_{2})$. To show that $\mathscr{IC}^{{\sf
LPST},l}_{\mathscr{P}}(x_{1},y_{1})\preceq^{S}_{L}\mathscr{IC}^{{\sf
LPST},l}_{\mathscr{P}}(x_{2},y_{2})$, consider now some
$z_{2}\in\mathscr{IC}^{{\sf LPST},l}_{\mathscr{P}}(x_{2},y_{2})$. We show that
$z_{2}\cap\bigcup\\{\mathsf{dom}(C)\mid C\in\mathscr{HD}^{{\sf
LPST},l}_{\mathscr{P}}(x_{1},y_{1})\\}\in\mathscr{IC}^{{\sf
LPST},l}_{\mathscr{P}}(x_{1},y_{1})$. Indeed, consider some
$C\in\mathscr{HD}^{{\sf LPST},l}_{\mathscr{P}}(x_{1},y_{1})$. Then
$C\in\mathscr{HD}^{{\sf LPST},l}_{\mathscr{P}}(x_{2},y_{2})$ (with $\dagger$)
and thus $\mathsf{dom}(C)\cap z_{2}\in{\sf sat}(C)$. As
$z_{2}\cap\bigcup\\{\mathsf{dom}(C)\mid C\in\mathscr{HD}^{{\sf
LPST},l}_{\mathscr{P}}(x_{1},y_{1})\\}\subseteq z_{2}$, this concludes the
proof of $\preceq^{S}_{L}$-monotonicity. $\preceq^{H}_{L}$-monotonicity of the
upper bound $\mathscr{IC}^{{\sf LPST},u}_{\mathscr{P}}$ follows immediately
from the previous item as $\mathscr{IC}^{{\sf
LPST},u}_{\mathscr{P}}=\mathscr{IC}^{{\cal U},u}_{\mathscr{P}}$.

It can be easily observed that $\mathscr{IC}^{{\sf
LPST},l}_{\mathscr{P}}(x,x)=\mathscr{IC}^{{\cal
LPST},u}_{\mathscr{P}}(x,x)=\mathit{IC}_{\mathscr{P}}(x)$, which demonstrates
_exactness_ and that $\mathscr{IC}_{\mathscr{P}}$ _approximates
$\mathit{IC}_{\mathscr{P}}$_.

${\sf x}={\sf MR}$

For _$\preceq^{S}_{L}$ -monotonicity_ of $\mathscr{IC}^{{\sf
MR},l}_{\mathscr{P}}(\cdot,y)$, consider some $x_{1}\subseteq x_{2}\subseteq
y\subseteq\mathscr{A}$. We show that $\mathscr{HD}^{l,{\sf
MR}}_{\mathscr{P}}(x_{1},y)\subseteq\mathscr{HD}^{l,{\sf
LPST}}_{\mathscr{P}}(x_{2},y)$, the proof of $\preceq^{S}_{L}$-monotonicity is
identical to that given in the previous item. Suppose thus that
$C\in\mathscr{HD}^{l,{\sf MR}}_{\mathscr{P}}(x_{1},y)$, i.e. there is some
$C\leftarrow C_{1},\ldots,C_{n}$ s.t. $y(C_{i})={\sf T}$ and there is some
$x\subseteq x_{1}$ s.t. $x(C_{i})={\sf T}$ (for every $i=1,\ldots,n$). But
then also $x\subseteq x_{2}$ and thus $C\in\mathscr{HD}^{l,{\sf
MR}}_{\mathscr{P}}(x_{2},y)$. $\preceq^{H}_{L}$-monotonicity of the upper
bound was established in the previous item. _Exactness_ and _approximation of
$\mathit{IC}_{\mathscr{P}}$_ are immediate.

${\sf x}={\sf GZ}$

For _$\preceq^{S}_{L}$ -monotonicity_, consider some
$(x_{1},y_{1})\leq_{i}(x_{2},y_{2})$ and $x_{2}\subseteq y_{2}$ (recall that
we restrict the input of the ${\sf GZ}$-operator to consistent pairs). We show
that $\mathscr{HD}^{l,{\sf
GZ}}_{\mathscr{P}}(x_{1},y_{1})\subseteq\mathscr{HD}^{l,{\sf
GZ}}_{\mathscr{P}}(x_{2},y_{2})$, the rest can be derived analogously to the
first item. Consider thus some $C\in\mathscr{HD}^{l,{\sf
GZ}}_{\mathscr{P}}(x_{1},y_{1})$, which means that there is some $C\leftarrow
C_{1},\ldots,C_{n}\in\mathscr{P}$ s.t.
$x_{1}\cap\mathsf{dom}(C_{i})=y_{1}\cap\mathsf{dom}(C_{i})\in\mathsf{sat}(C_{i})$
for every $i=1,\ldots,n$. As $x_{1}\subseteq x_{2}$, we see that
$x_{1}\cap\mathsf{dom}(C_{i})\subseteq x_{2}\cap\mathsf{dom}(C_{i})$ (and
similarly we see that $y_{2}\cap\mathsf{dom}(C_{i})\subseteq
y_{1}\cap\mathsf{dom}(C_{i})$). As we restricted ourselves to consistent pairs
(and thus $x_{2}\subseteq y_{2}$), we see that
$x_{1}\cap\mathsf{dom}(C_{i})=x_{2}\cap\mathsf{dom}(C_{i})=y_{2}\cap\mathsf{dom}(C_{i})=y_{1}\cap\mathsf{dom}(C_{i})$.
_Exactness_ and _approximation of $\mathit{IC}_{\mathscr{P}}$_ are immediate.

The following example shows that $\preceq^{A}_{i}$-monotonicity of
$\mathscr{IC}_{\mathscr{P}}^{\sf GZ}$ is not guaranteed when considering
inconsistent interpretations:

######  Example 4.

Consider $\mathscr{P}=\\{p\leftarrow\\{p,q\\}\neq 0\\}$. We see that

$\displaystyle(\\{p\\},\\{p\\})\leq_{i}(\\{p,q\\},\\{p\\})\quad\mbox{ yet }$
$\displaystyle\mathscr{IC}_{\mathscr{P}}^{{\sf
GZ},l}(\\{p\\},\\{p\\})=\\{\\{p\\}\\}\not\preceq^{S}_{L}\mathscr{IC}_{\mathscr{P}}^{{\sf
GZ},l}(\\{p,q\\},\\{p\\})=\\{\emptyset\\}$

To see that $\mathscr{IC}_{\mathscr{P}}^{{\sf
GZ},l}(\\{p,q\\},\\{p\\})=\\{\emptyset\\}$, observe that
$\mathsf{dom}(\\{p,r\\}\neq 0)\cap\\{p\\}\neq\mathsf{dom}(\\{p,r\\}\neq
0)\cap\\{p,q\\}$.

Furthermore, the ${\sf LPST}$ and ${\sf MR}$-operators coincide for normal
choice programs: For any normal choice program, $\mathscr{IC}^{\sf
MR}_{\mathscr{P}}(x,y)=\mathscr{IC}^{\sf LPST}_{\mathscr{P}}(x,y)$. We have to
show that $\mathscr{HD}^{l,{\sf MR}}(x,y)=\mathscr{HD}^{l,{\sf LPST}}(x,y)$
for a normal choice program $\mathscr{P}$ (the upper bound is already
identical by definition), which can be seen by observing that for any atom
$\alpha$, $z(\alpha)={\sf T}$ for every $z\in[x,y]$ iff $\alpha\in x$, and for
any negated literal $\lnot\alpha$, $z(\lnot\alpha)={\sf T}$ for every
$z\in[x,y]$ iff $\alpha\not\in y$.

######  Remark 1.

It can be easily verified that the ${\sf LPST}$ and ${\sf MR}$-operators
coincide with the four-valued Przymusinski operator for normal logic programs
[Przymusinski, 1990], which implies, with Proposition 3, Proposition 11 and
Theorem 6 by Heyninck et al. [2024], that the semantics based on these
operators faithfully generalize the (partial) supported, (partial) stable and
well-founded semantics of normal logic programs.

##  4 Supported Model Semantics

In this section, we look at the fixpoints of $\mathscr{IC}^{\sf
x}_{\mathscr{P}}$, which give a three-valued generalisation of the supported
model semantics by Liu et al. [2010] (and the three-valued model semantics of
normal logic programs). Intuitively, fixpoints of $\mathscr{IC}^{\sf
x}_{\mathscr{P}}$ generalise the idea that only atoms supported by activated
rules can be accepted.

A first insight is that the total fixpoints of all operators coincide with
_supported models_ [Liu et al., 2010]. Let a choice program $\mathscr{P}$ and
${\sf x}\in\\{{\sf LPST},{\sf MR},{\sf GZ},\mathscr{U}\\}$ be given. Then
$(x,x)$ is a fixpoint of $\mathscr{IC}^{{\sf x}}_{\mathscr{P}}$ iff $x$ is a
supported model of $\mathscr{P}$. Notice first that, as $\mathscr{IC}^{{\sf
x}}_{\mathscr{P}}$ approximates $\mathit{IC}_{\mathscr{P}}$ (Proposition 3),
$\mathscr{IC}^{{\sf x}}_{\mathscr{P}}(x,x)=\mathit{IC}_{\mathscr{P}}(x)$ for
any $x\subseteq\mathscr{A}$. For the $\Rightarrow$-direction, suppose that
$x\in\mathscr{IC}^{{\sf
x},l}_{\mathscr{P}}(x,x)=\mathit{IC}^{c}_{\mathscr{P}}(x)$. We first show $x$
is a model of $\mathscr{P}$. Indeed, consider a rule $C\leftarrow
C_{1},\ldots,C_{n}$ s.t. $x$ satisfies $C_{i}$ for $i=1,\ldots,n$. Then
$x(C_{i})={\sf T}$ and thus $C\in\mathscr{HD}^{{\sf
x},l}_{\mathscr{P}}(x,x)=\mathit{HD}_{\mathscr{P}}(x)$, which implies, since
$x\in\mathit{IC}^{c,l}_{\mathscr{P}}(x,x)$, that
$x\cap\mathsf{dom}(C)\in\mathsf{sat}(C)$. That $x$ is supported follows
immediately from the fact that $x\in\mathit{IC}_{\mathscr{P}}(x)$ implies
$z\subseteq\bigcup_{C\in\mathit{HD}^{l}_{\mathscr{P}}(x)}\mathsf{dom}(C)$. The
$\Leftarrow$-direction is analogous. However, our extension to three-valued
semantics allows to give semantics to a wider class of programs:

######  Example 5.

Let $\mathscr{P}=\\{\\{p,q\\}=1\leftarrow\\{p\\}\neq 1;p\leftarrow q.\\}$. It
can be easily checked that this program has no two-valued supported model.
However, $(\emptyset,\\{p\\})$ is a fixpoint of $\mathscr{IC}^{\sf
x}_{\mathscr{P}}$ for $x\in\\{{\sf LPST},{\sf MR},\mathscr{U}\\}$.

A more detailed investigation of conditions for the existence of fixpoints is
left for future work.

We now show that fixpoints of all four operators satisfy a notion of
supportedness, relative to how rule bodies are evaluated according to their
definition. For example, $C$ can be said to be true in $(x,y)$ according to
the ${\sf LPST}$-operator if $z(C)={\sf T}$ for every $z\in[x,y]$. We
formalize this as follows. Given $(x,y)$ and $\mathscr{IC}^{\sf
x}_{\mathscr{P}}$, $a\in x$ supported if $a$ occurs in the domain of the head
of a rule whose body is true, i.e. there is some $C\leftarrow
C_{1},\ldots,C_{n}$ s.t. $a\in\mathsf{dom}(C)$, and if would replace $C$ by
the dummy atom $p$, $p$ is the only consequence of $\mathscr{IC}^{{\sf
x},l}_{\\{p\leftarrow C_{1},\ldots,C_{n}\\}}(x,y)$ (and similarly for $y$).
Let a choice program $\mathscr{P}$ and ${\sf x}\in\\{{\sf LPST},{\sf MR},{\sf
GZ},\mathscr{U}\\}$ be given. Then $(x,y)\in\mathscr{IC}^{\sf
x}_{\mathscr{P}}(x,y)$ implies that for every $a\in y$, there is some
$C\leftarrow C_{1},\ldots,C_{n}$ with $a\in\mathsf{dom}(C)$ s.t.
$\mathscr{IC}^{{\sf x}}_{\\{p\leftarrow
C_{1},\ldots,C_{n}\\}}(x,y)=(\\{\\{p\\}\cap x\\},\\{\\{p\\}\cap y\\})$. We
show this for ${\sf x}=\mathscr{U},{\sf LPST}$, the proof of the other cases
are analogous.

${\sf x}=\mathscr{U}$

Suppose that $(x,y)\in\mathscr{IC}^{\mathscr{U}}_{\mathscr{P}}(x,y)$ and $p\in
y$ (and thus, also $p\in x$ as $x=y$ by definition of
$\mathscr{IC}^{\mathscr{U}}_{\mathscr{P}}$). This means that there is some
$z\in[x,y]$ s.t. $p\in\mathsf{dom}(C)$ for some $C\leftarrow\phi$ for which
$z(\phi)={\sf T}$. But then
$\mathscr{IC}^{\mathscr{U}}_{\\{p\leftarrow\phi\\}}(x,y)=(\\{\\{p\\}\\},\\{\\{p\\}\\})$.

${\sf x}={\sf LPST}$

Suppose that $(x,y)\in\mathscr{IC}^{\sf LPST}_{\mathscr{P}}(x,y)$ and $p\in
y$. The case for the upper bound follows from the previous case. Suppose thus
that $p\in x$. By definition of $\mathscr{IC}^{\sf LPST}$,
$p\in\bigcup_{C\in\mathscr{HD}_{\mathscr{P}}^{{\sf
LPST},l}(x,y)}\mathsf{dom}(C)$, which means that there is some $C\leftarrow
C_{1},\ldots,C_{n}$ s.t. for every $i=1,\ldots,n$, and for every for every
$z\in[x,y]$, $z(C_{i})={\sf T}$. But then $\mathscr{IC}^{{\sf
x},l}_{\\{p\leftarrow C_{1},\ldots,C_{n}\\}}(x,y)=\\{\\{p\\}\\}$.

#### Normal choice programs

We can simplify the definition of supported models for normal choice programs.
In order to do this, we first have to generalize the four-valued truth-
assignments to choice constructs. The following forms a generalization of
assignment of truth-values to choice constructs that forms a natural
generalization of the assignment of atoms to choice constructs. We first
recall the bilattice ${\sf FOUR}$, consisting of the elements ${\sf T}$
(true), ${\sf F}$ (false), ${\sf U}$ (undecided) and ${\sf C}$ (contradictory)
and two order relations $\leq_{i}$ and $\leq_{t}$:

$\leq_{i}$$\leq_{t}$${\sf U}$${\sf F}$${\sf T}$${\sf C}$

######  Definition 2.

Given a choice construct $C$ and an interpretation $(x,y)$, we say that:

  * •

${(x,y)(C)={\sf T}}$ if ${x\cap\mathsf{dom}(c)\in\mathsf{sat}(C)}$ and
$y\cap\mathsf{dom}(c)\in\mathsf{sat}(C)$;

  * •

${(x,y)(C)={\sf F}}$ if ${x\cap\mathsf{dom}(c)\not\in\mathsf{sat}(C)}$ and
$y\cap\mathsf{dom}(c)\not\in\mathsf{sat}(C)$;

  * •

$(x,y)(C)={\sf C}$ if $x\cap\mathsf{dom}(c)\in\mathsf{sat}(C)$ and
$y\cap\mathsf{dom}(c)\not\in\mathsf{sat}(C)$,

  * •

$(x,y)(C)={\sf U}$ if $x\cap\mathsf{dom}(c)\not\in\mathsf{sat}(C)$ and
$y\cap\mathsf{dom}(c)\in\mathsf{sat}(C)$.

We define _three-valued models_ of a normal choice program $\mathscr{P}$ as
consistent interpretations $(x,y)$ for which
$\bigsqcap_{\leq_{t}}\\{(x,y)(C_{i})\mid i=1\ldots n\\}\leq_{t}(x,y)(C)$ for
every $C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P}$, and _supported_ 222These
models have been called _weakly supported models_ [Brass and Dix, 1995] for
disjunctive logic programs. models as models $(x,y)$ of $\mathscr{P}$ s.t. for
every $p\in y$, there is a rule $C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P}$
with $p\in\mathsf{dom}(C)$ and $\bigsqcap_{\leq_{t}}\\{(x,y)(C_{i})\mid
i=1\ldots n\\}\geq_{t}(x,y)(p)$. I.e., a model is supported if for every non-
false atom $p$, we have a reason in the form of an activated rule for
accepting (or not rejecting) that atom.

Three-valued supported models of $\mathscr{P}$ coincide with fixpoints of
$\mathscr{IC}^{\sf LPST}_{\mathscr{P}}$ and $\mathscr{IC}^{\sf
MR}_{\mathscr{P}}$, whereas those of $\mathscr{IC}^{\sf GZ}_{\mathscr{P}}$ are
a subset of the three-valued supported models: Let some normal choice program
$\mathscr{P}$ and ${\sf x}\in\\{{\sf LPST},{\sf MR}\\}$ be given. Then $(x,y)$
is a three-valued supported model of $\mathscr{P}$ iff $(x,y)$ is a fixpoint
of $\mathscr{IC}^{\sf x}_{\mathscr{P}}$. Furthermore, if $(x,y)$ is a fixpoint
of $\mathscr{IC}^{\sf GZ}_{\mathscr{P}}$ then $(x,y)$ is supported, but not
always vice-versa. Supported models might not be fixpoints of
$\mathscr{IC}_{\mathscr{P}}^{\mathscr{U}}$ and vice-versa. Let $\mathscr{P}$
be an arbitrary but fixed normal choice program.

${\sf x}={\sf LPST},{\sf MR}$:

For the $\Rightarrow$-direction, suppose that $(x,y)$ is a three-valued
supported model of $\mathscr{P}$. As for every $p\in y$, there is a rule
$C\leftarrow\phi\in\mathscr{P}$ such that $p\in\mathsf{dom}(C)\cap x$ and
$(x,y)(\phi)\geq_{t}(x,y)(p)$, we see that
$x\subseteq\bigcup_{C\in\mathscr{HD}^{{\sf
x},l}_{\mathscr{P}}(x,y)}\mathsf{dom}(C)$ (and similarly for $y$). That for
every $C\leftarrow\phi\in\mathscr{HD}^{c,l}_{\mathscr{P}}(x,y)$,
$\mathsf{dom}(C)\cap x\in\mathsf{sat}(C)$ follows from $(x,y)$ being a model
of $\mathscr{P}$ (and similarly for $y$). For the $\Leftarrow$-direction,
suppose $(x,y)\in\mathscr{IC}^{\sf x}_{\mathscr{P}}(x,y)$. That $(x,y)$ is a
model follows straightforwardly from the definition of $\mathscr{IC}^{\sf
x}_{\mathscr{P}}(x,y)$. Consider now some $p\in y$. As
$y\subseteq\bigcup_{C\in\mathscr{HD}^{{\sf
x},u}_{\mathscr{P}}(x,y)}\mathsf{dom}(C)$, there is some
$C\leftarrow\bigwedge_{i=1}^{n}\alpha_{i}\land\bigwedge_{i=1}^{m}\lnot\beta_{i}\in\mathscr{P}$
s.t. $p\in\mathsf{dom}(C)\cap y$ (and similarly for $x$) and $\alpha_{i}\in y$
for $i=1\ldots n$ and $\beta_{j}\not\in x$ for $j=1\ldots m$.

${\sf x}={\sf GZ}$:

Suppose that $(x,y)\in\mathscr{IC}^{\sf GZ}_{\mathscr{P}}(x,y)$. That $(x,y)$
is a model follows straightforwardly from the definition of $\mathscr{IC}^{\sf
GZ}_{\mathscr{P}}(x,y)$. Consider now some $p\in y$. As
$y\subseteq\bigcup_{C\in\mathscr{HD}^{{\sf
GZ},u}_{\mathscr{P}}(x,y)}\mathsf{dom}(C)$, there is some
$C\leftarrow\bigwedge_{i=1}^{n}\alpha_{i}\land\bigwedge_{i=1}^{m}\lnot\beta_{i}\in\mathscr{P}$
s.t. $p\in\mathsf{dom}(C)\cap y$ (and similarly for $x$) and $\alpha_{i}\in y$
for $i=1\ldots n$ and $\beta_{j}\not\in x$ for $j=1\ldots m$. Thus $(x,y)$ is
a supported model.

Supported models might not be fixpoints of the ${\sf GZ}$-operator: For this,
consider $\mathscr{P}=\\{p\leftarrow\lnot q;q\leftarrow\lnot p\\}$. Then
$(\emptyset,\\{p,q\\})$ is a supported model. Yet as
$\emptyset\cap\\{q\\}\neq\\{p,q\\}\cap\\{q\\}$ (and similarly for $p$),
$\mathscr{IC}^{\sf
GZ}_{\mathscr{P}}(\emptyset,\\{p,q\\})=(\emptyset,\emptyset)$.

${\sf x}=\mathscr{U}$:

Supported models might not be fixpoints of the $\mathscr{U}$-operator:
Consider the program $\mathscr{P}=\\{p\leftarrow q;q\leftarrow\lnot q\\}$.
Then $(\emptyset,\\{p,q\\})$ is a supported model. However, as
$\bigcup_{z\subseteq\\{p,q\\}}\mathit{IC}_{\mathscr{P}}(z)=\\{\\{p,q\\}\\}$,
we see that
$\emptyset\not\in\mathscr{IC}^{l,\mathscr{U}}_{\mathscr{P}}(\emptyset,\\{p,q\\})$.

Fixpoints of the $\mathscr{U}$-operator might not be supported models:
Consider the program $\mathscr{P}=\\{1\\{p,q\\}\leftarrow p,\lnot q\\}$. Then
$\mathscr{IC}_{\mathscr{P}}^{\mathscr{U}}(\\{p\\},\\{p,q\\})=(\\{\\{p\\},\\{q\\},\\{p,q\\}\\},\\{\\{p\\},\\{q\\},\\{p,q\\}\\})$
and thus $(\\{p\\},\\{p,q\\})$ is a fixpoint. However, it is not supported, as
$(\\{p\\},\\{p,q\\})(\lnot q)={\sf U}$ yet $(\\{p\\},\\{p,q\\})(p)={\sf T}$
(i.e. we cannot find any support for $p$ being true).

#### Models as pre-fixpoints

It is well-known that for many non-monotonic formalisms, pre-fixpoints of an
operator can characterise models of the corresponding knowledge base. For the
general case of choice constructs, this correspondence does not hold:

######  Example 6.

Consider $\mathscr{P}=\\{{\\{p,q\\}=1\leftarrow}\\}$. Then
$(\\{p,q\\},\\{p,q\\})$ is a pre-fixpoint of $\mathscr{IC}_{\mathscr{P}}$ (as
$\mathscr{IC}_{\mathscr{P}}(\\{p,q\\},\\{p,q\\})=\\{\\{p\\},\\{q\\}\\}\times\\{\\{p\\},\\{q\\}\\}\preceq^{S}_{t}(\\{p,q\\},\\{p,q\\})$)
yet it is not a model (as the only models are $\\{p\\}$ and $\\{q\\}$): there
is no way to prove $p$ and $q$.

For choice programs with monotone heads, this correspondence _does_ hold: Let
some choice program $\mathscr{P}$ s.t. for every $C\leftarrow
C_{1},\ldots,C_{n}$, $C$ is monotone and some ${\sf x}\in\\{{\sf LPST},{\sf
MR},{\sf GZ},\mathscr{U}\\}$ be given. Then $x$ is a model of $\mathscr{P}$
iff $\mathscr{IC}^{l,{\sf x}}_{\mathscr{P}}(x,x)\preceq^{S}_{L}x$. Suppose
that $\mathscr{P}$ is a choice program with monotone choice constructs in the
head. For the $\Rightarrow$-direction, suppose that $x$ is a model of
$\mathscr{P}$. We show that
$x\cap\bigcup_{C\in\mathit{HD}(x)_{\mathscr{P}}(x)}\mathsf{dom}(C)\in\mathit{IC}_{\mathscr{P}}(x)=\mathscr{IC}^{{\sf
x},l}_{\mathscr{P}}(x,x)$ for any ${\sf x}\in\\{{\sf LPST},{\sf MR},{\sf
GZ},\mathscr{U}\\}$ (Notice that
$\mathit{IC}_{\mathscr{P}}(x)=\mathscr{IC}^{{\sf x},l}_{\mathscr{P}}(x,x)$
holds in view of Proposition 3), which implies $\mathscr{IC}^{{\sf
x},l}_{\mathscr{P}}(x,x)\preceq^{S}_{t}x$. Indeed, consider some
$C\in\mathit{HD}(x)_{\mathscr{P}}(x)$, i.e. there is some $C\leftarrow
C_{1},\ldots,C_{n}\in\mathscr{P}$ with $\mathsf{dom}(C_{i})\cap
x\in\mathsf{sat}(C_{i})$ for $i=1,\ldots,n$. As $x$ is a model, also
$\mathsf{dom}(C)\cap x\in\mathsf{sat}(C)$. Thus
$x\cap\mathsf{dom}(C)\in\mathit{IC}_{\mathscr{P}}(x)$. The
$\Leftarrow$-direction is similar.

##  5 Stable Semantics

We now move to the stable semantics, whose main aim is favvoding the
acceptance of self-supporting cycles, e.g. accepting $(\\{p\\},\\{p\\})$ as a
reasonable model of the program $\\{p\leftarrow p\\}$. For the deterministic
case, this is done by looking at fixpoints of the _stable operator_ , obtained
by calculating a new lower bound as the least fixpoint of
$\mathscr{O}_{l}(\cdot,y)$, where $y$ is the input upper bound (and similarly
for the upper bound). Intuitively, we take the least information the upper
bound obliges use to derive. In contradistinction to the deterministic case,
there are divergent options for how to define stable semantics for non-
deterministic operators. We first consider the minimality-based stable
semantics known from non-deterministic AFT [Heyninck et al., 2024], defined as
the $\leq$-minimal fixpoints of $\mathscr{O}_{l}(.,y)$ (cf. Section 2.2),
which where shown to generalize the (partial) stable model semantics for
disjunctive (aggregate) programs [Heyninck et al., 2024; Heyninck and
Bogaerts, 2023]. For choice constructs, this construction is overly strong:

######  Example 7.

Consider the program $\mathscr{P}=\\{1\\{p,q\\}2\leftarrow\\}$. Intuitively,
this rule allows to choose between one and two among $p$ and $q$. The stable
version of $\mathscr{IC}^{\sf x}_{\mathscr{P}}$ (cf. Section 2.1) behaves as
follows (for any ${\sf x}={\sf LPST},{\sf MR},{\sf GZ}$):

$S(\mathscr{IC}^{{\sf x},l}_{\mathscr{P}})(x)=\\{\\{p\\},\\{q\\}\\}\mbox{ for
any }x\subseteq\mathscr{A}$

$\\{p\\}$ and $\\{q\\}$ are the two stable fixpoints of $\mathscr{IC}^{\sf
x}_{\mathscr{P}}$. This is undesirable, as according to the intuitive reading
of $\mathscr{P}$, $\\{p,q\\}$ should also be allowed as a stable
interpretation.

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 [Heyninck et al., 2024] as follows. For deterministic
operators, the stable version of an approximation operator $\mathscr{O}$ is
defined as the greatest lower bound (glb) of fixpoints of
$\mathscr{O}_{l}(.,y)$. For deterministic operators over finite lattices, the
minimal fixpoint of $\mathscr{O}_{l}(.,y)$ are identical to the glb of
fixpoints of $\mathscr{O}_{l}(.,y)$, and it is also identical to the fixpoint
obtained by iterating $\mathscr{O}_{l}(.,y)$ starting from $\bot$ (i.e.
$\bigcup_{i=1}^{\infty}\mathscr{O}_{l}^{i}(\bot,y)$). For non-deterministic
operators, this correspondence does not hold. Indeed, the glb of fixpoints of
$\mathscr{O}_{l}(.,x)$ is often too weak (e.g. for the program $\mathscr{P}$
from Example 7 we get $\\{p\\}\cap\\{q\\}\cap\\{p,q\\}=\emptyset$ as the glb
of fixpoints). However, this still leaves a third choice: namely looking at
fixpoints reachable by applications of $\mathscr{O}_{l}(.,y)$ starting from
$\bot$. E.g. for choice programs, we are interested in the fixpoints of
$\mathscr{IC}^{{\sf x},l}_{\mathscr{P}}(.,y)$ that can built them up from the
ground up (i.e. from $\emptyset$) by a sequence of applications of
$\mathscr{IC}^{{\sf x},l}_{\mathscr{P}}(.,y)$. We first generalize the notion
of a well-founded sequence by Denecker and Vennekens [2014]:

######  Definition 3.

Given a non-deterministic operator $O:\mathscr{L}\to\wp(\mathscr{L})$ over a
complete lattice, a sequence $x_{0},\ldots,x_{n}\subseteq\mathscr{L}$ is
_well-founded relative to $O$_ if: (1) $x_{0}=\bot$; (2) $x_{i}\leq x_{i+1}$
and $x_{i+1}\in O(x_{i})$ for every successor ordinal $i\geq 0$; and (3)
$x_{\lambda}=\mathrm{(}\bigsqcap\\{x_{i}\\}_{i<\lambda})$ for a limit ordinal
$\lambda$. The well-founded sequences relative to $O$ are denoted by ${\sf
wfs}(O)$.

######  Remark 2.

The assumption of a complete lattice in Definition 3 is needed since the
greatest lower bound is used in point 3 of Definition 3.

Notice that, in contradistinction to the deterministic version of a well-
founded sequence Denecker and Vennekens [2014], we require not merely that
$x_{i+1}\preceq^{S}_{L}O(x_{i})$ (or, in the case of deterministic operators
$O$, $x_{i+1}<O(x_{i})$) but $x_{i+1}\in O(x_{i})$. This is to ensure that
$x_{i+1}$ can actually be constructed from $x_{i}$. For non-deterministic
operators, this is not ensured by $x_{i+1}\preceq^{S}_{L}O(x_{i})$:

######  Example 8.

Let $\mathscr{P}=\\{\\{p,q\\}=2\leftarrow\\}$. If we would allow for
$x_{i+1}\preceq^{S}_{L}O(x_{i})$ in Definition 3.(2), $\emptyset,\\{p\\}$
would be a well-founded sequence according to
$\mathscr{IC}^{l}_{\mathscr{P}}(\cdot,y)$ (for any $y\subseteq\\{p,q\\}$) as
$\\{p\\}\preceq^{S}\mathscr{IC}^{l}_{\mathscr{P}}(\\{p\\},y)=\\{\\{p,q\\}\\}$.
However, we have no way of deriving just $p$ from the program $\mathscr{P}$.

We now define the _constructive stable operator_ :

######  Definition 4.

Given an semi-ndao $\mathscr{O}$ over a complete lattice $\mathscr{L}$ with
$y\in\mathscr{L}$, the _c(onstructive)-complete lower bound operator_ is
defined as:

$C^{c}(\mathscr{O}_{l})(y)=\\{x\in\mathscr{O}_{l}(x,y)\mid\exists
x_{0},..,x\in{\sf wfs}(\mathscr{O}_{l}(.,y))\\}$

The _c-complete upper bound operator_ $C^{c}(\mathscr{O}_{u})$ is defined
analogously, and the _c-stable operator_ is defined as
$S^{c}(\mathscr{O})(x,y)=(C^{c}(\mathscr{O}_{l})(y),C^{c}(\mathscr{O}_{u})(x))$.
$(x,y)$ is a _c-stable fixpoint_ iff $(x,y)\in S^{c}(\mathscr{O})(x,y)$.

######  Example 9 (Example 7 continued).

Consider again the program from Example 7. We see that (for any
$y\subseteq\\{p,q\\}$), $S^{c}(\mathscr{IC}^{{\sf
x},l}_{\mathscr{P}})(y)=\\{\\{p\\},\\{q\\},\\{p,q\\}\\}$, as
$\emptyset,\\{p\\}$, $\emptyset,\\{q\\}$ and $\emptyset,\\{p,q\\}$ are all
well-founded sequences. Thus, the total c-stable fixpoints of
$\mathit{IC}^{{\sf x}}_{\mathscr{P}}$ are $(\\{p\\},\\{p\\})$,
$(\\{q\\},\\{q\\})$ and $(\\{p,q\\},\\{p,q\\})$ (for ${\sf x}={\sf LPST},{\sf
MR},{\sf GZ},\mathscr{U}$).

It is easy to see that for a deterministic operator over a complete lattice,
the c-stable operator coincides with the stable operator known from
deterministic AFT. The c-stable operator generalizes the minimality-based one:
Let an (semi-)ndao $\mathscr{O}$ over a complete lattice
$L=\langle\mathscr{L},\leq\rangle$ be given s.t. $\mathscr{O}_{u}(x,\cdot)$ is
$\preceq^{S}_{L}$-monotonic for any $x\in\mathscr{L}$. Then
$C^{c}(\mathscr{O}_{\dagger})(y)\supseteq C(\mathscr{O}_{\dagger})(y)$ for any
$y\in\mathscr{L}$ and $\dagger=l,u$. Furthermore, if $(x,y)\in
S(\mathscr{O})(x,y)$ then $(x,y)\in S^{c}(\mathscr{O})(x,y)$. We first show
that $(\dagger)$: for any $\preceq^{S}_{L}$-monotonic operator $O$, for every
$x\in\min_{\leq}\\{x\in\mathscr{L}\mid x\in O(x)\\}$, there is a well-founded
sequence $x_{0},\ldots,x_{n},x$ relative to $O$. Indeed, as $O$ is
$\preceq^{S}_{L}$-monotonic, for any $x_{1}\leq x$,
$O(x_{1})\preceq^{S}_{L}O(x)\ni x$, i.e. there is some $x_{2}\in O(x_{1})$
with $x_{2}\leq x$. This means we can define a $\leq$-monotonic operator
$O_{s}:\\{x\in\mathscr{L}\mid x^{\prime}\leq
x\\}\rightarrow\\{x^{\prime}\in\mathscr{L}\mid x^{\prime}\leq x\\}$ by simply
defining a selection function that selects some $x_{2}\in O(x_{1})$ s.t.
$x_{2}\leq x$ for every $x_{1}\leq x$. We now show that
$\\{x^{\prime}\in\mathscr{L}\mid x^{\prime}\leq x\\}$ is a complete partially
ordered set. Indeed, consider some $X\subseteq\\{x^{\prime}\in\mathscr{L}\mid
x^{\prime}\leq x\\}$. As $L$ is a complete lattice, $\bigsqcup
X\in\mathscr{L}$. As every $x^{\prime}\in X$, $x^{\prime}\leq x$, also
$\bigsqcup X\leq x$, thus $\bigsqcup X\in\\{x^{\prime}\in\mathscr{L}\mid
x^{\prime}\leq x\\}$. As $\\{x^{\prime}\in\mathscr{L}\mid x^{\prime}\leq x\\}$
is a complete partially ordered set and $O_{s}$ is a monotone mapping, with
Theorem 5.1 of Cousot and Cousot [1979], we know that there is a unique well-
founded sequence $O_{s}^{1}(\bot),O_{s}^{2}(\bot)\ldots x^{\prime}$ that
results in a least fixpoint $x^{\prime}$ of $O_{s}$. Clearly also $x^{\prime}$
is a fixpoint of $O$. As $x$ is a minimal fixpoint of $O$ and $x^{\prime}\leq
x$, $x=x^{\prime}$.

We can now show the first part of the proposition. We first show that
$C^{c}(\mathscr{O}_{l})(y)\supseteq C(\mathscr{O}_{l})(y)$: since
$\mathscr{O}$ is $\preceq^{A}_{i}$-monotonic, with Lemma 2 by Heyninck et al.
[2024] respectively the definition of a semi-ndao, $\mathscr{O}_{l}(.,y)$ is
$\preceq^{S}_{L}$-monotonic, which with $\dagger$ implies
$C^{c}(\mathscr{O}_{l})(y)\supseteq C(\mathscr{O}_{l})(y)$. That
$C^{c}(\mathscr{O}_{u})(y)\supseteq C(\mathscr{O}_{u})(y)$ follows with the
assumption that $\mathscr{O}_{u}(x,\cdot)$ is $\preceq^{S}_{L}$-monotonic and
$\dagger$.

For the second part, observe that if $(x,y)\in S(\mathscr{O})(x,y)$ then with
the first part, $x\in S^{c}(\mathscr{O}_{l})(y)$ and $y\in
S^{c}(\mathscr{O}_{u})(x)$ and thus $(x,y)\in S^{c}(\mathscr{O})(x,y)$.

Thus, what might appear to be a change to the previously formulated stable
semantics for non-deterministic approximation operators [Heyninck et al.,
2024], is a mere generalization of these semantics.

In general, non-deterministic operators might not admit a fixpoint, which
means that the c-complete operator is not always well-defined (e.g.
$C^{c}(O_{l})(x)=\emptyset$ or $C^{c}(O_{u})(y)=\emptyset$). We illustrate
this for $C^{c}(O_{u})(y)$, by giving an example of a
$\preceq^{H}_{L}$-monotonic operator that does not admit a well-founded
sequence.

######  Example 10.

Let $O:\mathbb{N}\cup\\{\infty\\}$ where $O(i)=\\{i+1\\}$ for any
$i\in\mathbb{N}$ and $\mathbb{\infty}=\mathbb{N}$. Observe that $O$ is
$\preceq^{H}_{L}$-monotonic, as for any finite $i,j$ s.t. $i\leq j$,
$O(i)=\\{i+1\\}$ and $i+1\leq j+1\in O(j)$, and for any finite $i$, $i\in
O(\infty)$. However, it is clear that $O$ admits no fixpoint and thus no well-
founded sequence.

To ensure well-definedness of the c-stable operator we will assume that the
lower bound is downwards closed and the upper bound satisfies the following,
analogous, notion, called _upwards closedness_ :

######  Definition 5.

An operator $O$ is _upwards closed_ if for every sequence
$X=\\{x_{\epsilon}\\}_{\epsilon<\alpha}$ of elements in $\mathscr{L}$ s.t.

  1. 1.

for every $\epsilon<\alpha$, $x_{\epsilon}\preceq^{H}_{L}O(x_{\epsilon})$, and

  2. 2.

for every $\epsilon^{\prime}<\epsilon<\alpha$,
$x_{\epsilon^{\prime}}<x_{\epsilon}$,

it holds that $\bigsqcup X\preceq^{H}_{L}O(\bigsqcup X)$.

It can be easily observed that the operator from Example 10 is not upwards
closed. Downwards closedness of $\mathscr{O}_{l}(\cdot,y)$ and upwards
closedness of $\mathscr{O}_{l}(x,\cdot)$ guarantee well-definedness of the
c-stable operator: For any (semi-)ndao $\mathscr{O}$ over a complete lattice
s.t. $\mathscr{O}_{l}(.,y)$ is downwards closed and $\mathscr{O}_{u}(x,.)$ is
upwards closed for any $x,y\in\mathscr{L}$,
$C^{c}(\mathscr{O}_{l})(y)\neq\emptyset$ and
$C^{c}(\mathscr{O}_{y})(x)\neq\emptyset$. We first show that
$C^{c}(\mathscr{O}_{l})(y)\neq\emptyset$. Suppose first that $\mathscr{O}$ is
an ndao. Then the proposition is immediate as
$C(\mathscr{O}_{l})(y)\neq\emptyset$ and $C(\mathscr{O}_{y})(x)\neq\emptyset$
in view of Proposition 13 by Heyninck et al. [2024] and
$C^{c}(\mathscr{O}_{l})(y)\supseteq C(\mathscr{O}_{l})(y)$ and
$C^{c}(\mathscr{O}_{u})(x)\supseteq C(\mathscr{O}_{u})(x)$ (Proposition 5). In
fact, it can be checked that the proof of Proposition 13 by Heyninck et al.
[2024], which means the proofs generalize to semi-ndaos.

We now show that $C^{c}(\mathscr{O}_{y})(x)\neq\emptyset$. For this, we show
some intermediate results (Lemma 1 and Lemma 2). It will be useful to define,
given a non-deterministic operator $O$ over $\mathscr{L}$, a post-fixpoint of
$O$ is any $x\in\mathscr{L}$ s.t. $x\preceq^{H}_{L}O(x)$.

######  Lemma 1.

Let $O$ be an upwards closed $\preceq^{H}_{L}$-monotonic operator over a
complete lattice. Then any $\leq$-maximal post-fixpoint of $O$ is also a
fixoint of $O$.

###### Proof.

Suppose that $x$ is a $\leq$-maximal post-fixpoint of $O$. Thus,
$\\{x\\}\preceq^{H}_{L}O(x)$, i.e. there is some $z\in O(x)$ s.t. $x\leq z$.
As $O$ is $\preceq^{H}_{L}$-monotonic, this implies $O(x)\preceq^{H}_{L}O(z)$,
and, as $z\in O(x)$, this means that $\\{z\\}\preceq^{H}_{L}O(z)$, which means
that $z$ is a post-fixpoint. As $x$ is a $\leq$-maximal post-fixpoint and
$x\leq z$, this implies $z=x$. Thus, $x\in O(x)$ which means $x$ is a fixpoint
of $O$. ∎

######  Lemma 2.

Any upwards closed $\preceq^{H}_{L}$-monotonic operator over a complete
lattice admits a fixpoint.

###### Proof.

Consider a complete lattice $L=\langle\mathscr{L},\leq\rangle$ and suppose
that $O$ is a $\preceq^{H}_{L}$-monotonic operator. Clearly, the set of post-
fixpoints of $O$ is a partially ordered set. With upwards closedness, every
chain of post-fixpoints has an upper bound (which is also a post-fixpoint),
and thus, by the Kuratowski-Zorn lemma [Kuratowski, 1922; Zorn, 1935], there
is a maximal post-fixpoint. With Lemma 1, this maximal post-fixpoint is a
fixpoint. ∎

We have established thus that $\mathscr{O}_{u}(x,\cdot)$ admits a fixpoint (as
$\mathscr{O}_{u}(x,\cdot)$ is a $\preceq^{H}_{L}$-monotonic operator for any
(semi)-ndao $\mathscr{O}$ and any $x\in\mathscr{L}$). We can show, analogous
to the proof of Proposition 5, that this means a well-founded sequence exists.

We now show that the c-stable operator is well-defined for all of the ndao’s
considered in this paper for choice programs $\mathscr{P}$ built up from
choice atoms whose domain is finite. This is a sufficient condition: other
conditions might also guarantee well-definedness. For most applications, this
assumption seems warranted. Let a choice program $\mathscr{P}$ s.t. for every
$C_{1}\leftarrow C_{2},\ldots,C_{n}\in\mathscr{P}$, $\mathsf{dom}(C_{i})$ is
finite for $i=1\ldots n$, and ${\sf x}\in\\{{\sf MR},{\sf
LPST},\mathscr{U}\\}$ and $x\subseteq y\subseteq\mathscr{A}$ be given. Then
$S^{c}(\mathscr{IC}_{\mathscr{P}}^{\sf x})(x,y)\neq\emptyset$. Furthermore,
$C^{c}(\mathscr{IC}^{{\sf GZ},l}_{\mathscr{P}})(y)\neq\emptyset$.333Notice
that, as $\mathscr{IC}^{{\sf GZ},u}_{\mathscr{P}}$ is only
$\preceq^{H}_{L}$-monotonic for consistent inputs, the complete operator for
the upper-bound will not be well-defined as it starts from
$\mathscr{IC}_{\mathscr{P}}^{{\sf GZ},u}(x,\emptyset)$. This means that the
${\sf GZ}$-operator is only useful for total stable fixpoints. We first show
$C^{s}(\mathscr{IC}_{\mathscr{P}}^{{\sf x},l})(\cdot,y)\neq\emptyset$ for any
$y\subseteq\mathscr{A}$. We have to show that $\mathscr{IC}^{l,{\sf
x}}_{\mathscr{P}}(\cdot,y)$ is downward closed $\mathscr{IC}^{u,{\sf
x}}_{\mathscr{P}}(x,\cdot)$ is upwards closed.

We now show downward closedness. For this, let
$\\{x_{\epsilon}\\}_{\epsilon\prec\alpha}$ be a descending chain of sets of
atoms that are subsets of $y$ and are post-fixpoints of $\mathscr{IC}^{{\sf
x},l}_{\mathscr{P}}(\cdot,y)$ for some $y\subseteq\mathscr{A}$, and let
$x=\bigcap\\{x_{\epsilon}\\}_{\epsilon\prec\alpha}$. We show that
$\mathscr{IC}^{{\sf x},l}_{\mathscr{P}}(x,y)\preceq^{S}_{L}\\{x\\}$. If the
chain is finite, this is trivial. Suppose therefore that
$\\{x_{\epsilon}\\}_{\epsilon\prec\alpha}$ is infinite.

${\sf x}={\sf MR}$

Consider some $C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P}$ s.t. for every
$i=1,\ldots,n$, $y(C_{i})={\sf T}$ and there is some $z^{\prime}\subseteq x$
s.t. $z^{\prime}(C_{i})$. As
$x=\bigcap\\{x_{\epsilon}\\}_{\epsilon\prec\alpha}$, also $z^{\prime}\subseteq
x_{\epsilon}$ for every $\epsilon\prec\alpha$. Thus, as $\mathscr{IC}^{{\sf
x},l}_{\mathscr{P}}(x_{\epsilon},y)\preceq^{S}_{L}\\{x_{\epsilon}\\}$, there
is some $z_{\epsilon}\subseteq x_{\epsilon}$ s.t.
$z_{\epsilon}\cap\mathsf{dom}(C)\in\mathsf{sat}(C)$ for every
$\epsilon<\alpha$. As $\\{x_{\epsilon}\\}_{\epsilon\prec\alpha}$ is a
$\subseteq$-descending chain, and $\mathsf{dom}(C)$ is finite, there is some
$\beta<\alpha$ s.t. for every $\epsilon,\epsilon^{\prime}<\beta$,
$\mathsf{dom}(C)\cap z_{\epsilon}=\mathsf{dom}(C)\cap
z_{\epsilon}^{\prime}\in\mathsf{sat}(C)$. But then also $\mathsf{dom}(C)\cap
z_{\epsilon}^{\prime}\subseteq x$, and thus $\mathscr{IC}^{{\sf
x},l}_{\mathscr{P}}(x,y)\preceq^{S}_{L}\\{x\\}$.

${\sf x}={\sf LPST}$

Consider some $C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P}$ s.t. for every
$i=1,\ldots,n$, and every $z\in[x,y]$, $z(C_{i})={\sf T}$. As $x\subseteq
x_{\epsilon}$ for every $\epsilon<\alpha$,
$C\in\mathscr{HD}_{\mathscr{P}}^{{\sf LPST},l}(x_{\epsilon},y)$ (for every
$\epsilon<\alpha$), and thus, as $\mathscr{IC}^{{\sf
x},l}_{\mathscr{P}}(x_{\epsilon},y)\preceq^{S}_{L}\\{x_{\epsilon}\\}$, there
is some $z_{\epsilon}\subseteq x_{\epsilon}$ s.t.
$z_{\epsilon}\cap\mathsf{dom}(C)\in\mathsf{sat}(C)$ for every
$\epsilon<\alpha$. The rest of the proof is similar to the previous item.

${\sf x}={\sf GZ}$

Consider some $C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P}$ s.t. for every
$i=1,\ldots,n$,
$x\cap\mathsf{dom}(C_{i})=y\cap\mathsf{dom}(C_{i})\in\mathsf{sat}(C_{i})$. As
$x\subseteq y$, for every $z\in[x,y]$,
$z\cap\mathsf{dom}(C_{i})=x\cap\mathsf{dom}(C_{i})\in\mathsf{sat}(C_{i})$. As
$\mathscr{IC}^{{\sf
x},l}_{\mathscr{P}}(x_{\epsilon},y)\preceq^{S}_{L}\\{x_{\epsilon}\\}$, there
is some $z_{\epsilon}\subseteq x_{\epsilon}$ s.t.
$z_{\epsilon}\cap\mathsf{dom}(C)\in\mathsf{sat}(C)$ for every
$\epsilon<\alpha$. The rest of the proof is similar to the previous item.

${\sf x}=\mathscr{U}$

We have to show that for every $z\in[x,y]$ there is some
$z^{\prime}\in\mathit{IC}_{\mathscr{P}}(z)$ s.t. $z^{\prime}\subseteq x$. As
$z\in[x_{\epsilon},y]$ for any $\epsilon<\alpha$, for every $\epsilon<\alpha$
there is some $z_{\epsilon}\subseteq x_{\epsilon}$ with
$z_{\epsilon}\in\mathit{IC}_{\mathscr{P}}(z)$. For every such $z_{\epsilon}$,
it holds that for every $C\in\mathit{HD}_{\mathscr{P}}(z)$,
$z_{\epsilon}\cap\mathsf{dom}(C)\in\mathsf{sat}(C)$. As $\mathsf{dom}(C)$ is
finite, there is some $\beta<\alpha$ s.t. for every
$\epsilon,\epsilon^{\prime}<\beta$,
$z_{\epsilon}\cap\mathsf{dom}(C)=z_{\epsilon^{\prime}}\cap\mathsf{dom}(C)\in\mathsf{sat}(C)$
for every $\epsilon<\alpha$. But then also
$z_{\epsilon}\cap\mathsf{dom}(C)\subseteq x$.

We now show upwards closedness of
$\mathscr{IC}^{\mathscr{U},u}_{\mathscr{P}}(x,\cdot)$ (for an arbitrary but
fixed $x\subseteq\mathscr{A}$). For this, let
$\\{y_{\epsilon}\\}_{\epsilon<\alpha}$ be an ascending chain of sets of atoms
that are supersets of $x$ and postfxipoints of
$\mathscr{IC}^{\mathscr{U},u}_{\mathscr{P}}(x,\cdot)$ and let
$y=\bigcup\\{y_{\epsilon}\\}_{\epsilon<\alpha}$. We show that
$\mathscr{IC}^{\mathscr{U},u}_{\mathscr{P}}(x,y)\preceq^{H}_{L}\\{y\\}$. If
the chain is finite, this is trivial. Suppose thus that
$\\{y_{\epsilon}\\}_{\epsilon<\alpha}$ is infinite. We show that there is some
$z\in[x,y]$ s.t. $y\in\mathit{IC}_{\mathscr{P}}(y)$. Indeed, consider some
$C\leftarrow C_{1},\ldots,C_{n}$ s.t. $\mathsf{dom}(C_{i})\cap
y\in\mathsf{sat}(C_{i})$ for every $i=1,\ldots,n$. As
$y=\bigcup\\{y_{\epsilon}\\}_{\epsilon<\alpha}$, and $\mathsf{dom}(C_{i})$ is
finite (for every $i=1,\ldots,n$), there is an $\epsilon<\alpha$ s.t. for
every $\epsilon^{\prime}\in[\epsilon,\alpha]$, $\mathsf{dom}(C_{i})\cap
y_{\epsilon^{\prime}}\in\mathsf{sat}(C_{i})$ (for $i=1,\ldots,n$). Thus, for
every $\epsilon^{\prime}\in[\epsilon,\alpha]$, $\mathsf{dom}(C)\cap
y_{\epsilon^{\prime}}\in\mathsf{sat}(C)$ (as
$\\{y_{\epsilon^{\prime}}\\}\preceq^{H}_{L}\mathscr{IC}_{\mathscr{P}}^{\mathscr{U},u}(x,y_{\epsilon^{\prime}})$).
Again in view of the finitude of $\mathsf{dom}(C)$, there is some
$\epsilon<\alpha$ s.t. for every $\epsilon^{\prime}\in[\epsilon,\alpha]$,
$\mathsf{dom}(C)\cap y_{\epsilon}=\mathsf{dom}(C)\cap y_{\epsilon^{\prime}}$,
which implies that $\mathsf{dom}(C)\cap y_{\epsilon}=\mathsf{dom}(C)\cap y$,
and, since $\mathsf{dom}(C)\cap y_{\epsilon}\in\mathsf{sat}(C)$, shows that
$\mathsf{dom}(C)\cap y\in\mathsf{sat}(C)$.

That $C^{c}(\mathscr{IC}^{{\sf x},u}_{\mathscr{P}})(x)\neq\emptyset$ follows
from Lemma 2 and the fact that $\mathscr{IC}_{\mathscr{P}}^{{\sf
x},u}(x,\cdot)$ is $\preceq^{H}_{L}$-monotonic (Proposition 3) for any
$x\subseteq\mathscr{A}$.

Upwards closedness is not guaranteed when allowing choice constructs with
infinite domains:

######  Example 11.

Consider the set of atoms $x=\\{a_{i}\mid i\in\mathbb{N}\\}$ and the choice
atom $C=(A,\\{A^{\prime}\subseteq A\mid A^{\prime}\mbox{ is infinite}\\})$. We
let $\mathscr{P}=\\{C\leftarrow\\}$. Let $x_{j}=A\setminus\\{a_{j}\mid j\leq
i\\}$ for any $i\in\mathbb{N}$. Then $\\{x_{j}\\}_{j<\infty}$ is a
$\subseteq$-descending chain of infinite sets. We see that for any $j<\infty$,
$\mathit{IC}_{\mathscr{P}}(x_{j})=\\{A^{\prime}\subseteq A\mid
A^{\prime}\mbox{ is infinite}\\}\preceq^{S}_{L}\\{x_{j}\\}$ as
$x_{j}\in\\{A^{\prime}\subseteq A\mid A^{\prime}\mbox{ is infinite}\\}$.
However, $\bigcap_{j<\infty}\\{x_{j}\\}=\emptyset$, whereas
$\mathit{IC}_{\mathscr{P}}(\emptyset)=\\{A^{\prime}\subseteq A\mid
A^{\prime}\mbox{ is infinite}\\}\preceq^{S}_{L}\\{x_{j}\\}$ and thus
$\mathit{IC}_{\mathscr{P}}(\emptyset)\not\preceq^{S}_{L}\\{\emptyset\\}$.

######  Remark 3.

Another property that stable fixpoints of both deterministic and non-
deterministic operators have in common is that they are $\leq_{t}$-minimal. As
is to be expected and as can be seen from the constructive stable fixpoint
$(\\{p,q\\},\\{p,q\\})$ in Example 9, constructive stable fixpoints are not
necessariy $\leq_{t}$-minimal, in contradistinction to minimiality-based
stable fixpoints (Proposition 14 by Heyninck et al. [2024]).

We now show a host of representation results: the ${\sf LPST}$-operator allows
to generalize the semantics of Liu et al [Liu et al., 2010] from two- to
three-valued. The ${\sf GZ}$-operator allows to adapt the semantics of Gelfond
and Zhang [2014] (defined for disjunctive programs) to choice programs, and
the semantics of Marek and Remmel [2004] from two- to three-valued.

Let a choice program $\mathscr{P}$ be given.

  1. 1.

$x$ is a stable model according to Liu et al. [2010] iff $(x,x)$ is a stable
fixpoint of $\mathscr{IC}^{\sf LPST}_{\mathscr{P}}$.

  2. 2.

$x$ is a stable model according to Marek and Remmel [2004] iff $(x,x)$ is a
stable fixpoint of $\mathscr{IC}^{\sf MR}_{\mathscr{P}}$.

  3. 3.

If $\mathscr{P}$ is a aggregate program then $x$ is a stable model according
to Gelfond and Zhang [2014] iff $x\in C^{c}(\mathscr{IC}^{{\sf
GZ},l}_{\mathscr{P}})(x)$.

For 1., we recall first some necessary preliminaries from [Liu et al., 2010]:

######  Definition 6.

Given some sets $x,y\subseteq\mathscr{A}$ and a choice atom $C$:

  * •

$y\triangleright^{\mathrm{spt}}_{x}C$ iff $y$ is an $x$-trigger for $C$.

  * •

$\mathscr{P}^{\triangleright^{\mathrm{spt}}_{x}}(y)=\\{C\leftarrow
C_{1},\ldots,C_{n}\mid y\triangleright^{\mathrm{spt}}_{x}C_{i}\mbox{ for
}i=1\ldots n\\}$,

  * •

$T^{nd,\triangleright^{\mathrm{spt}}_{x}}_{\mathscr{P}}(y)=\\{z\subseteq\bigcup_{C\in\mathscr{P}^{\triangleright^{\mathrm{spt}}_{x}}(y)}\mathsf{dom}(C)\mid
z\cap\mathsf{dom}(C)\in\mathsf{sat}(C)\>\forall
C\leftarrow\phi\in\mathscr{P}^{\triangleright^{\mathrm{spt}}_{x}}(y)\\}$,

  * •

A sequence $\emptyset=x_{1},\ldots,x_{n}=x$ is a self-justified
$\triangleright^{\mathrm{spt}}_{x}$-computation if $x_{i+1}\in
T^{nd,\triangleright^{\mathrm{spt}}_{x}}_{\mathscr{P}}(x_{i})$ for every
$i\geq 1$, and $x\in
T^{nd,\triangleright^{\mathrm{spt}}_{x}}_{\mathscr{P}}(x)$.

We first show that $(\dagger)$: a sequence $\emptyset=x_{1},\ldots,x_{n}=x$ is
well-founded relative to $\mathscr{IC}^{{\sf LPST},l}_{\mathscr{P}}(\cdot,x)$
iff it is a self-justified weak
$\triangleright^{\mathrm{spt}}_{x}$-computation. That this is the case is
easily seen by observing that $\mathscr{IC}_{\mathscr{P}}^{{\sf
LPST},l}(x^{\prime},x)=T^{nd,\triangleright^{\mathrm{spt}}_{x}}_{\mathscr{P}}(x^{\prime})$
for any $x^{\prime},x\subseteq\mathscr{A}$ (as $x^{\prime}$ is an $x$-trigger
for $C$ iff for every $z\in[x^{\prime},x]$, $z(C)={\sf T}$). We now show the
main claim. Suppose for the $\Rightarrow$-direction that $x$ is a stable model
according to [Liu et al., 2010]. With Proposition 12 from Liu et al. [2010],
there is a self-justified $\triangleright^{\mathrm{spt}}_{x}$-computation for
$x$. With $\dagger$, there is a well-founded sequence relative to
$\mathscr{IC}^{{\sf LPST},l}_{\mathscr{P}}(\cdot,x)$ for $x$. Thus, $x\in
S^{c}(\mathscr{IC}^{\sf LPST}_{\mathscr{P}})(x,x)$. Suppose now for the
$\Leftarrow$-direction that $x\in S^{c}(\mathscr{IC}^{\sf
LPST}_{\mathscr{P}})(x,x)$, i.e. there is a well-founded sequence relative to
$\mathscr{IC}^{{\sf LPST},l}_{\mathscr{P}}(\cdot,x)$ for $x$. With $\dagger$,
this sequence is a self-justified weak
$\triangleright^{\mathrm{spt}}_{x}$-computation. With Proposition 11 by Liu et
al. [2010], this is a founded computation. By Definition 5 by Liu et al.
[2010], this means $x$ is an answer set according to Liu et al. [2010].

2\. We first recall the relevant definitions [Marek and Remmel, 2004] (adapted
to our notation): Given a choice atom $C=(\mathsf{dom},\mathsf{sat})$, and a
set of atoms $x$, $\overline{C}_{y}=\\{z\subseteq y\mid\exists
z^{\prime}\in\mathsf{sat}(C)\mbox{ and }z\subseteq z^{\prime}\\}$. A perhaps
helpful alternative description is:
$\overline{C}_{y}=\bigcup_{z\in\mathsf{sat}(C)}^{z\subseteq y}[z,y]$. Given a
choice program $\mathscr{P}$ and a set of atoms $x$,
$\mathrm{NSS}(\mathscr{P},y)$ is obtained by:

  1. 1.

Removing any $C\leftarrow C_{1},\ldots,C_{n}$ s.t. $y(C_{i})={\sf F}$ for some
$i=1,\ldots,n$,

  2. 2.

For every rule $r=C\leftarrow C_{1},\ldots,C_{n}$ not removed in the first
step, replace $r$ by
$\\{\alpha\leftarrow\overline{C_{1}}_{x},\ldots,\overline{C_{n}}_{x}\mid\alpha\in\mathsf{dom}(C)\\}$.

Marek and Remmel [2004] show that for any choice program $\mathscr{P}$,
$\mathrm{NSS}(\mathscr{P},y)$ has a unique least model obtained by iteratively
applying the one-step provability operator
$T_{\mathrm{NSS}(\mathscr{P},y)}(x)=\\{\alpha\mid\alpha\leftarrow\overline{C_{1}}_{x},\ldots,\overline{C_{n}}_{x}\in\mathrm{NSS}(\mathscr{P},y)\mbox{
and }\forall i=1\ldots
n:x\cap\mathsf{dom}(\overline{C_{i}}_{x})\in\mathsf{sat}(\overline{C_{i}}_{x})\\}$.
Call this least model $N_{\mathscr{P},y}$. Then $y$ is a ${\sf MR}$-stable
model of $\mathscr{P}$ iff $y$ is a model of $\mathscr{P}$ and
$y=N_{\mathscr{P},y}$. We show that ($\dagger$):
$T_{\mathrm{NSS}(\mathscr{P},x)}(z)\in\mathscr{IC}^{{\sf
MR},l}_{\mathscr{P}}(z,x)$ for any $z\subseteq x$. For this, consider some
$C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P}$. We distinguish two cases:

  1. 1.

$x(C_{i})={\sf F}$ for some $i=1,\ldots,n$. Then $C\not\in\mathscr{HD}^{{\sf
MR},l}_{\mathscr{P}}(z,x)$ for any $z\subseteq x$ and thus we are done.

  2. 2.

$x(C_{i})={\sf T}$ for every $i=1,\ldots,n$. We distinguish two cases:

    1. (a)

Suppose first that there is no $z\subseteq x$ s.t. $z(C_{i})={\sf T}$ for some
$i=1,\ldots,n$. Then $C\not\in\mathscr{HD}^{{\sf MR},l}_{\mathscr{P}}(z,x)$
and thus we are done.

    2. (b)

Suppose now that there is a $z^{\prime}\subseteq z$ s.t.
$z^{\prime}(C_{i})={\sf T}$ for every $i=1,\ldots,n$. Then
$C\in\mathscr{HD}^{{\sf MR},l}_{\mathscr{P}}(z,x)$. Also, for every
$i=1,\ldots,n$, $z\in\mathsf{sat}(\overline{C_{i}}_{x})$ and, as
$\alpha\leftarrow\overline{C_{1}}_{x},\ldots,\overline{C_{n}}_{x}\in\mathrm{NSS}(\mathscr{P},x)$
for every $\alpha\in\mathsf{dom}(C)\cap x$, $\mathsf{dom}(C)\cap x\subseteq
T_{\mathrm{NSS}(\mathscr{P},x)}(z)$. As $x$ is a model of $\mathscr{P}$ and
$x(C_{i})={\sf T}$ for every $i=1,\ldots,n$,
$x\cap\mathsf{dom}(C)\in\mathsf{sat}(C)$.

We now show that $x\in S^{c}(\mathscr{IC}^{{\sf MR},l}_{\mathscr{P}})(x,x)$
iff $x$ is a ${\sf MR}$-stable model of $\mathscr{P}$. For the
$\Rightarrow$-direction, observe first that as $x$ is a fixpoint of
$\mathscr{IC}^{{\sf MR},l}_{\mathscr{P}}$, it is, with Proposition 4, a model
of $\mathscr{P}$. With $\dagger$,
$T_{\mathrm{NSS}(\mathscr{P},x)}(z)\in\mathscr{IC}^{{\sf
MR},l}_{\mathscr{P}}(z,x)$ for any $z\subseteq x$, which implies (with a
simple induction on the well-founded sequence $\emptyset,\ldots,x$) that
$x=N_{\mathscr{P},x}$. For the $\Leftarrow$-direction, suppose that $x$ is an
${\sf MR}$-stable model. Notice that as $x=N_{\mathscr{P},x}$, there is a
sequence $\emptyset=x_{0},x_{1},\ldots,x_{n}=x$ s.t.
$x_{i+1}=T_{\mathrm{NSS}(\mathscr{P},x)}(x_{i})$ for any $i=0,\ldots,n$. With
$\dagger$, this is a well-founded sequence relative to
$\mathscr{IC}_{\mathscr{P}}^{{\sf MR},l}(\cdot,x)$.

3\. follows from the fact that for choice programs with only atoms in the
head, $\mathscr{IC}^{{\sf GZ},l}$ coincides with $\mathscr{I}^{\sf
GZ}_{\mathscr{P},x}(y)$, used by Alviano et al. [2023] to characterize the
semantics of Gelfond and Zhang [2014]. Furthermore, for normal logic programs,
all operators besides the ultimate coincide, and the stable fixpoints
respectively partial stable fixpoint coincide with the stable respectively
partial stable models (and similarly for the well-founded semantics) (recall
Remark 1). Thus, the semantics studied in this paper do not only generalize
existing semantics for choice or aggregate programs, but also the well-known
semantics for normal logic programs.

##  6 Groundedness

We introduce several postulates to facilitate a comparison between semantics
for choice programs (thus solving an open question in the literature Alviano
et al. [2023]) formalizing in different ways the idea of _groundedness_.
Furthermore, we show that for every notion of groundedness, there exist
examples which have been argued in the literature to be counter-intuitive.

Intuitively, the idea behind groundedness is that models should be derivable
_from the ground up_ , i.e. they should be supported by non-cyclic arguments.
For choice programs, what constitutes a cycle becomes less clear:

######  Example 12 ([Liu et al., 2010]).

Consider the program $\mathscr{P}=\\{\\{p,q\\}=2\leftarrow\\{p,q\\}\neq 1\\}$.
There are two candidates for stable models: $\emptyset$ and $\\{p,q\\}$ (as
the only satisfier of the head of the only rule is $\\{p,q\\}$), which we
discuss:
(1) If we choose $\emptyset$, then we see that the only rule in the program is
applicable but not applied.
(2) If we choose $\\{p,q\\}$, we could justify this intuitively by the
sequence $\emptyset,\\{p,q\\}$: at the first step, $\emptyset$ makes
$\\{p;q\\}\neq 1$ true and thus we derive $\\{p,q\\}$. At the second step,
however, we can only justify our choice by a self-supporting justification:
$\\{p,q\\}$ is true since it is derivable using the head of the rule
$\\{p,q\\}=2\leftarrow\\{p;q\\}\neq 1$ and since $\\{p,q\\}(\\{p;q\\}\neq
1)={\sf T}$.

We observe that $\\{p,q\\}$ is stable fixpoint for the $\mathscr{U}$\- and
${\sf MR}$-operator, but not for the ${\sf LPST}$\- and ${\sf GZ}$-operators.

The benefit of our operator-based framework is that we do not have to choose
for a single “best” semantics: the choices outlined above will be obtainable
by using different operators. We now carry forward our study of self-support
on a more general level by introducing three postulates of decreasing
strength. The first notion (inspired by Gelfond and Zhang [2014]) requires
that we can find a stratification of the program (i.e. an assignment $\kappa$
of natural numbers representing levels) s.t. the entire domain of the head of
a rule is strictly higher stratified then the domain of the choice constructs
in the body.

######  Definition 7.

A set $x$ is _d(omain)-grounded_ (for $\mathscr{P}$) if there is some
$\kappa:x\rightarrow\mathbb{N}$ s.t. every $a\in x$ there is some
$r=C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P}$ s.t. $a\in\mathsf{dom}(C)$,
$\kappa(a)>\max\\{\kappa(b)\mid b\in\bigcup_{i=1}^{n}\mathsf{dom}(C_{i})\\}$.

As already observed by Alviano et al. [2023], this requirement might be overly
strong:

######  Example 13.

Consider $\mathscr{P}=\\{b\leftarrow 1\\{a,b\\};a\leftarrow\\}$. Then one
might expect $\\{a,b\\}$ to be a good candidate for a stable model. Indeed,
$a$ is a fact and allows to support $b$. However, $\\{a,b\\}$ is not
d-grounded, as there is no $\kappa:\\{a,b\\}\rightarrow\mathbb{N}$ s.t.
$\kappa(b)>\max\\{\kappa(a),\kappa(b)\\}$.

The following weaker notion (inspired in name and idea by Liu et al. [2010])
requires that at some point in a sequence, there is support for the body of a
rule, and this support persists in every following step:

######  Definition 8.

(1) A set $x$ is an _$y$ -trigger_ for $C\leftarrow C_{1},\ldots,C_{n}$ if for
every $z\in[x,y]$, $z(C_{i})={\sf T}$ for every $i=1,\ldots,n$. (2) A set $x$
is _s(trongly)-grounded_ (for $\mathscr{P}$) if there is some
$\kappa:x\rightarrow\mathbb{N}$ s.t. every $a\in x$, there is some
$r=C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P}$ s.t. $a\in\mathsf{dom}(C)$
and there is an $x$-trigger $z$ for $r$ s.t. $\kappa(a)>max\\{\kappa(b)\mid
b\in z\\}$.

Intuitively, $x$ is s-grounded if for every atom $a\in x$, we can find a rule
that that has an $x$-trigger in a strictly lower level.

D-grounded sets are s-grounded, but not vice-versa:

######  Example 14.

Consider $\mathscr{P}$ as in Example 13. We see that $\\{a,b\\}$ is strongly
grounded. Indeed, if we take $\kappa(a)=0$ and $\kappa(b)=1$, we see that
$b\leftarrow 1\\{a,b\\}$ has a $\kappa$-lower $\\{a,b\\}$-trigger in $\\{a\\}$
as $\\{a\\}(1\\{a,b\\})=\\{a,b\\}(1\\{a,b\\})={\sf T}$.

The following example, first introduced by Alviano and Faber [2019], shows
that in some circumstances, s-groundedness might be overly strong:

######  Example 15.

Consider $\mathscr{P}=\\{a\leftarrow\\{a,b\\}\neq 1;b\leftarrow\\{a,b\\}\neq
1\\}$. One might expect the set $\\{a,b\\}$ to be acceptable. Suppose it is
s-grounded. Then there is an $\\{a,b\\}$-trigger $y$ for $a$ s.t.
$y\subseteq\\{b\\}$. This is impossible as $\\{b\\}\in[\emptyset,\\{a,b\\}]$
and $\\{b\\}\in[\\{b\\},\\{a,b\\}]$ and $\\{b\\}\cap\mathsf{dom}(\\{a,b\\}\neq
1)\not\in\mathsf{sat}(\\{a,b\\})$. Thus, $\\{a,b\\}$ cannot be s-grounded.

We thus introduce an even weaker notion of groundedness which we call
_antecedent groundedness_ , which requires that for every accepted atom, we
can find a rule that is activated by a lower $\kappa$-level:

######  Definition 9.

A set $x$ is _a(ntecedent)-grounded_ if there is some
$\kappa:x\rightarrow\mathbb{N}$ s.t. every $a\in x$, there is some
$r=C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P}$ s.t. $a\in\mathsf{dom}(C)$
and for every $i=1,\ldots,n$ there is some
$z\subseteq\\{b\mid\kappa(b)<\kappa(a)\\}$ s.t. $z(C_{i})={\sf T}$ .

S-grounded sets are a-grounded, but not vice-versa:

######  Example 16.

Consider again $\mathscr{P}$ from Example 12. We first observe that
$\\{p,q\\}$ is antecedent grounded as $\emptyset(\\{p,q\\}\neq 1)={\sf T}$ and
thus we have found our antecedent justification for $\\{p,q\\}$. However,
$\emptyset$ is _not_ a $\\{p,q\\}$-trigger, as
$\\{p\\}\in[\emptyset,\\{p,q\\}]$ and $\\{p\\}(\\{p,q\\}\neq 1)={\sf F}$.
Likewise, it can be seen that $\\{a,b\\}$ in Example 15 is a-grounded.

The reader might think that a-groundedness is the most suitable notion of
groundedness, as it avoids the behavior (deemed problematic by Alviano and
Faber [2019] in Example 15). However, Liu et al. [2010] argued that, for
$\mathscr{P}$ from Example 12, $\\{p,q\\}$ is not a feasible candidate for an
answer set. Altogether, we see that for every notion of groundedness, one can
find examples deemed as counter-intuitive in the literature.

Notice that all notions of groundedness generalize a well-known notion of
groundedness proposed for normal logic programs [Erdem and Lifschitz, 2003]:
Let $\mathscr{P}$ a normal logic program $\mathscr{P}$. Then $x$ is a-grounded
$\mathscr{P}$ then $x$ is grounded according to Erdem and Lifschitz [2003],
namely: there is a ranking $\kappa:x\rightarrow\mathbb{N}$ s.t. for every
$a\in x$, there is some $a\leftarrow a_{1},\ldots,a_{n},\lnot
b_{1},\ldots,\lnot b_{m}\in\mathscr{P}$ s.t. for every $i=1,\ldots,n$,
$\kappa(a)>\kappa(a_{i})$. Suppose that $x$ is a-grounded for $\mathscr{P}$,
i.e. there is some $\kappa:x\rightarrow\mathbb{N}$ s.t. for every $a\in x$,
there is some
$r=a\leftarrow\bigwedge_{i=1}^{n}a_{i}\land\bigwedge_{i=1}^{m}\lnot b_{i}$
s.t. for every $i=1,\ldots,n$, there is some
$z\subseteq\\{b\mid\kappa(b)<\kappa(a)\\}$ with $z(a_{i})={\sf T}$. As
$z(a_{i})={\sf T}$ iff $a_{i}\in z$, this means that $\kappa(a)>\kappa(a_{i})$
for every $i=1,\ldots,n$.

######  Remark 4.

Notice that the other direction of Proposition 6 does not necessarily hold:
take e.g. $\mathscr{P}=\\{b\leftarrow\lnot c.,c\leftarrow\lnot b.\\}$. Then
$\\{b,c\\}$ is grounded according to Erdem and Lifschitz [2003] (trivially, as
there are no rules with positive bodies) but not a-grounded.

The $\mathscr{U}$-operator does not satisfy any notion of groundedness,
whereas all other operators give rise to a-grounded stable models, but only
the ${\sf LPST}$-operator and ${\sf GZ}$-operator give rise to s-grounded
stable models and only the ${\sf GZ}$-operator gives rise to d-grounded stable
models: Let $\mathscr{P}$ be a choice program and $\dagger\in\\{{\sf GZ},{\sf
LPST},{\sf MR}\\}$. Then if $(x,y)\in
S^{c}(\mathscr{IC}_{\mathscr{P}}^{\dagger})(x,y)$:

  1. 1.

$x$ and $y$ are a-grounded (for $\mathscr{P}$), and

  2. 2.

$x$ is s-grounded (for $\mathscr{P}$) if $\dagger\in\\{{\sf GZ},{\sf
LPST}\\}$.

  3. 3.

$x$ and $y$ are d-grounded (for $\mathscr{P}$) if $\dagger={\sf GZ}$.

There are programs $\mathscr{P}$ s.t. $(x,y)\in
S^{c}(\mathscr{IC}_{\mathscr{P}}^{\mathscr{U}})(x,y)$ yet $x$ and $y$ are not
antecedent grounded. Let $\mathscr{P}$ be a choice program and
$\dagger\in\\{{\sf GZ},{\sf LPST},{\sf MR}\\}$.

Ad 1.: We first consider $C^{c}(\mathscr{IC}^{l,{\sf MR}}_{\mathscr{P}})$.
Suppose that $x\in C^{c}(\mathscr{IC}^{l,{\sf MR}}_{\mathscr{P}})(y)$, i.e.
there is a well-founded sequence $\emptyset=x_{0},\ldots,x_{n},x$ relative to
$\mathscr{IC}^{{\sf MR},l}_{\mathscr{P}}(\cdot,y)$. We let
$\kappa(a)=\min\\{i\mid a\in x_{i}\\}$. Consider some $a\in x$ and let $i$ be
the ordinal s.t. $a\in x_{i+1}\setminus x_{i}$. Then there is some
$C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P}$ s.t. $a\in\mathsf{dom}(C)\cap
x_{i+1}$ and for every $j=1\ldots n$, $y(C_{j})={\sf T}$ and there is some
$w\subseteq x_{i}$ s.t. $w(C_{j})={\sf T}$. But then $w(C_{j})={\sf T}$ and
$\kappa(b)\leq i<\kappa(a)=i+1$.
We now consider $C^{c}(\mathscr{IC}^{{\sf
GZ},u}_{\mathscr{P}})=C^{c}(\mathscr{IC}^{{\sf
LPST},u}_{\mathscr{P}})=C^{c}(\mathscr{IC}^{\mathscr{U},u}_{\mathscr{P}})$.
Suppose that $y\in C^{c}(\mathscr{IC}^{u,{\sf MR}}_{\mathscr{P}})(x)$, i.e.
there is a well-founded sequence $\emptyset=y_{0},\ldots,y_{n},y$ relative to
$\mathscr{IC}^{\mathscr{U},u}_{\mathscr{P}}(x,\cdot)$. We let
$\kappa(a)=\min\\{i\mid a\in y_{i}\\}$. Consider some $a\in y$ and let $i$ be
the ordinal s.t. $a\in y_{i+1}\setminus y_{i}$. Then there is some
$z\in[x,y_{i}]$ and some $C\leftarrow C_{1},\ldots,C_{n}$ s.t. $z(C_{j})={\sf
T}$ for every $j=1,\ldots,n$ and $a\in\mathsf{dom}(C)$. As $z\subseteq y_{i}$,
$z\subseteq\\{a\in\mathscr{A}\mid\kappa(z)\leq i\\}$, whereas $\kappa(a)=i+1$.
Thus, we have found our justification for $a$.

Ad 2.: Suppose that $x$ is a constructive stable fixpoint of
$\mathscr{IC}^{\sf LPST}_{\mathscr{P}}$, i.e. there is a well-founded sequence
relative to $\mathscr{IC}^{{\sf LPST},l}_{\mathscr{P}}(\cdot,y)$
$\emptyset=x_{0},\ldots,x_{n},x$. We let $\kappa(a)=\min\\{i\mid a\in
x_{i}\\}$. Consider some $a\in x$ and let $i$ be the ordinal s.t. $a\in
x_{i+1}\setminus x_{i}$. Then there is some $r=C\leftarrow
C_{1},\ldots,C_{n}\in\mathscr{P}$ s.t. $a\in\mathsf{dom}(C)\cap x_{i+1}$ and
for every $z\in[x_{i},y]$ and every $j=1,\ldots,n$, $z(C_{j})={\sf T}$. But
then clearly $x_{i}$ is an $y$-trigger for $r$ and for every $b\in x_{i}$,
$\kappa(b)\leq i<\kappa(a)=i+1$.

Ad 3.: suppose that $x$ is a constructive stable fixpoint of
$\mathscr{IC}^{\sf GZ}_{\mathscr{P}}$, i.e. there is a well-founded sequence
relative to $\mathscr{IC}^{{\sf GZ},l}_{\mathscr{P}}(\cdot,y)$
$\emptyset=x_{0},\ldots,x_{n},x$. We let $\kappa(a)=\min\\{i\mid a\in
x_{i}\\}$. Consider now some $a\in x$ and let $i$ be the ordinal s.t. $a\in
x_{i+1}\setminus x_{i}$. This means that $a\in\mathsf{dom}(C)$ for some
$C\in\mathscr{HD}^{{\sf GZ},l}_{\mathscr{P}}(x_{i},x)$. Suppose towards a
contradiction that for every $C\leftarrow C_{1},\ldots,C_{n}\in\mathscr{P}$
with $a\in\mathsf{dom}(C)$, there is some $i=1,\ldots,n$ s.t. for some
$b\in\mathsf{dom}(C_{i})$, $\kappa(b)\geq\kappa(a)$. For any such $b$,
$b\not\in x_{i}$, which implies that $b\not\in\mathsf{dom}(C_{i})\cap x_{i}$
yet $b\in\mathsf{dom}(C_{i})\cap x$, i.e. $\mathsf{dom}(C_{i})\cap
x_{i}\neq\mathsf{dom}(C_{i})\cap x$, contradiction to $C\in\mathscr{HD}^{{\sf
GZ},l}_{\mathscr{P}}(x_{i},x)$.

Regarding the ultimate operator, consider
$\mathscr{P}=\\{\\{p,q\\}=2\leftarrow\\{p,q\\}=2\\}$. Then we see that
$\mathscr{IC}^{\mathscr{U}}_{\mathscr{P}}(\emptyset,\\{p,q\\})=(\bigcup_{z\subseteq\\{p,q\\}}\mathit{IC}_{\mathscr{P}}(z),\bigcup_{z\subseteq\\{p,q\\}}\mathit{IC}_{\mathscr{P}}(z))=(\\{\emptyset,\\{p,q\\}\\},\\{\emptyset,\\{p,q\\}\\})$.
Thus, the sequence $\emptyset,\\{p,q\\}$ is well-founded relative to
$\mathscr{IC}^{\mathscr{U},l}_{\mathscr{P}}(\cdot,\\{p,q\\})$. However, it is
clearly not antecedent grounded as we cannot justify $\\{p,q\\}$ in view of
$\emptyset$.

Summing up, we see that the different semantics satisfy different notions of
groundedness, and that no notion of groundedness is uncontested. It seems that
it depends on the application at hand which notion of groundedness is the most
suitable. The results of this section are summarized in Table 3.

Operator | d-ground. | s-ground. | a-ground.
---|---|---|---
${\sf GZ}$ | $\vee$ | $\vee$ | $\vee$
${\sf LPST}$ | $\times$ | $\vee$ | $\vee$
${\sf MR}$ | $\times$ | $\times$ | $\vee$
$\mathscr{U}$ | $\times$ | $\times$ | $\times$
Example of violation | Ex. 13 | Ex. 15 | Ex. 12
Counter-intuitive according to | [Alviano et al., 2023] | [Alviano and Faber, 2019] | [Liu et al., 2010]
Table 3: Results on Postulates

##  7 Disjunctions are Choice Constructs

Our study allows us to give a principled account of the relation between
stable semantics for disjunctive logic programs (DLPs) and choice programs.
Indeed, in this section, we show that for DLPs [Heyninck et al., 2024;
Heyninck and Bogaerts, 2023] are a special case of the operator for choice
programs. This means that all semantics obtained on the basis of these
operators coincide, thus explaining the difference between semantics for
stable models of disjunctive logic programs and choice logic programs in terms
of the choice of stable operator (minimality-based versus constructive). In
the rest of this section, we show this claim in more detail, first providing
the necessary background on DLPs and then showing DLP-operators are a special
case of the operators studied in this paper.

#### Preliminaries on disjunctive logic programs

We first recall some necessary preliminaries on disjunctive logic programming.
For simplicity, we restrict attention to disjunctive logic programs whose
bodies consist solely of literals, leaving the generalization of these results
to stronger languages for future work.

In what follows we consider a propositional444We restrict ourselves to the
propositional case. language ${\mathfrak{L}}$, whose atomic formulas are
denoted by $p,q,r$ (possibly indexed), and that contains the propositional
constants ${\sf T}$ (representing truth), ${\sf F}$ (falsity), ${\sf U}$
(unknown), and ${\sf C}$ (contradictory information). The connectives in
${\mathfrak{L}}$ include negation $\neg$, conjunction $\wedge$ and disjunction
$\vee$. Formulas are denoted by $\phi$, $\psi$, $\delta$ (again, possibly
indexed). A (propositional) disjunctively normal logic program $\mathscr{P}$
in ${\mathfrak{L}}$ (a dlp in short) is a finite set of rules of the form
$\bigvee_{i=1}^{n}p_{i}~{}\leftarrow~{}\bigwedge_{i=1}^{n}a_{i}\land\bigwedge_{i=1}^{m}\lnot
b_{i}$, where the head $\bigvee_{i=1}^{n}p_{i}$ is a non-empty disjunction of
atoms, and the body $\psi$ is a formula in ${\mathfrak{L}}$. We furthermore
recall that a formula of the form
$\bigwedge_{i=1}^{n}a_{i}\land\bigwedge_{i=1}^{m}\lnot b_{i}$ can be evaluated
over the bilattice FOUR relative to $(x,y)$ by assuming the involution $-$
defined by $-{\sf T}={\sf F}$, $-{\sf F}={\sf T}$, $-{\sf U}={\sf U}$ and
$-{\sf C}={\sf C}$, and by defining truth assignments to complex formulas
recursively as follows:

  * •

$(x,y)({p})=\begin{cases}{\sf T}&\text{ if }{p}\in x\text{ and }{p}\in y,\\\
{\sf U}&\text{ if }{p}\not\in x\text{ and }{p}\in y,\\\ {\sf F}&\text{ if
}{p}\not\in x\text{ and }{p}\not\in y,\\\ {\sf C}&\text{ if }{p}\in x\text{
and }{p}\not\in y.\end{cases}$

  * •

$(x,y)(\lnot\phi)=-(x,y)(\phi)$,

  * •

$(x,y)(\psi\land\phi)=\sqcap_{\leq_{t}}\\{(x,y)(\phi),(x,y)(\psi)\\}$,

  * •

$(x,y)(\psi\lor\phi)=\sqcup_{\leq_{t}}\\{(x,y)(\phi),(x,y)(\psi)\\}$.

Notice that this is equivalent to the evaluations introduced in Section 4.

We recall the following ndao $\mathscr{IC}^{d}_{\mathscr{P}}$ introduced by
[Heyninck et al., 2024] and defined as follows (given a dlp $\mathscr{P}$ and
an interpretation $(x,y)$):

  * •

$\mathscr{HD}^{d,l}_{\mathscr{P}}(x,y)=\\{\Delta\mid\bigvee\\!\Delta\leftarrow\phi\in\mathscr{P},(x,y)(\phi)\geq_{t}{\sf
C}\\}$,

  * •

$\mathscr{HD}^{d,u}_{\mathscr{P}}(x,y)=\\{\Delta\mid\bigvee\\!\Delta\leftarrow\phi\in\mathscr{P},(x,y)(\phi)\geq_{t}{\sf
U}\\}$,

  * •

$\mathscr{IC}^{d,\dagger}_{\mathscr{P}}(x,y)=\\{x_{1}\subseteq\bigcup\mathscr{HD}^{d,\dagger}_{\mathscr{P}}(x,y)\mid\forall\Delta\in\mathscr{HD}^{d,\dagger}_{\mathscr{P}}(x,y),\
x_{1}\cap\Delta\neq\emptyset\\}$ (for $\dagger\in\\{l,u\\}$),

  * •

$\mathscr{IC}^{d}_{\mathscr{P}}(x,y)=(\mathscr{IC}^{d,l}_{\mathscr{P}}(x,y),\mathscr{IC}^{d,u}_{\mathscr{P}}(x,y))$.

The operator $\mathscr{IC}^{d}_{\mathscr{P}}$ faithfully represents the
semantics of dlps: In general, total stable fixpoints of $\mathscr{P}$
correspond to stable models of $\mathscr{P}$ [Gelfond and Lifschitz, 1991],
and weakly supported models of $\mathscr{P}$ [Brass and Dix, 1995] correspond
to fixpoints of $\mathscr{IC}^{d}_{\mathscr{P}}$ [Heyninck et al., 2024].

#### Disjunctions as Choice Constructs

We now show how the operator $\mathscr{IC}^{d}_{\mathscr{P}}$ can be seen as a
special case of the operators for choice constructs. In more detail, for a DLP
$\mathscr{P}$, we define ${\tt
D2C}(\mathscr{P})=\\{1\Delta\leftarrow\phi\mid\bigvee\Delta\leftarrow\phi\in\mathscr{P}\\}$.
E.g. ${\tt D2C}(\\{p\lor q\leftarrow\\})=\\{1\\{p,q\\}\leftarrow\\}$. In other
words, we replace every disjunction by the choice atom that requires at least
one element of $\Delta$ is true. We will show here that the operator defined
for disjunctive logic programs [Heyninck et al., 2024] then coincides with the
operator $\mathscr{IC}^{\sf x}_{{\tt D2C}(\mathscr{P})}$ (for ${\sf x}={\sf
MR},{\sf LPST}$). This implies that all AFT-based semantics coincide for DLPs
and their conversion into choice rules. We can now point in a very exact way
to the difference between DLPs and choice programs: it lies not in how the
constructs of disjunction and choice atoms are treated (i.e. when they should
be made true or false), but rather in how the stable semantics is defined: for
disjunctions, typically (e.g. in the most popular solvers [Gebser et al.,
2016; Eiter et al., 2012]), a minimality-based stable operator is used,
whereas for choice constructs, the c-stable operator is more apt. Thus,
disjunctive and choice programs use the same (approximation) operators, but
differ in how the corresponding stable operator is constructed.

We now show that the operator $\mathscr{IC}^{d}_{\mathscr{P}}$ is a special
case of the ${\sf MR}$\- and ${\sf LPST}$-operators from this paper, when
applied to the choice program ${\tt D2C}(\mathscr{P})$. For any disjunctive
normal logic program $\mathscr{P}$,
$\mathscr{IC}_{\mathscr{P}}=\mathscr{IC}^{\sf MR}_{{\tt
D2C}(\mathscr{P})}=\mathscr{IC}^{\sf LPST}_{{\tt D2C}(\mathscr{P})}$. We first
notice that, as ${\tt D2C}(\mathscr{P})$ does not change the bodies of rules
in $\mathscr{P}$, if $\mathscr{P}$ is a disjunctively normal logic program,
${\tt D2C}(\mathscr{P})$ is a normal choice program. This means that, with
Proposition 3, $\mathscr{IC}^{\sf MR}_{{\tt
D2C}(\mathscr{P})}=\mathscr{IC}^{\sf LPST}_{{\tt D2C}(\mathscr{P})}$.

Furthermore, it can be straightforwardly shown that for any disjunctively
normal logic program,
$\mathscr{HD}^{d,\dagger}_{\mathscr{P}}(x,y)=\mathscr{HD}^{{\sf
MR},\dagger}_{\mathscr{P}}(x,y)$. Finally, it suffices to observe that
$z\cap\mathsf{dom}(1\leq\Delta)\in\mathsf{sat}(1\leq\Delta)$ iff $\Delta\cap
z\neq\emptyset$ for any $z\subseteq\mathscr{A}$, which means that
$z\in\mathscr{IC}_{\mathscr{P}}(x,y)$ iff $z\in\mathscr{IC}^{\sf MR}_{{\tt
D2C}(\mathscr{P})}(x,y)$ for any $x,y\subseteq\mathscr{A}$. From this, we
immediately obtain that all the major semantics for disjunctive logic
programming are special cases of the semantics introduced in this paper.
Namely, weakly supported models of $\mathscr{P}$ coincide with fixpoints of
$\mathscr{IC}^{\sf MR}_{{\tt D2C}(\mathscr{P})}$ whereas minimality-based
stable fixpoints of $\mathscr{P}$ coincide with stable models of
$\mathscr{P}$. Since, the c-stable semantics does not enforce minimality, it
will in general _not_ correspond to the stable models semantics:

######  Example 17.

Let $\mathscr{P}=\\{p\lor q\leftarrow\\}$. Then $(\\{p,q\\},\\{p,q\\})$ is a
c-stable fixpoint of $\mathscr{IC}^{\sf MR}_{{\tt D2C}(\mathscr{P})}$ but it
is not a stable model of $\mathscr{P}$ according to Gelfond and Lifschitz
[1991].

This also gives an answer to the question of how to combine disjunctions and
choice constructs in logic programs: a choice as to which stable semantics are
used has to be made: either preserve the minimality of answer sets as in DLPs
and loses some reasonable models, or one gives up the minimality requirement
by 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. On the other hand, we can now also use
minimality-based stable semantics on more complicated choice construct than
simple disjunctions.

##  8 Related Work

To the best of our knowledge, this is the first application of AFT to the
semantics of choice programs. We have shown how major semantics for choice
programs [Marek and Remmel, 2004; Liu et al., 2010] can be characterized in
our framework. Other well-known semantics for (disjunctive) aggregate programs
are those by Faber et al. [2004]; Alviano and Faber [2019]; Ferraris [2011],
which are the ones used in the solvers DLV respectively clingo [Ferraris,
2011; Alviano et al., 2017].

Another semantics, the FLP-semantics [Faber et al., 2004], were originally not
defined for programs with choice constructs in the head, but were generalized
to allow choice constructs in the head by Eiter and Geibinger [2023].
Nevertheless, these semantics only allow for two-valued stable models, and
were shown to differ from the semantics by [Gelfond and Zhang, 2014], [Liu et
al., 2010] and [Marek and Remmel, 2004] already for aggregate programs
[Alviano et al., 2023], which means, in view of Proposition 5, that the stable
semantics induced by the ${\sf LPST}$-, ${\sf MR}$\- and ${\sf GZ}$-operators
also differ from the FLP-semantics. This comparison also holds for the
semantics by Ferraris [2011] as the latter coincide with the FLP-semantics for
aggregates with positive atoms [Alviano et al., 2023].

Another line of work that is relevant for this paper is the application of AFT
to logic programs with aggregates. Pelov et al. [2007] introduce several
approximation operators for aggregate programs, whereas Pelov et al. [2007]
introduces operator-based semantics for disjunctive aggregate programs. These
semantics were generalized by Heyninck and Bogaerts [2023] in the framework of
non-deterministic AFT. Generalizing the operator by Pelov et al. [2007] to
choice programs is left for future work. An overview of semantics that are
(non-)representable in the deterministic AFT-framework is given by Vanbesien
et al. [2022]. This work severed as an important foundation of our paper, as
the operators $\mathscr{IC}^{\sf GZ}_{\cal P}$ and $\mathscr{IC}^{\sf
MR}_{\cal P}$ are generalizations of the operator-based characterisations by
Vanbesien et al. [2022] of the corresponding semantics.

##  9 Conclusion

The main contributions of this paper are the definition of several ndaos for
choice programs, the definition of the constructive stable operator, the
characterisation of several existing semantics for various dialects of logic
and choice programs and the introduction and study of postulates for choice
programs. We provide a principled view of choice programs versus disjunctive
programs.

This paper is subject to one restriction: we assume
$\mathscr{IC}^{c}_{\mathscr{P}}(x,y)\neq\emptyset$ for every interpretation
$(x,y)$. In future work, we will generalize our results beyond this
assumption. We also plan to study the complexity of the resulting semantics,
device implementations and study other AFT-based semantics, such as the
Kripke-Kleene and well-founded states and semi-equilibrium semantics [Heyninck
and Bogaerts, 2023; Heyninck et al., 2024] and study other operators, e.g.
inspired by Pelov et al. [2007].

#### Acknowledgements

I thank Bart Bogaerts and Wolfgang Faber for interesting discussions on this
topic, and the reviewers for their dilligent reviews.

## References

  * Alviano and Faber [2019] Mario Alviano and Wolfgang Faber.  Chain answer sets for logic programs with generalized atoms.  In Francesco Calimeri, Nicola Leone, and Marco Manna, editors, Logics in Artificial Intelligence - 16th European Conference, JELIA2019, Rende, Italy, May 7-11, 2019, Proceedings, volume 11468 of Lecture Notes in Computer Science, pages 462–478. Springer, 2019.
  * Alviano et al. [2017] Mario Alviano, Francesco Calimeri, Carmine Dodaro, Davide Fuscà, Nicola Leone, Simona Perri, Francesco Ricca, Pierfrancesco Veltri, and Jessica Zangari.  The asp system dlv2.  In Logic Programming and Nonmonotonic Reasoning: 14th International Conference, LPNMR 2017, Espoo, Finland, July 3-6, 2017, Proceedings 14, pages 215–221. Springer, 2017.
  * Alviano et al. [2023] Mario Alviano, Wolfgang Faber, and Martin Gebser.  Aggregate semantics for propositional answer set programs.  Theory and Practice of Logic Programming, 23(1):157–194, 2023.
  * Brass and Dix [1995] Stefan Brass and Jürgen Dix.  Characterizations of the stable semantics by partial evaluation.  In Proceedings of LPNMR’95, pages 85–98. Springer, 1995.
  * Calimeri et al. [2012] Francesco Calimeri, Wolfgang Faber, Martin Gebser, Giovambattista Ianni, Roland Kaminski, Thomas Krennwallner, Nicola Leone, Francesco Ricca, and Torsten Schaub.  Asp-core-2: Input language format.  ASP Standardization Working Group, 2012.
  * Cousot and Cousot [1979] Patrick Cousot and Radhia Cousot.  Constructive versions of tarski’s fixed point theorems.  Pacific journal of Mathematics, 82(1):43–57, 1979.
  * Denecker and Vennekens [2014] Marc Denecker and Joost Vennekens.  The well-founded semantics is the principle of inductive definition, revisited.  In Fourteenth International Conference on the Principles of Knowledge Representation and Reasoning, 2014.
  * Denecker et al. [2000] Marc Denecker, Victor Marek, and Mirosław Truszczyński.  Approximations, stable operators, well-founded fixpoints and applications in nonmonotonic reasoning.  In Logic-based Artificial Intelligence, volume 597 of Engineering and Computer Science, pages 127–144. Springer, 2000.
  * Eiter and Geibinger [2023] Thomas Eiter and Tobias Geibinger.  Explaining answer-set programs with abstract constraint atoms.  In Proceedings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023, to appear), 2023.
  * Eiter et al. [2012] Thomas Eiter, Michael Fink, Thomas Krennwallner, and Christoph Redl.  Conflict-driven asp solving with external sources.  Theory and Practice of Logic Programming, 12(4-5):659–679, 2012\.
  * Erdem and Lifschitz [2003] Esra Erdem and Vladimir Lifschitz.  Tight logic programs.  Theory and Practice of Logic Programming, 3(4-5):499–518, 2003\.
  * Faber et al. [2004] Wolfgang Faber, Nicola Leone, and Gerald Pfeifer.  Recursive aggregates in disjunctive logic programs: Semantics and complexity.  In Proceedings of JELIA’04, volume 3229 of Lecture Notes in Computer Science, pages 200–212. Springer, 2004.
  * Ferraris [2011] Paolo Ferraris.  Logic programs with propositional connectives and aggregates.  ACM Transactions on Computational Logic (TOCL), 12(4):1–40, 2011\.
  * Gebser et al. [2016] Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Max Ostrowski, Torsten Schaub, and Philipp Wanko.  Theory solving made easy with clingo 5.  In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016.
  * Gelfond and Lifschitz [1991] Michael Gelfond and Vladimir Lifschitz.  Classical negation in logic programs and disjunctive databases.  New generation computing, 9(3-4):365–385, 1991.
  * Gelfond and Zhang [2014] Michael Gelfond and Yuanlin Zhang.  Vicious circle principle and logic programs with aggregates.  Theory and Practice of Logic Programming, 14(4-5):587–601, 2014\.
  * Heyninck and Bogaerts [2023] Jesse Heyninck and Bart Bogaerts.  Non-deterministic approximation operators: Ultimate operators, semi-equilibrium semantics, and aggregates.  Theory Pract. Log. Program., 23(4):632–647, 2023.
  * Heyninck et al. [2024] Jesse Heyninck, Ofer Arieli, and Bart Bogaerts.  Non-deterministic approximation fixpoint theory and its application in disjunctive logic programming.  Artif. Intell., 331:104110, 2024.
  * Heyninck [2023] Jesse Heyninck.  Semantics for logic programs with choice constructs on the basis of approximation fixpoint theory (preliminary report).  In Kai Sauerwald and Matthias Thimm, editors, Proceedings of the 21st International Workshop on Non-Monotonic Reasoning co-located with the 20th International Conference on Principles of Knowledge Representation and Reasoning (KR 2023) and co-located with the 36th International Workshop on Description Logics (DL 2023), Rhodes, Greece, September 2-4, 2023, volume 3464 of CEUR Workshop Proceedings, pages 74–83. CEUR-WS.org, 2023.
  * Kaminski and Schaub [2023] Roland Kaminski and Torsten Schaub.  On the foundations of grounding in answer set programming.  Theory and Practice of Logic Programming, 23(6):1138–1197, 2023\.
  * Kuratowski [1922] Kazimierz Kuratowski.  Une méthode d’élimination des nombres transfinis des raisonnements mathématiques.  Fundamenta mathematicae, 3(1):76–108, 1922.
  * Liu et al. [2010] Lengning Liu, Enrico Pontelli, Tran Cao Son, and Miroslaw Truszczyński.  Logic programs with abstract constraint atoms: The role of computations.  Artificial Intelligence, 174(3-4):295–315, 2010.
  * Marek and Remmel [2004] Victor W Marek and Jeffrey B Remmel.  Set constraints in logic programming.  In Logic Programming and Nonmonotonic Reasoning: 7th International Conference, LPNMR 2004 Fort Lauderdale, FL, USA, January 6-8, 2004 Proceedings 7, pages 167–179. Springer, 2004.
  * Pelov et al. [2007] Nikolay Pelov, Marc Denecker, and Maurice Bruynooghe.  Well-founded and stable semantics of logic programs with aggregates.  Theory and Practice of Logic Programming, 7(3):301–353, 2007.
  * Przymusinski [1990] Teodor C. Przymusinski.  The well-founded semantics coincides with the three-valued stable semantics.  Fundamenta Informaticae, 13(4):445–463, 1990.
  * Simons et al. [2002] Patrik Simons, Ilkka Niemelä, and Timo Soininen.  Extending and implementing the stable model semantics.  Artificial Intelligence, 138(1-2):181–234, 2002.
  * Son and Pontelli [2007] Tran Cao Son and Enrico Pontelli.  A constructive semantic characterization of aggregates in answer set programming.  Theory and Practice of Logic Programming, 7(3):355–375, 2007.
  * Vanbesien et al. [2022] Linde Vanbesien, Maurice Bruynooghe, and Marc Denecker.  Analyzing semantics of aggregate answer set programming using approximation fixpoint theory.  Theory and Practice of Logic Programming, 22(4):523–537, 2022.
  * Zorn [1935] Max Zorn.  A remark on method in transfinite algebra.  Bulletin of the American Mathematical Society, 41(10):667–670, 1935\.