vaelii.impl.special — com.vaelii/vaelii 0.24.0

The special-predicate dispatch table: what each functor the engine interprets does to the derived state around the store, stated once, with every half of every behaviour 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 arms live once here, in arms, keyed by functor:

: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 context]) structural well-formedness (vaelii.impl.wff keeps the check fns; the table points at them. context scopes the arms that read it — today only disjoint-problems)

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.

The enumeration is not here. Which functors the engine interprets, in what order, what each one says — its sentence shape, the :props kind it maintains, whether its arms run on the derivation path — is one entry per term in vaelii.impl.predicates, which requires nothing and so can be read by taxonomy, wff and provers, none of which can read this namespace. That split is what lifts the four-place ceiling above: the arms need functions from four layers and can only ever live at layer three, while what a predicate says is needed at every layer there is. entries joins the two, check-declarations refuses a disagreement, and predicates_test pins the join against the live rosters.

structural-integrate stays outside that framework permanently and no declaration can name its arms: they dispatch on a sentence's shape rather than on its functor — a rule, an exceptWhen meta, a visibility except, and a disjoint metatype's member, whose functor is the metatype and so is data rather than vocabulary.

What this namespace still owns is everything the arms are and everything they need: all four arm columns, the five walks over them, 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.

antisym-equate-existing clj

(antisym-equate-existing kb sentence)

When an (anti_symmetric P) declaration arrives, derive the equalities P's already stored facts license — the twin of equate-existing, over the antisymmetric merge. Sweeps the whole spec subtree beneath P (the mark descends), and hands each stored fact back to derive-antisymmetric-equalities, so the two arrival directions cannot drift about what a converse licenses or what justifies the merge. nil when sentence declares nothing antisymmetric.

antisym-equate-under-context-edge clj

(antisym-equate-under-context-edge kb sentence)

When a (genlCx sub super) edge arrives, derive the equalities an (anti_symmetric …) mark already licenses over facts the widened ancestor set newly makes jointly visible — the twin of equate-under-context-edge, over the antisymmetric merge and anti-symmetric-mark-relevant? in place of the functional one. Same shape, same reasoning throughout — see equate-under-context-edge, including for why a later retraction of this edge does not un-merge what it derives.

antisym-equate-under-edge clj

(antisym-equate-under-edge kb sentence)

When a (genl sub super) edge arrives, derive the equalities an (anti_symmetric …) mark above super now licenses over the (sub …) facts already stored — the twin of equate-under-edge. Free for an edge no anti_symmetric mark stands above, decided before the subtree is read. nil when sentence is not a genl edge.

arrival-releasable-rule? clj

(arrival-releasable-rule? kb rh)

Can an arriving fact release a block on the rule stored at rh? True when rules/arrival-releasable? holds of it, or rules/exception-arrival-releasable? of its exceptions. The settle loop owes such a rule a re-join, and the two edge triggers below exempt it from their firing-side narrowing.

believed-again-sweeps clj

(believed-again-sweeps kb handles)

Run, for each symbol-merge supporter in handles that is stored and believed, what its arrival runs over the stored facts: the re-check of the merged class (recheck-equality-edge) and the migration (equality-arrival-sweep). Returns one {:new :superseded :violations}. handles is tax/take-believed-again!'s answer: a supporter whose firing was held void met its arrival with nothing to restate, and a relabel brings it IN with no arrival. Walked in content order, and scoped to each supporter's class.

check-declarations clj

(check-declarations entries)

(check-declarations entries arm-functors)

Refuse a table whose arms and declarations disagree — the cross-layer half of check-entries, which sees only the arms and so can only check that they mirror each other. Three disagreements are refused, all at namespace load:

• a functor with arms and no declaration, or a declaration and no arms. The two are one enumeration now, and a functor in only one of them is a predicate the engine either interprets without saying so or says something about and does nothing with. arm-functors is the set of functors the arms map keys, read before entries filters to pr/in-special-table — so an arm keyed on a functor no declaration places in the table is refused here rather than left out of the join unreported. The one-argument arity reads the functors off entries itself, for a caller driving the validator over a hand-built table.
• a :cached declaration whose arms have no cache triple, or the reverse.
• a :checked declaration whose arms have no :wff, or the reverse.

check-entries catches a missing arm; neither validator can catch an arm attached to the wrong functor, which is what special_table_test and predicates_test are for. Two validators at two layers, each checking what it can see: they are not to be merged.

One :type between them — :bad-table-entry, discriminated by :mismatch — for the reason check-entries already gives itself two shapes under one word: whichever way the table is bad, the caller catching it is the namespace load, and there is nothing a second keyword would let that caller do.

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. :mismatch says which — :partial-cache-triple or :no-arm — the same discriminant every other :bad-table-entry in the tree carries, so a caller reads one key rather than guessing from the message. Returns entries unchanged so it can wrap the def.

class-moved-merges clj

(class-moved-merges kb region asked drop?)

Re-ask the collision merges of the handles in region (a delay over jtms/touched) whose class can have moved: drop each collision justification whose members are all IN and one at :default (off when drop? is false), and re-derive from each member IN at :monotonic but a premise this window created at that class. asked is the settle's volatile set of [handle class] asked already. {:new :superseded :violations :removed :members}, :removed the merged removals for the caller's stores and :members the dropped justifications' members; nil, with region unforced, when no merge mark is declared. See docs/equality.md, "functional infers equality instead of throwing".

clear-except-moves! clj

(clear-except-moves! kb)

Empty :except-moves outright — a rebuild reconciles every supersession from scratch.

closure-edge-relation clj

(closure-edge-relation sentence)

The closure relation sentence puts edges into: its functor for a binary genl or genlCx edge, genl for a cover (tax/installed-edges), and nil for any other sentence.

deduce-arg-types clj

(deduce-arg-types kb entailments handle context)

(deduce-arg-types kb entailments handle context pre-checked?)

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.

pre-checked? says these entailments already passed the definitional constraint check, so each mint's admissibility test skips it (inadmissible). Only the assert path passes true, and only for its first level: checks/entailment-check validated those before the trigger was stored. The default is false, which every other caller takes and which the cascade the materializer walks itself takes — a mint drawn one level down was not on entailment-check's pre-store list, so it is checked in full.

deduce-lifts clj

(deduce-lifts kb sentence handle context)

Deduce sentence (stored at handle in context) into CxUniverse if its predicate is decontextualized or is a permuting mark — {:new [handles] :violations [v]}, nil when neither holds.

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.

A permuting mark is lifted whatever the KB declares. (symmetric P) and the three commutativity marks (inherit/permuting-marks) decide the argument order a (P …) sentex is stored in, and the store sorts by a mark stated in any context (res/kb-sentex) from the moment it is stated anywhere. Every other reader of the mark — has-prop? from a context, the symmetric prover, the supporter a mirrored firing names — reads it where its sentex is visible, so a mark stated in one theory would answer the mirror from a sibling through the store and deny it through every other path. The copy in CxUniverse is what makes the two agree: it is visible wherever the store's reading holds. It rests on the mark's statement alone, since a (decontextualized_predicate symmetric) declaration adds nothing the key has not already decided, and on a KB carrying CxCore, which declares one, the copy is the same copy.

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.

departed-edge-seeds clj

(departed-edge-seeds kb handles)

The chaining seeds a settle owes the records among handles that hold closure edges (closure-edge-relation: a genl or genlCx edge, or a cover) and went IN ⇒ OUT in it — resubsumption-seeds for an edge that lost belief rather than its record.

A defeat sweeps nothing: the firings that named the edge as a witness go OUT with it and are retained for revival, so the retraction path's re-join never runs, and a reachability that outlives the edge over a second route never re-derives them. The same three sentences then leave a conclusion believed where the negation arrived first and withdrawn where it arrived last (docs/nmtms.md, "Where the layer stops").

Gated per edge on a dependent that is now OUT, the defeat's counterpart of resubsumption-seeds' gate on the sweep having taken something: an edge nothing rests on, or whose dependents all kept another justification, owes no re-join. The spec subtree is read with the edge already OUT, which changes no answer: specs of the edge's own sub is what lies below sub, and the edge runs above it.

derive-antisymmetric-equalities clj

(derive-antisymmetric-equalities kb sentence context handle)

(derive-antisymmetric-equalities kb sentence context handle readers)

derive-antisymmetric-equalities-in, run from context and from every reader that can see it — the antisymmetric twin of derive-functional-equalities's own wrapper, same reachability (tax/context-down), same two-gate shape (KB-wide, then anti-symmetric-mark-relevant? per fact before the closure read), same reason: two mutually-blind contexts each holding one direction of a converse pair merge only from a reader below both, and a context edge alone (antisym-equate-under-context-edge) is not the only way that reader comes to exist — the facts can just as well be the last of the three to arrive, into a topology the edges already connect.

readers narrows the sweep exactly as it does in the functional twin, is passed by the same one caller, and rests on the same argument — read that docstring for it. The two take the argument together because equate-under-context-edge-via hands it to whichever derive it was given: one twin narrowing and the other not would be the drift the shared body exists to prevent.

derive-functional-equalities clj

(derive-functional-equalities kb sentence context handle)

(derive-functional-equalities kb sentence context handle readers)

derive-functional-equalities-in, run from context and from every reader that can see it — (tax/context-down tax context), which already includes context itself.

A functional clash is a property of what a vantage sees, not of where the arriving fact happens to be stored. Scoping to context alone was fine while nothing could see context but context — the ordinary KB, one flat namespace — but a fact arriving into a context that some other, already-connected reader below it can see is exactly the shape two mutually-blind siblings joined from below present: neither CxLeft nor CxRight can see the other's filler when its own fact lands, so a derivation scoped only to the arriving fact's own context finds nothing, and the reader below — CxBottom, which was told about both edges before either fact arrived — is never asked at all. functional-clashes is itself already context-scoped and answers a different, generally wider, set of clashes for a reader below than for context alone (that is the whole point of asking it again per reader rather than reusing one answer), so this cannot be phrased as context's own result handed down to its readers — each reader gets its own call.

Gated before context-down is read, on the same global roster equate-under-edge/equate-under-context-edge gate on — a KB that declares nothing functional and nothing functionalInArg gets one map read here and never the closure walk, whatever context topology it has, matching the docstring's own standing claim that a KB using none of the feature pays an O(1) set lookup per fact and no more. On the common single-context KB context-down answers #{context}, so the sweep runs its one iteration and reduces to exactly today's behaviour.

Idempotent for the reason equate-existing gives, applied once per reader instead of once per direction: derive-functional-equalities-in itself skips a pair same-class-in? already holds from that reader's own view, so a reader whose ancestor set overlaps another's — which every reader below context overlaps context on, since context-down always includes it — pays a repeated no-op read rather than a repeated merge.

readers, when given, is the only reader set this sweeps — the intersection with context-down(context), not a replacement for it. One caller passes it: equate-under-context-edge-via, which hands down the contexts a genlCx edge actually changed the ancestor set of. A reader outside that set sees exactly what it saw before the edge, so no pair can have newly become jointly visible to it; whichever of the other three arrival orders applies had already run there, each with its full fan. Which set that is comes straight out of context-down, which filters its raw candidates by (sees? tax % c) — every candidate's own forward walk — and so is the exact inverse of context-up, except holes included: context-up(R) gains super's side exactly when sub is in it, which is exactly when R is in context-down(sub).

nil is the default and the every-other-caller case: a fact, a declaration or a genl edge arriving last changes no context's ancestor set, so there is no smaller set to narrow to and all of context-down is swept. genlcx_sweep_test pins both the pairs the narrowing must keep deriving and the readers it must not visit, and genlcx_sweep_cost_test pins that the count does not grow with readers the edge did not reach.

This is what lets equate-under-context-edge and equate-under-edge stay the same shape: each already calls this function once per stored fact, using that fact's own storage context, exactly as it always has — the sweep this wrapper adds is what reaches the readers a fact's own context cannot, so neither caller needs a reader computation of its own any more. derive-antisymmetric-equalities is the twin, over derive-antisymmetric-equalities-in.

A second, per-fact gate stands in front of the reader sweep (functional-mark-relevant?), and it is not redundant with the KB-wide one above it. The KB-wide gate answers does this feature exist at all; a KB that declares (functional birthYear) and nothing else still asserts every other predicate it has, and without the per-fact gate every one of those unrelated facts pays a full context-down closure read regardless — a plain, unrelated fact landing in a context with thousands of readers below it costs a thousands-of-contexts sweep for a functional-clashes call that is always going to answer empty. The per-fact gate is what functional-clashes is always going to check anyway (tax/props-over, tax/functional-in-arg-over), asked once, early, before the expensive part rather than N times inside it.

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 integration arms a derived sentex may reach, 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).

The dispatch is run-integrate-arms's, narrowed. A functor the table keys runs its :integrate arm iff the entry is flagged :derived? (integrate-transitive); a functor it does not key runs the structural walk, minus the rule arm the caller posts by name (structural-integrate's derived?). Both halves have to be here or the derivation path reaches a strictly smaller set of caches than recover's rebuild does, and the running KB and the restarted one then disagree about one store: a rule concluding a disjoint metatype's member separated nothing until a restart replayed it, and a rule-derived (except (sentexHandle H)) hid its target from the reads — the index holds it from the store primitive (kb/create-sentex) — while no firing that used H was ever queued for the sweep.

The except arm's reconcile-belief-change is called inline, mid-fixpoint, and that is safe. Neither half of it re-enters chaining or settling: tax/note-supporter-visibility-change! is one swap! bumping a generation, and tax/refresh-beliefs is a swap! over the taxonomy that reads jtms/in? and writes cache entries — no assert, no chain, no settle, and no relabel. It is scoped to the arriving except and the handle it hides, so it costs two handles' worth of edge lookups rather than the vocabulary's. recheck-except beside it only pushes rule handles onto the re-check queue, which is what the settle around this drains; that is exactly what the assert path does from inside its own integrate-sentex.

The one ordering difference from the assert path is that mark-premise runs before integrate/sentex-added, where two of this fn's four callers run it before the justification — so the except is stored, rostered and generation-bumped a few lines ahead of being believed. Nothing reads a scoped taxonomy answer in that window (the callers write a justification and nothing else), and the JTMS labels the region as the justification lands, so the first read after it recomputes against settled belief.

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, the decontextualized_predicate lift, the argument-constraint entailment, and 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.

drain-departures! clj

(drain-departures! kb)

The records note-departure! queued since the last drain, and the queue emptied.

drain-except-moves! clj

(drain-except-moves! kb sweep?)

Take the pending handles off :except-moves, sweep them (except-move-sweeps, with sweep?), and keep the supersessions the sweeps found and the region the moves can change (except-move-region) for take-except-moves!. Returns the sweeps' result, its :new joined by the believed facts of the targets' consequence closure and of the antecedents resting on it, to chain from, or nil when nothing was pending.

drop-kinds clj

(drop-kinds m k gone)

Refusal record m, from which the entries gone have left handle k, with k no longer named under a kind of gone that no entry still under k holds.

drop-replaced-routes! clj

(drop-replaced-routes! kb just)

(drop-replaced-routes! kb just route)

Drop the justifications the one just added as just replaces: the same firing over a route the witness rule no longer names. Returns the merged jtms/drop-justification! results, for the caller to apply to its stores; the dropped records are deleted here.

A justification is replaced when it has just's informant, consequence and bindings, holds every antecedent of just outside route, and differs from it only in genl / genlCx edges that are all believed. route is just's own route handles; nil reads them off the antecedents by shape. The consequence keeps just, whose antecedents are groundable, so the sweep collects nothing just does not hold up.

An edge of the older route that is OUT keeps its justification: a route a defeat took away comes back when the defeat lifts, and the store then holds both (docs/nmtms.md, "Where the layer stops").

edge-descended-justifications clj

(edge-descended-justifications kb gone removed-jids)

The justifications among removed-jids that a departing route edge (route-functors) invalidated while every other ingredient survives, as records — the derivations a teardown owes a re-derivation (rederive-descended). gone is the sentexes the sweep removed.

Read before the teardown deletes the justification records, since the records are what name the fact and the declaration to derive from again. Gated on gone holding a route edge, so a removal that took none fetches no justification record.

A justification qualifies when its informant is an edge-descended derivation, one of its antecedents is a removed route edge, and no removed antecedent is anything else: a removed fact or declaration withdraws the derivation, and re-deriving it would undo the removal.

entail-existing clj

(entail-existing kb sentence dh)

When an (arg P n T) / (genlArg P n T) / (interArg 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.

triggered-mints reaches a conditional form's trigger arriving after both the fact and the declaration, in the settle.

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 predicate extents 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 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.

A declaration whose type is not mintable reads no extent: every arm asks checks/mintable-type? of that type before it draws, so no fact would yield an entailment, and the entry note-unmintable! leaves runs the sweep once it is.

entail-under-context-edge clj

(entail-under-context-edge kb sentence)

When a (genlCx sub super) edge arrives, draw what the declarations it makes visible say about the facts already stored in sub and every context under it — the fourth arrival order of an entailment through an inherited declaration, beside the fact, the declaration and the genl edge. Each derivation names the genlCx edges it sees its declaration through (checks/entailment-support), so retracting this edge takes back what rests on it, and rederive-descended draws again what a second route still reaches. nil when sentence is not a genlCx edge.

Off unless *assertive-arg-types?* and some predicate declares. The facts are read from the smaller of two sides, compared by index counts: the facts stored in the contexts under sub, kept when a declaration reaches their functor, or the facts of the functors a declaration reaches, kept when stored under sub. So the arm costs the lesser of the edge's extent and the declared extent, and a context holding many undeclared facts or a KB holding many declared ones elsewhere costs only the other. Snapshotted 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.

Three 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'; off unless some predicate carries an entailing declaration (declaring-predicates, the taxonomy's roster, no index read); and off unless a genl-ancestor of super carries one (super-reaches-declaration?). The first two keep an edge under a predicate nobody constrained from reading a subtree's extent to discover there was nothing to draw; the third keeps an edge whose sub is constrained but whose super reaches no declaration from reading it, since every mint this arm draws cites the arriving edge and so reaches its declaring predicate through super. The extent itself is subtree-sentexes, filtered by cardinality for the same reason one step further in.

entries clj

The special-predicate dispatch table: an ordered vector of [functor spec] pairs, joined from the arms above and the declarations in vaelii.impl.predicates.

The order is the declaration's — predicates/entries filtered to the functors this table holds an entry for. post-taxonomy-supporters! 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 adds no work), so the order is content and belongs with the other content.

This vector is the functor enumeration the four walks use: integrate, disintegrate, rebuild and wff all walk it, so a predicate declared and armed is added to all four at once, check-entries refuses it half-armed and check-declarations refuses it armed without being declared — the latter reading the arms map keys, which hold every armed functor, not this filtered vector, which by construction holds only the declared ones. table below is the lookup view.

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 predicate-extent 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 — the scoped same-class-in? skips a pair the reader's visible 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 predicate extents 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 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 extents the walk is reading.

equate-under-context-edge clj

(equate-under-context-edge kb sentence)

When a (genlCx sub super) edge arrives, derive the equalities a (functional …) mark already licenses over facts the widened ancestor set newly makes jointly visible — the fourth arrival order of the same three ingredients, and the context twin of equate-under-edge.

The context twin of equate-under-edge's shape, over an ancestor set instead of a subtree: sweep the stored facts context-edge-reader-ancestors says this edge newly makes relevant, kept when functional-mark-relevant? admits their functor, and hand each back to derive-functional-equalities at its own storage context, exactly as equate-under-edge already does. What makes that correct here is that derive-functional-equalities no longer answers only for the context it is handed — it sweeps every reader below that context too (tax/context-down), which is what reaches a joining context this edge just connected without this arm needing a second, independent reachability computation of its own. Before that wrapper existed, this function was that computation, reading each candidate's visibility here instead of leaving it to the callee — one caller's worth of correctness-sensitive logic that a second caller (the plain fact-arrival trigger, which has exactly the same problem when the topology is wired before the facts arrive rather than after) could not share. Centralizing it is what let both shrink back to this shape.

Still genlCx-triggered and still necessary, not redundant with the wrapper's own sweep: a genlCx edge arriving after both facts are already stored changes no fact and fires no ordinary assert, so nothing else re-invokes derive-functional- equalities for either of them — this arm is what does, over the extent context-edge-reader-ancestors names. Gated identically to equate-under-edge at the top: free for a KB that declares nothing functional and nothing functionalInArg, decided before the ancestor set is read.

Budgeted, unlike equate-under-edge. A genl edge's own subtree is bounded by real vocabulary growth — the edge names the very predicate whose subtree is swept, so a big walk means a big subtree the edge itself accounts for. A genlCx edge names two contexts: context-edge-reader-ancestors scopes the walk to what this specific edge makes relevant, so an edge between two small, unrelated contexts no longer costs a KB-wide predicate's whole extent — but the ancestor set itself can still be large (a small edge into a context whose readers reach a genuinely huge, genuinely relevant store), so budgeted-context-edge-candidates still caps what reaches derive-functional-equalities at tax/*exposure-instance-budget* — the same knob the revived-edge merge sweep spends, so a cut here and a cut there answer to one dial — and files a :context-edge-exposure-truncated violation when it cuts, since a pair past the cap is not derived by anything else afterward this same edge (docs/equality.md).

Idempotent for the reason every other direction is: derive-functional- equalities skips a pair same-class-in? already holds from a reader's own view, so reprocessing the same candidate on a later edge, or reaching the same reader through two different marked predicates, costs a repeated no-op read rather than a repeated merge.

Retracting the edge does not un-merge, and that is a pre-existing limitation of derive-functional-equalities rather than something owed here. Its antecedents name the declaration, the two facts, and any genl edges either spelling descended (checks/edge-support) — never a genlCx edge, because no arrival order needs a context edge in that list. An equality this arm derives therefore rests on nothing that names the genlCx edge that made the pair jointly visible, and the same is already true of every other arrival order whenever a fact or a declaration arrives last under a genlCx edge asserted earlier: the merge outlives a later retraction of that edge exactly as it would here. Closing it is a genlCx-support addition to edge-support and to the antecedent list derive-functional-equalities builds, not a gap this arrival order introduces or one its own addition should paper over.

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 an edge no functional-family mark stands above, decided before the subtree is read rather than per fact inside the fold (equate-under-edge-via). This arm fires on a genl edge — the commonest thing an ontology says — so it is the one that reaches for an extent on an ordinary write, and an edge under a broad type whose subtree holds most of the vocabulary reads nothing unless a mark stands over its upper end.

The family, not the arity-2 spelling alone: the fold asks derive-functional-equalities, which reads both spellings, so the gate reads both too (tax/functional-family-declared?, functional-mark-relevant?), or an edge arriving last under (functionalInArg P n) would merge nothing where (functional P) in the same order merges (functional_in_arg_test).

subsumption-seeds reads the subtree's believed handles on every edge regardless, since those facts become matchable at the new supertype.

except-move-region clj

(except-move-region kb pending)

The superseded data whose supersession an except that moved can change: the ones naming a term an equality in the excepted handles' reach re-spells (except-move-terms), stored in a context that sees one of the contexts the moving excepts are stated in. pending is {target #{except-context}}.

A supersession is decided at the datum's own context from the equalities that context sees (displacement), and an except changes that only for the contexts that read it and only for the equalities it withdraws, so this set is the whole of what the settle's reconcile re-examines for it. Each candidate costs a term-index lookup per term, the same lookups the arrival sweep makes, and a KB superseding nothing costs one deref.

except-move-sweeps clj

(except-move-sweeps kb handles sweep? whole scoped)

Run, for each handle in handles whose visibility an except moved, the sweep its arrival runs over the facts already stored: the equality migration for an equality sentex (equality-arrival-sweep), and revived-declaration-sweeps' for a merge or lift mark. Returns one {:new :superseded :violations :removed}, or nil when handles is empty.

An equality restates a fact for the readers that see it, and an except changes which readers those are without the equality arriving, leaving or changing label. A fact stored while the except hid the equality from the fact's context was stored as spelled, with no twin, and every goal from that context is normalized under the equality the moment the except goes — so without this sweep the fact is believed and answered by no read (docs/equational.md, "An except of an equation"). The sweeps are the arrival ones and idempotent, so a twin already made gains nothing, and a handle that is no longer stored, or restates nothing, costs a record fetch. The handles are walked in content order.

The argument-type derivations move the same way (docs/argtypes.md, "An except of an ingredient"): with sweep?, the ones resting on a record an except now hides are dropped (drop-hidden-mints!, :removed for the caller to apply), and the records it stopped hiding draw again. For a handle in whole, whose except itself moved, that is every context and the record's own arrival sweep (revealed-entailments). For one only in scoped, {handle #{[sub super]}}, moved by genlCx edges, it is the contexts under each sub and the edge's own sweep over them (entail-under-context-edge).

except-moved clj

(except-moved kb)

The handles an except of which arrived, left or flipped since the last drain-except-moves!, read without emptying the queue (note-except-move!).

forget-kinds clj

(forget-kinds m k)

Refusal record m with handle k named under no kind: its entries left together.

inadmissible clj

(inadmissible kb sentence context)

(inadmissible kb sentence context constraint-arm)

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

These hold 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, the computed genlCx edge of a context-valued function (context-nat), and abduction, which asks it before minting a hypothesis so that a sentence no assertion could legally make is never one the search assumes. Forward chaining runs the same four over a rule's conclusion in chain/place-conclusion, the naming arm only where a consequent literal's functor is a variable.

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 neither may abort halfway; the third would rather refuse a hypothesis than fail the query that wanted it.

constraint-arm is the definitional-constraint check, checks/constraint-violation by default, which refuses every violation. The argument-type mint passes checks/derivation-violation instead: a mint that clashes with a believed membership is placed, and settle weighs the pair as it weighs a rule's conclusion that clashes (docs/argtypes.md).

A nil constraint-arm omits the arm, for a caller that has already run it against this exact content. The assert path's first-level argument-type mints are the one such caller: checks/entailment-check runs constraint-problem (and cascade-clash, which reads the source's own membership) over every mint of the cascade before the trigger is stored, and refuses the trigger if any mint fails — so a first-level mint reaching the materializer has passed the constraint check already, and storing the trigger and the mints beside it only adds memberships, which cannot turn a passing args/disjoint/arity check into a failing one (each convicts on an absent type, never a present one). Naming, well-formedness and edge stratification are not what entailment-check runs, so they are asked here whether or not the arm is. Every other caller — forward chaining, the retroactive sweeps, and the cascade's own deeper levels, none of which entailment-check pre-validates — leaves it false and pays the full check.

index-closed-extent-rules clj

(index-closed-extent-rules kb pred)

A (closed_extent_predicate P) grant arrived or left: post every stored rule with a closed (not (P …)) antecedent in the re-check index under P, and queue it for a blanket re-check.

The grant is what turns such an antecedent from a lookup into negation as failure, so a rule asserted before the grant carries no posting and no fact on P would ever bring its firings back. Reached through the antecedent index on [:not P], which is the key rules/antecedent-key files a negation under, so this is one lookup and no scan.

Queued with :all-rejoin: what the grant moved is a whole reading, not a sentence, so there is nothing to narrow the firings by — and the rule owes a fresh join as well as a re-check, since the grant blocked nothing for the blocked set to notice and the firings it licenses are ones no justification exists for yet. That is the same asymmetry a widened genlCx ancestor set takes :all-rejoin for. The posting is left in place when the grant leaves: a spurious re-check costs one query, and a missing one is a conclusion that should have been swept and wasn't.

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, queue the rule for a blanket re-check (a fact may already have arrived that its new exception blocks), lower the rule's firings to :default (restrength-firings!), and hold void the firings of a roster rule it convicts (checks/force-sentexes!).

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. A rule whose consequent functor is a variable is filed under the p/var-consequent-key catch-all instead of a canonical ?var0 (see rules/consequent-index-pred); completeness of the consequent read is then the concrete bucket unioned with that catch-all, which resolution/concluding-rule-handles does.

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 :engines / :defeasible are read off it by every consumer. Nothing enumerates rules by defeasibility — 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 entry point 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 table half of derived-sentex-added: for a functor the table keys, only the arms flagged :derived? — the genl / genlCx closure edges, and the marks that carry the flag for their own reasons — 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.) A functor the table does not key is the structural walk's, not this one's.

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, where derived-sentex-added (the forward-chaining conclusion path) narrows the table half to the :derived? entries and drops the rule arm its own caller posts by name.

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.

kind-entries clj

(kind-entries m kind)

Every entry of kind in refusal record m, as [handle entry] pairs, read off the sets of the handles the roster names under kind.

lift-refusals clj

(lift-refusals kb)

The lifts waiting on an argument conviction, as [source-handle entry] pairs in handle order.

lost-descended-derivations clj

(lost-descended-derivations kb handles edges-only?)

The edge-descended derivations among the dependents of handles whose conclusion is OUT, as justification records — edge-descended-justifications for an ingredient that lost belief rather than its record. edges-only? keeps only the handles that are route edges (route-functors).

Two settle arms read it. A genl edge that went IN ⇒ OUT takes the derivation naming it OUT, where a second route to the declaration still licenses it; a defeat deletes nothing, so the justification stays and nothing else draws the derivation again. And a spelling an un-merge gives back is a fact the derivation could not be drawn from while the merge superseded it: an equality over two spellings of one merged pair is found by matching both, so it is drawn only once both are believed again.

Only a justification whose conclusion is OUT, or withdrawn at its own context (exc/believed-own?), qualifies: one that kept another support owes nothing to belief, and asking it again every pass of the settle would re-read a conclusion that cannot move. The dependents are a network read and the record a store fetch, so the gate that drops nearly every handle runs first.

materialize-defn-rules clj

(materialize-defn-rules kb sentence defn-handle context)

Materialize the forward rule(s) a defn* fact stored at defn-handle in context expands into (sx/defn-companion-rules), each a derived rule sentex justified by the defn* fact alone. {:new [handles] :violations [v]} — the new rule handles the caller seeds chaining with (so a rule fires over the facts already stored), and any rule that could not be admitted.

Called from assert-one once the defn* fact has a handle to be justified by. A non-defn* sentence returns the empty result, so the caller pays one defn-sentence? read and stops — the gate that keeps every ordinary assert free of it.

migrate-handle-metas clj

(migrate-handle-metas kb orig twin eqs reader)

(migrate-handle-metas kb orig twin informant witnesses reader)

Carry every believed handle-naming meta of sentex orig onto its migrated twin twin.

A meta and the sentex it names are separate sentexes linked by the handle — (exceptWhen … (sentexHandle H)), (except (sentexHandle H)), a target-following (P … (sentexHandle H) …) — so migrating the named sentex to a new handle would strand its metas on the superseded original: an exceptWhen twin would fire unguarded, an excepted twin would become visible, a reply would name a claim no longer believed. So each such meta gets a twin naming twin (its terms rewritten to the representatives too, a no-op when it mentions no merged term), derived and justified by [the meta, the equality] — the same belief-following discipline the sentex twin itself rides. Retracting the merge collects the meta twins with it and the originals revive. Registered through integrate-twin, so the twin reaches every index arm the original did — the exception re-check, the except roster, the reply cascade.

eqs are the witnesses that migrated the sentex — the meta twin exists because the sentex did, so it rests on the same merge. Public because a (symmetric P) mark folding two mirrored rows into one owes its doomed row's metas the same carry, and hands the declaration itself as the single witness (integrate/commute-existing): what raises a twin differs between the two callers, what a stranded meta costs does not. The 6-arity takes justify-twin!'s informant and witnesses, for a reader's copy.

Rewrites read from reader, the vantage the twin's own form was elected from (migrate-into), so a meta elects the spellings its target does; the unscoped rewrite used the global election, which a merge reader cannot see would diverge from — a twin mis-guarded, mis-hidden or mis-aimed.

migrate-meta-onto-twins clj

(migrate-meta-onto-twins kb sentex)

A handle-naming meta s was just asserted. If the sentex it names already migrated to twins, the merge ran before this meta existed, so migration never saw it — the meta lands on the superseded original and the live twin is unguarded / visible / unendorsed (docs/equality.md, the meta-after-merge case). For each twin, replay migrate-handle-metas — it re-points every believed meta of the target (this new one included) and is idempotent for those already carried. A no-op when s names nothing or its target has no twin, the common path; returns nil either way, and the twins settle with the caller's settle. Takes the stored sentex (like migrate-sentex), not the bare sentence.

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 required:

• 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 as a derivation. The twin is asked what a rule's conclusion is asked (checks/derivation-violation). A merge that creates a disjointness clash — (dog Rex) + (cat Fluffy) + a merge makes one individual both — stores the twin, and the clash is decided and reported like any stored clash. Only an inadmissible twin (an argument conviction, a malformed form) is dropped and reported through violations, and the original is then left believed: superseding a spelling whose restatement was dropped 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.

migrate-under-context-edge clj

(migrate-under-context-edge kb sentence)

When a (genlCx sub super) edge arrives, restate the sentexes the widened ancestor set newly exposes to a merge — the third arrival order of the same three ingredients, and the equality twin of visibility-seeds.

An equality applies where it is visible, so which sentexes it restates is as much a question about the genlCx ancestor set as about the closure. migrate-class covers the merge arriving last and migrate-sentex on the assert path covers the fact arriving last; without this the edge arriving last leaves the record spelled the way a context that could not see the merge stored it, while every read from a context that now can asks after the representative and misses it — a sentex believed and answering no query, in exactly the orderings that wire the contexts last. reconcile-context-edge runs the full supersession reconcile on the same edge, which re-derives which spellings are displaced; what it cannot do is write the restatement, since an entry there is only ever dropped or restated and a spelling starts being displaced when migration says so.

Both ancestor sets, because an edge pairs facts and merges in two directions. The whole of the new reachability is that a reader in context-down(sub) now sees context-up(super), so a triple of reader, fact and merge is new only if the reader newly reached one of the two — which puts that one in super's ancestor set and the reader in sub's descendant set, whichever it was. So there are two halves: a merge above meeting the facts the widened readers already saw, and a fact above meeting the merges they already saw. Taking one and not the other fixes half the orders and leaves the rest.

Enumerated from the merges, not from the ancestor set, for visibility-seeds' reason: the candidates are the stored sentexes naming a term one of those merges displaces, and the inverted term index answers that in one lookup per term. Cost is then proportional to the standing merges and to what they reach, and independent of how much ontology the ancestor set holds — a KB that has merged nothing pays one set-empty test, and each half is gated on the other side holding a merge the reader can see, so wiring a context under one whose merges it already inherits enumerates nothing.

The removal side needs no twin of this. Dropping an edge narrows what a reader sees, and a twin names the equality edges it was elected over (justify-twin!), so the ordinary dependency-directed sweep collects one whose merge the reader can no longer see, and refresh-supersessions hands the spelling back.

mint-informant? clj

(mint-informant? informant)

Is informant one an argument declaration's mint is justified under?

mint-refusals clj

(mint-refusals kb)

(mint-refusals kb gens)

The declarations waiting on a type to become mintable, as [decl-handle entry] pairs in handle order — empty on nearly every KB. With gens, only the entries stamped under other generations, compared before the sort, so a settle pass under unmoved generations sorts nothing.

minted-seeds clj

(minted-seeds kb handles)

handles — sentexes an entailment minted — as chaining seeds, followed by the subsumption-seeds of each one that is a genl edge. A genlArg mint is an edge like an asserted one, and the facts under it become matchable at the new supertype whichever of the two stored it: seeding the handle alone fires the rules keyed on genl, not the rules the edge connected, so (wolf Rex) and a rule on (animal ?x) stored before a minted (genl wolf animal) would derive nothing in that order only.

naming-violation clj

(naming-violation kb sentence context)

The :naming violation sentence in context carries under kb's naming policy, or nil: nm/blocking-problems as the value a caller that may not throw drops a sentence for. Nil under :warn and :off.

note-departure! clj

(note-departure! kb sentex)

Queue sentex, leaving the store, for withheld-releases when it is a record that can have subsumed a mint (subsumer-shaped?). Called from integrate/sentex-removed!, the one place a record leaves, and only with pruning on.

note-except-move! clj

(note-except-move! kb h context edge)

Queue handle h on :except-moves: an except of it stated in context arrived, left or flipped, so what h restates or merges is visible to a different set of readers there and below. edge, a (genlCx sub super) edge's [sub super], says the move is that edge's and reaches the contexts under sub alone (:scoped); nil says the except itself moved (:whole). The settle drains the queue (drain-except-moves!, take-except-moves!).

note-kind clj

(note-kind m k e)

Refusal record m with handle k named under entry e's kind.

note-unpremised! clj

(note-unpremised! kb h)

Queue the record at h, whose premise mark a retraction removed while a derivation still holds it up, for the settle's withdrawal question: a record an author stated beside a mint of the same sentence is not the entailment's to withdraw, and once the statement goes it is (mint-only?), so a believed record that says it more specifically withdraws it as it withdraws a mint it meets on arrival.

offer-marked-existing clj

(offer-marked-existing kb sentence)

When a functional, functionalInArg, asymmetric or anti_transitive mark arrives, offer every stored fact of the marked predicate's spec subtree to decide/offer!, which reads the nogoods each forms under the mark. nil.

offer-marked-under-edge clj

(offer-marked-under-edge kb sentence)

When a (genl sub super) edge arrives under an offered-marks mark on super or above it, offer the stored facts of sub's spec subtree to decide/offer!. nil, and free for a KB declaring none of the marks.

post-mint! clj

(post-mint! index sentence context h)

File record h, holding sentence in context and concluded by a stored justification mint-informant? accepts, in index's mint family, when the sentence has a roster-term. Posted from the sentence in hand: entail-arg-type as it stores the justification, and reindex from the record it is indexing.

post-taxonomy-supporters! clj

(post-taxonomy-supporters! kb)

Post the taxonomy's supporter families (kv/post-supporter!) for every stored declaration in kb: the :rebuild column replayed in entry order over a scratch taxonomy whose index store is kb's, then each stored disjoint metatype's members. reindex's share of the index that its per-record pass cannot post, since the key a declaration installs is the table's to say. kb's own taxonomy is not touched, and the equality relations, whose partition keeps its own supporters, post nothing.

A stored genl / genlCx declaration whose positional read is not a well-formed edge is dropped rather than posted (replay-edge), and the count is warned once — the same discipline rebuild-tms follows for a justification the store cannot root. A well-formed store never has one; a store an older or foreign writer left a non-edge sentex in the genl / genlCx predicate extent does, and posting it would seed a null closure node that crashes restore-depths.

posts-recheck? clj

(posts-recheck? kb sentence)

Would sentence arriving or leaving queue a watched rule (recheck-on-sentence)? Queues nothing.

rebuild-pending! clj

(rebuild-pending! kb)

Rebuild the engine's own waiting derivations after recover: every stored entailing declaration whose type is not yet mintable, and every decontextualized lift an argument conviction refuses (a permuting mark's included), re-noted as their arrival noted them. The refusal record is in-memory state no store holds, and chain/rerecord-refusals! rebuilds only the rules' half of it. The lift sweep is lift-existing's, which over copies already stored adds nothing and so only re-notes the refused ones.

rebuild-taxonomy clj

(rebuild-taxonomy kb)

Rebuild the in-memory taxonomy over a cleared one: the believed side of every key the index's supporter families hold (tax/refresh-beliefs with no region, reading the network's labels), and the equality partition and rewrite rules, which keep their own supporters, replayed from their stored declarations by the :rebuild column. Reads no other record.

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-defeat-target clj

(recheck-defeat-target kb sx)

Post the re-check a (defeat (sentexHandle H)) sentex sx owes H's watchers when it is stored, removed or relabelled: the defeat moves H's belief at the contexts that see it with no relabel of H, so H's sentence posts what its own arrival posts (recheck-on-sentence), and a permuting mark resting on H re-spells its facts (note-mark-reach!). A no-op for any other sentex, and for an H no longer stored.

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 ancestor set, 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)

(recheck-except kb except-sentex trigger edge)

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 rest on H through any chain (the justifications of H's consequence closure, jtms/consequence-closure) — the conclusions to sweep when the except arrives, and the blocked ones to release when it leaves; and

• the rules that could fire on H or on what rests on it (rules-by-antecedent over each predicate of the closure and its supertypes, the same fan matching does) — the conclusions to re-derive when the except leaves, since by then the firing that used one has been swept or refused and dependents no longer names it; and

• H itself, when H is a rule. A firing rests on its rule as it rests on its antecedents — the rule handle is in the stored justification, which is what sweeps its conclusions when the except arrives — but on departure the swept firing is gone from dependents, and the predicate fan above is keyed on a fact's functor, which a rule sentence never matches. Re-chaining the rule is the departure-side twin the fact arm has in rules-by-antecedent: without it, retracting a rule-targeting except revives the rule's visibility and none of its conclusions.

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.

H goes on :except-moves as well (note-except-move!), for the restatements the visibility change moves: an equality or a merge mark H restates facts only where it is visible, so the settle re-runs H's arrival sweep and reconciles every supersession.

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-ancestors clj

(recheck-except-ancestors kb sub super)

A (genlCx sub super) 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 ancestor set — so a derivation it blocks or releases must be re-checked too. Re-queues the affected firings of each except the edge moves (recheck-except): one stated in a context super sees, since an except hides its target from the contexts that see its own, and the edge changes what a context under sub sees only by super's ancestor set. An except naming one of those adds the except it names, whose cascade moves with it. Read off the except extent in super's ancestor set, so an edge whose super sees no context stating an except re-queues none (lein perf's genlcx-edge-beside-excepted-declarations).

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.

recheck-subjects clj

declaration-subjects' functors as a set — which declarations post to the exception re-check queue through the shared path rather than from arms of their own.

Public because predicates/check-facets holds every declaration that answers goals about a predicate to posting by one route or the other, and the two routes live in different namespaces: a :retriggers facet says the arms do it, this says recheck-declaration does. A declaration in neither decides by arrival order, which is what that rule refuses at load.

reconcile-belief-change clj

(reconcile-belief-change kb)

(reconcile-belief-change kb moved)

(reconcile-belief-change kb moved visibility-moved?)

Reconcile every belief-derived taxonomy cache after moved may have changed truth.

Bare, like recover and every other recompute: it rebuilds caches from what the KB currently believes and stores nothing of its own, so re-running it is the whole of taking it back.

This is the engine-level choke point above tax/refresh-beliefs: ordinary JTMS defeat/revival/supersession and visibility except both change whether a stored declaration currently has force. moved may name either declaration handles or except handles; the latter are expanded to their targets before the scoped refresh.

The three-argument form lets a removal path report a visibility change explicitly: once the exception record has been deleted, its target alone cannot prove why the effective-supporter generation changed.

The caches read the network (jtms/in?); a scoped read filters a supporter through the read walk (res/supporter-believed?). The two-argument form decides visibility-moved? by reading moved's records for an except, whose relabel moves what the scoped reads see, and evicts the scoped closures each relabelled defeat can move (kb/retire-defeated-reads!) — each behind a stored except or defeat (reads/stores-any?), so a KB storing neither pays no fetch per moved handle (belief-change-region says why the gate is exact).

reconcile-context-edge clj

(reconcile-context-edge kb sentence)

Everything a (genlCx sub super) edge means for the equality closure and the argument-type entailments, in one call: the sentexes the widened ancestor set newly exposes to a standing merge (migrate-under-context-edge), the two merges the same widening newly licenses (equate-under-context-edge for the functional family, antisym-equate-under-context-edge for the antisymmetric one), and the derivations the declarations it makes visible draw (entail-under-context-edge). Returns the usual {:new :superseded :violations}. Safe on any sentence: each arm gates on the genlCx functor itself, so a non-edge costs three functor reads and returns the empty result.

One function because a genlCx edge arrives by three entry points, and only two of them remembered the list. An edge can be asserted (assert-entry/assert-one), concluded by a rule (chain/place-fact-conclusion), or computed — materialized by the structural producer off a contextArgSubrelation declaration with nobody asserting anything (context-nat/materialize-edge). The first two spelled the trio out side by side and the third spelled none of it, so a calendar month→year edge posted the exception re-checks and ran no merge at all: two fillers of one functional slot, made jointly visible for the first time by that edge, stayed unmerged and uncontradicted, and asserting a single irrelevant stated edge afterwards repaired it (vaelii#56). An entry point that has to remember a list is an entry point that forgets it — this is the list, and it is the only thing a fourth entry point has to call.

Not merged into the genlCx :integrate arm, which would be the one place every entry point already passes through, for a timing reason that is not incidental: the arm runs from integrate/sentex-added and derived-sentex-added before the edge is justified, so the edge is a node nothing supports, tax/context-up and tax/context-down — belief-filtered like every closure here — have not widened yet, and all three sweeps would enumerate the pre-edge ancestor set and find nothing. Chaining learned this first and says so at its own call site; the rule is the same one: reconcile after the justification, never beside the integrate arm.

nil when no arm did anything, which is the shape each of them already returns and the one the fixpoint's mig gate reads: a conclusion re-derived on every round of every defaults pass must added no work rather than a little, so this collapses to nil rather than to an empty accumulator.

An edge changes which merges a reader sees, so while any spelling is superseded it runs the full supersession reconcile itself, over the arms' output too, and hands back no :superseded for the caller to reconcile again.

reconcile-removed-supersession! clj

(reconcile-removed-supersession! kb sentex)

The supersession reconcile sentex leaving the store owes, from the removal choke point: the full pass for a genlCx edge or a schematic rewrite rule while any spelling is superseded, and the narrowed one over sentex and the classes it moved for a superseded datum or an equality sentence. A superseded datum leaving drops its entry, and an equality leaving gives back the spellings its class displaced.

record-arg-types clj

(record-arg-types kb)

Record the argument-type entailments every stored fact draws, over a store whose facts were written without them: {:facts n :new [handle …] :violations [v …]}.

assert draws them as each fact arrives. A store loaded around that path — a dump import, *bulk-load?*, bulk-assert-facts! — holds the facts and none of their derived memberships and edges, and recover rebuilds belief from the stored justifications without drawing any. This is the one pass that records them, so the store then holds what a per-fact load of the same facts holds. Run it once, after the load and after the store is recovered or reindexed, since the declarations and the hierarchy they name are read from the taxonomy.

Facts are read per declared functor, every predicate under an entailing declaration in content order, and each fact is asked once whatever number of declarations reach it. Idempotent: a derivation already recorded adds nothing (has-justification?).

rederive-descended clj

(rederive-descended kb justs)

Draw each of justs (edge-descended-justifications) again from the taxonomy as it now stands, and return the handles it created as chaining seeds. The violations are reported and the spellings a merge displaces are refreshed here, as the arrival path does for the same derivations.

Each derivation is asked for through the function its arrival arms ask: the entailment through retroactive-mints, narrowed to the declaration the removed justification named; a descended equality through derive-functional-equalities or derive-antisymmetric-equalities over the fact at the head of its antecedents. So where a second route survives, the derivation comes back resting on it, and where none does, nothing is drawn. A conclusion that kept another justification takes the surviving route's as well, which is the justification the same content loaded without the edge records.

An entailment's antecedents lead with the fact and the declaration, in that order (entail-arg-type). An equality's are in content order (derive-equality), so its facts are read off by functor: every antecedent that is neither a genl edge nor a mark declaration. Each task is drawn once however many of the removed justifications name it.

refile-mint! clj

(refile-mint! kb old h)

Bring record h's entry in the mint family to its stored spelling: out from under the roster term of old, the record h held before (nil when its spelling did not move), and under the current one while a mint justification concludes it. The callers are the store mutations that move a record's spelling (integrate/respell!) or the justifications concluding it (integrate/fold-row!).

refresh-supersessions clj

(refresh-supersessions kb)

(refresh-supersessions kb extra)

(refresh-supersessions kb extra region)

Reconcile the superseded set with the equality closure (supersession-map), on the write path: where a migration hands over extra (the two-arity, which examines extra and the moved classes), where a sentence leaves the store (reconcile-removed-supersession!), where a genlCx edge arrives (reconcile-context-edge), and at recover, which passes nil for the full pass. The settle calls it only for an except that moved and for an equality edge that moved in belief (settle/settle-finish).

release-lift! clj

(release-lift! kb src-handle entry gens)

Re-ask the lift of the fact at src-handle under declaration (:dh entry), or on the statement alone where that is nil (a permuting mark's): {:new [handle …]} when it is admitted now, the entry restamped under gens and the term of the conviction read now (checks/conviction-watch) when the conviction still holds, and retired when the fact or the declaration has left. An admitted lift withdraws the ledger entry its refusal filed, since the order that brought the type first would have filed none.

release-mint! clj

(release-mint! kb dh gens mintable?)

Re-ask declaration dh's waiting entry under generations gens, with mintable? answering for its types (unmintable-declaration?): {:new [handle …]} with the types its sweep minted once the type is mintable, the entry restamped when it still is not (:waits then names the types mintable? refuses), and the entry retired when the declaration has left the store.

entail-existing is the sweep a declaration arriving after its facts runs, so the mints are the ones the other arrival order made, deduplicated on content.

restrength-firings! clj

(restrength-firings! kb rh)

(restrength-firings! kb rh dropping-id)

Set the strength of every justification rule rh informs to the rule's current provers/firing-strength, in both copies: the record store's justification records (what supporting-justifications shows and what recover rebuilds the network from) and the network's (jtms/restrength-informant, which relabels the region). A rule's firing strength moves when its defeasibility resolves or an exceptWhen arrives or leaves; dropping-id is the exception meta-sentex leaving, if any.

resubsumption-seeds clj

(resubsumption-seeds kb removed removed-jids)

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 (each part's, for a cover), and for a genlCx edge the two sets visibility-seeds names — super's ancestor set and what the lower contexts see besides it. The rules with an antecedent on the edge's own relation go back too (closure-reader-rules), since what they join over is the closure rather than a fact under the edge.

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 two context sets are read at the same moment and are not sensitive to it. Removing (genlCx sub super) changes neither who reaches sub nor what super reaches, and a lower context loses only contexts reached through super, which are super's ancestor set and are subtracted from the second set; 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. An argument-type mint whose every removed justification types the departing edge itself (first antecedent, mint-informant?) is not counted: the edge was its fact, not a route it was found over, so no surviving reachability re-licenses it (edge-own-mints).

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.

retire-mint! clj

(retire-mint! kb sentex)

Take the departing sentex out of the mint family, when it is filed there.

retire-unjustified-mints! clj

(retire-unjustified-mints! kb removals)

Take out of the mint family each record a mint justification removed in removals concluded, once no other mint justification concludes it. removals is a jtms/retract!-shaped result, whose :removed-supports names each removed justification's consequence and informant, read off the network before the removal. A consequence the removal swept leaves through retire-mint!; one still in the network is retired here, and its record is the one fetch.

revived-declaration-sweeps clj

(revived-declaration-sweeps kb handles)

Run, for each sentex in handles the settle just brought back OUT ⇒ IN, the sweeps its arrival runs over the facts already stored: equate-existing and antisym-equate-existing for a merge mark, revived-edge-sweep for a genl edge under one, and lift-existing for a decontextualized_predicate. Returns one {:new :superseded :violations}, or nil when the KB declares no merge or lift mark.

A fact arriving while its mark is OUT meets a taxonomy that does not hold the mark, so its own arrival merges and lifts nothing, and nothing written later reaches it: the mark's arrival is over and the revival is a relabel, not an arrival. Without this, a mark stated, defeated, handed two facts and revived leaves them unmerged where the mark stated first or last merges them. The other direction needs no sweep: a merge or copy drawn while the mark held names the mark's sentex among its antecedents, so a defeat takes it OUT and the revival brings it back through the JTMS.

The sweeps are the arrival ones, so they read what is stored and are idempotent: a revival of a mark whose facts all arrived while it held re-derives nothing new. The handles are walked in content order. The symmetric and commuting marks are not here; a revived permuting mark re-spells its rows through chain/reconcile-spellings!.

A revived genl edge's sweep is budgeted where its arrival's is not: a settle revives an edge far more often than one arrives, and lein perf's constraint-genl-mark-descent holds a revived edge flat in the subtree past the budget.

Gated on the taxonomy holding any functional-family, anti_symmetric or decontextualized_predicate mark, so a KB declaring none pays three map reads.

subsumed-mint-blocks clj

(subsumed-mint-blocks kb moved was-in asked believed?)

The justifications to block because the records they hold up are redundant, and the records — {:blocked #{jid} :withdrawn #{handle}} over the records the sentexes in moved can have displaced.

Every justification of a withdrawn record, because a record survives on any one of them: two facts can entail the same type, and blocking one would leave the record standing on the other, so how many facts happened to entail it would decide whether it stayed.

moved is a delay over the region's records, and the gates in front of it decide whether it is ever forced: off unless the entailment is on, off unless the mint is prunable, and off while the mint family is empty. A KB holding no mint therefore fetches no record here however much it asserts, which is what record_fetch_cost_test counts. Forced, the region is filtered by shape (subsumer-shaped?) and the candidates are the mint family's (withdrawal-candidates per record, edge-route-candidates once for all the genl edges the records install), so a membership about a term holding no mint reads nothing.

Only a record that became believed is asked, which is what keeps this off the price of a settle that relabels a large region without moving much of it — a qualitative network relabels its whole network per fact and moves a handful of nodes.

The records a retraction left standing on a derivation alone (note-unpremised!) are asked too, each the whole question.

asked is the settle's own record of which of them it has already put this question to, and a record is asked once per settle however many passes relabel it. Nothing is missed by that: a mint stored after a pass examined its subsumer never reaches the store, since entail-arg-type asks the same question of every mint it is about to write. believed? is belief now, jtms/in? or own-context belief.

subsumption-seeds clj

(subsumption-seeds kb sentence)

The stored facts the genl edges sentence installs newly make matchable, as chaining seeds — the taxonomy twin of lift-existing, and there for exactly the same reason. The edges are tax/installed-edges': a (genl sub super) edge, or one per part of a cover, whose edges subsume exactly as a stated one does.

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. Gated per edge on rule-reads-above?: a fact below the edge newly reaches the terms at or above super and no other, so where no rule reads one the subtree is not read. Every functor of the subtree reaches the same terms, so the gate decides for all of its facts at once. Sound on a departing edge for negative-subsumption-seeds' reason: a firing that climbed it read a term at or above super.

A negated antecedent is answered contravariantly, so the facts an edge newly offers it sit on the other side of the edge entirely: negative-subsumption-seeds above reads them up super's genl closure.

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.

take-except-moves! clj

(take-except-moves! kb)

Empty :except-moves and return what the settle's supersession reconcile owes it: {:extra [[datum reason]] :region #{datum} :full? bool} — the supersessions except-move-sweeps found, the superseded data an except that moved can change (except-move-region), and whether a move is still pending undrained, which leaves the reconcile nothing narrower than a full pass. nil when nothing moved.

take-supersession-moves! clj

(take-supersession-moves! kb)

{:moved #{datum} :was {datum entry}}: the datums whose supersession entry changed since the last call, each with its entry before the first change (nil when it was not superseded), emptied; nil when the KB keeps no supersession moves. settle-finish reads it once per settle: a supersession moves belief with no relabel, so jtms/touched does not name these.

taxonomy-generations clj

(taxonomy-generations kb)

The genl and genlCx generations with the rebuild epoch (tax/relation-epoch), the stamp a waiting entry is decided under: a refused mint, a refused lift, and (as chain/constraint-generations) an argument conviction. settle re-asks an entry only when this moves from its stamp, so the stamp and the comparison are this one function. The epoch moves at every recover, which restarts the generations at 0.

transitive-rule-seeds clj

(transitive-rule-seeds kb rule-sentex)

The stored facts a newly forward-capable RULE needs back on the agenda when one of its antecedents reads a declared-transitive predicate — the third arrival order of transitive-seeds' three ingredients, and there for the reason the other two are.

A rule seeded on its own handle is joined over the stored facts, and that join reaches the closure only from whichever side it leads: led from the transitive antecedent it enumerates the STORED links and nothing else, since the closure is answered rather than stored and an open goal on it yields no record to lead from. So a rule arriving after its facts derives the direct pairs and stops, where the same rule arriving before them derives the closure — the same sentences, two answer sets, decided by which came last.

Seeding the partner facts fixes it the way it fixes the other two arms: each becomes a trigger, and a trigger binds the shared variable before the transitive antecedent is asked, which is the direction that reaches the closure.

Off unless an antecedent is actually declared transitive, so an ordinary rule assert pays one property lookup per antecedent and reads nothing.

transitive-seeds clj

(transitive-seeds kb sentence)

The stored facts a declared-transitive predicate's closure makes newly matchable, as chaining seeds — the TransitivePredicateProver's twin of subsumption-seeds above, and there for exactly the same reason.

A declared-transitive predicate's closure is answered, never stored. (causes E0 E2) is provable the moment both links are in and is never a record — so it is never a datum, never on the agenda, and never a trigger. A rule joined to that predicate, [(does ?a ?act) (causes ?act ?e)], can reach a closure pair only from its OTHER antecedent's trigger; and when the closure grows, nothing puts that trigger back. Assert the does before the second link and the firing has already run against a shorter closure; assert it after and the join reaches the whole of it. Same four sentences, two answer sets, which is the one thing belief may not depend on (docs/nmtms.md). subsumption-seeds states the principle for the taxonomy: firing the rules keyed on the arriving predicate is not the same thing as re-firing the rules the arrival just connected. This is that, one closure over.

Two arrival orders, because the closure has two ingredients — the links and the declaration — and either can come last. deduce-arg-types / entail-existing / entail-under-edge are the same three-cornered shape for an argument type:

• a link (pred a b), with pred already transitive: the reach that grew is a's and that of everything behind it (transitive-left-ends), so the seeds are the believed facts mentioning one of those.
• the declaration (transitive pred), over links already stored: every pair of the closure appears at once, so every believed fact on a partner functor goes back. This is the arm a (transitive …) asserted after its links needs, and without it a KB that declares its properties at the end of a file answers differently from one that declares them at the start.

The seeds are the partner triggers, not the links. Re-seeding the pred facts themselves buys nothing: their own trigger position joins the other antecedent at the term the link already names, which is the pair the run made anyway.

The gates are what keep an ordinary assert free. Both arms are off unless some rule takes a pred antecedent — with no such rule there is no join to re-drive — and the link arm reads the inverted index's posting per left end rather than any functor extent, so a KB whose transitive facts feed no rule pays two lookups and reads nothing.

The removal side needs no twin: a retracted link withdraws the closure pairs that rested on it through the justifications the firings recorded, which is the TMS's ordinary business and not a reachability question.

triggered-mints clj

(triggered-mints kb moved was-in asked believed?)

Draw what the memberships and genl edges among moved that came IN this settle trigger (trigger-entailments): {:new [handle …] :violations [v …]}. A membership (T x) arriving after a fact and an interArg or homogeneity declaration over it is the trigger's arrival order, which the fact and the declaration cannot reach because the trigger did not hold when each arrived. was-in and believed? are belief before the settle and now; asked holds the records this settle has asked.

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, restores the rule's firing strength when no guard remains (restrength-firings!), and releases the firings of a roster rule no exception convicts any more (checks/force-sentexes!).

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. up is super's ancestor set, seen what the contexts below sub see beside it, and fresh the part of up sub did not see before. The facts of fresh are seeded when seen states a rule, the facts of seen when fresh states a rule or a genl edge, the facts of up when seen states a rule and fresh a genl edge, the smaller side when only the rest of up states a rule, and the facts of up under a genl edge seen states (under-seen-edges). A fact is read under a roster antecedent fanned by genl or a licensing functor (seeds-in). The ungated arity, resubsumption-seeds' revival, seeds every such fact of up and seen. See docs/contexts.md, "A genlCx edge owes the same debt".

wff-problems clj

(wff-problems tax sentence context)

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 arg constraints.

context is the asserting (or, on the derivation path, the landing) context, passed to every arm. Every arm is a context-free structural check and ignores it.

wff-violation clj

(wff-violation kb sentence context)

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.

withdrawn-edge-seeds clj

(withdrawn-edge-seeds kb handles)

The chaining seeds a settle owes the closure edges among handles — mints it is about to withdraw as redundant (subsumed-mint-blocks), or spellings a merge retired (settle/withdraw-retired-firings!) — that a rule firing names as its witness: departed-edge-rejoin's facts and rules for each such edge and for each of its twins (handle-twins). The closure holds a retired edge's twin in place of the edge, so the re-join over the twin draws the firing the merge-first order makes.

The firing is what is owed, not the conclusion. A genl mint is withdrawn because a stated route now reaches as far as it did, so every firing that climbed it has a surviving route, and the same content loaded with the stated route first stores that firing over it. Its conclusion keeping another firing says nothing about this one, so the gate is a dependent justification whose informant is a rule, read before the sweep deletes it, and not a dependent conclusion that went OUT. Without the re-join the store keeps whichever firings the arrival order happened to draw, and a later full join — a re-join, forward-chain — draws the rest at fresh handles.

withheld-releases clj

(withheld-releases kb moved was-in asked withdrawn believed?)

The mints no longer withheld because a record that subsumed them left, and the justifications a withheld mint owes a record of its sentence that arrived: {:new [handle …]}, drawn by rederive-mints (docs/argtypes.md, "Nothing records a withheld mint").

The departures are the records note-departure! queued as they left the store, and the records in moved (a delay over the settle's region) that went IN ⇒ OUT against was-in; the arrivals are the ones that came IN. believed? is belief now. withdrawn holds the mints this settle withdrew, which release nothing. asked holds what this settle has already asked, so each record is asked once per settle however many passes relabel it. The queue is drained whether or not the gates pass.