Bounds on the propagation of selection into logic programs

摘要

We consider the problem of propagating selections into logic programs (i.e., recursive Horn clause programs). In particular, we study the class of chain programs and formalize selection propagation on such a logic program as: the task of finding an equivalent program containing only monadic derived predicates. Selection propagation is always possible for database programs (i.e., first-order formula programs) and is often a desirable optimization. We show that the situation is qualitatively different for logic programs. We associate a context free language L(H) with every chain program H. We show that, given H, propagating a selection involving some constant is possible iff L(H) is regular and therefore undecidable. We also show that propagating a selection of the form p(X, X) is possible iff L(H) is finite and therefore decidable. We demonstrate the connection of these two cases, respectively, with the weak monadic second-order theory of one successor and with monadic generalized spectra. We further clarify the analogy between chain programs and context-free languages from the point of view of program equivalence, first-order expressibility over finite structures, and selection propagation heuristics.