Apt, Blair & Walker (1988) -- Towards a Theory of Declarative Knowledge

The paper

K. R. Apt, H. A. Blair, and A. Walker, “Towards a Theory of Declarative Knowledge,” Foundations of Deductive Databases and Logic Programming, pp. 89–148, 1988.

doi:10.1016/b978-0-934613-40-8.50006-3 · read the paper

A summary of the paper and how gen uses it.

Paper Summary

Negation is the point where logic programming stops being declarative. A positive program has an unambiguous meaning — its least Herbrand model, equivalently the least fixed point of the van Emden-Kowalski immediate-consequence operator T_P. Add negation and both halves collapse at once: T_P becomes nonmonotonic and may have no fixed point at all, and the program may have several minimal models with no principled reason to prefer one. The program p <- ~q, q <- ~p has two minimal models and nothing in the syntax distinguishes them. Apt, Blair & Walker identify a syntactic restriction that recovers a single canonical meaning, and then spend the bulk of the chapter proving that the meaning so obtained is not an artifact of how the restriction was applied.

The restriction is stratification, and the authors motivate it before formalizing it (p. 95): “When using negation we should refer to an already known relation. More specifically, first some relations should be defined (perhaps recursively) in terms of themselves without the use of negation. Next, some new relations can be defined in terms of themselves without the use of negation and in terms of the previous ones, possibly with the use of negation. This process can be iterated.” The formal content is DEFINITION 3 (p. 96), and it is stated as a partition of the program, not as a level mapping. A program P is stratified if there is a partition P = P_1 u ... u P_n such that for each i: if a relation symbol occurs positively in a clause in P_i then its definition is contained in the union of P_j for j <= i; if it occurs negatively then its definition is contained in the union of P_j for j < i. The two conditions are deliberately asymmetric. The authors gloss it themselves in the following sentence: “each stratum defines new relations in terms of itself only positively and in terms of the relations from the previous strata, possibly negatively.” Positive recursion within a stratum is exactly what stratification is designed to permit; it is negation that must reach strictly downward. Note also what gets stratified: DEFINITION 2 (p. 96) fixes “the definition of a relation symbol r” as the set of clauses whose head has relation symbol r, and DEFINITION 3’s conditions range over relation symbols. Stratification here is over predicate symbols, not over ground atoms.

The definition is existential — “there is a partition” — so it is not obviously decidable, and DEFINITION 4 (p. 97) supplies the decision procedure. The dependency graph of P has the relation symbols as nodes and an edge (p,q) whenever some clause has p in the head and q in a body literal. Edges carry signs: (p,q) is positive [negative] if some clause has q in a positive [negative] body literal, and the authors are explicit that a single edge may be both positive and negative. LEMMA 1 (pp. 97-98) then gives the characterization the literature usually quotes: “A program P is stratified iff in its dependency graph there are no cycles containing a negative edge.” The forward direction restates DEFINITION 3 as a level mapping over the graph, and does so in words, which makes it the cleanest statement of the asymmetry in the chapter: “If (p,q) is a positive edge in the dependency graph of P then the level assigned to q is smaller than or equal to that assigned to p, and if (p,q) is a negative edge, then the level assigned to q is strictly smaller than that assigned to p.” The converse is the argument of most interest to a graph framework: decompose the dependency graph into maximal strongly connected components; observe that the induced “there is an edge from component G to component H” relation on the condensation is finite and acyclic, hence well founded; number the components consistently with it; and take P_i to be the definitions of all relations in component i. Positive edges stay within or descend a component, negative edges must descend because no cycle carries one. The SCC condensation is not incidental — it constructs a canonical stratification, and it is what makes stratification checkable in linear time on the dependency graph rather than searched for among partitions.

Having restricted the syntax, the authors need a semantics, and here the chapter does something more general than logic programming. Because T_P is nonmonotonic under negation, Knaster-Tarski does not apply and the usual least-fixed-point construction is unavailable. Sections “Fixed Points” and “Iteration Versus Simultaneity” (pp. 99-107) therefore develop a fixed-point theory for sequences of possibly nonmonotonic operators, independent of logic programming. An operator T is finitary if it commutes appropriately with unions of increasing chains, and growing if it behaves monotonically on arguments sandwiched between an interpretation and its own upward iteration (DEFINITIONS 5-6, pp. 101-102). For a finite sequence T_1,...,T_n the chapter defines the staged iteration N_0 = I, N_i = T_i^w(N_{i-1}), written iter(T_1,...,T_n,I). Two structural properties of the sequence carry the results: local (later operators do not disturb the part of the space earlier ones have settled) and raising. COROLLARY 2 and THEOREM 1 (p. 104) show that for a local sequence of finitary growing operators the staged iteration is a fixed point of the union of the operators and is minimal above I among interpretations closed under them; THEOREM 2 (p. 106) shows that for a local and raising sequence the staged iteration coincides with the simultaneous one, iter(T_1,...,T_n,I) = (U T_i)^w(I). DEFINITION 9 (p. 106) introduces independence of two operators, and THEOREM 3 (p. 107) proves that independent operators commute: T_1^w(T_2^w(I)) = T_2^w(T_1^w(I)). That commutation theorem is the machinery behind the chapter’s central uniqueness result.

The semantics itself is then a bottom-up iteration over the strata (p. 108). Given P = P_1 u ... u P_n, put M_1 = T_{P_1}^w(phi), M_2 = T_{P_2}^w(M_1), …, M_n = T_{P_n}^w(M_{n-1}), and let M_P = M_n. Each stratum is saturated to its own fixed point before the next one begins, so by the time a negative literal in stratum i is evaluated, the relation it negates has already been decided and is never revised — negation is evaluated against a completed lower context, never against a partial one. The authors call M_P the standard model. Connecting it to the abstract theory requires DEFINITION 10 (p. 109): a program is semi-positive if none of its negated relation symbols occurs in a clause head (Neg_P n Def_P = phi), which is precisely the property each individual stratum has. THEOREM 4 (p. 108) shows T_P is finitary for every program; THEOREM 5 (p. 109) shows T_P is growing when P is semi-positive; THEOREM 6 (p. 110) shows that a sequence of strata defining new relations yields a local sequence of operators. The abstract results then apply, giving T_P(M_P) = M_P and hence THEOREM 7 (p. 111): M_P is a model of P and is supported (every atom in it is the head of a ground clause whose body it satisfies — so nothing is believed without a reason). THEOREM 8 (p. 112) adds that M_P is a minimal model.

The result that justifies the whole construction is THEOREM 11 (p. 116): M_P is independent of the stratification of P. A program generally admits many stratifications, and if different ones produced different models the “standard” model would be a property of the analyst’s choice rather than of the program. The proof refines the program into clusters (DEFINITION 12, p. 112 — essentially the SCC-derived finest strata), shows via LEMMA 11 that every stratification is a union of clusters, proves that operators of unrelated clusters are independent (THEOREM 9, p. 115) and that a stratum’s cluster sequence is raising (THEOREM 10, p. 115), and then uses the commutation theorem to permute any two stratifications into each other without changing the iteration’s result. The SCC decomposition thus does double duty: it decides stratifiability, and it supplies the canonical refinement through which all stratifications are shown equivalent.

The chapter then removes the remaining operational flavour. “An Alternative Characterization of M_P” (pp. 117-118) observes that defining M_P by iteration “is somewhat operational in the sense that it is defined in terms of the iterations of the operators T_P”, and gives an equivalent definition that refers to no computation mechanism at all: M(P_1) is the intersection of all supported models of P_1, and M(P_i) is the intersection of all supported models of P_i that agree with M(P_{i-1}) on the Herbrand base of the lower strata. THEOREM 12 proves M_P = M(P_n). The declarative reading is therefore: at each stratum take the least supported model consistent with everything already fixed below.

The remainder builds the procedural half and reconciles it with the classical literature. A top-down “elementary interpreter” I_P is defined over implication trees with a loop-trapping condition on negative leaves (pp. 122-138); THEOREM 13 (p. 129) proves it computes exactly M_P — exists T [I_P(A,T,phi)] iff A is in M_P, and I_P(~A,~A,phi) iff A is not — so the model-theoretic and back-chaining readings agree. THEOREM 14 (p. 134) proves the recursive definition of I_P is satisfiable at all (it is well founded only because P is stratified), and COROLLARY 4 (p. 136) re-derives stratification-independence from the interpreter side. For function-symbol-free programs the Herbrand base is finite and I_P is an effective, terminating procedure. Finally, THEOREM 15 (p. 139) restates Clark’s completion model-theoretically (I is a model of comp(P) iff T_P(I) = I) and THEOREM 16 (p. 139) concludes that comp(P) is consistent for every stratified program — a genuinely useful corollary, since consistency of the completion is the standard soundness precondition for SLDNF and can fail for unrestricted programs. The authors are careful to add that the two views do not coincide: for p <- p, q <- ~p, comp(P) leaves p undetermined while M_P decides it false.

A terminology caution for anyone citing this chapter, because two terms routinely attributed to it are not its own and the chapter says so. First, ABW stratify relation (predicate) symbols via a partition of the program; the ground-atom generalization is not theirs. Their “Bibliographic Remarks” (p. 144) state it plainly: “The notion of stratified programs has been further generalized to locally stratified programs in Przymusinski [1988].” The phrase “local stratification” does not occur in the chapter, and “locally stratified” occurs exactly once — in that sentence, crediting someone else. Second, the canonical model here is the standard model M_P, not the “perfect model”; “perfect model” also appears exactly once, on the same page, likewise credited to Przymusinski. Both cited works are Przymusinski’s chapter in the same Minker volume, pp. 193-216. The chapter also positions its own notion against Clark’s: stratification generalizes Clark’s 1978 hierarchical constraint, which assigns relations to levels but “rules out recursive definitions” — removing negation collapses stratified programs to positive ones, removing recursion collapses them to hierarchically constrained ones.

Key Concepts

• Stratification is a partition of the program, and the two conditions are asymmetric. DEFINITION 3 (p. 96): positive occurrences resolve within U_{j<=i} P_j, negative occurrences within U_{j<i} P_j. Same-stratum positive dependency is permitted, which is what allows recursion to survive the restriction. Only negation is forced strictly downward. A guard that applies the strict rule to every read implements Clark’s hierarchical constraint, which ABW distinguish (p. 144) as the recursion-free special case.

• What gets stratified is a predicate symbol. DEFINITION 2 (p. 96) defines “the definition of a relation symbol”, and DEFINITION 3 quantifies over relation symbols. The index of the discipline is therefore the relation kind. The ground-atom refinement is Przymusinski’s separate notion (p. 144).

• Sign-labelled dependency graph with a negative-cycle criterion. DEFINITION 4 (p. 97) and LEMMA 1 (pp. 97-98): stratifiability is decidable as “no cycle contains a negative edge”. A single edge may be both positive and negative, because the signs label the edge.

• SCC condensation as the canonical stratification. LEMMA 1’s converse decomposes the dependency graph into maximal strongly connected components and numbers the condensation, which is finite and acyclic hence well founded. This yields the finest stratification (“clusters”, DEFINITION 12, p. 112) through which all others factor.

• Staged iteration iter over a sequence of nonmonotonic operators. N_0 = I, N_i = T_i^w(N_{i-1}) (p. 104). Developed abstractly for finitary/growing operators over local/raising sequences, then instantiated at T_{P_i}. Substitutes for Knaster-Tarski, which is unavailable because T_P is nonmonotonic under negation.

• Saturate each stratum before starting the next. M_i = T_{P_i}^w(M_{i-1}), M_P = M_n (p. 108). Negation in stratum i is evaluated against a stratum that is already at fixed point and will not be revised. The operational content of the discipline is to read only what has finished.

• Independence implies commutation. DEFINITION 9 (p. 106) and THEOREM 3 (p. 107): independent operators commute under upward iteration. The lever for the uniqueness result.

• M_P is a minimal supported model, and is independent of the stratification chosen. THEOREMS 7, 8, 11 (pp. 111, 112, 116). Supportedness is the “no belief without a reason” condition; stratification-independence is what makes M_P a property of the program rather than of the analyst.

• A computation-free characterization. THEOREM 12 (pp. 117-118): M_P = M(P_n) where each M(P_i) is the intersection of supported models of P_i agreeing with M(P_{i-1}) below. The declarative reading of the same object.

• Consistency of Clark’s completion for stratified programs. THEOREMS 15-16 (p. 139). Stratification buys a standard soundness precondition. The completion and M_P differ: comp(P) may leave undetermined what M_P decides.

How gen uses this

gen-scope: stratify

gen-scope’s stratify is gen’s one stratification driver. An instance supplies a schedule of strata, a way to place each item in a stratum and a function that runs one stratum. The driver returns every stratum’s settled output in schedule order. It cites ABW’s construction M_i = T_{P_i}^w(M_{i-1}) (p. 108) for the one guarantee it gives: when a stratum runs, every earlier stratum has reached its fixed point and its output is closed. This is why aggregation needs stratification. A fold over a set that is still growing answers about a prefix.

stratify imposes no visibility rule. DEFINITION 3 forces only negative occurrences strictly downward, and lets a positive occurrence resolve within the same stratum. Strictly-below indexing is a sufficient condition for a negated read to be sound, and a driver that enforced it on every read would reject programs the definition admits.

The minting pass in gen-scope (mintStrata) is an instance. Each pass is a stratum, and a pass resolves identifiers only against what strictly earlier passes settled. So a cycle among minted nodes cannot be written.

gen-scope and gen-program: sign-labelled programs and the well-founded model

gen-scope’s mkProgram keeps the dependency graph of a rule program sign-labelled, as DEFINITION 4 does. The labels decide which semantics applies. ABW give a meaning to a program whose cycles are all positive, and give nothing to a cycle through a negative edge. gen-scope’s wellFoundedModel computes Van Gelder’s well-founded model, which assigns such a cycle the value undefined and agrees with the stratified model on every program ABW cover. gen-program builds rule programs that contain negation from a framework’s declarations and solves them this way.

gen-graph: the graph half of LEMMA 1

LEMMA 1 states that a program is stratified exactly when no cycle in its dependency graph contains a negative edge, and its proof decomposes the graph into strongly connected components. gen-graph’s cyclicEdgesWhere implements that proof method: it partitions the graph into strongly connected components, then reports the labelled edges whose endpoints share a component. Which labels count as negative is the caller’s choice, since gen-graph has no notion of programs or clauses.

gen-view: DEFINITION 3 clause 2 by structure

gen-view’s ordering takes a materialised view as its input, never the raw labelled edges, so no query’s answer can decide whether an edge exists. A cycle of the form includes → ¬holds → includes therefore cannot be written, which gives DEFINITION 3’s clause 2 by the shape of the input type instead of a check at read time.

Appendix: Follow-up Work

Unexploited Ideas

Clusters as the canonical stratification (DEFINITION 12, p. 112). The SCC condensation yields the finest admissible stratification. A framework that assigns strata by declaration could derive them instead: compute the finest layering the relation graph admits, and treat a declared stratum as an assertion checked against it.

Stratification-independence as a testable property (THEOREM 11, p. 116). The theorem generates tests. Evaluate under two admissible stratifications and require byte-identical output. This checks that admissible variation has no effect, which is stronger than checking that a violation throws.

The computation-free characterisation (THEOREM 12, pp. 117-118). M(P_i) is the intersection of the supported models of P_i that agree with M(P_{i-1}) below. This specifies what the output of resolution is without reference to the iteration order that produces it, which makes it a candidate oracle wherever current oracles are stated operationally.

Supportedness as a distinct invariant (THEOREM 7, p. 111). ABW separate “is a model” from “is supported”, where every true atom has a ground clause justifying it. A check that every materialised fact has a producing rule whose body held would catch facts emitted by accident.

Potential New Libraries or Features

A stratifiability decision. cyclicEdgesWhere answers the graph half of LEMMA 1. A caller that has programs could pair it with a numbering of the condensation to return either an assignment of relations to strata or the offending negative cycle, which is LEMMA 1’s proof as a function.

Stratum-consistency assertion for negation sites. For each negated relation, assert that its stratum is strictly below the negating rule’s, computed from the derived stratification, and permit same-stratum positive reads explicitly.

Research Directions

Local stratification, adopted deliberately. Przymusinski’s ground-atom refinement (same Minker volume, pp. 193-216) admits programs whose predicate-level dependency graph has a negative cycle while their ground instantiation has none. Parametric aspects make the predicate-level graph coarser than the instance-level one, so some programs rejected at kind level are sound at instance level. That is a reason to want the local notion, adopted with Przymusinski cited.

Whether each stratum’s operator is growing. THEOREM 5 (p. 109) requires semi-positivity per stratum (Neg_P ∩ Def_P = ∅: no negated relation symbol appears in a head within the stratum). The chapter’s guarantees rest on it. A rule that both negates and produces the same relation kind violates it.

Completion consistency (THEOREMS 15-16, p. 139). ABW obtain consistency of Clark’s completion as a corollary of stratification. The analogue for a rule program is that the “if and only if” reading of its rules is satisfiable, so no query can be answered both ways.

Effectiveness without function symbols (pp. 136-137). For function-symbol-free programs the Herbrand base is finite and the interpreter terminates, with worst-case cost no worse than depth-first search. A configuration’s entity graph is finite, which is the same situation. The observation bounds what resolution can cost and gives a termination argument.