{'fraction_non_alphanumeric': 0.04726131819085707, 'fraction_numerical': 0.0073797476744956805, 'mean_word_length': 4.350514245182645, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 15, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Productivity Checker for Logic Programming

Automated analysis of recursive derivations in logic programming is known to be a hard problem. Both termination and non-termination are undecidable problems in Turing-complete languages. However, some declarative languages offer a practical work-around for this problem, by making a clear distinction between whether a program is meant to be understood inductively or coinductively. For programs meant to be understood inductively, termination must be guaranteed, whereas for programs meant to be understood coinductively, productive non-termination (or"productivity") must be ensured. In practice, such classification helps to better understand and implement some non-terminating computations. Logic programming was one of the first declarative languages to make this distinction: in the 1980's, Lloyd and van Emden's"computations at infinity"captured the big-step operational semantics of derivations that produce infinite terms as answers. In modern terms, computations at infinity describe"global productivity"of computations in logic programming. Most programming languages featuring coinduction also provide an observational, or small-step, notion of productivity as a computational counterpart to global productivity. This kind of productivity is ensured by checking that finite initial fragments of infinite computations can always be observed to produce finite portions of their infinite answer terms. In this paper we introduce a notion of observational productivity for logic programming as an algorithmic approximation of global productivity, give an effective procedure for semi-deciding observational productivity, and offer an implemented automated observational productivity checker for logic programs.


Introduction
Induction is pervasive in programming and program verification. It arises in definitions of finite data (e.g., lists, trees, and other algebraic data types), in program semantics (e.g., of finite iteration and recursion), and proofs (e.g., of properties of finite data and processes). Coinduction, too, is important in these arenas, arising in definitions of infinite data (e.g., lazily defined infinite streams), in program semantics (e.g., of concurrency), and in proofs (e.g., of observational equivalence, or bisimulation, of potentially infinite processes). It is thus desirable to have good support for both induction and coinduction in systems for reasoning about programs.
Given a logic program P and a term A, SLD-resolution provides a mechanism for automatically (and inductively) inferring that P ⊢ A holds, i.e., that P logically entails A. The "answer" for a program P and a query ? ← A is a substitution σ computed from The importance of developing sufficient infrastructure to support coinduction in automated proving has been argued across several communities; see, e.g., [13,17,21]. In LP, the ability to work with non-terminating and coinductive programs depends crucially on understanding the structural properties of non-terminating SLD-derivations. To illustrate, consider the non-terminating programs P 3 , P 4 , and P 5 : Program Program definition For query ? ← p(X), computes the answer: {X → f(f...)} Programs P 3 and P 4 each loop without producing any substitutions at all; only P 5 computes an infinite term at infinity. It is of course not a coincidence that only P 5 resembles a (co)inductive data definition by pattern matching on a constructor, as is commonly used in functional programming.
When an infinite SLD-derivation computes an infinite object, and this object can be successively approximated by applying to the initial query the substitutions computed at each step of the derivation, the derivation is said to be globally productive. The only derivation for program P 5 and the query ? ← p(X) is globally productive since it approximates, in the sense just described, the infinite term p(f(f...)). In terminology of [14], it computes p(f(f...)) at infinity. Programs P 2 and P ′ 1 similarly give rise to globally productive derivations. But no derivations for P 3 or P 4 are globally productive.
Since global productivity determines which non-terminating logic programs can be seen as defining coinductive data structures, we would like to identify exactly when a program is globally productive. But porting functional programming methods of ensuring productivity by static syntactic checks is hardly possible. Unlike pattern matching in functional programming, SLD-resolution is based on unification, which has very different operational properties -including termination and productivity properties -from pattern matching. For example, programs P 1 , P ′ 1 , P 2 , and P 5 are all terminating by termmatching SLD-resolution, i.e., resolution in which unifiers are restricted to matchers, as in term rewriting. We thus call this kind of derivations rewriting derivations.
Example 4 (Coinductive program defining an irrational infinite term). The program P 6 comprises the single clause 0. from(X, scons(X, Y)) ← from(s(X), Y) For P 6 and the query ? ← from(0, Y), SLD-resolution computes at infinity the answer substitution {Y → [0, s(0), s(s(0)), . . .]}. Here [t 1 , t 2 , . . .] abbreviates scons(t 1 , scons(t 2 , . . .)), and similarly in the remainder of this paper. This derivation depends crucially on unification since variables occurring in the two arguments to from in the clause head overlap. If we restrict to rewriting, then there are no successful derivations (terminating or nonterminating) for this choice of program and query.
Example 4 shows that any analysis of global productivity must necessarily rely on specific properties of the operational semantics of LP, rather than on program syntax alone. It has been observed in [11,9] that one way to distinguish globally productive programs operationally is to identify those that admit infinite SLD-derivations, but for which rewriting derivations always terminate. We call this program property observational productivity. The programs P 1 , P ′ 1 , P 2 , P 5 , P 6 are all observationally productive. The key observation underlying observational productivity is that terminating rewriting derivations can be viewed as points of finite observation in infinite derivations. Consider again program P 6 and query ? ← from(0, Y) from Example 4. Drawing rewriting derivations vertically and unification-based resolution steps horizontally, we see that each unification substitution applied to the original query effectively observes a further fragment of the stream computed at infinity: If we compute unifiers only when rewriting derivations terminate, then the resulting derivations exhibit consumer-producer behaviour: rewriting steps consume structure (here, the constructor scons), and unification steps produce more structure (here, new sconses) for subsequent rewriting steps to consume. This style of interleaving matching and unification steps was called structural resolution (or S-resolution) in [9,12].
Model-theoretic properties of S-resolution relative to least and greatest Herbrand models of programs were studied in [12]. In this paper, we provide a suitable algorithm for semi-deciding observational productivity of logic programs, and present its implementation [19], see also Appendix B online. As exemplified above, observational productivity of a program P is in fact a conjunction of two properties of P : 1. universal observability: termination of all rewriting derivations, and 2. existential liveness: existence of at least one non-terminating S-resolution or SLDresolution derivation.
While the former property is universal, the latter must be existential. For example, the program P 1 defining the Peano numbers can have both inductive and coinductive meaning. When determining that a program is observationally productive, we must certify that the program actually does admit derivations that produce infinite data, i.e., that it actually can be seen as a coinductive definition. Our algorithm for semi-deciding observational productivity therefore combines two checks: 1. guardedness checks that semi-decide universal observability: if a program is guarded, then it is universally observable. (The converse is not true in general.) 2. liveness invariant checks ensuring that, if a program is guarded and exhibits an invariant in its consumption-production of constructors, then it is existentially live.
This is the first work to develop productivity checks for LP. An alternative approach to coinduction in LP, known as CoLP [7,21], detects loops in derivations and closes them coinductively. However, loop detection was not intended as a tool for the study of productivity and, indeed, is insufficient for that purpose: programs P 3 , P 4 and P 5 , of which only the latter is productive, are all treated similarly by CoLP, and all give coinductive proofs via its loop detection mechanism.
Our approach also differs from the usual termination checking algorithms in termrewriting systems (TRS) [22,1,8] and LP [3,16,18,20,15]. Indeed, these algorithms focus on guaranteeing termination, rather than productivity, see Section 5. And although the notion of productivity has been studied in TRS [4,5], the actual technical analysis of productivity is rather different there because it considers infinitary properties of rewriting, whereas observational productivity relies on termination of rewriting.
The rest of this paper is organised as follows. In Section 2 we introduce a contraction ordering on terms that extends the more common lexicographic ordering, and argue that this extension is needed for our productivity analysis. We also recall that static guardedness checks do not work for LP. In Section 3 we employ contraction orderings in dynamic guardedness checks and present a decidable property, called GC2, that characterises guardedness of a single rewriting derivation, and thus certifies existential observability. In Section 4 we employ GC2 to develop an algorithm, called GC3, that analyses consumer-producer invariants of S-resolution derivations to certify universal observability. For universally observable programs, these invariants also serve as liveness invariant checks. We also prove that GC3 indeed semi-decides observational productivity. In Section 5 we discuss related work and in Section 6 -implementation and applications of the productivity checker. In Section 7 we conclude the paper.
In this section, we will introduce the contraction ordering on first-order terms, on which our productivity checks will rely. We work with the standard definition of first-order logic programs. A signature Σ consists of a set F of function symbols f, g, . . . each equipped with an arity. Nullary (0-ary) function symbols are constants. We also assume a countable set Var of variables, and a set P of predicate symbols each equipped with an arity. We have the following standard definition for terms, formulae and Horn clauses: In what follows, we will use letters A, B with subscripts to refer to elements of At. Given a program P , we assume all clauses are indexed by natural numbers starting from 0. When we need to refer to ith clause of program P , we will use notation P (i). To refer to the head of clause P (i), we will use notation head (P (i)).
A substitution is a total function σ : Var → T erm. Substitutions are extended from variables to terms as usual: if t ∈ T erm and σ is a substitution, then the application σ(t) is a result of applying σ to all variables in t. A substitution σ is a unifier for t, u if σ(t) = σ(u), and is a matcher for t against u if σ(t) = u. A substitution σ is a most general unifier (mgu) for t and u if it is a unifier for t and u and is more general than any other such unifier. A most general matcher (mgm) σ for t against u is defined analogously.
We can view every term and atom as a tree. Following standard definitions [2,14], such trees can be indexed by elements of a suitably defined tree language. Let N * be the set of all finite words (i.e., sequences) over the set N of natural numbers. A set L ⊆ N * is a (finitely branching) tree language if the following two conditions hold: (i) for all w ∈ N * and all i, j ∈ N, if wj ∈ L then w ∈ L and, for all i < j, wi ∈ L, and (ii) for all w ∈ L, the set of all i ∈ N such that wi ∈ L is finite. A tree language L is finite if it is a finite subset of N * , and infinite otherwise. Term trees (for terms and atoms) are defined as mappings from a tree language L to the given signature, see [2,14,9]. Informally speaking, every symbol occurring in a term or an atom receives an index from L.
In what follows, we will work with term tree representation of all terms and atoms, and for brevity we will refer to all term trees simply as terms. We will use notation t(w) when we need to talk about the element of the term tree t indexed by a word w ∈ L. Note that leaf nodes are always given by variables or constants.
Example 5. Given L = {ǫ, 0, 00, 01}, the atom stream(scons(0, Y)) can be seen as a term tree t given by the map We can use such indexing to refer to subterms, and notation subterm(t, w) will refer to a subterm of term t starting at node w. In the above example, where t = stream(scons(0, Y)), Two most popular tools for termination analysis of declarative programs are lexicographic ordering and (recursive) path ordering of terms. Informally, the idea can be adopted to LP setting as follows. Suppose we have a clause A ← B 1 , . . . , B i , . . . , B n . We may want to check whether each B i sharing the predicate with A is "smaller"' than A, since this guarantees that no infinite rewriting derivation is triggered by this clause. For lexicographic ordering we will write B i < l A and for path ordering we will write B i < p A.
Using standard orderings to prove universal observability works well for program P 2 , since stream(Y) < l stream(scons(0, Y)) and stream(Y) < p stream(scons(0, Y)), and so any rewriting derivation for P 2 terminates. But universal observability of P 6 from Example 4 cannot be shown by this method. Indeed, none of the four orderings from(X, scons(X, Y)) < l from(s(X), Y), from(s(X), Y) < l from(X, scons(X, Y)), from(X, scons(X, Y)) < p from(s(X), Y), and from(s(X), Y) < p from(X, scons(X, Y)) holds because the subterms pairwise disagree on the ordering. This situation is common for LP, where some arguments hold input data and some hold output data, so that some decrease while others increase in recursive calls. Nevertheless, P 6 is universally observable, and we want to be able to infer this. Studying the S-resolution derivation for P 6 in Section 1, we note that universal observability of P 6 is guaranteed by contraction of from's second argument. It is therefore sufficient to establish that terms get smaller in only one argument. This inspires our definition of a contraction ordering, which takes advantage of the tree representation of terms.
Definition 2 (Contraction, recursive contraction). If t 1 and t 2 are terms, then t 2 is a contraction of t 1 (written t 1 ⊲ t 2 ) if there is a leaf node t 2 (w) on a branch B in t 2 , and there exists a branch B ′ in t 1 that is identical to B up to node w, however, t 1 (w) is not a leaf. If, in addition, subterm(t 1 , w) contains the symbol given by t 2 (w), then t 2 is a recursive contraction of t 1 .
We distinguish variable contractions and constant contractions according as t 2 (w) is a variable or constant, and call subterm(t 1 , w) a reducing subterm for t 1 ⊲ t 2 at node w. We call subterm(t 1 , w) a recursive, variable or constant reducing subterm if t 1 ⊲ t 2 is a recursive, variable or constant contraction, respectively. Example 6 (Contraction orderings). We have from(X, scons(X, Y)) ⊲ from(s(X), Y), as the leaf Y in the latter is "replaced" by the term scons(X, Y) in the former. Formally, scons(X, Y) is a recursive and variable reducing subterm. It can be used to certify termination of all rewriting derivations for P 6 . Note that from(s(X), Y) ⊲ from(X, scons(X, Y)) also holds, with (recursive and variable) reducing subterm s(X).
The fact that ⊲ is not well-founded makes reasoning about termination delicate. Nevertheless, contractions emerge as precisely the additional ingredient needed to formulate our productivity check for a sufficiently general and interesting class of logic programs.
In general, static termination checking for LP suffers serious limitations; see, e.g., [3]. The following example illustrates this phenomenon.

Example 7 (Contraction ordering on clause terms is insufficient for termination checks).
The program P 7 , that is not universally observable, is given by mutual recursion: No two terms from the same clause of P 7 can be related by any contraction ordering because their head symbols differ. But recursion arises for P 7 when a derivation calls its two clauses alternately, so we would like to examine rewriting derivations for queries, such as ? ← p(s(X1), X2, s(Y1), Y2) and ? ← p(s(X1), s(X2), s(Y1), s(Y2)), that exhibit its recursive nature. Unfortunately, such queries are not given directly by P 7 's syntax, and so are not available for static program analysis.
As static checking for contraction ordering in clauses is not sufficient, we will define dynamic checks in the next section. The idea is to build a rewriting tree for each clause, and check whether term trees featured in that derivation tree obey contraction ordering.

Rewriting Trees: Guardedness Checks for Rewriting Derivations
To properly reason about rewriting derivations in LP, we need to take into account that i) in LP, unlike, e.g., in TRS, we have conjuncts of terms in the bodies of clauses, and ii) a logic program can have overlapping clauses, i.e., clauses whose heads unify. These two facts have been analysed in detail in the LP literature, usually using the notion of andor-trees and, where optimisation has been concerned, and-or-parallel trees. We carry on this tradition and consider a variant of and-or trees for derivations. However, the trees we consider are not formed by general SLD-resolution, but rather by term matching resolution. Rewriting trees are so named because each of their edges represents a term matching resolution step, i.e., a matching step as in term rewriting.
Definition 3 (Rewriting tree). Let P be a logic program with n clauses, and A be an atomic formula. The rewriting tree for P and A is the possibly infinite tree T satisfying the following properties.
-A is the root of T -Each node in T is either an and-node or an or-node -Each or-node is given by P (i), for some i ∈ {0, . . . , n} -Each and-node is an atom seen as a term tree.
-For every and-node A ′ occurring in T , if there exist exactly k > 0 distinct clauses P (j), . . . , P (m) in P (a clause P (i) has the form B i ← B i 1 , . . . , B i ni for some n i ), such that A ′ = θ j (B j ) = . . . = θ m (B m ), for mgms θ j , . . . , θ m , then A ′ has exactly k children given by or-nodes P (j), . . . , P (m), such that, every or-node P (i) has n i children given by and-nodes θ i (B i 1 ), . . . , θ i (B i ni ). When constructing rewriting trees, we assume a suitable algorithm [9] for renaming free variables in clause bodies apart. Figure 1 gives examples of rewriting trees. An andsubtree of a rewriting tree (a subtree in which a derivation always pursues only one or-choice at a time) is a rewriting derivation, see [9] for a formal definition.
Because mgms are unique up to variable renaming, given a program P and an atom A, rewriting tree T for P and A is unique. Following the same principle as with definition of term trees, we use suitably defined finitely-branching tree languages for indexing rewriting trees, see [9] for precise definitions. When we need to talk about a node of a rewriting tree T indexed by a word w ∈ L, we will use notation T (w).
We can now formally define our notion of universal observability.
Definition 4 (Universal observability). A program P is universally observable if, for every atom A, the rewriting tree for A and P is finite.
Programs P 1 , P ′ 1 , P 2 , P 5 , P 6 are universally observable, whereas programs P 3 , P 4 and P 7 are not. An exact analysis of why P 7 is not universally observable is given in Example 9.
We can now apply the contraction ordering we defined in the previous section to analyse termination properties of rewriting trees. A suitable notion of guardedness can be defined by checking for loops in rewriting trees whose terms fail to decrease by any contraction ordering. But note that our notion of a loop is more general than that used in CoLP [7,21] since it does not require the looping terms to be unifiable.
Definition 5 (Loop in a rewriting tree). Given a program P and an atom A the rewriting tree T for P and A contains a loop at nodes w and v, denoted loop(T, w, v), if w properly precedes v on some branch of T , T (w) and T (v) are and-nodes whose atoms have the same predicate, and parent or-nodes of T (w) and T (v) are given by the same clause P (i).
Examples of loops in rewriting trees are given (underlined) in Figure 1.
If T has a loop at nodes w and v, and if t is a recursive reducing subterm for T (w) ⊲ T (v), then loop(T, w, v) is guarded by (P (i), t), where P (i) is the clause that was resolved against to obtain T (w) and T (v). It is unguarded otherwise. A rewriting tree T is guarded if all of its loops are guarded, and is unguarded otherwise. We write GC2(T ) when T is guarded, and say that GC2(T ) holds.
Example 8. In Figure 1, we have (underlined) loops in the third rewriting tree (for q(s(X ′′ ), s(X ′′ ), s(Y ′ ), Y ′′ ) and q(s(X ′ ), s(X ′′ ), Y ′′ , Y ′′ )) and the fourth rewriting tree (for q(s(X ′′ ), s(X ′′ ), s(Y ′ ), s(Y ′′ )) and q(s(X ′′ ), s(X ′′ ), s(Y ′′ ), s(Y ′′ ))). Neither is guarded. In the former case, there is a contraction on the third argument, but because s(Y ′ ) and Y ′′ do not share a variable, it is not recursive contraction. In the latter loop, there is no contraction at all. By Definition 5, each repetition of a clause and predicate in a branch of a rewriting tree triggers a check to see if the loop is guarded by some recursive reducing subterm.
Proposition 1 (GC2 is decidable). GC2 is a decidable property of rewriting trees. 4 The proof of Proposition 1 also establishes that every guarded rewriting tree is finite.
The decidable guardedness property GC2 is a property of individual rewriting trees. But our goal is to decide guardedness universally, i.e., for all of a program's rewriting trees. The next example shows that extrapolating from existential to universal guardedness is a difficult task.
Example 9 (Existential guardedness does not imply universal guardedness). For program P 7 , the rewriting trees constructed for the two clause heads p(s(X ′ ), X ′′ , Y ′ , Y ′′ ) and q(s(X ′ ), X ′′ , s(Y ′ ), Y ′′ ) are both guarded since neither contains any loops at all. Nevertheless, there is a rewriting tree for P 7 (the last tree in Figure 1) that is unguarded and infinite. The third tree is not guarded (due to the unguarded loop), but it is finite.
The example above shows that our initial idea of checking rewriting trees generated by clause heads is insufficient to detect all cases of nonterminating rewriting. Since a similar P7 (1) . . . situation can obtain for any finite set of rewriting trees, universal observability, and hence observational productivity, of programs cannot be determined by guardedness of rewriting trees for program clauses alone. The next section addresses this problem.

Derivation Trees: Observational Productivity Checks
The key idea of this section is, given a program P , to identify a finite set S of rewriting trees for P such that checking guardedness of all rewriting trees in S is sufficient for guaranteeing guardedness of all rewriting trees for P . One way to identify such sets will be to use the strategy of Example 9 and Figure 1: for every clause P (i) of P , to construct a rewriting tree for the head of P (i), and, if that tree is guarded, explore what kind of mgus the leaves of that tree generate, and see if applications of those mgus may give an unguarded tree. As Figure 1 shows, we may need to apply this method iteratively until we find a nonguarded rewriting tree. But we want the number of such iterations to be finite. This section presents a solution to this problem.
We start with a formal definition of rewriting tree transitions, which we have seen already in Figure 1, see also Figure 2.
Definition 6 (Rewriting tree transition). Let P be a program and T be a rewriting tree for P and an atom A. If T (w) is a leaf node of T given by an atom B, and B unifies with a clause P (i) via mgu σ, we define a tree T w as follows: we apply σ to every and-node of T , and extend the branches where required, according to Definition 3.
Computation of T w from T is denoted T → T w . The operation T → T w is the tree transition for T and w.
If a rewriting tree T is constructed for a program P and an atom A, a (finite or infinite) sequence T → T ′ → T ′′ → . . . of tree transitions is an S-resolution derivation for P and A. For a given rewriting tree T , several different S-resolution derivations are possible from T . This gives rise to the notion of a derivation tree.
Definition 7 (Derivation tree, guarded derivation tree). Given a logic program P and an atom A, the derivation tree D for P and A is defined as follows: -The root of D is given by the rewriting tree for P and A.
-For a rewriting tree T occurring as a node of D, if there exists a transition T → T w , for some leaf node w in T , then the node T has a child given by T w .
A derivation tree is guarded if each of its nodes is a guarded rewriting tree, i.e., if GC2(T ) holds for each of its nodes T . Figure 1 shows an initial fragment of the derivation tree for P 7 and p(s(X ′ ), X ′′ , Y ′ , Y ′′ ). Note that we now have three kinds of trees: term trees have signature symbols as nodes, rewriting trees have atoms (term trees) as nodes, and derivation trees have rewriting trees as nodes. For a given P and A, the derivation tree for P and A is unique up to renaming. We use our usual notation D(w) to refer to the node of D at index w ∈ L.
Definition 8 (Existential liveness, observational productivity). Let P be a universally observable program and let A be an atom. An S-resolution derivation for P and A is live if it constitutes an infinite branch of the derivation tree for P and A. The program P is existentially live if there exists a live S-resolution derivation for P and some atom A. P is observationally productive if it is universally observable and existentially live.
To show that observational productivity is semi-decidable, we first show that universal observability is semi-decidable by means of a finite (i.e., decidable) guardedness check. We started this section by motivating the need to construct a finite set S of rewriting trees checking guardedness of which will guarantee guardedness for any rewriting tree for the given program. Our first logical step is to use derivation trees built for clause heads as generators of such a set S. Due to the properties of mgu's used in forming branches of derivation trees, derivation trees constructed for clause heads generate the set of most general rewriting trees. The next lemma exposes this fact:

Lemma 1 (Guardedness of derivation trees implies universal observability).
Given a program P , if derivation trees for P and each head (P (i)) are guarded, then P is universally observable.
However, derivation trees are infinite, in general. So it still remains to define a method that extracts representative finite subtrees from such derivation trees; we call such subtrees observation subtrees. For this, we need only be able to detect an invariant property guaranteeing guardedness through tree transitions in the given derivation tree. To illustrate, let us check guardedness of the program P 6 . As it consists of just one clause, we take the head of that clause as the goal atom, and start constructing the infinite derivation tree D for P 6 and from(X, scons(X, Y)) as shown in Figure 2. The first rewriting tree in the derivation tree has no loops, so we cannot identify any invariants. We make a transition to the second rewriting tree which has one loop (underlined) involving the recursive reducing subterm [s(X), Y ′ ]. This reducing subterm is our first candidate invariant, it is the pattern that is consumed from the root of the second rewriting tree to its leaf. We now need to check this pattern is added back, or produced, in the next tree transition. The next mgu involves substitution Y ′ → [s(s(X)), Y ′′ ]. Because this derivation gradually computes an infinite irrational term (rational terms are terms that can be represented as trees that have a finite number of distinct subtrees), the two terms [s(X), Y ′ ] and [s(s(X)), Y ′′ ] we have identified are not unifiable. We need to be able to abstract away from their current shape and identify a common pattern, which is [ , ]. By the properties of mgu's used in transitions, such most general pattern can always be extracted from the clause head itself. Indeed, the subterm of the clause head from(X, scons(X, Y)) has the subterm [X, Y] that is exactly the pattern we look for. Thus, our current (coinductive) assumption is: given a rewriting tree T in the derivation tree D, [X, Y] will be consumed by rewriting steps from its root to its leaves, and exactly [X, Y] will be produced (i.e., added back) in the next tree transition. X and Y are seen as placeholders for some terms. Consumption is always finite (by the loop guardedness), and production is potentially infinite.
We now need to check that this coinductive assumption will hold for the next rewriting tree of D. The third rewriting tree indeed has guarded loops with recursive reducing subterm [s(s(X)), Y ′′ ], and the next mgu it gives rise to is Y ′′ → [s(s(s(X))), Y ′′ ]. Again, to abstract away the common pattern, we look for a subterm in the clause head of P 6 (0) that matches with both of these terms, it is the same subterm [X, Y]. Thus, our coinductive assumption holds again, and we conclude by coinduction that the same pattern will hold for any further rewriting tree in D. When implementing this reasoning, we take the observation subtree of D up to the third tree shown in Figure 2 as a sufficient set of rewriting trees to check guardedness of (otherwise infinite) D.
The rest of this section generalises and formalises this approach. In the next definition, we introduce the notion of a clause projection to talk about the process of "abstracting away" a pattern from an mgu σ by matching it with a subterm t of a clause head. When t also matches with a recursive reducing subterm of a loop in a rewriting tree, we call t a coinductive invariant.
Definition 9 (Clause projection and coinductive invariant). Let P be a program and A be an atom, and let D be a derivation tree for P and A in which a tree transition from T to T ′ is induced by an mgu σ of some P (k) and an atom B given by a leaf node T (u).
The clause projection for T ′ , denoted π(T ′ ), is the set of all triples (P (k), t, v), where t is a subterm of head (P (k)) at position v, such that the following conditions hold: σ(B)⊲B with variable reducing subterm t ′ , and t ′ matches against t (i.e. t ′ = σ ′ (t) for some σ ′ ).
Additionally, the coinductive invariant at T ′ , denoted ci(T ′ ), is a subset of the clause projection for T ′ , satisfying the following condition. An element (P (k), t, v) ∈ π(T ′ ) is also in ci(T ′ ), if T contains a loop in the branch leading from T 's root to T (u) that is guarded by (P (k), t ′′ ) for some t ′′ such that t ′′ matches against t (t ′′ = θ(t) for some θ).
Given a program P , an atom A and a derivation tree D for P and A, the clause projection set for D is cproj(D) = T π(T ) and the coinductive invariant set for D is cinv(D) = T ci(T ), where these unions are taken over all rewriting trees T in D.
Generally, clause projection sets are finite, as the number of subterms in the clause heads of P is finite. This property is crucial for termination of our method: Proposition 2 (Finiteness of clause projection sets). Given a program P , an atom A, and a derivation tree D for P and A, the clause projection set cproj(D) is finite.
In particular, this holds for derivation trees induced by clause heads.
We terminate the construction of each branch of a derivation tree when we notice repeating coinductive invariant. A subtree we get as a result is an observation subtree. Formally, given a derivation tree D for a program P and an atom A, with a branch in which nodes D(w) and D(wv) are defined, if ci(D(w)) = ci(D(wv)) = ∅, then D has a guarded transition from D(w) to D(wv) (denoted D(w) =⇒ D(wv)). Every guarded transition thus identifies a repeated "consumer-producer" invariant in the derivation from D(w) to D(wv). This tells us that observation of this branch of D can be concluded. Imposing this condition on all branches of D gives us a general method to construct finite observation subtrees of potentially infinite derivation trees: Definition 10 (Observation subtree of a derivation tree). If D is a derivation tree for a program P and an atom A, the tree D ′ is the observation subtree of D if 1) the roots of D and D ′ are given by the rewriting tree for P and A, and 2) if w is a node in both D and D ′ , then the rewriting trees in D and D ′ at node w are the same and, for every child w ′ of w in D, the rewriting tree of D ′ at node w ′ exists and is the same as the rewriting tree of D at w ′ , unless either a) GC2 does not hold for D(w ′ ), or b) there exists a v such that D(v) =⇒ D(w). In either case, D ′ (w) is a leaf node. We say that D ′ is unguarded if Condition 2a holds for at least one of D's nodes, and that D ′ is guarded otherwise.
A branch in an observation subtree is thus truncated when it reaches an unguarded rewriting tree or its coinductive invariant repeats. The observation subtree of any derivation tree is unique. The following proposition and lemma prove the two most crucial properties of observation subtrees: that they are always finite, and that checking their guardedness is sufficient for establishing guardedness of the whole derivation trees.
Proposition 3 (Finiteness of observation subtrees). If D is a derivation tree for a program P and an atom A then the observation subtree of D is finite.
Lemma 2 (Guardedness of observation subtree implies guardedness of derivation tree). If the observation subtree for a derivation tree D is guarded, then D is guarded.
Example 11 (Finite observation subtree of an infinite derivation tree). The initial fragment D ′ of the infinite derivation tree D given by the three rewriting trees in Figure 2 is D's observation subtree. The third rewriting tree T ′′ in D is the last node in the observation tree D ′ because ci(T ′ ) = ci(T ′′ ) = {(P 6 (0), scons(X, Y), 1)} = ∅. Since D ′ is guarded, Lemma 2 above ensures that the whole infinite derivation tree D is guarded.
It now only remains to put the properties of the observation subtrees into practical use, and, given a program P , construct finite observation subtrees for each of its clauses. If none of these observation subtrees detects unguarded rewriting trees, we have guarantees that this program will never give rise to infinite rewriting trees. The next definition, lemmas and a theorem make this intuition precise.
Definition 11 (Guarded clause, guarded program). Given a program P , its clause P (i) is guarded if the observation subtree for the derivation tree for P and the atom head (P (i)) is guarded, and P (i) is unguarded otherwise. A program P is guarded if each of its clauses P (i) is guarded, and unguarded otherwise. We write GC3(P (i)) to indicate that P (i) is guarded, and similarly for P .

Lemma 3 uses Proposition 3 to show that GC3 is decidable.
Lemma 3 (GC3 is decidable). GC3 is a decidable property of logic programs. Theorem 1 (Universal observability is semi-decidable). If GC3(P ) holds, then P is universally observable.
Proof: If GC3(P ) holds, then the observation subtree for each P (i) is guarded. Thus, by Lemma 2, the derivation tree for each P (i) is guarded. But then, by Lemma 1, P is universally observable. Combining this with Lemma 3, we also obtain that universal observability is semi-decidable.
The converse of Theorem 1 does not hold: the program comprising the clause p(a) ← p(X) is universally observable but not guarded, hence the above semi-decidability result.
From our check for universal observability we obtain the desired check for existential liveness, and thus for observational productivity: Corollary 1 (Observational productivity is semi-decidable). Let P be a guarded logic program. If there exists a clause P (i) such that the derivation tree D for P and P (i) has an observation subtree D ′ one of whose branches was truncated by Condition 2b of Definition 10, then P is existentially live. In this case, since P is also guarded and hence universally observable, P is observationally productive.
Because observational productivity is a combination of universal observability and existential liveness, and the former property amounts to termination of all rewriting trees, there is an intersection between this work and termination checking in TRS [22,1,8].
Termination checking via transformation of LP into TRS has been given in [20]. Here we consider termination of restricted form of SLD-resolution (given by rewriting derivations), therefore a much simpler method of translation of LP into TRS can be used for our purposes [6]: Given a logic program P and a clause P (i) = A ← B 1 , . . . , B n containing no existential variables, we define a rewrite rule A → f i (B 1 , . . . , B n ) for some fresh function symbol f i . Performing this translation for all clauses, we get a translation from P to a term-rewriting system T P . Rewriting derivations for P can be shown operationally equivalent to term-rewriting reductions for T P ; see [6] for a proof. Therefore, for logic programs containing no existential variables, any termination method from TRS may be applied to check universal observability (but not existential liveness).
Algorithmically, our guardedness check compares directly with the method of dependency pairs due to Arts and Giesl [1,8]. Consider again T P obtained from a program P . The set R of dependency pairs contains, for each rewrite rule A → f i (B 1 , . . . , B n ) in T P , a pair (A, B j ), j = 1, . . . , n; see [6]. The method of dependency pairs consists of checking whether there exists an infinite chain of dependency pairs (s i , t i ) i=1,2,3,... such that σ i (t i ) → * σ i+1 (s i+1 ). If there is no such infinite chain, then T P is terminating. Again this translation from LP to dependency pairs in TRS is simpler than in [15], as rewriting derivations are a restricted form of SLD-resolution. Due to the restricted syntax of T P (compared to the general TRS syntax), generating the set of dependency pairs is equivalent to generating a set of rewriting trees for each clause of P and assuming σ i = σ i+1 (cf. our GC2). To find infinite chains, a dependency graph is defined, in which dependency pairs are nodes and arcs are defined whenever a substitution that allows a transition from one pair to another can be found. Finding such substitutions is the hardest part algorithmically. Note that every pair of neighboring and-nodes in a rewriting tree corresponds to a node in a dependency graph. Generating arcs in a dependency graph is equivalent to using our GC3 to find a representative set of substitutions. However, the way GC3 generates such substitutions via rewriting tree transitions differs completely from the methods approximating dependency graphs [1,22], and relies on the properties of S-resolution, rather than recursive path orderings. This is because GC3 additionally generates coinductive invariants for checking existential liveness of programs.
Conceptually, observational productivity is a new property that does not amount to either termination or nontermination in LP or TRS. E.g. programs P 3 and P 4 are nonterminating (seen as LP or TRS), and P 8 : p(X) ← q(Y ) is terminating (seen as LP and TRS) but none of them is productive. This is why the existing powerful tools (such as AProVE) and methods [1,8,15,20] that can check termination or nontermination in TRS or LP are not sufficient to serve as productivity checks. To check termination of rewriting trees, GC3 can be substituted by existing termination checkers for TRS, but none of the previous approaches can semi-decide existential liveness as GC3 does.

Implementation and Applications
We implemented the observational productivity checker in parallel Go (golang.org) [19], which allows to experiment with parallelisation of proof search [10]. Loading a logic program P , one runs a command line to initialise the GC3 check. The algorithm then certifies whether or not the program is guarded (and hence universally observable). If that is the case, it also checks whether GC3 found valid coinductive invariants, i.e. whether P is existentially live and hence admits coinductive interpretations for some predicates. Appendix B (available in online version) gives further details.
In the context of S-resolution [11,9], observational productivity of a program is a pre-condition for (coinductive) soundness of S-resolution derivations. This gives the first application for the productivity checker. But the notion of global productivity (as related to computations at infinity [14]) is a general property tracing its roots to the 1980s. A program is productive, if it admits SLD-or S-resolution derivations that compute (or produce) an infinite term at infinity. Thus the productivity checker has more general practical significance for Prolog. In this paper we further exposed its generality by showing that productivity can be seen as a general property of logic programs, rather than property of derivations in some special dialect of Prolog.
Based on this observation, we identify three applications for productivity checks encompassing the S-resolution framework. (1) In the context of CoLP [7,21] or any other similar tool based on loop detection in SLD-derivations, one can run the observational productivity checker for a given program prior to running the usual interpreter of CoLP. If the program is certified as productive, all computations by CoLP for this program will be sound relative to the computations at infinity [14]. It gives a way to characterise a subset of theorems proven by CoLP that describe the process of production of infinite data. I.e., as explained in Introduction, CoLP will return answers for programs P 3 , P 4 and P 5 . But if we know that only P 5 is productive, we will know that only CoLP's answers for P 5 will correspond to production of infinite terms at infinity.
(2) As our productivity checker also checks liveness of programs, it effectively identifies which predicates may be given coinductive semantics. This knowledge can be used to type predicates as inductive or coinductive. We can use these types to mark predicates in CoLP or any other coinductive dialect of logic programming, cf. Appendix B.
(3) Observational productivity is also a guarantee that a sequence of mgus approximating the infinite answer can be constructed lazily even if the answer is irregular. E.g. our running example of program P 6 is irrational and hence cannot be handled by CoLP's loop detection. But even if we cannot form a closed-term answer for a query from(0, X), the productivity checker gives us a weaker but more general certificate that lazy approximation of our infinite answer is possible.
These three groups of applications show that the presented productivity checker can be implemented and applied in any dialect of logic programming, irrespective of the fact that it initially arose from S-resolution research [11,9].

Conclusions
In this paper we have introduced an observational counterpart to the classical notion of global productivity of logic programs. Using the recently introduced formalism of Sresolution, we have defined observational productivity as a combination of two program properties, namely, universal observability and existential liveness. We have introduced an algorithm for semi-deciding observational productivity for any logic program. We did not impose any restrictions on the syntax of logic programs. In particular, our algorithm handles both existential variables and non-linear recursion.
The algorithm relies on the observation that rewriting trees for productive and guarded programs must show term reduction relative to a contraction ordering from their roots to their leaves. But S-resolution derivations involving such trees can only proceed by adding term structure back in transitioning to new rewriting trees via mgus. This "producer/consumer" interaction can be formally traced by observing a derivation's coinductive invariants: these record exactly the term patterns that both reduce in the loops of rewriting trees and are added back in transitions between these trees.