vaelii.impl.taxonomy — com.vaelii/vaelii 0.1.0

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

genl relates unary types (genl dog animal) — the type hierarchy genlContext relates contexts (genlContext AContext BContext) — 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 an insert O(1) amortized and a closure read O(reachable-subgraph), which is what a deep or bulk load needs. 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 / genlContext 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: (genlContext 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

A relation is {:support {[a b] {handle ctx}} :edges #{[a b]} :fwd {} :rev {} :nodes #{} :depth {} :gen n}. :support records every sentex that asserts an edge, keyed by handle with the asserting sentex's context as the value — handle and context enter and leave together, so they cannot desync; a nil context means the writer had none to record (a probe) and the edge constrains everywhere. :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 :support discipline above 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 four flat caches too — disjoint, the disjoint metatypes and their members, the predicate properties, and inverse. They carry no per-claim :support record of their own; their supporters are reference-counted in the shared :cache-support map, 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.

*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.

*scoped-memo-budget* clj

How many distinct visibility sets the scoped closure memo holds per relation before the scoped level is flushed and repopulated by demand. Sized by the OpenCyc census — 445 asserting contexts induce 561 distinct vissets across its 13,196 readers — where an unbounded level on a quiescent KB served from many contexts would grow monotonically (a heap, not a wrong answer; only a :gen bump reclaims it). A flush costs what an ordinary edit's gen bump costs; a working set under the budget never flushes at all.

add-arity clj

(add-arity tax pred n handle)

(add-arity tax pred n 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-genl clj

(add-genl tax sub super handle)

(add-genl tax sub super handle ctx)

add-genlContext clj

(add-genlContext tax sub super handle)

(add-genlContext 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).

arity-declarations clj

(arity-declarations tax)

The whole pred -> #{n} declared-arity table, for a caller that needs to know whether the KB declares any arity at all, or whether the table has moved since it last looked. One map read; never walked here.

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 CoreContext, or in the microtheory 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, support and all. 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 all eight caches, 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 seven is what makes recover a rebuild rather than a top-up.

Clearing then replaying the stored declarations (defeated ones included) is deliberate: :support and :cache-support must record every asserting sentex, and the refresh-beliefs in the settle at the end of recover decides which entries are active — so a defeated (disjoint dog cat) is rebuilt into the cache and then dropped by belief, giving the same answer either side of a restart. Belief-filtering the replay instead would lose the disbelieved supporter, and clearing its defeat could never revive the entry.

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 (settle's exposure asks each whether it can prove a disjointness).

context-down clj

(context-down tax c)

Contexts that inherit from c, incl c.

context-up clj

(context-up tax c)

Contexts c inherits from, incl c.

contexts clj

(contexts tax)

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.

del-arity! clj

(del-arity! tax pred n 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-genl! clj

(del-genl! tax sub super handle)

del-genlContext! clj

(del-genlContext! 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.

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.

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. :vis-index is a side atom 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.

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 — either by a declared (disjoint x y), or by both being members of one disjoint metatype. Either way disjointness is inherited downward through genl (subtypes of disjoint types are disjoint), which is what the walk over both up-closures buys.

The metatype arm is why no clique is stored: (disjointMetatype 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.

Monotone on visibility by construction, and it must stay so: seeing more contexts can only add witnesses, never remove one. That is what lets a descendant context detect a clash its ancestors cannot while the ancestors stay clean — the whole exposure story rests on it — so no closed-world arm (no "not disjoint because I can see a reason they overlap") may ever be added here.

disjointness-test clj

(disjointness-test tax a context)

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

What survives the build is only what a can possibly be separated by: the supertypes of a that are declared disjoint from something, and the metatypes some supertype of a belongs to. Both are usually empty — most types are declared disjoint from nothing and belong to no metatype — and when they are, no candidate is looked at at all, not even to read its closure. A type that is separable pays a set lookup per declaration rather than a walk over the closure product.

One body for both readings. A nil, variable, or otherwise unscoped context gives visibility predicates that are constantly true and take no key, so the unscoped path never builds the #{x y} a visibility lookup would need — the whole reason the pair set is not what disjointness is asked of.

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, or a metatype mark plus both memberships). 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. Empty exactly when the pair is not globally disjoint, which is the cheap 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.

equality-edges clj

(equality-edges tax)

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.

genl-edges clj

(genl-edges tax)

genl? clj

(genl? tax sub super)

(genl? tax sub super context)

Is sub a (transitive) subtype of super — through every active edge, or (with context) only the edges visible from it?

genlContext-edges clj

(genlContext-edges tax)

genls clj

(genls tax t)

(genls tax t context)

Supertypes of t, incl t — through every active edge, or (with context) only the edges visible from it.

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?

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.

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)

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 genlContext 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 microtheories that already see each other.

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 shape 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 microtheories: there is nothing for a second to meet, so no closure is read at all.

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)

prop-supporters clj

(prop-supporters tax kind pred)

The sentexes declaring property kind of pred.

props clj

(props tax kind)

The set of predicates carrying property kind.

reach-support clj

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

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. Breadth-first, so the witness is a shortest path — the fewest supports the reachability can be made to depend on — and neighbours are expanded in name order, so the answer is a function of the hierarchy rather than of the order it was built in.

refresh-beliefs clj

(refresh-beliefs tax believed?)

(refresh-beliefs tax believed? moved)

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. A settle that defeats nothing therefore does no real work.

All six caches follow belief here — the two transitive relations, the equality partition, and the four flat caches (disjoint, disjoint metatypes + members, the predicate properties, inverse) — 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 cache none of them supports is left alone, so a defeat/revival/block that touches no taxonomy declaration — the common belief-moving settle — pays O(1) instead of O(vocabulary). nil reconciles every cache unconditionally: the recover path and the supersession pass, where a declaration's belief moved with no relabel to record it with no relabel to record it.

relation-gen clj

(relation-gen tax rel-key)

The generation counter of a cached relation (:genl / :genlContext), 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.

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. Sorting by the printed LHS is arbitrary but stable and handle-free, so the same rule set always yields the same normal form, confluent or not.

Sorted once per rule set, not once per call. kb/rewrite-term calls this and kb/rewrite-goal calls that, so every query carrying a context reached the pr-str-per-rule sort — a cost the empty case (no schematic equations, the KB the gate above is written for) does not have but every KB with one pays 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.

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 shape 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.

sees? clj

(sees? tax k y)

Does context k see assertions in context y?

specs clj

(specs tax t)

(specs tax t context)

Subtypes of t, incl t — through every active edge, or (with context) only the edges visible from it.

types clj

(types tax)

unmark-disjoint-metatype! clj

(unmark-disjoint-metatype! tax m handle)

unmark-prop! clj

(unmark-prop! tax kind pred 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. Interned per [genlContext-gen ctxs-gen], so repeated reads from one context share one set object (O(1) hash for the memo level keyed on it) and the intersection runs once per context per taxonomy epoch, not once per call.