vaelii.impl.special — com.vaelii/vaelii 0.8.0

The special-predicate dispatch table: what each functor the engine interprets means to the derived state around the store, stated once, with both halves of every meaning side by side.

A special predicate needs behaviour in four places — reflecting a stored sentex into the caches, the removal mirror, recover's cache-only replay, and wff's per-functor well-formedness check — and the compiler cross-checks none of them, so the enumeration lives once here: entries maps each functor to its arms,

:integrate (fn [kb sentex handle]) reflect a newly stored sentex into the caches :disintegrate (fn [kb sentex]) the mirror, reference-counted on (:id sentex) :rebuild (fn [tax sentex]) recover's cache-only replay — no re-check posting, no migration, no universal lifting, because the store already holds what those side effects produced :wff (fn [tax sentence]) structural well-formedness (vaelii.impl.wff keeps the check fns; the table points at them) :derived? bool the :integrate arm also runs on the derivation path (see integrate-transitive)

and check-entries refuses an asymmetric entry at namespace load, so an add-side arm without its removal and rebuild halves is a build failure rather than a cache that drifts on the first retraction or restart.

Because the arms are where a special predicate's whole behaviour lives, the machinery those behaviours need lives here too: the exception re-check queue the taxonomy arms post to, the universal-predicate lifting, and the equality migration. Third layer of the engine stack (kb <- checks <- special <- integrate <- chain <- settle): everything here reads kb and checks, and the store-mutation choke points in vaelii.impl.integrate sit directly above.

check-entries clj

(check-entries entries)

Refuse an ill-formed table at namespace load, so add/remove symmetry is a structural property rather than a review item.

Two shapes are refused. An entry with some of the cache arms — an :integrate whose :disintegrate or :rebuild is missing (or any other partial triple) is exactly the mirrored-cond drift this table exists to end: the cache would fill on assert and leak on retract, or come back wrong after recover. And an entry with no arm at all, which is a typo. Returns entries unchanged so it can wrap the def.

deduce-arg-types clj

(deduce-arg-types kb entailments handle context)

Materialize the entailments checks/constraint-entailments drew over a sentence stored at handle in context — {:new [handles] :violations [v]}.

Called from both stores of new content — assert and forward chaining's place-conclusion — because what a declaration says about an argument is a claim about the predicate, not about how a particular sentence arrived. Entailing only what a caller asserted would make belief depend on arrival order, exactly as lifting only asserted content would.

deduce-lifts clj

(deduce-lifts kb sentence handle context)

Deduce sentence (stored at handle in context) into CxUniverse if its predicate is decontextualized — {:new [handles] :violations [v]}, nil when the predicate carries no declaration.

Called from both stores of new content — assert and forward chaining's place-conclusion — because a decontextualized predicate is a claim about the predicate, not about how a particular sentence arrived. Lifting only what a caller asserted would make belief depend on arrival order: declare-then-derive would leave the conclusion unlifted while derive-then-declare lifted it through lift-existing, and the two orders are the same knowledge.

The gate is a single in-memory cache read, because every assert and every placed rule conclusion pays it to find out there is nothing to do.

derive-functional-equalities clj

(derive-functional-equalities kb sentence context handle)

(functional P) plus two symbol values for the same first argument derives (equals V1 V2) rather than throwing (docs/equality.md).

equals specifically, not sameAs: the value of a functional role need not be an individual — a birthplace, a measurement — and OWL's sameAs is individuals-only. equals is the one of the three that always type-checks here.

Making it a real justification is what makes it safe. The risk of auto-inference is that one wrong functional declaration silently merges two real individuals across the whole KB — so the merge is justified by [both facts, the declaration], why names exactly which declaration and which two facts caused it, and retracting any one of them runs the ordinary sweep and un-merges. An opaque merge would be dangerous; an inspectable, reversible one is knowledge.

Gated on the taxonomy's :functional mark before it reads the store. This runs on every asserted fact and the store read is a sentexes-matching over an unscoped context, so on a KB that declares nothing functional — the common case, and every bulk load — the mark is what stands between an assert and an index query per fact to learn what an O(1) set lookup answers. The mark is maintained by the same table entry that stores the declaration and replayed by recover, so it holds exactly when the query finds something; the unscoped arity is what keeps that equivalence, since the query under it names no context either. The handle comes from the store, because a justification needs the declaring sentex itself, and only the true branch pays for it.

One justification per declaring sentex, not one off an arbitrary declaration. A KB may state (functional P) in two contexts, which is two sentexes and two handles and is refused by nothing; taking first of them put an assertion-ordered handle into the justification's antecedents, so retracting that declaration withdrew the merge while the other still stood — and which of the two it was depended on the order they arrived in. tax/prop-supporters is the whole set, defeated members included (its docstring says why: a derivation revives by itself when its supporter does), and unfiltered by what context sees — the whole set on the visibility axis too, and deliberately: filtering to visible supporters would make the surviving merge depend on which declaration was retracted first, and a-merge-rests-on-every-functional-declaration-not-on-one-of-them pins both directions on independent predicates so no arbitrary choice can pass as this. The equality takes a justification from each — the shape deduce-lift already uses for the same reason, so retracting one of two declarations leaves the merge standing on the other. Sorted only to make each antecedent list stable to read; the set of justifications is what carries the meaning, and a set has no order to depend on.

A mark on a super-predicate counts, and brings its genl edges with it. (functional parentOf) says a child has one mother however the tuple is spelled, so two fatherOf fillers merge under it (tax/props-over) — and the merge then rests on the subsumption as much as on the declaration, so checks/edge-support puts the edge handles into the same antecedent list. Without them, retracting the edge would leave two names merged on a declaration that no longer reaches either of them.

Both spellings' edges, and only the mark that convicted. Two things follow from the clash being a pair, and the earlier reading of it got both wrong.

The pair has two sides and each reached the marked predicate its own way. Naming the arriving sentence's descent and not the stored filler's left the merge standing after the filler's own genl edge was retracted — at which point that fact is not a tuple of the marked predicate at all, and nothing licenses the merge. That is verbatim the failure edge-support exists to prevent, avoided on one side and not the other, so both descents are named.

And functional-clashes reports which mark convicted, as the via of its triple, computed for exactly this. Justifying the merge with every marked predicate above the functor instead let a mark that never covered the pair hold it up: with (functional guardianOf) over a hierarchy where only one of the two spellings is a guardianOf, the merge survived retracting the only declaration that ever reached both. One clash, one convicting mark, its declaring sentexes — which is still every sentex of that mark, since a predicate declared functional in two contexts is two handles and the merge may not depend on which arrived first.

Scoped to the reader, matching the clash it is drawn from: props-over is read through functional-clashes' own scoped call and the descent through context, so a mark or an edge in a sibling context cannot support a merge that context cannot see. prop-supporters stays unfiltered, deliberately and for the reason its own docstring gives.

The two descents are a set, not a concatenation. They overlap whenever the two sides share any of the path up to the mark, which is the ordinary case rather than the odd one: two fatherOf fillers under (functional parentOf) descend the same edge, and a dadOf filler beside a fatherOf one shares the fatherOf → parentOf hop. Appending them left the shared handles twice over in the record derive-equality stores, so core/why's :because, why-not's :missing and preview's :antecedents each listed one edge two or three times. Belief never moved — valid? is an every? and has-justification? keys on a set — which is why it reads as cosmetic and is not: an antecedent list is the explanation a caller is given, and one that counts a single edge twice describes a justification the KB does not hold. distinct rather than a set literal, so the list keeps the order the descent produced and stays stable to read.

derived-sentex-added clj

(derived-sentex-added kb sentex handle)

The derivation-path add choke point: everything that must happen because a derived sentex landed in the store — the closure-reaching integration above, and the exception re-check post, since a derived fact is a re-check trigger like an asserted one (an exception may be stated over a predicate that only ever arrives by inference — the cried-wolf case, where liar is concluded by another rule).

Lives here rather than beside sentex-added in vaelii.impl.integrate because the equality arms are themselves derivation sites: a migrated twin and a functional-inferred equals are derived sentexes, and hand-rolling this pair at those sites is exactly the copy-paste the choke points exist to end. Callers: forward chaining's place-conclusion, migrate-sentex, derive-equality.

disintegrate-sentex! clj

(disintegrate-sentex! kb sentex)

The mirror walk: reverse a departing sentex's cache effects through the :disintegrate column, or the matching structural arm. Every cache below is reference-counted on the departing sentex's id, so an entry survives while another sentex still asserts the same claim.

entail-existing clj

(entail-existing kb sentence dh)

When an (argIsa P n T) / (argGenl P n T) / (interArgIsa P n T m U) declaration arrives, draw what it now says about the (P …) sentexes already stored — so a declaration arriving after the facts reaches them exactly as one arriving before reaches the facts that follow. Same {:new :violations} result, so the types it mints are chaining seeds like any other new content. nil when sentence is not an argument constraint.

Two of interArgIsa's three arrival orders are covered here and at the door; the third — the trigger's type arriving after both the fact and the declaration — is the family's documented open-world non-reach (docs/taxonomy.md, "What each constraint does in each arrival order"), and argIsa has it too from the other side.

Sweeps what is stored, not what is believed, for lift-existing's reason: a type minted off a defeated fact is justified by that fact and so is defeated too — the JTMS already says what a disbelieved antecedent means — whereas skipping it would leave the type missing when the fact revives, which is belief depending on the order the defeat and the declaration arrived in.

The extent is read off the functor roots of P's whole spec subtree, which is the precise answer to "every stored tuple this declaration constrains": a declaration on P binds every predicate beneath it (res/constraining-predicates), so an extent read off P's own root alone would mint over (parentOf …) and not over (fatherOf …) — a type the same three sentences produce in one arrival order and not the other. subtree-sentexes reads it, and snapshots it before the first mint.

entail-under-edge clj

(entail-under-edge kb sentence)

When a (genl sub super) edge arrives, draw what the declarations on super now say about the (sub …) sentexes already stored — the third arrival order of the same three ingredients, and there for the reason subsumption-seeds beside it is.

A constraint descends the predicate hierarchy, so the fact, the declaration and the edge are all ingredients of one entailment. deduce-arg-types covers the fact arriving last and entail-existing the declaration arriving last; without this, the edge arriving last mints nothing and the same three sentences leave the KB holding a type in two orders out of three. nil when sentence is not a genl edge.

The whole spec subtree of sub, because subsumption is transitive: an edge at the top of a predicate hierarchy brings every predicate below it under the declarations above it. Each stored sentex is put back through checks/constraint-entailments in its own context — the same function the other two directions ask, so the three cannot disagree — and the mints deduplicate on content, so a fact whose type was already entailed by a route that survives contributes a justification and no second record.

Two gates in front of the subtree, because this arm fires on a genl edge — the commonest thing an ontology says, where the other two fire on a declaration. Off unless *assertive-arg-types?*, since with the entailment off there is nothing to mint and the edge's other consequences are subsumption-seeds'; and off unless the KB stores an argument constraint at all, which is one index count per kind and is what keeps an edge under a predicate nobody constrained from reading a subtree's extent to discover there was nothing to draw. The extent itself is subtree-sentexes, filtered by cardinality for the same reason one step further in.

entries clj

The special-predicate dispatch table, as an ordered vector of [functor spec] pairs — ordered because rebuild-taxonomy replays it top to bottom and a rebuild arm may read what an earlier one wrote (metatype membership reads the marks; nothing else is order-sensitive today, and keeping the assert path's traditional order costs nothing). table below is the lookup view.

This vector is the functor enumeration: integrate, disintegrate, rebuild and wff all walk it, so a predicate added here is added to all four at once and check-entries refuses it half-done.

equate-existing clj

(equate-existing kb sentence)

When a (functional P) declaration arrives, derive the equalities P's already stored facts license — the other direction of derive-functional-equalities, which is a fact meeting the declaration. nil when sentence declares nothing functional.

A declaration has to reach the facts already stored exactly as it reaches the facts that follow, which is the rule entail-existing states for the argument constraints and holds here for the same reason: whether two spellings denote one woman is a question about the KB's content, and an answer that depended on whether the schema or the facts were loaded first would be an answer about the file. Written the ordinary way — declaration first, then the facts — this finds an empty extent and costs one functor-root read.

Each fact is handed to derive-functional-equalities, which asks the same question from the other side, so the two directions cannot drift about what a functional slot licenses or what justifies the merge: the equality names both facts and this declaration whichever way round it was reached, and retracting any of the three un-merges. Re-deriving is idempotent — same-class? skips a pair the closure already holds and has-justification? skips an argument it already has — so a slot filled by three values collapses to one class rather than to the first pair walked.

Sweeps what is stored rather than what is believed, for entail-existing's reason: an equality derived off a defeated fact rests on that fact and is defeated with it, where skipping it would leave the merge missing when the fact revives — belief depending on the order the defeat and the declaration arrived in. The extent is read off the functor roots of P's whole genl spec subtree, because the mark binds every predicate beneath the one it names (tax/props-over) — an extent read off P's own root alone would merge two parentOf fillers and leave two fatherOf ones apart. subtree-sentexes reads it, snapshotted before the first merge, since migration writes twins to the roots the walk is reading.

equate-under-edge clj

(equate-under-edge kb sentence)

When a (genl sub super) edge arrives, derive the equalities a (functional …) mark above super now licenses over the (sub …) facts already stored — the third arrival order of the same three ingredients, and the equality twin of entail-under-edge.

A functional mark descends the predicate hierarchy, so the two facts, the declaration and the edge are all ingredients of one merge. derive-functional-equalities covers the fact arriving last and equate-existing the declaration arriving last; without this, the edge arriving last merges nothing and whether two names denote one woman would depend on which of the three was written first. nil when sentence is not a genl edge.

The whole spec subtree of sub, because subsumption is transitive, and each stored fact is put back through derive-functional-equalities in its own context — the same function the other two directions ask, so the three cannot disagree about what a slot licenses or what justifies the merge. Re-deriving is idempotent for the reason equate-existing gives.

Free for a KB that declares nothing functional, and that is decided before the subtree is read rather than per fact inside the fold. This arm fires on a genl edge — the commonest thing an ontology says — where the other two fire on a declaration and are gated by their own trigger, so it is the one that reaches for an extent on an ordinary write. tax/props answers it in one map read; subtree-sentexes filters what survives by index cardinality.

What that does not buy is a smaller edge. subsumption-seeds walks the same spec subtree on the same edge and must — those facts really do become matchable — so a genl write is Ω(subtree extent) whatever this arm does, and the gate removes a redundant traversal rather than an order of growth. Measured on a 16x subtree the two read alike, which is why no lein perf check states this: the gate is worth having because repeated work and a false docstring are both worth removing, not because it moves a curve.

inadmissible clj

(inadmissible kb sentence context)

The violation that stops sentence from being stored in context, or nil — naming, the definitional constraints, well-formedness, and edge stratification, as one value.

This is the triple place-conclusion runs over a rule's conclusion, and it holds of any content the engine mints on its own behalf: a (T x) can clash with a disjoint membership, a (genl X T) edge can close a taxonomy cycle or a cycle through negation, and a type used at the wrong arity is not a type membership at all. Three callers ask it — the argument-type entailment below, forward chaining, and abduction, which asks it before minting a hypothesis so that a sentence no assertion could legally make is never one the search assumes.

A value, never a throw. Two of its callers run after their triggering sentex is stored (that is what gives them a handle to be justified by) and inside a fixpoint, neither of which may abort halfway; the third would rather refuse a hypothesis than fail the query that wanted it.

index-exceptWhen-meta clj

(index-exceptWhen-meta kb meta-sentex)

Register the exceptWhen meta-sentex meta-sentex in the re-check index: post the rule it names under each predicate its query mentions and into the :rules roster, and queue the rule for a blanket re-check (a fact may already have arrived that its new exception blocks).

index-rule-sentex clj

(index-rule-sentex kb handle rule-sentex)

Index a rule handle by all of its predicates — both sets are complete, so rules-by-consequent answers "what could conclude P?" for a forward-only rule too.

Only the predicates are indexed. The record is the source of truth for what a rule may do: a set/*Rule wrapper canonicalizes into the sentex (see vaelii.impl.sentex), and :direction / :defeasible are read off it by every consumer. Nothing enumerates rules by defeasibility any more — defaults fire from the same agenda as strict rules — so there is no default-rule index to maintain.

A rule is not a table entry: its trigger is the shape of the sentence (any functor can head an implication), so it is the structural arm of the integrate-sentex walk below, and this is its add half.

integrate-equality-sentex clj

(integrate-equality-sentex kb sentex handle)

The three equality relations' add arm, whichever door the sentex came through, and the whole of what one of them means to the derived state: the closure learns the edge and migration restates what the edge displaces. Returns the migration result — {:new :superseded :violations} — which is why this is a named function rather than the table's anonymous arm.

Two compound shapes are not a symbol merge and each is dispatched here (the reasons are equality-entry's, beside the removal and rebuild halves that mirror this one): a schematic (equals L R) is an oriented rewrite rule, and (rewriteOf T E) with a compound E is a NAT reify-to-term declaration the partition holds no part of.

The derivation path reaches it here too — a rule concluding one of the three merges exactly as an asserted one does — and it has to be by this function rather than by flagging the entry :derived?: integrate-transitive discards what an arm returns, and here the return value is the work, since the twins are chaining seeds and a migration a definitional check refused is a violation somebody must report.

integrate-sentex clj

(integrate-sentex kb sentex handle)

Reflect a newly stored sentex into the taxonomy / rule index / disjointness — the :integrate column of the table, walked, plus the structural arms above.

Returns {:new [handles] :superseded [[datum reason]] :violations [v]} for an equality sentex — the twins it created are chaining seeds and the violations are the caller's to report — and nil for everything else. (Only the equality arm has anything to say; every other arm mutates a cache and its return value is whatever that mutator handed back, so the result is normalized here rather than left for the caller to sort out.)

integrate-transitive clj

(integrate-transitive kb sentex handle)

The derivation-path subset of integrate-sentex: only the arms flagged :derived? — the genl / genlCx closure edges — run for a rule-derived conclusion, because the rest of integration either does not apply to a derived sentex or would re-enter assert from inside forward chaining. Without this on the derivation path, a rule concluding (genl a b) stored and believed the sentex while the taxonomy never learned the edge — and recover, which reads the store, then disagreed with the running KB about what the KB entailed. (A derived equality is not reached from here: chain/place-fact-conclusion calls integrate-equality-sentex by name, because this fn discards what an arm returns and there the return value is the work — the twins and the violations.)

integrate-twin clj

(integrate-twin kb sentex handle)

Full integration for a migrated twin — a restated declaration or fact the equality migration derives (migrate-sentex). A twin must reach the same caches an asserted declaration would, or its class-representative spelling is stored and believed while the taxonomy never learns what it declares: a merged (disjoint dog cat) twin (disjoint canine cat) must reach add-disjoint, a (transitive containedBy) twin must reach mark-prop, and a migrated rule twin must reach the rule index or it never fires. So this runs the same arms integrate-sentex does — the fuller integration derived-sentex-added (the forward-chaining conclusion path) deliberately narrows to the genl closure edges.

The equality arm is skipped: a twin is never an equality sentex (those are held back from migration, kb/rewritable-sentex?), and running migrate-class from inside a migration would recurse. Then the same re-check post every derived sentex gets — a migrated fact / declaration arriving is a trigger like an asserted one.

Migration can run inside a forward-chaining pass (derive-functional-equalities infers an equality from a derived fact), so the table/structural arms can fire mid-fixpoint. That is safe: none of them re-enter assert or chain — they add cache entries, justifications, and re-check queue items — and the common functional merge is of two individual values, whose twins are facts that match no declaration arm at all.

migrate-sentex clj

(migrate-sentex kb sentex)

Restate one stored sentex under its terms' representatives — once per reader whose election differs, not once per sentex.

Returns {:new [handles] :superseded [[datum reason]] :violations [v]}. Five things are load-bearing:

• Re-canonicalized, not substituted. The twin is built by find-or-create from the rewritten sentence, so it goes back through the sentex constructor. A merge changes what a symmetric predicate's sorted argument order should be — (siblingOf lo mid) with lo retired in favour of a term sorting after mid has to come back as (siblingOf mid hi), not (siblingOf hi mid) — and a textual substitution would quietly store one fact under two handles.
• Justified, not asserted. The twin is a derivation from [the original, the equality], one justification per incident equality edge, so each merge is an independent witness and dropping the equality collects the twin through the ordinary dependency-directed sweep. Dedup falls out: when the rewritten form is already stored, find-or-create returns that handle and it simply gains a support.
• One twin per election, placed where the reader that elected it lives. A merge applies where it is visible, so a fact above one is read by contexts that inherit different sets of edges and elect different representatives (reader-contexts-for). The fact's own context is always a reader and takes the twin that supersedes the original; a reader below it that elects something else gets its own twin, placed in that reader's context — the restatement is the reader's, not the fact's, and putting it where the fact lives would publish it to contexts whose election it is not. Two readers electing the same form share one twin, at the more general of them.
• Checked, and dropped rather than thrown on failure. A merge can create a disjointness violation — (dog Rex) + (cat Fluffy) + a merge makes one individual both — so the same definitional checks place-conclusion runs guard this, and a failure is reported through violations. The original is then left believed: superseding a spelling whose restatement was refused would lose the caller's knowledge outright.
• A reader that changes nothing costs one rewrite. The overwhelming case is a single reader — the fact's own context — because it takes two contexts stating equalities for a second election to exist at all.

note-rule! clj

(note-rule! kb rule-sentex preds f)

Add (inc) or drop (dec) a rule in the two rosters visibility-seeds reads: the predicates it takes as antecedents, and the context it is stated in.

Both are kept here rather than derived on demand because both answer a question a genlCx edge asks and the index cannot: which predicates could a seed usefully have, and does this cone hold a rule at all. Maintained at the rule index/unindex choke points, beside :opposed at the store's, and rebuilt by recover because recovery replays rule indexing.

rebuild-taxonomy clj

(rebuild-taxonomy kb)

Rebuild the in-memory taxonomy from the durable store: the :rebuild column of the table, replayed in entry order over the stored declarations of each functor.

Drops every cache first: a rebuild that merged into the existing one could only ever add, so an entry whose sentex is gone would survive the recovery that was supposed to re-derive it.

recheck-every-exception clj

(recheck-every-exception kb)

Re-check every rule carrying an exception — the blanket trigger. Two channels take it: recover, where nothing about blocking survives a restart so every exception must be re-decided from scratch and there is no edge or fact to narrow by, and recheck-equality-edge on the sides where its own narrowing is blind — a class splitting, and a schematic rewrite arriving.

(A genlCx edge change does not come here: recheck-genlCx-edge narrows it to the excepted rules whose firings live in the moved visibility cone, the context-keyed twin of recheck-genl-edge's predicate keying.)

There is no triggering sentence here — the whole blocking state is being rebuilt — so this queues :all and every firing of every queued rule is re-evaluated.

recheck-except clj

(recheck-except kb except-sentex)

An (except (sentexHandle H)) fact arrived or left: queue every rule the visibility change touches, so settle (on arrival) sweeps a conclusion now resting on an invisible antecedent and retract! (on departure) re-derives one the fact can be seen for again. Two rule sets, because the two directions need different rules:

• the rules of firings that use H (jtms/dependents) — the conclusions to sweep when the except arrives; and
• the rules that could fire on H (rules-by-antecedent over H's predicate and its supertypes, the same fan matching does) — the conclusions to re-derive when the except leaves, since by then the firing that used H has been swept away and dependents no longer names it.

Queuing both on both directions over-approximates (the per-placement hidden-set test in chain/justification-excepted? and derive-conclusion's block narrow it), which is the safe direction — a spurious re-check costs one query, a missed one leaves a conclusion resting on an invisible fact or fails to bring one back.

Returns the rule handles it marked — the settle loop re-chains them when the trigger was a belief flip, which moves no blocked justification for the drain to notice on its own.

recheck-except-cone clj

(recheck-except-cone kb)

A genlCx edge moved visibility for the contexts in context-down(sub), which changes not only what an exceptWhen query sees (recheck-genlCx-edge) but also which handles a believed except hides from a context in the cone — so a derivation it blocks or releases must be re-checked too. Re-queues every except's affected firings (recheck-except). Gated on the except root, so a KB using no except pays one count and stops; excepts are rare, so re-queuing all of them on a rare edge change is the cheap over-approximation.

recheck-on-sentence clj

(recheck-on-sentence kb sentence)

The re-check trigger for a whole sentence: its functor, and — for a negation — the functor of the positive body underneath, since (not (penguin X)) is content about penguin and an exception on penguin must see it come and go.

Both postings carry the whole sentence as the trigger, not the predicate they were keyed on: what narrows a firing is the arguments as well, and the negation is content about the same arguments as its body.

underlying-body, not positive-body: a genuinely negative sentence is exactly the interesting case here. (not (penguin X)) arriving is what defeats a believed (penguin X), and a re-check condition reading belief — an unknown, an aggregate's census — moves on the defeat with no fact having been stored or removed.

The body is read once and serves all four consumers: the predicate-keyed posting above, the declaration posting, the qualitative trigger and the preservation trigger — each for the same reason, that a calculus, a declaration's subject and a predicate are named by what is under the not, never by the not.

refresh-supersessions clj

(refresh-supersessions kb)

(refresh-supersessions kb extra)

Reconcile the superseded set with the equality closure — the equality analogue of tax/refresh-beliefs, and called from the same place for the same reason.

It reads the moved region itself rather than being handed it, because it is called from three places (an assert that merged, the end of a settle, and recover) and the window each of them wants is the same one: everything the TMS has relabelled since the last settle finished.

resubsumption-seeds clj

(resubsumption-seeds kb removed)

The chaining seeds a teardown owes, given the removed sentexes its sweep collected — subsumption-seeds and visibility-seeds in the retraction direction.

A firing names one witness for each reachability it rests on: the genl path a subsumed match climbed, and the genlCx path its placement saw each ingredient context over (taxonomy/reach-support, chain/visibility-support). So removing an edge on one of those paths invalidates the justification and the dependency-directed sweep collects the conclusion. That is the point. But a reachability can outlive one of its supporters — the same edge asserted from a second context, or a second path around the one that went — and then the conclusion is still licensed and must come back. So the facts the departed edge could have carried go back on the agenda and the rules fire again over them: a genl edge's spec subtree, a genlCx edge's two cones.

Revival is a re-derivation, at a fresh handle, exactly as it is under exceptWhen: the sweep deleted the conclusion, so there is no label to flip back. That is the price of naming a witness rather than every witness, and it is the same price the qualitative support pays for the same reason (docs/qcn.md) — carrying every route would be one justification per path through a hierarchy where paths multiply.

Two things make the reading exact.

It is taken before the teardown, while the taxonomy still holds the departing edge: specs is what decides which facts could have subsumed through it, and reading it afterwards asks the shrunken hierarchy a question about the whole one — with (genl dog mammal) gone, specs(mammal) no longer names dog, whose facts are exactly the ones that need re-joining. The context cones are read at the same moment and are not sensitive to it, since removing (genlCx sub super) changes neither who reaches sub nor what super reaches; reading them early is the same answer, from the one place that has the records in hand.

And it is gated on the sweep having taken something besides the records asked for: a justification naming the departing edge is deleted with it, so a conclusion that survived kept another one and needs no re-derivation, and a conclusion that did not is in removed. So retracting an edge that licensed nothing — the common case — costs one functor read per removed record and no chaining at all.

The re-join is unconditional where it happens, and asking it any other way would be a bug. Whether the reachability really survived is place-conseq's question, decided from the taxonomy as it now stands; a gate here guessing the answer from the departing edge alone would be wrong wherever the surviving route runs somewhere other than between that edge's own endpoints, and a missed revival is the arrival-order dependence the witnesses exist to remove. That is why visibility-seeds is called in its ungated arity: its own gate is the one this paragraph forbids, sound for an arriving edge and not for a departing one. So most of what this seeds finds nothing to place, and that pass is deliberately silent: chain/*report-no-placement?* is bound off around it, since a firing the caller's own retraction just killed is the retraction restated rather than a diagnosis of the KB.

subsumption-seeds clj

(subsumption-seeds kb sentence)

The stored facts a new (genl sub super) edge newly makes matchable, as chaining seeds — the taxonomy twin of lift-existing, and there for exactly the same reason.

Matching fans an antecedent's functor over its genl spec closure, so an edge arriving after the facts changes which antecedents they satisfy: (dog Muffet) stored, then (genl dog animal), and a rule on (animal ?x) should fire. The semi-naive agenda never sees it — the arriving datum is the edge, and firing the rules keyed on genl is not the same thing as re-firing the rules the edge just connected. Without this the same three sentences derive a conclusion in one order and not the other, which is the one thing belief may not depend on (docs/nmtms.md).

The seeds are sub's whole spec subtree, because subsumption is transitive: an edge at the top of a hierarchy makes every fact below it matchable at the new supertype. Believed only — a disbelieved fact matches nothing, and it will seed the agenda itself when it revives. Cost is the subtree's extent, paid once per edge, and it is nothing on the ordinary load order (a hierarchy arrives before the facts under it, when the extent is empty).

The removal side is resubsumption-seeds below: a firing names the genl edges it subsumed through, so dropping one withdraws what it licensed — and the facts have to go back on the agenda when the reachability outlives the supporter that left.

table clj

entries as the lookup map the walks below dispatch through.

unindex-exceptWhen-meta clj

(unindex-exceptWhen-meta kb meta-sentex)

The mirror of index-exceptWhen-meta: withdraw the departing exceptWhen meta-sentex's postings, then re-post the rule from the predicates its remaining exceptions and NAF antecedents still need — a set re-add restores any shared predicate the blanket withdraw over-removed, and leaves the rule off the :rules roster exactly when nothing watches it any more. Queues the rule for re-check, since losing an exception may revive what it was blocking.

universal-context clj

visibility-seeds clj

(visibility-seeds kb sentence)

(visibility-seeds kb sentence gated?)

The stored facts a new (genlCx sub super) edge newly makes matchable, as chaining seeds — the context twin of subsumption-seeds, and there for exactly the same reason.

Matching fans an antecedent up the visibility cone, so an edge arriving after both the rule and the facts changes which facts the rule can see: (cFactP CA) in CxMid, a rule in CxLow, then (genlCx CxLow CxMid), and the rule should fire. The semi-naive agenda never sees it — the arriving datum is the edge, and firing the rules keyed on genlCx is not the same thing as re-joining the rules the edge just gave a wider view. Without this the same four sentences derive a conclusion in the orders that put the edge first and nothing in the others, which is the one thing belief may not depend on (docs/nmtms.md).

Both cones, because an edge pairs rules and facts in two directions. It is not only that a rule below can now see facts above: a rule stated above applies in every context that sees it, so the edge equally hands the general rule the specialized context's own facts, and places its conclusion there. Seeding is by fact, so the seeds are the believed sentexes of super's up-cone — seeing super means seeing everything super sees — together with those of sub's down-cone, the contexts a rule above is now inherited into. Taking one and not the other fixes half the orders and leaves the rest, which is worse than either: the shape that still fails is the narrower one, and so the easier to mistake for correct.

Enumerated from the rules, not from the cone, and the difference is asymptotic rather than a constant. Walking the cone and keeping the facts some rule could match costs one record fetch per sentex in the cone — so wiring N contexts under a CxUniverse holding K facts is O(N·K) where the KB without this is O(N+K), and building a spindle D deep is O(D²) because each edge's up-cone is the whole chain above it. Measured: 3.9x on the first shape, 5x and climbing with depth on the second, and 1.8x on the starter load, which does wire contexts after filling them.

So it goes the other way. :rule-antecedents is the live roster of predicates some rule takes as an antecedent, kept O(1) at the rule index/unindex choke points beside :opposed; this walks those predicates' extents and keeps the facts whose context is in the cone. Cost is then proportional to the rule-relevant facts and independent of how much ontology the cone holds — a KB with no rules pays one map read, and the upper ontology sitting in CxUniverse is not walked because almost none of it is a rule antecedent. The cone is a set membership per candidate, so it costs nothing to ask about both cones.

And each half is gated on the other holding a rule, which is what makes the ordinary case free rather than merely cheap. Seeding super's facts is worth nothing unless some rule sits in sub's down-cone to newly see them, and seeding sub's facts nothing unless a rule sits in super's up-cone to be inherited into it. Wiring an empty context under a full one — the commonest edge there is — holds no rule on the new side, so it seeds nothing at all, where without the gate it re-seeds the whole ontology above and re-joins rules that already fired on every fact of it. That is the difference between 3.9x on the shape and 1.0x, and it is not the enumeration but the chaining the seeds provoke. :rule-contexts answers it as a map read per context in the cone, and contexts are few.

Withdrawal needs no twin of this, because dropping an edge narrows what a rule sees and a firing names the genlCx edges its placement saw its ingredients over (chain/visibility-support) — so the ordinary dependency-directed sweep already withdraws one whose antecedent stopped being visible. What the removal side does owe is the other half, revival, and this is called for that too: resubsumption-seeds puts these same seeds back when a sighting outlives the edge that witnessed it.

And on that path the gate does not apply, which is the two-arity form. The gate is sound for an arriving edge because an arriving edge is the only new reachability: nothing can newly match except through it, so a cone holding no rule newly matches nothing. A departing edge says nothing of the kind. The firing being revived was placed where it could see the rule and the facts by whatever route it liked, and the route that went need not be the route either of them lay on — a placement seeing the rule down one branch and the facts down another loses an edge whose two cones hold neither. Asking the gate there answers a question about the departed edge's own line and calls it a question about the firing, which is resubsumption-seeds's stated reason for re-joining unconditionally: a missed revival is exactly the arrival-order dependence the witnesses exist to remove, and the KB that never held the edge derives the conclusion. The cost is bounded by the same thing that bounds the pass around it — it runs only where a sweep already took a record the caller did not ask for.

wff-problems clj

(wff-problems tax sentence)

Structural well-formedness problems for sentence (empty if OK) — the :wff column of the table, walked. A sentence whose functor has no entry (or no :wff arm) is structurally unconstrained here; its argument types are still checked by the argIsa constraints.

wff-violation clj

(wff-violation kb sentence)

The same check as a value, for content a rule derived rather than one a caller asserted: nil when sentence is well-formed, else a violation map in the shape checks/constraint-violation returns.

assert checks this on the way in, but a rule may conclude a special predicate — (implies (relates ?x ?y) (genl ?x ?y)) derives taxonomy edges — and the derivation path had no such check. A derived edge reaches the closure through integrate-transitive, so a rule could close a genl cycle that the same edge asserted directly would have been refused for, leaving genls/specs cyclic — and those are what matching, placement and stratification all read.

Dropped and reported rather than thrown, like every check on that path: chaining is a fixpoint and must not abort halfway through one.