DGp(P), whose vertices are the predicate symbols of P's language. Edges are defined by analogy with the atom dependency graph. An *odd-cycle* is a cycle in an atom (resp.

predicate) dependency graph with an odd number of negative edges. A ground atom (resp.

a predicate symbol) is *odd-cyclic* if it occurs in an odd-cycle. Given a graph G, we denote by SCC(G) the set of all strongly connected components in G. We say that a rule R is in a component C of a predicate dependency graph if pred(head(R)) is a vertex in C.

## 3 Norms And Term Comparisons

Norms have been introduced for the static termination analysis of logic programs, see for example (Bossi et al. 1994; Genaim et al. 2002). Termination proofs require certain predicate arguments to decrease strictly during recursion; we admit cyclic programs, instead, and consider non-strict orderings. For all sets of (possibly nonground) terms t, let |t| (the norm of t) be the number of variables and function symbols occurring in t (constants are regarded as 0-ary functions). Norms are extended to term sequences ~t = t1**, . . . , t**n in the natural way: By |t1**, . . . , t**n| we denote |t1| + **· · ·** + |tn|. For all vectors of terms ~t and
~u, define ~t 4 ~u (resp. ~t ≺ ~u) iff for all grounding substitutions σ, |~tσ| ≤ |~uσ| (resp.

|~tσ| < |~uσ|). Moreover, we write ~t - ~u iff ~t is *almost never larger than* ~u, that is, there exist only finitely many (possibly no) grounding substitutions σ such that |~tσ| > |~uσ|. Note that ~t ≺ ~u ⇒ ~t 4 ~u and ~t 4 ~u ⇒ ~t - ~u. Note also that the norm over term sequences and the three comparison relations are insensitive to permutations. More precisely, for all permutations ~t1 of ~t, we have |~t1| = |~t|; therefore, if ⋖ is any of the relations 4, ≺, and -,
then for all ~u, ~t1 ⋖ ~u ⇔ ~t ⋖ ~u and ~u ⋖~t1 ⇔ ~u ⋖~t. All of these relations can be computed via simple variable occurrence counting.

## Theorem 3.1

Let NOcc(**s,~t**) denote the number of occurrences of symbol s in ~t. For all (possibly nonground) term vectors ~t and ~u, 1. ~t ≺ ~u iff |~t| < |~u| and for all variables x, NOcc(**x,~t**) ≤ NOcc(**x, ~u**); 2. ~t 4 ~u iff |~t**| ≤ |**~u| and for all variables x, NOcc(**x,~t**) ≤ NOcc(**x, ~u**); 3. ~t - ~u iff either ~t 4 ~u or for all variables x, NOcc(**x,~t**) < NOcc(**x, ~u**)
1.

Proof. It is easier to prove the contrapositive (which is equivalent).

1) First suppose that |~t**| ≥ |**~u|. Then for all σ mapping all variables onto constants, we have |~t| = |~tσ | and |~u| = |~uσ|. This implies |~tσ | ≥ |~uσ|, and hence ~t ≺ ~u does not hold.

Second, if for some variable x, NOcc(**x,~t**) > NOcc(**x, ~u**), then there exists a σ mapping all variables but x onto constants, and mapping x on a term with size > |u|. It is not hard to see that |~tσ | > |~uσ|, and hence ~t ≺ ~u does not hold. This concludes the proof of point 1. The proof of points 2 and 3 is based on analogous arguments. ✷