# On the Foundations of Grounding in
Answer Set Programming

ROLAND KAMINSKI and TORSTEN SCHAUB
University of Potsdam
<EMAIL_ADDRESS>
###### Abstract

We provide a comprehensive elaboration of the theoretical foundations of
variable instantiation, or grounding, in Answer Set Programming (ASP).
Building on the semantics of ASP’s modeling language, we introduce a formal
characterization of grounding algorithms in terms of (fixed point) operators.
A major role is played by dedicated well-founded operators whose associated
models provide semantic guidance for delineating the result of grounding along
with on-the-fly simplifications. We address an expressive class of logic
programs that incorporates recursive aggregates and thus amounts to the scope
of existing ASP modeling languages. This is accompanied with a plain
algorithmic framework detailing the grounding of recursive aggregates. The
given algorithms correspond essentially to the ones used in the ASP grounder
gringo.

###### keywords:

answer set programming, grounding theory, grounding algorithms

##  1 Introduction

Answer Set Programming (ASP; lifschitz02a) allows us to address knowledge-
intense search and optimization problems in a greatly declarative way due to
its integrated modeling, grounding, and solving workflow [Gebser and Schaub
(2016), Kaufmann et al. (2016)]. Problems are modeled in a rule-based logical
language featuring variables, function symbols, recursion, and aggregates,
among others. Moreover, the underlying semantics allows us to express defaults
and reachability in an easy way. A corresponding logic program is then turned
into a propositional format by systematically replacing all variables by
variable-free terms. This process is called _grounding_. Finally, the actual
ASP solver takes the resulting propositional version of the original program
and computes its answer sets.

Given that both grounding and solving constitute the computational
cornerstones of ASP, it is surprising that the importance of grounding has
somehow been eclipsed by that of solving. This is nicely reflected by the
unbalanced number of implementations. With lparse [Syrjänen (2001b)], (the
grounder in) dlv [Faber et al. (2012)], and gringo [Gebser et al. (2011)],
three grounder implementations face dozens of solver implementations, among
them smodels [Simons et al. (2002)], (the solver in) dlv [Leone et al.
(2006)], assat [Lin and Zhao (2004)], cmodels [Giunchiglia et al. (2006)],
clasp [Gebser et al. (2012)], wasp [Alviano et al. (2015)] just to name the
major ones. What caused this imbalance? One reason may consist in the high
expressiveness of ASP’s modeling language and the resulting algorithmic
intricacy [Gebser et al. (2011)]. Another may lie in the popular viewpoint
that grounding amounts to database materialization, and thus that most
fundamental research questions have been settled. And finally the semantic
foundations of full-featured ASP modeling languages have been established only
recently [Harrison et al. (2014), Gebser et al. (2015)], revealing the
semantic gap to the just mentioned idealized understanding of grounding. In
view of this, research on grounding focused on algorithm and system design
[Faber et al. (2012), Gebser et al. (2011)] and the characterization of
language fragments guaranteeing finite propositional representations [Syrjänen
(2001b), Gebser et al. (2007), Lierler and Lifschitz (2009), Calimeri et al.
(2008)].

As a consequence, the theoretical foundations of grounding are much less
explored than those of solving. While there are several alternative ways to
characterize the answer sets of a logic program [Lifschitz (2008)], and thus
the behavior of a solver, we still lack indepth formal characterizations of
the input-output behavior of ASP grounders. Although we can describe the
resulting propositional program up to semantic equivalence, we have no formal
means to delineate the actual set of rules.

To this end, grounding involves some challenging intricacies. First of all,
the entire set of systematically instantiated rules is infinite in the worst —
yet not uncommon — case. For a simple example, consider the program:

$\displaystyle p(a)$ $\displaystyle p(X)$ $\displaystyle\leftarrow p(f(X))$

This program induces an infinite set of variable-free terms, viz. $a$, $f(a)$,
$f(f(a)),\dots$, that leads to an infinite propositional program by
systematically replacing variable $X$ by all these terms in the second rule,
viz.

$\displaystyle p(a),\quad p(a)\leftarrow p(f(a)),\quad p(f(a))\leftarrow
p(f(f(a))),\quad p(f(f(a)))\leftarrow p(f(f(f(a)))),\quad\dots$

On the other hand, modern grounders only produce the fact $p(a)$ and no
instances of the second rule, which is semantically equivalent to the infinite
program. As well, ASP’s modeling language comprises (possibly recursive)
aggregates, whose systematic grounding may be infinite in itself. To
illustrate this, let us extend the above program with the rule

$\displaystyle q$
$\displaystyle\leftarrow\\#\mathit{count}\\{X\mathrel{:}p(X)\\}=1$ (1)

deriving $q$ when the number of satisfied instances of $p$ is one. Analogous
to above, the systematic instantiation of the aggregate’s element results in
an infinite set, viz.

$\displaystyle\\{a\mathrel{:}p(a),\ f(a)\mathrel{:}p(f(a)),\
f(f(a))\mathrel{:}p(f(f(a))),\ \dots\\}.$

Again, a grounder is able to reduce the rule in 1 to the fact $q$ since only
$p(a)$ is obtained in our example. That is, it detects that the set amounts to
the singleton $\\{a\mathrel{:}p(a)\\}$, which satisfies the aggregate. After
removing the rule’s (satisfied) antecedent, it produces the fact $q$. In fact,
a solver expects a finite set of propositional rules including aggregates over
finitely many objects only. Hence, in practice, the characterization of the
grounding result boils down to identifying a finite yet semantically
equivalent set of rules (whenever possible). Finally, in practice, grounding
involves simplifications whose application depends on the ordering of rules in
the input. In fact, shuffling a list of propositional rules only affects the
order in which a solver enumerates answer sets, whereas shuffling a logic
program before grounding may lead to different though semantically equivalent
sets of rules. To see this, consider the program:

$\displaystyle p(X)$ $\displaystyle\leftarrow\neg q(X)\wedge u(X)$
$\displaystyle u(1)\quad$ $\displaystyle u(2)$ $\displaystyle q(X)$
$\displaystyle\leftarrow\neg p(X)\wedge v(X)$ $\displaystyle v(2)\quad v(3)$

This program has two answer sets; both contain $p(1)$ and $q(3)$, while one
contains $q(2)$ and the other $p(2)$. Systematically grounding the program
yields the obvious four rules. However, depending upon the order, in which the
rules are passed to a grounder, it already produces either the fact $p(1)$ or
$q(3)$ via simplification. Clearly, all three programs are distinct but
semantically equivalent in sharing the above two answer sets.

Our elaboration of the foundations of ASP grounding rests upon the semantics
of ASP’s modeling language [Harrison et al. (2014), Gebser et al. (2015)],
which captures the two aforementioned sources of infinity by associating non-
ground logic programs with infinitary propositional formulas [Truszczyński
(2012)]. Our main result shows that the stable models of a non-ground input
program coincide with the ones of the ground output program returned by our
grounding algorithm upon termination. In formal terms, this means that the
stable models of the infinitary formula associated with the input program
coincide with the ones of the resulting ground program. Clearly, the resulting
program must be finite and consist of finitary subformulas only. A major part
of our work is thus dedicated to equivalence preserving transformations
between ground programs. In more detail, we introduce a formal
characterization of grounding algorithms in terms of (fixed point) operators.
A major role is played by specific well-founded operators whose associated
models provide semantic guidance for delineating the result of grounding. More
precisely, we show how to obtain a finitary propositional formula capturing a
logic program whenever the corresponding well-founded model is finite, and
notably how this transfers to building a finite propositional program from an
input program during grounding. The two key instruments accomplishing this are
dedicated forms of _program simplification_ and _aggregate translation_ , each
addressing one of the two sources of infinity in the above example. In
practice, however, all these concepts are subject to _approximation_ , which
leads to the order-dependence observed in the last example.

We address an expressive class of logic programs that incorporates recursive
aggregates and thus amounts to the scope of existing ASP modeling languages
[Gebser et al. (2015)]. This is accompanied with an algorithmic framework
detailing the grounding of recursive aggregates. The given grounding
algorithms correspond essentially to the ones used in the ASP grounder gringo
[Gebser et al. (2011)]. In this way, our framework provides a formal
characterization of one of the most widespread grounding systems. In fact,
modern grounders like (the one in) dlv [Faber et al. (2012)] or gringo [Gebser
et al. (2011)] are based on database evaluation techniques [Ullman (1988),
Abiteboul et al. (1995)]. The instantiation of a program is seen as an
iterative bottom-up process starting from the program’s facts while being
guided by the accumulation of variable-free atoms possibly derivable from the
rules seen so far. During this process, a ground rule is produced if its
positive body atoms belong to the accumulated atoms, in which case its head
atom is added as well. This process is repeated until no further such atoms
can be added. From an algorithmic perspective, we show how a grounding
framework (relying upon database evaluation techniques) can be extended to
incorporate recursive aggregates.

Our paper is organized as follows.

Section 2 lays the basic foundations of our approach. We start in Section 2.1
by recalling definitions of (monotonic) operators on lattices; they constitute
the basic building blocks of our characterization of grounding algorithms. We
then review infinitary formulas along with their stable and well-founded
semantics in Sections 2.2, LABEL:, 2.3, LABEL: and 2.4, respectively. In this
context, we explore several operators and define a class of infinitary logic
programs that allows us to capture full-featured ASP languages with
(recursive) aggregates. Interestingly, we have to resort to concepts borrowed
from id-logic [Bruynooghe et al. (2016), Truszczyński (2012)] to obtain
monotonic operators that are indispensable for capturing iterative algorithms.
Notably, the id-well-founded model can be used for approximating regular
stable models. Finally, we define in Section 2.5 our concept of program
simplification and elaborate upon its semantic properties. The importance of
program simplification can be read off two salient properties. First, it
results in a finite program whenever the interpretation used for
simplification is finite. And second, it preserves all stable models when
simplified with the id-well-founded model of the program.

Section 3 is dedicated to the formal foundations of component-wise grounding.
As mentioned, each rule is instantiated in the context of all atoms being
possibly derivable up to this point. In addition, grounding has to take
subsequent atom definitions into account. To this end, we extend well-known
operators and resulting semantic concepts with contextual information, usually
captured by two- and four-valued interpretations, respectively, and elaborate
upon their formal properties that are relevant to grounding. In turn, we
generalize the contextual operators and semantic concepts to sequences of
programs in order to reflect component-wise grounding. The major emerging
concept is essentially a well-founded model for program sequences that takes
backward and forward contextual information into account. We can then
iteratively compute this model to approximate the well-founded model of the
entire program. This model-theoretic concept can be used for governing an
ideal grounding process.

Section 4 turns to logic programs with variables and aggregates. We align the
semantics of such aggregate programs with the one of ferraris11a but consider
infinitary formulas [Harrison et al. (2014)]. In view of grounding aggregates,
however, we introduce an alternative translation of aggregates that is
strongly equivalent to that of Ferraris but provides more precise well-founded
models. In turn, we refine this translation to be bound by an interpretation
so that it produces finitary formulas whenever this interpretation is finite.
Together, the program simplification introduced in Section 2.5 and aggregate
translation provide the basis for turning programs with aggregates into
semantically equivalent finite programs with finitary subformulas.

Section 5 further refines our semantic approach to reflect actual grounding
processes. To this end, we define the concept of an instantiation sequence
based on rule dependencies. We then use the contextual operators of Section 3
to define approximate models of instantiation sequences. While approximate
models are in general less precise than well-founded ones, they are better
suited for on-the-fly grounding along an instantiation sequence. Nonetheless,
they are strong enough to allow for completely evaluating stratified programs.

Section 6 lays out the basic algorithms for grounding rules, components, and
entire programs and characterizes their output in terms of the semantic
concepts developed in the previous sections. Of particular interest is the
treatment of aggregates, which are decomposed into dedicated normal rules
before grounding, and reassembled afterward. This allows us to ground rules
with aggregates by means of grounding algorithms for normal rules. Finally, we
show that our grounding algorithm guarantees that an obtained finite ground
program is equivalent to the original non-ground program.

The previous sections focus on the theoretical and algorithmic cornerstones of
grounding. Section 7 refines these concepts by further detailing aggregate
propagation, algorithm specifics, and the treatment of language constructs
from gringo’s input language.

We relate our contributions to the state of the art in Section 8 and summarize
it in Section 9.

Although the developed approach is implemented in gringo series 4 and 5, their
high degree of sophistication make it hard to retrace the algorithms from
Section 6. Hence, to ease comprehensibility, we have moreover implemented the
presented approach in $\mu$-gringo111The $\mu$-gringo system is available at
https://github.com/potassco/mu-gringo. in a transparent way and equipped it
with means for retracing the developed concepts during grounding. This can
thus be seen as the practical counterpart to the formal elaboration given
below. Also, this system may enable some readers to construct and to
experiment with own grounder extensions.

This paper draws on material presented during an invited talk at the third
workshop on grounding, transforming, and modularizing theories with variables
[Gebser et al. (2015)].

##  2 Foundations

###  2.1 Operators on lattices

This section recalls basic concepts on operators on complete lattices.

A _complete lattice_ is a partially ordered set $(L,\leq)$ in which every
subset $S\subseteq L$ has a greatest lower bound and a least upper bound in
$(L,\leq)$.

An _operator_ $O$ on lattice $(L,\leq)$ is a function from $L$ to $L$. It is
_monotone_ if $x\leq y$ implies $O(x)\leq O(y)$ for each $x,y\in L$; and it is
_antimonotone_ if $x\leq y$ implies $O(y)\leq O(x)$ for each $x,y\in L$.

Let $O$ be an operator on lattice $(L,\leq)$. A _prefixed point_ of $O$ is an
$x\in L$ such that $O(x)\leq x$. A _postfixed point_ of $O$ is an $x\in L$
such that $x\leq O(x)$. A _fixed point of_ $O$ is an $x\in L$ such that
$x=O(x)$, i.e., it is both a prefixed and a postfixed point.

######  Theorem 1 (Knaster-Tarski; tarski55).

Let $O$ be a monotone operator on complete lattice $(L,\leq)$. Then, we have
the following properties:

  1. (a)

Operator $O$ has a least fixed and prefixed point which are identical.

  2. (b)

Operator $O$ has a greatest fixed and postfixed point which are identical.

  3. (c)

The fixed points of $O$ form a complete lattice.

###  2.2 Formulas and interpretations

We begin with a propositional signature $\Sigma$ consisting of a set of atoms.
Following truszczynski12a, we define the sets
$\mathcal{F}_{0},\mathcal{F}_{1},\ldots$ of formulas as follows:

  * •

$\mathcal{F}_{0}$ is the set of all propositional atoms in $\Sigma$,

  * •

$\mathcal{F}_{i+1}$ is the set of all elements of $\mathcal{F}_{i}$, all
expressions $\mathcal{H}^{\wedge}$ and $\mathcal{H}^{\vee}$ with
$\mathcal{H}\subseteq\mathcal{F}_{i}$, and all expressions $F\rightarrow G$
with $F,G\in\mathcal{F}_{i}$.

The set $\mathcal{F}=\bigcup_{i=0}^{\infty}\mathcal{F}_{i}$ contains all
_(infinitary propositional) formulas_ over $\Sigma$.

In the following, we use the shortcuts

  * •

$\top=\emptyset^{\wedge}$ and $\bot=\emptyset^{\vee}$,

  * •

${\neg}F=F\rightarrow\bot$ where $F$ is a formula, and

  * •

$F\wedge G={\\{F,G\\}}^{\wedge}$ and $F\vee G={\\{F,G\\}}^{\vee}$ where $F$
and $G$ are formulas.

We say that a formula is _finitary_ , if it has a finite number of
subformulas.

An occurrence of a subformula in a formula is called _positive_ , if the
number of implications containing that occurrence in the antecedent is even,
and _strictly positive_ if that number is zero; if that number is odd the
occurrence is _negative_. The sets ${F}^{+}$ and ${F}^{-}$ gather all atoms
occurring positively or negatively in formula $F$, respectively; if applied to
a set of formulas, both expressions stand for the union of the respective
atoms in the formulas. Also, we define ${F}^{\pm}={F}^{+}\cup{F}^{-}$ as the
set of all atoms occurring in $F$.

A _two-valued interpretation_ over signature $\Sigma$ is a set $I$ of
propositional atoms such that $I\subseteq\Sigma$. Atoms in an interpretation
$I$ are considered _true_ and atoms in $\Sigma\setminus I$ as _false_. The set
of all interpretations together with the $\subseteq$ relation forms a complete
lattice.

The satisfaction relation between interpretations and formulas is defined as
follows:

  * •

$I\models a$ for atoms $a$ if $a\in I$,

  * •

$I\models\mathcal{H}^{\wedge}$ if $I\models F$ for all $F\in\mathcal{H}$,

  * •

$I\models\mathcal{H}^{\vee}$ if $I\models F$ for some $F\in\mathcal{H}$, and

  * •

$I\models F\rightarrow G$ if $I\not\models F$ or $I\models G$.

An interpretation $I$ is a _model_ of a set $\mathcal{H}$ of formulas, written
$I\models\mathcal{H}$, if it satisfies each formula in the set.

In the following, all atoms, formulas, and interpretations operate on the same
(implicit) signature, unless mentioned otherwise.

###  2.3 Logic programs and stable models

Our terminology in this section keeps following the one of truszczynski12a.

The _reduct_ $F^{I}$ of a formula $F$ w.r.t. an interpretation $I$ is defined
as:

  * •

$\bot$ if $I\not\models F$,

  * •

$a$ if $I\models F$ and $F=a\in\mathcal{F}_{0}$,

  * •

${\\{G^{I}\mid G\in\mathcal{H}\\}}^{\wedge}$ if $I\models F$ and
$F=\mathcal{H}^{\wedge}$,

  * •

${\\{G^{I}\mid G\in\mathcal{H}\\}}^{\vee}$ if $I\models F$ and
$F=\mathcal{H}^{\vee}$, and

  * •

$G^{I}\rightarrow H^{I}$ if $I\models F$ and $F=G\rightarrow H$.

An interpretation $I$ is a _stable model_ of a formula $F$ if it is among the
(set inclusion) minimal models of $F^{I}$.

Note that the reduct removes (among other unsatisfied subformulas) all
occurrences of atoms that are false in $I$. Thus, the satisfiability of the
reduct does not depend on such atoms, and all minimal models of $F^{I}$ are
subsets of $I$. Hence, if $I$ is a stable model of $F$, then it is the only
minimal model of $F^{I}$.

Sets $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$ of infinitary formulas are
_equivalent_ if they have the same stable models and _classically equivalent_
if they have the same models; they are _strongly equivalent_ if, for any set
$\mathcal{H}$ of infinitary formulas, $\mathcal{H}_{1}\cup\mathcal{H}$ and
$\mathcal{H}_{2}\cup\mathcal{H}$ are equivalent. As shown by halipeva17a, this
also allows for replacing a part of any formula with a strongly equivalent
formula without changing the set of stable models.

In the following, we consider implications with atoms as consequent and
formulas as antecedent. As common in logic programming, they are referred to
as rules, heads, and bodies, respectively, and denoted by reversing the
implication symbol. More precisely, an _$\mathcal{F}$ -program_ is set of
_rules_ of form $h\leftarrow F$ where $h\in\mathcal{F}_{0}$ and
$F\in\mathcal{F}$. We use $H(h\leftarrow F)=h$ to refer to rule _heads_ and
$B(h\leftarrow F)=F$ to refer to rule _bodies_. We extend this by letting
$H(P)\ =\\{H(r)\mid r\in P\\}$ and $B(P)\ =\\{B(r)\mid r\in P\\}$ for any
program $P$.

An interpretation $I$ is a model of an $\mathcal{F}$-program $P$, written
$I\models P$, if $I\models B(r)\rightarrow H(r)$ for all $r\in P$. The latter
is also written as $I\models r$. We define the reduct of $P$ w.r.t. $I$ as
$P^{I}=\\{r^{I}\mid r\in P\\}$ where $r^{I}=H(r)\leftarrow B(r)^{I}$. As
above, an interpretation $I$ is a _stable model_ of $P$ if $I$ is among the
minimal models of $P^{I}$. Just like the original definition of gellif88b, the
reduct of such programs leaves rule heads intact and only reduces rule bodies.
(This feature fits well with the various operators defined in the sequel.)

This program-oriented reduct yields the same stable models as obtained by
applying the full reduct to the corresponding infinitary formula.

######  Proposition 2.

Let $P$ be an $\mathcal{F}$-program.

Then, the stable models of formula ${\\{B(r)\rightarrow H(r)\mid r\in
P\\}}^{\wedge}$ are the same as the stable models of program $P$.

For programs, truszczynski12a introduces in an alternative reduct, replacing
each negatively occurring atom with $\bot$, if it is falsified, and with
$\top$, otherwise. More precisely, the so-called _id -reduct_ $F_{I}$ of a
formula $F$ w.r.t. an interpretation $I$ is defined as

$\displaystyle a_{I}$ $\displaystyle=a$ $\displaystyle a_{\overline{I}}$
$\displaystyle=\top\text{\ if }a\in I$ $\displaystyle a_{\overline{I}}$
$\displaystyle=\bot\text{\ if }a\notin I$
$\displaystyle\mathcal{H}^{\wedge}_{I}$ $\displaystyle={\\{F_{I}\mid
F\in\mathcal{H}\\}}^{\wedge}$
$\displaystyle\mathcal{H}^{\wedge}_{\overline{I}}$
$\displaystyle={\\{F_{\overline{I}}\mid F\in\mathcal{H}\\}}^{\wedge}$
$\displaystyle\mathcal{H}^{\vee}_{I}$ $\displaystyle={\\{F_{I}\mid
F\in\mathcal{H}\\}}^{\vee}$ $\displaystyle\mathcal{H}^{\vee}_{\overline{I}}$
$\displaystyle={\\{F_{\overline{I}}\mid F\in\mathcal{H}\\}}^{\vee}$
$\displaystyle{(F\rightarrow G)}_{I}$
$\displaystyle=F_{\overline{I}}\rightarrow G_{I}$ $\displaystyle{(F\rightarrow
G)}_{\overline{I}}$ $\displaystyle=F_{I}\rightarrow G_{\overline{I}}$

where $a$ is an atom, $\mathcal{H}$ a set of formulas, and $F$ and $G$ are
formulas.

The id-reduct of an $\mathcal{F}$-program $P$ w.r.t. an interpretation $I$ is
$P_{I}=\\{r_{I}\mid r\in P\\}$ where $r_{I}=H(r)\leftarrow B(r)_{I}$. As with
$r^{I}$, the transformation of $r$ into $r_{I}$ leaves the head of $r$
unaffected.

######  Example 1.

Consider the program containing the single rule

$\displaystyle p$ $\displaystyle\leftarrow{\neg}{\neg}p.$

We get the following reduced programs w.r.t. interpretations $\emptyset$ and
$\\{p\\}$:

$\displaystyle\\{p\leftarrow{\neg}{\neg}p\\}^{\emptyset}$
$\displaystyle=\\{p\leftarrow\bot\\}$
$\displaystyle\\{p\leftarrow{\neg}{\neg}p\\}^{\\{p\\}}$
$\displaystyle=\\{p\leftarrow{\neg}\bot\\}$
$\displaystyle\\{p\leftarrow{\neg}{\neg}p\\}_{\emptyset}$
$\displaystyle=\\{p\leftarrow{\neg}{\neg}p\\}\qquad=$
$\displaystyle\\{p\leftarrow{\neg}{\neg}p\\}_{\\{p\\}}$
$\displaystyle=\\{p\leftarrow{\neg}{\neg}p\\}$

Note that both reducts leave the rule’s head intact.

Extending the definition of positive occurrences, we define a formula as
_(strictly) positive_ if all its atoms occur (strictly) positively in the
formula. We define an $\mathcal{F}$-program as (strictly) positive if all its
rule bodies are (strictly) positive.

For example, the program in Example 1 is positive but not strictly positive
because the only body atom $p$ appears in the scope of two antecedents within
the rule body ${\neg}{\neg}p$.

As put forward by emdkow76a, we may associate with each program $P$ its _one-
step provability operator_ $T_{P}$, defined for any interpretation $X$ as

$\displaystyle T_{P}(X)$ $\displaystyle=\\{H(r)\mid r\in P,X\models B(r)\\}.$

######  Proposition 3 (truszczynski12a).

Let $P$ be a positive $\mathcal{F}$-program.

Then, the operator $T_{P}$ is monotone.

Fixed points of $T_{P}$ are models of $P$ guaranteeing that each contained
atom is supported by some rule in $P$; prefixed points of $T_{P}$ correspond
to the models of $P$. According to Theorem 1 (a), the $T_{P}$ operator has a
least fixed point for positive $\mathcal{F}$-programs. We refer to this fixed
point as the _least model_ of $P$, and write it as $\mathit{LM}(P)$.

Observing that the id-reduct replaces all negative occurrences of atoms, any
id-reduct $P_{I}$ of a program w.r.t. an interpretation $I$ is positive and
thus possesses a least model $\mathit{LM}(P_{I})$. This gives rise to the
following definition of a stable operator [Truszczyński (2012)]: Given an
$\mathcal{F}$-program $P$, its _id -stable operator_ is defined for any
interpretation $I$ as

$S_{P}(I)=\mathit{LM}(P_{I}).$

The fixed points of $S_{P}$ are the _id -stable models_ of $P$.

Note that neither the program reduct $P^{I}$ nor the formula reduct $F^{I}$
guarantee (least) models. Also, stable models and id-stable models do not
coincide in general.

######  Example 2.

Reconsider the program from Example 1, comprising rule

$\displaystyle p$ $\displaystyle\leftarrow{\neg}{\neg}p.$

This program has the two stable models $\emptyset$ and $\\{p\\}$, but the
empty model is the only id-stable model.

######  Proposition 4 (truszczynski12a).

Let $P$ be an $\mathcal{F}$-program.

Then, the id-stable operator $S_{P}$ is antimonotone.

No analogous antimonotone operator is obtainable for $\mathcal{F}$-programs by
using the program reduct $P^{I}$ (and for general theories with the formula
reduct $F^{I}$). To see this, reconsider Example 2 along with its two stable
models $\emptyset$ and $\\{p\\}$. Given that both had to be fixed points of
such an operator, it would behave monotonically on $\emptyset$ and $\\{p\\}$.

In view of this, we henceforth consider exclusively id-stable operators and
drop the prefix ‘id’. However, we keep the distinction between stable and id-
stable models.

truszczynski12a identifies in a class of programs for which stable models and
id-stable models coincide. The set $\mathcal{N}$ consists of all formulas $F$
such that any implication in $F$ has $\bot$ as consequent and no occurrences
of implications in its antecedent. An $\mathcal{N}$-program consists of rules
of form $h\leftarrow F$ where $h\in\mathcal{F}_{0}$ and $F\in\mathcal{N}$.

######  Proposition 5 (truszczynski12a).

Let $P$ be an $\mathcal{N}$-program.

Then, the stable and id-stable models of $P$ coincide.

Note that a positive $\mathcal{N}$-program is also strictly positive.

###  2.4 Well-founded models

Our terminology in this section follows the one of truszczynski18a and traces
back to the early work of belnap77a and fitting02a.222The interested reader is
referred to the tutorial by truszczynski18a for further details.

We deal with pairs of sets and extend the basic set relations and operations
accordingly. Given sets $I^{\prime}$, $I$, $J^{\prime}$, $J$, and $X$, we
define:

  * •

$(I^{\prime},J^{\prime})\mathrel{\bar{\prec}}(I,J)$ if $I^{\prime}\prec I$ and
$J^{\prime}\prec J$ for
$(\bar{\prec},\prec)\in\\{(\sqsubset,\subset),(\sqsubseteq,\subseteq)\\}$

  * •

$(I^{\prime},J^{\prime})\mathrel{\bar{\circ}}(I,J)=(I^{\prime}\circ
I,J^{\prime}\circ J)$ for
$(\bar{\circ},\circ)\in\\{(\sqcup,\cup),(\sqcap,\cap),(\smallsetminus,\setminus)\\}$

  * •

$(I,J)\mathrel{\bar{\circ}}X=(I,J)\mathrel{\bar{\circ}}(X,X)$ for
$\bar{\circ}\in\\{\sqcup,\sqcap,\smallsetminus\\}$

A _four-valued interpretation_ over signature $\Sigma$ is represented by a
pair $(I,J)\sqsubseteq(\Sigma,\Sigma)$ where $I$ stands for _certain_ and $J$
for _possible_ atoms. Intuitively, an atom that is

  * •

certain and possible is _true_ ,

  * •

certain but not possible is _inconsistent_ ,

  * •

not certain but possible is _unknown_ , and

  * •

not certain and not possible is _false_.

A four-valued interpretation $(I^{\prime},J^{\prime})$ is more precise than a
four-valued interpretation $(I,J)$, written
$(I,J)\leq_{p}(I^{\prime},J^{\prime})$, if $I\subseteq I^{\prime}$ and
$J^{\prime}\subseteq J$. The precision ordering also has an intuitive reading:
the more atoms are certain or the fewer atoms are possible, the more precise
is an interpretation. The least precise four-valued interpretation over
$\Sigma$ is $(\emptyset,\Sigma)$. As with two-valued interpretations, the set
of all four-valued interpretations over a signature $\Sigma$ together with the
relation $\leq_{p}$ forms a complete lattice. A four-valued interpretation is
called _inconsistent_ if it contains an inconsistent atom; otherwise, it is
called _consistent_. It is _total_ whenever it makes all atoms either true or
false. Finally, $(I,J)$ is called _finite_ whenever both $I$ and $J$ are
finite.

Following truszczynski18a, we define the _id -well-founded operator_ of an
$\mathcal{F}$-program $P$ for any four-valued interpretation $(I,J)$ as

$W_{P}(I,J)=(S_{P}(J),S_{P}(I)).$

This operator is monotone w.r.t. the precision ordering $\leq_{p}$. Hence, by
Theorem 1 (a), $W_{P}$ has a least fixed point, which defines the _id -well-
founded model_ of $P$, also written as $\mathit{WM}(P)$. In what follows, we
drop the prefix ‘id’ and simply refer to the id-well-founded model of a
program as its well-founded model. (We keep the distinction between stable and
id-stable models.)

Any well-founded model $(I,J)$ of an $\mathcal{F}$-program $P$ satisfies
$I\subseteq J$.

######  Lemma 6.

Let $P$ be an $\mathcal{F}$-Program.

Then, the well-founded model $\mathit{WM}(P)$ of $P$ is consistent.

######  Example 3.

Consider program ${P}_{\ref{ex:well-founded}}$ consisting of the following
rules:

$\displaystyle a$ $\displaystyle b$ $\displaystyle\leftarrow a$ $\displaystyle
c$ $\displaystyle\leftarrow{\neg}b$ $\displaystyle d$ $\displaystyle\leftarrow
c$ $\displaystyle e$ $\displaystyle\leftarrow{\neg}d$

We compute the well-founded model of ${P}_{\ref{ex:well-founded}}$ in four
iterations starting from $(\emptyset,\Sigma)$:

$\displaystyle S_{P}(\Sigma)$ $\displaystyle=\\{a,b\\}$ $\displaystyle
S_{P}(\emptyset)$ $\displaystyle=\\{a,b,c,d,e\\}$ 1. $\displaystyle
S_{P}(\\{a,b,c,d,e\\})$ $\displaystyle=\\{a,b\\}$ $\displaystyle
S_{P}(\\{a,b\\})$ $\displaystyle=\\{a,b,e\\}$ 2. $\displaystyle
S_{P}(\\{a,b,e\\})$ $\displaystyle=\\{a,b,e\\}$ $\displaystyle
S_{P}(\\{a,b\\})$ $\displaystyle=\\{a,b,e\\}$ 3. $\displaystyle
S_{P}(\\{a,b,e\\})$ $\displaystyle=\\{a,b,e\\}$ $\displaystyle
S_{P}(\\{a,b,e\\})$ $\displaystyle=\\{a,b,e\\}$ 4.

The left and right column reflect the certain and possible atoms computed at
each iteration, respectively. We reach a fixed point at Step 4. Accordingly,
the well-founded model of ${P}_{\ref{ex:well-founded}}$ is
$(\\{a,b,e\\},\\{a,b,e\\})$.

Unlike general $\mathcal{F}$-programs, the class of $\mathcal{N}$-programs
warrants the same stable and id-stable models for each of its programs.
Unfortunately, $\mathcal{N}$-programs are too restricted for our purpose (for
instance, for capturing aggregates in rule bodies333Ferraris’ semantics
[Ferraris (2011)] of aggregates introduces implications, which results in
rules beyond the class of $\mathcal{N}$-programs.). To this end, we define a
more general class of programs and refer to them as $\mathcal{R}$-programs.
Although id-stable models of $\mathcal{R}$-programs may differ from their
stable models (see below), their well-founded models encompass both stable and
id-stable models. Thus, well-founded models can be used for characterizing
stable model-preserving program transformations. In fact, we see in Section
2.5 that the restriction of $\mathcal{F}$\- to $\mathcal{R}$-programs allows
us to provide tighter semantic characterizations of program simplifications.

We define $\mathcal{R}$ to be the set of all formulas $F$ such that
implications in $F$ have no further occurrences of implications in their
antecedents. Then, an _$\mathcal{R}$ -program_ consists of rules of form
$h\leftarrow F$ where $h\in\mathcal{F}_{0}$ and $F\in\mathcal{R}$. As with
$\mathcal{N}$-programs, a positive $\mathcal{R}$-program is also strictly
positive.

Our next result shows that (id-)well-founded models can be used for
approximating (regular) stable models of $\mathcal{R}$-programs.

######  Theorem 7.

Let $P$ be an $\mathcal{R}$-program and $(I,J)$ be the well-founded model of
$P$.

If $X$ is a stable model of $P$, then $I\subseteq X\subseteq J$.

######  Example 4.

Consider the $\mathcal{R}$-program ${P}_{\ref{ex:r-program}}$:444The choice of
the body $b\rightarrow a$ is not arbitrary since it can be seen as
representing the aggregate $\mathrm{\\#sum}\\{1:a,-1:b\\}\geq 0$.

$\displaystyle c$ $\displaystyle\leftarrow(b\rightarrow a)$ $\displaystyle a$
$\displaystyle\leftarrow b$ $\displaystyle a$ $\displaystyle\leftarrow c$
$\displaystyle b$ $\displaystyle\leftarrow a$

Observe that $\\{a,b,c\\}$ is the only stable model of
${P}_{\ref{ex:r-program}}$, the program does not have any id-stable models,
and the well-founded model of ${P}_{\ref{ex:r-program}}$ is
$(\emptyset,\\{a,b,c\\})$. In accordance with Theorem 7, the stable model of
${P}_{\ref{ex:r-program}}$ is enclosed in the well-founded model.

Note that the id-reduct handles $b\rightarrow a$ the same way as ${\neg}b\vee
a$. In fact, the program obtained by replacing

$\displaystyle c$ $\displaystyle\leftarrow(b\rightarrow a)$

with

$\displaystyle c$ $\displaystyle\leftarrow{\neg}b\vee a$

is an $\mathcal{N}$-program and has neither stable nor id-stable models.

Further, note that the program in Example 2 is not an $\mathcal{R}$-program,
whereas the one in Example 3 is an $\mathcal{R}$-program.

###  2.5 Program simplification

In this section, we define a concept of program simplification relative to a
four-valued interpretation and show how its result can be characterized by the
semantic means from above. This concept has two important properties. First,
it results in a finite program whenever the interpretation used for
simplification is finite. And second, it preserves all (regular) stable models
of $\mathcal{R}$-programs when simplified with their well-founded models.

######  Definition 1.

Let $P$ be an $\mathcal{F}$-program, and $(I,J)$ be a four-valued
interpretation.

We define the simplification of $P$ w.r.t. $(I,J)$ as

$\displaystyle P^{(I,J)}$ $\displaystyle=\\{r\in P\mid J\models B(r)_{I}\\}.$

For simplicity, we drop parentheses and we write $P^{I,J}$ instead of
$P^{(I,J)}$ whenever clear from context.

The program simplification $P^{I,J}$ acts as a filter eliminating inapplicable
rules that fail to satisfy the condition $J\models B(r)_{I}$. That is, first,
all negatively occurring atoms in $B(r)$ are evaluated w.r.t. the certain
atoms in $I$ and replaced accordingly by $\bot$ and $\top$, respectively.
Then, it is checked whether the reduced body $B(r)_{I}$ is satisfiable by the
possible atoms in $J$. Only in this case, the rule is kept in $P^{I,J}$. No
simplifications are applied to the remaining rules. This is illustrated in
Example 5 below.

Note that $P^{I,J}$ is finite whenever $(I,J)$ is finite.

Observe that for an $\mathcal{F}$-program $P$ the head atoms in ${P^{I,J}}$
correspond to the result of applying the provability operator of program
$P_{I}$ to the possible atoms in $J$, i.e., $H(P^{I,J})=T_{P_{I}}(J)$.

Our next result shows that programs simplified with their well-founded model
maintain this model.

######  Theorem 8.

Let $P$ be an $\mathcal{F}$-program and $(I,J)$ be the well-founded model of
$P$.

Then, $P$ and $P^{I,J}$ have the same well-founded model.

######  Example 5.

In Example 3, we computed the well-founded model $(\\{a,b,e\\},\\{a,b,e\\})$
of ${P}_{\ref{ex:well-founded}}$. With this, we obtain the simplified program
${P}_{\ref{ex:well-founded}}^{\prime}={P}_{\ref{ex:well-
founded}}^{\\{a,b,e\\},\\{a,b,e\\}}$ after dropping $c\leftarrow{\neg}b$ and
$d\leftarrow c$:

$\displaystyle a$ $\displaystyle b$ $\displaystyle\leftarrow a$ $\displaystyle
e$ $\displaystyle\leftarrow{\neg}d$

Next, we check that the well-founded model of ${P}_{\ref{ex:well-
founded}}^{\prime}$ corresponds to the well-founded model of
${P}_{\ref{ex:well-founded}}$:

$\displaystyle S_{{P}_{\ref{ex:well-founded}}^{\prime}}(\Sigma)$
$\displaystyle=\\{a,b\\}$ $\displaystyle S_{{P}_{\ref{ex:well-
founded}}^{\prime}}(\emptyset)$ $\displaystyle=\\{a,b,e\\}$ 1. $\displaystyle
S_{{P}_{\ref{ex:well-founded}}^{\prime}}(\\{a,b,e\\})$
$\displaystyle=\\{a,b,e\\}$ $\displaystyle S_{{P}_{\ref{ex:well-
founded}}^{\prime}}(\\{a,b\\})$ $\displaystyle=\\{a,b,e\\}$ 2. $\displaystyle
S_{{P}_{\ref{ex:well-founded}}^{\prime}}(\\{a,b,e\\})$
$\displaystyle=\\{a,b,e\\}$ $\displaystyle S_{{P}_{\ref{ex:well-
founded}}^{\prime}}(\\{a,b,e\\})$ $\displaystyle=\\{a,b,e\\}$ 3.

We observe that it takes two applications of the well-founded operator to
obtain the well-founded model. This could be reduced to one step if atoms
false in the well-founded model would be removed from the negative bodies by
the program simplification. Keeping them is a design decision with the goal to
simplify notation in the following.

The next series of results further elaborates on semantic invariants
guaranteed by our concept of program simplification. The first result shows
that it preserves all stable models between the sets used for simplification.

######  Theorem 9.

Let $P$ be an $\mathcal{F}$-program, and $I$, $J$ and $X$ be two-valued
interpretations.

If $I\subseteq X\subseteq J$, then $X$ is a stable model of $P$ iff $X$ is a
stable model of $P^{I,J}$.

As a consequence, we obtain that $\mathcal{R}$-programs simplified with their
well-founded model also maintain stable models.

######  Corollary 10.

Let $P$ be an $\mathcal{R}$-program and $(I,J)$ be the well-founded model of
$P$.

Then, $P$ and $P^{I,J}$ have the same stable models.

For instance, the $\mathcal{R}$-program in Example 3 and its simplification in
Example 5 have the same stable model. Unlike this, the program from Example 2
consisting of rule $p\leftarrow{\neg}{\neg}p$ induces two stable models, while
its simplification w.r.t. its well-founded model $(\emptyset,\emptyset)$
yields an empty program admitting the empty stable model only.

Note that given an $\mathcal{R}$-program with a finite well-founded model, we
obtain a semantically equivalent finite program via simplification. As
detailed in the following sections, grounding algorithms only compute
approximations of the well-founded model. However, as long as the
approximation is finite, we still obtain semantically equivalent finite
programs. This is made precise by the next two results showing that any
program between the original and its simplification relative to its well-
founded model preserves the well-founded model, and that this extends to all
stable models for $\mathcal{R}$-programs.

######  Theorem 11.

Let $P$ and $Q$ be $\mathcal{F}$-programs, and $(I,J)$ be the well-founded
model of $P$.

If $P^{I,J}\subseteq Q\subseteq P$, then $P$ and $Q$ have the same well-
founded models.

######  Corollary 12.

Let $P$ and $Q$ be $\mathcal{R}$-programs, and $(I,J)$ be the well-founded
model of $P$.

If $P^{I,J}\subseteq Q\subseteq P$, then $P$ and $Q$ are equivalent.

##  3 Splitting

One of the first steps during grounding is to group rules into components
suitable for successive instantiation. This amounts to splitting a logic
program into a sequence of subprograms. The rules in each such component are
then instantiated with respect to the atoms possibly derivable from previous
components, starting with some component consisting of facts only. In other
words, grounding is always performed relative to a set of atoms that provide a
context. Moreover, atoms found to be true or false can be used for on-the-fly
simplifications.

Accordingly, this section parallels the above presentation by extending the
respective formal concepts with contextual information provided by atoms in a
two- and four-valued setting. We then assemble the resulting concepts to
enable their consecutive application to sequences of subprograms.
Interestingly, the resulting notion of splitting allows for more fine-grained
splitting than the traditional concept [Lifschitz and Turner (1994)] since it
allows us to partition rules in an arbitrary way. In view of grounding, we
show that once a program is split into a sequence of programs, we can
iteratively compute an approximation of the well-founded model by considering
in turn each element in the sequence.

In what follows, we append letter ‘$C$’ to names of interpretations having a
contextual nature.

To begin with, we extend the one-step provability operator accordingly.

######  Definition 2.

Let $P$ be an $\mathcal{F}$-program and $\mathit{I\\!C}$ be a two-valued
interpretation.

For any two-valued interpretation $I$, we define the _one-step provability
operator of $P$ relative to_ $\mathit{I\\!C}$ as

$\displaystyle T_{P}^{\mathit{I\\!C}}(I)$
$\displaystyle=T_{P}(\mathit{I\\!C}\cup I).$

A prefixed point of $T_{P}^{\mathit{I\\!C}}$ is a also a prefixed point of
$T_{P}$. Thus, each prefixed point of $T_{P}^{\mathit{I\\!C}}$ is a model of
$P$ but not vice versa.

To see this, consider program $P=\\{a\leftarrow b\\}$. We have
$T_{P}(\emptyset)=\emptyset$ and $T_{P}^{\\{b\\}}(\emptyset)=\\{a\\}$. Hence,
$\emptyset$ is a (pre)fixed point of $T_{P}$ but not of $T_{P}^{\\{b\\}}$
since $\\{a\\}\not\subseteq\emptyset$. The set $\\{a\\}$ is a prefixed point
of both operators.

######  Proposition 13.

Let $P$ be a positive program, and $\mathit{I\\!C}$ and $J$ be two valued
interpretations.

Then, the operators $T_{P}^{\mathit{I\\!C}}$ and
$T_{P}^{\,\boldsymbol{\cdot}}(J)$ are both monotone.

We use Theorems 1 and 13 to define a contextual stable operator.

######  Definition 3.

Let $P$ be an $\mathcal{F}$-program and $\mathit{I\\!C}$ be a two-valued
interpretation.

For any two-valued interpretation $J$, we define the _stable operator
relative_ to $\mathit{I\\!C}$, written $S_{P}^{\mathit{I\\!C}}(J)$, as the
least fixed point of $T_{P_{J}}^{\mathit{I\\!C}}$.

While the operator is antimonotone w.r.t. its argument $J$, it is monotone
regarding its parameter $\mathit{I\\!C}$.

######  Proposition 14.

Let $P$ be an $\mathcal{F}$-program, and $\mathit{I\\!C}$ and $J$ be two-
valued interpretations.

Then, the operators $S_{P}^{\mathit{I\\!C}}$ and
$S_{P}^{\,\boldsymbol{\cdot}}(J)$ are antimonotone and monotone, respectively.

By building on the relative stable operator, we next define its well-founded
counterpart. Unlike above, the context is now captured by a four-valued
interpretation.

######  Definition 4.

Let $P$ be an $\mathcal{F}$-program and $(\mathit{I\\!C},\mathit{J\\!C})$ be a
four-valued interpretation.

For any four-valued interpretation $(I,J)$, we define the _well-founded
operator relative_ to $(\mathit{I\\!C},\mathit{J\\!C})$ as

$\displaystyle
W_{P}^{(\mathit{I\\!C},\mathit{J\\!C})}(I,J)=(S_{P}^{\mathit{I\\!C}}(J\cup\mathit{J\\!C}),S_{P}^{\mathit{J\\!C}}(I\cup\mathit{I\\!C})).$

As above, we drop parentheses and simply write $W_{P}^{I,J}$ instead of
$W_{P}^{(I,J)}$. Also, we keep refraining from prepending the prefix ‘id’ to
the well-founded operator along with all concepts derived from it below.

Unlike the stable operator, the relative well-founded one is monotone on both
its argument and parameter.

######  Proposition 15.

Let $P$ be an $\mathcal{F}$-program, and $(I,J)$ and
$(\mathit{I\\!C},\mathit{J\\!C})$ be four-valued interpretations.

Then, the operators $W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}$ and
$W_{P}^{\,\boldsymbol{\cdot}}(I,J)$ are both monotone w.r.t. the precision
ordering.

From Theorems 1 and 15, we get that the relative well-founded operator has a
least fixed point.

######  Definition 5.

Let $P$ be an $\mathcal{F}$-program and $(\mathit{I\\!C},\mathit{J\\!C})$ be a
four-valued interpretation.

We define the _well-founded model_ of $P$ _relative_ to
$(\mathit{I\\!C},\mathit{J\\!C})$, written
$\mathit{WM}^{(\mathit{I\\!C},\mathit{J\\!C})}(P)$, as the least fixed point
of $W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}$.

Whenever clear from context, we keep dropping parentheses and simply write
$\mathit{WM}^{I,J}(P)$ instead of $\mathit{WM}^{(I,J)}(P)$.

In what follows, we use the relativized concepts defined above to delineate
the semantics and resulting simplifications of the sequence of subprograms
resulting from a grounder’s decomposition of the original program. For
simplicity, we first present a theorem capturing the composition under the
well-founded operation, before we give the general case involving a sequence
of programs.

Just like suffix $C$, we use the suffix $E$ (and similarly letter $E$ further
below) to indicate atoms whose defining rules are yet to come.

As in traditional splitting, we begin by differentiating a bottom and a top
program. In addition to the input atoms $(I,J)$ and context atoms in
$(\mathit{I\\!C},\mathit{J\\!C})$, we moreover distinguish a set of external
atoms, $(\mathit{I\\!E},\mathit{J\\!E})$, which occur in the bottom program
but are defined in the top program. Accordingly, the bottom program has to be
evaluated relative to
$(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!E},\mathit{J\\!E})$ (and
not just $(\mathit{I\\!C},\mathit{J\\!C})$ as above) to consider what could be
derived by the top program. Also, observe that our notion of splitting aims at
computing well-founded models rather than stable models.

######  Theorem 16.

Let $\mathit{P\\!B}$ and $\mathit{P\\!T}$ be $\mathcal{F}$-programs,
$(\mathit{I\\!C},\mathit{J\\!C})$ be a four-valued interpretation,
$(I,J)=\mathit{WM}^{\mathit{I\\!C},\mathit{J\\!C}}(\mathit{P\\!B}\cup\mathit{P\\!T})$,
$(\mathit{I\\!E},\mathit{J\\!E})=(I,J)\sqcap({B(\mathit{P\\!B})}^{\pm}\cap
H(\mathit{P\\!T}))$,
$(\mathit{I\\!B},\mathit{J\\!B})=\mathit{WM}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!E},\mathit{J\\!E})}(\mathit{P\\!B})$,
and
$({\mathit{I\\!T}},{\mathit{J\\!T}})=\mathit{WM}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!B},\mathit{J\\!B})}(\mathit{P\\!T})$.

Then, we have
$(I,J)=(\mathit{I\\!B},\mathit{J\\!B})\sqcup({\mathit{I\\!T}},{\mathit{J\\!T}})$.

Partially expanding the statements of the two previous result nicely reflects
the decomposition of the application of the well-founded founded model of a
program:

$\displaystyle\mathit{WM}^{\mathit{I\\!C},\mathit{J\\!C}}(\mathit{P\\!B}\cup\mathit{P\\!T})$
$\displaystyle=\mathit{WM}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!E},\mathit{J\\!E})}(\mathit{P\\!B})\sqcup\mathit{WM}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!B},\mathit{J\\!B})}(\mathit{P\\!T}).$

Note that the formulation of the theorem forms the external interpretation
$(\mathit{I\\!E},\mathit{J\\!E})$, by selecting atoms from the overarching
well-founded model $(I,J)$. This warrants the correspondence of the overall
interpretations to the union of the bottom and top well-founded model. This
global approach is dropped below (after the next example) and leads to less
precise composed models.

######  Example 6.

Let us illustrate the above approach via the following program:

$\displaystyle a$ ($\mathit{P\\!B}$) $\displaystyle b$ ($\mathit{P\\!B}$)
$\displaystyle c$ $\displaystyle\leftarrow a$ ($\mathit{P\\!T}$)
$\displaystyle d$ $\displaystyle\leftarrow{\neg}b$ ($\mathit{P\\!T}$)

The well-founded model of this program relative to
$(\mathit{I\\!C},\mathit{J\\!C})=(\emptyset,\emptyset)$ is

$(I,J)=(\\{a,b,c\\},\\{a,b,c\\}).$

First, we partition the four rules of the program into $\mathit{P\\!B}$ and
$\mathit{P\\!T}$ as given above. We get
$(\mathit{I\\!E},\mathit{J\\!E})=(\emptyset,\emptyset)$ since
${B(\mathit{P\\!B})}^{\pm}\cap H(\mathit{P\\!T})=\emptyset$. Let us evaluate
$\mathit{P\\!B}$ before $\mathit{P\\!T}$. The well-founded model of
$\mathit{P\\!B}$ relative to
$(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!E},\mathit{J\\!E})$ is

$(\mathit{I\\!B},\mathit{J\\!B})=(\\{a,b\\},\\{a,b\\}).$

With this, we calculate the well-founded model of $\mathit{P\\!T}$ relative to
$(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!B},\mathit{J\\!B})$:

$(\mathit{I\\!T},\mathit{J\\!T})=(\\{c\\},\\{c\\}).$

We see that the union of
$(\mathit{I\\!B},\mathit{J\\!B})\sqcup(\mathit{I\\!T},\mathit{J\\!T})$ is the
same as the well-founded model of $\mathit{P\\!B}\cup\mathit{P\\!T}$ relative
to $(\mathit{I\\!C},\mathit{J\\!C})$.

This corresponds to standard splitting in the sense that $\\{a,b\\}$ is a
splitting set for $\mathit{P\\!B}\cup\mathit{P\\!T}$ and $\mathit{P\\!B}$ is
the “bottom” and $\mathit{P\\!T}$ is the “top” [Lifschitz and Turner (1994)].

######  Example 7.

For a complement, let us reverse the roles of programs $\mathit{P\\!B}$ and
$\mathit{P\\!T}$ in Example 6. Unlike above, body atoms in $\mathit{P\\!B}$
now occur in rule heads of $\mathit{P\\!T}$, i.e.,
${B(\mathit{P\\!B})}^{\pm}\cap{H(\mathit{P\\!T})}=\\{a,b\\}$. We thus get
$(\mathit{I\\!E},\mathit{J\\!E})=(\\{a,b\\},\\{a,b\\})$. The well-founded
model of $\mathit{P\\!B}$ relative to
$(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!E},\mathit{J\\!E})$ is

$\displaystyle(\mathit{I\\!B},\mathit{J\\!B})$
$\displaystyle=(\\{c\\},\\{c\\}).$

And the well-founded model of $\mathit{P\\!T}$ relative to
$(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!B},\mathit{J\\!B})$ is

$\displaystyle(\mathit{I\\!T},\mathit{J\\!T})$
$\displaystyle=(\\{a,b\\},\\{a,b\\}).$

Again, we see that the union of both models is identical to $(I,J)$.

This decomposition has no direct correspondence to standard splitting
[Lifschitz and Turner (1994)] since there is no splitting set.

Next, we generalize the previous results from two programs to sequences of
programs. For this, we let $\mathbb{I}$ be a well-ordered index set and direct
our attention to sequences ${({P}_{i})}_{i\in\mathbb{I}}$ of
$\mathcal{F}$-programs.

######  Definition 6.

Let ${({P}_{i})}_{i\in\mathbb{I}}$ be a sequence of $\mathcal{F}$-programs.

We define the _well-founded model_ of ${({P}_{i})}_{i\in\mathbb{I}}$ as

$\displaystyle\mathit{WM}({({P}_{i})}_{i\in\mathbb{I}})$
$\displaystyle=\bigsqcup_{i\in\mathbb{I}}(I_{i},J_{i})$ (2) where
$\displaystyle E_{i}$
$\displaystyle={B({P}_{i})}^{\pm}\cap\bigcup_{i<j}H({P}_{j}),$ (3)
$\displaystyle(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})$
$\displaystyle=\bigsqcup_{j<i}(I_{j},J_{j})\text{, and}$ (4)
$\displaystyle(I_{i},J_{i})$
$\displaystyle=\mathit{WM}^{(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})\sqcup(\emptyset,E_{i})}({P}_{i}).$
(5)

The well-founded model of a program sequence is itself assembled in (2) from a
sequence of well-founded models of the individual subprograms in (5). This
provides us with semantic guidance for successive program simplification, as
shown below. In fact, proceeding along the sequence of subprograms reflects
the iterative approach of a grounding algorithm, one component is grounded at
a time. At each stage $i\in\mathbb{I}$, this takes into account the truth
values of atoms instantiated in previous iterations, viz.
$(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})$, as well as dependencies to upcoming
components in $E_{i}$. Note that unlike Theorem 16, the external atoms in
$E_{i}$ are identified purely syntactically, and the interpretation
$(\emptyset,E_{i})$ treats them as unknown. Grounding is thus performed under
incomplete information and each well-founded model in (5) can be regarded as
an over-approximation of the actual one. This is enabled by the monotonicity
of the well-founded operator in Proposition 15 that only leads to a less
precise result when overestimating its parameter.

Accordingly, the next theorem shows that once we split a program into a
sequence of $\mathcal{F}$-programs, we can iteratively compute an
approximation of the well-founded model by considering in turn each element in
the sequence.

######  Theorem 17.

Let ${({P}_{i})}_{i\in\mathbb{I}}$ be a sequence of $\mathcal{F}$-programs.

Then,
$\mathit{WM}({({P}_{i})}_{i\in\mathbb{I}})\leq_{p}\mathit{WM}(\bigcup_{i\in\mathbb{I}}{P}_{i})$.

The next two results transfer Theorem 17 to program simplification by
successively simplifying programs with the respective well-founded models of
the previous programs.

######  Theorem 18.

Let ${({P}_{i})}_{i\in\mathbb{I}}$ be a sequence of $\mathcal{F}$-programs,
$(I,J)=\mathit{WM}({({P}_{i})}_{i\in\mathbb{I}})$, and $E_{i}$,
$(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})$, and $(I_{i},J_{i})$ be defined as
in 3, 4 and 5.

Then,
${P}_{k}^{I,J}\subseteq{P}_{k}^{(\mathit{I\\!C}_{k},\mathit{J\\!C}_{k})\sqcup(I_{k},J_{k})\sqcup(\emptyset,E_{k})}\subseteq{P}_{k}$
for all $k\in\mathbb{I}$.

######  Corollary 19.

Let ${({P}_{i})}_{i\in\mathbb{I}}$ be a sequence of $\mathcal{R}$-programs,
and $E_{i}$, $(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})$, and $(I_{i},J_{i})$ be
defined as in 3, 4 and 5.

Then, $\bigcup_{i\in\mathbb{I}}{{P}_{i}}$ and
$\bigcup_{i\in\mathbb{I}}{P}_{i}^{(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})\sqcup(I_{i},J_{i})\sqcup(\emptyset,E_{i})}$
have the same well-founded and stable models.

Let us mention that the previous result extends to sequences of
$\mathcal{F}$-programs and their well-founded models but not their stable
models.

######  Example 8.

To illustrate Theorem 17, let us consider the following programs, ${P}_{1}$
and ${P}_{2}$:

$\displaystyle a$ $\displaystyle\leftarrow{\neg}c$ (${P}_{1}$) $\displaystyle
b$ $\displaystyle\leftarrow{\neg}d$ (${P}_{1}$) $\displaystyle c$
$\displaystyle\leftarrow{\neg}b$ (${P}_{2}$) $\displaystyle d$
$\displaystyle\leftarrow e$ (${P}_{2}$)

The well-founded model of ${P}_{1}\cup{P}_{2}$ is

$(I,J)=(\\{a,b\\},\\{a,b\\}).$

Let us evaluate ${P}_{1}$ before ${P}_{2}$. While no head literals of
${P}_{2}$ occur positively in ${P}_{1}$, the head literals $c$ and $d$ of
${P}_{2}$ occur negatively in rule bodies of ${P}_{1}$. Hence, we get
$E_{1}=\\{c,d\\}$ and treat both atoms as unknown while calculating the well-
founded model of ${P}_{1}$ relative to $(\emptyset,\\{c,d\\})$:

$(I_{1},J_{1})=(\emptyset,\\{a,b\\}).$

We obtain that both $a$ and $b$ are unknown. With this and $E_{2}=\emptyset$,
we can calculate the well-founded model of ${P}_{2}$ relative to
$(I_{1},J_{1})$:

$(I_{2},J_{2})=(\emptyset,\\{c\\}).$

We see that because $a$ is unknown, we have to derive $c$ as unknown, too. And
because there is no rule defining $e$, we cannot derive $d$. Hence,
$(I_{1},J_{1})\sqcup(I_{2},J_{2})$ is less precise than $(I,J)$ because, when
evaluating ${P}_{1}$, it is not yet known that $c$ is true and $d$ is false.

Next, we illustrate the simplified programs according to Theorem 18:

$\displaystyle a$ $\displaystyle\leftarrow{\neg}c$ $\displaystyle a$
$\displaystyle\leftarrow{\neg}c$ (${P}_{1}$) $\displaystyle b$
$\displaystyle\leftarrow{\neg}d$ $\displaystyle b$
$\displaystyle\leftarrow{\neg}d$ (${P}_{1}$) $\displaystyle c$
$\displaystyle\leftarrow{\neg}b$ (${P}_{2}$)

The left column contains the simplification of ${P}_{1}\cup{P}_{2}$ w.r.t.
$(I,J)$ and the right column the simplification of ${P}_{1}$ w.r.t.
$(I_{1},J_{1})$ and ${P}_{2}$ w.r.t. $(I_{1},J_{1})\sqcup(I_{2},J_{2})$. Note
that $d\leftarrow e$ has been removed in both columns because $e$ is false in
both $(I,J)$ and $(I_{1},J_{1})\sqcup(I_{2},J_{2})$. But we can only remove
$c\leftarrow{\neg}b$ from the left column because, while $b$ is false in
$(I,J)$, it is unknown in $(I_{1},J_{1})\sqcup(I_{2},J_{2})$.

Finally, observe that in accordance with Theorems 9, 10 and 19, the program
${P}_{1}\cup{P}_{2}$ and the two simplified programs have the same stable and
well-founded models.

Clearly, the best simplifications are obtained when simplifying with the
actual well-founded model of the overall program. This can be achieved for a
sequence as well whenever $E_{i}$ is empty, that is, if there is no need to
approximate the impact of upcoming atoms.

######  Corollary 20.

Let ${({P}_{i})}_{i\in\mathbb{I}}$ be a sequence of $\mathcal{F}$-programs and
$E_{i}$ be defined as in 3.

If $E_{i}=\emptyset$ for all $i\in\mathbb{I}$ then
$\mathit{WM}({({P}_{i})}_{i\in\mathbb{I}})=\mathit{WM}(\bigcup_{i\in\mathbb{I}}{P}_{i})$.

######  Corollary 21.

Let ${({P}_{i})}_{i\in\mathbb{I}}$ be a sequence of $\mathcal{F}$-programs,
$(I,J)=\mathit{WM}({({P}_{i})}_{i\in\mathbb{I}})$, and $E_{i}$,
$(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})$, and $(I_{i},J_{i})$ be defined as
in 3, 4 and 5.

If $E_{i}=\emptyset$ for all $i\in\mathbb{I}$, then
${P}_{k}^{I,J}={P}_{k}^{(\mathit{I\\!C}_{k},\mathit{J\\!C}_{k})\sqcup(I_{k},J_{k})}$
for all $k\in\mathbb{I}$.

######  Example 9.

Next, let us illustrate Corollary 20 on an example. We take the same rules as
in Example 8 but use a different sequence:

$\displaystyle d$ $\displaystyle\leftarrow e$ (${P}_{1}$) $\displaystyle b$
$\displaystyle\leftarrow{\neg}d$ (${P}_{1}$) $\displaystyle c$
$\displaystyle\leftarrow{\neg}b$ (${P}_{2}$) $\displaystyle a$
$\displaystyle\leftarrow{\neg}c$ (${P}_{2}$)

Observe that the head literals of ${P}_{2}$ do not occur in the bodies of
${P}_{1}$, i.e., $E_{1}={B({P}_{1})}^{\pm}\cap{H({P}_{2})}=\emptyset$. The
well-founded model of ${P}_{1}$ is

$\displaystyle(I_{1},J_{1})$ $\displaystyle=(\\{b\\},\\{b\\}).$

And the well-founded model of ${P}_{2}$ relative to $(\\{b\\},\\{b\\})$ is

$\displaystyle(I_{2},J_{2})$ $\displaystyle=(\\{a\\},\\{a\\}).$

Hence, the union of both models is identical to the well-founded model of
${P}_{1}\cup{P}_{2}$.

Next, we investigate the simplified program according to Corollary 21:

$\displaystyle b$ $\displaystyle\leftarrow{\neg}d$ (${P}_{1}$) $\displaystyle
a$ $\displaystyle\leftarrow{\neg}c$ (${P}_{2}$)

As in Example 8, we delete rule $d\leftarrow e$ because $e$ is false in
$(I_{1},J_{1})$. But this time, we can also remove rule $c\leftarrow{\neg}b$
because $b$ is true in $(I_{1},J_{1})\sqcup(I_{2},J_{2})$.

##  4 Aggregate programs

We now turn to programs with aggregates and, at the same time, to programs
with variables. That is, we now deal with finite nonground programs whose
instantiation may lead to infinite ground programs including infinitary
subformulas. This is made precise by haliya14a and gehakalisc15a where
aggregate programs are associated with infinitary propositional formulas
[Truszczyński (2012)]. However, the primary goal of grounding is to produce a
finite set of ground rules with finitary subformulas only. In fact, the
program simplification introduced in Section 2.5 allows us to produce an
equivalent finite ground program whenever the well-founded model is finite.
The source of infinitary subformulas lies in the instantiation of aggregates.
We address this below by introducing an aggregate translation bound by an
interpretation that produces finitary formulas whenever this interpretation is
finite. Together, our concepts of program simplification and aggregate
translation provide the backbone for turning programs with aggregates into
semantically equivalent finite programs with finitary subformulas.

Our concepts follow the ones of gehakalisc15a; the semantics of aggregates is
aligned with that of ferraris11a yet lifted to infinitary formulas
[Truszczyński (2012), Harrison et al. (2014)].

We consider a _signature_ $\Sigma=(\mathcal{F},\mathcal{P},\mathcal{V})$
consisting of sets of function, predicate, and variable symbols. The sets of
variable and function symbols are disjoint. _Function_ and _predicate symbols_
are associated with non-negative arities. For short, a predicate symbol $p$ of
arity $n$ is also written as $p/n$. In the following, we use lower case
strings for function and predicate symbols, and upper case strings for
variable symbols. Also, we often drop the term ‘symbol’ and simply speak of
functions, predicates, and variables.

As usual, _terms_ over $\Sigma$ are defined inductively as follows:

  * •

$v\in\mathcal{V}$ is a term and

  * •

$f(t_{1},\dots,t_{n})$ is a term if $f\in\mathcal{F}$ is a function symbol of
arity $n$ and each $t_{i}$ is a term over $\Sigma$.

Parentheses for terms over function symbols of arity 0 are omitted.

Unless stated otherwise, we assume that the set of (zero-ary) functions
includes a set of numeral symbols being in a one-to-one correspondence to the
integers. For simplicity, we drop this distinction and identify numerals with
the respective integers.

An _atom_ over signature $\Sigma$ has form $p(t_{1},\dots,t_{n})$ where
$p\in\mathcal{P}$ is a predicate symbol of arity $n$ and each $t_{i}$ is a
term over $\Sigma$. As above, parentheses for atoms over predicate symbols of
arity 0 are omitted. Given an atom $a$ over $\Sigma$, a _literal_ over
$\Sigma$ is either the atom itself or its negation ${\neg}a$. A literal
without negation is called _positive_ , and _negative_ otherwise.

A _comparison_ over $\Sigma$ has form

$\displaystyle t_{1}\prec t_{2}$ (6)

where $t_{1}$ and $t_{2}$ are terms over $\Sigma$ and $\prec$ is a relation
symbol among $<$, $\leq$, $>$, $\geq$, $=$, and $\neq$.

An _aggregate element_ over $\Sigma$ has form

$\displaystyle t_{1},\dots,t_{m}$ $\displaystyle:a_{1}\wedge\dots\wedge a_{n}$
(7)

where $t_{i}$ is a term and $a_{j}$ is an atom, both over $\Sigma$ for $0\leq
i\leq m$ and $0\leq j\leq n$. The terms $t_{1},\dots,t_{m}$ are seen as a
tuple, which is empty for $m=0$; the conjunction $a_{1}\wedge\dots\wedge
a_{n}$ is called the _condition_ of the aggregate element. For an aggregate
element $e$ of form (7), we use $H(e)=(t_{1},\dots,t_{m})$ and
$B(e)=\\{a_{1},\dots,a_{n}\\}$. We extend both to sets of aggregate elements
in the straightforward way, that is, $H(E)=\\{H(e)\mid e\in E\\}$ and
$B(E)=\\{B(e)\mid e\in E\\}$.

An _aggregate atom_ over $\Sigma$ has form

$\displaystyle f\\{e_{1},\dots,e_{n}\\}\prec s$ (8)

where $n\geq 0$, $f$ is an aggregate name among $\mathrm{\\#count}$,
$\mathrm{\\#sum}$, $\mathrm{\\#sum}^{+}$, and $\mathrm{\\#sum}^{-}$, each
$e_{i}$ is an aggregate element, $\prec$ is a relation symbol among $<$,
$\leq$, $>$, $\geq$, $=$, and $\neq$ (as above), and $s$ is a term
representing the aggregate’s _bound_.

Without loss of generality, we refrain from introducing negated aggregate
atoms.555Grounders like lparse and gringo replace aggregates systematically by
auxiliary atoms and place them in the body of new rules implying the
respective auxiliary atom. This results in programs without occurrences of
negated aggregates. We often refer to aggregate atoms simply as aggregates.

An _aggregate program_ over $\Sigma$ is a finite set of _aggregate rules_ of
form

$\displaystyle h$ $\displaystyle\leftarrow b_{1}\wedge\dots\wedge b_{n}$

where $n\geq 0$, $h$ is an atom over $\Sigma$ and each $b_{i}$ is either a
literal, a comparison, or an aggregate over $\Sigma$. We refer to
$b_{1},\dots,b_{n}$ as body literals, and extend functions $H(r)$ and $B(r)$
to any aggregate rule $r$.

######  Example 10.

An example for an aggregate program is shown below, giving an encoding of the
_Company Controls Problem_ [Mumick et al. (1990)]: A company $X$ controls a
company $Y$ if $X$ directly or indirectly controls more than 50% of the shares
of $Y$.

$\displaystyle\mathit{controls}(X,Y)\leftarrow{}$
$\displaystyle\\!\begin{aligned}
\mathrm{\\#sum}^{+}\\{&S:\mathit{owns}(X,Y,S);\\\
&S,Z:\mathit{controls}(X,Z)\wedge\mathit{owns}(Z,Y,S)\\}>50\end{aligned}$
$\displaystyle{}\wedge{}$
$\displaystyle\mathit{company}(X)\wedge\mathit{company}(Y)\wedge X\neq Y$

The aggregate $\mathrm{\\#sum}^{+}$ implements summation over positive
integers. Notably, it takes part in the recursive definition of predicate
$\mathit{controls}$. In the following, we use an instance with ownership
relations between four companies:

$\displaystyle\mathit{company}(c_{1})$ $\displaystyle\mathit{company}(c_{2})$
$\displaystyle\mathit{company}(c_{3})$ $\displaystyle\mathit{company}(c_{4})$
$\displaystyle\mathit{owns}(c_{1},c_{2},60)$
$\displaystyle\mathit{owns}(c_{1},c_{3},20)$
$\displaystyle\mathit{owns}(c_{2},c_{3},35)$
$\displaystyle\mathit{owns}(c_{3},c_{4},51)$

We say that an aggregate rule $r$ is _normal_ if its body does not contain
aggregates. An aggregate program is normal if all its rules are normal.

A term, literal, aggregate element, aggregate, rule, or program is _ground_
whenever it does not contain any variables.

We assume that all ground terms are totally ordered by a relation $\leq$,
which is used to define the relations $<$, $>$, $\geq$, $=$, and $\neq$ in the
standard way. For ground terms $t_{1},t_{2}$ and a corresponding relation
symbol $\prec$, we say that $\prec$ holds between $t_{1}$ and $t_{2}$ whenever
the corresponding relation holds between $t_{1}$ and $t_{2}$. Furthermore,
$>$, $\geq$, and $\neq$ hold between $\infty$ and any other term, and $<$,
$\leq$, and $\neq$ hold between $-\infty$ and any other term. Finally, we
require that integers are ordered as usual.

For defining sum-based aggregates, we define for a tuple $t=t_{1},\dots,t_{m}$
of ground terms the following weight functions:

$\displaystyle w(t)$ $\displaystyle=\begin{cases}t_{1}&\text{if $m>0$ and
$t_{1}$ is an integer}\\\ 0&\text{otherwise,}\\\ \end{cases}$ $\displaystyle
w^{+}(t)$ $\displaystyle=\max\\{w(t),0\\}\text{, and}$ $\displaystyle
w^{-}(t)$ $\displaystyle=\min\\{w(t),0\\}.$

With this at hand, we now define how to apply aggregate functions to sets of
tuples of ground terms in analogy to gehakalisc15a.

######  Definition 7.

Let $T$ be a set of tuples of ground terms.

We define

$\displaystyle\mathrm{\\#count}(T)$ $\displaystyle=\begin{cases}|T|&\text{if
$T$ is finite},\\\ \infty&\text{otherwise},\end{cases}$
$\displaystyle\mathrm{\\#sum}(T)$ $\displaystyle=\begin{cases}\Sigma_{t\in
T}w(t)&\text{if $\\{t\in T\mid w(t)\neq 0\\}$ is finite,}\\\
0&\text{otherwise},\end{cases}$ $\displaystyle\mathrm{\\#sum}^{+}(T)$
$\displaystyle=\begin{cases}\Sigma_{t\in T}w^{+}(t)&\text{if $\\{t\in T\mid
w(t)>0\\}$ is finite,}\\\ \infty&\text{otherwise, and}\end{cases}$
$\displaystyle\mathrm{\\#sum}^{-}(T)$ $\displaystyle=\begin{cases}\Sigma_{t\in
T}w^{-}(t)&\text{if $\\{t\in T\mid w(t)<0\\}$ is finite,}\\\
-\infty&\text{otherwise.}\end{cases}$

Note that in our setting the application of aggregate functions to infinite
sets of ground terms is of theoretical relevance only, since we aim at
reducing them to their finite equivalents so that they can be evaluated by a
grounder.

A variable is _global_ in

  * •

a literal if it occurs in the literal,

  * •

a comparison if it occurs in the comparison,

  * •

an aggregate if it occurs in its bound, and

  * •

a rule if it is global in its head atom or in one of its body literals.

For example, the variables $X$ and $Y$ are global in the aggregate rule in
Example 10, while $Z$ and $S$ are neither global in the rule nor the
aggregate.

######  Definition 8.

Let $r$ be an aggregate rule.

We define $r$ to be _safe_

  * •

if all its global variables occur in some positive literal in the body of $r$
and

  * •

if all its non-global variables occurring in an aggregate element $e$ of an
aggregate in the body of $r$, also occur in some positive literal in the
condition of $e$.

For instance, the aggregate rule in Example 10 is safe.

Note that comparisons are disregarded in the definition of safety. That is,
variables in comparisons have to occur in positive body literals.666In fact,
gringo allows for variables in some comparisons to guarantee safety, as
detailed in Section 7.3.

An aggregate program is safe if all its rules are safe.

An _instance_ of an aggregate rule $r$ is obtained by substituting ground
terms for all its global variables. We use $\mathrm{Inst}(r)$ to denote the
set of all instances of $r$ and $\mathrm{Inst}(P)$ to denote the set of all
ground instances of rules in aggregate program $P$. An _instance_ of an
aggregate element $e$ is obtained by substituting ground terms for all its
variables. We let $\mathrm{Inst}(E)$ stand for all instances of aggregate
elements in a set $E$. Note that $\mathrm{Inst}(E)$ consists of ground
expressions, which is not necessarily the case for $\mathrm{Inst}(r)$. As seen
from the first example in the introductory section, both $\mathrm{Inst}(r)$
and $\mathrm{Inst}(E)$ can be infinite.

A literal, aggregate element, aggregate, or rule is _closed_ if it does not
contain any global variables.

For example, the following rule is an instance of the aggregate rule in
Example 10.

$\displaystyle\mathit{controls}(c_{1},c_{2})\leftarrow{}$
$\displaystyle\\!\begin{aligned}
\mathrm{\\#sum}^{+}\\{&S:\mathit{owns}(c_{1},c_{2},S);\\\
&S,Z:\mathit{controls}(c_{1},Z),\mathit{owns}(Z,c_{2},S)\\}>50\end{aligned}$
$\displaystyle{}\wedge{}$
$\displaystyle\mathit{company}(c_{1})\wedge\mathit{company}(c_{2})\wedge
c_{1}\neq c_{2}$

Note that both the rule and its aggregate are closed. It is also noteworthy to
realize that the two elements of the aggregate induce an infinite set of
instances, among them

$\displaystyle 20$ $\displaystyle:\mathit{owns}(c_{1},c_{2},20)$ and
$\displaystyle 35,c_{2}$
$\displaystyle:\mathit{controls}(c_{1},c_{2}),\mathit{owns}(c_{2},c_{3},35).$

We now turn to the semantics of aggregates as introduced by ferraris11a but
follow its adaptation to closed aggregates by gehakalisc15a: Let $a$ be a
closed aggregate of form (8) and $E$ be its set of aggregate elements. We say
that a set $D\subseteq\mathrm{Inst}(E)$ of its elements’ instances _justifies_
$a$, written $D\triangleright a$, if $f(H(D))\prec s$ holds.

An aggregate $a$ is _monotone_ whenever $D_{1}\triangleright a$ implies
$D_{2}\triangleright a$ for all $D_{1}\subseteq
D_{2}\subseteq\mathrm{Inst}(E)$, and accordingly $a$ is _antimonotone_ if
$D_{2}\triangleright a$ implies $D_{1}\triangleright a$ for all
$D_{1}\subseteq D_{2}\subseteq\mathrm{Inst}(E)$.

We observe the following monotonicity properties.

######  Proposition 22 (haliya14a).

  * •

Aggregates over functions $\mathrm{\\#sum}^{+}$ and $\mathrm{\\#count}$
together with relations $>$ and $\geq$ are monotone.

  * •

Aggregates over functions $\mathrm{\\#sum}^{+}$ and $\mathrm{\\#count}$
together with relations $<$ and $\leq$ are antimonotone.

  * •

Aggregates over function $\mathrm{\\#sum}^{-}$ have the same monotonicity
properties as $\mathrm{\\#sum}^{+}$ aggregates with the complementary
relation.

Next, we give the translation $\tau$ from aggregate programs to
$\mathcal{R}$-programs, derived from the ones of ferraris11a and haliya14a:

For a closed literal $l$, we have

$\displaystyle\tau(l)$ $\displaystyle=l\text{,}$ for a closed comparison $l$
of form (6), we have $\displaystyle\tau(l)$
$\displaystyle=\begin{cases}\top&\text{if $\prec$ holds between $t_{1}$ and
$t_{2}$}\\\ \bot&\text{otherwise}\end{cases}$ and for a set $L$ of closed
literals, comparisons and aggregates, we have $\displaystyle\tau(L)$
$\displaystyle={\\{\tau(l)\mid l\in L\\}}\text{.}$ For a closed aggregate $a$
of form (8) and its set $E$ of aggregate elements, we have
$\displaystyle\tau(a)$
$\displaystyle={\\{\tau(D)^{\wedge}\rightarrow\tau_{a}(D)^{\vee}\mid
D\subseteq\mathrm{Inst}(E),D\mathrel{\not\kern-1.0pt\triangleright}a\\}}^{\wedge}$
(9) where $\displaystyle\tau_{a}(D)$
$\displaystyle=\tau(\mathrm{Inst}(E)\setminus D)\text{\ for
$D\subseteq\mathrm{Inst}(E)$,}$ $\displaystyle\tau(D)$
$\displaystyle={\\{\tau(e)\mid e\in D\\}}\text{\ for
$D\subseteq\mathrm{Inst}(E)$, and}$ $\displaystyle\tau(e)$
$\displaystyle={\tau(B(e))}^{\wedge}\text{\ for $e\in\mathrm{Inst}(E)$}.$ For
a closed aggregate rule $r$, we have $\displaystyle\tau(r)$
$\displaystyle=\tau(H(r))\leftarrow\tau(B(r))^{\wedge}.$ For an aggregate
program $P$, we have $\displaystyle\tau(P)$ $\displaystyle=\\{\tau(r)\mid
r\in\mathrm{Inst}(P)\\}.$ (10)

While aggregate programs like $P$ are finite sets of (non-ground) rules,
$\tau(P)$ can be infinite and contain (ground) infinitary expressions. Observe
that $\tau(P)$ is an $\mathcal{R}$-program. In fact, only the translation of
aggregates introduces $\mathcal{R}$-formulas; rules without aggregates form
$\mathcal{N}$-programs.

######  Example 11.

To illustrate Ferraris’ approach to the semantics of aggregates, consider a
count aggregate $a$ of form

$\displaystyle\mathrm{\\#count}\\{X:p(X)\\}\geq n.$

Since the aggregate is non-ground, the set $G$ of its element’s instances
consists of all $t:p(t)$ for each ground term $t$.

The count aggregate cannot be justified by any subset $D$ of $G$ satisfying
$|\\{t\mid t:p(t)\in D\\}|<n$, or $D\mathrel{\not\kern-1.0pt\triangleright}a$
for short. Accordingly, we have that $\tau(a)$ is the conjunction of all
formulas

$\displaystyle{\\{p(t)\mid t:p(t)\in D\\}}^{\wedge}$
$\displaystyle\rightarrow{\\{p(t)\mid t:p(t)\in(G\setminus D)\\}}^{\vee}$ (11)

such that $D\subseteq G$ and $D\mathrel{\not\kern-1.0pt\triangleright}a$.
Restricting the set of ground terms to the numerals $1,2,3$ and letting $n=2$
results in the formulas

$\displaystyle\top$ $\displaystyle\rightarrow p(1)\vee p(2)\vee p(3),$
$\displaystyle p(1)$ $\displaystyle\rightarrow p(2)\vee p(3),$ $\displaystyle
p(2)$ $\displaystyle\rightarrow p(1)\vee p(3),\text{\ and\ }$ $\displaystyle
p(3)$ $\displaystyle\rightarrow p(1)\vee p(2).$

Note that a smaller number of ground terms than $n$ yields an unsatisfiable
set of formulas.

However, it turns out that a Ferraris-style translation of aggregates
[Ferraris (2011), Harrison et al. (2014)] is too weak for propagating monotone
aggregates in our id-based setting. That is, when propagating possible atoms
(i.e., the second component of the well-founded model), an id-reduct may
become satisfiable although the original formula is not. So, we might end up
with too many possible atoms and a well-founded model that is not as precise
as it could be. To see this, consider the following example.

######  Example 12.

For some $m,n\geq 0$, the program ${P}_{m,n}$ consists of the following rules:

$\displaystyle p(i)$ $\displaystyle\leftarrow{\neg}q(i)$ $\displaystyle\text{\
for\ }1\leq i\leq m$ $\displaystyle q(i)$ $\displaystyle\leftarrow{\neg}p(i)$
$\displaystyle\text{\ for\ }1\leq i\leq m$ $\displaystyle r$
$\displaystyle\leftarrow\mathrm{\\#count}\\{X:p(X)\\}\geq n$

Given the ground instances $G$ of the aggregate’s elements and some two-valued
interpretation $I$, observe that

$\displaystyle\tau(\mathrm{\\#count}\\{X:p(X)\\}\geq n)_{I}$ is classically
equivalent to $\displaystyle\tau(\mathrm{\\#count}\\{X:p(X)\\}\geq
n)_{I}\vee{\\{p(t)\in B(G)\mid p(t)\notin I\\}}^{\vee}.$ (12)

To see this, observe that the formula obtained via $\tau$ for the aggregate in
the last rule’s body consists of positive occurrences of implications of the
form $\mathcal{G}^{\wedge}\rightarrow\mathcal{H}^{\vee}$ where either
$p(t)\in\mathcal{G}$ or $p(t)\in\mathcal{H}$. The id-reduct makes all such
implications with some $p(t)\in\mathcal{G}$ such that $p(t)\notin I$ true
because their antecedent is false. All of the remaining implications in the
id-reduct are equivalent to $\mathcal{H}^{\vee}$ where $\mathcal{H}$ contains
all $p(t)\notin I$. Thus, we can factor out the formula on the right-hand side
of (12).

Next, observe that for $1\leq m<n$, the four-valued interpretation
$(I,J)=(\emptyset,H(\tau({P}_{m,n})))$ is the well-founded model of
${P}_{m,n}$:

$\displaystyle S_{\tau({P}_{m,n})}(J)$ $\displaystyle=I\text{\ and}$
$\displaystyle S_{\tau({P}_{m,n})}(I)$ $\displaystyle=J.$

Ideally, atom $r$ should not be among the possible atoms because it can never
be in a stable model. Nonetheless, it is due to the second disjunct in (12).

Note that not just monotone aggregates exhibit this problem. In general, we
get for a closed aggregate $a$ with elements $E$ and an interpretation $I$
that

$\displaystyle\tau(a)_{I}\text{\ is classically equivalent to\
}\tau(a)_{I}\vee{\\{c\in B(\mathrm{Inst}(E))\mid I\not\models c\\}}^{\vee}.$

The second disjunct is undesirable when propagating possible atoms.

To address this shortcoming, we augment the aggregate translation so that it
provides stronger propagation. The result of the augmented translation is
strongly equivalent to that of the original translation (cf. Proposition 23).
Thus, even though we get more precise well-founded models, the stable models
are still contained in them.

######  Definition 9.

We define $\pi$ as the translation obtained from $\tau$ by replacing the case
of closed aggregates in (9) by the following:

For a closed aggregate $a$ of form (8) and its set $E$ of aggregate elements,
we have

$\displaystyle\pi(a)$
$\displaystyle={\\{{\tau(D)}^{\wedge}\rightarrow{\pi_{a}}(D)^{\vee}\mid
D\subseteq\mathrm{Inst}(E),D\mathrel{\not\kern-1.0pt\triangleright}a\\}}^{\wedge}$
where $\displaystyle{\pi_{a}}(D)$ $\displaystyle=\\{{\tau(C)}^{\wedge}\mid
C\subseteq\mathrm{Inst}(E)\setminus D,C\cup D\triangleright a\\}\text{\ for\
}D\subseteq\mathrm{Inst}(E).$

Note that just as $\tau$ also $\pi$ is recursively applied to the whole
program.

Let us illustrate the modified translation by revisiting Example 11.

######  Example 13.

Let us reconsider the count aggregate $a$:

$\displaystyle\mathrm{\\#count}\\{X:p(X)\\}\geq n$

As with $\tau(a)$ in Example 11, $\pi(a)$ yields a conjunction of formulas,
one conjunct for each set $D\subseteq\mathrm{Inst}(E)$ satisfying
$D\mathrel{\not\kern-1.0pt\triangleright}a$ of the form:

$\displaystyle{\\{B(e)\mid e\in
D\\}}^{\wedge}\rightarrow{\big{\\{}{\\{B(e)\mid e\in(C\setminus
D)\\}}^{\wedge}\mid C\triangleright a,D\subseteq
C\subseteq\mathrm{Inst}(E)\big{\\}}}^{\vee}$ (13)

Restricting again the set of ground terms to the numerals $1,2,3$ and letting
$n=2$ results now in the formulas

$\displaystyle\top$ $\displaystyle\rightarrow(p(1)\wedge p(2))\vee(p(1)\wedge
p(3))\vee(p(2)\wedge p(3))\vee(p(1)\wedge p(2)\wedge p(3)),$ $\displaystyle
p(1)$ $\displaystyle\rightarrow p(2)\vee p(3)\vee(p(2)\wedge p(3)),$
$\displaystyle p(2)$ $\displaystyle\rightarrow p(1)\vee p(3)\vee(p(1)\wedge
p(3)),\text{\ and\ }$ $\displaystyle p(3)$ $\displaystyle\rightarrow p(1)\vee
p(2)\vee(p(1)\wedge p(2)).$

Note that the last disjunct can be dropped from each rule’s consequent. And as
above, a smaller number of ground terms than $n$ yields an unsatisfiable set
of formulas.

The next result ensures that $\tau(P)$ and $\pi(P)$ have the same stable
models for any aggregate program $P$.

######  Proposition 23.

Let $a$ be a closed aggregate.

Then, $\tau(a)$ and $\pi(a)$ are strongly equivalent.

The next example illustrates that we get more precise well-founded models
using the strongly equivalent refined translation.

######  Example 14.

Reconsider Program ${P}_{m,n}$ from Example 12.

As above, we apply the well-founded operator to program ${P}_{m,n}$ for $m<n$
and four-valued interpretation $(I,J)=(\emptyset,H(\pi({P}_{m,n})))$:

$\displaystyle S_{\pi({P}_{m,n})}(J)$ $\displaystyle=I\text{\ and\ }$
$\displaystyle S_{\pi({P}_{m,n})}(I)$ $\displaystyle=J\setminus\\{r\\}.$

Unlike before, $r$ is now found to be false since it does not belong to
$S_{\pi({P}_{m,n})}(\emptyset)$.

To see this, we can take advantage of the following proposition.

######  Proposition 24.

Let $a$ be a closed aggregate.

If $a$ is monotone, then $\pi(a)_{I}$ is classically equivalent to $\pi(a)$
for any two-valued interpretation $I$.

Note that $\pi(a)$ is a negative formula whenever $a$ is antimonotone; cf.
Proposition 36.

Let us briefly return to Example 14. We now observe that $\pi(a)_{I}=\pi(a)$
for $a=\mathrm{\\#count}\\{X:p(X)\\}\geq n$ and any interpretation $I$ in view
of the last proposition. Hence, our refined translation $\pi$ avoids the
problematic disjunct in 12 on the right. By Proposition 23, we can use
$\pi({P}_{m,n})$ instead of $\tau({P}_{m,n})$; both formulas have the same
stable models.

Using Proposition 24, we augment the translation $\pi$ to replace monotone
aggregates $a$ by the strictly positive formula $\pi(a)_{\emptyset}$. That is,
we only keep the implication with the trivially true antecedent in the
aggregate translation (cf. Section 5).

While $\pi$ improves on propagation, it may still produce infinitary
$\mathcal{R}$-formulas when applied to aggregates. This issue is addressed by
restricting the translation to a set of (possible) atoms.

######  Definition 10.

Let $J$ be a two-valued interpretation. We define the translation $\pi_{J}$ as
the one obtained from $\tau$ by replacing the case of closed aggregates in (9)
by the following:

For a closed aggregate $a$ of form (8) and its set $E$ of aggregate elements,
we have

$\displaystyle\pi_{J}(a)$
$\displaystyle={\\{\tau(D)^{\wedge}\rightarrow\pi_{a,J}(D)^{\vee}\mid
D\subseteq\mathrm{Inst}(E)|_{J},D\mathrel{\not\kern-1.0pt\triangleright}a\\}}^{\wedge}$
where $\displaystyle\pi_{a,J}(D)$ $\displaystyle={\\{\tau(C)^{\wedge}\mid
C\subseteq\mathrm{Inst}(E)|_{J}\setminus D,C\cup D\triangleright a\\}}\text{\
and\ }$ $\displaystyle\mathrm{Inst}(E)|_{J}$
$\displaystyle=\\{e\in\mathrm{Inst}(E)\mid B(e)\subseteq J\\}.$

Note that ${\pi_{J}}(a)$ is a finitary formula whenever $J$ is finite.

Clearly, $\pi_{J}$ also conforms to $\pi$ except for the restricted
translation for aggregates defined above. The next proposition elaborates this
by showing that $\pi_{J}$ and $\pi$ behave alike whenever $J$ limits the set
of possible atoms.

######  Theorem 25.

Let $a$ be a closed aggregate, and $I\subseteq J$ and $X\subseteq J$ be two-
valued interpretations.

Then,

  1. (a)

$X\models\pi(a)$ iff $X\models\pi_{J}(a)$,

  2. (b)

$X\models\pi(a)_{I}$ iff $X\models\pi_{J}(a)_{I}$, and

  3. (c)

$X\models\pi(a)^{I}$ iff $X\models\pi_{J}(a)^{I}$.

In view of Proposition 23, this result extends to Ferraris’ original aggregate
translation [Ferraris (2011), Harrison et al. (2014)].

The next example illustrates how a finitary formula can be obtained for an
aggregate, despite a possibly infinite set of terms in the signature.

######  Example 15.

Let ${P}_{m,n}$ be the program from Example 12. The well-founded model $(I,J)$
of $\pi({P}_{m,n})$ is $(\emptyset,H(\pi({P}_{m,n})))$ if $n\leq m$.

The translation ${\pi_{J}}({P}_{3,2})$ consists of the rules

$\displaystyle p(1)$ $\displaystyle\leftarrow{\neg}q(1),$ $\displaystyle q(1)$
$\displaystyle\leftarrow{\neg}p(1),$ $\displaystyle p(2)$
$\displaystyle\leftarrow{\neg}q(2),$ $\displaystyle q(2)$
$\displaystyle\leftarrow{\neg}p(2),$ $\displaystyle p(3)$
$\displaystyle\leftarrow{\neg}q(3),$ $\displaystyle q(3)$
$\displaystyle\leftarrow{\neg}p(3),\text{\ and\ }$ $\displaystyle r$
${}\leftarrow{\pi_{J}}(\mathrm{\\#count}\\{X:p(X)\\}\geq 2)$

where the aggregate translation corresponds to the conjunction of the formulas
in Example 13. Note that the translation $\pi({P}_{3,2})$ depends on the
signature whereas the translation ${\pi_{J}}({P}_{3,2})$ is fixed by the atoms
in $J$.

Importantly, Theorem 25 shows that given a finite (approximation of the) well-
founded model of an $\mathcal{R}$-program, we can replace aggregates with
finitary formulas. Moreover, in this case, Theorem 9 and Proposition 23
together indicate how to turn a program with aggregates into a semantically
equivalent finite $\mathcal{R}$-program with finitary formulas as bodies. That
is, given a finite well-founded model of an $\mathcal{R}$-program, the program
simplification from Definition 1 results in a finite program and the aggregate
translation from Definition 10 produces finitary formulas only.

This puts us in a position to outline how and when (safe non-ground) aggregate
programs can be turned into equivalent finite ground programs consisting of
finitary subformulas only. To this end, consider an aggregate program $P$
along with the well-founded model $(I,J)$ of $\pi(P)$. We have already seen in
Corollary 10 that $\pi(P)$ and its simplification $\pi(P)^{I,J}$ have the same
stable models, just like $\pi(P)^{I,J}$ and its counterpart
${\pi_{J}}(P)^{I,J}$ in view of Theorem 25.

Now, if $(I,J)$ is finite, then $\pi(P)^{I,J}$ is finite, too. Seen from the
perspective of grounding, the safety of all rules in $P$ implies that all
global variables appear in positive body literals. Thus, the number of ground
instances of each rule in $\pi(P)^{I,J}$ is determined by the number of
possible substitutions for its global variables. Clearly, there are only
finitely many possible substitutions such that all positive body literals are
satisfied by a finite interpretation $J$ (cf. Definition 1). Furthermore, if
$J$ is finite, aggregate translations in ${\pi_{J}}(P)^{I,J}$ introduce
finitary subformulas only. Thus, in this case, we obtain from $P$ a finite set
of rules with finitary propositional formulas as bodies, viz.
${\pi_{J}}(P)^{I,J}$, that has the same stable models as $\pi(P)$ (as well as
$\tau(P)$, the traditional Ferraris-style semantics of $P$ [Ferraris (2011),
Harrison et al. (2014)]).

An example of a class of aggregate programs inducing finite well-founded
models as above consists of programs over a signature with nullary function
symbols only. Any such program can be turned into an equivalent finite set of
propositional rules with finitary bodies.

##  5 Dependency analysis

We now further refine our semantic approach to reflect actual grounding
processes. In fact, modern grounders process programs on-the-fly by grounding
one rule after another without storing any rules. At the same time, they try
to determine certain, possible, and false atoms. Unfortunately, well-founded
models cannot be computed on-the-fly, which is why we introduce below the
concept of an approximate model. More precisely, we start by defining
instantiation sequences of (non-ground) aggregate programs based on their rule
dependencies. We show that approximate models of instantiation sequences are
underapproximations of the well-founded model of the corresponding sequence of
(ground) $\mathcal{R}$-programs, as defined in Section 3. The precision of
both types of models coincides on stratified programs. We illustrate our
concepts comprehensively at the end of this section in Examples 19 and 20.

To begin with, we extend the notion of positive and negative literals to
aggregate programs. For atoms $a$, we define $a^{+}={({\neg}a)}^{-}=\\{a\\}$
and $a^{-}={({\neg}a)}^{+}=\emptyset$. For comparisons $a$, we define
$a^{+}=a^{-}=\emptyset$. For aggregates $a$ with elements $E$, we define
positive and negative atom occurrences, using Proposition 24 to refine the
case for monotone aggregates:

  * •

$a^{+}=\bigcup_{e\in E}B(e)$,

  * •

$a^{-}=\emptyset$ if $a$ is monotone, and

  * •

$a^{-}=\bigcup_{e\in E}B(e)$ if $a$ is not monotone.

For a set of body literals $B$, we define $B^{+}=\bigcup_{b\in B}b^{+}$ and
$B^{-}=\bigcup_{b\in B}b^{-}$, as well as $B^{\pm}=B^{+}\cup B^{-}$.

We see in the following, that a special treatment of monotone aggregates
yields better approximations of well-founded models. A similar case could be
made for antimonotone aggregates but had led to a more involved algorithmic
treatment.

Inter-rule dependencies are determined via the predicates appearing in their
heads and bodies. We define $\mathrm{pred}(a)$ to be the predicate symbol
associated with atom $a$ and $\mathrm{pred}(A)=\\{\mathrm{pred}(a)\mid a\in
A\\}$ for a set $A$ of atoms. An aggregate rule $r_{1}$ _depends_ on another
aggregate rule $r_{2}$ if
$\mathrm{pred}(H(r_{2}))\in\mathrm{pred}({B(r_{1})}^{\pm})$. Rule $r_{1}$
depends _positively_ or _negatively_ on $r_{2}$ if
$\mathrm{pred}(H(r_{2}))\in\mathrm{pred}(B(r_{1})^{+})$ or
$\mathrm{pred}(H(r_{2}))\in\mathrm{pred}({B(r_{2})}^{-})$, respectively.

For simplicity, we first focus on programs without aggregates in examples and
delay a full example with aggregates until the end of the section.

######  Example 16.

Let us consider the following rules from the introductory example:

$\displaystyle u(1)$ ($r_{1}$) $\displaystyle p(X)$
$\displaystyle\leftarrow{\neg}q(X)\wedge u(X)$ ($r_{2}$) $\displaystyle q(X)$
$\displaystyle\leftarrow{\neg}p(X)\wedge v(X)$ ($r_{3}$)

We first determine the rule heads and positive and negative atom occurrences
in rule bodies:

$\displaystyle H(r_{1})$ $\displaystyle=u(1)$ $\displaystyle B(r_{1})^{+}$
$\displaystyle=\emptyset$ $\displaystyle B(r_{1})^{-}$
$\displaystyle=\emptyset$ $\displaystyle H(r_{2})$ $\displaystyle=p(X)$
$\displaystyle B(r_{2})^{+}$ $\displaystyle=\\{u(X)\\}$ $\displaystyle
B(r_{2})^{-}$ $\displaystyle=\\{q(X)\\}$ $\displaystyle H(r_{3})$
$\displaystyle=q(X)$ $\displaystyle B(r_{3})^{+}$ $\displaystyle=\\{v(X)\\}$
$\displaystyle B(r_{3})^{-}$ $\displaystyle=\\{p(X)\\}$

With this, we infer the corresponding predicates:

$\displaystyle\mathrm{pred}(H(r_{1}))$ $\displaystyle=u/1$
$\displaystyle\mathrm{pred}(B(r_{1})^{+})$ $\displaystyle=\emptyset$
$\displaystyle\mathrm{pred}(B(r_{1})^{-})$ $\displaystyle=\emptyset$
$\displaystyle\mathrm{pred}(H(r_{2}))$ $\displaystyle=p/1$
$\displaystyle\mathrm{pred}(B(r_{2})^{+})$ $\displaystyle=\\{u/1\\}$
$\displaystyle\mathrm{pred}(B(r_{2})^{-})$ $\displaystyle=\\{q/1\\}$
$\displaystyle\mathrm{pred}(H(r_{3}))$ $\displaystyle=q/1$
$\displaystyle\mathrm{pred}(B(r_{3})^{+})$ $\displaystyle=\\{v/1\\}$
$\displaystyle\mathrm{pred}(B(r_{3})^{-})$ $\displaystyle=\\{p/1\\}$

We see that $r_{2}$ depends positively on $r_{1}$ and that $r_{2}$ and $r_{3}$
depend negatively on each other. View Figure 1 in Example 17 for a graphical
representation of these inter-rule dependencies.

The _strongly connected components_ of an aggregate program $P$ are the
equivalence classes under the transitive closure of the dependency relation
between all rules in $P$. A strongly connected component ${P}_{1}$ _depends_
on another strongly connected component ${P}_{2}$ if there is a rule in
${P}_{1}$ that depends on some rule in ${P}_{2}$. The transitive closure of
this relation is antisymmetric.

A strongly connected component of an aggregate program is _unstratified_ if it
depends negatively on itself or if it depends on an unstratified component. A
component is _stratified_ if it is not unstratified.

A topological ordering of the strongly connected components is then used to
guide grounding.

For example, the sets $\\{r_{1}\\}$ and $\\{r_{2},r_{3}\\}$ of rules from
Example 16 are strongly connected components in a topological order. There is
only one topological order because $r_{2}$ depends on $r_{1}$. While the first
component is stratified, the second component is unstratified because $r_{2}$
and $r_{3}$ depend negatively on each other.

######  Definition 11.

We define an _instantiation sequence_ for $P$ as a sequence
${({P}_{i})}_{i\in\mathbb{I}}$ of its strongly connected components such that
$i<j$ if ${P}_{j}$ depends on ${P}_{i}$.

Note that the components can always be well ordered because aggregate programs
consist of finitely many rules.

The consecutive construction of the well-founded model along an instantiation
sequence results in the well-founded model of the entire program.

######  Theorem 26.

Let ${({P}_{i})}_{i\in\mathbb{I}}$ be an instantiation sequence for aggregate
program $P$.

Then, $\mathit{WM}({(\pi(P_{i}))}_{i\in\mathbb{I}})=\mathit{WM}(\pi(P))$.

######  Example 17.

The following example shows how to split an aggregate program into an
instantiation sequence and gives its well-founded model. Let $P$ be the
following aggregate program, extending the one from the introductory section:

$\displaystyle u(1)$ $\displaystyle u(2)$ $\displaystyle v(2)$ $\displaystyle
v(3)$ $\displaystyle p(X)$ $\displaystyle\leftarrow{\neg}q(X)\wedge u(X)$
$\displaystyle q(X)$ $\displaystyle\leftarrow{\neg}p(X)\wedge v(X)$
$\displaystyle x$ $\displaystyle\leftarrow{\neg}p(1)$ $\displaystyle y$
$\displaystyle\leftarrow{\neg}q(3)$

Figure 1: Rule dependencies for Example 19.

We have already seen how to determine inter-rule dependencies in Example 16. A
possible instantiation sequence for program $P$ is given in Figure 1. Rules
are depicted in solid boxes. Solid and dotted edges between such boxes depict
positive and negative dependencies between the corresponding rules,
respectively. Dashed and dashed/dotted boxes represent components in the
instantiation sequence (we ignore dotted boxes for now but turn to them in
Example 18). The number in the corner of a component box indicates the index
in the corresponding instantiation sequence.

For $F=\\{u(1),u(2),v(2),v(3)\\}$, the well-founded model of $\pi(P)$ is

$\displaystyle\mathit{WM}(\pi(P))$
$\displaystyle=(\\{p(1),q(3)\\},\\{p(1),p(2),q(2),q(3)\\})\sqcup F.$

By Theorem 26, the ground sequence ${(\tau({P}_{i}))}_{i\in\mathbb{I}}$ has
the same well-founded model as $\pi(P)$:

$\displaystyle\mathit{WM}({(\pi(P))}_{i\in\mathbb{I}})$
$\displaystyle=(\\{p(1),q(3)\\},\\{p(1),p(2),q(2),q(3)\\})\sqcup F.$

Note that the set $F$ comprises the facts derived from stratified components.
In fact, for stratified components, the set of external atoms (3) is empty. We
can use Corollary 20 to confirm that the well founded model $(F,F)$ of
sequence ${(\pi({P}_{i}))}_{1\leq i\leq 4}$ is total. In fact, each of the
intermediate interpretations (5) is total and can be computed with just one
application of the stable operator. For example, $I_{1}=J_{1}=\\{u(1)\\}$ for
component ${P}_{1}$.

We further refine instantiation sequences by partitioning each component along
its positive dependencies.

######  Definition 12.

Let $P$ be an aggregate program and ${({P}_{i})}_{i\in\mathbb{I}}$ be an
instantiation sequence for $P$. Furthermore, for each $i\in\mathbb{I}$, let
${({P}_{i,j})}_{j\in\mathbb{I}_{i}}$ be an instantiation sequence of ${P}_{i}$
considering positive dependencies only.

A _refined instantiation sequence_ for $P$ is a sequence
${({P}_{i,j})}_{(i,j)\in\mathbb{J}}$ where the index set
$\mathbb{J}=\\{(i,j)\mid i\in\mathbb{I},j\in\mathbb{I}_{i}\\}$ is ordered
lexicographically.

We call ${({P}_{i,j})}_{(i,j)\in\mathbb{J}}$ a refinement of
${({P}_{i})}_{i\in\mathbb{I}}$.

We define a component ${P}_{i,j}$ to be _stratified_ or _unstratified_ if the
encompassing component ${P}_{i}$ is stratified or unstratified, respectively.

Examples of refined instantiation sequences are given in Figures 1 and 2.

The advantage of such refinements is that they yield better or equal
approximations (cf. Theorems 28 and 19). On the downside, we do not obtain
that $\mathit{WM}({({P}_{i})}_{i\in\mathbb{J}})$ equals $\mathit{WM}(\pi(P))$
for refined instantiation sequences in general.

######  Example 18.

The refined instantiation sequence for program $P$ from Example 17 is given in
Figure 1. A dotted box indicates a component in a refined instantiation
sequence. Components that cannot be refined further are depicted with a
dashed/dotted box. The number or pair in the corner of a component box
indicates the index in the corresponding refined instantiation sequence.

Unlike in Example 17, the well-founded model of the refined sequence of ground
programs ${(\tau({P}_{i,j}))}_{(i,j)\in\mathbb{J}}$ is

$\displaystyle\mathit{WM}({(\tau({P}_{i,j}))}_{(i,j)\in\mathbb{J}})$
$\displaystyle=(\\{q(3)\\},\\{p(1),p(2),q(2),q(3),x\\})\sqcup F,$

which is actually less precise than the well-founded model of $P$. This is
because literals over ${\neg}q(X)$ are unconditionally assumed to be true
because their instantiation is not yet available when ${P}_{5,1}$ is
considered. Thus, we get $(I_{5,1},J_{5,1})=(\emptyset,\\{p(1),p(2)\\})$ for
the intermediate interpretation (5). Unlike this, the atom $p(3)$ is false
when considering component ${P}_{5,2}$ and $q(3)$ becomes true. In fact, we
get $(I_{5,2},J_{5,2})=(\\{q(3)\\},\\{q(2),q(3)\\})$. Observe that
$(I_{5},J_{5})$ from above is less precise than
$(I_{5,1},J_{5,1})\sqcup(I_{5,2},J_{5,2})$.

We continue with this example below and show in Example 19 that refined
instantiation sequences can still be advantageous to get better approximations
of well-founded models.

We have already seen in Section 3 that external atoms may lead to less precise
semantic characterizations. This is just the same in the non-ground case,
whenever a component comprises predicates that are defined in a following
component of a refined instantiation sequence. This leads us to the concept of
an approximate model obtained by overapproximating the extension of such
externally defined predicates.

######  Definition 13.

Let $P$ be an aggregate program, $(\mathit{I\\!C},\mathit{J\\!C})$ be a four-
valued interpretation, $\mathcal{E}$ be a set of predicates, and $P^{\prime}$
be the program obtained from $P$ by removing all rules $r$ with
$\mathrm{pred}(B(r)^{-})\cap\mathcal{E}\neq\emptyset$.

We define the _approximate model of $P$ relative_ to
$(\mathit{I\\!C},\mathit{J\\!C})$ as

$\displaystyle\mathit{AM}^{(\mathit{I\\!C},\mathit{J\\!C})}_{\mathcal{E}}(P)$
$\displaystyle=(I,J)$ where $\displaystyle I$
$\displaystyle=S_{\pi(P^{\prime})}^{\mathit{I\\!C}}(\mathit{J\\!C})\text{\
and\ }$ $\displaystyle J$
$\displaystyle=S_{\pi(P)}^{\mathit{J\\!C}}(\mathit{I\\!C}\cup I)$

We keep dropping parentheses and simply write
$\mathit{AM}^{\mathit{I\\!C},\mathit{J\\!C}}_{\mathcal{E}}(P)$ instead of
$\mathit{AM}^{(\mathit{I\\!C},\mathit{J\\!C})}_{\mathcal{E}}(P)$.

The approximate model amounts to an immediate consequence operator, similar to
the relative well-founded operator in Definition 4; it refrains from any
iterative applications, as used for defining a well-founded model. More
precisely, the relative stable operator is applied twice to obtain the
approximate model. This is similar to Van Gelder’s alternating transformation
[Van Gelder (1993)]. The certain atoms in $I$ are determined by applying the
operator to the ground program obtained after removing all rules whose
negative body literals comprise externally defined predicates, while the
possible atoms $J$ are computed from the entire program by taking the already
computed certain atoms in $I$ into account. In this way, the approximate model
may result in fewer unknown atoms than the relative well-founded operator when
applied to the least precise interpretation (as an easy point of reference).
How well we can approximate the certain atoms with the approximate operator
depends on the set of external predicates $\mathcal{E}$. When approximating
the model of a program $P$ in a sequence, the set $\mathcal{E}$ comprises all
negative predicates occurring in $P$ for which possible atoms have not yet
been fully computed. This leads to fewer certain atoms obtained from the
reduced program, $P^{\prime}=\\{r\in
P\mid\mathrm{pred}(B(r)^{-})\cap\mathcal{E}=\emptyset\\}$, stripped of all
rules from $P$ that have negative body literals whose predicates occur in
$\mathcal{E}$.

The next theorem identifies an essential prerequisite for an approximate model
of a non-ground program to be an underapproximation of the well-founded model
of the corresponding ground program.

######  Theorem 27.

Let $P$ be an aggregate program, $\mathcal{E}$ be a set of predicates, and
$(\mathit{I\\!C},\mathit{J\\!C})$ be a four-valued interpretation.

If $\mathrm{pred}(H(P))\cap\mathrm{pred}(B(P)^{-})\subseteq\mathcal{E}$ then
$\mathit{AM}^{\mathit{I\\!C},\mathit{J\\!C}}_{\mathcal{E}}(P)\leq_{p}\mathit{WM}^{\mathit{I\\!C},\mathit{J\\!C}\cup\mathit{E\\!C}}(\pi(P))$
where $\mathit{E\\!C}$ is the set of all ground atoms over predicates in
$\mathcal{E}$.

In general, a grounder cannot calculate on-the-fly a well-founded model.
Implementing this task efficiently requires an algorithm storing the grounded
program, as, for example, implemented in an ASP solver. But modern grounders
are able to calculate the stable operator on-the-fly. Thus, an approximation
of the well-founded model is calculated. This is where we use the approximate
model, which might be less precise than the well-founded model but can be
computed more easily.

With the condition of Theorem 27 in mind, we define the approximate model for
an instantiation sequence. We proceed similar to Definition 6 but treat in
(14) all atoms over negative predicates that have not been completely defined
as external.

######  Definition 14.

Let ${({P}_{i})}_{i\in\mathbb{I}}$ be a (refined) instantiation sequence for
$P$.

Then, the _approximate model_ of ${({P}_{i})}_{i\in\mathbb{I}}$ is

$\displaystyle\mathit{AM}({({P}_{i})}_{i\in\mathbb{I}})$
$\displaystyle=\bigsqcup_{i\in\mathbb{I}}(I_{i},J_{i}).$ where
$\displaystyle\mathcal{E}_{i}$
$\displaystyle=\mathrm{pred}({B({P}_{i})}^{-})\cap\mathrm{pred}(\bigcup_{i\leq
j}H({P}_{j})),$ (14) $\displaystyle(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})$
$\displaystyle=\bigsqcup_{j<i}(I_{j},J_{j})\text{, and}$ (15)
$\displaystyle(I_{i},J_{i})$
$\displaystyle=\mathit{AM}^{\mathit{I\\!C}_{i},\mathit{J\\!C}_{i}}_{\mathcal{E}_{i}}({P}_{i}).$
(16)

Note that the underlying approximate model removes rules containing negative
literals over predicates in ${\mathcal{E}}_{i}$ when calculating certain
atoms. This amounts to assuming all ground instances of atoms over
${\mathcal{E}}_{i}$ to be possible.777To be precise, rules involving
aggregates that could in principle derive certain atoms might be removed, too.
Here, we are interested in a syntactic criteria that allows us to
underapproximate the set of certain atoms. Compared to (3), however, this
additionally includes recursive predicates in (14). The set
${\mathcal{E}}_{i}$ is empty for stratified components.

The next result relies on Theorem 17 to show that an approximate model of an
instantiation sequence constitutes an underapproximation of the well-founded
model of the translated entire program. In other words, the approximate model
of a sequence of aggregate programs (as computed by a grounder) is less
precise than the well-founded model of the whole ground program.

######  Theorem 28.

Let ${({P}_{i})}_{i\in\mathbb{I}}$ be an instantiation sequence for aggregate
program $P$ and ${({P}_{j})}_{j\in\mathbb{J}}$ be a refinement of
${({P}_{i})}_{i\in\mathbb{I}}$.

Then,
$\mathit{AM}({({P}_{i})}_{i\in\mathbb{I}})\leq_{p}\mathit{AM}({({P}_{j})}_{j\in\mathbb{J}})\leq_{p}\mathit{WM}(\pi(P))$.

The finer granularity of refined instantiation sequences leads to more precise
models. Intuitively, this is because a refinement of a component may result in
a series of approximate models, which yield a more precise result than the
approximate model of the entire component because in some cases fewer
predicates are considered external in (14).

We remark that all instantiation sequences of a program have the same
approximate model. However, this does not carry over to refined instantiation
sequences because their evaluation is order dependent.

The two former issues are illustrated in Example 19.

The actual value of approximate models for grounding lies in their underlying
series of consecutive interpretations delineating each ground program in a
(refined) instantiation sequence. In fact, as outlined after Theorem 25,
whenever all interpretations $(I_{i},J_{i})$ in (16) are finite so are the
$\mathcal{R}$-programs $\pi_{\mathit{J\\!C}_{i}\cup
J_{i}}({P}_{i})^{(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})\sqcup(I_{i},J_{i})}$
obtained from each ${P}_{i}$ in the instantiation sequence.

######  Theorem 29.

Let ${({P}_{i})}_{i\in\mathbb{I}}$ be a (refined) instantiation sequence of an
aggregate program $P$, and let $(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})$ and
$(I_{i},J_{i})$ be defined as in 15 and 16.

Then, $\bigcup_{i\in\mathbb{I}}\pi_{\mathit{J\\!C}_{i}\cup
J_{i}}({P}_{i})^{(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})\sqcup(I_{i},J_{i})}$
and $\pi(P)$ have the same well-founded and stable models.

Notably, this union of $\mathcal{R}$-programs is exactly the one obtained by
the grounding algorithm proposed in the next section (cf. Theorem 34).

######  Example 19.

We continue Example 18.

The approximate model of the instantiation sequence
${({P}_{i})}_{i\in\mathbb{I}}$, defined in Definition 14, is less precise than
the well-founded model of the sequence, viz.

$\displaystyle\mathit{AM}({({P}_{i})}_{i\in\mathbb{I}})$
$\displaystyle=(\emptyset,\\{p(1),p(2),q(2),q(3),x,y\\})\sqcup F.$

This is because we have to use $\mathit{AM}^{F,F}_{\mathcal{E}}({P}_{5})$ to
approximate the well-founded model of component ${P}_{5}$. Here, the set
$\mathcal{E}=\\{a/1,b/1\\}$ determined by 14 forces us to unconditionally
assume instances of ${\neg}q(X)$ and ${\neg}p(X)$ to be true. Thus, we get
$(I_{5},J_{5})=(\emptyset,\\{p(1),p(2),q(2),q(3)\\})$ for the intermediate
interpretation in (16). This is also reflected in Definition 13, which makes
us drop all rules containing negative literals over predicates in
$\mathcal{E}$ when calculating true atoms.

In accord with Theorem 28, we approximate the well-founded model w.r.t. the
refined instantiation sequence ${({P}_{i,j})}_{(i,j)\in\mathbb{J}}$ and obtain

$\displaystyle\mathit{AM}({({P}_{i,j})}_{(i,j)\in\mathbb{J}})$
$\displaystyle=(\\{q(3)\\},\\{p(1),p(2),q(2),q(3),x\\})\sqcup F,$

which, for this example, is equivalent to the well-founded model of the
corresponding ground refined instantiation sequence and more precise than the
approximate model of the instantiation sequence.

In an actual grounder implementation the approximate model is only a
byproduct, instead, it outputs a program equivalent to the one in Theorem 29:

$\displaystyle u(1)$ $\displaystyle u(2)$ $\displaystyle v(2)$ $\displaystyle
v(3)$ $\displaystyle p(1)$ $\displaystyle\leftarrow{\neg}q(1)\wedge u(1)$
$\displaystyle p(2)$ $\displaystyle\leftarrow{\neg}q(2)\wedge u(2)$
$\displaystyle q(2)$ $\displaystyle\leftarrow{\neg}p(2)\wedge v(2)$
$\displaystyle q(3)$ $\displaystyle\leftarrow{\neg}p(3)\wedge v(3)$
$\displaystyle x$ $\displaystyle\leftarrow{\neg}p(1)$

Note that the rule $y\leftarrow{\neg}q(3)$ is not part of the simplification
because $q(3)$ is certain.

######  Remark 1.

The reason why we use the refined grounding is that we cannot expect a
grounding algorithm to calculate the well-founded model for a component
without further processing. But at least some consequences should be
considered. Gringo is designed to ground on-the-fly without storing any rules,
so it cannot be expected to compute all possible consequences but it should at
least take all consequences from preceding interpretations into account. With
the help of a solver, we could calculate the exact well-founded model of a
component after it has been grounded.

Whenever an aggregate program is stratified, the approximate model of its
instantiation sequence is total (and coincides with the well-founded model of
the entire ground program).

######  Theorem 30.

Let ${({P}_{i})}_{i\in\mathbb{I}}$ be an instantiation sequence of an
aggregate program $P$ such that $\mathcal{E}_{i}=\emptyset$ for each
$i\in\mathbb{I}$ as defined in 14.

Then, $\mathit{AM}({({P}_{i})}_{i\in\mathbb{I}})$ is total.

######  Example 20.

The dependency graph of the company controls encoding is given in Figure 2 and
follows the conventions in Example 19. Because the encoding only uses positive
literals and monotone aggregates, grounding sequences cannot be refined
further. Since the program is positive, we can apply Theorem 30. Thus, the
approximate model of the grounding sequence is total and corresponds to the
well-founded model of the program. We use the same abbreviations for
predicates as in Figure 2. The well-founded model is $(F\cup I,F\cup I)$ where

$\displaystyle F=\\{$ $\displaystyle c(c_{1}),c(c_{2}),c(c_{3}),c(c_{4}),$
$\displaystyle
o(c_{1},c_{2},60),o(c_{1},c_{3},20),o(c_{2},c_{3},35),o(c_{3},c_{4},51)\\}\text{\
and\ }$ $\displaystyle I=\\{$ $\displaystyle
s(c_{1},c_{2}),s(c_{3},c_{4}),s(c_{1},c_{3}),s(c_{1},c_{4})\\}.$

Figure 2: Rule dependencies for the company controls encoding and instance in
Example 10 where $c=\mathit{company}$, $o=\mathit{owns}$, and
$s=\mathit{controls}$.

##  6 Algorithms

This section lays out the basic algorithms for grounding rules, components,
and entire programs and characterizes their output in terms of the semantic
concepts developed in the previous sections. Of particular interest is the
treatment of aggregates, which are decomposed into dedicated normal rules
before grounding and reassembled afterward. This allows us to ground rules
with aggregates by means of grounding algorithms for normal rules. Finally, we
show that our grounding algorithm guarantees that an obtained finite ground
program is equivalent to the original non-ground program.

In the following, we refer to terms, atoms, comparisons, literals, aggregate
elements, aggregates, or rules as _expressions_. As in the preceding sections,
all expressions, interpretations, and concepts introduced below operate on the
same (implicit) signature $\Sigma$ unless mentioned otherwise.

A _substitution_ is a mapping from the variables in $\Sigma$ to terms over
$\Sigma$. We use $\iota$ to denote the identity substitution mapping each
variable to itself. A _ground substitution_ maps all variables to ground terms
or themselves. The result of _applying_ a substitution $\sigma$ to an
expression $e$, written $e\sigma$, is the expression obtained by replacing
each variable $v$ in $e$ by $\sigma(v)$. This directly extends to sets $E$ of
expressions, that is, $E\sigma=\\{e\sigma\mid e\in E\\}$.

The _composition_ of substitutions $\sigma$ and $\theta$ is the substitution
$\sigma\circ\theta$ where $(\sigma\circ\theta)(v)=\theta(\sigma(v))$ for each
variable $v$.

A substitution $\sigma$ is a _unifier_ of a set $E$ of expressions if
$e_{1}\sigma=e_{2}\sigma$ for all $e_{1},e_{2}\in E$. In what follows, we are
interested in one-sided unification, also called _matching_. A substitution
$\sigma$ matches a non-ground expression $e$ to a ground expression $g$, if
$e\sigma=g$ and $\sigma$ maps all variables not occurring in $e$ to
themselves. We call such a substitution the _matcher_ of $e$ to $g$. Note that
a matcher is a unique ground substitution unifying $e$ and $g$, if it exists.
This motivates the following definition.

For a (non-ground) expression $e$ and a ground expression $g$, we define:

$\displaystyle\textnormal{{match}}(e,g)=\begin{cases}\\{\sigma\\}&\text{if
there is a matcher $\sigma$ from $e$ to $g$}\\\
\emptyset&\text{otherwise}\end{cases}$

When grounding rules, we look for matches of non-ground body literals in the
possibly derivable atoms accumulated so far. The latter is captured by a four-
valued interpretation to distinguish certain atoms among the possible ones.
This is made precise in the next definition.

######  Definition 15.

Let $\sigma$ be a substitution, $l$ be a literal or comparison, and $(I,J)$ be
a four-valued interpretation.

We define the set of _matches_ for $l$ in $(I,J)$ w.r.t. $\sigma$, written
$\textnormal{{Matches}}^{I,J}_{l}(\sigma)$,

for an atom $l=a$ as $\displaystyle\textnormal{{Matches}}^{I,J}_{a}(\sigma)$
$\displaystyle=\\{\sigma\circ\sigma^{\prime}\mid a^{\prime}\in
J,\sigma^{\prime}\in\textnormal{{match}}(a\sigma,a^{\prime})\\}\text{,}$ for a
ground literal $l={\neg}a$ as
$\displaystyle\textnormal{{Matches}}^{I,J}_{{\neg}a}(\sigma)$
$\displaystyle=\\{\sigma\mid a\sigma\not\in I\\}\text{, and}$ for a ground
comparison $l=t_{1}\prec t_{2}$ as in (6) as
$\displaystyle\textnormal{{Matches}}^{I,J}_{t_{1}\prec t_{2}}(\sigma)$
$\displaystyle=\\{\sigma\mid\text{$\prec$ holds between $t_{1}\sigma$ and
$t_{2}\sigma$}\\}.$

In this way, positive body literals yield a (possibly empty) set of
substitutions, refining the one at hand, while negative and comparison
literals are only considered when ground and then act as a test on the given
substitution.

1 function  _$\textnormal{{GroundRule}}^{I,J}_{r,f,J^{\prime}}(\sigma,L)$_

2 if  _$L\neq\emptyset$_ then // match next

3 $(G,l)\leftarrow(\emptyset,\textnormal{{Select}}_{\sigma}(L))$;

4 foreach  _$\sigma^{\prime}\in\textnormal{{Matches}}^{I,J}_{l}(\sigma)$_ do

5 $G\leftarrow
G\cup\textnormal{{GroundRule}}^{I,J}_{r,f,J^{\prime}}(\sigma^{\prime},L\setminus\\{l\\})$;

6

7 return $G$;

8

9 else if  _$f=\textnormal{{t}}$ or ${B(r\sigma)}^{+}\nsubseteq J^{\prime}$_
then // rule instance

10 return $\\{r\sigma\\}$;

11

12 else // rule seen

13 return $\emptyset$;

14

15

Algorithm 1 Grounding Rules

Our function for rule instantiation is given in Algorithm 1. It takes a
substitution $\sigma$ and a set $L$ of literals and yields a set of ground
instances of a safe normal rule $r$, passed as a parameter; if called with the
identity substitution and the body literals $B(r)$ of $r$, it yields ground
instances of the rule. The other parameters consist of a four-valued
interpretation $(I,J)$ comprising the set of possibly derivable atoms along
with the certain ones, a two-valued interpretation $J^{\prime}$ reflecting the
previous value of $J$, and a Boolean flag $f$ used to avoid duplicate ground
rules in consecutive calls to Algorithm 1. The idea is to extend the current
substitution in Algorithms 1 to 1 until we obtain a ground substitution
$\sigma$ that induces a ground instance $r\sigma$ of rule $r$. To this end,
$\textnormal{{Select}}_{\sigma}(L)$ picks for each call some literal $l\in L$
such that $l\in L^{+}$ or $l\sigma$ is ground. That is, it yields either a
positive body literal or a ground negative or ground comparison literal, as
needed for computing $\textnormal{{Matches}}^{I,J}_{l}(\sigma)$. Whenever an
application of Matches for the selected literal in $B(r)$ results in a non-
empty set of substitutions, the function is called recursively for each such
substitution. The recursion terminates if at least one match is found for each
body literal and an instance $r\sigma$ of $r$ is obtained in Algorithm 1. The
set of all such ground instances is returned in Algorithm 1. (Note that we
refrain from applying any simplifications to the ground rules and rather leave
them intact to obtain more direct formal characterizations of the results of
our grounding algorithms.) The test ${B(r\sigma)}^{+}\nsubseteq J^{\prime}$ in
Algorithm 1 makes sure that no ground rules are generated that were already
obtained by previous invocations of Algorithm 1. This is relevant for
recursive rules and reflects the approach of semi-naive database evaluation
[Abiteboul et al. (1995)].

For characterizing the result of Algorithm 1 in terms of aggregate programs,
we need the following definition.

######  Definition 16.

Let $P$ be an aggregate program and $(I,J)$ be a four-valued interpretation.

We define $\mathrm{Inst}^{I,J}(P)\subseteq\mathrm{Inst}(P)$ as the set of all
instances $g$ of rules in $P$ satisfying $J\models\pi(B(g))^{\wedge}_{I}$.

In terms of the program simplification in Definition 1, an instance $g$
belongs to $\mathrm{Inst}^{I,J}(P)$ iff
$H(g)\leftarrow\pi(B(g))^{\wedge}\in\pi(r)^{I,J}$. Note that the members of
$\mathrm{Inst}^{I,J}(P)$ are not necessarily ground, since non-global
variables may remain within aggregates; though they are ground for normal
rules.

We use Algorithm 1 to iteratively compute ground instances of a rule w.r.t. an
increasing set of atoms. The Boolean flag $f$ and the set of atoms
$J^{\prime}$ are used to avoid duplicating ground instances in successive
iterations. The flag $f$ is initially set to true to not filter any rule
instances. In subsequent iterations, duplicates are omitted by setting the
flag to false and filtering rules whose positive bodies are a subset of the
atoms $J^{\prime}$ used in previous iterations. This is made precise in the
next result.

######  Proposition 31.

Let $r$ be a safe normal rule and $(I,J)$ be a finite four-valued
interpretation.

Then,

  1. (a)

$\mathrm{Inst}^{I,J}(\\{r\\})=\textnormal{{GroundRule}}^{I,J}_{r,\textnormal{{t}},\emptyset}(\iota,B(r))$
and

  2. (b)

$\mathrm{Inst}^{I,J}(\\{r\\})=\mathrm{Inst}^{I,J^{\prime}}(\\{r\\})\cup\textnormal{{GroundRule}}^{I,J}_{r,\textnormal{{f}},J^{\prime}}(\iota,B(r))$
for all $J^{\prime}\subseteq J$.

Now, let us turn to the treatment of aggregates. To this end, we define the
following translation of aggregate programs to normal programs.

######  Definition 17.

Let $P$ be a safe aggregate program over signature $\Sigma$.

Let $\Sigma^{\prime}$ be the signature obtained by extending $\Sigma$ with
fresh predicates

$\displaystyle\alpha_{a,r}/{n}\text{, and}$ (17)
$\displaystyle\epsilon_{a,r}/{n}$ (18)

for each aggregate $a$ occurring in a rule $r\in P$ where $n$ is the number of
global variables in $a$, and fresh predicates

$\displaystyle\eta_{e,a,r}/{(m+n)}$ (19)

for each aggregate element $e$ occurring in aggregate $a$ in rule $r$ where
$m$ is the size of the tuple $H(e)$.

We define ${P}^{\alpha}$, ${P}^{\epsilon}$, and ${P}^{\eta}$ as normal
programs over $\Sigma^{\prime}$ as follows.

  * •

Program ${P}^{\alpha}$ is obtained from $P$ by replacing each aggregate
occurrence $a$ in $P$ with

$\displaystyle\alpha_{a,r}(X_{1},\dots,X_{n})$ (20)

where $\alpha_{a,r}/{n}$ is defined as in (17) and $X_{1},\dots,X_{n}$ are the
global variables in $a$.

  * •

Program ${P}^{\epsilon}$ consists of rules

$\displaystyle\epsilon_{a,r}(X_{1},\dots,X_{n})$ $\displaystyle\leftarrow
t\prec b\wedge b_{1}\wedge\dots\wedge b_{l}$ (21)

for each predicate $\epsilon_{a,r}/{n}$ as in (18) where $X_{1},\dots,X_{n}$
are the global variables in $a$, $a$ is an aggregate of form $f\\{E\\}\prec b$
occurring in $r$, $t=f(\emptyset)$ is the value of the aggregate function
applied to the empty set, and $b_{1},\dots,b_{l}$ are the body literals of $r$
excluding aggregates.

  * •

Program ${P}^{\eta}$ consists of rules

$\displaystyle\eta_{e,a,r}(t_{1},\dots,t_{m},X_{1},\dots,X_{n})$
$\displaystyle\leftarrow c_{1}\wedge\dots\wedge c_{k}\wedge
b_{1}\wedge\dots\wedge b_{l}$ (22)

for each predicate $\eta_{e,a,r}/{m+n}$ as in (19) where
$(t_{1},\dots,t_{m})=H(e)$, $X_{1},\dots,X_{n}$ are the global variables in
$a$, $\\{c_{1},\dots,c_{k}\\}=B(e)$, and $b_{1},\dots,b_{l}$ are the body
literals of $r$ excluding aggregates.

Summarizing the above, we translate an aggregate program $P$ over $\Sigma$
into a normal program ${P}^{\alpha}$ along with auxiliary normal rules in
${P}^{\epsilon}$ and ${P}^{\eta}$, all over a signature extending $\Sigma$ by
the special-purpose predicates in 17, 18 and 19. In fact, there is a one-to-
one correspondence between the rules in $P$ and ${P}^{\alpha}$, so that we get
$P={P}^{\alpha}$ and ${P}^{\epsilon}={P}^{\eta}=\emptyset$ whenever $P$ is
normal.

######  Example 21.

We illustrate the translation of aggregate programs on the company controls
example in Example 10. We rewrite the rule

$\displaystyle\begin{split}\mathit{controls}(X,Y)\leftarrow{}&\\!\overbrace{\begin{aligned}
\mathrm{\\#sum}^{+}\\{&\underbrace{S:\mathit{owns}(X,Y,S)}_{e_{1}};\\\
&\underbrace{S,Z:\mathit{controls}(X,Z)\wedge\mathit{owns}(Z,Y,S)}_{e_{2}}\\}>50\end{aligned}}^{a}\\\
{}\wedge{}&\mathit{company}(X)\wedge\mathit{company}(Y)\wedge X\neq
Y\end{split}$ ($r$)

containing aggregate $a$ with elements $e_{1}$ and $e_{2}$, into rules $r_{1}$
to $r_{4}$:

$\displaystyle\begin{split}\mathit{controls}(X,Y)\leftarrow{}&\alpha_{a,r}(X,Y)\\\
{}\wedge{}&\mathit{company}(X)\wedge\mathit{company}(Y)\wedge X\neq
Y,\end{split}$ ($r_{1}$)
$\displaystyle\begin{split}\epsilon_{a,r}(X,Y)\leftarrow{}&0>50\\\
{}\wedge{}&\mathit{company}(X)\wedge\mathit{company}(Y)\wedge X\neq
Y,\end{split}$ ($r_{2}$)
$\displaystyle\begin{split}\eta_{e_{1},a,r}(S,X,Y)\leftarrow{}&\mathit{owns}(X,Y,S)\\\
{}\wedge{}&\mathit{company}(X)\wedge\mathit{company}(Y)\wedge X\neq Y,\text{\
and\ }\end{split}$ ($r_{3}$)
$\displaystyle\begin{split}\eta_{e_{2},a,r}(S,Z,X,Y)\leftarrow{}&\mathit{controls}(X,Z)\wedge\mathit{owns}(Z,Y,S)\\\
{}\wedge{}&\mathit{company}(X)\wedge\mathit{company}(Y)\wedge X\neq
Y.\end{split}$ ($r_{4}$)

We have ${P}^{\alpha}=\\{r_{1}\\}$, ${P}^{\epsilon}=\\{r_{2}\\}$, and
${P}^{\eta}=\\{r_{3},r_{4}\\}$.

This example illustrates how possible instantiations of aggregate elements are
gathered via the rules in ${P}^{\eta}$. Similarly, the rules in
${P}^{\epsilon}$ collect instantiations warranting that the result of applying
aggregate functions to the empty set is in accord with the respective bound.
In both cases, the relevant variable bindings are captured by the special head
atoms of the rules. In turn, groups of corresponding instances of aggregate
elements are used in Definition 20 to sanction the derivation of ground atoms
of form 20. These atoms are ultimately replaced in ${P}^{\alpha}$ with the
original aggregate contents.

We next define two functions gathering information from instances of rules in
${P}^{\epsilon}$ and ${P}^{\eta}$. In particular, we make precise how groups
of aggregate element instances are obtained from ground rules in ${P}^{\eta}$.

######  Definition 18.

Let $P$ be an aggregate program, and ${G}^{\epsilon}$ and ${G}^{\eta}$ be
subsets of ground instances of rules in ${P}^{\epsilon}$ and ${P}^{\eta}$,
respectively. Furthermore, let $a$ be an aggregate occurring in some rule
$r\in P$ and $\sigma$ be a substitution mapping the global variables in $a$ to
ground terms.

We define

$\displaystyle\epsilon_{r,a}({G}^{\epsilon},\sigma)$
$\displaystyle=\bigcup_{g\in{G}^{\epsilon}}\textnormal{{match}}(r_{a}\sigma,g)$
where $r_{a}$ is a rule of form (21) for aggregate occurrence $a$, and
$\displaystyle\eta_{r,a}({G}^{\eta},\sigma)$
$\displaystyle=\\{e\sigma\theta\mid g\in{G}^{\eta},e\in
E,\theta\in\textnormal{{match}}(r_{e}\sigma,g)\\}$

where $E$ are the aggregate elements of $a$ and $r_{e}$ is a rule of form (22)
for aggregate element occurrence $e$ in $a$.

Given that $\sigma$ maps the global variables in $a$ to ground terms,
$r_{a}\sigma$ is ground whereas $r_{e}\sigma$ may still contain local
variables from $a$. The set $\epsilon_{r,a}({G}^{\epsilon},\sigma)$ has an
indicative nature: For an aggregate $a\sigma$, it contains the identity
substitution when the result of applying its aggregate function to the empty
set is in accord with its bound, and it is empty otherwise. The construction
of $\eta_{r,a}({G}^{\eta},\sigma)$ goes one step further and reconstitutes all
ground aggregate elements of $a\sigma$ from variable bindings obtained by
rules in ${G}^{\eta}$. Both functions play a central role below in defining
the function Propagate for deriving ground aggregate placeholders of form 20
from ground rules in ${G}^{\epsilon}$ and ${G}^{\eta}$.

######  Example 22.

We show how to extract aggregate elements from ground instances of rules
($r_{3}$) and ($r_{4}$) in Example 21.

Let ${G}^{\epsilon}$ be empty and ${G}^{\eta}$ be the program consisting of
the following rules:

$\displaystyle\eta_{e_{1},a,r}(60,c_{1},c_{2})\leftarrow{}$
$\displaystyle\mathit{owns}(c_{1},c_{2},60)$ $\displaystyle{}\wedge{}$
$\displaystyle\mathit{company}(c_{1})\wedge\mathit{company}(c_{2})\wedge
c_{1}\neq c_{2},$ $\displaystyle\eta_{e_{1},a,r}(20,c_{1},c_{3})\leftarrow{}$
$\displaystyle\mathit{owns}(c_{1},c_{3},20)$ $\displaystyle{}\wedge{}$
$\displaystyle\mathit{company}(c_{1})\wedge\mathit{company}(c_{3})\wedge
c_{1}\neq c_{3},$ $\displaystyle\eta_{e_{1},a,r}(35,c_{2},c_{3})\leftarrow{}$
$\displaystyle\mathit{owns}(c_{2},c_{3},35)$ $\displaystyle{}\wedge{}$
$\displaystyle\mathit{company}(c_{2})\wedge\mathit{company}(c_{3})\wedge
c_{2}\neq c_{3},$ $\displaystyle\eta_{e_{1},a,r}(51,c_{3},c_{4})\leftarrow{}$
$\displaystyle\mathit{owns}(c_{3},c_{4},51)$ $\displaystyle{}\wedge{}$
$\displaystyle\mathit{company}(c_{3})\wedge\mathit{company}(c_{4})\wedge
c_{3}\neq c_{4},\text{\ and\ }$
$\displaystyle\eta_{e_{2},a,r}(35,c_{2},c_{1},c_{3})\leftarrow{}$
$\displaystyle\mathit{controls}(c_{1},c_{2})\wedge\mathit{owns}(c_{2},c_{3},35)$
$\displaystyle{}\wedge{}$
$\displaystyle\mathit{company}(c_{1})\wedge\mathit{company}(c_{3})\wedge
c_{1}\neq c_{3}.$

Clearly, we have $\epsilon_{r,a}({G}^{\epsilon},\sigma)=\emptyset$ for any
substitution $\sigma$ because ${G}^{\epsilon}=\emptyset$. This means that
aggregate $a$ can only be satisfied if at least one of its elements is
satisfiable. In fact, we obtain non-empty sets $\eta_{r,a}({G}^{\eta},\sigma)$
of ground aggregate elements for four substitutions $\sigma$:

$\displaystyle\eta_{r,a}({G}^{\eta},\sigma_{1})$
$\displaystyle=\\{60:\mathit{owns}(c_{1},c_{2},60)\\}$ for
$\displaystyle\sigma_{1}:X\mapsto c_{1},Y\mapsto c_{2},$
$\displaystyle\eta_{r,a}({G}^{\eta},\sigma_{2})$
$\displaystyle=\\{51:\mathit{owns}(c_{3},c_{4},51)\\}$ for
$\displaystyle\sigma_{2}:X\mapsto c_{3},Y\mapsto c_{4},$
$\displaystyle\eta_{r,a}({G}^{\eta},\sigma_{3})$ $\displaystyle=\hbox
to0.0pt{$\\{35,c_{2}:\mathit{controls}(c_{1},c_{2})\wedge\mathit{owns}(c_{2},c_{3},35)$;\hss}$
$\displaystyle\phantom{{}=\\{}20:\mathit{owns}(c_{1},c_{3},20)\\}$ for
$\displaystyle\sigma_{3}:X\mapsto c_{1},Y\mapsto c_{3},\text{\ and\ }$
$\displaystyle\eta_{r,a}({G}^{\eta},\sigma_{4})$
$\displaystyle=\\{35:\mathit{owns}(c_{2},c_{3},35)\\}$ for
$\displaystyle\sigma_{4}:X\mapsto c_{2},Y\mapsto c_{3}.$

For capturing the result of grounding aggregates relative to groups of
aggregate elements gathered via ${P}^{\eta}$, we restrict their original
translation to subsets of their ground elements. That is, while $\pi(a)$ and
${\pi_{a}}(\cdot)$ draw in Definition 9 on all instances of aggregate elements
in $a$, their counterparts ${\pi_{G}}(a)$ and ${\pi_{a,G}}(\cdot)$ are
restricted to a subset of such aggregate element instances:888Note that the
restriction to sets of ground aggregate elements is similar to the one to two-
valued interpretations in Definition 10.

######  Definition 19.

Let $a$ be a closed aggregate and of form (8), $E$ be the set of its aggregate
elements, and $G\subseteq\mathrm{Inst}(E)$ be a set of aggregate element
instances.

We define the translation ${\pi_{G}}(a)$ of $a$ w.r.t. $G$ as follows:

$\displaystyle{\pi_{G}}(a)$
$\displaystyle={\\{{\tau(D)}^{\wedge}\rightarrow{{\pi_{a,G}}(D)}^{\vee}\mid
D\subseteq G,D\mathrel{\not\kern-1.0pt\triangleright}a\\}}^{\wedge}$ where
$\displaystyle{\pi_{a,G}}(D)$ $\displaystyle=\\{{\tau(C)}^{\wedge}\mid
C\subseteq G\setminus D,C\cup D\triangleright a\\}.$

As before, this translation maps aggregates, possibly including non-global
variables, to a conjunction of (ground) $\mathcal{R}$-rules. The resulting
$\mathcal{R}$-formula is used below in the definition of functions Propagate
and Assemble.

######  Example 23.

We consider the four substitutions $\sigma_{1}$ to $\sigma_{4}$ together with
the sets $G_{1}=\eta_{r,a}({G}^{\eta},\sigma_{1})$ to
$G_{4}=\eta_{r,a}({G}^{\eta},\sigma_{4})$ from Example 22 for aggregate $a$.

Following the discussion after Proposition 24, we get the formulas

$\displaystyle{\pi_{G_{1}}}(a\sigma_{1})$
$\displaystyle=\mathit{owns}(c_{1},c_{2},60),$
$\displaystyle{\pi_{G_{2}}}(a\sigma_{2})$
$\displaystyle=\mathit{owns}(c_{3},c_{4},51),$
$\displaystyle{\pi_{G_{3}}}(a\sigma_{3})$
$\displaystyle=\mathit{controls}(c_{1},c_{2})\wedge\mathit{owns}(c_{2},c_{3},35)\wedge\mathit{owns}(c_{1},c_{3},20)\text{,
and\ }$ $\displaystyle{\pi_{G_{4}}}(a\sigma_{4})$ $\displaystyle=\bot.$

The function Propagate yields a set of ground atoms of form (20) that are used
in Algorithm 2 to ground rules having such placeholders among their body