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

This page is our reading of it, not a substitute for 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 — that is the whole point, since it is what allows recursion to survive the restriction. Only negation is forced strictly downward. A guard that applies the strict rule to every read is not implementing this definition; it is implementing Clark’s hierarchical constraint, which ABW explicitly distinguish (p. 144) as the recursion-free special case.

• What gets stratified is a predicate symbol, not a ground atom. 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, not the individual fact. 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”. Note the modelling detail that a single edge may be simultaneously positive and negative — signs label the edge, not a pair of parallel edges.

• 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. This is the operational content of the discipline: not “read less”, but “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 are not the same view: comp(P) may leave undetermined what M_P decides.

Implementation Mapping

Current Usage in Gen Ecosystem

den-hoag (MAJOR)

den-hoag cites this chapter as the soundness law governing non-monotone reads in the kernel. The citation sites are lib/stratum-scope.nix, lib/concern-derived.nix, lib/attributes/claim-accessor.nix, lib/attributes/resolution-relations.nix, and the CI witnesses ci/tests/negation-gate.nix, ci/tests/claim-negation.nix, ci/tests/claim-provide-witness.nix.

Stratum-scoped reads (L1). lib/stratum-scope.nix splits the capability boundary into a silent source (edgesBelowStratum, where an out-of-scope edge is simply absent from the query surface) and a loud projection (ceilingGate, where reading a relation kind at or above the ceiling is replaced by a named throw). The correspondence to DEFINITION 3 is direct: a reader’s ceiling is its stratum index i, and the question of which U_{j..i} P_j an edge must fall within is exactly the question the two conditions answer differently for positive and negative occurrences.

Stratified claim negation (L4). lib/concern-derived.nix rejects a negates entry that does not name a relation, on the grounds that an unrestricted negation would be unsound. That is the correct shape of the ABW restriction — negation is admitted only where the negated thing is a relation whose definition can be located in a stratum.

Discrepancies against the primary text, recorded here because they are what the archive is for. Two substantive errors, plus one citation-hygiene ambiguity:

1. The comparison operator. lib/stratum-scope.nix describes the discipline as “stratum n may only see facts at strata STRICTLY BELOW n”. DEFINITION 3 condition 1 permits a positive occurrence to resolve at j <= i. Applying the strict rule uniformly is strictly stronger than ABW and forbids same-stratum positive recursion, which is the case stratification exists to allow. REFERENCE.md line 959 states it correctly (“same-stratum positive reads are permitted”); the two statements are not compatible and the archive sides with 959.

2. What is indexed. gen-specs/den-hoag/REFERENCE.md line 83 calls this “the local-stratification discipline of Apt, Blair & Walker (1988)”. Local stratification is Przymusinski’s and ranges over ground atoms; ABW’s ranges over relation symbols (p. 144, and DEFINITIONS 2-3). This is not a naming quibble — it determines whether a guard is keyed on a relation kind or on an individual fact, and ABW’s notion is the kind-indexed one. The same line’s gloss “a predicate may depend only on strictly-lower strata” repeats error (1).

3. Citation hygiene — NOT a bad citation. ABW’s chapter has no numbered sections; it uses named headers (“Preliminaries”, “Syntax”, “Stratified Programs”, “Fixed Points”, “Iteration Versus Simultaneity”, “Model Theory of Stratified Programs”, “An Alternative Characterization of M_P”, “An Elementary Interpreter”, “Existence of the Interpreter”, “Other Views of Negation and Stratified Programs”, “Bibliographic Remarks”). The citable locator for the definition is therefore “Stratified Programs”, DEFINITION 3, p. 96, and for the asymmetry stated in words, the Lemma 1 proof, pp. 97-98.

   That fact does not imply anyone cited a nonexistent ABW section. §2.3 is den-hoag’s own spec section — the capability-scope section — used correctly and consistently at ~69 sites across lib/ and ci/ (e.g. lib/concern-productions.nix:121 “not in the compiled strata order (§2.3)”; lib/compat/deliver.nix:3 “the §2.3 error cases”). The narrow defect is the two sites where the paper’s name and our section number sit adjacent, so the number can be misread as the paper’s:

   • lib/concern-derived.nix:55 — “(unsound, Apt-Blair-Walker §2.3)” — genuinely ambiguous.
   • ci/tests/negation-gate.nix:3 — “(Apt-Blair-Walker stratified negation, §2.3)” — milder; parses as “ABW stratified negation, [our] §2.3”.

   Both want a separator, not a rewrite.

Relevance to Den v2 HOAG Pipeline

The pipeline’s two-layer fixpoint is a staged iteration in exactly ABW’s sense: forward expand, neededBy scan, repeat until stable. Where den-hoag admits a non-monotone step — a negated claim, an absence check, a drop — ABW’s result says what makes it sound, and the condition is about completeness of the lower context, not about restricted visibility per se. A negative read is safe when the relation it negates has reached its fixed point; it is unsound when that relation could still grow. This reframes the guard: the invariant to enforce is “the negated relation’s stratum has been saturated”, and strictly-below indexing is the conservative way to guarantee that, not the property itself.

The scope graph is den’s dependency graph, and LEMMA 1 transfers directly: the check for admissibility of a negation set is “no cycle in the relation-dependency graph contains a negative edge”, decidable by SCC condensation rather than by search over candidate stratifications. gen-graph already has the fixpoint and reachability machinery this needs.

THEOREM 11 is the result with the most architectural weight and the least current uptake. It says the canonical model does not depend on which admissible stratification was chosen. The den-hoag analogue is that resolution output must not depend on the particular phase assignment the scheduler picked — a property currently assumed rather than witnessed. The chapter also supplies the proof technique: refine to clusters (SCCs), show every stratification is a union of clusters, show unrelated clusters commute.

Appendix: Follow-up Work

Unexploited Ideas

The negative-cycle criterion as a static admissibility check (LEMMA 1, pp. 97-98). den-hoag currently enforces stratification by construction — the ceiling is declared and the gate throws at read time. ABW’s criterion permits the dual: accept a declared relation graph, sign its edges, and decide whether a stratification exists at all. A program with a negation cycle is rejected at definition time with the cycle exhibited, rather than at read time with a ceiling violation. This is a better error and it is a graph query den already knows how to run.

Clusters as the canonical stratification (DEFINITION 12, p. 112). The SCC condensation yields the finest admissible stratification. den-hoag assigns strata by declaration. Deriving them instead would remove a class of hand-tuning: the framework computes the finest layering the relation graph admits, and a user-declared ceiling becomes an assertion to check against it rather than the source of truth.

Stratification-independence as a testable property (THEOREM 11, p. 116). The theorem is a witness generator: evaluate under two different admissible stratifications and require byte-identical output. This is a stronger CI property than the current negation-gate witnesses, which check that a violation throws, not that admissible variation is inert.

The computation-free characterization (THEOREM 12, pp. 117-118). M(P_i) = intersection of supported models of P_i agreeing with M(P_{i-1}) below. A specification of what resolution output is, stated without reference to the iteration order that produces it — useful as an oracle in exactly the places where the current parity oracles are phrased operationally.

Supportedness as a distinct invariant (THEOREM 7, p. 111). ABW separate “is a model” from “is supported” (every atom has a ground clause justifying it). den-hoag has no corresponding check that every materialized fact has a producing rule whose body held. Unsupported facts are the shape of a bug where something is emitted by accident rather than derived.

Potential New Libraries or Features

Signed dependency graph + stratifiability decision, in gen-graph. mkSignedGraph { nodes; edges = [{ from; to; sign; }]; } with stratify returning either an assignment of nodes to strata or the offending negative cycle. Implements LEMMA 1’s SCC-condensation proof directly. gen-graph already has SCC and fixpoint primitives; this is a labelling layer plus the numbering argument.

Staged-iteration combinator. iter over a sequence of operators with saturation at each stage (N_i = T_i^w(N_{i-1}), p. 104), plus the finitary/growing preconditions as documented obligations. den-hoag’s phase loop is an instance; naming the abstraction makes the preconditions checkable rather than implicit.

Stratum-consistency assertion for negation sites. For each declared negates, assert that the negated relation’s stratum is strictly below the negating clause’s, computed from the derived stratification rather than the declared ceiling — and permit same-stratum positive reads explicitly, which is where the current strict-everywhere guard diverges from the paper.

Research Directions

Local stratification, deliberately rather than by accident. Przymusinski’s ground-atom refinement (same Minker volume, pp. 193-216) admits programs whose predicate-level dependency graph has a negative cycle but whose ground instantiation does not. den-hoag’s aspects are parametric, so the predicate-level graph is coarser than the instance-level one and there will be real cases rejected at kind level that are sound at instance level. That is a genuine reason to want the local notion — but it should be adopted on purpose, with Przymusinski cited, not inherited through a mis-citation of ABW.

Whether den’s fixpoint operators are actually “growing”. THEOREM 5 (p. 109) requires semi-positivity per stratum (Neg_P n Def_P = phi: no negated relation symbol appears in a head within the stratum). The chapter’s guarantees rest on this. Whether den-hoag’s per-phase operators satisfy the analogous condition is unverified, and it is the precondition most likely to be silently violated by a rule that both negates and produces the same relation kind.

Completion consistency as a den-level property (THEOREMS 15-16, p. 139). ABW get consistency of Clark’s completion as a corollary of stratification. The den analogue — that the “if and only if” reading of the rule set is satisfiable, so no query can be answered both ways — is a soundness property the framework currently has no statement of.

Effectiveness without function symbols (pp. 136-137). ABW note that for function-symbol-free programs the Herbrand base is finite and the interpreter terminates, with worst-case complexity no worse than ordinary depth-first search. den’s entity graph is finite by construction, which is the same situation; the observation bounds what the resolution loop can cost and may be worth stating as a termination argument rather than relying on an iteration cap.