Semantics of infinite tree logic programming (Q1090469)

The logic programs considered here consist of clauses \(A\leftarrow S[ ]B\), where A is an atom, B is a finite sequence of atoms and S is a finite sequence of equations and inequations. Unification is made as in PROLOG, i.e. without ''occurs check'', so f(x) and x are unifiable and the result is the infinite term f(f(...)). The main difference from the treatment in the literature [cf. \textit{J. W. Lloyd}, Foundations of logic programming (1984; Zbl 0547.68005)] concerns inequalities. The equation (resp. inequation) of terms u, v is true for a substitution s if us, vs coincide (resp. do not coincide). A satisfier of a system S of equations and inequations is a substitution s such that any element of S is true under any ground instance of s. Derivation sequences, success set SS(P), finite failure set FF(P), immediate consequence function \(T_ p\) for a program P are defined in a familiar way. In the absence of inequations \(T_ p\) is continuous in Baire topology on infinite terms and atoms containing such terms, but for the program \(Q=\{p(x)\leftarrow (x=a[ ]q(y));q(x)\leftarrow (x=f(y),x\neq f(x)[ ]q(y))\}\), the \(T_ Q\) is discontinuous at q(f(f(...))). So, instead of simply considering closed Herbrand interpretations to prove standard results on fixed points, the authors have to check that the results of T-operations have rational cover: any ground atom in a set is an instance of a rational atom (having only a finite number of subterms). This turns out to be possible since unification (without the occurs check) preserves rationality and any finite system S having ground satisfier s, has also a rational satisfier s'\(\geq s\). Defining a (Clark-)completed program \(P^*\) for a program P in the usual way, the authors prove that \(P^*\vDash A\) iff A belongs to SS(P). Here \(\vDash\) means consequence in all Herbrand models. Similar equivalence for \(\sim A\) and FF(P) holds exactly when P is derivation compact: the sequence S' of equations and inequations arising in any (possibly infinite) P-derivation is solvable iff each of its finite stumps is solvable. This is true for programs containing no inequations, but is false for the program Q above.