vaelii.impl.taxonomy — com.vaelii/vaelii 0.24.0

Cached transitive closures for the two transitivity relations at the heart of common-sense reasoning:

genl relates predicates (genl dog animal) — types are its unary case genlCx relates contexts (genlCx CxA CxB) — context inheritance

Transitivity is not done with rules (too central, too hot); instead we store the direct adjacency of each relation and answer the reflexive-transitive up/down closure on demand. genls is ancestors-incl-self, specs is descendants- incl-self.

We deliberately do not materialize the full closure. A materialized closure is Θ(V²) for a deep hierarchy — a 10k-node genl chain stores ~50M pairs — so building it incrementally makes a bulk load quadratic no matter how clever each insert is: the representation itself is the cost. Storing only the O(V+E) adjacency makes a closure read O(reachable-subgraph) and an insert the adjacency write plus a depth repair — O(1) for an edge arriving parent-before-child, and proportional to the descendants of the node raise-depth lifts for one arriving child-first, so that order is quadratic in the hierarchy and *defer-depths?* is the trade written for it. Reads are memoized per closure generation (bumped on every edge change), so a shallow hierarchy — where the reachable subgraph is tiny — still answers each repeat read in O(1).

• Insertion records the edge in :fwd / :rev and, so cycle checks stay cheap, maintains a topological :depth potential (edge x→y ⇒ depth[x] > depth[y]). No closure is touched.
• Deletion drops the edge from the adjacency and prunes any node left with no edge. Depths are left as loose upper bounds — a deletion only relaxes the ordering, so the invariant survives untouched.
• Cycle safety. genl? / sees? answer reachability with an early-exit walk pruned by :depth: a real path x → … → y has strictly decreasing depth, so depth[x] ≤ depth[y] rejects the pair in O(1). wff rejects genl / genlCx cycles up front, so the closures stay acyclic; reach guards with a seen set regardless, so a stray cycle terminates rather than being subtly wrong.

closures (the from-scratch materialized build) survives as the reference implementation the on-demand reads are tested against — the oracle test in taxonomy_test compares genls / specs for every node against it after every random edit.

Context semantics: (genlCx Sub Super) means Sub sees Super's assertions, so a context K sees a sentex in context Y iff Y is in genls-of-contexts(K).

Edges are supported, and support is belief-sensitive

Every sentex that asserts an edge is a supporter, stored in the index's supporter families under the key [:genl a b] (kv/post-supporter!) with its context; a nil context means the writer had none to record (a probe) and the edge constrains everywhere. A relation is {:edges #{[a b]} :edge-ctxs {} :fwd {} :rev {} :nodes #{} :depth {} :gen n}, and :edges is the active set the closures are computed from — an edge with no believed supporter is not in it. That distinction is what keeps three things right:

• Belief. A defeated (genl dog animal) leaves the closure, so isa? cannot outrun belief. Matching is belief-sensitive everywhere in the engine, the taxonomy included; refresh-beliefs reconciles after a relabel.
• Reference counting. The same edge asserted in two contexts is two sentexes. Retracting one must not remove the edge while the other still asserts it.
• Idempotence. Re-asserting an edge that is already active is a no-op — activate returns early rather than touching the adjacency at all.

Equality is the third supported relation, and it is not a partial order

rewriteOf / sameAs / equals all feed one equivalence closure, so it is stored as a partition — member → class, class → members and representative — rather than as up/down closures. It shares the supporter discipline above, keeping its own :support map, and nothing else: insertion is a union, and deletion can split a class, which no union-find can undo, so it rebuilds the affected class from its surviving edges. See the section below and docs/equality.md.

The same belief discipline reaches the six flat caches too — disjoint, the disjoint metatypes and their members, the sibling-disjoint marks, the predicate properties, inverse, and the declared arities. Their supporters are stored in the same families under each entry's [kind key], and refresh-beliefs reconciles each cache entry against belief exactly as refresh-relation does for genl — an entry is active iff some supporter is stored and believed. So a defeated (disjoint dog cat) stops constraining, a defeated (functional P) stops merging, and a defeated (inverse P Q) stops answering the swapped goal, the way a defeated genl edge leaves the closure. See docs/taxonomy.md.

*closure-pass-cache* clj

An optional atom for the span of a read-only pass over a still taxonomy, holding the exception-filtered context down-sets (context-down) the pass reads, keyed [:genlCx :down-vis c nil], and the genl?-per-pass answers, keyed [:genl? sub super context]. The closures themselves are in the taxonomy's LRU, which a still taxonomy serves for the whole pass; a second holder here would keep alive what the LRU evicts. nil off such a pass.

*defer-cycle-scc?* clj

When true, an edge that closes a cycle marks the relation :loose? and leaves the strong-component recompute to restore-depths, instead of running repair-depths outright inside activate.

activate repairs a cycle-closing edge eagerly by default, even under *defer-depths?*: a forward firing seeded by that edge reads :scc through placement-rep before the batch settles, so a deferred :scc would place one conclusion on two members of a genlCx cycle (see activate). Recovery has no such reader. rebuild-taxonomy and the belief reconcile that follows it read :scc only through reachable?, which walks unpruned while :loose? and so answers correctly from a stale :scc; the first placement-rep read is settle, which runs after restore-depths. So recovery binds this true and pays one O(V+E) repair for the whole replay, not one per cycle-closing edge. A corpus decides how many those are, and a foreign or bulk writer, or a store replayed past the assert-time cycle checks (wff/genl-problems, wff/genlCx-problems), can leave a large strong component whose every internal edge would otherwise repair the whole relation again.

A caller that binds this must call restore-depths before any placement-rep reader runs, as vaelii.impl.recovery/recover does; a bind without that closing repair would leave :scc stale for the life of the KB.

*defer-depths?* clj

When true, an edge insert skips raise-depth and lifts only the edge's own source (local-lift), going :loose? if that breaks an edge above it; restore-depths rebuilds every depth in one pass when the batch settles.

raise-depth is proportional to the descendants of the node it lifts, which is the one thing an insert is not supposed to be: adding a hundred thousand edges in an order that repeatedly lifts high nodes re-walks their subtrees over and over, so a bulk load arriving child-first is quadratic in the hierarchy. Deferring makes the insert O(1) plus the source's in-degree, and pays one O(V+E) repair per batch.

Going loose is not free, which is why local-lift exists rather than a blanket :loose?: while loose reachable? drops its pruning, and wff runs one such walk per taxonomy edge asserted. Trading the eager repair for a blanket loose potential would only swap which arrival order is quadratic — child-first would get cheap and parent-first, the natural order for a hierarchy, would get expensive. The local lift keeps the potential sound for exactly the orders raise-depth was already cheap on, so neither order pays.

Bound by vaelii.core/with-deferred-settle, whose settle does the repair — the same bargain that scope already makes for belief.

*exposure-instance-budget* clj

How many candidate instances one bounded merge sweep will enumerate: vaelii.impl.special/equate-under-context-edge, which a genlCx edge arriving over stored facts runs, and the sweep a revived genl edge under a merge mark runs (special/revived-declaration-sweeps). A small edge can make a large, already-stored extent jointly visible, and the walk that decides whether any of it merges must not grow with the extent once it is past the cap. A sweep cut short is never silent: each caller files its own notice naming its trigger.

Where a cut can see arrival order, and why it is left there. Below the trigger level — the down-closure, the context ancestor set, the posting list of one type or predicate — nothing is sorted: the enumerations are lazy so a budgeted consumer realizes only its prefix, and sorting to choose that prefix forces the whole extent, which is the cost the cap was added to refuse.

That is measured rather than assumed. Sorting the context ancestor set took retract-context-cycle-scaling from 0.08 to 0.28 ms/op at 2048 contexts — a 3.4x growth against a 2x bound — because a context cycle makes the ancestor set the whole graph. The check exists to say a retraction is flat in the graph it is not about, and a sort is exactly what stops it being.

The residual is stated on each sweep. The cap selects a handle-ordered prefix, and a merge a sweep fails to reach is not derived by a later settle, so past the cap the order-dependence is in whether a merge is derived at all. It is bounded and reported (a :context-edge-exposure-truncated or :genl-edge-revival-truncated violation per cut), and below the cap it is exact.

Why 8192 and not 4096. The cap bounds a sweep against a large extent, and 4096 sat within 3% of what the shipped ontology plus a 200-fact generated corpus (generate_test/a-generated-kb-derives-cleanly) enumerated. A cap a mid-size KB reaches by existing truncates a normal sweep rather than refusing an unbounded one. 8192 restores the headroom.

*network-belief* clj

True while a firing's witness search reads the scoped closures (chain's placement): a supporter is read at its network label and through the except roster, and no placed defeat is read (:network-filter-active?, :network-visible?). The scope key carries the callback it reads, so the two readings never share a memo entry.

*search* clj

nil outside a second-route search (exc/route-answer), else :belief while the search answers a belief read and :visibility otherwise. A scope that reads supporter belief carries the value in its key, as the effective ancestor set does, so a walk inside a search and one outside it never share a memo entry.

*separation-frame-cache* clj

An optional atom {[a context] frame} for a read-only pass (see *closure-pass-cache*). A pass asks disjointness-test — and so separation-frame — once per membership it reads, but the frame depends on a and context alone, and the nogoods of a large KB name millions of memberships over a few thousand types, so the same [a context] frame is rebuilt once per instance of the type. Bound and dropped by the pass, which holds the taxonomy still, so the frame is gen-stable for its span; nil off such a pass.

*visible-neighbours-cache* clj

An optional atom holding a {[dir-key vis n] neighbours} map for a read-only pass (see *closure-pass-cache*). The closure memo keys whole closures per (node, vis), so a shared upper ancestor set is re-filtered under every distinct root that walks through it — the cost the closure cache structurally cannot fold and the one this one does: each node's edges are context-filtered once per pass, not once per walk. Bound and dropped by the pass, which holds the taxonomy still, so the filtered set is gen-stable for its span; nil off such a pass.

add-arity clj

(add-arity tax pred n handle)

(add-arity tax pred n handle ctx)

add-commuting clj

(add-commuting tax pred group handle)

(add-commuting tax pred group handle ctx)

Install a commutativity group on pred. group is [:rest f] or [:args [p1 p2 …]] — the two written spellings reduced to the one descriptor commuting-components reads.

add-cover clj

(add-cover tax whole parts kind handle)

(add-cover tax whole parts kind handle ctx)

add-disjoint clj

(add-disjoint tax a b handle)

(add-disjoint tax a b handle ctx)

add-equality clj

(add-equality tax a b handle preferred)

Record handle as asserting that a and b denote one thing, merging their classes. preferred names the term a rewriteOf puts on top (a, b, or nil for sameAs / equals, which deprecate nothing).

add-functional-in-arg clj

(add-functional-in-arg tax pred n handle)

(add-functional-in-arg tax pred n handle ctx)

add-genl clj

(add-genl tax sub super handle)

(add-genl tax sub super handle ctx)

add-genlCx clj

(add-genlCx tax sub super handle)

(add-genlCx tax sub super handle ctx)

add-inverse clj

(add-inverse tax p q handle)

(add-inverse tax p q handle ctx)

add-metatype-member clj

(add-metatype-member tax m t handle)

(add-metatype-member tax m t handle ctx)

add-rewrite-rule clj

(add-rewrite-rule tax handle lhs rhs context)

Cache the oriented rewrite lhs → rhs asserted by equation handle in context. Recorded in both the support map (for revival) and the active map (assumed believed on assert; a settle reconciles).

add-sib-exception clj

(add-sib-exception tax a b handle)

(add-sib-exception tax a b handle ctx)

arg-declaration-props clj

Per argument-constraint kind, the :props roster its subject is marked under — (arg parentOf 1 person) marks parentOf as declaring arg.

A declaration constrains the tuples of every predicate beneath the one it names, so reading it means asking, per super-predicate of the sentence's own functor, whether it declares anything at all. Asked of the index that is one argument-root probe per super per assert — proportional to how deep in the type hierarchy the predicate sits, on the path assert names its dominant per-fact cost. Marked here it is a set membership, which is the same trade (arity P n) takes one screen up and for the same reason: a declaration is not something to re-derive per write.

The roster is the global one, so a filter built on it is a superset of what any context can see; the scoped retrieval it gates is what decides which declarations actually speak for a reader.

Read off the declarations: the family is predicates/:argument-constraint and the keyword is each spelling's own :prop storage target, so a fifth constraint is declared once and arrives here.

asserting-contexts-among clj

(asserting-contexts-among tax ctxs)

The contexts of ctxs that state a genl edge or a flat-cache declaration, as a set: census-in over the two, with no belief callback.

asserting-contexts-in clj

(asserting-contexts-in tax rel-key ctxs)

The contexts of the set ctxs that assert a supporter of a rel-key edge, or nil when ctxs holds every context asserting one: a closure over the edges asserted in ctxs is then the global closure, and the set answers the same as ctxs does otherwise.

cache-contexts clj

(cache-contexts tax k)

The supporting contexts of flat-cache entry k ([:disjoint #{a b}], [:prop kind pred], …) — the flat-cache twin of edge-contexts.

class-fully-visible? clj

(class-fully-visible? tax term visible?)

Does visible? admit every believed supporter of every active edge in term's class? When it does, the scoped election is the global one — same members, because no edge drops, and same representative, because no preference claim drops — so the caller can take representative's O(1) map lookup instead of rebuilding the class.

The condition is per supporter, not per edge, and that is what makes it sound. One edge may carry a sameAs and a rewriteOf at once; hiding only the rewriteOf leaves the class intact and moves the head, so an edge-level test would licence the fast path on exactly the case that needs the slow one.

This is the common shape rather than an optimisation for a corner: a KB states its merges in CxCore, or in the context doing the reading, and either way every supporter is visible. A reader pays one memoized visible? per supporter of a class that is a handful of terms — against scoped-class's reachability walk and preference election, which is the cost this exists to skip.

clear-relations! clj

(clear-relations! tax)

Drop every cache and the supporter cache. recover rebuilds them from the durable store and must not merge into whatever the in-memory taxonomy already had — otherwise a stale entry outlives the data it came from.

Clearing must cover every cache, not just the two transitive relations: because recover merges into whatever it clears, a merge can only ever add, so a disjoint pair, a predicate property, an inverse or a declared arity whose sentex is gone would survive the recovery that is supposed to re-derive it. The equality partition is the same story and worse — a stale merge makes two individuals one. Clearing all of them is what makes recover a rebuild rather than a top-up. The supporters themselves are stored content in the index, which this leaves alone.

closure-memo-limit clj

How many terms, summed over the closures it holds, one taxonomy's closure cache keeps before it evicts the least recently used — the shipped default the cache profile scales and the memory guard shrinks. A closure is a persistent set, tens of bytes a term, so this is on the order of a few gigabytes. It is a bound rather than the vocabulary because a large import can hold millions of types with closures of hundreds to thousands, and an unbounded memo of every type's supertypes grows with that product.

closure-relations clj

The two relations whose transitive closure the engine caches and answers itself — genl and genlCx. They are held out of the generic :transitive prop machinery, so a (transitive genl) fact stays queryable but inert: it never routes genl to the generic closure prover, never sets has-prop? :transitive genl, and the taxonomy answers genl-transitivity from its own cache as it always has. provers/transitive-predicates and inherit/virtual-relations are both this set, and special's mark ingestion reads it as the skip-set.

Read off the declarations rather than written: :edge is the storage kind for a relation the engine closes itself, so being in this set and being cached as a closure are one fact rather than two lists that have to agree.

closures clj

(closures edges)

Compute {:edges :up :down} from scratch, for a set of [sub super] edges — the fully materialized closure this namespace deliberately does not keep.

O(V·(V+E)) — a DFS per node. This is the reference implementation: the on-demand genls / specs reads must answer exactly as it would, and the oracle test in taxonomy_test checks that node by node over random graphs.

common-descendant? clj

(common-descendant? tax ctxs)

Does any context see every member of ctxs — is the common-descendant-set non-empty? The boolean of maximal-common-descendant-contexts, for the callers that only ever ask existence (settle's nogood pairing asks it of every opposed belief pair): the maximality filter never runs, the comparable case never reads a closure, and the fallback intersection stops at the first empty.

common-descendants clj

(common-descendants tax ctxs)

Every context that sees all of ctxs — the intersection of their down closures. The set maximal-common-descendant-contexts takes the maxima of, for a caller that needs to ask something of each member rather than only where the most general ones are (clashes/exposed-clashes asks each whether it can prove a disjointness).

commuting-declared? clj

(commuting-declared? tax)

Does any predicate carry a commutativity group? The table-wide gate a caller opens on before it builds the spec closure commuting-predicates-among would be asked over.

commuting-groups clj

(commuting-groups tax pred)

The commutativity group descriptors declared of pred itself, as a set. Empty when none are, which is the answer for all but a handful of predicates.

The exact functor, and global, unlike functional-in-arg-over, which walks up. Two separate reasons, and they point the same way:

• A commutativity mark canonicalizes where the argument constraints convict. The store keys a fact by the sort every stored mark gives it (res/kb-sentex); a reader that does not believe a group reads through res/spelling-planner.
• A genl edge below a commutative predicate does not make the sub-predicate commutative, exactly as it does not make it symmetric (integrate/commute-existing, constraint_descension_test). A row re-spelled at a sub-predicate would be one the assert entry point stores the other way round on the very next write.

One map read, no closure walk, so an unmarked predicate pays a single miss — which is what lets this sit on the canonicalization path every assert runs.

commuting-predicates-among clj

(commuting-predicates-among tax specs)

The members of specs carrying any commutativity group, as a set, or nil when none do — commuting-groups mirrored for a caller holding a whole spec closure rather than one probe predicate.

Driven from the table, and in one pass. The marked predicates are a handful where a broad functor's spec closure is the whole type hierarchy, so the membership test runs the small side against the large one — props' own trade, and matches-hierarchical makes it for symmetric a few lines above the caller. Iterating the entries rather than the key set is what keeps a retrieval off an allocation: the key set would be built and thrown away once per matched literal, and on a KB carrying the CxCore bridge every symmetric predicate is in this table.

Nil rather than an empty set, so the caller's gate is a nil? and the common answer allocates nothing at all.

commuting-supporters clj

(commuting-supporters tax pred group)

The handles of the sentexes installing commuting group on pred, as a set, defeated members included — prop-supporters for the :commuting table.

context-down clj

(context-down tax c)

Contexts that inherit from c, incl c, after context-visible genlCx exceptions.

Reverse visibility has no single reader: every candidate descendant brings its own exception ancestor set. So while some except targets a genlCx supporter (relation-filter-active?), the raw candidates are filtered by each candidate's own forward answer rather than by one static reverse scope — a filtered walk per candidate, which is why the answer is memoized per context, one level beside the raw closure in the genlCx memo entry and stamped on the visibility generation: an edge change retires the entry with the rest of the relation's reads, an except arriving or leaving moves the generation, and a belief flip of a supporter moves it too (refresh-beliefs). Read from the pass cache on a read-only pass like the closures are. With no except reaching genlCx the raw closure is the answer.

context-down-global clj

(context-down-global tax c)

Contexts that inherit from c, incl c, through the active genlCx cache, with no except holes: context-down's unscoped read, for context-up-global's callers.

context-floor clj

(context-floor tax ctxs)

The most specific members of ctxs, as a set: a nil member and every member another member sees are dropped, since a reader seeing the rest sees those too. Two members that see each other count once, and the member kept is the first in printed order.

context-parents-global clj

(context-parents-global tax c)

The contexts c reaches over one active genlCx edge, with no except holes.

context-specificity clj

(context-specificity tax c)

How specific context c is, as the size of its genlCx ancestor set; 0 for a supporter with no recorded context, which is seen from everywhere. A context strictly below another has the larger ancestor set, so the number orders every comparable pair the way sees? does, and gives the incomparable ones one total order to be tie-broken in. A function of the topology alone, so no arrival order reaches it.

context-up clj

(context-up tax c)

Contexts c inherits from, incl c, after context-visible genlCx exceptions.

context-up-besides clj

(context-up-besides tax c parent usable?)

The contexts c inherits from, incl c, over every genlCx edge but c's own edge to parent and every edge usable? refuses — c's ancestor set as it stood before that edge arrived, read after it has. A walk up the adjacency under the scope context-up reads from c, asking (usable? a b) of each edge [a b] it would cross.

The caller subtracts this set from what the new edge shows, so an edge refused makes the answer smaller and the caller's set larger, never the reverse. A walk that comes back to c has found a cycle — which reaches the taxonomy through a belief race or a recovered store — whose members already see what the new edge added, and it answers #{c}.

context-up-global clj

(context-up-global tax c)

Contexts c inherits from through the active genlCx cache, with no except holes — the unscoped read, and named for it the way genls-global is.

For genlCx the scope is the except filter, so this and context-up agree on every KB where nothing excepts a genlCx supporter — which is why the two carry different names rather than one name and an option. Exception evaluation reads this non-recursive base relation to decide which exception declarations a reader can see, and that is what it is for: the filter cannot be asked to answer the question it is itself derived from. Every other caller wants context-up.

contexts clj

(contexts tax)

cover-key clj

(cover-key whole parts kind)

The support key one whole-and-parts declaration is held under: [:cover [whole parts] kind], with parts deduplicated and sorted by printed name. Sorted here rather than trusted from the sentence, so a KB whose commutativity marks are absent records the key a canonicalized one records.

cover-kinds clj

The three claims a whole-and-parts declaration can make about its roster, as the keyword each is cached under. Closed, and the two questions below are the whole of what a reader asks of one: covering says the parts leave nothing of the whole uncovered, separating says no two of them share an instance, and partition says both. Two independent claims, so the third kind is their conjunction rather than a mechanism of its own.

cover-parts clj

(cover-parts sentence)

The [whole parts] one (covering W P …), (separating W P …) or (partition W P …) sentence declares, or nil when the stored sentence is not one.

reindex replays stored sentexes rather than checked ones, so a foreign or stale store reaches the rebuild arm with a two-element row or a non-symbol part, and reading it positionally would record a cover over nil. The guard special/replay-edge applies to a taxonomy edge, applied to a roster: at least three elements, every one of them a symbol, and at least two distinct parts.

covering-kind? clj

(covering-kind? kind)

Does a declaration of this kind claim that its parts exhaust the whole?

coverings clj

(coverings tax)

Every declaration whose parts exhaust its whole, as {whole #{[parts kind]}} — the covering and partition spellings, and not separating (covering-kind?). The roster a cover refutation is convicted against (checks/cover-refutations).

covers-naming clj

(covers-naming tax part)

Every covering declaration naming part among its parts, as [whole parts kind]. Empty for every type no cover mentions, which is the lookup CoveringProver declines on — and empty for a separating roster, which claims no coverage to infer from.

covers-naming-visible clj

(covers-naming-visible tax part context)

covers-naming filtered to the declarations context can see — the scoped read a query takes, as disjoint? takes separation-frame's. An unscoped context sees every declaration, exactly as it sees every disjointness.

covers-of clj

(covers-of tax whole)

Every covering declaration over whole, as [parts kind].

covers-over clj

(covers-over tax t context)

Every declaration covering t or any of its supertypes, as [whole parts] — what a membership (t x) puts x under. Scoped: the declarations context cannot see are dropped, as they are in covers-naming-visible. context may be an ancestor set, read as disjoint? reads one.

Walks the smaller of the two sides: the covered wholes tested against t's closure, or the closure looked up in the cover table. A clash pass asks this of every membership, and a KB's covers are usually far fewer than a type's supertypes.

create-taxonomy clj

(create-taxonomy)

A KB's taxonomy: one atom holding the cached relations, plus a watch bumping observe/note-change on every write to it.

The clock is what a structure derived from the taxonomy — a qualitative constraint network reads context-up and the genl spec closure — stamps itself with. A watch rather than a bump per mutator, because there are two dozen of those and the whole point of a clock is that no write can forget it. detached-copy deliberately carries no watch: its purpose is to be mutated where nothing learns of it. The two side atoms need none either — they are caches stamped by the relation's own :gen, so neither can move an answer without the main map having moved first.

declared-arity clj

(declared-arity tax pred)

(declared-arity tax pred context)

The arity pred is declared with, or nil — anywhere, or (with context) declared from a context the reader can see.

(arity P n) is a declaration the engine interprets, so it is cached here beside transitive and inverse rather than re-queried: the arity check runs on every assertion, and answering it from the index walked 16 candidate postings per assertion — 13.3M over an OpenCyc load, nearly all of them finding nothing, and 22% of the whole load's allocation.

Nil when the KB has been told two different arities for one predicate. That is not the same as being told nothing, but the answer to "which arity does this predicate have" is genuinely unsettled, and refusing an assertion on whichever of two contradictory declarations was found first would be arbitrary — open-world is the same stance the check takes toward a predicate nobody has declared.

Scoped, that uniqueness is asked of what the reader can see rather than of the whole KB: two contexts declaring different arities leave each reader with one answer, and only a reader seeing both has none. Testing uniqueness first and filtering after would instead let a declaration a reader cannot see suppress the one it can.

defeat-moves-scoped? clj

(defeat-moves-scoped? tax)

(defeat-moves-scoped? tax slot)

May a defeat stored, removed or relabelled move a memoized scoped read: has the belief reading's filter gate (relation-filter-active?) answered true for genl under its current generation and the current visibility generation? Only then is a scoped genl closure or visible-context set memoized under a key holding that visibility generation. The genlCx gate reads no defeat. The gate itself is read again after a roster move, whose entries it compares by value. slot :filter-active-network asks the same of the network reading's gate (*network-belief*).

del-arity! clj

(del-arity! tax pred n handle)

del-commuting! clj

(del-commuting! tax pred group handle)

del-cover! clj

(del-cover! tax whole parts kind handle)

del-disjoint! clj

(del-disjoint! tax a b handle)

del-equality! clj

(del-equality! tax a b handle)

Drop handle's support for the merge of a and b. The merge survives while any other sentex still asserts it; when the last one goes the class splits back into whatever its remaining edges still connect.

del-functional-in-arg! clj

(del-functional-in-arg! tax pred n handle)

del-genl! clj

(del-genl! tax sub super handle)

del-genlCx! clj

(del-genlCx! tax sub super handle)

del-inverse! clj

(del-inverse! tax p q handle)

del-metatype-member! clj

(del-metatype-member! tax m t handle)

del-rewrite-rule! clj

(del-rewrite-rule! tax handle)

Drop equation handle's rewrite rule entirely — the last (and only) supporter is gone, so the rule leaves both maps.

del-sib-exception! clj

(del-sib-exception! tax a b handle)

deprecated? clj

(deprecated? tax term)

(deprecated? tax term visible?)

Did a believed rewriteOf name term the dispreferred side? False for a sameAs or equals member — those merge without deprecating either name.

With a visible? supporter predicate, only the rewriteOfs that reader inherits count — the same scoping representative / same-class? / equiv-class take, and necessary for the same reason: a retirement is a sentex, so a context that cannot see it has not been told, and reporting the term deprecated there would contradict the representative that same context elects for it. Read per supporter rather than off the aggregated :edge-prefs, since one edge may carry a rewriteOf and a sameAs at once and only the first deprecates.

derives-from? clj

(derives-from? tax handle)

Does handle assert something the taxonomy derives an answer from — an edge of a cached relation (genl, genlCx), or a flat-cache entry (a separation, a metatype mark and its memberships, a sibling-disjointness mark, a siblingDisjointException pair, a cover roster, a predicate property, an inverse, an arity)?

One read, of the keys handle installs (keys-of), which the reconcile reads forward and the supporter family holds. The equality partition is left out: it holds no definitional grounds a clash convicts through, and a caller asking about one is asking about genl and the flat caches.

It names a handle the taxonomy reads at all rather than the grounds of one nogood.

detached-copy clj

(detached-copy tax)

The current taxonomy state in a fresh atom, for a what-if probe: mutate the copy, read its closures, and the real taxonomy never learns any of it.

The :closure-memo must be the copy's own — it is a side atom, so copying the map alone would share it by reference, and the probe's reads would write entries stamped with the probe's bumped :gen into the live memo. Those entries are not merely wasted: the moment the live relation's gen catches up (its next real edge change), they answer real reads with closures computed over the probe's hypothetical edge — and a second probe copies the live gen, bumps to the same number, and reads them as its own. :closure-lru is a side object with the same stamp discipline, so it gets the same isolation.

:rewrite-order is stamped on the map object it sorted rather than on a number, so a probe's entry could never be mistaken for the live one's — but a shared atom would still have the two evicting each other's single slot on every alternation, and a side atom belonging to whoever reads it is the rule here rather than the exception.

:index is a fork of the original's (fork-index), so the supporters a probe posts land where only the copy reads them.

direct-genls clj

(direct-genls tax t context)

The types t is a subtype of by one genl edge of the closure — its direct parents, where genls is everything those parents in turn reach. An edge counts whatever installed it: a stated (genl t super) or a cover roster naming t as a part.

O(degree), off the :fwd adjacency the closure walk is built on, against a closure read that is O(1) only because it is memoized. The closure is what a subsumption check needs, and the parents are what a reader is shown.

direct-genls-global clj

(direct-genls-global tax t)

direct-genls through every active edge — no context scope. genls-global's reasoning: a caller holding a context wants direct-genls.

direct-specs clj

(direct-specs tax t context)

The types that are a subtype of t by one genl edge of the closure — its direct children. direct-genls' reasoning, the other direction.

direct-specs-global clj

(direct-specs-global tax t)

direct-specs through every active edge — no context scope.

disjoint-metatype? clj

(disjoint-metatype? tax m)

disjoint-metatypes clj

(disjoint-metatypes tax)

disjoint-pairs clj

(disjoint-pairs tax)

disjoint? clj

(disjoint? tax a b)

(disjoint? tax a b context)

Are types a and b provably disjoint? True when some supertype of a and some different supertype of b are separated — by a declared (disjoint x y), by both being members of one disjoint metatype, by both being non-genl-related proper specializations of one (sibling_disjoint C) parent, or by both being parts of one partition roster. Every way, disjointness is inherited downward through genl (subtypes of disjoint types are disjoint), which is what the walk over both up-closures buys.

The sibling arm is the metatype arm keyed off the genl closure rather than a recorded membership set: (sibling_disjoint C) separates C's specializations by being consulted, and its one added guard skips a separator pair x,y when one is a genl of the other — read globally, so a reader that cannot see a genl edge does not separate a pair the KB knows overlaps.

The metatype arm is why no clique is stored: (disjoint_metatype M) separates M's members by being consulted, not by materializing a (disjoint a b) per pair. Only metatypes still marked are consulted, so unmarking one releases every pair it separated in a single step. Being consulted is also what makes the arm scopable at all — a materialized clique would have frozen each pair in whatever context the expansion ran from.

The context arity scopes on three levels: the two genls closures walk only visible edges, a (disjoint x y) pair counts only when some supporter's context is visible, and the metatype arm asks the same of the mark and of each of the two memberships. Every added visibility probe sits behind an existing cheap membership guard, so the negative path — the overwhelming majority, since this runs on every unary assert — costs what the global read costs over the (smaller) scoped closures.

context may be an ancestor set instead: the closures and declarations read are those some supporter states in the set, with no belief callback (genls-asserted-in), so the read does not re-enter the supporter callback.

Monotone on the visibility of declarations and edges: seeing more of them only adds witnesses. A siblingDisjointException is the one read that removes one: the three mark arms spare the separated pair it names at a reader that sees it, so a context below the exception reads the pair apart and a context above it, or beside it, reads it separated. An unscoped read sees every exception.

disjointness-test clj

(disjointness-test tax a context)

(disjointness-test tax a context exempt?)

A predicate type -> boolean answering (disjoint? tax a <type> context) — the question with everything that depends on a and context alone read once (separation-frame). disjoint? is this asked once; checks/disjoint-problem asks it of every type the term already holds, which is the shape it exists for.

A type a no declaration reaches answers false without looking at the candidate at all; one that is separable pays a set lookup per declaration rather than a walk over the closure product.

exempt? is the siblingDisjointException read, (fn [x y]), consulted by the three mark arms over the separated pair of supertypes and never by the disjoint arm: by default the exceptions context reads (exemption); (constantly false) reads none, which answers true for every pair some reader can read separated.

disjointness-witnesses clj

(disjointness-witnesses tax a b)

Lazy seq of witness context sets for the provable disjointness of a and b: each is the supporting contexts of one complete derivation — a genl path from a up to one separated type, a path from b up to the other, and the separating declaration (a (disjoint x y) pair, a metatype mark plus both memberships, a sibling_disjoint mark plus the steps down to it, or a partition / separating roster naming both). All four spellings are here because a caller reads emptiness as not disjoint, and one left out would make that reading disagree with disjoint? about one KB. A reader sees the clash iff it sees every context in some witness; a supporter with no recorded context imposes nothing and never appears.

Lazy on every level — paths, separated pairs, and per-ingredient supporter choices can all multiply, and a node can have exponentially many ancestor paths — so a consumer that finds its witness early never pays for the tail.

No siblingDisjointException is read: an exemption removes a separation at the readers that see it, which a set of contexts to see cannot state, so a caller tests the reader it names with disjoint?. Empty exactly when no reader separates the pair, disjointness-test reading no exemption, which is the guard a caller runs first.

edge-contexts clj

(edge-contexts tax rel-key e)

The supporting contexts of active edge [a b] in relation rel-key — the believed supporters' after a settle, every supporter's between a write and the settle (the same discipline as :edges liveness). nil in the set is a supporter with no recorded context, which constrains everywhere. Empty when the edge is not active.

edge-installing-functors clj

The functors of the sentences installed-edges reads a genl edge off.

equality-edges clj

(equality-edges tax)

equality-moves? clj

(equality-moves? tax reader)

Does reader hold moved terms take-equality-moves! has not taken?

equality-partition clj

(equality-partition edges prefs)

Compute {:class :members} from scratch, given the active undirected edges and the active [preferred dispreferred] claims.

This is the reference implementation, the equality analogue of closures: the incremental union above and the class-local rebuild below must agree with it edge for edge, and the oracle test in taxonomy_test checks exactly that after every edit of a random sequence.

equality-prefs clj

(equality-prefs tax)

Every active [preferred dispreferred] claim — the directed rewriteOf graph, flattened out of the per-edge preference sets. wff walks it to reject a cycle; nothing else needs the direction, since the partition itself is undirected.

equality-supporters clj

(equality-supporters tax term)

The handles of the sentexes asserting an active equality edge incident on term — the merges that put term in a class other than its own.

Migration reads this to justify a rewritten twin: each incident edge is an independent witness for the rewrite, so the twin gets one justification per supporter and survives losing any single one.

equiv-class clj

(equiv-class tax term)

Every term known equal to term, incl. itself.

exact-arity-classes clj

What each exact-arity class membership says the arity is. The arity sentexes and these memberships derive each other through the CxCore rules, so a declared relation normally has both — but a {:chain? false} assert or a KB loaded without the rules has only what was written, so both spellings are read.

Nine spellings, because CxCore ships nine classes. unary / binary / ternary are the relation-wide ones and the other six specialize them by kind, so a KB may write the arity of a function as (binary_function F) exactly as it writes a predicate's as (binary_predicate P). The relation-wide three alone would answer membered-arity, which reads the term's whole genl closure — but the arity nogoods read a stored membership by its own functor (vaelii.impl.decide), and what a KB stored is whichever of the nine its author wrote.

The three arities never disagree across the spellings one term holds: a class and its specializations map to one number, and (disjoint unary binary) and its two peers separate the relation-wide three, which the six inherit through their genl edges.

Here, below the checks, kb/relation-arity and the provers, because all three read it; a roster read twice is a roster that drifts.

flat-contexts clj

(flat-contexts tax)

Each flat-cache entry mapped to the contexts its recorded supporters assert it from, as one value: a memo diffs two of them to find the entries a declaration stated, withdrawn or moved to another context moved, where flat-moves does not reach back.

flat-moves clj

(flat-moves tax since)

[pos moved]: the position of the journal set-cache-ctxs writes, and the flat-cache keys whose supporting contexts moved since the position since (an earlier pos), nil when the journal does not reach back that far or since is nil.

floor-covers? clj

(floor-covers? tax f1 f2)

Does a reader that sees every context of floor f2 see every context of floor f1? Answered by each member of f1 being seen from some member of f2, which is what the genlCx ancestor sets decide without enumerating readers.

functional-family-declared? clj

(functional-family-declared? tax)

Does the taxonomy carry a functional-family mark of either spelling — the global, unscoped gate every merge entry point of that family opens on, before it reads any extent?

One predicate rather than the or written at each entry point, because the two spellings store in different places (props :functional and the :functional-in-arg table) and an entry point that asks only the first is closed to the generalized mark while reporting itself as free-for-a-KB-that-declares-nothing. That is not hypothetical: it is what equate-under-edge did, so a genl edge arriving last under (functionalInArg P 2) merged nothing where the same edge under (functional P) merged — the arity-2 behaviour the generalization is not allowed to move. See functional-family-marks for the spelling roster this is the storage half of.

Two set-emptiness reads and no walk, the or short-circuiting on the commoner spelling, which is what lets it sit in front of every extent sweep.

functional-family-marks clj

The spellings of the functional mark, each with its written shape: :mark for the one-place (functional P), :mark-in-arg for the two-place (functionalInArg P n). The marked predicate is argument 1 of either, which is what lets a reader that only wants the predicate ignore the shape entirely.

One roster because the family lives in two lanes and has twice been joined to only one — the argument, with #52 and #54, is on predicates/mark-families, which is where a third spelling is now added and where this reads it back from.

What a lane still owns for itself is what it does with the shape: settle also checks the argument kinds because its triggers come off a moved region and may be malformed, where special's entry point is downstream of well-formedness and checks only the arity.

Not :props-keyed, and that is the point of the split from settle's definitional-marks: functional stores under the :functional prop where functionalInArg stores [pred n] pairs in the :functional-in-arg table, so the two have no common storage to be rostered by — only a common family and a common argument 1.

functional-in-arg-over clj

(functional-in-arg-over tax p)

(functional-in-arg-over tax p context)

[pred n] pairs — p and every super-predicate of it carrying a (functionalInArg pred n) declaration, anywhere or (with context) declared from a context the reader can see. Empty when none does.

This is props-over's shape and it walks up for props-over's reason: the constraint refuses tuples rather than licensing them, so a declaration on a super binds the sub. (functionalInArg parentOf 2) has to convict two fatherOf mothers exactly as (functional parentOf) does, or the generalization would be weaker than the arity-2 case it generalizes — which the regression half of functional-in-arg-test forbids.

Storage is arity's rather than :props': the declaration carries an integer, and a :props roster is a set of predicates with nowhere to put one. ::prop-kind is therefore not extended — arity is not in it either, and the spec is the :prop storage targets read off the declarations, which a kind derived from n has none of.

Unlike declared-arity this does not collapse to a single n. Two arities for one predicate are a genuine ambiguity about which one it has; two functional positions are two independent constraints, both of which hold, and a KB is free to say (functionalInArg P 2) and (functionalInArg P 3) of the same predicate. Visibility is asked per [pred n] entry, which is what scopes a declaration to the vantage that can see it without any machinery of its own.

functional-in-arg-predicates clj

(functional-in-arg-predicates tax)

Every predicate carrying any functionalInArg mark, at any position, as a set — the twin of props for a table keyed pred -> #{n1 n2 …} rather than membership alone, and read the same ungated way: one map read, no closure walk.

functional-in-arg-over answers a different question and cannot stand in for this one — it walks up from one probe predicate to the marks that reach it, so there is no predicate to start it from when the question is the reverse: which predicates carry the mark at all, with no probe in hand yet. special/equate-under-context-edge is exactly that caller — a genlCx edge names two contexts, not a predicate, and needs the whole marked roster to walk each one's stored extent, the same way it already reads props :functional for the arity-2 mark.

functional-in-arg-supporters clj

(functional-in-arg-supporters tax pred n)

The handles of the sentexes declaring (functionalInArg pred n), as a set.

The functionalInArg twin of prop-supporters, and it keys on the pair: a merge derived under (functionalInArg P 3) rests on the declarations naming position 3, not on every functionalInArg declaration P happens to carry. Defeated members included, for the reason prop-supporters gives.

general-reach-supports clj

(general-reach-supports tax rel-key sub super context)

Every witness for sub →* super in rel-key that context sees and no other witness covers (uncovered-routes), each the [handle ctx] of one supporter per edge along a single path. [[]] for sub = super, which rests on nothing; [] when context sees no path.

reach-support names a shortest path, and a shorter route through a specific context drags a conclusion resting on it down there while a longer route through general contexts would have left it above. Here a route is judged by the contexts it was stated in, so the route through general contexts covers the short one and is the one returned. Routes stated in contexts neither of which sees the other are each returned, since each places a dependant in a reader the other does not reach.

Ties are settled on content: the specificity of the route's most specific context, then its length, then the printed terms. Nothing keys on a handle, so two KBs holding the same edges name the same witnesses whatever order they were built in (docs/nmtms.md).

genl-asserted-in? clj

(genl-asserted-in? tax sub super ctxs)

Is sub at or below super through the active edges some supporter asserts from a context in the set ctxs, with no belief callback? Membership in genls-asserted-in's answer, walked depth-pruned (reachable-filtered?) with no closure built.

The answer is a function of the relation's edges and their supporting contexts, which :gen moves with, and of ctxs, so it is held in the closure cache under both: a reader's arity read asks it of every stored pair of related predicates, and readers whose ancestor sets assert the same genl contexts ask the same pairs. Before the walk it reads one path through every active edge (genl-path, held in the closure cache too): none is a no for every set, and one whose every edge ctxs states is a yes, so the walk runs only for a set stating part of that path.

genl-edge-supporters clj

(genl-edge-supporters tax sub super context)

The handles of the believed supporters of genl edge [sub super] a reader at context can use: each (genl sub super) sentex, and each covering, separating or partition roster that installs the edge, that genl? from context would walk the edge through. Empty when the edge is not active. Belief is read as :edge-ctxs records it, so a caller wanting the JTMS's word filters again.

genl-edges clj

(genl-edges tax)

genl? clj

(genl? tax sub super context)

Is sub a (transitive) subtype of super through the edges visible from context? genl?-global is the unscoped read.

genl?-global clj

(genl?-global tax sub super)

Is sub a (transitive) subtype of super through any active edge — no context scope. genls-global's reasoning, as a membership test.

genl?-global-held clj

(genl?-global-held tax sub super)

genl?-global, held in the closure cache under the genl generation, for a caller that asks one pair once per fact of a sweep: a pair the depth potential does not reject walks sub's ancestors on every ask (checks/mintable-type?).

genl?-per-pass clj

(genl?-per-pass tax sub super context)

genl?, walked once per [sub super context] for the span of a read-only pass that binds *closure-pass-cache*, and plain genl? off one. For a caller that asks the same pair once per instance of a type many instances share.

genlCx-edges clj

(genlCx-edges tax)

genlCx?-global clj

(genlCx?-global tax sub super)

Does context sub see context super through any active edge — no context scope. The genlCx twin of genl?-global, and sees?'s unscoped read; wff uses it to refuse a cycle, which is a property of the whole edge set.

genls clj

(genls tax t context)

Supertypes of t, incl t, through the edges visible from context (docs/contexts.md).

genls-global is the unscoped read, and it is spelled out rather than reached by dropping the argument.

genls-asserted-among clj

(genls-asserted-among tax sub among ctxs)

The terms of the set among at or above sub through the active edges some supporter asserts from a context in the set ctxs, with no belief callback: genl-asserted-in? of each, read off one walk up from sub. The walk is pruned by the depth potential at the shallowest term of among, keeping a node level with it when the node sits in a component, as reachable-filtered? keeps one level with its target, and it stops once every term of among is reached. For a caller asking one term against many above it, where a walk per pair costs the pairs times the reach.

genls-asserted-in clj

(genls-asserted-in tax t ctxs)

Supertypes of t, incl t, through the active edges some supporter asserts from a context in the set ctxs, with no belief callback. A predicate genl edge is forced monotonic, so for a predicate this is genls from a reader whose ancestor set is ctxs. It reads no belief, so a caller that must not re-enter the supporter callback (res/supporter-believed?) reads it in place of a scoped genls.

genls-global clj

(genls-global tax t)

Supertypes of t, incl t, through every active edge — no context scope.

For a caller that has no vantage to read from, or one whose answer must not depend on having one: an assert-time refusal, a re-check trigger that must over-approximate, a rebuild. A caller holding a context wants genls.

genls-global-among clj

(genls-global-among tax t among memo)

genls-global of t cut to the terms the set among holds: genls-global-union with a filter, and memo is kept for one among.

genls-global-union clj

(genls-global-union tax t xf memo)

The union of what the transducer xf makes of each term of genls-global of t, for a caller asking something small of every type above each of many: arity/recompute-arity asks which exact lengths are bound at or above every tracked functor at a rebuild. Built like the closure, from the parents' answers (reach-by-parents), but each answer holds only what xf makes, which is a few terms or none where the closure holds every ancestor, so reading it for every type costs the edges rather than the sum of the closures.

Nothing enters the closure cache. memo, a volatile map the caller makes for one xf over one still taxonomy, keeps the answers by component representative across the caller's reads. A cycle :scc has not recorded reads the closure instead.

genls-global-while clj

(genls-global-while tax t enter?)

genls-global of t cut above each type enter? refuses (closure-while), for a caller keeping a set closed upward that stops where the set already holds a type: arity/conflict-raised.

genls-global-within clj

(genls-global-within tax t limit)

genls-global of t when it holds at most limit terms, else nil — for a caller that wants the closure only when it is small, and must not pay for building a large one to find out.

genls-within clj

(genls-within tax t context limit)

genls of t from context when it holds at most limit terms, else nil: genls-global-within through the edges visible from context, which stores nothing and stops past limit.

has-prop? clj

(has-prop? tax kind pred)

(has-prop? tax kind pred context)

Does pred carry property kind — anywhere, or (with context) declared from a context the reader can see?

:symmetric and :commutative are read from every context, as the store sorts a fact stated in a context that sees no statement of the mark — one with no genlCx edge, or one above CxUniverse, where the lifted copy sits. With a context they answer whether that context believes a statement (keyed-entry-believed?), which a defeat or an except it sees takes away.

install-index! clj

(install-index! tax index)

Install the KB's index store on tax: the supporter families are posted to it and read from it, and census-in reads the contexts that state a supporter there.

install-supporter-visibility! clj

(install-supporter-visibility! tax active? visible?)

(install-supporter-visibility! tax
                               active?
                               visible?
                               network-active?
                               network-visible?
                               reaches?)

Install the KB-owned visibility callbacks on tax.

active? is the cheap whole-KB gate: nil or false while no except or placed defeat is stored, else truthy — and when truthy, the roster's entries, a seq of [key #{target-handle …}], which is what lets relation-filter-active? ask whether a supporter of the relation being read rests on a target (a bare truthy value is honoured as "every relation"). reaches? answers that, given the roster, a view of a relation's stored supporters (supporter-view) and whether the placed defeats count: they do not for genlCx, whose supporters rest only on forced-monotonic sentences, which no defeat targets. Without it a target must be a supporter itself. visible? answers whether one stored supporter handle is believed and seen from one concrete reader context. network-active? and network-visible? are the same two reads over the network and the except roster alone, with no placed defeat read: what a firing's witness search reads (*network-belief*). Taxonomy remains independent of the JTMS and exception grammar; the KB owns those facts and supplies the reads after its mutually-referential parts exist.

installed-edges clj

(installed-edges sentence)

The [sub super] pairs sentence adds to the genl closure: one for a (genl sub super) edge with a symbol sub, one per part for a covering, separating or partition declaration (special/cover-arms installs them against the declaration's handle), and none for any other sentence. A part equal to the whole gives no pair, as it installs no edge.

Every reader asking which edges a datum put into or took out of the closure reads this, so a cover's edges seed and re-join the rules an asserted edge in the same place does (docs/taxonomy.md, "A cover states the specialization it rests on").

inverse-of clj

(inverse-of tax p)

(inverse-of tax p context)

The declared inverse of p, or nil — anywhere, or (with context) declared from a context the reader can see.

One partner, chosen by content. A predicate may carry several declared inverses, and this answers the lexicographically smallest of them so the answer is a function of the knowledge rather than of the order it arrived in — the tie-break every other many-to-one read here takes, and for the reason the README gives. A caller that must see all of them asks inverses-of; this one exists for the callers that want a partner (the applicability tests, the vocabulary reports) and are not walking a graph.

inverses-of clj

(inverses-of tax p)

(inverses-of tax p context)

Every predicate declared inverse to p, as a set — anywhere, or (with context) the ones declared from a context the reader can see. Empty when none is.

Nearly every predicate has none, so a caller probing per partner does one map read and no work; the set has more than one member only where a KB declared (inverse P Q) and (inverse P R), which nothing refuses. This is the reader a step relation wants — a hop somebody recorded on any declared partner is a hop, and answering off one of them would leave the others silently off the graph.

inverses-under clj

(inverses-under tax p)

(inverses-under tax p context)

Every predicate declared inverse to p or to a sub-predicate of p, as a set — anywhere, or (with context) declared from a context the reader can see, walking only the genl edges visible from it.

A hop somebody recorded on a partner of a sub-predicate is a hop of the super too: (Q y x) under (inverse P' Q) is (P' x y), and a P' tuple is a P tuple by subsumption, however it is spelled. A step relation or a swapped-goal delegate reading only p's own partners leaves those edges silently off the graph — a claim then answers under the sub-predicate and not under its super, which no reading of genl admits.

The :inverse map is empty for nearly every KB, so the common case is one map read and no closure walk; the spec closure is consulted only when some inverse exists.

mark-disjoint-metatype clj

(mark-disjoint-metatype tax m handle)

(mark-disjoint-metatype tax m handle ctx)

mark-prop clj

(mark-prop tax kind pred handle)

(mark-prop tax kind pred handle ctx)

mark-sibling-disjoint clj

(mark-sibling-disjoint tax c handle)

(mark-sibling-disjoint tax c handle ctx)

maximal-common-descendant-contexts clj

(maximal-common-descendant-contexts tax ctxs)

The maximal elements of the common descendants of ctxs: the contexts K that see every ctx (each ctx in up(K)) — i.e. the intersection of the down closures — keeping only the most general. Returns a set: possibly empty (no common view), possibly several (incomparable maxima). Used to place a forward-derived sentex given the contexts of the rule and its antecedent facts.

Two exits ahead of the closure work, because this runs on every forward firing: a member that sees every other member is the maximum (seeing-member), and an intersection that empties part-way skips the maximality filter, whose context-up read per survivor is the expensive half on a wide lattice.

Mutually visible contexts are one maximum, not none and not two. A common ancestor only dominates k if it does not see k back; two contexts in a genlCx cycle are equally general, so each would otherwise strike the other out and the firing would have nowhere to land. They are collapsed to one by term-min — the same content-keyed choice seeing-member makes — since placing the conclusion in every member of a cycle would store one claim several times over in contexts that already see each other.

maximal-contexts clj

(maximal-contexts tax ctxs)

The maximal (most general) contexts in the supplied ctxs under the current context-visibility relation.

Unlike maximal-common-descendant-contexts, this does not manufacture a candidate set from assertion contexts. It maximizes a set a caller has already filtered by a stronger predicate — notably forward placement while visibility exceptions are active, where a sentex can be hidden at its assertion context and restored only in a descendant by a meta-exception. Mutually visible contexts are collapsed through the same stable representative used by ordinary placement.

A CxInference fan is the other caller (vaelii.impl.vantage): it has the set of readers that answered, and the readers below one that answered add no claim — a more specific context sees a superset of the same knowledge, so it answers whatever its ancestor did and for the same reasons. Reporting all of them would make the answer count a fact about how finely the KB happens to be divided rather than about the question.

meet-closure clj

(meet-closure tax ctxs)

ctxs closed under maximal-common-descendant-contexts of its pairs: every context where two or more of them meet, plus the members themselves.

The form a reader enumeration needs. Knowledge stated in several contexts is read by whoever inherits some combination of them, and which combination changes the answer — a qualitative network composes only the constraints one reader can see (docs/qcn.md), an equality election runs only over the edges one reader can see (docs/equality.md). So the parties are the fact-holding contexts and the contexts where they meet, and both callers want exactly this set.

Pairs reach every subset. A common descendant of {a b c} is a common descendant of {a b}, so it lies under some maximal one m, and under c; hence under a maximal common descendant of {m c}, which the next round adds. The closure may therefore hold a context that is maximal for no subset — harmless for both callers, since a more specific reader sees a superset of the knowledge and so either agrees with a more general one or refines it.

Fewer than two contexts closes immediately, which is every KB that has not divided the knowledge in question between contexts: there is nothing for a second to meet, so no closure is read at all.

mention-marks clj

(mention-marks tax)

The two declarations that make a position a mention — a term named as syntax rather than one the sentence refers with — as {:quoting #{…} :modal #{…}}, or nil when the KB declares neither. Nil is the gate: res/representative-term then takes the ordinary full-representative walk with no per-node check, and the sets are read once per walk rather than a taxonomy deref per compound node.

A quoting_function quotes its arguments (Quote, Quasiquote). A modal_predicate quotes the proposition it attributes to its agent: an attitude is opaque, so the merges the asker believes may not rewrite a term inside what somebody else holds true (docs/belief.md). Both are opaque to identity congruence and both follow a rewriteOf spelling rename.

Read globally, where BeliefProjectionProver reads the same :modal mark scoped from the asking context. The two questions differ: whether a belief projects is a policy of the context granting the marker, while whether an argument is a quotation is a fact about the sentence — and a reader-scoped answer to the second would migrate a stored belief for one context while holding it for another, after which neither could retrieve what the other had renamed. Same reasoning as kb-sentex's global symmetry read.

merged-term-pred clj

(merged-term-pred tax)

A term -> boolean closed over one snapshot of the partition, or nil when the closure is empty — the gate for a caller asking merged? of many terms in a row.

merged? derefs per call, which is the right shape for the single question a scoped class read asks and the wrong one for a filter running over every symbol of every match in a query's answer set. Returning nil rather than a constantly-false predicate is what lets such a caller drop the whole filter, which is what every KB that has merged nothing does.

merged? clj

(merged? tax term)

Has anything merged term at all? The O(1) gate every scoped read takes first: a KB with no equalities, and a term in none of them, never pays for scoped-class.

metatype-members clj

(metatype-members tax m)

moves-since clj

(moves-since tax rel-key gen)

The lower ends of the edges of relation rel-key whose activation or supporting contexts moved after generation gen (note-move), as a set. A closure that moved since gen is one of a node at or below one of them. A relation rebuilt from nothing (clear-relations!) restarts its generation, and its log holds only what the rebuild moved.

note-supporter-visibility-change! clj

(note-supporter-visibility-change! tax)

Invalidate context-scoped derived reads after an except's effective belief moves, or a placed defeat is stored, removed or relabelled while a scoped read may hold it (defeat-moves-scoped?).

No edge or flat-cache entry is activated/deactivated here: an except or a defeat is a hole in a reader's view, not a global retraction. The generation is carried in scoped memo keys, so the next affected read recomputes while the unscoped cache stays hot.

prop-supporter-contexts clj

(prop-supporter-contexts tax kind pred)

prop-supporters with the context each was stated in, as {handle context} — for a caller that names only the statements its reader sees.

prop-supporters clj

(prop-supporters tax kind pred)

The handles of the sentexes declaring property kind of pred, as a set — every one of them, defeated members included, which is what lets a derivation resting on one revive by itself when that supporter does.

Handles, not sentexes: the callers put these straight into a justification's antecedents, and a set has no order for such a list to inherit.

props clj

(props tax kind)

The set of predicates carrying property kind.

props-over clj

(props-over tax kind p)

(props-over tax kind p context)

p and every super-predicate of it carrying property kind — anywhere, or (with context) declared from a context the reader can see, walking only the genl edges visible from it. Empty when none does.

For the properties a violation is convicted against, and only those. A genl edge between predicates says the sub's tuples are the super's, so a clash among the sub's tuples is a clash among the super's: (fatherOf a b) beside (fatherOf b a) breaks (asymmetric parentOf), and two fatherOf mothers for one child are two parentOf values against (functional parentOf). Read the mark off the exact functor and those become bypassable through a sub-predicate entry point while the converse probe fans down the same hierarchy, so which spelling arrived second would decide whether the pair is found.

Not for the generative ones. transitive, symmetric, reflexive and transitiveInArg license tuples rather than refusing them, and a licence read for a predicate nobody declared it of manufactures knowledge — inherit-test's the-licence-stays-with-the-predicate-it-names and provers-test's the-walk-reads-hops-through-the-subsumption-fan pin that, and both call has-prop? for the goal's own predicate. The direction is what separates the two families, and it is also why this walks up where inverses-under walks down: an inverse recorded on a sub-predicate is a hop of the super, and a constraint declared of a super binds the sub.

The :props roster is empty for the kind on nearly every KB, so the common case is one map read and no closure walk — the gate inverses-under takes on the empty :inverse map, and it is what keeps a descending read off the goal paths that ask has-prop? per goal.

props-over-among clj

(props-over-among tax kind p memo)

props-over with no context, read off the kind roster's cut of p's global closure (genls-global-among) rather than the closure: memo is a volatile map the caller keeps for one roster over one still taxonomy, so a caller asking it of many predicates pays the edges once rather than a closure per predicate.

quoting-function? clj

(quoting-function? tax head)

Is head declared a quoting_function? Its arguments are a mention, held opaque to identity congruence (res/representative-term spelling mode).

reach-strength clj

(reach-strength tax rel-key sub super context supporter-class)

The defeat class of the strongest route sub →* super in rel-key that context sees — :monotonic / :default, or nil when unreachable. :monotonic for sub = super, which rests on nothing and so holds as strongly as anything can. supporter-class is the same handle → class read reach-support takes.

Derived from reach-support's widest-bottleneck path so the number and the witness can never disagree: the floor of the path it names is the strength, since each edge on it contributes its strongest supporter (docs/taxonomy.md, "Strength of a subsumption path").

reach-support clj

(reach-support tax rel-key sub super context)

(reach-support tax rel-key sub super context supporter-class)

A witness for sub →* super in relation rel-key, as the [handle ctx] of one supporter per edge along a single path — or nil when context sees no such path. Empty for sub = super, which rests on nothing. A nil context walks unscoped, which is what a caller wanting the witness before it knows its vantage asks for.

Walks the same visible adjacency the scoped closure reads do, so it finds a witness for exactly the pairs genl? answers true from that context, and the two can never disagree about what a context can reach. Neighbours are expanded in name order, so the answer is a function of the hierarchy rather than of the order it was built in.

Without supporter-class it is breadth-first — the witness is a shortest path (the fewest supports the reachability can be made to depend on), and each edge names its most general supporter (edge-supporter), the choice placement wants. This is the read the genlCx visibility walk and every unstrengthened caller take.

With supporter-class (a handle → defeat-class read) it is a widest-bottleneck path: the route whose floor — the min defeat class along it — is highest, tie-broken by depth then by the same name order. Each edge names its strongest supporter (strongest-edge-supporter), so the conclusion a firing builds over these handles is capped at the floor and no lower. Since there are exactly two classes (strength.clj), the widest floor is found by trying each class as a threshold, highest first, and taking the first shortest path made only of edges that clear it — a threshold scan that stays correct for any fixed number of classes and is two passes for two.

reach-supports clj

(reach-supports tax rel-key sub super context supporter-class)

(reach-supports tax rel-key sub super context supporter-class hidable)

Every witness for sub →* super in rel-key that context sees and no other witness covers, weighing the defeat class of each supporter (supporter-class) beside its context: a route covers another only if its floor class is at least as strong and it is seen wherever the other is. The routes a placement that has to descend below the firing's other ingredients chooses among (chain/placement-ingredients). With hidable (handle → boolean), a route resting on a supporter an except can hide covers only the routes resting on that supporter too.

refresh-beliefs clj

(refresh-beliefs tax believed?)

(refresh-beliefs tax believed? moved)

(refresh-beliefs tax believed? moved premise?)

Reconcile the cached relations with current belief: an edge (or a flat-cache entry) is active iff some sentex asserting it is believed. Called after a relabel (from settle), which is the only thing that can flip a supporter's label without adding or removing one.

Cheap in the common case — believed? is an in-memory JTMS lookup, the closures are only rebuilt if the active edge set actually moved, an equality edge whose supporters did not change label is skipped outright, and the flat caches are single-op idempotent reconciles. So a settle that defeats nothing applies no difference; what it still pays is its region. Only the equality partition and the rewrite rules decline to look at all (the gate below), while the two transitive relations and the flat caches evaluate believed-ctxs for every edge and entry the region names before finding that none of them moved. Zero work is a region naming nothing, not a belief that held still.

Every cache follows belief here — the two transitive relations, the equality partition, and the seven flat caches (disjoint, disjoint metatypes + members, the sibling-disjoint marks, the siblingDisjointException pairs, the predicate properties, inverse, the declared arities) — so a defeated declaration stops taking effect the moment settle relabels, and a revived one takes effect again.

moved is the set of handles whose belief just flipped (jtms/touched, a superset), and the caches read it two ways. The two transitive relations and the flat caches scope by it — moved-keys turns the moved handles into the keys they install, read from the supporter families, and a settle reconciles those and nothing else, which is what keeps a flip in a 100k-edge taxonomy the price of a flip.

The equality partition and the rewrite rules gate on it instead: a cache no moved handle supports is left alone, and a hit rescans it. Both hold the KB's asserted term-identity claims rather than its vocabulary, and the gate reads whichever of the two sides is smaller, so a settle that moves neither pays the size of its own region.

nil reconciles every key with a stored supporter, for a caller holding no region. recover is that caller and passes it: a settle's reconcile is scoped and gated on belief having moved, so a declaration nothing supports — OUT from the moment its node is made, opposed by nothing — has no settle event to lean on (core/recover). Every settle path names a region instead; the supersession pass widens its own by hand rather than dropping it, because a supersession flip is a belief change with no relabel to record it.

relation-epoch clj

(relation-epoch tax)

How many times clear-relations! has rebuilt tax's relations. A rebuild restarts each relation-gen at 0, so a stamp that must not compare equal across a recover carries this beside the generations (special/taxonomy-generations).

relation-gen clj

(relation-gen tax rel-key)

The generation counter of a cached relation (:genl / :genlCx), bumped on every edge change. A caller memoizing something derived from a closure reads this to notice it must recompute, without comparing edge sets — which is the whole point, since the edge set is the thing that is too big to compare.

representative clj

(representative tax term)

The term that stands for term's equivalence class — term itself when nothing has merged it.

restore-depths clj

(restore-depths tax)

Repair the depth potential of every relation a deferred batch left :loose?. Idempotent, and free when no relation is loose — which includes the common deferred batch, whose local-lift kept the potential sound throughout — so settle can call it unconditionally, and so can a caller unwinding from an aborted batch.

retirable? clj

(retirable? tax term)

Can some reader's scoped election (scoped-class) retire term? Every merged member but the representative can. The representative can when a rewriteOf names it preferred and its class holds a supporter that is not such a claim: a reader that sees that supporter and not the claim elects another member. A representative no claim names preferred is the smallest member, and every reader's election keeps it.

retire-scoped-genl! clj

(retire-scoped-genl! tax edges placement network?)

Evict the scoped genl closures that can cross one of edges (genl edges [a b]): each held under the belief reading, for a reader that sees placement (every reader when nil), of a node at or below some a (an up-closure) or at or above some b (a down-closure). The global relation decides both tests, since a scoped closure is a subset of the global one. Every other closure, and every visible-context set, stays. A defeat stored, removed or relabelled calls it with the edges its target reaches and its own context. network? also evicts the closures held under the network reading (*network-belief*), which reads no defeat: retire-genl-moves! passes it with the edges whose supporters moved in label or in justifications. Scans the closure cache once; answers how many entries went.

retire-support-moves! clj

(retire-support-moves! tax moved premise?)

Evict the scoped reads a justification added to or dropped from a stored supporter in moved can move, after a settle that flipped no label: the scoped genl closures that cross the edge of a supporter edge-moves names (retire-genl-moves!), and every scoped read keyed on the visibility generation for a genlCx one. A supporter's justifications decide where the read walk finds it believed, so a justification over no hidden handle shows an edge a defeat or except hid, and dropping one can hide it, with the edge network IN throughout. premise? is refresh-beliefs'. The supporters are read past the supporter cache, which holds nothing for this read. The caller asks scoped-reads-held? first.

rewrite-rules clj

(rewrite-rules tax)

The active oriented rewrite rules — a seq of {:handle :lhs :rhs :context} for every schematic equation currently believed. vaelii.impl.kb/rewrite-term reads these to normalize terms; the empty case is the gate that keeps normalization a no-op for a KB with no schematic equations.

Content-ordered, not insertion-ordered. Normalization tries rules in this order at each redex, so two overlapping rules that could rewrite one term must be ordered by content and not by which equation was asserted first — otherwise the normal form (and thus the stored twin) would depend on arrival order, which order-independence (docs/nmtms.md) forbids. The key is the LHS then the RHS, arbitrary but stable and handle-free, so the same rule set always yields the same normal form, confluent or not.

The key is structural, compared by nm/compare-form rather than printed. A printed key is where this ordering would leak: rewrite-active is a map keyed by handle, so a caller with an ambient *print-length* — a REPL's, typically — would elide two long left-hand sides to one prefix, collapse the key, and drop the choice between two overlapping rules back onto that map's iteration order, which is a fact about which equation was asserted first.

Sorted once per rule set, not once per call. kb/rewrite-term calls this and kb/rewrite-goal calls that, so an unmemoized sort would put a key-build-per-rule cost on every query carrying a context — a cost the empty case (no schematic equations, the KB the gate above is written for) does not have but every KB with one would pay on every read. The order is memoized in the :rewrite-order side atom, beside the main map for the reasons :closure-memo is (a read that memoizes must not contend with the writer, or mutate the snapshot a concurrent reader holds).

Stamped on the identity of the :rewrite-active map, not on a generation counter. A persistent map is its own change detector: every writer here already replaces it (add-rewrite-rule, del-rewrite-rule!, refresh-rewrite, clear-relations!) and none can replace it without producing a different object, so no writer has to remember to bump anything — the failure mode a counter has, and the one that matters most for a field three separate paths write. It is also ABA-free where a counter is not: clear-relations! installs a fresh empty map, which is a new object, whereas a counter reset to 0 would make a cleared taxonomy read as the pre-clear one (exactly why clear-relations! has to drop the gen-stamped memo by hand). The cost is a re-sort when refresh-rewrite rebuilds an equal set, which is a handful of rules.

route-exempted? clj

(route-exempted? tax {:keys [pair mark?]} context)

Does a siblingDisjointException that context reads (a context or an ancestor set) exempt the separated pair of the mark route route (separation-routes, :mark?)? False for a route through a stated disjoint and for a route with no :pair.

same-class? clj

(same-class? tax a b)

Do a and b denote the same thing?

scoped-class clj

(scoped-class tax term visible?)

[members representative] for term counting only the equality edges some supporter visible? admits — the equality analogue of the scoped closure reads, and the form a context-scoped rewrite needs.

It has to be recomputed rather than filtered out of the global partition, because dropping an edge can split a class: A~B~C with only A~B visible is the class {A B}, and its representative is elected among those two alone, not inherited from the class C was in. The election rule is class-rep's, over the visible edges' preference claims — so a rewriteOf this context cannot see neither retires a term nor promotes one.

Recomputed per call and not memoized: a class is a handful of terms, and the callers already pay a record fetch per supporter to decide visible?. The global read is representative above and stays the fast path — nothing that has not merged ever reaches here.

scoped-reads-held? clj

(scoped-reads-held? tax)

May a scoped genl or genlCx read be memoized under the filter: does either relation's filter gate (relation-filter-active?) hold an entry under the relation's current generation that is stamped, or that answered true under the current visibility generation, while an except or defeat is stored? The closure memo is read first, so a KB that never asked the gate with one stored pays no index read.

sees? clj

(sees? tax k y)

Does context k see assertions in context y?

separating-covers clj

(separating-covers tax)

Every declaration whose parts separate each other, as [whole parts kind] — the partition and separating spellings, and not covering, which claims no separation (separating-kind?). The roster separation-frame reads its parts arm off, and the fourth way this KB spells disjointness: a caller asking whether the KB separates any two types at all has to read it beside disjoint-pairs, disjoint-metatypes and sibling-disjoints.

separating-keys clj

(separating-keys tax a b context)

(separating-keys tax a b context exempt?)

The flat-cache keys of the declarations context sees that separate a from b, as a set: each [:disjoint #{x y}] pair, each disjoint metatype's [:metatype m] mark with its two [:member m _] memberships, each [:sib-disjoint c] parent and each separating cover's [:cover [whole parts] kind], over a supertype x of a and a different supertype y of b. The entries disjointness-test answers true through, under its guards, read off the same frame; empty when a and b are not disjoint at context.

exempt? is the siblingDisjointException read, as for disjointness-test: by default the pairs context reads exempted; (constantly false) names every separation stated over the pair, the marks an exception lifts included.

separating-kind? clj

(separating-kind? kind)

Does a declaration of this kind claim that no two of its parts share an instance?

separating-pairs clj

(separating-pairs tax context)

Every ordered pair [x y], x ≠ y, that a visible declaration separates — the declared pairs in both directions, plus each disjoint metatype's members against each other.

separating-partners with neither side given, and it answers the same question for the goal that gives nothing away: (disjoint ?x ?y) is specs(x) × specs(y) over these. Bounded by the declaration set by construction, which is what keeps a two-variable goal — a shape a user types by accident — from being a walk over the vocabulary squared.

separating-partners clj

(separating-partners tax a context)

The types a visible declaration separates a from: every y such that some supertype of a is declared (disjoint x y) with x ≠ y, shares a disjoint metatype with y, stands beside y as a proper specialization of one (sibling_disjoint C) parent, or stands beside y in one partition roster — the same four arms disjointness-test tests, with the same global genl-relatedness guard and the same siblingDisjointException exemptions at context on the latter three.

This is the enumeration disjointness-test is the membership test of, and the two read one frame so they cannot disagree. Every type disjoint from a is a subtype of one of these and nothing else is — disjointness is inherited downward through genl and reaches a candidate no other way — so (disjoint a ?t) is answered by specs of this set. What that buys is the bound: the answer is a function of the declarations, which are few, rather than of the vocabulary, which is not.

Belief and context are the frame's, so a retracted declaration has already left :disjoint-index / :metatype-members, and a declaration the reader's context cannot see is dropped by the same visibility predicate that decides the pair for disjoint?. The index is not itself context-scoped, which is why the filter is applied here rather than trusted to the lookup.

separation-ends clj

(separation-ends tax k)

The types a move of flat-cache entry k can change disjoint? between: a type whose global genls hold none of them reads the same separations either side of the move. The pair of a disjoint or siblingDisjointException key, a sibling_disjoint parent, a metatype's members, a member, and a cover's whole and parts. nil for a key no separation reads.

separation-moves clj

(separation-moves old new)

The types whose separations can differ between two separation-stamp values old and new, as a set: the pair of each disjoint and siblingDisjointException entry one holds and the other does not, the members of a disjoint metatype that moved and each member that moved, a sibling_disjoint parent that moved, and the parts of a partition that moved. A type whose global genls hold none of them reads the same separation of every partner under both values. A cover moving separates nothing and adds no type. Reads a roster only when the two values hold different ones, and then costs its entries.

separation-routes clj

(separation-routes tax a b)

Each way the declarations separate a from b over the unscoped closures with no siblingDisjointException read, as {:keys #{k} :links [[sub super]] :pair [x y]}: the flat-cache keys it reads (separating-keys' entries), the separated supertypes x of a and y of b, and the genl subsumptions it climbs, a to x and b to y, and for a sibling_disjoint parent c also x and y to c. A reflexive subsumption is left out. Empty exactly when disjointness-test reading no exemption answers false from a's side. A placed nogood names one route's supporters and edges as its grounds (docs/nmtms.md). A route through a mark carries :mark? true: an exception can exempt it (route-exempted?).

separation-stamp clj

(separation-stamp tax)

What a separation or a cover over two types reads of tax besides the genl closures, as one value compared with =: the separating and covering declarations with the siblingDisjointException pairs that exempt a pair from the separation marks. A declaration moving replaces its roster's value, so an unmoved stamp compares on identity. The closures that moved are moves-since's.

separation-test clj

(separation-test tax a context)

(separation-test tax a context exempt?)

disjointness-test, or nil when no declaration reaches a: a caller testing many candidates against a learns from the nil that every one answers false, and tests none. Unscoped (context nil), the test is symmetric: when a's answers b, b's answers a, so a nil for a also means no candidate's test answers a.

sib-exceptions? clj

(sib-exceptions? tax)

Is any siblingDisjointException stored?

sibling-disjoints clj

(sibling-disjoints tax)

specs clj

(specs tax t context)

Subtypes of t, incl t, through the edges visible from context. specs-global is the unscoped read.

specs-global clj

(specs-global tax t)

Subtypes of t, incl t, through every active edge — no context scope. genls-global's reasoning, the other direction.

specs-global-while clj

(specs-global-while tax t enter?)

specs-global of t cut below each type enter? refuses (closure-while), for a caller keeping a property of every subtype that a subtype holding it passes down unchanged, which stops where the property is already held: arity/spread-lengths.

specs-global-within clj

(specs-global-within tax t limit)

specs-global of t when it holds at most limit terms, else nil. genls-global-within's reasoning, the other direction.

specs-of-all clj

(specs-of-all tax nodes)

The union of specs over every node in nodes, walked once.

specs memoizes per node, which is the right shape for one question asked repeatedly and the wrong one for many questions asked together: n nodes are n closures, and where the nodes nest — a chain, which is what a batch of genl edges written by a load is — those closures sum to n²/2 elements though their union holds n. The memo cannot help, since it is keyed on the node a walk started from and every walk starts somewhere else.

So this seeds one traversal with all of them and guards with one seen, making the cost the union plus the edges under it rather than the sum of the parts. Reflexive like specs, and unscoped like its two-arity: a caller wanting the visibility filter wants specs per node and the memo that comes with it.

Deliberately not memoized. The key would be the seed set, which is a different set almost every time and would hold every predicate it ever named.

specs-within clj

(specs-within tax t context limit)

specs of t from context when it holds at most limit terms, else nil. genls-within's reasoning, the other direction.

spelling-representative clj

(spelling-representative tax term)

(spelling-representative tax term visible?)

term's representative considering only rewriteOf (spelling) edges — a sameAs / equals identity merge is not followed. This is the mention read: a quoted term tracks a spelling rename of its symbol but not a coreference merge of its referent, so res/representative-term uses it inside a quoting_function's arguments.

The rewriteOf edges form their own sub-partition; the answer is the representative of term's rewriteOf-connected component, elected by the same rule class-rep uses — a preferred term nothing deprecates, else the lexicographically smallest. A term no rewriteOf touches — including one merged only by sameAs — is its own representative, returned unchanged. With visible?, only the believed edges that reader inherits count, the scoping deprecated? / representative take. Recomputed per call: a class is a handful of terms, and the caller's merged? gate skips it entirely for an unmerged one.

stored-disjoint-metatype? clj

(stored-disjoint-metatype? tax m)

Whether some stored sentex marks m a disjoint metatype, believed or not: the supporter family under [:metatype m] counts one. This is the gate the member arms read (special/structural-integrate and its disintegrate mirror), and it is storage rather than belief by the same discipline the disjoint_metatype integrate sweep follows: a membership is a supporter, recorded whatever the mark's label, so that belief can follow it through refresh-cache-support. Gated on the believed set instead, a member asserted while the mark is defeated would never be recorded and reviving the mark would not separate it, and one retracted while the mark is defeated would leave its supporter behind for the life of the KB.

stored-disjoint-metatypes clj

(stored-disjoint-metatypes tax)

Every metatype some stored sentex marks, believed or not — the set special/post-taxonomy-supporters!' member pass walks, so a defeated mark's members are posted exactly as the live member arm posts them.

supported-edges clj

(supported-edges tax rel-key hs)

The rel-key edges [a b] the stored handles hs support, as a set.

supported-keys clj

(supported-keys tax hs)

The flat-cache keys the handles hs support, as a set.

supporter-cache-limit clj

How many entries the supporter cache (:supporters) holds, keys and handles together, before it is cleared wholesale: the shipped default the cache profile scales.

supporter-count-in clj

(supporter-count-in tax rel-key ctxs)

How many facts stating a supporter of a rel-key edge are stored in the contexts of the set ctxs, either polarity and whatever their belief: one leaf count per context stating one, per functor (census-functors). A raw taxonomy counts its recorded supporters.

supporters clj

(supporters tax k)

Taxonomy key k's stored supporters, believed or not, as {handle ctx}: k is [:genl a b], [:genlCx a b] or a flat-cache key ([:disjoint #{a b}], [:prop kind pred], …).

take-believed-again! clj

(take-believed-again! tax)

Empty and return the equality supporters refresh-equality found believed since the last call while :out held them, or nil when there are none. A supporter is in :out only after a reconcile found it disbelieved, so each of these became believed by a relabel and not by its arrival (special/believed-again-sweeps).

take-equality-moves! clj

(take-equality-moves! tax reader)

Empty reader's copy of the equality partition's moved terms and return it: every term in the class of either end of an edge a supporter joined, left, or moved in or out of belief on since reader's last call, read after the edge was applied. A term whose class, representative or scoped class moved is among them, and so is a term whose class did not move. nil when nothing moved. The one reader (equality-move-readers) is :supersessions, for special/supersession-map.

types clj

(types tax)

uncovered clj

(uncovered tax label alts)

The members of alts whose label no other member's label covers, in their given order. label maps a member to [rank floor] (rank nil where strength takes no part), or to [rank floor hid], hid the set of its handles an except can hide. Of two members that cover each other, the earlier is kept, so a caller that hands alts over in content order gets a result that is a function of the content.

uncovered-routes clj

(uncovered-routes tax start goal step)

Every route start →* goal whose label no other route's covers (covers?), as a vector of routes, each the [handle ctx] supporters along it with the goal end first. [[]] when start is goal, which rests on nothing; [] when no route exists.

step maps a node to its outgoing steps [next [handle ctx] rank hid?] in content order, one per supporter a route may name for that edge. rank is the supporter's strength rank, or nil where strength takes no part, and hid? is true when an except can hide the supporter. A route's label is its weakest rank, the floor of its supporters' contexts (context-floor) and the set of its hidable supporters. Extending a route never makes its label cover more, so the walk drops a partial route whose label a route already held at the same node covers, or one a route already found at goal covers. A node therefore holds one partial route per uncovered label, and where every edge is stated in contexts one reader sees, that is one route per node.

The queue orders by rank, then by the specificity of the floor's most specific member, then by length, then by the printed terms of the step and the printed floor. Of two routes with equal labels the walk keeps the one it pops first, so the kept route is a function of the content, and the routes come back in that order.

unmark-disjoint-metatype! clj

(unmark-disjoint-metatype! tax m handle)

Drop handle's support for the mark on m. The last supporter going forgets m (forget-metatype), and its members' supporters leave the index store with it.

unmark-prop! clj

(unmark-prop! tax kind pred handle)

unmark-sibling-disjoint! clj

(unmark-sibling-disjoint! tax c handle)

visible-ctxs clj

(visible-ctxs tax rel-key context)

up(K) ∩ ctxs for relation rel-key — the supporting contexts context can see — or nil when the scoped answer could not differ from the global one. Read on each call: the ancestor set from the closure cache, then census-among.

visible-supporters clj

(visible-supporters tax k context)

The handles of flat-cache entry k's recorded supporters a reader at context sees: each stated from a context in context's ancestor set or with no recorded context, through the except-aware check while an except is stored (scope-admits-supporter?). Every supporter for an unscoped context. Belief is the caller's filter, except where that check reads it.

with-neighbours clj

(with-neighbours nc f)

Run f with nc, an atom, as the scoped walks' neighbour cache (*visible-neighbours-cache*) when none is bound: for a caller that asks many scoped walks over a taxonomy and a belief that hold still for as long as it keeps nc.