vaelii.impl.taxonomy — com.vaelii/vaelii 0.31.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] (post!) 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.

*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 inside activate. A caller that binds this must call restore-depths before any placement-rep reader runs, as vaelii.impl.recovery/recover does. See docs/taxonomy.md, "Depth repair and the reconcile's arms".

*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. Bound by vaelii.core/with-deferred-settle. See docs/taxonomy.md, "What a batch does to the depth potential".

*exposure-instance-budget* clj

How many candidate instances one bounded merge sweep will enumerate: vaelii.impl.special/equate-under-context-edge and the sweep a revived genl edge under a merge mark runs (special/revived-declaration-sweeps). A sweep cut short files a :context-edge-exposure-truncated or :genl-edge-revival-truncated violation. The cap selects a handle-ordered prefix, so past it the order dependence is in whether a merge is derived at all (docs/defenses.md; docs/nmtms.md for the cap's value).

*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 stored excepts, 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.

*visible-neighbours-cache* clj

An optional atom holding a {[dir-key vis n] neighbours} map for a read-only pass over a still taxonomy, bound and dropped by the pass. It also holds the other reads a pass repeats (pass-held). nil off such a pass. See docs/taxonomy.md, "Side atoms, probe copies and symmetric entries".

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-genl-inverse clj

(add-genl-inverse tax p q handle)

(add-genl-inverse tax p q 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-meet clj

(add-meet tax f order handle)

(add-meet tax f order handle ctx)

Install (meetFunctionOf f order): f is the meet of order.

add-metatype-member clj

(add-metatype-member tax m t handle)

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

add-negates clj

(add-negates tax p q handle)

(add-negates tax p q 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 set its subject is marked under: (arg parentOf 1 person) marks parentOf as declaring arg. The set is global, so a filter built on it is a superset of what any context sees. Read off the declarations: the family is predicates/:argument-constraint and the keyword is each spelling's :prop storage target. See docs/taxonomy.md, "Predicate metadata reads".

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.

before-copy clj

(before-copy tax)

The value tax held when the open write record first recorded it, or its value now when the record holds none, in a fresh atom with side caches of its own and no watch, as detached-copy builds them: the taxonomy of kb/prior-kb, which installs its index store and callbacks.

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? Then the scoped election equals the global one, and a caller takes representative's map lookup. The test is per supporter, not per edge: hiding only the rewriteOf of an edge that a sameAs also supports keeps the class and moves the head.

class-supporters clj

(class-supporters tax term)

The supporters, believed or not, of every active edge in term's class.

clear-relations! clj

(clear-relations! tax)

Drop every cache and the supporter cache, so recover rebuilds them from the durable store and a stale entry (a disjoint pair, a property, an inverse, an arity, an equality merge) cannot outlive its sentex. The supporters are stored content in the index and stay.

clock-held clj

(clock-held tax slot k read)

(read), held in the closure memo's slot under k for one stretch of the change clock: a new clock value drops the slot's entries of the old one. Read afresh when the taxonomy holds no memo.

Public so a reader above this namespace can hold a value it derives from the taxonomy and the store for the same stretch, under a slot of its own (res/arg-constraints).

closure-memo-limit clj

The most terms, summed over the closures it holds, a taxonomy's closure cache keeps in any KB: one term per 256 bytes of the JVM's maximum heap. A closure is a persistent set: about 24 bytes a term held alone, and about 1 byte a term built on its parent's set (reach-by-parents), so the bound holds under a tenth of the heap. 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-bound scales it down to one taxonomy's size.

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. 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 (:edge storage kind).

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

common-genls clj

(common-genls tax types context)

The types that are supertypes of every member of types, through the edges visible from context: the intersection of the members' genls. Reflexive, as genls is, so a member above all the others is in the set, and one type's common genls are its genls. A set; #{} for an empty types. One memoized up-closure read per distinct member. A nil context reads every active edge, as common-genls-global does.

common-genls-global clj

(common-genls-global tax types)

common-genls through every active edge — no context scope.

common-specs clj

(common-specs tax types context)

The types that are subtypes of every member of types, through the edges visible from context: the intersection of the members' specs. Reflexive, as specs is. common-genls' reasoning, the other direction.

common-specs-global clj

(common-specs-global tax types)

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

commuting-declared? clj

(commuting-declared? tax)

Does any predicate carry a commutativity group? The table-wide presence check a caller reads before it builds the spec closure commuting-predicates-among is asked over.

commuting-groups clj

(commuting-groups tax pred)

The commutativity group descriptors declared of pred itself, as a set; empty for all but a handful of predicates. The exact functor, and global: a commutativity mark canonicalizes (res/kb-sentex, res/spelling-planner) and a genl edge below it does not make the sub-predicate commutative. One map read.

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 spec closure. Iterates the table's entries, so a miss allocates nothing.

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-children-global clj

(context-children-global tax c)

The contexts that reach c over one active genlCx edge, with no except holes: context-parents-global's reverse, an adjacency read with no closure walk.

context-down clj

(context-down tax c)

Contexts that inherit from c, including c, after context-visible genlCx exceptions. While some except targets a genlCx supporter (relation-filter-active?) the raw candidates are filtered by each candidate's own forward answer, memoized per context and reading (*network-belief*, *search*) and keyed by the change clock; otherwise 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-move clj

(context-move tax sub super except-ctxs usable?)

(context-move tax sub super except-ctxs usable? off)

What the move of the genlCx edge [sub super] (stored, removed or flipped in label) shows or hides, read from the taxonomy as it stands: the contexts some reader under sub sees through the edge and no other route. except-ctxs holds the contexts stating an except that reaches a genlCx supporter's support (exc/genlCx-except-contexts); usable? refuses an edge the walks without the edge must not cross. Keys: :raw (the global stratum), :moved (per reader class, reader-classes), :shown / :hidden, :readers, :up, and the delays :under, :seen, :below, :gained-below, :gains and :displaced (move-gains; both nil while an except reaches a genlCx supporter, and past move-gain-readers). See docs/contexts.md, "One context move".

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

(context-up-global tax c)

Contexts c inherits from through the active genlCx cache, with no except holes: the unscoped read, which exception evaluation uses. Every other caller wants context-up (docs/contexts.md).

contexts clj

(contexts tax)

contexts-seen-with-global clj

(contexts-seen-with-global tax c xs)

The contexts of xs that a context at or below c sees, through every active genlCx edge: x at or above c, at or below c, or sharing a descendant with c. The last test walks the contexts below c and those below x one step each in turn and stops when one walk ends. The walk below c is one for the call, and once it ends one walk up from its contexts answers every x, so the call costs the smaller of c's down-set and the xs' down-sets together, plus that upward walk, and never builds the larger down-set.

contrapositive-closure clj

(contrapositive-closure tax p context supporter-class)

[straight swapped]: signed-closure :up of p from context, over only the genl and genlInverse edges a reader holds at :monotonic: the predicates a negated pattern on p fans over. A genl edge's class is its strongest visible supporter's (edge-class); a genlInverse hop needs one visible supporter that supporter-class reads :monotonic (handle -> class, nil for OUT; res/holding-class). A p with no supertype answers signed-closure's set. See docs/inference.md, "Under a negation the fan reverses".

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 parts, 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-moves clj

(cover-moves old new)

The wholes of the covering declarations one of two separation-inputs values old and new holds and the other does not, as a set. Reads the cover declarations only when the two values hold different ones.

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 part list: 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 table a cover refutation is convicted against (checks/cover-problem).

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 declaration, 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.

covers-over-global-fn clj

(covers-over-global-fn tax)

(fn [t]) → covers-over of t unscoped, for a caller asking it of many types over one still taxonomy: the wholes above t are read by genls-global-among over one memo the fn holds, so a type's closure is not built, and an ancestor two types share is read once. The memo is dropped when the genl relation or the stored covers move.

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. detached-copy carries no watch. The side atoms need none (docs/taxonomy.md, "Side atoms, probe copies and symmetric entries").

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. Nil when the visible declarations give two different arities. Cached because the arity check runs on every assertion (docs/taxonomy.md, "Predicate metadata reads").

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-genl-inverse! clj

(del-genl-inverse! tax p q handle)

del-genlCx! clj

(del-genlCx! tax sub super handle)

del-inverse! clj

(del-inverse! tax p q handle)

del-meet! clj

(del-meet! tax f order handle)

del-metatype-member! clj

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

del-negates! clj

(del-negates! tax p q 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. With visible?, only the supporters that reader admits count, read per supporter, since one edge may carry a rewriteOf and a sameAs at once.

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 declaration, a predicate property, an inverse, an arity)? One read of the keys handle installs (keys-of). The equality partition is excluded.

detached-copy clj

(detached-copy tax)

The current taxonomy state in a fresh atom, for a what-if probe: mutate the copy and the real taxonomy never learns it. :closure-memo, :closure-lru and :rewrite-order are the copy's own, and :index is a fork of the original's (mount/fork-families). See docs/taxonomy.md, "Side atoms, probe copies and symmetric entries".

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 declaration 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 (genl-relatedness read globally), or by both being parts of one partition declaration. Disjointness is inherited downward through genl. The context arity scopes the two genls closures, a (disjoint x y) pair's supporters and the metatype arm's mark and memberships. context may be an ancestor set: the closures and declarations read are those some supporter states in the set, with no belief callback (genls-asserted-in). Monotone in the visibility of declarations and edges, except a siblingDisjointException, which spares its pair at a reader that sees it. An unscoped read sees every exception. See docs/taxonomy.md, "Disjointness".

disjointness-test clj

(disjointness-test tax a context)

(disjointness-test tax a context exempt?)

A predicate type -> boolean answering (disjoint? tax a <type> context) 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. A type a no declaration reaches answers false without looking at the candidate. exempt? is the siblingDisjointException read (fn [x y]), consulted by the three mark arms and never by the disjoint arm: by default the exceptions context reads (exemption); (constantly false) reads none.

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 to one separated type, a path from b to the other, and the separating declaration in any of the four spellings). A reader sees the clash iff it sees every context in some witness; a supporter with no recorded context imposes nothing. Lazy on every level. Reads no siblingDisjointException: empty exactly when no reader separates the pair, disjointness-test reading no exemption.

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.

edge-steps clj

(edge-steps tax rel-key context supporter-class hidable)

(edge-steps tax rel-key context supporter-class hidable dir-key)

step for uncovered-routes over relation rel-key as context sees it: from a node, each visible neighbour once per visible supporter of the edge that no other visible supporter covers. dir-key :fwd steps along the edges and :rev against them. With supporter-class each supporter carries its strength rank; with hidable (handle -> boolean) each supporter an except can hide is marked. Built eagerly into a vector, and a node's sorted neighbours are held for a reading pass under reach-support's key (pass-held).

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 believed sentexes asserting an active equality edge incident on term: the equalities migration reads a reader's copy's witnesses from.

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: sx/exact-arity-classes, read here by kb/relation? and the quality and integrity passes.

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 presence check every merge entry point of that family reads before it reads any extent? Two set-emptiness reads; see functional-family-marks.

functional-family-marks clj

The spellings of the functional mark, each with its written shape: :mark for (functional P), :mark-in-arg for (functionalInArg P n). The marked predicate is argument 1 of either. Read back from predicates/mark-families, where a third spelling is added. The spellings store apart (:functional prop, :functional-in-arg table), so they share a family and argument 1 and no storage.

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. props-over's shape, walking up for its reason. Storage is arity's table; ::prop-kind is not extended. Does not collapse to a single n.

functional-in-arg-predicates clj

(functional-in-arg-predicates tax)

Every predicate carrying any functionalInArg mark, at any position, as a set: one map read, no closure walk. For callers with no probe predicate (special/equate-under-context-edge).

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; [] when context sees no path. A route through general contexts covers a shorter one through a specific context, and routes whose contexts neither sees are each returned. Ties are settled on content, never a handle (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, and held in the closure cache (docs/taxonomy.md, "What the pure reads of the hierarchy promise").

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 declaration 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-inverse-free? clj

(genl-inverse-free? tax)

True when no genlInverse edge is installed — one map read, and the answer for nearly every KB. The signed closure is the plain genl closure then.

genl-inverse-key clj

(genl-inverse-key p q)

The flat-cache key a (genlInverse p q) declaration installs.

genl-path-edges clj

(genl-path-edges tax sub super)

The [a b] edges of one path of active genl edges from sub up to super (genl-path), held in the closure cache under the relation's :gen, or nil when there is none.

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.

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

(genls-among tax t context among memo)

genls of t from context cut to the set among: genls-global-among over memo, then each term genl? from context when a scope applies there, for a caller asking many terms about one among over one still taxonomy. A pass costs the genl edges above its terms once rather than a closure per term.

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)

(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. Without memo, a walk down from each term of among to t (reached-from?) answers the same cut, for a caller asking one t about a few terms: it costs the terms' descendants above t's depth, not t's ancestors, so a t deep in a chain is not walked to the top.

genls-global-meets-without? clj

(genls-global-meets-without? tax t among a b)

Does t reach a term of the set among up every active genl edge but the one from a to b? A walk up that returns at the first such term and stores nothing.

genls-global-meets? clj

(genls-global-meets? tax t among)

(genls-global-meets? tax t among missed)

Does genls-global of t hold a term among accepts, a set or a predicate? A walk up that returns at the first such term and stores nothing. missed, when given, is a volatile set kept by the caller for one among over one still taxonomy.

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 (arity/bound-above asks which predicates above a functor store a binding). memo, a volatile map the caller makes for one xf over one still taxonomy, keeps answers by component representative. Nothing enters the closure cache. A cycle :scc has not recorded reads the closure.

genls-global-union-held clj

(genls-global-union-held tax t xf held hold!)

genls-global-union of t with the answers by component representative read from (held node) and handed to (hold! node answer), for a caller keeping them past one pass in a store it retires itself: arity/entry holds them in a weighted LRU, and the ancestors a type shares with one read before are not read again. An answer held by one call is read by the next, so a call whose xf makes something else of a term replaces the answers it held under the terms that differ.

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.

grounds-stated-in clj

(grounds-stated-in tax ctxs)

The handles stated in a context of ctxs whose functor states a genl edge or a flat-cache declaration (census-functors), read per functor from the predicate extents of the installed index store; a raw taxonomy's store holds no extent, so there each context of ctxs is read whole.

grows-since clj

(grows-since tax rel-key gen)

The edges [a b] of relation rel-key that entered the active set after generation gen (note-grow), as a set, nil when the relation keeps no such log.

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?
                               sentence-of)

Install the KB-owned visibility callbacks on tax. active? is the O(1) whole-KB presence check: falsy while no except or placed defeat is stored, else truthy, and then the stored target entries, a seq of [key #{target-handle …}] (a bare truthy value means every relation). reaches? answers whether a supporter of the relation being read rests on a target, given the entries, a supporter-summary and whether placed defeats count (they do not for genlCx). visible? answers whether one stored supporter handle is believed and seen from one reader context. network-active? and network-visible? read the network and stored excepts alone (*network-belief*). sentence-of answers the sentence a supporter handle states, for most-general-of. The taxonomy stays independent of the JTMS and exception grammar.

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), none for any other sentence. A part equal to the whole gives no pair. See 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. The lexicographically smallest of several, so the answer does not depend on arrival order. inverses-of answers all of them.

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

(inverses-over tax p)

(inverses-over tax p context supporter-class)

The partners a denial of p reads: each Q an (inverse P' Q) declares for a P' at or above p. (not (Q y x)) is (not (P' x y)), and a denial of P' denies p. With context and supporter-class (contrapositive-closure's), P' ranges over the straight half of contrapositive-closure and the declaration needs a visible supporter supporter-class reads :monotonic, since a :default declaration does not contrapose. Without them, the unscoped superset over every genl edge and declaration, for a trigger.

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. One map read when the :inverse map is empty.

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)

max-common-specs clj

(max-common-specs tax types context)

The maximal strict common subtypes of types, through the edges visible from context: max-types of common-specs with the members of types removed. One distinct member is max-specs of it, exactly. min-common-genls' reasoning, the other direction.

max-common-specs-global clj

(max-common-specs-global tax types)

max-common-specs through every active edge — no context scope.

max-context-children clj

(max-context-children tax c)

The maximal contexts that inherit from c: the contexts that reach c over one genlCx edge with no other such context strictly above them. max-specs over genlCx, and min-context-parents' reverse. While some except targets a genlCx supporter (relation-filter-active?) each direct child is judged by its own min-context-parents; otherwise the raw adjacency is the answer (docs/contexts.md).

max-specs clj

(max-specs tax t context)

The maximal subtypes of t through the edges visible from context: max-types of t's direct children, the direct children with no other one strictly above them. min-genls' reasoning, the other direction. One memoized up-closure read per direct child.

max-specs-global clj

(max-specs-global tax t)

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

max-types clj

(max-types tax types context)

The maximal members of types: the members with no other member strictly above them, through the edges visible from context. min-types' reasoning, the other direction, and #{animal} in its example. max-types-global is the unscoped read.

max-types-global clj

(max-types-global tax types)

max-types through every active edge — no context scope.

maximal-common-descendant-contexts clj

(maximal-common-descendant-contexts tax ctxs)

The maximal elements of the common descendants of ctxs (the contexts K with each ctx in up(K)), as a set: possibly empty, possibly several. Places a forward-derived sentex given the contexts of the rule and its antecedent facts. Early exits: a member that sees every other (seeing-member), and an intersection that empties. Mutually visible contexts collapse to one by term-min. See docs/contexts.md.

maximal-contexts clj

(maximal-contexts tax ctxs)

The maximal (most general) contexts in the supplied ctxs under the current visibility relation, for a set the caller already filtered. Mutually visible contexts collapse through placement-rep. See docs/contexts.md.

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. Fewer than two contexts close with no read. See docs/contexts.md.

meet-orders clj

(meet-orders tax f)

The orders f is declared the meet of, as a set; empty for nearly every function. The exact functor, and global, for commuting-groups' reasons: the mark decides the stored key of an application of f, which every reader shares.

meet-supporters clj

(meet-supporters tax f order)

The handles of the sentexes stating (meetFunctionOf f order), defeated members included.

mention-marks clj

(mention-marks tax)

The two kinds of head that make a position a mention (a term named as syntax), as {:quoting #{…} :modal #{…}}, read once per walk. :quoting is sx/quoting-functors (Quote, Quasiquote); :modal is the modal_predicate marks, read globally (docs/belief.md). Both are opaque to identity congruence and follow a rewriteOf spelling rename. See docs/taxonomy.md, "Predicate metadata reads".

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, so a caller filtering every symbol of an answer set drops the filter outright for a KB that has merged nothing.

merged? clj

(merged? tax term)

Has anything merged term at all? The O(1) presence check 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)

min-common-genls clj

(min-common-genls tax types context)

The minimal strict common supertypes of types, through the edges visible from context: min-types of common-genls with the members of types removed. Every other type strictly above all the members is above one of these. For dog and cat under mammal ⊂ animal it is #{mammal}; for dog and mammal it is #{animal}, since a member is never its own answer. One distinct member is min-genls of it, exactly. A set; #{} for an empty types or for members with no common supertype above them. The cost is one memoized up-closure read per distinct member and one per common genl.

min-common-genls-global clj

(min-common-genls-global tax types)

min-common-genls through every active edge — no context scope.

min-context-parents clj

(min-context-parents tax c)

The minimal contexts c inherits from: the contexts c reaches over one genlCx edge with no other such context strictly below them. min-genls over genlCx, read as context-up reads, after the except holes c reads (relation-scope). Not reflexive. One memoized up-closure read per direct parent.

min-genls clj

(min-genls tax t context)

The minimal supertypes of t through the edges visible from context: min-types of t's direct parents, the direct parents with no other one strictly below them. Every other strict supertype of t is a supertype of one of these. A stated (genl dog animal) beside dog ⊂ mammal ⊂ animal leaves animal out. An edge counts whatever installed it, as for direct-genls. One memoized up-closure read per direct parent.

min-genls-global clj

(min-genls-global tax t)

min-genls through every active edge — no context scope.

min-types clj

(min-types tax types context)

The minimal members of types, a collection of types: the members with no other member strictly below them, through the edges visible from context. A set. (min-types tax '[dog mammal animal] c) is #{dog} where dog ⊂ mammal ⊂ animal. Members that subsume each other both stay; a member that is not a node stays. No closure is read for fewer than two distinct members. min-types-global is the unscoped read.

min-types-global clj

(min-types-global tax types)

min-types through every active edge — no context scope.

monotonic-route-witness clj

(monotonic-route-witness tax
                         {:keys [keys links pair] :as route}
                         context
                         supporter-class)

What a reader at context reads the separation route route (separation-routes) through when the route answers a denial, or nil when the reader reads no denial off it. Three conditions (docs/taxonomy.md, "A separation answers a denial"): every flat-cache key of the route has a supporter the reader sees (visible-supporters) that supporter-class reads believed, and a disjoint metatype's [:member m y] membership reads :monotonic; no siblingDisjointException the reader sees exempts the pair (route-exempted?); each subsumption the route climbs has a path whose every edge holds at :monotonic (reach-support with supporter-class). supporter-class is a live handle -> defeat-class read, nil for OUT. The witness is {:keys :pair :supports :edges}.

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.

negates-key clj

(negates-key p q)

The flat-cache key for a negates declaration between p and q, inverse-key's shape: (negates P P) keys #{P}.

negates-of clj

(negates-of tax p)

(negates-of tax p context)

Every predicate declared to negate p, as a set: anywhere, or (with context) declared from a context the reader can see.

negates-over clj

(negates-over tax q)

(negates-over tax q context)

[P R] for each predicate P at or above q and each R declared to negate P: a tuple of q is a tuple of P, so no tuple of R's spec subtree holds of its arguments. Over the unscoped closure, or (with context) the edges and declarations the reader sees. One map read on a KB with no declaration.

negates? clj

(negates? tax)

Does the taxonomy hold a negates declaration? One map read.

negating-predicates clj

(negating-predicates tax)

Every predicate a negates declaration names.

pair-separated? clj

(pair-separated? tax a b)

Does a declaration separate the type a from the type b over the unscoped closures, with no siblingDisjointException read: separation-test with no reader and no exemption, a superset over every reader, and symmetric. Held in the closure cache under the genl generation and the separation inputs, so the membership family's cover arm (membership/term-nogoods) tests a held type against a part once per value and reads a map entry after.

pass-held clj

(pass-held k read)

(read), held under k in the reading pass's neighbour cache (*visible-neighbours-cache*) when one is bound: the pass holds the taxonomy, belief and the stored records still, so k need name only what the read is asked of and the dynamic readings it depends on (*network-belief*, *search*). A nil or false answer is held as any other.

path-alternatives clj

(path-alternatives path)

The handle sets a path's per-edge supporter sets give (scoped-path-supporters): one supporter of each edge, in every combination.

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, not for the generative ones (transitive, symmetric, reflexive, transitiveInArg). See docs/taxonomy.md, "Predicate metadata reads".

props-over-among clj

(props-over-among tax kind p memo)

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

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. supporter-class is the read reach-support takes. Derived from reach-support's widest-bottleneck path (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)

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

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

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. A nil context walks unscoped. It walks the same visible adjacency as the scoped closure reads, so it finds a witness exactly for the pairs genl? answers true. Neighbours expand in name order. Without supporter-class it is breadth-first, a shortest path, each edge naming its most general supporter (edge-supporter). With supporter-class (a handle -> defeat-class read) it is a widest-bottleneck path: each defeat class is tried as a threshold, highest first, and the first shortest path whose edges all clear it is taken, each edge naming its strongest supporter (strongest-edge-supporter). thresholds names the classes tried ([:monotonic] walks no second pass; monotonic-route-witness).

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.

read-scope clj

(read-scope tax rel-key context)

The scope a read of rel-key from context walks under (relation-scope), as a key: a walk's answer is a function of the scope and not of the context, so two contexts whose scopes are equal read one answer.

refresh-beliefs clj

(refresh-beliefs tax believed?)

(refresh-beliefs tax believed? moved)

Reconcile the cached relations with current belief: an edge or flat-cache entry is active iff some sentex asserting it is believed. Called after a relabel (from settle). moved is the set of handles whose belief just flipped (jtms/touched, a superset): the two transitive relations and the flat caches scope by it (moved-keys); the equality partition and rewrite rules run a presence check (moved-touches?). nil reconciles every key with a stored supporter, for a caller holding no region (core/recover). The supersession pass widens its region by hand. See docs/taxonomy.md, "The belief reconcile is scoped to the moved region".

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

relations-match? clj

(relations-match? tax before)

Do tax's genl and genlCx relations hold the active edges and supporting contexts the taxonomy value before held, under the same rebuild epoch? Compares the edges out of each lower end moved since before's generations (moves-since), so the cost is the moved ends, not the relations.

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-stored-supporter! clj

(retire-stored-supporter! idx h)

Take stored handle h out of the supporters of every taxonomy key it installs, in index store idx alone: the index half of a declaration's departure, for a KB whose taxonomy is not built (vaelii.impl.record-edit). The taxonomy's in-memory entries are untouched. Returns the number of keys.

rewrite-rules clj

(rewrite-rules tax)

The active oriented rewrite rules: a seq of {:handle :lhs :rhs :context} for every schematic equation currently believed, which vaelii.impl.kb/rewrite-term reads to normalize terms. Empty is the presence check that keeps normalization a no-op. Content-ordered by LHS then RHS (nm/compare-form, never printed), and memoized in the :rewrite-order side atom keyed by the identity of the :rewrite-active map. See docs/equational.md, "Order independence".

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 over the equality edges some supporter visible? admits, elected by class-rep's rule over the visible preference claims. Recomputed per call rather than filtered from the global partition, since dropping an edge can split a class: A~B~C with only A~B visible is the class {A B}.

scoped-path-supporters clj

(scoped-path-supporters tax a b visible?)

The supporters of one path joining a and b over the equality edges some supporter visible? admits, as a vector holding each edge's admitted supporters in path order; nil when no such path joins them. The path is a shortest one, searched breadth-first with each term's edges in content order, so the path chosen does not depend on the order the edges arrived in.

seeing-member clj

(seeing-member tax ctxs)

The member of ctxs that sees every other member, or nil. It is a maximal common descendant; two members that see each other tie by term-min (docs/contexts.md, "Context placement of justifications").

sees? clj

(sees? tax k y)

Does context k see assertions in context y?

sentence-separation-ends clj

(sentence-separation-ends tax sentence)

The types sentence names whose subtypes' separations it moves, arriving or leaving, as a set: the lower end of each genl edge it installs (installed-edges) whose upper end is separable?, the types a stated disjoint, siblingDisjointException or sibling_disjoint mark names, the parts of a partition or separating declaration, the members of a disjoint_metatype mark, and for a membership in a disjoint metatype the type it names and the metatype's members. The sentence twin of separation-ends; taxonomy reads alone.

separable? clj

(separable? tax t)

Does a separation reach t from above: is t or one of its supertypes declared disjoint from something, a member of a disjoint metatype, a sibling-disjoint parent or a part of a partition (separable-genls)? A genl edge whose upper end answers false places its lower end under no separated type.

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 table 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. Empty when a and b are not disjoint at context. exempt? is as for disjointness-test; (constantly false) names every separation stated over the pair.

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)

(separating-partners tax a context exempt?)

The types a visible declaration separates a from: every y such that some supertype of a is declared (disjoint x y) with x not 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 declaration: the four arms of disjointness-test, with the same global genl-relatedness guard and siblingDisjointException exemptions on the latter three. Every type disjoint from a is a subtype of one of these and of nothing else, so (disjoint a ?t) is specs of this set. exempt? is as for disjointness-test.

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

The functors whose sentence moves which pairs are separated, beside a stated disjoint, a genl edge (a cover's installed ones included) and a membership in a disjoint metatype: the two separating declarations, the two marks and an exception.

separation-inputs clj

(separation-inputs 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 kind's value, so an unchanged value compares on identity. The closures that moved are moves-since's.

separation-moves clj

(separation-moves old new)

The types whose separations can differ between two separation-inputs 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 member or part set 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]}: separating-keys' entries, the separated supertypes x of a and y of b, and the genl subsumptions climbed (a to x, b to y, and for a sibling_disjoint parent c also x and y to c; a reflexive one is left out). Empty exactly when disjointness-test reading no exemption answers false from a's side. A route through a mark carries :mark? true, which an exception can exempt (route-exempted?). A placed nogood names one route as its grounds (docs/nmtms.md).

separation-routes-held clj

(separation-routes-held tax a b)

separation-routes of a and b, as a vector held in the closure cache under the genl generation and the separation inputs: the routes are read over the unscoped closures and the declarations alone, so a reader asking one pair again before either moves reads a map entry (res/separation-denials, membership/cover-routes).

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.

shrinks-since clj

(shrinks-since tax rel-key gen)

The lower ends of the edges of relation rel-key that left the active set, or whose supporting contexts moved, after generation gen (note-shrink), as a set: the ends of moves-since that did not only gain edges. A relation whose log predates the shrink log (an image written before it) reads every moved end.

sib-exceptions? clj

(sib-exceptions? tax)

Is any siblingDisjointException stored?

sibling-disjoints clj

(sibling-disjoints tax)

signed-closure clj

(signed-closure tax dir p context)

[straight swapped]: the predicates p's matching fan reaches through the genl and genlInverse edges visible from context, dir :down the specs or :up the generals. straight holds those reached over an even number of genlInverse edges, read with arguments as written; swapped those over an odd number, read with arguments 1 and 2 exchanged. With no genlInverse edge installed this is [(specs tax p context) #{}] (or genls). Otherwise a walk over [predicate parity] states, memoized in the closure memo for one stretch of the change clock.

signed-reach-support clj

(signed-reach-support tax sub super swapped? context supporter-class)

A witness for sub reaching super through the signed closure with parity swapped? — the [handle ctx] supporters of one path's genl and genlInverse edges, as reach-support names a genl path's — or nil when context sees no such path.

A pair the genl closure relates with swapped? false is reach-support's answer unchanged. Otherwise the path is the one with the fewest genlInverse edges, found breadth-first over [predicate parity] states in name order, each genl stretch of it witnessed by reach-support (widest-bottleneck under supporter-class, as there).

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-union-held clj

(specs-global-union-held tax t xf held hold!)

genls-global-union-held downward: the union of what xf makes of each term of specs-global of t, built from the children's answers, read from (held node) and handed to (hold! node answer) by component representative.

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 whose question a subtype answers for every type below it: arity/drain! stops at a subtype whose own binding gives the length a moved binding gave.

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 with one seen. Reflexive and unscoped, and not memoized (docs/taxonomy.md, "What the pure reads of the hierarchy promise").

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 over the rewriteOf edges alone, a sameAs / equals merge not followed: the mention read res/representative-term takes inside a quoted position. Elected by class-rep's rule over the rewriteOf-connected component; a term no rewriteOf touches is returned unchanged. With visible?, only the believed edges that reader admits count.

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. The presence check the member arms read (special/structural-integrate), on storage rather than belief so that belief can follow a recorded membership through refresh-cache-support.

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-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 readers (equality-move-readers) are :supersessions, for special/supersession-map, and :covers, for special/covered-merges.

types clj

(types tax)

(types tax context)

Every type currently in the genl hierarchy — the nodes of the closure, i.e. every type named by some believed genl edge. With a context, only a node touched by an edge visible from it counts: the same visibility genl? and disjoint? read, applied to every edge instead of to one pair's walk.

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; [] when no route exists. step maps a node to its outgoing steps [next [handle ctx] rank hid?] in content order, with an optional fifth element, the supporter's content key. rank is the supporter's strength rank or nil, 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 its hidable supporters; a partial route a held label covers is dropped. The queue order is total (trail-order), so the kept route is a function of content. goal is a node, or a predicate a node satisfies. See docs/inherit.md.

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: the ancestor set from the closure cache, then census-among. Memoized per context in the closure memo under the relation's generation, keyed by the change clock and the genlCx generation, as context-down-visible is: the census reads stored extents, which move only at a write.

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.