3.1 Logic programs and their semantics

Many-sorted first-order formulas. We assume a many-sorted signature consisting of two sorts, integer and general, where the integer sort is a subsort of the general sort. This signature contains arithmetic functions such as $+$ , $-$ , and $\times$ , whose argument and value sorts are integer, and comparison predicate constants such as $\leq$ or $\gt$ , whose argument sorts are of sort general. We use infix notation for these arithmetic function and predicate constants. This signature also contains as object constants of sort integer all numerals $\overline {0},\overline {1},\overline {-1},\overline {2},\dots$ . We often identify numerals with integers and just write $0$ instead of $\overline {0}$ , but sometimes it is important to distinguish them. When it is important to distinguish a numeral that is an element of the signature from an underlying integer we will use an overline. This notation allows us to distinguish between expressions $\overline {5+3}$ and $\overline {5}+\overline {3}$ . The former is identified with the numeral $\overline {8}$ , whereas the later is identified with an algebraic expression that encodes function application to two numerals $\overline {5}$ and $\overline {3}$ . In the remainder we use the overline only in cases exemplified by expression $\overline {5+3}$ . We assume that for every sort, an infinite sequence of object variables of that sort is chosen. Terms over a signature $\sigma$ are defined recursively as usual with the addition that arguments of functions have to be of appropriate sorts. Atomic formulas over $\sigma$ are either (i) expressions of the form $p(t_1,\dots ,t_n)$ , where $p$ is a predicate constant and $t_1,\dots ,t_n$ are terms such that their sorts are subsorts of the argument sorts $s_1,\dots ,s_n$ of $p$ , or (ii) expressions of the form $t_1=t_2$ , where $t_1$ and $t_2$ are terms. (First-order) formulas over signature $\sigma$ are formed from atomic formulas and the 0-place connective $\bot$ (falsity) using the binary connectives $\land$ , $\lor$ , $\to$ and the quantifiers $\forall$ , $\exists$ . The other connectives are treated as abbreviations: $\neg F$ stands for $F\to \bot$ and $F\leftrightarrow G$ stands for $(F\to G)\land (G\to F)$ . A term or other expression is called ground if it contains no variables. A ground expression is called precomputed if it contains no arithmetic function constants. For instance, $p(f(1))$ is precomputed, whereas $p(1+2)$ is ground but not precomputed.

A rule is a formula of the form $\mathit{Head} \leftarrow \mathit{Body}$ (or, $\texttt {Head :- Body}$ in source code format), where $\mathit{Head}$ is an atomic formula or $\bot$ , and $\mathit{Body}$ is a list of literals, that is, atomic formulas possibly preceded by one or two occurrences of $not$ . A program is a set of rules.

Every rule can be identified with some first-order formula over signature $\sigma$ (Fandinno et al. Reference Fandinno, Lifschitz, Lühne and Schaub2020). Thus, a program can be seen as a first-order theory over $\sigma$ . The translation from rules to formulas is not trivial due to the need to handle all possible terms occurring in the rule. Here, we use a simplified version of this translation, which is sufficient for the examples considered in this paper. Formal results apply to any translation that captures the intended meaning of rules as formulas. We identify each rule $\mathit{Head} \leftarrow \mathit{Body}$ with the universal closure of the formula $B \to \mathit{Head}$ , where $B$ is the conjunction of all literals in $\mathit{Body}$ after replacing $\mathit{not}$ by $\neg$ . In the resulting formulas, every variable or constant occurring as an argument of an arithmetic function is assumed to be of the sort integer, similarly to the translation by Lifschitz (Reference Lifschitz2021). We often write rules as formulas $B \to \mathit{Head}$ omitting the reference to the universal closure. For instance, we identify the rule listed in Line 4 of Listing 1 with the universal closure of formula $q(N-1,k) \to q(N,k+1),$ where $N$ is a variable and $k$ is an object constant, both of the integer sort.

Interpretations are defined as usual for many-sorted first-order languages (Lifschitz et al. Reference Lifschitz, Morgenstern and Plaisted2008, Section 1.2.2). An interpretation $I$ of a signature $\sigma$ is standard if it satisfies the following conditions:

• • its domain of the sort integer is the set of all numerals, and its domain of the sort general contains all precomputed terms,

• • all numerals and object constants of the sort general are interpreted as themselves,

• • arithmetic function are interpreted as customary in arithmetic, and

• • predicate constants corresponding to comparison are interpreted according to some fixed total order such that numerals are contiguous and ordered as usual.

The value $t^I$ assigned to a ground term $t$ over $\sigma$ by an interpretation $I$ and the satisfaction relation (denoted, $\models$ ) between an interpretation of $\sigma$ and a sentence over $\sigma$ are defined recursively, in the usual way (Lifschitz et al. Reference Lifschitz, Morgenstern and Plaisted2008, Section 1.2.2). An interpretation is called a model of a theory – a (possibly infinite) set of sentences – when it satisfies every sentence in this theory.

Pearce and Valverde (Reference Pearce and Valverde2004, Reference Pearce and Valverde2005) introduced the quantified logic of here-and-there. One of its applications is an alternative definition of stable models for logic programs. A key benefit of this alternative is that it bypasses a reference to a grounding process when characterizing stable models. The many-sorted case of the quantified logic of here-and-there was recently studied by Fandinno et al. (Reference Fandinno, Lifschitz and Temple2024). We review it here considering a signature $\sigma$ as described above and standard interpretations. We start by introducing some notation. Let $I$ to be a standard interpretation over signature $\sigma$ . If $\mathbf{t}$ is a tuple $t_1,\dots ,t_n$ of ground terms, then $\mathbf{t}^I$ is the tuple $t_1^I,\dots ,t_n^I$ of values. By $\mathcal{A}_{I}$ we denote the set of atoms of the form $p(\mathbf{t})$ such that $I \models p(\mathbf{t})$ , where $p$ is a predicate symbol and $\mathbf{t}$ is a tuple of precomputed terms. An HT-interpretation over $\sigma$ is a pair $\langle \mathcal{H},I\rangle$ , where $I$ is a standard interpretation and $\mathcal{H}\subseteq \mathcal{A}_{I}$ . (In terms of Kripke models with two worlds, $\mathcal{H}$ describes the predicates in the here-world and $I$ captures the there-world). The satisfaction relation ${\models }_{\!\!\scriptscriptstyle \rm ht}$ between HT-interpretation $\langle \mathcal{H}, I\rangle$ of $\sigma$ and a sentence $F$ over $\sigma ^I$ is defined recursively:

• • $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} p(\mathbf{t})$ , if $p(\mathbf{t}^I)\in \mathcal{H}$ ;

• • $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} t_1=t_2$ if $t_1^I=t_2^I$ ;

• • $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} F\land G$ if $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} F$ and $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} G$ ;

• • $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} F\lor G$ if $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} F$ or $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} G$ ;

• • $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} F\to G$ if (i) $\langle \mathcal{H}, I\rangle \not {{\models }_{\!\!\scriptscriptstyle \rm ht}} F$ or $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} G$ , and (ii) $I \models F\to G$ ;

• • $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}}\forall X F(X)$ with $X$ of the general sort, if $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} F(t)$ for every precomputed term $t$ ;

• • $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}}\forall X F(X)$ with $X$ of the integer sort, if $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} F(\overline {n})$ for every integer $n$ ;

• • $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}}\exists X F(X)$ with $X$ of the general sort, if $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} F(t)$ for some precomputed term $t$ ;

• • $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}}\exists X F(X)$ with $X$ of the integer sort, if $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} F(\overline {n})$ for some integer $n$ .

If $\langle \mathcal{H}, I\rangle {{\models }_{\!\!\scriptscriptstyle \rm ht}} F$ holds, we say that $\langle \mathcal{H}, I\rangle$ satisfies $F$ and that $\langle \mathcal{H}, I\rangle$ is an HT-model of $F$ .

It is easy to see that $(\mathcal{A}_{I},I)$ is an HT-model of a sentence $F$ whenever $I$ is a model of $F$ . About a model $I$ of a theory $\Gamma$ , we say it is stable if, for every proper subset $\mathcal{H}$ of $\mathcal{A}_{I}$ , HT-interpretation $\langle \mathcal{H},I \rangle$ does not satisfy $\Gamma$ . In application to theories of a single sort (and thus in the absence of arithmetic function symbols), this definition is equivalent to the original definition by Pearce and Valverde (Reference Pearce and Valverde2004, Reference Pearce and Valverde2005). In addition, if the theory is finite, then this definition of a stable model is also equivalent to the definition of such model in terms of the operator SM (Ferraris et al. Reference Ferraris, Lee and Lifschitz2007, Reference Ferraris, Lee and Lifschitz2011), when all predicate constants are considered to be “intensional”. In the sequel, we sometimes abuse our terminology and notation and identify set $\mathcal{A}_{I}$ of ground atoms with interpretation $I$ .

3.2 Parameterizable subprograms

We now review the key concepts introduced by Gebser et al. (Reference Gebser, Kaminski, Kaufmann and Schaub2019) when discussing the multi-shot framework. We then use these concepts to formally characterize the collective control described in Section 2. A program declaration is an expression of the form $\texttt {#program}\ m(p_1, \dots , p_j ),$ where $m, p_1, \dots , p_j$ are symbolic constants. We call $m$ the name of the declaration and $p_1, \dots p_j$ its parameters/placeholders. Different occurrences of program declarations with the same name are assumed to share the same parameters. In this way, each name is associated with a unique parameter specification. A clingo-program is a list of rules and declarations. Listings 1 exemplifies this concept. The scope of a program declaration in a clingo-program consists of the set of all rules following this declaration up to the next program declaration or the end of the list. In Listing 1, the scope of the declaration in Line 1 consists of atom q(0,0), while that in Line 3 contains q(N,k + 1):-(N-1,k). Given clingo-program $R$ along with a symbolic constant $m$ , we define $R(m)$ as the set of all rules in the scope of all occurrences of program declarations with name $m$ . We often refer to $R(m)$ as a subprogram of $R$ . All rules outside the scope of any (explicit) program declaration are thought of being implicitly preceded by #program base. Take $R_1$ to denote Listing 1, $R_1(base) = \{q(0,0)\}$ and $R_1(property)$ = $\{q(N-1,k) \to q(N,k+1) \}$ .

A valuation $v$ of a set of placeholders $\mathit{PH}$ is a function that maps elements in this set to precomputed terms. Given a program/formula $F$ , a set $\mathit{PH}$ of placeholders and valuation $v$ on $\mathit{PH}$ , by $v(F)$ we denote a program/formula constructed from $F$ by substituting each of the occurrences of some placeholder $c \in \mathit{PH}$ with the value $v(c)$ assigned to it by the valuation $v$ . Given a name $m$ with associated parameters/placeholders $p_1,\dots , p_j$ , and valuation $v$ on $\{p_1,\dots , p_j\}$ , we say that $v(R(m))$ is the $v$ -instantiation of subprogram $R(m)$ . For instance, if $v$ is the valuation $\{k \mapsto 42\}$ , then $v(R_1(property))$ consists of the universal closure of $q(N-1,42) \to q(N,42+1)$ . We are now almost ready to formally characterize the collective control that provides specifications for instantiations of subprograms of interest and then considers these collectively as the union. Let us define one more concept. A subprogram-spec is a triple $ [m,\mathit{PH},v],$ where $m$ is a name, $\mathit{PH}$ is a set of associated parameters/placeholders with $m$ , and $v$ is a valuation on $\mathit{PH}$ . Given (i) clingo-program $R$ and (ii) set $[m_1,\mathit{PH}_1,v_1],\dots ,[m_j,\mathit{PH}_j,v_j]$ of subprogram-specs, the collective control associates this pair with the logic program composed of the rules

(2) \begin{align} v_1(R(m_1))\cup v_2(R(m_2))\cup \cdots \cup v_j(R(m_j)). \end{align}

For instance, command line %clingo property -c n = 100 (discussed in Section 2) assumes clingo-program in Listing 1 and the set composed of the following subprogram-specs: $[base,\emptyset ,()],\ [property,\{k\},(k\mapsto 0)],\ \cdots ,\ [property,\{k\},(k\mapsto 99)].$ Although clingo-programs provide means to group rules into subprograms, the expression (2) clearly states that the object resulting from an application of the collective control to a clingo-program looses any aspect of the modularity.

As customary in logic programming, its programs define signatures implicitly. Namely, predicate and object symbols occurring in a program form its signature. If arithmetic operations are present the signature is infinite containing all numerals.

4.1 Simple intensionality statements

Fandinno and Lierler (Reference Fandinno and Lierler2023) introduced intensionality statements to generalize the notion of intensional predicate constants. This concept allows some predicate constants to be intensional on some arguments while being extensional on others. This fine granularity came with the price that checking certain interesting properties is an undecidable problem. In particular, this is true for deciding whether the granular version of splitting theorem studied by Fandinno and Lierler (Reference Fandinno and Lierler2023) is applicable. In the sequel, the splitting theorem by Fandinno and Lierler (Reference Fandinno and Lierler2023) plays an important role. For these reasons, we find of value to focus on a special case of intensionality statements, which we call simple. Despite the fact that they are less general they are sufficient for our purposes and importantly more tractable. Before we proceed towards the presentation of the formal definitions let us take a moment to discuss the terms intensional and extensional. This terminology roots in deductive databases, where tuples in the database are seen as purely extensional in the sense that the whole extension of the predicate is known. Derived predicates are then purely intensional in the sense that only their definition is fixed. Here, we adjust this terminology to allow ourselves to be more detailed. We can point at a predicate and some of its arguments as the ones being “defined”, while the same predicate on the remaining arguments is considered “known”. This is important in our context. Indeed, as mentioned in the introduction, one of the distinguished uses of $\mathit{ASP}\!+\!\mathit{control}$ is for modeling dynamic domains. These applications form a natural example where the same predicate is used both as intensional and extensional depending on its arguments. In a modular program describing a dynamic domain, a subprogram may naturally represent the effects of the actions at a given time step, where the same predicate is used to represent the state of the world at different time steps. In this case, the predicate is intensional for the arguments representing the current time step, and extensional for the arguments representing the previous time step.

A simple intensionality statement $\kappa$ over a signature $\sigma$ is a function mapping each predicate symbol $p/n$ in $\sigma$ to a set of $n$ -tuples satisfying the following conditions: (i) each element of the tuple is either a variable or a precomputed term of $\sigma$ , and (ii) no variable occurs twice in a tuple. In the following, we name the $i$ -th element of a tuple assigned by a simple intensionality statement as $X_i$ and variations when it is a variable. We say that a predicate symbol is (purely) extensional when its associated set is empty, and that it is (purely) intensional when it contains a tuple of variables (with no ground terms). When all predicate symbols are purely intensional or purely extensional, then the simple intensionality statement corresponds to the notion of intensional predicate constants (Ferraris et al. Reference Ferraris, Lee and Lifschitz2011). When the arity of $p/n$ is clear from the context, we write $\kappa ^p$ instead of $\kappa (p/n)$ . Consider, for instance, predicate symbol $\mathit{q}/2$ and let $\kappa ^{\mathit{q}}$ be set $\{ \langle X,1 \rangle , \langle X,2 \rangle \}$ . Intuitively, this intensionality statement states that the ground atoms formed by predicate constant $q$ with its arguments of the form $\langle t,1 \rangle$ or $\langle t,2 \rangle$ are intensional for any term $t$ ; otherwise, these atoms are extensional. For an intensionality statement $\kappa$ and a predicate symbol $p/n$ , by ${\lambda }_\kappa ^p(\mathbf{X})$ we denote the formula

(3) \begin{align} \bigvee _{(t_1,\dots t_n)\in \kappa ^p} \left({\bigwedge _{\small \begin{array}{c} t_i \hbox{ is not a variable}\\ (1\le i\le n)\end{array}}{X_i=t_i}}\right) \end{align}

where $\mathbf{X} = \langle X_1,\dots ,X_n \rangle$ is a tuple of distinct variables of the appropriate length and sort (in the sequel we adopt this convention and use $\mathbf{X}$ to denote tuples of variables). To each simple intensionality statement $\kappa$ , we associate a set $\mathit{EM}(\kappa )$ of sentences, called the extensional axioms of $\kappa$ , containing a sentence of the form

(4) \begin{gather} \forall \mathbf{X} \left ( \neg {\lambda }_\kappa ^p(\mathbf{X}) \to p(\mathbf{X}) \vee \neg p(\mathbf{X}) \right ) \end{gather}

for every predicate symbol $p/n$ in $\sigma$ . For a theory $\Gamma$ over $\sigma$ , we say that a standard interpretation $I$ is $\kappa$ -stable if it is a stable model of $\Gamma \cup \mathit{EM}(\kappa )$ . When it is clear from the context we sometimes drop $\kappa$ as a subscript of ${\lambda }_\kappa ^p$ .

Let us illustrate these concepts on examples. Assume the signature $\sigma _1$ composed of a single predicate $q$ . Consider $\kappa _1^{\mathit{q}} = \{ \langle X,1 \rangle , \langle X,2 \rangle \}$ ; then ${\lambda }_1^{\mathit{q}}(X_1,X_2)$ is $(X_2 = 1 \vee X_2 = 2)$ (here and in the sequel we understand ${\lambda }_i$ as an abbreviation for ${\lambda }_{\kappa _i}$ ). Thus, extensional axioms formula $\mathit{EM}(\kappa _1)$ is equivalent to the the universal closure of

(5) \begin{gather} \big (X_2 \neq 1\wedge X_2 \neq 2\big ) \rightarrow \big (q(X_1,X_2)\vee \neg q(X_1,X_2)\big ). \end{gather}

Consider theory $\Gamma _1$ composed of the universal closures of formulas $q(X,0)\rightarrow q(X,1),$ and $q(X,1)\rightarrow q(X,2).$ Sets $\{ q(1,3)\} \hbox{ and } \{q(0,0), q(0,1), q(0,2)\}$ are among the $\kappa _1$ -stable models of $\Gamma _1$ . In case of the former, note that $q/2$ is not intensional for $\langle 1,3 \rangle$ and hence the extensional axiom (5) allows $q(1,3)$ to be either true or false. In case of the latter, note that $q/2$ is not intensional for $\langle 0,0 \rangle$ either; hence, the extensional axiom allows $q(0,0)$ to be either true or false. Atoms $q(0,1)$ and $q(0,2)$ must now be true. On the other hand, set $\{ q(0,1) \}$ is not a $\kappa _1$ -stable model of $\Gamma _1$ because $q/2$ is intensional for $\langle 0,1 \rangle$ and there is no rule to derive it from.

There are some well known general properties about traditional logic programs and their stable models. For example, we can conclude that an atom is not a member of any answer set when it does not occur as a head of any rule. A similar result is also the case for $\kappa$ -stable models. Proposition1 below presents this result formally. We call a substitution $\theta$ simple with respect to signature $\sigma$ whenever all values assigned by $\theta$ are precomputed terms over $\sigma$ (we drop the reference to the signature when it is clear from the context).

Intuitively, condition $I\models {\lambda }_{\kappa }^p(\mathbf{t})$ means that given a simple intensionality statement $\kappa$ , theory $\Gamma$ “defines” this predicate on the tuples associated with it.

4.2 Modules and modular programs

A module over signature $\sigma$ is a pair $\langle {\kappa },{\Pi } \rangle$ , where $\kappa$ is a simple intensionality statement over $\sigma$ and $\Pi$ is a program over $\sigma$ ; we say that a $\kappa$ -stable model of $\Pi$ is a model of the module. For instance, consider module $\Delta _1$ over $\sigma _1$ to stand for $ \langle {\kappa _1},{\Gamma _1} \rangle ,$ where $\sigma _1$ , $\kappa _1$ and $\Gamma _1$ are defined in Section 4.1. The models of $\Delta _1$ are the $\kappa _1$ -stable models of $\Gamma _1$ .

A modular program $\mathcal{P}$ is a pair $\langle \kappa , \mathcal{M} \rangle$ where $\kappa$ is a simple intensionality statement and $\mathcal{M} = \{ \Delta _1,\dots ,\Delta _n \}$ is a finite set of modules over $\sigma$ such that

(6) \begin{gather} \text{$\forall \mathbf{X} \left ( {\lambda }_i^p(\mathbf{X}) \to {\lambda }^p(\mathbf{X}) \right )$ is valid} \end{gather}

for every predicate symbol $p/n$ in $\sigma$ and every module $\Delta _i$ in $\mathcal{M}$ ; where ${\lambda }^p$ and ${\lambda }_i^p$ respectively are the formulas associated with $p/n$ by $\kappa$ and each $\kappa _i$ . Intuitively, condition (6) states that every atom defined in a submodule must be intensional in the modular program. A standard interpretation $I$ is a stable model/answer set of $\mathcal{P}$ if it is a model of each of its modules $\Delta _i$ and it satisfies formula

(7) \begin{gather} \forall {\mathbf{X}}\big ({\lambda }^p(\mathbf{X}) \wedge \neg {\lambda }_1^p(\mathbf{X}) \wedge \dotsc \wedge \neg {\lambda }_n^p(\mathbf{X}) \to \neg p(\mathbf{X})\big ) \end{gather}

for every predicate symbol $p/n$ in $\sigma$ . Intuitively, formula (7) states that every intensional atom that is not defined in any submodule must be false in all stable models.

Consider a sample modular program $\mathcal{P}_1$ over $\sigma _1$ whose simple intensionality statement is defined by $\kappa ^q=\langle X,Y \rangle$ (in other words, predicate symbol $q$ is purely intensional); and set of modules consists of $\Delta _0$ , $\Delta _1$ and $\Delta _2$ , where

\begin{align*} \Delta _0 &= \langle {\kappa _0},{ \{ q(0,0) \} } \rangle ,\hbox{ and}\\ \Delta _2 &= \langle {\kappa _2},{ \{ q(0,2)\rightarrow q(0,3), q(0,3)\rightarrow q(0,4) \} } \rangle \end{align*}

with $\kappa _0^{\mathit{q}} = \{ \langle 0,0 \rangle \}$ and $\kappa _2^{\mathit{q}} = \{ \langle X,3 \rangle , \langle X,4 \rangle \}$ ; and $\Delta _1$ is understood as earlier. The only stable model of $\mathcal{P}_1$ is

(8) \begin{gather} \{q(0,0),\ q(0,1),\ q(0,2),\ q(0,3),\ q(0,4)\}. \end{gather}

We assume that an empty conjunction is equivalent to $\top$ . The condition (7) for $q$ is equivalent to the universal closure of $(X_1 \neq 0 \wedge X_2 = 0) \vee \neg (0 \leq X_2 \leq 4) \to \neg q(X_1,X_2).$ Hence, every atom of the form $q(t_1,t_2)$ is false when both $t_1 \neq 0$ and $t_2 = 0$ or when $t_2 \not \in \{0,1,2,3,4\}$ . All models of $\Delta _1$ where $q(t_1,0)$ is false must also satisfy that $q(t_1,1)$ and $q(t_2,2)$ are false, and all models of $\Delta _2$ where $q(t_1,2)$ is false must also satisfy that $q(t_1,3)$ and $q(t_1,4)$ are false. Since $q(t_1,0)$ is false for every $t_1 \neq 0$ , then atoms $q(t_1,t_2)$ with $t_1 \neq 0$ and $t_2 \in \{1,2,3,4\}$ must be false as well. Hence, it remains to discuss atoms of the form $q(0,t_2)$ with $t_2 \in \{0,1,2,3,4\}$ . Atom $q(0,0)$ must be true because all the models of $\Delta _0$ satisfy it. Atoms $q(0,1)$ and $q(0,2)$ must be true because they are true in the only models of $\Delta _1$ satisfying $q(0,0)$ . Atoms $q(0,3)$ and $q(0,4)$ must be true because they are true in the only models of $\Delta _2$ satisfying $q(0,2)$ . Note that, set (8) is exactly the unique $\kappa$ -stable model of the program containing all rules in $\Delta _0$ , $\Delta _1$ and $\Delta _2$ . This is not a coincidence, as we show in the next section.

Relation between modular programs and non-modular ones. For every term $t$ , we define $[t]$ recursively as follows:

• • if $t$ is a variable or a precomputed term, then $[t] = t$ ;

• • if $t$ is $t_1 \odot t_2$ with $\odot \in \{ +, -, \times \}$ and both $t_1$ and $t_2$ are ground terms, then $[t]$ is the numeral $\overline {n_1 \odot n_2}$ with $\overline {n_1} = [t_1]$ and $\overline {n_2} = [t_2]$ ;

• • if $t$ is $t_1 \odot t_2$ with $\odot \in \{ +, -, \times \}$ and at least one of $t_1$ and $t_2$ is a variable, then $[t]$ is the expression $[t_1] \odot [t_2]$ ;

For example, $[0+1] = 1$ , and $[X+1] = X + 1$ . If $\mathbf{t} = (t_1,\dots ,t_n)$ is a tuple of terms, then $[\mathbf{t}]$ denotes the tuple $([t_1],\dots ,[t_n])$ .

A module $\langle {\kappa },{\Pi } \rangle$ is called simple when for every atom $p(\mathbf{t})$ in the head of a rule in $\Pi$ , there is a tuple $\mathbf{u}$ in $\kappa ^p$ and a substitution $\theta$ such that $[\mathbf{t}] = \mathbf{u}\theta$ . A modular program is called simple if all its modules are simple. Modular program $\mathcal{P}_1$ defined above is simple. Indeed, we can check that module $\Delta _1=\langle {\kappa _1},{\Gamma _1} \rangle$ is simple. We have two atoms in the heads of its rules, namely, $q(X,1)$ and $q(X,2)$ . A substitution that maps $X_1$ to $X$ will turn tuples in $\kappa _1$ into the arguments of these atoms. Similarly, we can check that modules $\Delta _0$ and $\Delta _2$ are also simple. As another example, let us consider module

(9) \begin{gather} \langle \{\langle X,1 \rangle \}, \{q(N-1,0) \to q(N,0+1) \} \rangle \end{gather}

which corresponds to the program $\mathit{property}(k)$ in Listing 1 with $k=0$ . This module is also simple. Take the substitution that maps $X$ to $N$ and note that $[{0}+{1}]$ is numeral $1$ .

We next introduce the notion of coherent modular program and show that every coherent modular program has the same stable models as a non-modular program obtained by taking the union of all rules in its modules. To do so, we need to introduce the notion of a dependency graph of a modular program. Given a modular program $\mathcal{P} = \langle \kappa , \{ \Delta _1,\dots ,\Delta _n \} \rangle$ , the (directed) graph of dependencies, denoted $\mathfrak{G}(\mathcal{P})$ , is defined as follows:

• • Its vertices are pairs $(p,i)$ with $p$ a predicate symbol and $1 \leq i \leq n$ .

• • It has an edge from $(p,i)$ to $(q,j)$ when for some rule $r$ of $\mathcal{P}$ ,

1. – there is an atom of the form $p(\mathbf{t})$ in the head of $r$ , and

2. – there is a nonnegated atom of the form of $q(\mathbf{t}')$ in the body of $r$ , and

3. – there are tuples $\mathbf{u}_i$ in $\kappa _i^p$ and $\mathbf{u}_j$ in $\kappa _j^q$ , and substitutions $\theta$ and $\theta '$ such that $[\mathbf{t}] = \mathbf{u}_i\theta$ and $[\mathbf{t}'] = \mathbf{u}_j\theta '$ .

We say that a strongly connected component of $\mathfrak{G}(\mathcal{P})$ is contained in module $\Delta _i$ if all vertices in this component are of the form $(p,i)$ .

As an example dependency graph $\mathfrak{G}(\mathcal{P}_1)$ contains three vertices $(q,0)$ , $(q,1)$ and $(q,2)$ and an edges from $(q,2)$ to $(q,1)$ and from $(q,1)$ to $(q,0)$ . It is easy to see that the strongly connected component $(q,i)$ is contained in module $\Delta _i$ for any $i \in \{0,1,2\}$ .

A simple modular program $\mathcal{P}$ is called coherent if it satisfies the following two conditions:

• • every strongly connected component of the dependency graph $\mathfrak{G}(\mathcal{P})$ is contained in some module; and

• • every pair of modules $\langle {\kappa _i},{\Pi _i} \rangle$ and $\langle {\kappa _j},{\Pi _j} \rangle$ in $\mathcal{P}$ satisfy that, for every predicate symbol $p$ , there is no pair of tuples $\mathbf{u}_i \in \kappa _i^p$ and $\mathbf{u}_j \in \kappa _j^p$ with $i \neq j$ , such that $\mathbf{u}_i$ and $\mathbf{u}_j$ unify. Two tuples $\mathbf{t}_i=\langle t^i_1,\dots t^i_m \rangle$ and $\mathbf{t}_j=\langle t^j_1,\dots t^j_m \rangle$ of terms unify if there is a substitution $\theta$ of the variables that applied to both $\mathbf{t}_i$ and $\mathbf{t}_j$ yields $t^i_k=t^j_k$ , $1\leq k\leq m$

4.3 Parametric modular logic programs

As illustrated in Section 3.2, in practice, modules are often defined in a parametric way, that is, in terms of some parameters that can be instantiated in different ways to obtain different modules. To capture this idea, we introduce the notion of parametric modules that generalize modules introduced in Section 4.2.

Consider a set $\mathit{PH}$ of object constants not occurring in $\sigma$ , then by $\sigma ^{\mathit{PH}}$ we denote the signature $\sigma$ extended with the object constants in $\mathit{PH}$ . By $\mathit{PH}^+$ we denote the signature composed of the object constants in $\mathit{PH}$ , numerals, and arithmetic function constants.

A parametric intensionality statement over $\sigma ^{\mathit{PH}}$ is a function mapping each predicate symbol $p/n$ in $\sigma$ to a set of $n$ -tuples satisfying the conditions:

• • each element of the tuple is either a variable, a precomputed term, or a ground term over signature $\mathit{PH}^+$ ;

• • no variable occurs twice in a tuple.

A parametric module over $\sigma$ is a triple $\big \langle \mathit{PH},\chi ,\Pi \big \rangle ,$ where $\chi$ is a parametric intensionality statement over $\sigma ^{\mathit{PH}}$ and $\Pi$ is a formula (program understood as a set of formulas) over $\sigma ^{\mathit{PH}}$ . In the sequel, to illustrate relevant concepts we use the parametric module

(10) \begin{equation} \langle \{k\}, \chi _1, \{q(N-1,k) \to q(N,k+1) \} \rangle , \end{equation}

where we assume the signature composed of a single predicate $q$ and parametric intensionality statement $\chi ^q_1$ is characterized by the singleton set consisting of $\langle X,k+1 \rangle$ .

Given a parametric intensionality statement $\chi$ over $\sigma ^{\mathit{PH}}$ and substitution $\Theta$ on $\mathit{PH}$ by $\chi \Theta$ we denote a function mapping each predicate symbol $p/n$ in $\sigma$ to the following set of $n$ -tuples $ \{{\langle [t_1\Theta ],\dots ,[t_n\Theta ] \rangle }\mid \langle t_1,\dots ,t_n \rangle \in \chi ^p\}.$ For a simple substitution $\Theta$ on $\mathit{PH}$ , $\chi \Theta$ forms a simple intensionality statement. (We defined simple substitutions in Section 4.1.)

For example, let $\Theta _1$ be a simple substitution that maps $k$ to precomputed term $1$ . Then

\begin{equation*} \begin{array}{lll} (q(N-1,k) \to q(N,k+1))\Theta _1&\hbox{ is }&q(N-1,1) \to q(N,1+1);\\ \chi _1^q\Theta _1&\hbox{ is }&\{\langle X,2 \rangle \}.\\ \end{array} \end{equation*}

Given a parametric module $\Phi =\big \langle \mathit{PH},\chi ,\Pi \big \rangle$ over signature $\sigma$ and a simple substitution $\Theta$ on $\mathit{PH}$ , we can construct a module $\Phi _\Theta =\langle \chi \Theta ,\Pi \Theta \rangle$ (as introduced in Section 4.2). In the scope of this section it is convenient to call such modules instances. The signature of any instance of the parametric module is that of a parametric module, namely, $\sigma$ . When the set of placeholders $\mathit{PH}$ is empty in a considered parametric module, it serves a role of an instance itself.

For example, let $D^k$ denote parametric module in (10). Take $\Theta _0$ be a simple substitution that maps $k$ to precomputed term $0$ . Then, instance $D^k_{\Theta _0}$ coincides with module (9). Similarly, if $\Theta _1$ is a simple substitution that maps $k$ to precomputed term $1$ , then instance $D^k_{\Theta _1}$ stands for $\langle \{\langle X,2 \rangle \}, \{q(N-1,1) \to q(N,1+1) \} \rangle$ .

We are ready to look into the example discussed in Section 2, namely, property parametric-program (Listing 1) that comes with collective control (A). We identify subprogram property(k) with parametric module $D^k$ ( $k\geq 0$ ) introduced above. Substitutions $\Theta _i$ ( $0\leq i\leq n$ ) map parameter $k$ into precomputed term (integer) $i$ . We identify subprogram $base$ in the running example with a parametric module

(11) \begin{equation} \langle \emptyset ,\{\langle 0,0 \rangle \}, \{q(0,0) \} \rangle \end{equation}

that we denote as $D$ and which coincides with the module $\Delta _0$ introduced in Section 4.2 (this module is an instance itself as its set of placeholders is empty). We view the property parametric-program together with the collective control as modular program

(12) \begin{equation} \langle \kappa ,\{ D, D^k_{\theta _0},\dots ,D^k_{\theta _n}\} \rangle , \end{equation}

where the signature of this modular program contains predicate $q/2$ and the simple intentionality statement $\kappa$ defines $q$ as purely intensional. This modular program has a unique answer set, which, for example, in case when $n=99$ coincides with the answer set of program (1). This last observation is not a coincidence and is supported by Theorem2. In fact, that theorem gives us formal grounds for our earlier actions of identifying subprograms $base$ and property(k) with parametric modules $D$ and $D^k$ ( $k\geq 0$ ), respectively.