The expressive power of stratified logic programs (Q803773)

Along the interface between the theory of logic programming and relational database theory a particular class of programs has been discovered which is in some sense maximal with respect to the property of having a well behaved semantics. It is the class of stratified programs, consisting of programs in a Datalog style, which combine recursion and negation, with the proviso that the collection of intensional predicates ocurring in these programs is stratified: the predicates can be ordered into strata in such a way that recursive definitions don't invoke predicates in a higher stratum than the predicate defined by this definition, and that all used predicates from the same stratum occur just positively. Aside from describing the class of stratified programs itself the theory has been looking for an independent description of its expressive power. For some time researchers believed that the expressive power of stratified programs over finite structures coincides with that of fixedpoint logic. Such an assertion was stated and proved by Chandra and Harel in 1985. The author of the present paper spotted a difficulty in the proof, and subsequently the result was found to be false by Dahlhaus in 1987. The present paper presents a proof for the correct characterization: the class of stratified programs are as powerful as the existential fragment of fixedpoint logic. Also the full fragment of fixedpoint logic is of a higher expressive power. The proof uses the game trees introduced by Chandra and Harel in a paper from 1982. The result is extended to some infinite structures as well.