Bounded Programs: A New Decidable Class of Logic Programs with Function Symbols

1 Introduction

In recent years, there has been a great deal of interest in enhancing answer set solvers by supporting functions symbols. Function symbols often make modeling easier and the resulting encodings more readable and concise. The main problem with the introduction of function symbols is that common inference tasks become undecidable. In order to cope with this issue, research has focused on identifying sufficient conditions for a program to have finitely many stable models, each of finite size, leading to different criteria (that we call termination criteria).

In this paper, we present a more powerful technique to check whether a program has a finite number of stable models and each of them is of finite size. The termination criterion we propose relies on two powerful tools: the labelled argument graph, a directed graph whose edges are labelled with useful information on how terms are propagated from the body to the head of rules, and the activation graph, a directed graph specifying whether a rule can "activate" another rule (we will make clear what this means in the following). The labelled argument graph is used in synergy with the activation graph for a better understanding of how terms are propagated. Another relevant aspect that distinguishes our criterion from past work is that current termination criteria analyze one group of arguments (depending on each other) at a time, without looking at how groups of arguments are related. On the contrary, our criterion is able to perform an analysis of how groups of arguments affect each other.

Example 1 Consider the logic programP1 below:

The bottom-up evaluation of P1 terminates yielding the set of atoms count([a, b, c], 0), count([b, c], 1), count([c], 2), and count([ ], 3). The query goal count([ ], L) can be used to retrieve the length L of list [a, b, c]. 1 ✷

None of the current termination criteria is able to realize that the bottom-up evaluation of P1 terminates. Intuitively, this is because they analyze how the first argument of count affects itself and how the second argument of count affects itself, but miss noticing that the growth of latter is bounded by the reduction of the former. One of the novelties of our criterion is the capability of doing this kind of reasoningindeed, as shown in Example 8, our criterion is able to realize that the bottom-up evaluation of P1 terminates.

The following example shows another classical program computing the concatenation of two lists.

Example 2 Consider the following logic programP2:

As an example, the top-down evaluation of P2 w.r.t. the query goal append([a, b], [c, d], W) gives the concatenation of the lists [a, b] and [c, d]. This query cannot be evaluated by standard bottom-up evaluators as the second rule in P2 is not range restricted (because variable X in the rule head does not appear in a positive body literal). However, one might apply rewriting techniques such as magic-set to rewrite P2 into a program whose bottom-up evaluation gives the same result [Beeri and Ramakrishnan, 1991]. In this case, P2 and the query goal append([a, b], [c, d], W) give the following program P ′2 :

1 Notice that P1 has been written so as to count the number of elements in a list when evaluated in a bottom-up fashion, and therefore differs from the classical formulation relying on a top-down evaluation strategy. However, as shown in Example 2, programs relying on a top-down evaluation strategy can be rewritten into programs whose bottom-up evaluation gives the same result. Our criterion can then be applied to rewritten programs.

r0 : magic append([a, b], [c, d]). r1 : magic append(L1, L2) ← magic append([X|L1], L2). r2 : append([ ], L, L) ← magic append([ ], L). r3 : append([X|L1],L2, [X|L3]) ← magic append([X|L1], L2), append(L1, L2, L3). ✷

Also in the example above, current termination criteria are not able to recognize termination of the bottom-up evaluation of P ′2 , while the new criterion introduced in this paper does.

A significant body of work has been done on termination of logic programs under top-down evaluation [Schreye and Decorte, 1994; Voets and Schreye, 2011; Marchiori, 1996; Ohlebusch, 2001; Codish et al., 2005; Serebrenik and De Schreye, 2005; Nishida and Vidal, 2010; Schneider-Kamp et al., 2009b; 2009a; 2010; Nguyen et al., 2007; Bruynooghe et al., 2007; Bonatti, 2004; Baselice et al., 2009] and in the area of term rewriting [Zantema, 1995; Sternagel and Middeldorp, 2008; Arts and Giesl, 2000; Endrullis et al., 2008; Ferreira and Zantema, 1996]. In this paper, we consider logic programs with function symbols under the stable model semantics [Gelfond and Lifschitz, 1988; 1991], and thus all the excellent works above cannot be straightforwardly applied to our setting (for a discussion on this see, e.g., [Calimeri et al., 2008; Alviano et al., 2010]). In our context, [Calimeri et al., 2008] introduced the class of finitely ground programs, guaranteeing the existence of a finite set of stable models, each of finite size, for programs in the class. Since membership in the class is not decidable, decidable subclasses have been proposed: ω-restricted programs [Syrj¨anen, 2001], λ-restricted programs [Gebser et al., 2007], finite domain programs [Calimeri et al., 2008], argument-restricted programs [Lierler and Lifschitz, 2009], safe programs [Greco et al., 2012], and Γacyclic programs [Greco et al., 2012].

The main contribution of this paper is the introduction of the new decidable class BP of bounded programs that strictly includes all the aforementioned classes in the literature. We present different results on the correctness, the expressiveness, and the complexity of BP.

2 Logic Programs with Function Symbols

Syntax. We assume to have infinite sets of constants, variables, predicate symbols, and function symbols. Each predicate and function symbol is associated with a fixed arity, which is a natural number.

A term is either a constant, a variable, or an expression of the form f(t1, ..., tm), where f is a function symbol of arity m and the ti's are terms (in the first two cases we say the term is simple while in the last case we say it is complex). The binary relation subterm over terms is recursively defined as follows: every term is a subterm of itself; if t is a complex term of the form f(t1, ..., tm), then every ti is a subterm of t, for 1 ≤ i ≤ m; if t1 is a subterm of t2 and t2 is a subterm of t3, then t1 is a subterm of t3.

An atom is of the form p(t1, ..., tn), where p is a predicate symbol of arity n and the ti's are terms (we also say that the atom is a p-atom). A literal is either an atom A (positive literal) or its negation ¬A (negative literal).

A rule r is of the form:

where m > 0, k ≥ 0, n ≥ 0, and A1, ...,Am,B1, ...,Bk, C1, ...,Cn are atoms. The disjunction A1 ∨ ... ∨ Am is called the head of r and is denoted by head(r); the conjunction B1, ..., Bk, ¬C1, ..., ¬Cn is called the body of r and is denoted by body(r). The positive (resp. negative) body of r is the conjunction B1, ...,Bk (resp. ¬C1, ..., ¬Cn) and is denoted by body+(r) (resp. body-(r)). With a slight abuse of notation we use head(r) (resp. body(r), body+(r), body-(r)) to also denote the set of atoms (resp. literals) appearing in the head (resp. body, positive body, negative body) of r. If m = 1, then r is normal; if n = 0, then r is positive. A program is a finite set of rules. A program is normal (resp. positive) if every rule in it is normal (resp. positive). A term (resp. an atom, a literal, a rule, a program) is said to be ground if no variables occur in it. A ground normal rule with an empty body is also called a fact. We assume that programs are range restricted, i.e., for each rule, the variables appearing in the head or in negative body literals also appear in some positive body literal.

The definition of a predicate symbol p in a program P consists of all rules in P with p in the head. Predicate symbols are partitioned into two different classes: base predicate symbols, whose definition can contain only facts, and derived predicate symbols, whose definition can contain any rule. Facts defining base predicate symbols are called database facts. 2

Given a predicate symbol p of arity n, the i-th argument of p is an expression of the form p[i], for 1 ≤ i ≤ n. If p is a base (resp. derived) predicate symbol, then p[i] is said to be a base (resp. derived) argument. The set of all arguments of a program P is denoted by arg(P).

Semantics. Consider a program P. The Herbrand universe HP of P is the possibly infinite set of ground terms which can be built using constants and function symbols appearing in P. The Herbrand base BP of P is the set of ground atoms which can be built using predicate symbols appearing in P and ground terms of HP. A rule r′ is a ground instance of a rule r in P if r′ can be obtained from r by substituting every variable in r with some ground term in HP. We use ground(r) to denote the set of all ground instances of r and ground(P) to denote the set of all ground instances of the rules in P, i.e., ground(P) = ∪r∈Pground(r). An interpretation of P is any subset I of BP. The truth value of a ground atom A w.r.t. I, denoted valueI(A), is true if A ∈ I, false otherwise. The truth value of ¬A w.r.t. I, denoted valueI(¬A), is true if A ̸∈ I, false otherwise. The truth value of a conjunction of ground literals C = L1, ..., Ln w.r.t. I is valueI(C) = min({valueI(Li) | 1 ≤ i ≤ n})- here the ordering false < true holds-whereas the truth value of a disjunction of ground literals D = L1 ∨ ... ∨ Ln w.r.t. I is valueI(D)=max({valueI(Li) | 1 ≤ i ≤ n}); if n = 0, then valueI(C) = true and valueI(D) = false. A ground rule r is satisfied by I, denoted I |= r, if valueI(head(r)) ≥ valueI(body(r)); we write I ̸|= r if r is not satisfied by I. Thus, a ground rule r with empty body is satisfied by I if valueI(head(r)) = true. An interpretation of P is a model of P if it satisfies every ground rule in ground(P). A model M of P is minimal if no proper subset of M is a model of P. The set of minimal models of P is denoted by MM(P).

2 Database facts are not shown in our examples as they are not relevant for the proposed criterion.

Given an interpretation I of P, let P I denote the ground positive program derived from ground(P) by (i) removing every rule containing a negative literal ¬A in the body with A ∈ I, and (ii) removing all negative literals from the remaining rules. An interpretation I is a stable model of P if and only if I ∈ MM(P I ). The set of stable models of P is denoted by SM(P). It is well known that stable models are minimal models (i.e., SM(P) ⊆ MM(P)). Furthermore, minimal and stable model semantics coincide for positive programs (i.e., SM(P) = MM(P)). A positive normal program has a unique minimal model.

An argument q[i] in arg(P) is said to be limited iff for any finite set of database facts D and for every stable model M of P ∪D, the set {ti | q(t1, ..., ti, ..., tn) ∈M} is finite.

3 Termination Analysis Tools

In this section, we describe different tools that will be used in the paper to analyze logic programs with function symbols.

Activation graph. The activation graph of a program has been introduced in [Greco et al., 2012] to define the class SP of safe programs. In a nutshell, the nodes of the graph are the rules of the program and there is an edge from rule r1 to rule r2 iff r1 "activates" r2. Activation of rules is defined as follows. Let P be a program and r1, r2 be (not necessarily distinct) rules of P. We say that r1 activates r2 iff there exist two ground rules r′1 ∈ ground(r1), r′2 ∈ ground(r2) and a set of ground atoms D such that (i) D ̸|= r′1 , (ii) D |= r′2 , and (iii) D ∪ head(r′1 ) ̸|= r′2 . This intuitively means that if D does not satisfy r′1 , D satisfies r′2 , and head(r′1 ) is added to D to satisfy r′1 , this causes r′2 not to be satisfied anymore (and then to be "activated").

The activation graph of a program P, denoted Ω(P), is a directed graph whose nodes are the rules of P, and there is an edge (ri, rj) in the graph iff ri activates rj.

Example 3 Consider the following programP3:

r0 : nat(X) ← b(X). r1 : next(f(X)) ← nat(X). r2 : nat(X) ← next(f(X)).

where b is a base predicate symbol. It is easy to see that r0 activates r1, but not vice versa; r1 activates r2 and vice versa. The activation graph of P3 is shown in Figure 1 (left). ✷

Argument graph. The argument graph, used in [Calimeri et al., 2008] to define the class FD of finite domain programs, represents the propagation of values among arguments of a program. The argument graph of a program P, denoted G(P), is a directed graph whose nodes are the arguments of P, and there is an edge (q[j], p[i]) iff there is a rule r ∈ P such that (i) an atom p(t1, ..., tn) appears in head(r), (ii) an atom q(u1, ..., um) appears in body+(r), and (iii) terms ti and uj have a common variable. For instance, the argument graph of program P3 in Example 3 is reported in Figure 1 (right).

A variation of the argument graph, called propagation graph, has been proposed in [Greco et al., 2012] to define the class AP of Γ-acyclic programs. The main difference is that in the propagation graph only arguments where complex terms may be introduced or propagated are considered.

Argument ranking. The argument ranking of a program has been proposed in [Lierler and Lifschitz, 2009] to define the class AR of argument restricted programs.

For any atom A of the form p(t1, ..., tn), A0 denotes the predicate symbol p, and Ai denotes term ti, for 1 ≤ i ≤ n. The depth d(X, t) of a variable X in a term t that contains X is recursively defined as follows:

An argument ranking for a program P is a partial function φ from arg(P) to non-negative integers such that, for every rule r of P, every atom A occurring in the head of r, and every variable X occurring in a term Ai , if φ(A0 [i]) is defined, then body+(r) contains an atom B such that X occurs in a term Bj , φ(B0 [j]) is defined, and the following condition is satisfied

The set of restricted arguments of P is AR(P) = {p[i] | p[i] ∈ arg(P)∧∃φ s.t. φ(p[i]) is defined}. A program P is said to be argument restricted iff AR(P) = arg(P).

Example 4 Consider again program P3 of Example 3. An argument ranking φ can be defined as follows: φ(b[1]) = 0, φ(nat[1]) = 0, and φ(next[1]) = 1. Thus, P3 is argument restricted. ✷

Argument restricted programs strictly include ω-restricted, λ-restricted, and finite domain programs.

4 Bounded Programs

In this section, we introduce a new criterion, more general than the ones in the literature (cf. Section 1), guaranteeing that a program has a finite set of stable models and each of them is finite.

For ease of presentation, we assume that if the same variable occurs in two terms appearing in the head and in the body of a rule, then one term is a subterm of the other and complex terms are of the form f(t1, ..., tm) with the ti's being simple terms. There is no loss of generality in such assumptions as every program can be rewritten into an equivalent one satisfying such conditions (e.g., a rule of the form p(f(h(X))) ← q(g(X)) can be rewritten into the three rules p(f(X))←p′ (X), p′ (h(X))←p′′ (X), and p′′ (X)←q(g(X))).

We start by introducing a new graph derived from the argument graph by labelling edges with additional information.

Definition 1 (Labelled argument graph) The labelled argument graph of a program P, denoted GL(P), is a directed graph whose set of nodes is arg(P) and the set of labelled edges is defined as follows. For each pair of nodes p[i], q[j] ∈ arg(P) and for every rule r ∈ P such that (i) an atom p(t1, ..., tn) appears in head(r), (ii) an atom q(u1, ..., um) appears in body+(r), (iii) terms ti and uj have a common variable X, there is an edge (q[j], p[i], 〈α, r, h, k〉), where h and k are natural numbers denoting the positions of p(t1, ..., tn) in head(r) and q(u1, ..., um) in body+(r), respectively, 3 and

Example 5 Consider the following programP5

where a and b are base predicate symbols. The labelled argument and activation graphs of P5 are depicted in Figure 2. For instance, the edge (t[1], q[1], 〈f, r1 , 1, 1〉) in GL(P5) says that the first atom in the positive body of r1 is a t-atom, its first term is a variable, say X, and the first atom in the head of r1 is a q-atom whose first term is of the form f(..., X, ...). We will show how this kind of information can be profitably used to analyze programs (e.g., to keep track of how complex terms are generated from argument to argument). ✷

A path ρ from a1 to bm in a labelled argument graph GL(P) is a non-empty sequence (a1, b1, 〈α1, r1, h1, k1〉), . . . , (am, bm, 〈αm, rm, hm, km〉) of labelled edges of GL(P) s.t. bi = ai+1 for all 1 ≤ i < m; if the first and last nodes coincide (i.e., a1 = bm), then ρ is called a cyclic path. We define λ1(ρ) = α1 ... αm, denoting the sequence of ϵ and function symbols labelling the edges of ρ, λ2(ρ) = r1, ..., rm, denoting the sequence of rules labelling the edges of ρ, and λ3(ρ) = 〈r1, h1, k1〉 ... 〈rm, hm, km〉, denoting the sequence of triples 〈rule, head atom identifier, body atom identifier〉 labelling the edges of ρ. In the case where the indication of the start edge is not relevant, we will call a cyclic path a cycle. Given a cycle π consisting of n labelled edges e1, ..., en, we can derive n different cyclic paths starting from each of the ei's-we use τ(π) to denote the set of such cyclic paths. As an example, if π is a cycle consisting of labelled edges e1, e2, e3, then τ(π) = {(e1, e2, e3), (e2, e3, e1), (e3, e2, e1)}. Given two cycles π1 and π2, we write π1 ≈ π2 iff ∃ρ1 ∈ τ(π1) and ∃ρ2 ∈ τ(π2) such that λ3(ρ1) = λ3(ρ2). A cycle is basic if it does not contain two occurrences of the same edge.

3 We assume that literals in the head (resp. body) are ordered with the first one being associated with 1, the second one with 2, etc.

We say that a node p[i] of GL(P) depends on a node q[j] of GL(P) iff there is a path from q[j] to p[i] in GL(P). Moreover, we say that p[i] depends on a cycle π iff it depends on a node q[j] appearing in π. Clearly, nodes belonging to a cycle π depend on π. We say that λ2(ρ) = r1, ..., rm denotes a cyclic path in the activation graph Ω(P) iff (r1, r2), ..., (rm-1, rm), (rm, r1) are edges of Ω(P).

Definition 2 (Active cycle) Given a program P, we say that a cycle π in GL(P) is active iff ∃ρ ∈ τ(π) such that λ2(ρ) denotes a cyclic path in the activation graph Ω(P). ✷

Thus, checking if a cycle in the labelled argument graph is active requires to look at the activation graph. Here the basic idea is to check if the propagation of terms along a cycle of the labelled argument graph can really take place based on the information reported in the activation graph. We illustrate this aspect in the following example.

Example 6 Consider the labelled argument graph and the activation graph of program P5 (cf. Figure 2). Cycles π1 and π3 in Figure 2 are active as (r1, r2), (r2, r1) is a cyclic path in Ω(P5). On the contrary, it is easy to check that cycles π2 and π4 in Figure 2, are not active. ✷

In the previous example, the labelled edges of the nonactive cycle π4 say that a complex term with function symbol f might be generated from s[2] to q[2] (using rule r3), be propagated from q[2] to s[2] (using rule r4), and so on so forth possibly causing the generation of complex terms of unbounded size. However, in order for this to happen, rules r3 and r4 should activate each other, which is not the case from an analysis of the activation graph. Thus, we can conclude that the generation of unbounded terms cannot really happen.

On the other hand, active cycles might lead to the generation of terms of unbounded size. To establish whether this can really be the case, we perform a deeper analysis of the cycles in the labelled argument graph. Specifically, we use grammars to analyze edge labels to get a better understanding of what terms can be propagated among arguments. We introduce two distinct languages which allows us to distinguish between "growing" paths, which could give rise to terms of infinite size, and "balanced" paths, where propagated terms do not grow (see Definition 4).

Definition 3 (Grammars ΓP and Γ′P ) Let P be a program and FP the set of function symbols occurring in P. The grammars ΓP and Γ′P are 4-tuples (N, T,R, S) and (N ′ , T,R′ , S), respectively, where N = {S, S1, S2} and N ′ = {S} are the sets of nonterminal symbols, T = {f | f ∈ FP} ∪ {f | f ∈ FP} is the set of terminal symbols, S is the start symbol, R is the set of production rules:

• S →S1 fi S2, ∀fi ∈ FP;
• S1 → fi S1 fi S1 | ϵ, ∀fi ∈ FP;
• S2 → (S1 | fi)S2 | ϵ, ∀fi ∈ FP.

and R′ is the set of production rules:

• S → fi S fi S | ϵ, ∀fi ∈ FP.

The languages L(ΓP) and L(Γ′P ) are the sets of strings generated by ΓP and Γ′P , respectively. ✷

Notice that L(ΓP) ∩ L(Γ′P ) = ∅. Grammar ΓP has been introduced in [Greco et al., 2012] to analyze cycles of the propagation graph. Here we propose a more detailed analysis of the relationships among arguments by considering also Γ′P . Intuitively, strings in L(ΓP) describe growing sequences of functions symbols used to compose and decompose complex terms, so that starting from a given term we obtain a larger term. On the other hand, strings in L(Γ′P ) describe "balanced" sequences of functions symbols used to compose and decompose complex terms, so that starting from a given term we obtain the same term.

Definition 4 (Classification of cycles) Given a program P and a cycle π in GL(P), we say that π is

• growing if there is ρ ∈ τ(π) s.t. λ1(ρ) ∈ L(ΓP),
• balanced if there is ρ ∈ τ(π) s.t. λ1(ρ) ∈ L(Γ′P ),
• failing otherwise. ✷

Consider the labelled argument graph in Figure 2. Cycles π1, π3, and π4 are growing, whereas cycle π2 is failing. Observe that, in general, a failing cycle is not active, but the vice versa is not true. In fact, cycle π4 from Figure 2 is not active even if it is not failing.

The tools introduced so far are used to define the binding operator ΨP (Definition 5 below). If operator ΨP is applied to a set of limited arguments A, then it gives a set ΨP(A) ⊇ A of arguments which are guaranteed to be limited too. The idea of our termination criterion is to compute the fixpoint of ΨP starting from a set of limited arguments so as to get a set of limited arguments, which can be used as an underestimation of the limited arguments of the program. If the fixpoint computation gives us all arguments of P, then P is bounded.

Definition 5 (ΨP operator) Let P be a program and A ⊆ arg(P). We define ΨP(A) as the set of arguments q[k] of P such that for each basic cycle π in GL(P) on which q[k] depends, at least one of the following conditions holds:

1. π is not active or is not growing;
2. π contains an edge (s[j], p[i], 〈f, r, l1, l2〉) and, letting p(t1, ..., tn) be the l1-th atom in the head of r, for every variable X in ti, there is an atom b(u1, ..., um) in body+(r) s.t. X appears in a term uh and b[h] ∈ A;
3. there is a basic cycle π′ in GL(P) s.t. π′ ≈π, π′ is not balanced, and π′ passes only through arguments in A.✷

Observe that base arguments belong to ΨP(A) for any set of arguments A, because they do not depend on cycles.

Proposition 1 Let P be a program and A a set of limited arguments of P. Then, all arguments in ΨP(A) are limited.

Example 7 Consider program P5 of Example 5, whose labelled argument and activation graphs are reported in Figure 2. Notice that basic cycles π1 and π3 are growing and active, π2 is failing and non-active, π4 is growing and nonactive. The basic cycle π5 composed by π1 and π2 (denoted by a dashed line) is failing and non-active, and the basic cycle π6 composed by π3 and π4 (denoted by a dashed line) is growing and non-active. Furthermore, base arguments a[1] and b[1] do not depend on any cycle; t[1], q[1], s[1] depend on π1, π2, and π5; t[2], q[2], s[2] depend on π3, π4, and π6. By iteratively applying operator ΨP5 starting from ∅ we have: (i) A1 = ΨP5 (∅) = {a[1], b[1]};

(ii) A2 = ΨP5 (A1) = A1 ∪ {t[1], q[1], s[1]} as Condition 2 of Definition 5 applies to π1, and Condition 1 applies to π2 and π5;

(iii) A3 = ΨP5 (A2) = A2 ∪ {t[2], q[2], s[2]} as Condition 1 applies to π4 and π6, and Condition 3 applies to π3 (in fact, π1 ≈π3, π1 is not balanced and goes only through nodes in A3).

Therefore, we derive that all arguments are limited. ✷

Notice that in order to guarantee that arguments in ΨP(A) are limited, it does not suffice to consider simple cycles only (i.e., cycles going through each node only once), but basic cycles have to be considered. As an example, Figure 3 shows a labelled argument graph with two failing simple cycles composed by edges e1, e2, e5 and e3, e4, respectively. However, the basic cycle consisting of edges e1, e2, e3, e4, e5 is growing and the generation of infinite terms can take place.

Proposition 2 Given a program P and a set A of limited arguments of P, then:

1. ΨiP (A) ⊆ Ψi+1 P (A) for i ≥ 0, and
2. there is a finite n such that ΨnP (A) = Ψ∞P (A),

Observe that ΨiP (A) ⊆ Ψi+1 P (A), for i > 0, for every set of limited arguments A, but the relationship A ⊆ ΨP(A) does not always hold if A is an arbitrary non-empty set of arguments of P. Below we report some examples illustrating the computation of Ψ∞P (∅) and the conditions of Definition 5.

Example 8 Consider program P1 of Example 1. To comply with the conditions mentioned at the beginning of this section, P1 is rewritten into the following programP8:

r0 : count(lc(a, lc(b, lc(c, nil))), 0).

• r1 : f-count(X, L, I) ← count(lc(X, L), I).

r2 : count(L, s(I, 1)) ← f-count(X, L, I).

Here function symbol lc denotes the list constructor operator "|", function symbol s denotes the sum operator, and nil denotes the empty list "[ ]". The labelled argument graph is shown in Figure 4, where c and fc stand for count and f-count, respectively. The activation graph is not shown, but it is easy to see that r1 activates r2 and vice versa; thus, both cycles π1 and π2 are active. Furthermore, π1 is failing and π2 is growing. Notice also that c[1], fc[1], and fc[2] depend on π1; c[2] and fc[3] depend on π2.

As π1 is failing, then A1 = ΨP8 (∅) = {c[1], fc[1], fc[2]} by Condition 1. Then, A2 = ΨP8 (A1) = A1 ∪ {c[2], fc[3]} by Condition 3 because π1 ≈π2, π1 is not balanced and goes through arguments c[1] and fc[2] which both belong to A1. It is worth noting that current termination criteria are not able to realize this kind of dependency between π1 and π2. As ΨP8 (A2) gives A2, the fixpoint is reached with all arguments of P8 belonging to Ψ∞P8 (∅). By Proposition 1, all arguments are limited, thus P8 has a finite minimal model. ✷

Example 9 Consider program P9 below derived from program P ′2 of Example 2 by replacing rule r3 of P ′2 with the two rules r3 and r4 below (to satisfy the conditions stated at the beginning of this section):

r0 : magic append([a, b], [c, d]). r1 : magic append(L1, L2) ← magic append([X|L1], L2). r2 : append([ ], L, L) ← magic append([ ], L). r3 : f-magic append(X,L1,L2)←magic append([X|L1],L2). r4 : append([X|L1], L2, [X|L3]) ← f-magic append(X,L1,L2), append(L1, L2, L3).

Figure 5 shows the labelled argument graph of P9, where ma, a, and fma stand for magic append, append and f-magic append, respectively. As π1, π2, and π3 are not growing, then Ψ1P9 (∅) = {ma[1], ma[2], fma[1], fma[2], fma[3], a[2]} by Condition 1. Since fma[1] and fma[2] belong to Ψ1P9 (∅), then a[1] ∈ Ψ 2P9 (∅) by Condition 2. As π5 ≈π4, π5 is not balanced and goes only through a[1] which is in Ψ2P9 (∅), then a[3] belongs to Ψ3P9 (∅) by Condition 3. Since all arguments are in Ψ3P9 (∅), then Ψ3P9 (∅) = Ψ∞P9 (∅) and the program has a finite minimal model. ✷

We are now ready to define the class of bounded programs. Given a program P, we start with the set of restricted arguments AR(P) (see Section 3), which gives a good and efficiently computable approximation of the set of limited arguments; then, we iteratively apply operator ΨP trying to infer more limited arguments. If, eventually, all arguments in arg(P) are determined as limited, then P is bounded. We do not start from the empty set as there are programs P s.t. Ψ∞P (∅) ⊊ Ψ∞P (AR(P)). Observe also that the relation A ⊆ ΨP(A) holds for A = AR(P).

Definition 6 (Bounded programs) The set of bounded arguments of a program P is Ψ∞P (AR(P)). We say that P is bounded iff all its arguments are bounded. The set of all bounded programs is denoted as BP. ✷

Theorem 1 [Correcteness] Given a bounded program P, then SM(P ∪ D) is finite and every M ∈ SM(P ∪ D) is finite for any finite set of database facts D.

Theorem 2 [Complexity] The worst-case time complexity of checking whether a program P belongs to the class BP is O(k + n3 + n m l (s b + m)), where

• k is the cost of building Ω(P) and GL(P),
• n is the number of arguments of P,
• m is the number of basic cycles in GL(P),
• l is the maximal length of a basic cycle,
• s is the maximal number of distinct variables occurring in a term in the head of a rule,
• b is the maximal size of a rule body (considering the number of body atoms and arities of predicate and function symbols).

In the theorem above, O(k) is polynomial in the size of P; O(n3 ) is the complexity of computing the set of restricted arguments. As the number of basic cycles m can be exponential in the size of the program, the overall complexity is exponential. However, in many cases m is "small" (polynomial in the size of P) and the overall complexity becomes polynomial.

The following theorem says that BP strictly includes AR and AP (resp., argument restricted and Γ-acyclic programs), the more general decidable classes in the literature, and is included in the class FG of finitely ground programs.

Definition 7 (Linear programs) A program P is linear iff each node in GL(P) appears in at most one basic cycle. ✷

For instance, P8 and P9 of Examples 8 and 9 are linear, while program P5 of Example 5 is not linear.

Theorem 4 Checking if a linear program P belongs to the class BP can be solved in polynomial time in the size of P.

5 Conclusions

Enhancing answer set solvers by providing support for function symbols has attracted a great deal of interest in recent years. As the introduction of function symbols make common inference tasks undecidable, different classes of programs imposing restrictions on the use of function symbols and guaranteeing decidability of common inference tasks have been proposed. In this paper, we have presented a more general class that strictly includes all classes in the literature, along with different results on its correctness and complexity.