Tie-Breaking Semantics and Structural Totality

摘要

We address the question of when the structure of a Datalog program with negation guarantees the existence of a fixpoint. We propose a semantics of Datalog programs with negation, which we call the tie-breaking semantics. The tie-breaking semantics can be computed in polynomial time and results in a fixpoint whenever the rule-goal graph of the program has no cycle with an odd number of negative edges. We show that, in some well-defined sense, this is the most general fixpoint semantics of negation possible; in particular, we show that if a cycle with an odd number of negative edges is present, then the logic program is not structurally total, that is, it has an alphabetic variant which has no fixpoint semantics whatsoever. Determining whether a program is total is undecidable.