Logic Program Termination Analysis Using Atom Sizes

1 Introduction

Function symbols are widely acknowledged as an important feature in answer set programming as they make modeling easier and increase the language's expressive power. Current solvers provide support for them, but offer only a limited apriori termination analysis of programs. The main problem is that the evaluation of a program (with function symbols) might not terminate and checking termination is undecidable.

To cope with this issue, recent research has focused on identifying decidable classes of logic programs allowing only a restricted use of function symbols but guaranteeing the program evaluation termination (we will discuss current approaches in the related work subsection).

Most of the work in the literature analyzes programs by looking at how terms are propagated from one individual argument to another. More general approaches such as the mapping-restricted [Calautti et al., 2013] and the bounded [Greco et al., 2013a] techniques are able to perform a more complex (yet limited) analysis of how some groups of arguments affect each other. Recently, [Calautti et al., 2014a] proposed the rule-bounded criterion, which checks if the head size is bounded by the size of a body atom in a rule. However, all current approaches have several limitations that we illustrate in the following example.

Example 1 Consider the following simple program P1:

The program evaluation always terminates whatever finite set of facts is added to the program-however, all current termination criteria fail to realize this. For instance, the simple fact that the first argument of p has a size in the head greater than the one in the body prevents several techniques from realizing termination of the program evaluation. Also, when comparing the overall size of the head with the body size, current criteria do not succeed in identifying the program as terminating. In contrast, as we will show in the following, our approach performs a more accurate analysis and realizes that the program evaluation always terminates. ✷

To provide a practical example, below we report a general program which recognizes strings of the language corresponding to an arbitrary LR(1) grammar.

Example 2 Consider the following programP2:

where we use the classical syntax [H|T] for a list. LR(1) grammars can be encoded in a standard form using an action table defined by facts of the form act(〈state〉, 〈symbol〉, 〈operation〉).

Specifically, given the current parsing state 〈state〉 and a symbol 〈symbol〉 to be parsed, 〈operation〉 describes one of the following four parsing operations: shift(〈newstate〉), i.e., the next token is read from the input and pushed to the parsing stack along with the new parsing state 〈newstate〉; reduce(A, B), i.e., there is a production rule A → B in the grammar and the top of the parsing stack contains B (according to 〈state〉), which must be replaced with A; goto(〈newstate〉), i.e., once the reduce operation is complete, the parsing state changes accordingly; accept, i.e., the input string is accepted. The computation starts by providing as input the action table and a fact of the form par([a1, ..., an, $], [s0]), where [a1, ..., an, $] is the input string, followed by the "end of string symbol" $, and [s0] is the parsing stack containing the initial state s0. The string is accepted iff the program model contains two atoms of the form par([$], [s|L]) and act(s, $, accept). ✷

Once again, the program above terminates for every finite set of facts-while none of the current approaches is able to realize it, our technique detects the program as terminating.

Related work. A significant body of work has been done on termination of logic programs under top-down evaluation [De Schreye and Decorte, 1994; Marchiori, 1996; Ohlebusch, 2001; Codish et al., 2005; Schneider-Kamp et al., 2009; Nguyen et al., 2007; Bruynooghe et al., 2007; Baselice et al., 2009; Voets and De Schreye, 2011] and in the area of term rewriting [Sternagel and Middeldorp, 2008; Arts and Giesl, 2000; Endrullis et al., 2008]. Termination properties of query evaluation for normal programs under tabling have been studied in [Riguzzi and Swift, 2013; 2014; Verbaeten et al., 2001]. Another approach are FDNC programs [Eiter and Simkus, 2010], which have infinite answer sets in general, but a finite representation that can be exploited for knowledge compilation and fast query answering.

In this paper, we consider logic programs with function symbols under the stable model semantics [Gelfond and Lifschitz, 1988; 1991], and thus all the 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. Since membership in the class is not decidable, decidable subclasses have been proposed: ω-restricted programs [Syrjanen, 2001], λ-restricted programs [Gebser et al., 2007], finite domain programs [Calimeri et al., 2008], argument-restricted programs [Lierler and Lifschitz, 2009], safe and Γ-acyclic programs [Calautti et al., 2014b]. More general classes are mapping-restricted programs [Calautti et al., 2013], bounded programs [Greco et al., 2013a], and rule- and cycle-bounded programs [Calautti et al., 2014a]. An adornment-based approach that can be used in conjunction with the techniques above to detect more programs as finitely-ground has been proposed in [Greco et al., 2013b].

Our approach recognizes terminating programs that do not belong to any of the aforementioned classes; also, it can be easily combined with them allowing us to identify more programs (we provide a precise comparison in Section 4).

Concepts of "term size" similar to the one used in this paper have been considered to check termination of logic programs evaluated in a top-down fashion [Sohn and Gelder, 1991], in the context of partial evaluation to provide conditions for strong termination and quasi-termination [Leuschel and Vidal, 2014], and in the context of tabled resolution [Riguzzi and Swift, 2013; 2014]. These approaches are geared to work under top-down evaluation, looking at how terms are propagated from the head to the body, while our approach is developed to work under bottom-up evaluation, looking at how terms are propagated from the body to the head. This gives rise to significant differences in how the program analysis is carried out, making one approach not applicable in the setting of the other. As a simple example, the rule p(X) ← p(X) leads to a non-terminating top-down evaluation, while it is completely harmless under bottom-up evaluation.

Our work is also related to research done in the database community on termination of the chase procedure, where existential rules are considered (see [Greco et al., 2012; 2011]).

Contribution. We propose a novel class of logic programs with function symbols whose evaluation always terminates. Our technique is based on the idea of measuring the size of terms and atoms using linear constraints to check whether the rule head size is bounded by the body. The proposed approach generalizes previous work along different dimensions.

First, our approach identifies as terminating strictly more programs than the rule-bounded criterion, including programs that are not identified by any of the current approaches in the literature. While the rule-bounded technique looks at the entire size of a single atom, our technique performs a more accurate analysis by looking at the size of parts of multiple atoms, overcoming different limitations of the rulebounded criterion.

Second, in contrast to several current criteria, rather than adopting an "all-or-nothing" approach (either we can say that the program evaluation terminates or we cannot say anything), our technique can identify arguments that are "limited" (i.e., arguments where there is no infinite propagation of terms) even when the program is not entirely recognized. Identifying arguments that are limited can support the user in the problem formulation. Moreover, termination criteria that use limited arguments as a starting point (e.g., the bounded criterion) can take advantage of this information.

Third, our technique can leverage external information about limited arguments for a better understanding of the program evaluation behavior-current approaches such as the argument-restricted and the bounded criteria can provide such sets of limited arguments when they fail to recognize a program. This feature as well as the previous one are an important step towards the combination of termination criteria, enabling different approaches to benefit from each other-this is an issue where little effort has be done so far.

Finally, we provide results on the correctness, the complexity, and the expressivity of the proposed technique.

Organization. In Section 2 we report preliminaries. Section 3 introduces our technique. Section 4 reports results on the complexity and expressivity. Section 5 shows how our technique can be iteratively applied.

2 Preliminaries

This section recalls syntax and the stable model semantics of logic programs with function symbols [Gelfond and Lifschitz, 1988; 1991; Gebser et al., 2012].

Syntax. We assume to have (pairwise disjoint) infinite sets of logical variables, predicate symbols, and function symbols. Logical variables are used in logic programs and are denoted by upper-case letters. To each logical variable X, there corresponds a (unique) integer variable x (denoted by the same letter in lower case) which may occur in linear constraints. Each predicate and function symbol g is associated with an arity, which is a non-negative integer. Function symbols of arity 0 are called constants. A term is either a logical variable or an expression of the form f(t1, ..., tm), where f is a function symbol of arity m ≥ 0 and t1, ..., tm are terms.

An atom is of the form p(t1, ..., tn), where p is a predicate symbol of arity n ≥ 0 and t1, ..., tn are terms-we also call the atom a p-atom. We use pr(A) to denote the predicate symbol of an atom A. A literal is either an atom A (positive literal) or its negation ¬A (negative literal).

A rule r is of the form

A1 ∨ ... ∨ Am ← B1, ..., Bk, ¬C1, ..., ¬Cn 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). With a slight abuse of notation, we sometimes use body(r) (resp. head(r)) to also denote the set of literals appearing in the body (resp. head) of r. If m = 1, then r is normal; in this case, head(r) denotes the head atom. 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). We assume that programs are range restricted, i.e., for every rule, every logical variable appears in some positive body literal. A term (resp. atom, literal, rule, program) is ground if no logical variables occur in it. A ground normal rule with an empty body is also called a fact.

Let P be a program. The set of all predicate symbols appearing in P (resp. appearing in the head of a rule in P) is denoted as pred(P) (resp. def (P)). 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. The set of all arguments of the predicate symbols in pred(P) is denoted by args(P).

Semantics. Consider a program P. The Herbrand universe HP of P is the possibly infinite set of ground terms that can be built using function symbols (and thus also constants) appearing in P. The Herbrand base BP of P is the set of ground atoms that can be built using predicate symbols appearing in P and ground terms of HP.

A substitution θ is of the form {X1/t1, ...,Xn/tn}, where X1, ...,Xn are distinct logical variables and t1, ..., tn are terms. The result of applying θ to an atom A, denoted Aθ, is the atom obtained from A by simultaneously replacing each occurrence of a logical variable Xi in A with ti if Xi/ti belongs to θ. Two atoms A1 and A2 unify if there exists a substitution θ such that A1θ = A2θ.

A rule (resp. atom) r′ is a ground instance of a rule (resp.

atom) r in P if r′ can be obtained from r by substituting every logical 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 atomAw.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. A ground rule r is satisfied by I, denoted I |= r, if there is a ground literal L in body(r) s.t. valueI(L) = false or there is a ground atomA in head(r) s.t. valueI(A) = true. Thus, if the body of r is empty, r is satisfied by I if there is an atom A in head(r) s.t. valueI(A)=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). 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 I ∈ MM(P I ). The set of stable models of P is denoted by SM(P). It is well known that SM(P) ⊆ MM(P), and SM(P) = MM(P) for positive programs. A positive normal program P has a unique minimal model, which we denote as MM(P).

Limited programs. Consider a program P. An argument p[i] in args(P) is said to be limited iff for every finite set of facts D and for every stable model M of P ∪ D, the set {ti | p(t1, ..., ti, ..., tn) ∈ M} is finite. Moreover, P is said to be limited iff every argument in args(P) is limited.

3 Size-Restricted Programs

In this paper we study new conditions under which a positive normal program P is limited-equivalently, the bottomup evaluation always terminates for every finite set of facts added to the program. It is worth mentioning that our technique can be used to check if an arbitrary program P (possibly with disjunction in the head and negation in the body) has a finite number of stable models, each of them has finite size and can be computed. Specifically, it suffices to apply our technique to a positive normal program st(P) derived from P as follows. Every rule A1 ∨ ... ∨ Am ← body in P is replaced with m positive normal rules of the form Ai ← body+ (1 ≤ i ≤ m) where body+ is obtained from body by deleting all negative literals. In fact, the minimal model of st(P) contains every stable model of P-whence, finiteness and computability of the minimal model of st(P) implies that P has a finite number of stable models, each of finite size, which can be computed [Calautti et al., 2014b]. Thus, for ease of presentation, in the rest of the paper a program is understood to be positive and normal.

Also, notice that a (positive normal) program P is limited iff the program obtained from P by deleting all its facts is limited. Thus, w.l.o.g., hereafter we assume that every given program P does not contain facts.

We start by reporting the definition of firing graph [Calautti et al., 2014a], a directed graph that keeps track of whether a rule can trigger another.

Definition 1 (Firing graph) The firing graph of a program P, denoted Ω(P), is a directed graph whose nodes are the rules in P and where there is an edge 〈r, r′ 〉 iff there exist two (not necessarily distinct) rules r, r′ ∈ P s.t. head(r) and an atom in body(r′ ) unify. ✷

Intuitively, an edge 〈r, r′ 〉 of Ω(P) means that rule r may cause rule r′ to "fire". In the definition above, w.l.o.g., we assume that different rules do not share logical variables, and when r = r′ we assume that r and r′ are two "copies" that do not share any logical variable.

A strongly connected component (SCC) of a program P is a maximal set C of nodes of Ω(P) s.t. every node of C can be reached from every node of C through the edges in Ω(P)-a node always reaches itself.

Given a rule r ∈ P, we say that the head atom is mutually recursive with an atom B ∈ body(r) if there is an SCC C of P containing r and containing a rule r′ (possibly equal to r) s.t. head(r′ ) and B unify. The set of all atoms in body(r) that are mutually recursive with head(r) is denoted as rbody(r).

Given a program P and a set A of limited arguments of P, we say that a rule r ∈ P is A-relevant if head(r) contains at least one variable which does not appear in body(r)\rbody(r) and does not appear in a term ti of a body atom p(t1, ..., tn) such that p[i] ∈ A. Rules that are not A-relevant will not be considered in the analysis of an SCC (Definition 4) because they cannot infinitely propagate terms (when the SCC is considered in isolation), as all head variables appear in either a body atom which is not mutually recursive with the head or in correspondence of a limited argument. The following example illustrates the aforementioned notions.

Example 3 Consider the following programP3:

The firing graph of P3 has the edges 〈r1, r1〉, 〈r2, r2〉, and 〈r1, r2〉. The SCCs of P3 are C1 = {r1} and C2 = {r2}. Atom B is mutually recursive with A, and atom E is mutually recursive with D. Atom C is not mutually recursive with A. Furthermore, given the set of limited arguments A = {p[2]}, rule r2 is A-relevant, since variable X occurring in D appears only in the mutually recursive body atom E inside argument p[1], which is not in A. Conversely, r1 is not Arelevant, since variables X, Y appearing in A occur in the body respectively in the non-mutually recursive atom C and inside p[2] ∈ A of atom B. ✷

We use Z to denote the set of all integers and N to denote the set of all non-negative integers. Given two k-vectors v = (v1, ..., vk) and w = (w1, ..., wk) in Zk , we use v·w to denote the classical scalar product, that is, v · w = ∑ki=1 vi · wi. We also use the notation v[i] to refer to vi, for 1 ≤ i ≤ k.

Definition 2 (Term/atom size) The size of a term t, denoted size(t), is recursively defined as follows:

where x is the integer variable corresponding to X. The size of an atom A = p(t1, ..., tn), denoted as size(A), is the nvector (size(t1), ..., size(tn)). ✷

In the definition above, an integer variable x intuitively represents the possible sizes that the logical variable X can have during the bottom-up evaluation. The size of a term of the form f(t1, ..., tm) is defined by summing up the size of its terms ti plus the arity m of f. Note that the size of every constant is 0.

Example 4 Consider the atom A = p(a, X, f(X, g(X, Y))). Since size(a) = 0, size(X) = x, and size(f(X, g(X, Y))) = 2 + x + (2 + x + y) = 2x + y + 4, we have that size(A) = (0, x, 2x + y + 4). ✷

As mentioned before, one of the features of our technique is the capability of leveraging information about arguments that are known to be limited. In order to enable our technique to exploit this kind of information, several notions introduced in the following are defined w.r.t. a set A of arguments, to be read as the set of arguments that are known to be limited when our criterion is applied to a given program.

Definition 3 (Argument/predicate domain) Given a program P and a set of arguments A, the domain of an argument p[i] ∈ args(P) w.r.t. A, denoted DA(p[i]), is Z if p[i] ∈ A, and N otherwise. The domain of a predicate symbol p of arity n is DA(p) = DA(p[1]) × · · · × DA(p[n]). ✷

Below we define when an argument is A-size-restricted in an SCC of a program-as shown in the following, this ensures that the argument is limited when the SCC is considered in isolation. Then, in Definition 6, we will define how to combine the information coming from all the SCCs in order to determine whether or not an argument is A-size-restricted in the entire program.

Definition 4 (Size-restricted arguments in an SCC)

Consider a program P and a set A of limited arguments of P. Let C be an SCC of P with pred(C) = {p1, ..., pn}. We say that an argument pi[j] of C is A-size-restricted in C iff

1. for every rule r ∈ C such that head(r) = pi(t1, ..., tm) the following condition holds: for every variable X occurring in tj, there exists a term uk of a body atom q(u1, ..., um′ ) s.t. X occurs in uk and q[k] ∈ A; or
2. there exist n vectors αh ∈ DA(ph), 1 ≤ h ≤ n, such that for every A-relevant rule r ∈ C there exists an atom B in body(r) such that if pr(head(r)) = pk and pr(B) = pl, then the following conditions hold:
3. (a) the constraint

is satisfied for every non-negative value of the integer variables in it; and

is satisfied for every non-negative value of the integer variables in it. ✷

Condition 1 of the definition above simply checks if pi[j] is A-size-restricted because for every rule of C having pi in the head, all variables appearing in correspondence of pi[j] appear in the body in correspondence of a limited argument.

As for Condition 2, roughly speaking, Definition 4 says that an argument pi[j] is A-size-restricted in an SCC if, for every (relevant) rule, the size of part of the head is always bounded by the size of part of a body atom, to within a constant factor. When αi[j] = 0, a stricter inequality must be satisfied for the rules having pi in the head. When other coefficients are 0, we are considering only parts of atoms in the analysis-e.g., assuming that αk[1] = 0, this means that the first term in every pk-atom is ignored in the analysis. Notice that only the coefficients associated with limited arguments can assume arbitrary values in Z. We notice that while the rule-bounded criterion allows positive coefficients only, here we allow coefficients to be zero and take negative values (this last case applies to limited arguments only).

Example 5 Consider programP1 of Example 1, reported below:

Let us consider A = ∅. The program has only one SCC C consisting of the rule above, which is A-relevant. The vector αp = (0, 1, 1) allows us to say that all arguments are A-sizerestricted in C. In fact, when arguments p[2] and p[3] are considered, Condition 2(a) of Definition 4 holds since

is satisfied for all non-negative values of the integer variables, and Condition 2(b) is trivially satisfied because both αp[2] and αp[3] are not 0. When argument p[1] is considered, Condition 2(a) is the same as before and thus is satisfied, and Condition 2(b) holds too since the constraint above with a strict inequality is still satisfied for all non-negative values of the integer variables. ✷

Example 6 Consider again program P2 of Example 2, which has only one SCC C coinciding with P2 itself. Let us consider A = ∅. All rules are A-relevant. We now show that every argument is A-size-restricted in C. In particular, consider the inequalities associated with the rules of P2 when the actatoms are selected in the body of the first, second, and fourth rule, and the red-atom is selected for the third rule:

⎧⎪⎪⎨⎪⎪⎩ αact ·(st, sym, 1+s1) ≥ αpar ·(t, 6+s1+sym+st+l) αact ·(st, sym, 2+a+b)≥ αred ·(2+sym+t, 2+st+l, a, b) αred ·(i, 4+s+x+l, a, 2+y+t) ≥ αred · (i, l, a, t) αact ·(st, a, 1+s1) ≥ αpar ·(i, 6+s1+a+st+l)

By incorporating the vectors αact = (1, 1, 1), αpar = (0, 0), αred = (0, 0, 1, 1) into the constraints above, we obtain:

It is easy to see that the constraints above are satisfied for every st, sym, s1, a, b, y, t ∈ N, and thus Condition 2(a) of Definition 4 holds for all arguments. Moreover, since αact[1], αact[2], αact[3], αred[3], and αred[4] are all different from 0, we can say that arguments act[1], act[2], act[3], red[3], and red[4] are A-size-restricted in C, as Condition 2(b) is also satisfied. For arguments par[1], par[2], red[1], and red[2] (whose coefficients are 0), we have to check if the constraints associated with the rules having predicate symbol par (resp. red) in the head, namely the first and the last one (resp. the second and third one), are satisfied with a strict inequality. As this is the case, Condition 2(b) holds, and arguments par[1], par[2], red[1], and red[2] are A-size-restricted in C. ✷

We now define how to determine if an argument is A-sizerestricted in the entire program. This is done by combining the information obtained from the individual analysis of the SCCs. We start by introducing some additional notions.

Given a program P, we assume an arbitrary but fixed numbering C1, ..., Cn of its SCCs. We also define ex-args(P) as the set {p[i/j] | Cj is an SCC of P and p[i] ∈ args(Cj)}. Each element of ex-args(P) is called an extended argument of P. The next tool is called extended argument graph-a directed graph keeping track of the propagation of terms between arguments. It is a refinement of the argument graph of [Calimeri et al., 2008] and it leverages the firing graph to perform a component-wise analysis of how terms are propagated between arguments and to get rid of propagation (between arguments) that cannot really occur.

Definition 5 (Extended argument graph) The extended argument graph of a program P, denoted ∆(P), is a directed graph whose set of nodes is ex-args(P) and where there is an edge 〈q[j/k], p[i/l]〉 iff

• k = l and there is a rule r ∈ Ck such that (1) head(r) is a p-atom, (2) there is a q-atom B in body(r), (3) the i-th term of head(r) and j-th term of B have a common variable, and (4) there is a rule r′ ∈ P such that head(r′ ) and B unify; or
• k ̸= l and p = q, i = j, and there are two rules r1 ∈ Ck and r2 ∈ Cl such that pr(head(r1)) = p and 〈r1, r2〉 is an edge of Ω(P). ✷

Intuitively, an edge 〈q[j/k], p[i/l]〉 of ∆(P) means that there can be a propagation of terms from q[j] in component Ck to p[i] in component Cl. We say that an extended argument p[i/l] depends on an extended argument q[j/k] if there is a path from the latter to the former in ∆(P).

Example 7 Consider again program P3 of Example 3. Figure 1 illustrates ∆(P3). ✷

We are now ready to define when an argument is A-sizerestricted in a program.

Definition 6 (A-size-restricted arguments/programs) Let P be a program and A be a set of limited arguments of P. An argument p[i] is A-size-restricted in P if for every SCC Cl of P such that p ∈ pred(Cl),

1. p[i] is A-size-restricted in Cl, and
2. p[i/l] depends only on extended arguments q[j/k] such that q[j] is A-size-restricted in Ck.

We denote by RA(P) the set of all A-size-restricted arguments in P. We say that P is A-size-restricted iff args(P) = A ∪ RA(P). ✷

Example 8 Consider program P3 of Example 3, whose extended argument graph is shown in Figure 1 and let A = {p[2]}. Below we show that p[1] is A-size-restricted in P3. Since p ∈ pred(C1) and p ∈ pred(C2), we first need to check if p[1] is A-size-restricted in C1 and C2. Since C1 = {r1} and r1 is not A-relevant, we can easily conclude that p[1] is A-size-restricted in C1. In the case of C2 = {r2}, where r2 is A-relevant, we consider the (only) linear constraint associated with r2, which is αp · (1+x, y) ≥ αp · (x, 1+y). Given αp = (1, 1), the constraint is satisfied for all x, y ∈ N, and since αp[1] ̸= 0, then p[1] is A-size-restricted also in C2.

We now just need to check if for every SCC Cl such that p ∈ pred(Cl), p[1/l] only depends on extended arguments q[j/k] such that q[j] is A-size-restricted in Ck. Considering C1, we have that p[1/1] depends only on itself (see Figure 1). Concerning C2, we have that p[1/2] depends on itself and p[1/1]. Since p[1] is A-size-restricted in both C1 and C2, we can conclude that p[1] is A-size-restricted in P3.

Likewise, it can be easily verified that all other arguments of P3 are A-size-restricted in P3 as well. ✷

Theorem 1 Let P be a program and A be a set of limited arguments of P. Every A-size-restricted argument of P is limited. If P is A-size-restricted then it is limited.

4 Complexity and Expressivity

In this section, we provide results on the complexity and the expressivity of the class of A-size-restricted programs.

We start by showing that checking if an argument is Asize-restricted in an SCC is in NP.

Theorem 2 Let P be a program and A be a set of limited arguments of P. Given an SCC C of P, checking whether an argument of C is A-size-restricted in C is in NP.

From the theorem above, we obtain that checking whether a program is A-size-restricted is in NP.

Theorem 3 Let P be a program and A be a set of limited arguments of P. Checking whether (an argument of) P is A-size-restricted (in P) is in NP.

We use AR, BP , RB, and SR to denote, respectively, the set of all argument-restricted [Lierler and Lifschitz, 2009], bounded [Greco et al., 2013a], rule-bounded [Calautti et al., 2014a], and ∅-size-restricted programs. Moreover, given two sets A and B, we use A ∦ B as a shorthand for A ̸⊆ B ∧B ̸⊆ A. The following theorem compares our approach with wellknown terminating classes previously proposed.

Theorem 4 AR ∦ SR, RB ⊊ SR, and BP ∦ SR

Note that our technique strictly generalizes the rulebounded criterion even when the set of limited arguments A is empty. Looking at the size of parts of multiple atoms, as opposed to the entire size of a single atom like the rule-bounded criterion does, allows our criterion to include more programs.

By combining our technique with the argument-restricted or bounded criterion we can recognize more limited programs than by using any of them alone. We use AR + SR (resp. BP + SR) to denote the set of all A-size-restricted programs where, for each program, A is the set of its argumentrestricted (resp. bounded) arguments.

5 Iterated Criterion

The size-restricted technique presented in the previous section starts from a (possibly empty) set of limited arguments A and gives as output a new set of limited arguments A′ . The question is whether the technique, starting from the resulting set of limited arguments A′ , could compute a new set of limited arguments A′′ ⊃ A′ . As shown by the next example, the answer is positive and thus our technique can benefit from an iterative application of itself.

Example 9 Consider the following programP9.

The program has only one SCC consisting of the rule above. Assume that A = ∅. By choosing the first body atom of the rule, we get the following inequality:

The vectors αp = (0, 0) and αb = (1) satisfy the conditions of Definition 4. Therefore, the resulting set of A-sizerestricted arguments is A′ = {b[1]}.

Now, considering A′ as the starting set of limited arguments, we determine that p[1] is limited too, by Condition 1 of Definition 4. The new set of limited arguments is A′′ = A′ ∪ {p[1]}. Finally, considering the vectors αp = (-1, 1) (recall that p[1] ∈ A′′ ) and αb = (0), the constraint is satisfied for all non-negative values of its integer variables. Then, p[2] is limited, A′′′ = A′′ ∪{p[2]}, and hence P9 is limited. ✷

Thus, we introduce a simple operator that iteratively applies the size-restricted criterion by using at each iteration the limited arguments derived at previous iterations.

Definition 7 Let P be a program and A be a set of limited arguments of P. We define the operator ΨP (A) = A∪RA(P). For i ≥ 1, we define the i-th iteration of ΨP as follows:

Obviously, ΨiP (A) ⊆ Ψi+1 P (A) for every i ≥ 1 and since the number of arguments of P is finite, then there always exists a finite n ≤ |args(P)| such that Ψn P (A) = Ψn+1 P (A); we denote Ψn P (A) as Ψ∞ P (A).

Corollary 2 Let P be a program and A be a set of limited arguments of P. Every argument in Ψ∞ P (A) is limited.

6 Conclusion

In this paper, we have proposed a novel class of logic programs with function symbols whose bottom-up evaluation always terminates. Our technique identifies programs that are not captured by any of the current approaches and can be combined with them to recognize even more programs.

Interesting directions for future work are to plug termination criteria in the framework proposed in [Eiter et al., 2013] and study their combination in such a framework, and analyze the relationships between the notions of safety of [Eiter et al., 2013] and the notions of limitedness of termination criteria.