Parametric Modular Answer Set Programs Made Declarative

TPLP: Page 1–8.

© The Author(s), 2021. Published by Cambridge University Press 2021

1

doi:10.1017/xxxxx

Parametric Modular Answer Set Programs Made Declarative JORGE FANDINNO University of Nebraska Omaha, USA

arXiv:2605.22716v1 [cs.AI] 21 May 2026

YULIYA LIERLER University of Nebraska Omaha, USA

TORSTEN SCHAUB University of Potsdam, Germany

submitted xx xx xxxx; revised xx xx xxxx; accepted xx xx xxxx

Abstract In this paper, we explore the concept of modularity in first-order answer set programming (ASP). We introduce a new formalism called parametric modular logic programs, which allows defining subprograms with parameters and intensionality statements. We demonstrate how this formalism can capture the semantics of clingo-programs with collective control, a feature that enables structuring and instantiating subprograms. We provide theoretical foundations for modular ASP, illustrate its usefulness, and connect to traditional non-modular ASP. KEYWORDS: Answer Set Programming, Modularity, Formal Methods

1 Introduction Answer set programming (ASP) is a well-established declarative logic programming paradigm under the answer set/stable models semantics (Gelfond and Lifschitz 1988). The ASP methodology relies on devising a logic program so that its answer sets are in one-to-one correspondence to the solutions of the target problem. This approach is fully declarative, since the logic program only describes a problem and conditions on its solutions, not the way to obtain them. The latter is delegated to systems called answer set solvers. A software engineer is then tasked with translating problem’s specifications into the formal language of logic programs rather than devising algorithms for obtaining solutions to a problem. Under these circumstances both the art of programming and the construction of an argument for code’s correctness become more direct (Cabalar et al. 2020; Fandinno et al. 2020; Hansen and Lierler 2025; Fandinno et al. 2025). This is essential in building trustworthy software solutions, making ASP a viable role player in the current programming landscape. Yet, to realize the full potential of ASP more attention to its theoretical and practical aspects have to be paid. Here, we target advancing theoretical foundations of the “modularity” frontiers of this programming paradigm. Modularity is one of the key techniques in principled software development, and it is essential for modeling large-scale practical applications. It provides a solid abstraction to study distinct approaches to solving a problem by identifying modules/parts of code that

2 are responsible for different aspects and helps in constructing arguments of correctness by decomposing the argument about the whole program into arguments about its components (Cabalar et al. 2020). In general, traditional ASP programs lack modularity because subsections of the code cannot be evaluated in isolation. Most well known variants of ASP systems — lparse-smodels pair, earlier versions of clingo, dlv — expect a program at its full length bypassing any support for modularity. Yet, researchers realized early the importance of this aspect. Theoretical and practical advances exist. For instance, Oikarinen and Janhunen (2006; 2008) and Janhunen et al. (2007) devise a propositional modular framework for answer set programming and introduce concepts of equivalence for such programs; Harrison and Lierler (2016) introduce first-order modular logic programs. Lifschitz and Turner (1994) proposed splitting as a tool to “modularize” otherwise monolithic logic programs. Mentioned works were at the origin of more theoretical advances refining their proposals. On the practical side, Gebser et al. (2014) describe the ASP +control framework that, for example, allows encodings which include time horizons and assume repetitive code for each time step mimicking settings of planning domains. This framework was implemented within clingo 4. A PDDL planner plasp backed up by ASP technology utilizes this feature (Dimopoulos et al. 2017). Multi-shot solving (Gebser et al. 2019) became one of the staples of clingo 5. It prominently positions an interactive mode of programming with ASP making control over ASP “modules” simple. Yet, control equates with a procedure that encroaches on the declarativness of ASP. In this paper, we study how “first-order modules” and “control” can be given a declarative meaning, by tackling on particular kind of control that we call collective. This work is a foundational step towards making the concepts pertaining (i) ASP modules as they are used in practice and (ii) control precise, well understood and declarative. This allow us to construct arguments of correctness for logic programs with collective control. This paper is organized as follows. We start by introducing a motivating example. We then introduce theoretical preliminaries. Modular programs are introduced as the basis for what we call parametrized modular logic programs. We conclude by illustrating how parametrized modular programs capture the semantics of programs such as the one discussed as a motivating example. We use this example to showcase possible formal claims that can be seen as arguments of correctness for modular ASP programs.

2 Motivating Examples We start by introducing a simple example that illustrates the key concepts of parametric modular logic programs and collective control. Listing 1. The property parametric-program #program base. q(0,0). #program property(k). q(N,k+1) :- q(N-1,k).

1 2 3 4

Listing 1 contains two subprograms base and property(k). Keyword base marks a dedicated subprogram (with an empty parameter list). The base subprogram in Listing 1 includes the single fact q(0,0). Without further control instructions, clingo grounds and solves the base subprogram only. This yields the standard behavior of answer set systems.

Parametric Modular Answer Set Programs Made Declarative

3

Listing 2. The implementation of control (A) 5 6 7 8 9 10 11 12 13 14

#script(python) from clingo.symbol import Number def main(prg): n = prg.get_const("n").number subs = [("base",[])] for k in range(0,n): subs.append(("property",[Number(k)])) prg.ground(subs) prg.solve() #end.

In order to process the other subprograms such as property(k), control instructions have to be explicitly stated. For instance, assume the property parametric-program in the context of the following control : given a positive integer n, compute the answer sets of a program constructed from the property program by appending the content of its base program fact q(0, 0) to n copies of the rules in property(k) where parameter k ranges from 0 to n − 1.

(A)

The python routine presented in Listing 2 below implements control (A). If the contents of Listings 1 and 2 are stored in a file named property.lp then the command line clingo property.lp -c n=100 (the presented code is compatible with clingo version 5.6) returns the unique answer set {q(0, 0) q(1, 1) q(2, 2) . . . q(100, 100)}. Directive -c n=100 provides a specific value 100 to be utilized in place of n by clingo. The while-loop of the routine in Listing 2 appends to the base program n pairs of the subprogram named property where the placeholder k is replaced by numbers 0 through n − 1. In line 12, the instruction is given to ground all rules in base together with all rules in the property subprograms with their parameters k substituted by the corresponding integers. In line 13, the resulting ground program is solved. Thus, the property parametric-program together with the specified control is understood as the following “typical” logic program: q(0, 0).

q(N, 0 + 1) :- q(N − 1, 0).

···

q(N, 99 + 1) :- q(N − 1, 99).

q(N, 1 + 1) :- q(N − 1, 1).

(1)

Though extremely simple, the program in Listing 1 illustrates the key concepts of parametric modular logic programs and collective control that appear in planning problems. A parametric program together with its control can be seen as the means to concisely described what can be a lengthy program. Furthermore, it naturally groups rules of a program together. In the closing section, we illustrate how such grouping can be used in constructing arguments about formal properties of a program augmented with control based on the properties about its individual subcomponents. Let us summarize what we call a collective control exemplified by (A): this control • collects the subprograms of interest with the values for the respective parameters; • instantiates the respective parameters by their values in each of the subprograms; • grounds the collection as if it were the union of rules; • solves the ground program.

4 In what follows we provide the declarative semantics to clingo programs with the collective control. The proposed semantics allow us to associate meaning with each individual component of a program with control without referring to concatenation and grounding.

3 Theoretical Preliminaries We open this section by describing syntax and semantics of normal logic programs with arithmetic (Fandinno et al. 2020; Lifschitz 2021; Fandinno et al. 2024). Then, we review the key concepts stemming from the multi-shot framework (Gebser et al. 2019). 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 ×, whose argument and value sorts are integer, and comparison predicate constants such as ≤ or >, 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 0, 1, −1, 2, . . . . We often identify numerals with integers and just write 0 instead of 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 5 + 3 and 5 + 3. The former is identified with the numeral 8, whereas the later is identified with an algebraic expression that encodes function application to two numerals 5 and 3. In the remainder we use the overline only in cases exemplified by expression 5 + 3. We assume that for every sort, an infinite sequence of object variables of that sort is chosen. Terms over a signature σ are defined recursively as usual with the addition that arguments of functions have to be of appropriate sorts. Atomic formulas over σ are either (i) expressions of the form p(t1 , . . . , tn ), where p is a predicate constant and t1 , . . . , tn are terms such that their sorts are subsorts of the argument sorts s1 , . . . , sn of p, or (ii) expressions of the form t1 = t2 , where t1 and t2 are terms. (First-order) formulas over signature σ are formed from atomic formulas and the 0-place connective ⊥ (falsity) using the binary connectives ∧, ∨, → and the quantifiers ∀, ∃. The other connectives are treated as abbreviations: ¬F stands for F → ⊥ and F ↔ G stands for (F → G) ∧ (G → 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 Head ← Body (or, Head :- Body in source code format), where Head is an atomic formula or ⊥, and 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 σ (Fandinno et al. 2020). Thus, a program can be seen as a first-order theory over σ. 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 Head ← Body with the

Parametric Modular Answer Set Programs Made Declarative

5

universal closure of the formula B → Head , where B is the conjunction of all literals in Body after replacing not by ¬. 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 (2021). We often write rules as formulas B → 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) → 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. 2008, Section 1.2.2). An interpretation I of a signature σ 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 tI assigned to a ground term t over σ by an interpretation I and the satisfaction relation (denoted, |=) between an interpretation of σ and a sentence over σ are defined recursively, in the usual way (Lifschitz et al. 2008, 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 (2004; 2005) 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. (2024). We review it here considering a signature σ as described above and standard interpretations. We start by introducing some notation. Let I to be a standard interpretation over signature σ. If t is a tuple t1 , . . . , tn of ground terms, then tI is the tuple tI1 , . . . , tIn of values. By AI we denote the set of atoms of the form p(t) such that I |= p(t), where p is a predicate symbol and t is a tuple of precomputed terms. An HT-interpretation over σ is a pair ⟨H, I⟩, where I is a standard interpretation and H ⊆ AI . (In terms of Kripke models with two worlds, H describes the predicates in the here-world and I captures the there-world). The satisfaction relation |= ht between HT-interpretation ⟨H, I⟩ of σ and a sentence F over σ I is defined recursively: • ⟨H, I⟩ |= p(t), if p(tI ) ∈ H; ht • ⟨H, I⟩ |= t = t2 if tI1 = tI2 ; ht 1 • ⟨H, I⟩ |= F ∧ G if ⟨H, I⟩ |= F and ⟨H, I⟩ |= G; ht ht ht • ⟨H, I⟩ |= F ∨ G if ⟨H, I⟩ |= F or ⟨H, I⟩ |= G; ht ht ht • ⟨H, I⟩ |= F → G if (i) ⟨H, I⟩ ̸|= F or ⟨H, I⟩ |= G, and (ii) I |= F → G; ht ht ht • ⟨H, I⟩ |= ∀X F (X) with X of the general sort, if ⟨H, I⟩ |= F (t) for every precomht ht puted term t; • ⟨H, I⟩ |= ∀X F (X) with X of the integer sort, if ⟨H, I⟩ |= F (n) for every integer n; ht ht • ⟨H, I⟩ |= ∃X F (X) with X of the general sort, if ⟨H, I⟩ |= F (t) for some precomht ht puted term t;

6 • ⟨H, I⟩ |= ∃X F (X) with X of the integer sort, if ⟨H, I⟩ |= F (n) for some integer n. ht ht If ⟨H, I⟩ |= F holds, we say that ⟨H, I⟩ satisfies F and that ⟨H, I⟩ is an HT-model of F . ht It is easy to see that (AI , I) is an HT-model of a sentence F whenever I is a model of F . About a model I of a theory Γ, we say it is stable if, for every proper subset H of AI , HT-interpretation ⟨H, I⟩ does not satisfy Γ. 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 (2004; 2005). 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. 2007; 2011), when all predicate constants are considered to be “intensional”. In the sequel, we sometimes abuse our terminology and notation and identify set AI of ground atoms with interpretation I. 3.2 Parameterizable Subprograms We now review the key concepts introduced by Gebser et al. (2019) 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 #program m(p1 , . . . , pj ), where m, p1 , . . . , pj are symbolic constants. We call m the name of the declaration and p1 , . . . pj 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 R1 to denote Listing 1, R1 (base) = {q(0, 0)} and R1 (property) = {q(N − 1, k) → q(N, k + 1)}. A valuation v of a set of placeholders PH is a function that maps elements in this set to precomputed terms. Given a program/formula F , a set PH of placeholders and valuation v on PH , by v(F ) we denote a program/formula constructed from F by substituting each of the occurrences of some placeholder c ∈ PH with the value v(c) assigned to it by the valuation v. Given a name m with associated parameters/placeholders p1 , . . . , pj , and valuation v on {p1 , . . . , pj }, we say that v(R(m)) is the v-instantiation of subprogram R(m). For instance, if v is the valuation {k 7→ 42}, then v(R1 (property)) consists of the universal closure of q(N − 1, 42) → 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, PH , v], where m is a name, PH is a set of associated parameters/placeholders with m, and v is a valuation on PH . Given (i) clingo-program R and (ii) set [m1 , PH 1 , v1 ], . . . , [mj , PH j , vj ] of subprogram-specs, the collective control associates this pair with the logic program composed of the rules v1 (R(m1 )) ∪ v2 (R(m2 )) ∪ · · · ∪ vj (R(mj )).

(2)

Parametric Modular Answer Set Programs Made Declarative

7

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, ∅, ()], [property, {k}, (k 7→ 0)], · · · , [property, {k}, (k 7→ 99)]. Although clingoprograms 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 Modular Logic Programs Our ultimate goal is to define parametrized modular programs that are capable to capture semantics of clingo-programs with collective control declaratively in a way that such modular programs treat individual subprograms with reverie so that each instantiation of a subprogram will have its individual meaning devoid of the rest of the context. Prior to that we introduce modular logic programs that are close relatives to first-order modular logic program proposed by Harrison and Lierler (2016). In that work, first-order modular logic program was a collection of logic programs with some predicates identified as intensional and others as extensional. Thus, some members of that collection could be viewed as “definitions/modules” for concepts captured by intensional predicates. Here, we allow arithmetic and use a concept called intensionality statements introduced by Fandinno and Lierler (2023) to claim more control over granularity of modules. This section is organized as follows. We start by introducing simple intensionality statements – a special case of such statements. We then define modules and modular programs that use intensionality statements, intuitively, to pin the scope of module’s applicability. The section culminates in defining parametric modular programs. 4.1 Simple Intensionality Statements Fandinno and Lierler (2023) 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 (2023) is applicable. In the sequel, the splitting theorem by Fandinno and Lierler (2023) 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

8 arguments is considered “known”. This is important in our context. Indeed, as mentioned in the introduction, one of the distinguished uses of ASP +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 κ over a signature σ is a function mapping each predicate symbol p/n in σ 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 σ, 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 Xi 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. 2011). When the arity of p/n is clear from the context, we write κp instead of κ(p/n). Consider, for instance, predicate symbol q/2 and let κq be set {⟨X, 1⟩, ⟨X, 2⟩}. Intuitively, this intensionality statement states that the ground atoms formed by predicate constant q with its arguments of the form ⟨t, 1⟩ or ⟨t, 2⟩ are intensional for any term t; otherwise, these atoms are extensional. For an intensionality statement κ and a predicate symbol p/n, by λpκ (X) we denote the formula   _ ^ Xi = ti (3) (t1 ,...tn )∈κp

ti is not a variable (1 ≤ i ≤ n)

where X = ⟨X1 , . . . , Xn ⟩ is a tuple of distinct variables of the appropriate length and sort (in the sequel we adopt this convention and use X to denote tuples of variables). To each simple intensionality statement κ, we associate a set EM (κ) of sentences, called the extensional axioms of κ, containing a sentence of the form ∀X (¬λpκ (X) → p(X) ∨ ¬p(X))

(4)

for every predicate symbol p/n in σ. For a theory Γ over σ, we say that a standard interpretation I is κ-stable if it is a stable model of Γ ∪ EM (κ). When it is clear from the context we sometimes drop κ as a subscript of λpκ . Let us illustrate these concepts on examples. Assume the signature σ1 composed of a single predicate q. Consider κq1 = {⟨X, 1⟩, ⟨X, 2⟩}; then λq1 (X1 , X2 ) is (X2 = 1 ∨ X2 = 2) (here and in the sequel we understand λi as an abbreviation for λκi ). Thus, extensional axioms formula EM (κ1 ) is equivalent to the the universal closure of

X2 ̸= 1 ∧ X2 ̸= 2 → q(X1 , X2 ) ∨ ¬q(X1 , X2 ) . (5) Consider theory Γ1 composed of the universal closures of formulas q(X, 0) → q(X, 1), and q(X, 1) → q(X, 2). Sets {q(1, 3)} and {q(0, 0), q(0, 1), q(0, 2)} are among the κ1 -stable models of Γ1 . In case of the former, note that q/2 is not intensional for ⟨1, 3⟩ and hence

Parametric Modular Answer Set Programs Made Declarative

9

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 ⟨0, 0⟩ 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 κ1 -stable model of Γ1 because q/2 is intensional for ⟨0, 1⟩ 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 κ-stable models. Proposition 1 below presents this result formally. We call a substitution θ simple with respect to signature σ whenever all values assigned by θ are precomputed terms over σ (we drop the reference to the signature when it is clear from the context). Proposition 1. Let I be a κ-stable model of Γ, p/n be predicate symbol, and t be a tuple of terms of length n such that I |= λpκ (t). It is the case that I ̸|= p(t) when there is no rule of the form B → p(r) in Γ and simple variable substitution θ such that (rθ)I = t and I |= Bθ. Intuitively, condition I |= λpκ (t) means that given a simple intensionality statement κ, theory Γ “defines” this predicate on the tuples associated with it. 4.2 Modules and Modular Programs A module over signature σ is a pair ⟨κ, Π⟩, where κ is a simple intensionality statement over σ and Π is a program over σ; we say that a κ-stable model of Π is a model of the module. For instance, consider module ∆1 over σ1 to stand for ⟨κ1 , Γ1 ⟩, where σ1 , κ1 and Γ1 are defined in Section 4.1. The models of ∆1 are the κ1 -stable models of Γ1 . A modular program P is a pair ⟨κ, M⟩ where κ is a simple intensionality statement and M = {∆1 , . . . , ∆n } is a finite set of modules over σ such that ∀X (λpi (X) → λp (X)) is valid

(6)

for every predicate symbol p/n in σ and every module ∆i in M; where λp and λpi respectively are the formulas associated with p/n by κ and each κ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 P if it is a model of each of its modules ∆i and it satisfies formula
∀X λp (X) ∧ ¬λp1 (X) ∧ . . . ∧ ¬λpn (X) → ¬p(X) (7) for every predicate symbol p/n in σ. 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 P1 over σ1 whose simple intensionality statement is defined by κq = ⟨X, Y ⟩ (in other words, predicate symbol q is purely intensional); and set of modules consists of ∆0 , ∆1 and ∆2 , where ∆0 = ⟨κ0 , {q(0, 0)}⟩, and ∆2 = ⟨κ2 , {q(0, 2) → q(0, 3), q(0, 3) → q(0, 4)}⟩

10 with κq0 = {⟨0, 0⟩} and κq2 = {⟨X, 3⟩, ⟨X, 4⟩}; and ∆1 is understood as earlier. The only stable model of P1 is {q(0, 0), q(0, 1), q(0, 2), q(0, 3), q(0, 4)}.

(8)

We assume that an empty conjunction is equivalent to ⊤. The condition (7) for q is equivalent to the universal closure of (X1 ̸= 0 ∧ X2 = 0) ∨ ¬(0 ≤ X2 ≤ 4) → ¬q(X1 , X2 ). Hence, every atom of the form q(t1 , t2 ) is false when both t1 ̸= 0 and t2 = 0 or when t2 ̸∈ {0, 1, 2, 3, 4}. All models of ∆1 where q(t1 , 0) is false must also satisfy that q(t1 , 1) and q(t2 , 2) are false, and all models of ∆2 where q(t1 , 2) is false must also satisfy that q(t1 , 3) and q(t1 , 4) are false. Since q(t1 , 0) is false for every t1 ̸= 0, then atoms q(t1 , t2 ) with t1 = ̸ 0 and t2 ∈ {1, 2, 3, 4} must be false as well. Hence, it remains to discuss atoms of the form q(0, t2 ) with t2 ∈ {0, 1, 2, 3, 4}. Atom q(0, 0) must be true because all the models of ∆0 satisfy it. Atoms q(0, 1) and q(0, 2) must be true because they are true in the only models of ∆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 ∆2 satisfying q(0, 2). Note that, set (8) is exactly the unique κ-stable model of the program containing all rules in ∆0 , ∆1 and ∆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 t1 ⊙ t2 with ⊙ ∈ {+, −, ×} and both t1 and t2 are ground terms, then [t] is the numeral n1 ⊙ n2 with n1 = [t1 ] and n2 = [t2 ]; • if t is t1 ⊙ t2 with ⊙ ∈ {+, −, ×} and at least one of t1 and t2 is a variable, then [t] is the expression [t1 ] ⊙ [t2 ]; For example, [0 + 1] = 1, and [X + 1] = X + 1. If t = (t1 , . . . , tn ) is a tuple of terms, then [t] denotes the tuple ([t1 ], . . . , [tn ]). A module ⟨κ, Π⟩ is called simple when for every atom p(t) in the head of a rule in Π, there is a tuple u in κp and a substitution θ such that [t] = uθ. A modular program is called simple if all its modules are simple. Modular program P1 defined above is simple. Indeed, we can check that module ∆1 = ⟨κ1 , Γ1 ⟩ is simple. We have two atoms in the heads of its rules, namely, q(X, 1) and q(X, 2). A substitution that maps X1 to X will turn tuples in κ1 into the arguments of these atoms. Similarly, we can check that modules ∆0 and ∆2 are also simple. As another example, let us consider module ⟨{⟨X, 1⟩}, {q(N − 1, 0) → q(N, 0 + 1)}⟩

(9)

which corresponds to the program 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 P = ⟨κ, {∆1 , . . . , ∆n }⟩, the (directed) graph of dependencies, denoted G(P), is defined as follows: • Its vertices are pairs (p, i) with p a predicate symbol and 1 ≤ i ≤ n. • It has an edge from (p, i) to (q, j) when for some rule r of P,

Parametric Modular Answer Set Programs Made Declarative

11

— there is an atom of the form p(t) in the head of r, and — there is a nonnegated atom of the form of q(t′ ) in the body of r, and — there are tuples ui in κpi and uj in κqj , and substitutions θ and θ′ such that [t] = ui θ and [t′ ] = uj θ′ . We say that a strongly connected component of G(P) is contained in module ∆i if all vertices in this component are of the form (p, i). As an example dependency graph G(P1 ) 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 ∆i for any i ∈ {0, 1, 2}. A simple modular program P is called coherent if it satisfies the following two conditions: • every strongly connected component of the dependency graph G(P) is contained in some module; and • every pair of modules ⟨κi , Πi ⟩ and ⟨κj , Πj ⟩ in P satisfy that, for every predicate symbol p, there is no pair of tuples ui ∈ κpi and uj ∈ κpj with i ̸= j, such that ui and uj unify. Two tuples ti = ⟨ti1 , . . . tim ⟩ and tj = ⟨tj1 , . . . tjm ⟩ of terms unify if there is a substitution θ of the variables that applied to both ti and tj yields tik = tjk , 1≤k≤m Theorem 2. The answer sets of a coherent modular program P are the same as the answer sets of the program obtained by taking the union of all rules in its modules. Theorem 3. Deciding if a modular program is coherent is feasible in polynomial time. 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 PH of object constants not occurring in σ, then by σ PH we denote the signature σ extended with the object constants in PH . By PH + we denote the signature composed of the object constants in PH , numerals, and arithmetic function constants. A parametric intensionality statement over σ PH is a function mapping each predicate symbol p/n in σ 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 PH + ; • no variable occurs twice in a tuple. A parametric module over σ is a triple PH , χ, Π , where χ is a parametric intensionality statement over σ PH and Π is a formula (program understood as a set of formulas) over σ PH . In the sequel, to illustrate relevant concepts we use the parametric module ⟨{k}, χ1 , {q(N − 1, k) → q(N, k + 1)}⟩,

(10)

where we assume the signature composed of a single predicate q and parametric intensionality statement χq1 is characterized by the singleton set consisting of ⟨X, k + 1⟩.

12 Given a parametric intensionality statement χ over σ PH and substitution Θ on PH by χΘ we denote a function mapping each predicate symbol p/n in σ to the following set of n-tuples {⟨[t1 Θ], . . . , [tn Θ]⟩ | ⟨t1 , . . . , tn ⟩ ∈ χp }. For a simple substitution Θ on PH , χΘ forms a simple intensionality statement. (We defined simple substitutions in Section 4.1.) For example, let Θ1 be a simple substitution that maps k to precomputed term 1. Then (q(N − 1, k) → q(N, k + 1))Θ1 χq1 Θ1

is is

q(N − 1, 1) → q(N, 1 + 1); {⟨X, 2⟩}.

Given a parametric module Φ = PH , χ, Π over signature σ and a simple substitution Θ on PH , we can construct a module ΦΘ = ⟨χΘ, ΠΘ⟩ (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, σ. When the set of placeholders PH is empty in a considered parametric module, it serves a role of an instance itself. For example, let Dk denote parametric module in (10). Take Θ0 be a simple substitution k that maps k to precomputed term 0. Then, instance DΘ coincides with module (9). 0 Similarly, if Θ1 is a simple substitution that maps k to precomputed term 1, then k instance DΘ stands for ⟨{⟨X, 2⟩}, {q(N − 1, 1) → q(N, 1 + 1)}⟩. 1 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 Dk (k ≥ 0) introduced above. Substitutions Θi (0 ≤ i ≤ n) map parameter k into precomputed term (integer) i. We identify subprogram base in the running example with a parametric module ⟨∅, {⟨0, 0⟩}, {q(0, 0)}⟩

(11)

that we denote as D and which coincides with the module ∆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 ⟨κ, {D, Dθk0 , . . . , Dθkn }⟩,

(12)

where the signature of this modular program contains predicate q/2 and the simple intentionality statement κ 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 Theorem 2. In fact, that theorem gives us formal grounds for our earlier actions of identifying subprograms base and property(k) with parametric modules D and Dk (k ≥ 0), respectively.

5 Utility of Declarative Approach to Modularity We now illustrate how this declarative approach to modularity allows us to make formal claims about a program with control without a reference to underlying workings of clingo. Rather, these arguments naturally accompany intuitive readings of the parametric programs that we supply clingo with. Consider the property program in Listing 1. Our first intuition is that its base subprogram states that pair ⟨0, 0⟩ of integers has property q. (13)

Parametric Modular Answer Set Programs Made Declarative

13

In Section 4.3 we argued that the base subprogram can be identified with module D defined in (11). Any model of this instance supports claim (13) formally. Our second intuition is that the property(k) subprogram states that given i is an integer substituted for k within this subprogram and property q holds for some pair ⟨j−1, i⟩, where j is an integer, then property q also holds for the pair ⟨j, i + 1⟩. Take i to denote an arbitrary integer and Θi to denote a simple substitution that maps k into i. Recall that k we view the property(k) subprogram as parametric module Dk ; whereas DΘ captures i an instance of that program obtained by replacing integer i for parameter k. With that it is easy to see that any model of this instance supports the intuition we claim. Last but not least is grasping the overall meaning of the property program when control is in place and formally reasoning about its properties. First, the control specifies which exact instances of the subprograms are being part of an overall program being processed. Second, it implicitly defines the signature under which the program is interpreted. To continue with our running example, consider control (A). This control together with the considered parameterizable subprograms warrants the signature of a single predicate q/2 and infinite set of numerals. We now construct an inductive proof that the modular program listed in (12) (the modular program that we identify with the property program with the collective control) has a unique answer set I whose set AI of true atoms has the form {q(0, 0) q(1, 1) q(2, 2) . . . q(n, n)}. The uniqueness of this answer set follows immediately from the following claims Claim 1: for any natural number i that is less or equal to n, q(i, i) belongs to AI ; Claim 2: for any natural number i that is greater than n, q(i, i) does not belong to AI ; Claim 3: for any distinct natural numbers i and j, q(i, j) does not belong to AI . We prove Claim 1 by induction. Base case. Take i to be 0, q(0, 0) is part of AI due to the observation we made as we discussed the first intuition. Our inductive hypothesis is that the claim in question is the case for some integer j that is less than n. We now show that it is the case for j + 1. By inductive hypothesis q(j, j) is part of AI . Then, q(j + 1, j + 1) is part of AI due to the presence of the instance Dθkj in (12) and observation we made as we discussed the second intuition. For Claim 2, condition (7) of the definition of stable models of modular programs for the case program (12) and predicate symbol q/2 has the form
∀X1 X2 ⊤ ∧ (X1 ̸= 0 ∨ X2 ̸= 0) ∧ X2 ̸= 1 ∧ · · · ∧ X2 ̸= n → ¬q(X1 , X2 ) . (14) This implies that whenever the second argument, let us call it m, of predicate q is greater than n, atom of the form q(·, m) is not part of AA . Claim 2 follows from this observation. To show that Claim 3 holds, it is sufficient to consider the case when j is less or equal to n. Indeed, recall the argument supporting Claim 2. Now we prove this claim by induction on j. Base case. Take j = 0. And consider arbitrary integer i different from j. Trivially, i = ̸ 0. The consequence of (14) is satisfied by I. Then, q(i, j) is not part of AI . Inductive step. Consider 0 ≤ j < n. The inductive hypothesis states: for any natural number i that is different from j, q(i, j) does not belong to AI . We now show that for any natural number i that is different from j + 1, q(i, j + 1) does not belong to AI . Consider any natural number i different from j + 1. Module Dθkj that has the form ⟨{⟨X, j + 1⟩}, {q(N − 1, j) → q(N, j + 1)}⟩. Formula λq (i, j + 1) is X2 = j + 1. Thus, I |= λq (i, j + 1). Take Θ to denote the substitution N 7→ i. This is the only substitution which turns atom q(N, j + 1) that occurs in the head of the only rule in Dθkj into ground

14 atom q(i, j + 1). Ground atom q(N − 1, j)Θ forms the body of that rule and has the form q(i − 1, j). Given that i = ̸ j + 1, it follows i − 1 ̸= j + 1. By inductive hypothesis q(i, j + 1) does not belong to AI . By Proposition 1, q(i, j + 1) is not part of AI . Note how all our formal claims about the shape and the uniqueness of the answer set of the property program with collective control are void from the reference to the inner workings of clingo. There is no reference to concatenation, grounding, and solving.

6 Conclusions This paper champions a need for investigating a declarative approach to modularity in ASP. We take a step in this direction by introducing parametric modular programs and their declarative semantics. In the concluding section we illustrate the utility of this approach by reasoning about a sample ASP program with collective control in a formal way that is void from the reference to the inner workings of ASP systems. This is an important step towards refining our understanding about modular formalisms and providing ASP practitioners with formal tools to reason about the properties of modular programs frequently required in the design of complex systems. Yet, we only scratched the surface of this important topic. There are many directions for future research. For example, it is important to investigate how the proposed approach can be extended to capture other forms of controls. In practice, it is common that controls use so called external atoms to “deactivate” certain parts of the subprograms “on demand”. We believe that our framework can be extended to capture this kind of control as well, and we plan to explore this direction. Another viable direction for future work is a development of a declarative meta-language for the instantiation of parametric modules. The specifications in that language would define which instantiations of parametric modules form the actual intended program. Acknowledgements. We would like to thank the anonymous reviewers for their valuable feedback that allowed us to improve the presentation of several points. This work was supported by the National Science Foundation CAREER award 2338635, USA, and the DFG grant SCHA 550/15, Germany. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.

References P. Cabalar, J. Fandinno, and Y. Lierler. Modular answer set programming as a formal specification language. Theory and Practice of Logic Programming, 20(5):767–782, 2020. Y. Dimopoulos, M. Gebser, P. Lühne, J. Romero, and T. Schaub. plasp 3: Towards effective ASP planning. In M. Balduccini and T. Janhunen, editors, Proceedings of the Fourteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’17), volume 10377 of Lecture Notes in Artificial Intelligence, pages 286–300. Springer-Verlag, 2017. J. Fandinno and Y. Lierler. Splitting answer set programs with respect to intensionality statements. In B. Williams, Y. Chen, and J. Neville, editors, Proceedings of the Thirty-seventh National Conference on Artificial Intelligence (AAAI’23), pages 6338–6345. AAAI Press, 2023. J. Fandinno, V. Lifschitz, P. Lühne, and T. Schaub. Verifying tight logic programs with anthem and vampire. Theory and Practice of Logic Programming, 20(5):735–750, 2020.

Parametric Modular Answer Set Programs Made Declarative

15

J. Fandinno, V. Lifschitz, and N. Temple. Locally tight programs. Theory and Practice of Logic Programming, 24(5):942–972, 2024. J. Fandinno, Z. Hansen, Yu. Lierler, Ch. Glinzer, J. Heuer, T. Schaub, T. Stolzmann, and V. Lifschitz. ANTHEM 2.0: Automated reasoning for answer set programming. Theory Pract. Log. Program., 25(4):668–684, 2025. P. Ferraris, J. Lee, and V. Lifschitz. A new perspective on stable models. In M. Veloso, editor, Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI’07), pages 372–379. AAAI/MIT Press, 2007. P. Ferraris, J. Lee, and V. Lifschitz. Stable models and circumscription. Artificial Intelligence, 175(1):236–263, 2011. M. Gebser, R. Kaminski, B. Kaufmann, and T. Schaub. Clingo = ASP + control: Extended report. Technical report, Universität Potsdam, 2014. URL http://www.cs.uni-potsdam.de/ wv/pdfformat/gekakasc14a.pdf. M. Gebser, R. Kaminski, B. Kaufmann, and T. Schaub. Multi-shot ASP solving with clingo. Theory and Practice of Logic Programming, 19(1):27–82, 2019. doi: 10.1017/S1471068418000054. M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In R. Kowalski and K. Bowen, editors, Proceedings of the Fifth International Conference and Symposium of Logic Programming (ICLP’88), pages 1070–1080. MIT Press, 1988. doi: 10.1201/b10397-6. Z. Hansen and Yu. Lierler. Sm-based semantics for answer set programs containing conditional literals and arithmetic. In PADL, volume 15537 of Lecture Notes in Computer Science, pages 71–87. Springer, 2025. A. Harrison and Yu. Lierler. First-order modular logic programs and their conservative extensions. Theory and Practice of Logic programming, 32nd Int’l. Conference on Logic Programming (ICLP) Special Issue, 2016. T. Janhunen, E. Oikarinen, H. Tompits, and S. Woltran. Modularity aspects of disjunctive stable models. In C. Baral, G. Brewka, and J. Schlipf, editors, Proceedings of the Ninth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’07), volume 4483 of Lecture Notes in Artificial Intelligence, pages 175–187. Springer-Verlag, 2007. V. Lifschitz. Transforming gringo rules into formulas in a natural way. In W. Faber, G. Friedrich, M. Gebser, and M. Morak, editors, Proceedings of the Seventeenth European Conference on Logics in Artificial Intelligence (JELIA’21), volume 12678 of Lecture Notes in Computer Science, pages 421–434. Springer-Verlag, 2021. V. Lifschitz and H. Turner. Splitting a logic program. In Pascal Van Hentenryck, editor, Proceedings of International Conference on Logic Programming (ICLP), pages 23–37, 1994. V. Lifschitz, L. Morgenstern, and D. Plaisted. Knowledge representation and classical logic. In Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter, editors, Handbook of Knowledge Representation, pages 3–88. Elsevier, 2008. URL http://www.cs.utexas.edu/users/ai-lab? lif08b. E. Oikarinen and T. Janhunen. Modular equivalence for normal logic programs. In Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso, editors, Proceedings of the 17th European Conference on Artificial Intelligence, ECAI 2006, pages 412–416, Amsterdam, The Netherlands, 2006. IOS Press. E. Oikarinen and T. Janhunen. Achieving compositionality of the stable model semantics for Smodels programs. Theory and Practice of Logic Programming, 5–6:717–761, 2008. D. Pearce and A. Valverde. Towards a first order equilibrium logic for nonmonotonic reasoning. In J. Alferes and J. Leite, editors, Proceedings of the Ninth European Conference on Logics in Artificial Intelligence (JELIA’04), volume 3229 of Lecture Notes in Computer Science, pages 147–160. Springer-Verlag, 2004. doi: 10.1007/978-3-540-30227-8\_15. D. Pearce and A. Valverde. A first order nonmonotonic extension of constructive logic. Studia Logica, 30(2-3):321–346, 2005.