On the Alternation-Free Horn μ-calculus

摘要

The Horn μ-calculus is a formalism extending logic programs by specifying for each predicate symbol with which (greatest or least) fix-point semantics, its denotation has to be computed. When restricted to a particular class of logic programs called uniform, the Horn μ-calculus provides a syntactic extension for Rabin tree automata. However, it has been shown that the denotation of the Horn μ-calculus restricted to a uniform program remains a regular set of trees and that moreover, the emptiness of the denotation of a predicate p is a Dexptime-complete problem (in the size of the program). In [3], these results have been extended to uniform programs that may contain both existential and universal quantifications on the variables occurring in the body of "clauses": considering this extension, the denotation of a program remains a regular set of trees, but the best known algorithm for testing the emptiness of the denotation of a predicate is doubly-exponential in the size of the program. In this paper, we consider uniform logic programs with both kinds of quantification in the body. But we add to the Horn μ-calculus a limitation on the way the fix-point semantics is specified for predicates. This restriction is close to the one defining the alternation-free fragment of the μ-calculus. Therefore, we name this fragment of the Horn μ-calculus the alternation-free fragment. We devise for it an algorithm which performs the emptiness test for the denotation of a predicate in single-exponential time in the size of the program. To obtain this result, we develop a constructive approach based on a new kind of tree automata running on finite and infinite trees, called monotonous tree automata. These automata are defined by means of a family of finite and complete lattices. The acceptance condition for monotonous tree automata is based on the ordering relations of the lattices.