Unification, pattern matching against the indexed store, and backward chaining.
Matching is type-aware: a unary type predicate is matched over the subtype
closure, so an antecedent (animal ?x) is satisfied by a stored (dog Muffet).
This is how increasing an individual's specificity never loses the reasoning
that applied to its more general types — we consult the genl closure at match
time rather than materializing supertype facts.
Unification, pattern matching against the indexed store, and backward chaining. Matching is *type-aware*: a unary type predicate is matched over the subtype closure, so an antecedent `(animal ?x)` is satisfied by a stored `(dog Muffet)`. This is how increasing an individual's specificity never loses the reasoning that applied to its more general types — we consult the genl closure at match time rather than materializing supertype facts.
How lead-candidates narrows a NON-symmetric literal with ≥2 indexable ground
arguments: the multi-column argument-root probe. Rather than lead with the single
tightest bound column and let unify reject every candidate the other bound columns
disagree with, intersect the columns at the index so only the conjunction reaches
unify — "fewest unifications".
Every choice is a pure cost decision, like *hierarchical-retrieval*: the result
is a subset of the single leading column and still a superset of the true matches
(each match holds every bound term at its position), so unify and the context filter
run over fewer candidates and the answer set is identical. A symmetric literal is
left on the mirror-widened single-column path — intersecting its forward columns would
drop the mirror-stored matches — as is a literal with fewer than two ground columns
(the belief-settle diet), so those paths take the single-column lead unchanged.
:two intersect the two lowest-count-with-arg ground columns (default)
:all intersect every indexable ground column
:gated :two, but only when the leading column is a wasteful superset — its agnostic
count exceeds *arg-intersect-floor*; below that a single unify sweep is
cheaper than allocating an intersection set
:off the pre-v3 single leading column, no intersection
Chosen by measurement (lein bench-argindex join); bind it to compare.
How `lead-candidates` narrows a NON-symmetric literal with **≥2 indexable ground
arguments**: the multi-column argument-root probe. Rather than lead with the single
tightest bound column and let `unify` reject every candidate the other bound columns
disagree with, intersect the columns at the index so only the conjunction reaches
`unify` — "fewest unifications".
Every choice is a **pure cost decision**, like `*hierarchical-retrieval*`: the result
is a subset of the single leading column and still a *superset* of the true matches
(each match holds every bound term at its position), so `unify` and the context filter
run over fewer candidates and the answer *set* is identical. A symmetric literal is
left on the mirror-widened single-column path — intersecting its forward columns would
drop the mirror-stored matches — as is a literal with fewer than two ground columns
(the belief-settle diet), so those paths take the single-column lead unchanged.
:two intersect the two lowest-`count-with-arg` ground columns (default)
:all intersect every indexable ground column
:gated :two, but only when the leading column is a wasteful superset — its agnostic
count exceeds `*arg-intersect-floor*`; below that a single `unify` sweep is
cheaper than allocating an intersection set
:off the pre-v3 single leading column, no intersection
Chosen by measurement (`lein bench-argindex join`); bind it to compare.The :gated strategy's floor: skip the intersection when the leading (tightest)
column already returns no more than this many handles, where feeding that short
superset straight to unify costs less than allocating an intersection set.
The `:gated` strategy's floor: skip the intersection when the leading (tightest) column already returns no more than this many handles, where feeding that short superset straight to `unify` costs less than allocating an intersection set.
Whether match-one may retrieve its candidate handles from a secondary argument
root instead of always walking the trie.
The trie narrows strictly left to right, so a pattern whose first argument is a
variable but a later argument is a ground term — (parentOf ?x Tom), the second
half of a grandparent join — cannot be answered by a prefix: the trie fans out over
every first-argument value (one lookup per node) only to keep the few
that match the later token. The argument-root node [pred pos term] indexes exactly
that later position under the pattern's own predicate, so it answers the same pattern
with one read per context the node lists (one, for a ground pattern context).
When several arguments are known, candidate-handles intersects the pattern's
scoped argument roots (sentexes-with-args — the scoping means a named functor
needs no predicate-extent intersection), so knowing more of the sentence narrows on all
of it at once instead of one column.
The set it returns is a superset of the trie's hits — match-one's existing
unify filters it to the identical result (the trie's own hit set is the
unifiable set, and the roots' intersection ⊇ that). So this changes only how the
candidates are fetched, never which sentexes match. Binding it false forces the
trie, which is what arg_root_retrieval_test compares against. True by default — a
strict improvement on the after-a-variable case and a no-op everywhere else.
Whether `match-one` may retrieve its candidate handles from a **secondary argument root** instead of always walking the trie. The trie narrows strictly left to right, so a pattern whose *first* argument is a variable but a later argument is a ground term — `(parentOf ?x Tom)`, the second half of a grandparent join — cannot be answered by a prefix: the trie fans out over every first-argument value (one lookup per node) only to keep the few that match the later token. The argument-root node `[pred pos term]` indexes exactly that later position under the pattern's own predicate, so it answers the same pattern with one read per context the node lists (one, for a ground pattern context). When several arguments are known, `candidate-handles` intersects the pattern's scoped argument roots (`sentexes-with-args` — the scoping means a named functor needs no predicate-extent intersection), so knowing more of the sentence narrows on all of it at once instead of one column. The set it returns is a **superset** of the trie's hits — `match-one`'s existing `unify` filters it to the identical result (the trie's own hit set *is* the unifiable set, and the roots' intersection ⊇ that). So this changes only *how* the candidates are fetched, never *which* sentexes match. Binding it false forces the trie, which is what `arg_root_retrieval_test` compares against. True by default — a strict improvement on the after-a-variable case and a no-op everywhere else.
Read the store as stored rather than as believed — CxEverything, and nothing
else.
This is a named opt-out of the fourth invariant ("a stored sentex is not a believed one", README.md), which is why it is a dynamic var scoped to one read by the entry point that resolves the symbol, and not an option any caller can set. It gives a syntactic query: unification against the store with no JTMS read at all, which is both the cheapest question the engine can be asked and the only one that can see a defeated default.
What it does not license is a belief claim. An answer taken under this flag is not
a justification and must not reach why or read as one — provable? under
CxEverything says a derivation is spelled in the store, not that the KB holds it.
Read the store as **stored** rather than as believed — `CxEverything`, and nothing
else.
This is a named opt-out of the fourth invariant ("a stored sentex is not a believed
one", README.md), which is why it is a dynamic var scoped to one read by the entry point that
resolves the symbol, and not an option any caller can set. It gives a
*syntactic* query: unification against the store with no JTMS read at all, which is both
the cheapest question the engine can be asked and the only one that can see a defeated
default.
What it does **not** license is a belief claim. An answer taken under this flag is not
a justification and must not reach `why` or read as one — `provable?` under
`CxEverything` says a derivation is *spelled* in the store, not that the KB holds it.An optional observer of the DFS's dead ends — (fn [goal depth]) — or nil, the
default.
A dead end is a subgoal, substituted under the frame's bindings, that no visible
believed fact and no rule consequent unified with. A branch cut short — by the
per-path loop guard, :max-depth or the term-growth ceiling
(default-max-term-growth) — is not reported. The return value is ignored, so an
observed run takes the same path as an unobserved one. Only prove's loop reports;
the lazy backward does not. nil costs one var deref per expanded goal.
docs/abduction.md, "The dead end", gives the reasons.
An optional observer of the DFS's **dead ends** — `(fn [goal depth])` — or nil, the default. A dead end is a subgoal, substituted under the frame's bindings, that no visible believed fact and no rule consequent unified with. A branch **cut short** — by the per-path loop guard, `:max-depth` or the term-growth ceiling (`default-max-term-growth`) — is not reported. The return value is ignored, so an observed run takes the same path as an unobserved one. Only `prove`'s loop reports; the lazy `backward` does not. nil costs one var deref per expanded goal. docs/abduction.md, "The dead end", gives the reasons.
Answer a context-scoped (p a ?x) query with the set-algebra retrieval below
(lead with the argument root, filter the predicate/context hierarchies in memory)
rather than the nested |context-up| × |specs| matches-visible fan-out.
On by default: the set-algebra path is lazy (lead-candidates), so it
short-circuits an existence check like the fan-out does while collapsing the
fan-out's product to a scoped argument-root lookup per sub-predicate — strictly
cheaper, and flat where the fan-out is O(context-hierarchy depth). Like plan/*enabled*, this is a pure cost decision that must
never change the answer set; bind it false to run the reference fan-out, which
is what matches_hierarchical_test compares against over patterns from the starter's
own facts.
Answer a context-scoped `(p a ?x)` query with the set-algebra retrieval below (lead with the argument root, filter the predicate/context hierarchies in memory) rather than the nested `|context-up| × |specs|` `matches-visible` fan-out. On by default: the set-algebra path is lazy (`lead-candidates`), so it short-circuits an existence check like the fan-out does while collapsing the fan-out's product to a scoped argument-root lookup per sub-predicate — strictly cheaper, and flat where the fan-out is O(context-hierarchy depth). Like `plan/*enabled*`, this is a pure cost decision that must never change the answer *set*; bind it **false** to run the reference fan-out, which is what `matches_hierarchical_test` compares against over patterns from the starter's own facts.
For a non-symmetric literal with a spec closure in hand, which side of the two
equivalent argument reads lead-candidates leads from — and the last cost decision in
this namespace to lack a knob.
A scoped literal's candidates can be read two ways, and each is a superset
matches-hierarchical's jtms/in?/unify filters reduce to the identical set (like
*arg-intersect*, a pure cost decision that must never change the answer):
:scoped one predicate-scoped node per sub-predicate ([pd pos term]). Exactly this literal's predicates, O(|specs|) index probes — the
pre-v4 lead, and the reference matches_hierarchical_test forces to compare.
:agnostic the slot roster ([:argument-slot pos term], every functor holding term
at pos), kept to specs, then the node of each kept functor. One
roster probe and one node read per kept functor.
:auto (default) :agnostic when the term holds no more postings at this position
than there are specs, else :scoped — read whichever side is smaller. The
choice is content-derived (count-with-arg vs a realised count, both
O(1)), so it is order-independent and free; ≤ ties to the one-probe read.
:auto is the whole of the cold-rebuild clash win: the queried type sits high and its
subtree spans the KB, while the term holds a handful of memberships, so :scoped's
O(|hierarchy|) probes collapse to one. checks/membership-handles reads this too —
:scoped runs its matches-visible reference, any other value leads from the term.
For a **non-symmetric** literal with a spec closure in hand, which side of the two
equivalent argument reads `lead-candidates` leads from — and the last cost decision in
this namespace to lack a knob.
A scoped literal's candidates can be read two ways, and each is a *superset*
`matches-hierarchical`'s `jtms/in?`/`unify` filters reduce to the identical set (like
`*arg-intersect*`, a pure cost decision that must never change the answer):
:scoped one predicate-scoped node per sub-predicate (`[pd pos term]`). Exactly this literal's predicates, O(|specs|) index probes — the
pre-v4 lead, and the reference `matches_hierarchical_test` forces to compare.
:agnostic the slot roster (`[:argument-slot pos term]`, every functor holding `term`
at `pos`), kept to `specs`, then the node of each kept functor. One
roster probe and one node read per kept functor.
:auto (default) `:agnostic` when the term holds no more postings at this position
than there are specs, else `:scoped` — read whichever side is smaller. The
choice is content-derived (`count-with-arg` vs a realised `count`, both
O(1)), so it is order-independent and free; `≤` ties to the one-probe read.
`:auto` is the whole of the cold-rebuild clash win: the queried type sits high and its
subtree spans the KB, while the term holds a handful of memberships, so `:scoped`'s
O(|hierarchy|) probes collapse to one. `checks/membership-handles` reads this too —
`:scoped` runs its `matches-visible` reference, any other value leads from the term.Candidate handles per prefetch hint a retrieval path gives its record store, or
false to give it none. false is the default, and it is the code that was here
before: no chunking, no hint, one get-sentex per candidate that survives the belief
filter.
Turned on, a walk takes its candidates a chunk at a time and tells the store which
handles the chunk is about to ask for, so a store that can answer many at one cost
(protocols/Prefetching) may do that instead of being asked one at a time. Nothing
about the result moves: the hint returns nothing and every record still arrives through
get-sentex, so this is a cost setting and never a semantic one.
It is off because it is only ever worth it over a fetch that is not local. On the
RAM and disk record stores no store implements the capability, so the hint would have
nobody to give it to; over a networked store it is worth it exactly when the candidates
are not already cached, which the store itself checks — so turning this on hands the
decision to the party that can make it, rather than making it here. The evidence that
says to turn it on is a :fetches tally (vaelii.impl.profile) large against a query's
wall clock on a corpus whose working set does not fit that store's cache.
The chunk is the unit of over-fetch: a consumer that takes one solution and stops has hinted at most this many handles, so a large chunk amortizes better and wastes more.
false or a positive integer, and anything else is refused where it is bound —
true above all, which is what a var with an off-value of false invites and which is
truthy enough to reach the chunk arithmetic before it fails.
Candidate handles per **prefetch hint** a retrieval path gives its record store, or `false` to give it none. `false` is the default, and it is the code that was here before: no chunking, no hint, one `get-sentex` per candidate that survives the belief filter. Turned on, a walk takes its candidates a chunk at a time and tells the store which handles the chunk is about to ask for, so a store that can answer many at one cost (`protocols/Prefetching`) may do that instead of being asked one at a time. Nothing about the result moves: the hint returns nothing and every record still arrives through `get-sentex`, so this is a cost setting and never a semantic one. **It is off because it is only ever worth it over a fetch that is not local.** On the RAM and disk record stores no store implements the capability, so the hint would have nobody to give it to; over a networked store it is worth it exactly when the candidates are not already cached, which the store itself checks — so turning this on hands the decision to the party that can make it, rather than making it here. The evidence that says to turn it on is a `:fetches` tally (`vaelii.impl.profile`) large against a query's wall clock on a corpus whose working set does not fit that store's cache. The chunk is the unit of over-fetch: a consumer that takes one solution and stops has hinted at most this many handles, so a large chunk amortizes better and wastes more. **`false` or a positive integer, and anything else is refused where it is bound** — `true` above all, which is what a var with an off-value of `false` invites and which is truthy enough to reach the chunk arithmetic before it fails.
nil, or [pred context entries]: while bound, kb-sentex sorts a literal on pred in
context by the permuting marks entries lists (mark-entries' keys) and no others,
so chain/respell-rows! stores, and core/handle-of looks up, the spelling a reader
that believes those marks reads (spelling-planner).
nil, or `[pred context entries]`: while bound, `kb-sentex` sorts a literal on `pred` in `context` by the permuting marks `entries` lists (`mark-entries`' keys) and no others, so `chain/respell-rows!` stores, and `core/handle-of` looks up, the spelling a reader that believes those marks reads (`spelling-planner`).
Whether candidate-handles may use the structural trie to narrow a positive
pattern with a nested compound argument — (mass ?o (QuantityFn ?n Kilogram)).
A positive fact's key linearizes its compound arguments into the trie path (see
vaelii.impl.sentex), so QuantityFn and Kilogram sit at their own trie levels
and p/lookup narrows on them even when the top-level argument is a
partially-variable compound — the one case the argument roots (top-level only) and
the flat trie both leave to a full functor-extent fan. On (default), that pattern
is answered by the structural trie; off, by the functor extent — a correct
superset the existing unify filters to the identical set, and the conservative
baseline the structural selectivity is measured against (structural_index_test,
modeled on arg_root_retrieval_test).
The structural key is written unconditionally, so the direct p/lookup paths
(find-sentex-handle, the level-0 raw lookup) always walk it; query and the
matching levels go through candidate-handles, so this gates their candidate
source too — never correctness: on and off return the same matches, on returns fewer
candidates. Negative and flat patterns are untouched — a :false key keeps its
body whole, so it has no deep positions to narrow on.
On by default: the oracle (structural_index_test) proves on == off over the
corpus, and the structural retrieval is a strict candidate-set win on a
compound-argument pattern (2 candidates vs the functor extent), so there is no
reason to prefer the looser fallback.
Whether `candidate-handles` may use the **structural trie** to narrow a positive pattern with a nested compound argument — `(mass ?o (QuantityFn ?n Kilogram))`. A positive fact's key linearizes its compound arguments into the trie path (see `vaelii.impl.sentex`), so `QuantityFn` and `Kilogram` sit at their own trie levels and `p/lookup` narrows on them even when the top-level argument is a partially-variable compound — the one case the argument roots (top-level only) and the flat trie both leave to a full functor-extent fan. On (default), that pattern is answered by the structural trie; off, by the **functor extent** — a correct superset the existing `unify` filters to the identical set, and the conservative baseline the structural selectivity is measured against (`structural_index_test`, modeled on `arg_root_retrieval_test`). The structural key is written unconditionally, so the direct `p/lookup` paths (`find-sentex-handle`, the level-0 raw lookup) always walk it; `query` and the matching levels go through `candidate-handles`, so this gates *their* candidate source too — never correctness: on and off return the same matches, on returns fewer candidates. Negative and flat patterns are untouched — a `:false` key keeps its body whole, so it has no deep positions to narrow on. On by default: the oracle (`structural_index_test`) proves on == off over the corpus, and the structural retrieval is a strict candidate-set win on a compound-argument pattern (2 candidates vs the functor extent), so there is no reason to prefer the looser fallback.
(belief-blind?)*belief-blind*, read once by a retrieval path rather than once per candidate.
The distinction is the whole reason this is a function and not a bare deref at each
filter. A ^:dynamic deref is a thread-bound check on every read, and the belief filter
sits in the innermost loop retrieval has — once per candidate handle, of which a broad
literal has thousands. Read into a local at the top of the path and the per-candidate
cost is an or against a boolean that short-circuits; read at the filter and it is a
var deref per handle, which negation-arbitration is close enough to its bound to see.
Correct to hoist because the value cannot change under a path: the entry point binds it around
the whole read and blind-seq re-establishes it per realization step, so whichever of
those constructed this seq had it bound already.
`*belief-blind*`, read **once** by a retrieval path rather than once per candidate. The distinction is the whole reason this is a function and not a bare deref at each filter. A `^:dynamic` deref is a thread-bound check on every read, and the belief filter sits in the innermost loop retrieval has — once per *candidate handle*, of which a broad literal has thousands. Read into a local at the top of the path and the per-candidate cost is an `or` against a boolean that short-circuits; read at the filter and it is a var deref per handle, which `negation-arbitration` is close enough to its bound to see. Correct to hoist because the value cannot change under a path: the entry point binds it around the whole read and `blind-seq` re-establishes it per realization step, so whichever of those constructed this seq had it bound already.
(believed-at? kb handle context)Is handle believed as context reads it: IN in the network, and not hidden from
context by a placed defeat in force there, or by resting only on a handle one hides
(exc/belief-hidden-fn)? The stored excepts are not applied, since an except is
visibility and this is belief.
The reader for a caller holding a sentex and no reader is the sentex's own context. A sentex resting only on a member every reader of it hides is IN in the network and hidden from every context that can read it, and this answers false for it.
Is `handle` believed as `context` reads it: IN in the network, and not hidden from `context` by a placed `defeat` in force there, or by resting only on a handle one hides (`exc/belief-hidden-fn`)? The stored excepts are not applied, since an `except` is visibility and this is belief. The reader for a caller holding a sentex and no reader is the sentex's own context. A sentex resting only on a member every reader of it hides is IN in the network and hidden from every context that can read it, and this answers false for it.
(blind-seq s)s, realized under *belief-blind* — one element at a time, with the binding
re-established for each.
A plain (binding [*belief-blind* true] (read …)) is wrong here and silently so,
which is the whole reason this exists. Every read entry point answers with a lazy seq, so the
binding frame is popped the moment the entry point returns and long before the first element is
computed: the belief filter then runs unbound, the read answers exactly what an ordinary
belief-following one would, and nothing anywhere reports that the flag did not take.
Wrapping the seq puts the binding back on the stack for each realization step — the
seq call and the first below both force inside it, chunk and all — so laziness
survives and so does the flag.
`s`, realized under `*belief-blind*` — one element at a time, with the binding re-established for each. A plain `(binding [*belief-blind* true] (read …))` is **wrong here and silently so**, which is the whole reason this exists. Every read entry point answers with a lazy seq, so the binding frame is popped the moment the entry point returns and long before the first element is computed: the belief filter then runs unbound, the read answers exactly what an ordinary belief-following one would, and nothing anywhere reports that the flag did not take. Wrapping the seq puts the binding back on the stack for each realization step — the `seq` call and the `first` below both force inside it, chunk and all — so laziness survives and so does the flag.
(concluding-rule-handles kb pred)(concluding-rule-handles kb pred context)(concluding-rule-handles kb pred context visible)Handles of rules whose consequent predicate is pred or a spec of it — a rule
concluding a subtype answers a supertype goal, the backward dual of fire-rules-for
fanning a new fact over its supertypes. Computed as the intersection specs(pred) ∩ rules-by-consequent: iterate the spec closure and probe the consequent index. A
non-symbol pred cannot be a type, so it degrades to the plain lookup.
Plus the variable-consequent catch-all. A rule concluding (?p ?y ?x) files its
consequent under p/var-consequent-key rather than under any concrete predicate (see
rules/consequent-index-pred), and could conclude any predicate once ?p binds — so
its bucket is unioned into every answer. Without it a goal on likes never discovers
a rule concluding (?p …), and backward chaining is blind to exactly the rules the
consequent-var-pred feature exists to make reachable.
A variable pred is the dual: the goal (?p Tom ?y) names no consequent bucket
and any rule may conclude it, subsuming-unify binding ?p to the consequent's
functor. So it answers every rule stated where visible reaches, read off the
rule extent (reads/as-stored-rules-in). Paid only for a variable functor, which
fact matching already answers through the argument roots; without it the open functor
reached stored facts and silently no rule.
The answer is bounded by the concluding rules; the cost is bounded by the taxonomy.
One index probe per spec, so a goal on a type with 364 subtypes takes 364 probes to
discover that no rule concludes any of them — and provers/shadowing-channels asks
this once per goal, on the path sole-prover takes. Cheap per probe and never a
record fetch, but it is the spec closure that sizes it, not the rule count.
With a context, the spec fan walks only the genl edges visible from it — a rule
concluding a subtype answers a supertype goal exactly where the subtype edge is
visible, mirroring the matching fan-out. With visible as well, a context set, every
index read returns only the rules stated in one of those contexts: both rule indexes
end in the context, so a rule stated where the reader cannot see is never read.
Handles of rules whose consequent predicate is `pred` **or a spec of it** — a rule concluding a subtype answers a supertype goal, the backward dual of `fire-rules-for` fanning a new fact over its supertypes. Computed as the intersection `specs(pred) ∩ rules-by-consequent`: iterate the spec closure and probe the consequent index. A non-symbol `pred` cannot be a type, so it degrades to the plain lookup. **Plus the variable-consequent catch-all.** A rule concluding `(?p ?y ?x)` files its consequent under `p/var-consequent-key` rather than under any concrete predicate (see `rules/consequent-index-pred`), and could conclude *any* predicate once `?p` binds — so its bucket is unioned into every answer. Without it a goal on `likes` never discovers a rule concluding `(?p …)`, and backward chaining is blind to exactly the rules the consequent-var-pred feature exists to make reachable. **A variable `pred` is the dual**: the goal `(?p Tom ?y)` names no consequent bucket and any rule may conclude it, `subsuming-unify` binding `?p` to the consequent's functor. So it answers **every** rule stated where `visible` reaches, read off the rule extent (`reads/as-stored-rules-in`). Paid only for a variable functor, which fact matching already answers through the argument roots; without it the open functor reached stored facts and silently no rule. **The answer is bounded by the concluding rules; the cost is bounded by the taxonomy.** One index probe per spec, so a goal on a type with 364 subtypes takes 364 probes to discover that no rule concludes any of them — and `provers/shadowing-channels` asks this once per goal, on the path `sole-prover` takes. Cheap per probe and never a record fetch, but it is the spec closure that sizes it, not the rule count. With a `context`, the spec fan walks only the genl edges visible from it — a rule concluding a subtype answers a supertype goal exactly where the subtype edge is visible, mirroring the matching fan-out. With `visible` as well, a context set, every index read returns only the rules stated in one of those contexts: both rule indexes end in the context, so a rule stated where the reader cannot see is never read.
(constraining-predicates kb kind pred context)The predicates whose argument declarations of kind kind bind a pred tuple —
pred itself first, then every super-predicate of it context can see that some
sentence declares kind of.
(genl fatherOf parentOf) says every fatherOf tuple is a parentOf tuple, and
a tuple set only narrows going down, so (arg parentOf 1 person) constrains every
fatherOf tuple exactly as it constrains every parentOf one. Reading the
declarations off the exact functor makes the refusal entry-point-dependent: the same
ill-typed claim is refused under the general spelling, admitted under the specialized
one, and then answers every general-spelling query through the matcher's own fan —
which is the one job the constraint exists for. Both readers of a declaration come
here, the constraint (checks/declaration-reader) and the inference
(provers/inferred-types), so assert and ask cannot disagree about whose
declarations speak for a tuple.
Scoped to the reader's own vantage. The closure is read from context, so a
genl edge asserted where the reader cannot see it imports no constraint — the same
judgement checks/args-problem already makes about the memberships it reads. A cycle
in predicate genl cannot loop the walk, genls being a closure read.
pred and its proper supers are both filtered against the roster of predicates
some declaration of kind names (tax/arg-declaration-props). A predicate the
roster does not name carries no (kind predicate …) declaration in any context, so
the scoped retrieval its inclusion would gate returns nothing; every consumer reads
declarations off the predicates handed back, so an undeclared predicate contributes an
empty retrieval whether it is listed or dropped. The filter is a set membership rather
than an index probe, which is what keeps the walk cheap: asked of the index it would be
one argument-root read per predicate per assert, so a membership of a type ten deep in
the hierarchy would pay ten of them, and nine of those types declare nothing —
including, on a minting assert, the mint's own functor (a type name like animal,
which no sentence declares arg of). The roster is global and therefore a superset of
what any context can see, and the scoped retrieval it gates decides which of the named
predicates actually speak here. When nothing anywhere declares kind the roster is
empty and the walk returns [] without reading the closure at all. The intersection
walks the smaller of the roster and the closure, so a membership of a type with
thousands of ancestors reads at most the roster.
The supers are sorted, so which declaration a refusal names — and the order the entailments are drawn in — is a function of the vocabulary rather than of the closure's hash order.
The predicates whose argument declarations of kind `kind` bind a `pred` tuple — `pred` itself first, then every super-predicate of it `context` can see that some sentence declares `kind` of. `(genl fatherOf parentOf)` says every `fatherOf` tuple **is** a `parentOf` tuple, and a tuple set only narrows going down, so `(arg parentOf 1 person)` constrains every `fatherOf` tuple exactly as it constrains every `parentOf` one. Reading the declarations off the exact functor makes the refusal *entry-point-dependent*: the same ill-typed claim is refused under the general spelling, admitted under the specialized one, and then answers every general-spelling query through the matcher's own fan — which is the one job the constraint exists for. Both readers of a declaration come here, the constraint (`checks/declaration-reader`) and the inference (`provers/inferred-types`), so `assert` and `ask` cannot disagree about whose declarations speak for a tuple. **Scoped to the reader's own vantage.** The closure is read from `context`, so a `genl` edge asserted where the reader cannot see it imports no constraint — the same judgement `checks/args-problem` already makes about the memberships it reads. A cycle in predicate `genl` cannot loop the walk, `genls` being a closure read. **`pred` and its proper supers are both filtered against the roster** of predicates some declaration of `kind` names (`tax/arg-declaration-props`). A predicate the roster does not name carries no `(kind predicate …)` declaration in any context, so the scoped retrieval its inclusion would gate returns nothing; every consumer reads declarations off the predicates handed back, so an undeclared predicate contributes an empty retrieval whether it is listed or dropped. The filter is a set membership rather than an index probe, which is what keeps the walk cheap: asked of the index it would be one argument-root read per predicate per assert, so a membership of a type ten deep in the hierarchy would pay ten of them, and nine of those types declare nothing — including, on a minting assert, the mint's own functor (a type name like `animal`, which no sentence declares `arg` of). The roster is global and therefore a superset of what any context can see, and the scoped retrieval it gates decides which of the named predicates actually speak here. When nothing anywhere declares `kind` the roster is empty and the walk returns `[]` without reading the closure at all. The intersection walks the smaller of the roster and the closure, so a membership of a type with thousands of ancestors reads at most the roster. The supers are sorted, so which declaration a refusal names — and the order the entailments are drawn in — is a function of the vocabulary rather than of the closure's hash order.
How many levels of compound nesting a subgoal may add over the deepest term its own
derivation path has already met (term-depth) before prove-from cuts the branch as
it cuts a repeated goal key — the :max-term-growth bound, where a caller names none.
The per-path seen set cuts a goal re-asking itself; a rule whose antecedent
nests a function application around a head variable, (implies (p (SuccFn ?x)) (p ?x)), never does: (p A) asks (p (SuccFn A)), which asks (p (SuccFn (SuccFn A))), each a goal nobody has asked. What the ceiling has to refuse is growth a
rule invented, and only that: a term is deep for two quite different reasons, and
the bound must tell them apart or it cuts derivable answers. So the basis it
measures against rises whenever a leaf match binds a deep stored term
(grown-term-base) and never when a rule expands, which leaves structural recursion
that shrinks a term — walking a list, counting a numeral down — untouched at any
depth, and leaves a conjunct that inherits a deep individual from the conjunct before
it measured from that individual's depth rather than from the query's. Termination is
unaffected: the store holds finitely many terms and each has a finite depth, so the
basis a path can reach is bounded by the deepest thing stored. Eight levels of growth
is room for a subgoal to nest an individual several layers deeper than anything it was
handed without being a term that grows without end.
How many levels of compound nesting a subgoal may add over the deepest term its own derivation path has already met (`term-depth`) before `prove-from` cuts the branch as it cuts a repeated goal key — the `:max-term-growth` bound, where a caller names none. The per-path `seen` set cuts a goal re-asking *itself*; a rule whose antecedent nests a function application around a head variable, `(implies (p (SuccFn ?x)) (p ?x))`, never does: `(p A)` asks `(p (SuccFn A))`, which asks `(p (SuccFn (SuccFn A)))`, each a goal nobody has asked. What the ceiling has to refuse is **growth a rule invented**, and only that: a term is deep for two quite different reasons, and the bound must tell them apart or it cuts derivable answers. So the basis it measures against rises whenever a leaf match binds a deep *stored* term (`grown-term-base`) and never when a rule expands, which leaves structural recursion that *shrinks* a term — walking a list, counting a numeral down — untouched at any depth, and leaves a conjunct that inherits a deep individual from the conjunct before it measured from that individual's depth rather than from the query's. Termination is unaffected: the store holds finitely many terms and each has a finite depth, so the basis a path can reach is bounded by the deepest thing stored. Eight levels of growth is room for a subgoal to nest an individual several layers deeper than anything it was handed without being a term that grows without end.
(defeatable-goal? idx goal)Could an answer to goal be one belief has already defeated — is its functor one some
defeated datum carries? False for every goal when idx is nil.
The push-time gate: a chainer that answers false here adds no check to the goal at all, so a KB with no defeat on that predicate runs the search it always ran.
Could an answer to `goal` be one belief has already defeated — is its functor one some defeated datum carries? False for every goal when `idx` is nil. The push-time gate: a chainer that answers false here adds no check to the goal at all, so a KB with no defeat on that predicate runs the search it always ran.
(defeated-answer? kb idx sentence context)Is sentence — an answer a rule expansion produced — a stored member of a nogood
(defeated-index) that a nogood's defeat in force, or a placed conflict, removes at the
query's reader (exc/defeats-of): context for a concrete one, and the member's own
context for an unscoped read, the reading a read with no reader gives? A guard defeat
covers one firing and not the sentence, so it removes no answer a rule expansion
produced.
Canonicalized against the KB before the lookup (kb-sentex), since the answer is built
from a goal and its bindings while the index holds stored sentences: a symmetric
literal's arguments are sorted in one and not the other, and comparing them raw would
miss the very answer being filtered.
Is `sentence` — an answer a rule expansion produced — a stored member of a nogood (`defeated-index`) that a nogood's defeat in force, or a placed conflict, removes at the query's reader (`exc/defeats-of`): `context` for a concrete one, and the member's own context for an unscoped read, the reading a read with no reader gives? A guard defeat covers one firing and not the sentence, so it removes no answer a rule expansion produced. Canonicalized against the KB before the lookup (`kb-sentex`), since the answer is built from a goal and its bindings while the index holds stored sentences: a symmetric literal's arguments are sorted in one and not the other, and comparing them raw would miss the very answer being filtered.
(defeated-index kb)What the backward chainers filter a rule-expanded answer against: {:standing {sentence #{handle}} :functors #{functor}} over the targets of the placed defeats
(reads/as-stored-named) and, while an except is stored, the members of the placed
(contradicts …), since a reader whose excepts lower a conflict member's class reads it
defeated — or nil when the walk reads nothing (exc/placed-reads?).
Nil is the gate every caller reads, and it is the common case: a KB with no
contradiction pays one set deref per query and nothing else. :functors is the second
gate, and the one that keeps the cost off a KB that has a defeat somewhere: a goal
whose functor no target carries can produce no withdrawn answer, so it is never
checked. The index reads the standing defeats and placed contradicts, and no nogood
candidate: a candidate that no defeat or placed contradicts names is defeated at no
reader.
Built once per query rather than asked per answer: a query writes nothing, so the
index cannot move underneath the search that read it. defeated-answer? asks the
query's reader whether it takes a member OUT (docs/nmtms.md, "A defeat is scoped to its
vantage").
What the backward chainers filter a rule-expanded answer against: `{:standing
{sentence #{handle}} :functors #{functor}}` over the targets of the placed defeats
(`reads/as-stored-named`) and, while an `except` is stored, the members of the placed
`(contradicts …)`, since a reader whose excepts lower a conflict member's class reads it
defeated — or **nil** when the walk reads nothing (`exc/placed-reads?`).
Nil is the gate every caller reads, and it is the common case: a KB with no
contradiction pays one set deref per query and nothing else. `:functors` is the second
gate, and the one that keeps the cost off a KB that *has* a defeat somewhere: a goal
whose functor no target carries can produce no withdrawn answer, so it is never
checked. The index reads the standing defeats and placed `contradicts`, and no nogood
candidate: a candidate that no defeat or placed `contradicts` names is defeated at no
reader.
Built once per query rather than asked per answer: a query writes nothing, so the
index cannot move underneath the search that read it. `defeated-answer?` asks the
query's reader whether it takes a member OUT (docs/nmtms.md, "A defeat is scoped to its
vantage").(displaced-terms-in kb visible? sentence)The {old-term representative} rewrites sentence undergoes under visible?, computed
the way representative-term actually rewrites it — so a quoted mention held opaque to a
sameAs is not reported displaced by why-not. Gated on tax/mention-marks: a KB declaring
no quoting_function and no modal_predicate takes the flat walk unchanged.
The `{old-term representative}` rewrites `sentence` undergoes under `visible?`, computed
the way `representative-term` actually rewrites it — so a quoted mention held opaque to a
`sameAs` is not reported displaced by `why-not`. Gated on `tax/mention-marks`: a KB declaring
no `quoting_function` and no `modal_predicate` takes the flat walk unchanged.(entries-at kb entries reader)The entries of entries some supporter of which reader believes
(supporter-believed?), as a set.
The entries of `entries` some supporter of which `reader` believes (`supporter-believed?`), as a set.
(equation? sentence)Is sentence a positive equation — (rewriteOf P D), (sameAs A B) or (equals A B)
at the top? Migration never restates one (kb/rewritable-sentex?), so the stored
equation is the only spelling of itself there will ever be. Two readers depend on
that: retired-for? never reports an equation retired, and goal-normal-form asks an
equation goal as spelled, so the goal and the stored sentence meet unrewritten. The
equality closure answers the rest of what an equation goal asks, through
provers/EqualityProver.
Is `sentence` a positive equation — `(rewriteOf P D)`, `(sameAs A B)` or `(equals A B)` at the top? Migration never restates one (`kb/rewritable-sentex?`), so the stored equation is the only spelling of itself there will ever be. Two readers depend on that: `retired-for?` never reports an equation retired, and `goal-normal-form` asks an equation goal as spelled, so the goal and the stored sentence meet unrewritten. The equality closure answers the rest of what an equation goal asks, through `provers/EqualityProver`.
(exception-aware-placements kb handles contexts)Placement candidates for handles stated in contexts: the maximal common
descendants of contexts, or, while an except hides one of handles somewhere, the
maximal contexts among the common descendants that see every handle with no except
hiding it (supporter-visible? with no defeat read). An except can hide a
supporter at its own context while a meta-exception restores it in only one descendant
ancestor set, so assertion contexts alone do not decide that case.
exc/closure-excepted-anywhere? is the coarse gate, so the ordinary placement path
takes no ancestor set walk when no except reaches the supporters. A firing's
conclusion, a placed nogood, a guard defeat and an inherited clash's askers read it.
Placement candidates for `handles` stated in `contexts`: the maximal common descendants of `contexts`, or, while an except hides one of `handles` somewhere, the maximal contexts among the common descendants that see every handle with no except hiding it (`supporter-visible?` with no `defeat` read). An except can hide a supporter at its own context while a meta-exception restores it in only one descendant ancestor set, so assertion contexts alone do not decide that case. `exc/closure-excepted-anywhere?` is the coarse gate, so the ordinary placement path takes no ancestor set walk when no except reaches the supporters. A firing's conclusion, a placed nogood, a guard defeat and an inherited clash's askers read it.
(fanned-match kb sentence vantage raw mapcat-fn)The fan-out itself, shared by every matcher that does one: decompose sentence into
the functor that fans and the rebuild that puts it back, take that functor's closure
from vantage, and run raw over each member — raw being the caller's own
as-written retrieval, and mapcat-fn its choice of lazy-mapcat or mapcat.
Shared for the reason sub-predicates and super-predicates are, one level up.
Those two keep the matchers from disagreeing about which predicates are in the fan;
this keeps them from disagreeing about what to do with the fan once they have it, which
is where the drift actually landed — the reference matcher counted the closure and its
rete twin rebuilt #{f} per call to compare against, the same reading written twice
and optimized once. A matcher joins by passing its own raw, so a new one cannot
quietly fan a negation the wrong way or skip the singleton short-circuit.
Three things it decides, once:
super-predicates), the direction a
genl edge carries through a negation, and rebuilds the not around each member.f itself, since both closures are reflexive, so there is
nothing to fan and the as-written retrieval is the whole answer. Counted rather than
compared against a freshly built #{f}; the same reading chain/fanning-functor?
takes of the same set.The fan-out itself, shared by every matcher that does one: decompose `sentence` into
the functor that fans and the rebuild that puts it back, take that functor's closure
from `vantage`, and run `raw` over each member — `raw` being the caller's own
as-written retrieval, and `mapcat-fn` its choice of `lazy-mapcat` or `mapcat`.
**Shared for the reason `sub-predicates` and `super-predicates` are, one level up.**
Those two keep the matchers from disagreeing about *which* predicates are in the fan;
this keeps them from disagreeing about what to do with the fan once they have it, which
is where the drift actually landed — the reference matcher counted the closure and its
rete twin rebuilt `#{f}` per call to compare against, the same reading written twice
and optimized once. A matcher joins by passing its own `raw`, so a new one cannot
quietly fan a negation the wrong way or skip the singleton short-circuit.
Three things it decides, once:
* **A variable or absent functor pins nothing** and fans not at all — one raw match on
the sentence as written.
* **A negation fans its body's functor upward** (`super-predicates`), the direction a
`genl` edge carries through a negation, and rebuilds the `not` around each member.
* **A singleton closure is `f` itself**, since both closures are reflexive, so there is
nothing to fan and the as-written retrieval is the whole answer. Counted rather than
compared against a freshly built `#{f}`; the same reading `chain/fanning-functor?`
takes of the same set.(freshen-rule {:keys [antecedents consequent guard] :as rule} taken)rule with every variable taken already speaks for renamed apart.
Without this, (anc ?x ?z) :- (parentOf ?x ?y) (anc ?y ?z) expanded twice on one path
asks unify to make ?x both the grandchild and the child. That fails, the branch
is lost, and an ancestor query answers only at distance one — a wrong answer, not a
slow one.
Nothing is renamed when nothing clashes: the top-level expansion of a query binds nothing yet, and a rule used once per path never meets itself. Those pay one set scan and get the rule they passed in.
The exceptWhen guard reads the rule's own variable names out of a completed
binding map (provers/exception-holds? substitutes the stored exception query with
them), so a renamed rule's guard is wrapped to bind those names to whatever this
instance's variables resolved to. A guard that fired before renaming fires after it.
`rule` with every variable `taken` already speaks for renamed apart. Without this, `(anc ?x ?z) :- (parentOf ?x ?y) (anc ?y ?z)` expanded twice on one path asks `unify` to make `?x` both the grandchild and the child. That fails, the branch is lost, and an ancestor query answers only at distance one — a wrong answer, not a slow one. Nothing is renamed when nothing clashes: the top-level expansion of a query binds nothing yet, and a rule used once per path never meets itself. Those pay one set scan and get the rule they passed in. The `exceptWhen` guard reads the rule's **own** variable names out of a completed binding map (`provers/exception-holds?` substitutes the stored exception query with them), so a renamed rule's guard is wrapped to bind those names to whatever this instance's variables resolved to. A guard that fired before renaming fires after it.
(goal-held-as-spelled? goal)Is goal asked as spelled, exempt from the goal rewrite? Two shapes are.
different — rewriting its arguments would map each to its class representative,
so a merged pair would compare equal, and reading class membership is the whole job
of different. provers/DifferentProver normalizes its own arguments instead.equation?) — its arguments are mentions, and a rewriteOf
spelling rename would turn (rewriteOf P D) into the self-edge (rewriteOf P P).
The stored equation is never restated, so the goal meets it only as spelled, and
provers/EqualityProver reads the closure for the symmetric, reflexive and
transitive answers.Is `goal` asked **as spelled**, exempt from the goal rewrite? Two shapes are. * **`different`** — rewriting its arguments would map each to its class representative, so a merged pair would compare equal, and reading class membership is the whole job of `different`. `provers/DifferentProver` normalizes its own arguments instead. * **A positive equation** (`equation?`) — its arguments are mentions, and a `rewriteOf` spelling rename would turn `(rewriteOf P D)` into the self-edge `(rewriteOf P P)`. The stored equation is never restated, so the goal meets it only as spelled, and `provers/EqualityProver` reads the closure for the symmetric, reflexive and transitive answers.
(goal-key g)A goal with all variables collapsed to ?, for loop detection: two goals that
differ only in variable names share a key.
A goal with all variables collapsed to `?`, for loop detection: two goals that differ only in variable names share a key.
(goal-normal-form kb goal context)normal-form for a goal, as context sees the merges, except for a goal
goal-held-as-spelled? exempts.
A question asked from a context is a question about what that context holds, so a merge
it does not inherit must not rename what it asked. kb/rewrite-goal is the read entry points'
spelling; BeliefProjectionProver calls this one directly, to put a proposition held
opaque to the asker into the normal form of the agent whose belief it is.
`normal-form` for a **goal**, as `context` sees the merges, except for a goal `goal-held-as-spelled?` exempts. A question asked from a context is a question about what that context holds, so a merge it does not inherit must not rename what it asked. `kb/rewrite-goal` is the read entry points' spelling; `BeliefProjectionProver` calls this one directly, to put a proposition held opaque to the asker into the normal form of the **agent** whose belief it is.
(grown-term-base base b)base raised to the nesting the extension bindings b bring in — the depth a term
bound to a variable contributes when it lands at a goal's top argument position, which
is 1 + its own (term-depth).
A leaf match reads what is stored, so a deep value here is a fact about the KB and
not about a rule growing a term; measuring the conjuncts that inherit it against the
query's own depth is what cut answers a reordering of the same conjunction returned.
One sequential? test per bound value, so a flat KB — every value a symbol — pays a
scan and nothing else.
`base` raised to the nesting the extension bindings `b` bring in — the depth a term bound to a variable contributes when it lands at a goal's top argument position, which is `1 +` its own (`term-depth`). A leaf match reads what is *stored*, so a deep value here is a fact about the KB and not about a rule growing a term; measuring the conjuncts that inherit it against the query's own depth is what cut answers a reordering of the same conjunction returned. One `sequential?` test per bound value, so a flat KB — every value a symbol — pays a scan and nothing else.
(initial-prove-stack kb goals context)(initial-prove-stack kb goals context est-override)The one-frame DFS stack prove starts from: the (cost-ordered) conjunction, no
bindings, an empty loop guard, depth 0, the answer variables — the query's own,
which every frame below inherits unchanged — and the query's own term depth
(term-depth), the basis the term-growth cut starts measuring a subgoal against. It
is a starting basis rather than a fixed one: a leaf match that binds a deeper stored
term raises it for the frames below (grown-term-base), so what the ceiling bounds is
the nesting a rule invented rather than the nesting the KB already held.
The basis rides the stack rather than the bounds map because the stack is the
continuation: a resume picks up frames it did not build, and a projection recomputed
from a budget could not know what the original question asked for. The term base
rides it for the same reason, and for a second: it is per path, so a resumed
segment measures growth from what its own frames had already met rather than from
whatever subgoal it happened to stop on.
Exposed so prove-within can seed a bounded run and hand its unfinished stack back to
resume.
est-override costs the top conjunction by something other than the index — the same
shape, and for the same reason, as planned-antecedents takes for a rule's antecedents.
An executor whose leaf is the prover registry passes it, because a genl conjunct that
a cached closure answers costs the closure's size and not the handful of stored edges
the trie can count.
The one-frame DFS stack `prove` starts from: the (cost-ordered) conjunction, no bindings, an empty loop guard, depth 0, the **answer variables** — the query's own, which every frame below inherits unchanged — and the query's own **term depth** (`term-depth`), the basis the term-growth cut starts measuring a subgoal against. It is a *starting* basis rather than a fixed one: a leaf match that binds a deeper stored term raises it for the frames below (`grown-term-base`), so what the ceiling bounds is the nesting a rule invented rather than the nesting the KB already held. The basis rides the *stack* rather than the bounds map because the stack is the continuation: a `resume` picks up frames it did not build, and a projection recomputed from a budget could not know what the original question asked for. The term base rides it for the same reason, and for a second: it is per **path**, so a resumed segment measures growth from what its own frames had already met rather than from whatever subgoal it happened to stop on. Exposed so `prove-within` can seed a bounded run and hand its unfinished stack back to `resume`. `est-override` costs the top conjunction by something other than the index — the same shape, and for the same reason, as `planned-antecedents` takes for a rule's antecedents. An executor whose leaf is the prover registry passes it, because a `genl` conjunct that a cached closure answers costs the closure's size and not the handful of stored edges the trie can count.
(kb-sentex kb sentence context)Build a sentex canonicalized against this KB's taxonomy: a symmetric predicate's
arguments are sorted, so (siblingOf Bob Ann) and (siblingOf Ann Bob) become the
same sentex. Every construction that stores or looks one up must go through this —
otherwise an asserted form and a queried form could key differently.
The commutativity marks generalize the same sorting to a declared set of positions at
any arity, and are read here the same way: tax/commuting-groups off the literal's own
functor, one map read that misses for every predicate declaring nothing.
The property read is global: the store keys a fact by the sort every stored mark gives
it, so an asserted form and a probe meet at one key. While *spelled-by* names this sentence's predicate and context, the sort reads only
the marks it lists, so a spelling a reader reads can be stored and looked up
(spelling-planner).
Build a sentex canonicalized against this KB's taxonomy: a symmetric predicate's arguments are sorted, so `(siblingOf Bob Ann)` and `(siblingOf Ann Bob)` become the same sentex. Every construction that stores or looks one up must go through this — otherwise an asserted form and a queried form could key differently. The commutativity marks generalize the same sorting to a declared set of positions at any arity, and are read here the same way: `tax/commuting-groups` off the literal's own functor, one map read that misses for every predicate declaring nothing. The property read is global: the store keys a fact by the sort every stored mark gives it, so an asserted form and a probe meet at one key. While `*spelled-by*` names this sentence's predicate and context, the sort reads only the marks it lists, so a spelling a reader reads can be stored and looked up (`spelling-planner`).
(lazy-mapcat f coll)mapcat that calls f one element at a time.
Not a stylistic preference — clojure.core/mapcat is (apply concat (map f coll)),
and map realizes a whole 32-element chunk at once when its source is chunked.
Over a handful of contexts or subtypes that means every branch is expanded (each
its own trie walk) before the first result is handed back, which is exactly the
cost the matching layers exist to avoid. Here the recursive call sits inside
lazy-seq, so a caller taking one solution expands one branch.
`mapcat` that calls `f` **one element at a time**. Not a stylistic preference — `clojure.core/mapcat` is `(apply concat (map f coll))`, and `map` realizes a whole 32-element chunk at once when its source is chunked. Over a handful of contexts or subtypes that means *every* branch is expanded (each its own trie walk) before the first result is handed back, which is exactly the cost the matching layers exist to avoid. Here the recursive call sits inside `lazy-seq`, so a caller taking one solution expands one branch.
(lead-literal? sentence)A literal matches-hierarchical answers from an argument lead — a plain positive
literal (hierarchical-literal?) with an indexable argument to read the argument
roots by. For such a literal the set-algebra path costs one slot read (or one scoped
read per spec, whichever is smaller — *lead-side*) where the nested fan-out costs a
trie walk per sub-predicate, and the two return the identical set. The forward join
asks this of a substituted antecedent (chain/join-antecedent) to route a bound type
test past the |specs| fan.
A literal `matches-hierarchical` answers from an **argument lead** — a plain positive literal (`hierarchical-literal?`) with an indexable argument to read the argument roots by. For such a literal the set-algebra path costs one slot read (or one scoped read per spec, whichever is smaller — `*lead-side*`) where the nested fan-out costs a trie walk per sub-predicate, and the two return the identical set. The forward join asks this of a substituted antecedent (`chain/join-antecedent`) to route a bound type test past the `|specs|` fan.
(mark-entries tax pred)The permuting marks the store sorts pred by, as {entry {handle context}}: the
symmetric entry [:prop :symmetric pred] and one [:commuting pred group] per
commuting group, each with its supporters. Empty for a predicate nothing permutes.
The permuting marks the store sorts `pred` by, as `{entry {handle context}}`: the
`symmetric` entry `[:prop :symmetric pred]` and one `[:commuting pred group]` per
commuting group, each with its supporters. Empty for a predicate nothing permutes.(match-pattern kb sentence)(match-pattern kb sentence context)(match-pattern kb sentence context vantage)Seq of [handle bindings] for stored sentexes matching sentence within
context (default the wildcard ?ctx). The functor fans out over its sub-predicate
(genl spec) closure, so a unary type predicate is met by its subtypes
((animal ?x) ← (dog Muffet)) and — with predicate-genl edges — an n-ary predicate
by its sub-predicates ((parentOf a ?x) ← (fatherOf a v)). A functor with no
sub-predicates has a singleton closure, so this is a no-op for it (the overwhelming
common case — one cached set lookup, no fan).
A negation fans its body's functor the other way, over super-predicates:
(not (dog ?x)) is answered by (not (animal Muffet)), since dog ⊑ animal entails
¬animal ⊑ ¬dog. The not itself heads nothing and has no closure of its own, so
the fan reads inside it and rebuilds the negation around each member; each rebuilt
pattern is retrieved by the negative key it names, exactly as the written one is.
The fan is scoped to the genl edges visible from vantage — by default the
literal context itself, and the global closure for a ?ctx match. The four-arity
exists for matches-visible*, which matches at each ancestor context in turn but
stands at the view context throughout: scoping the fan by the ancestor would
shrink the vantage as the walk ascends, and the set-algebra twin (which filters by
the view's ancestor set once) would disagree.
Seq of [handle bindings] for stored sentexes matching `sentence` within `context` (default the wildcard ?ctx). The **functor fans out over its sub-predicate (genl spec) closure**, so a unary type predicate is met by its subtypes (`(animal ?x)` ← `(dog Muffet)`) and — with predicate-genl edges — an n-ary predicate by its sub-predicates (`(parentOf a ?x)` ← `(fatherOf a v)`). A functor with no sub-predicates has a singleton closure, so this is a no-op for it (the overwhelming common case — one cached set lookup, no fan). **A negation fans its body's functor the other way**, over `super-predicates`: `(not (dog ?x))` is answered by `(not (animal Muffet))`, since `dog ⊑ animal` entails `¬animal ⊑ ¬dog`. The `not` itself heads nothing and has no closure of its own, so the fan reads inside it and rebuilds the negation around each member; each rebuilt pattern is retrieved by the negative key it names, exactly as the written one is. The fan is scoped to the genl edges visible from `vantage` — by default the literal context itself, and the global closure for a `?ctx` match. The four-arity exists for `matches-visible*`, which matches at each ancestor context in turn but stands at the *view* context throughout: scoping the fan by the ancestor would shrink the vantage as the walk ascends, and the set-algebra twin (which filters by the view's ancestor set once) would disagree.
(match1 kb antecedent fact)(match1 kb antecedent fact context)Unify a single antecedent pattern against a ground fact sentence, honoring predicate specificity: a fact whose functor is a spec (sub-predicate, via the genl closure) of the antecedent's functor satisfies it, with the arguments unified.
For a unary type antecedent this is the ordinary subtype rule — (animal ?x) is met
by (dog Muffet). Generalized to n-ary predicates, (parentOf ?x ?y) is met by
(fatherOf Tom Bob) once (genl fatherOf parentOf) holds — the same subsumption the
type hierarchy gives, applied to the predicate hierarchy. When the functors are
equal (the common case) or the antecedent's functor has no sub-predicates, this is a
plain unify, so nothing changes for a KB without predicate-genl edges.
Under a negation the fan reverses, because a genl edge carries the other way
through one: dog ⊑ animal makes (dog Muffet) satisfy (animal ?x) and makes
(not (animal Muffet)) satisfy (not (dog ?x)) — the contrapositive, so a negated
antecedent is met by a negative fact on a genl of its body's predicate. The two
directions are exclusive: (not (dog Muffet)) does not satisfy (not (animal ?x)),
which is the reading a fan in the positive direction would give it. Both sides must
be negations for this to apply; a negation matched against a positive fact fails on
polarity as it does anywhere else.
The subsumption is scoped when a context is given: the predicate-genl closure is
walked only through the edges that context can see, so a match reached through a genl
edge stated in a context the reader cannot see is not a match for it — a watcher in one
context stops answering through another's edge (core/watch-match), agreeing with what
ask from that context would say. The two-arity is unscoped, for the callers that fix
visibility elsewhere: the forward trigger match (chain/fire-rules-for) is a candidate
filter whose placement re-derives the genlCx supporters the firing then rests on, so a
subsumption invisible to the placement context drops out at placement, not here.
Unify a single antecedent pattern against a ground fact sentence, honoring **predicate specificity**: a fact whose functor is a *spec* (sub-predicate, via the genl closure) of the antecedent's functor satisfies it, with the arguments unified. For a unary type antecedent this is the ordinary subtype rule — `(animal ?x)` is met by `(dog Muffet)`. Generalized to n-ary predicates, `(parentOf ?x ?y)` is met by `(fatherOf Tom Bob)` once `(genl fatherOf parentOf)` holds — the same subsumption the type hierarchy gives, applied to the predicate hierarchy. When the functors are equal (the common case) or the antecedent's functor has no sub-predicates, this is a plain unify, so nothing changes for a KB without predicate-genl edges. **Under a negation the fan reverses**, because a `genl` edge carries the other way through one: `dog ⊑ animal` makes `(dog Muffet)` satisfy `(animal ?x)` and makes `(not (animal Muffet))` satisfy `(not (dog ?x))` — the contrapositive, so a negated antecedent is met by a negative fact on a **genl** of its body's predicate. The two directions are exclusive: `(not (dog Muffet))` does not satisfy `(not (animal ?x))`, which is the reading a fan in the positive direction would give it. Both sides must be negations for this to apply; a negation matched against a positive fact fails on polarity as it does anywhere else. **The subsumption is scoped when a `context` is given**: the predicate-genl closure is walked only through the edges that context can see, so a match reached through a `genl` edge stated in a context the reader cannot see is not a match for it — a watcher in one context stops answering through another's edge (`core/watch-match`), agreeing with what `ask` from that context would say. The two-arity is unscoped, for the callers that fix visibility elsewhere: the forward trigger match (`chain/fire-rules-for`) is a candidate filter whose placement re-derives the genlCx supporters the firing then rests on, so a subsumption invisible to the placement context drops out at placement, not here.
(matches-hierarchical kb sentence view-context)The set-algebra twin of matches-visible for a positive literal: the identical
[handle bindings stored] set, but reached by context-scoped index reads of the
sub-predicates' own nodes instead of the |specs| × |context-up| product of trie
walks. Falls back to matches-visible for any shape it does not handle, and for a
literal with a spec stored under another functor (folded-spec?).
The set-algebra twin of `matches-visible` for a positive literal: the identical `[handle bindings stored]` set, but reached by context-scoped index reads of the sub-predicates' own nodes instead of the `|specs| × |context-up|` product of trie walks. Falls back to `matches-visible` for any shape it does not handle, and for a literal with a spec stored under another functor (`folded-spec?`).
(matches-visible kb sentence view-context)(matches-visible kb sentence view-context cached?)Type-aware matches of sentence visible from view-context. A variable
context means any context; a concrete context sees a fact iff the fact's
context is in view-context's genlCx up-closure — this is how inference in a
specific context can use facts asserted in the general contexts it inherits.
A positive literal is answered by the set-algebra path (matches-hierarchical,
default) instead of the nested fan-out; bind *hierarchical-retrieval* false for the
reference fan-out.
A sentex an except has hidden from view-context is filtered out — the read side
of visibility removal. Forward chaining holds the same line by a different
mechanism: its join runs at '?ctx, where the hidden set is empty by construction,
and the block is applied per placement (chain/antecedent-hidden?,
justification-excepted?), where the context the except scopes to is known.
Answers are cached per KB by the literal they answer, α-renamed so two spellings
of one question share an entry, and stamped with the change clock so any mutation
retires them (vaelii.impl.literal-cache). All three retrieval-strategy vars are
part of the key rather than assumed away: the set-algebra and fan-out paths must agree
on the answer set, and so must the structural-trie and functor-extent candidate
sources, which is what retrieval_completeness_test and structural_index_test check
— a cache that served one path's answers to the other would be checking a result
against itself. With literal-cache/*enabled* false this is the bare call.
*belief-blind* is in the key for the same reason and a sharper one: a CxEverything
read and an ordinary one ask the same literal at the same context and must not answer
each other. Left off, the first read of a pair fills the entry and the second is served
it — so a blind read would hide a defeated default it was asked for, or an ordinary one
would report a default it must not, whichever happened to run first.
tax/*search* is in the key because a read inside a second-route search reads belief
alone for a belief read, and can read false off a route question still open above it.
tax/*network-belief* is in the key because a placement in chain reads the network
and the excepts, and no defeat (exc/hidden-fn).
cached? false asks the same question and neither consults the cache nor fills
it — for a caller whose repeats that cache cannot serve. A transitive closure walk
asks each node's neighbour literal once (provers/reach visits a node once), so there
is no repeat there for a solution cache to catch, while its insertion per node would
push the cache past its bound and clear it wholesale part-way through, evicting the
metadata literals a rule-heavy query really does re-ask. An argument rather than a
rebinding of literal-cache/*enabled*, for two reasons: a binding covers every read
under the walk rather than the neighbour probe alone, and it marks the var
thread-bound for the life of the process — so every later matches-visible on every
thread would take the thread-local path to read a flag nothing had rebound. The
repetition a walk does have is held where it is: provers/cached-reach for the whole
closure, observe/*reach-memo* for the neighbour sets a join re-walks.
Type-aware matches of `sentence` *visible from* `view-context`. A variable context means any context; a concrete context sees a fact iff the fact's context is in view-context's genlCx up-closure — this is how inference in a specific context can use facts asserted in the general contexts it inherits. A positive literal is answered by the set-algebra path (`matches-hierarchical`, default) instead of the nested fan-out; bind `*hierarchical-retrieval*` false for the reference fan-out. A sentex an `except` has hidden from `view-context` is filtered out — the read side of visibility removal. Forward chaining holds the same line by a different mechanism: its join runs at `'?ctx`, where the hidden set is empty by construction, and the block is applied per *placement* (`chain/antecedent-hidden?`, `justification-excepted?`), where the context the except scopes to is known. Answers are **cached per KB** by the literal they answer, α-renamed so two spellings of one question share an entry, and stamped with the change clock so any mutation retires them (`vaelii.impl.literal-cache`). **All three** retrieval-strategy vars are part of the key rather than assumed away: the set-algebra and fan-out paths must agree on the answer set, and so must the structural-trie and functor-extent candidate sources, which is what `retrieval_completeness_test` and `structural_index_test` check — a cache that served one path's answers to the other would be checking a result against itself. With `literal-cache/*enabled*` false this is the bare call. `*belief-blind*` is in the key for the same reason and a sharper one: a `CxEverything` read and an ordinary one ask the *same literal at the same context* and must not answer each other. Left off, the first read of a pair fills the entry and the second is served it — so a blind read would hide a defeated default it was asked for, or an ordinary one would report a default it must not, whichever happened to run first. `tax/*search*` is in the key because a read inside a second-route search reads belief alone for a belief read, and can read false off a route question still open above it. `tax/*network-belief*` is in the key because a placement in `chain` reads the network and the excepts, and no defeat (`exc/hidden-fn`). **`cached?` false asks the same question and neither consults the cache nor fills it** — for a caller whose repeats that cache cannot serve. A transitive closure walk asks each node's neighbour literal once (`provers/reach` visits a node once), so there is no repeat there for a solution cache to catch, while its insertion per node would push the cache past its bound and clear it wholesale part-way through, evicting the metadata literals a rule-heavy query really does re-ask. An argument rather than a rebinding of `literal-cache/*enabled*`, for two reasons: a `binding` covers every read *under* the walk rather than the neighbour probe alone, and it marks the var thread-bound for the life of the process — so every later `matches-visible` on every thread would take the thread-local path to read a flag nothing had rebound. The repetition a walk does have is held where it is: `provers/cached-reach` for the whole closure, `observe/*reach-memo*` for the neighbour sets a join re-walks.
(matches-visible* kb sentence view-context)The reference nested fan-out: |context-up| × |specs| trie walks. matches-visible
dispatches to this or to matches-hierarchical; the latter also falls back here for
a shape it does not handle, so this must not re-dispatch (it is the fixed point that
breaks the cycle).
The reference nested fan-out: `|context-up| × |specs|` trie walks. `matches-visible` dispatches to this or to `matches-hierarchical`; the latter also falls back here for a shape it does not handle, so this must not re-dispatch (it is the fixed point that breaks the cycle).
(normal-form kb term visible?)term (a sentence or a term) in the equality normal form the KB stores and asks in:
every symbol to its class representative (representative-term), then argument terms
reduced by the oriented schematic equations visible to the same reader
(rewrite/normalize-sentence). Migration and query both go through here, so a stored
term and a goal meet at one form.
Both halves are belief-following and both are gated: a KB with no merges pays a
representative lookup per symbol, one with no schematic equations skips normalization
entirely (tax/rewrite-rules is empty). visible? is the supporter predicate already
built (visible-supporter-fn), so a caller normalizing many sentences under one reader
builds it once; nil is the unscoped read, which asks about the KB rather than from a
vantage. kb/rewrite-term is the spelling for a caller holding a context instead.
`term` (a sentence or a term) in the **equality normal form** the KB stores and asks in: every symbol to its class representative (`representative-term`), then argument terms reduced by the oriented schematic equations visible to the same reader (`rewrite/normalize-sentence`). Migration and query both go through here, so a stored term and a goal meet at one form. Both halves are belief-following and both are gated: a KB with no merges pays a representative lookup per symbol, one with no schematic equations skips normalization entirely (`tax/rewrite-rules` is empty). `visible?` is the supporter predicate already built (`visible-supporter-fn`), so a caller normalizing many sentences under one reader builds it once; nil is the unscoped read, which asks about the KB rather than from a vantage. `kb/rewrite-term` is the spelling for a caller holding a context instead.
(permuted-functor sentence)The predicate whose permuting marks decide how sentence is spelled when stored — its
functor, under a not — or nil.
The predicate whose permuting marks decide how `sentence` is spelled when stored — its functor, under a `not` — or nil.
(planned-antecedents kb antecedents consequent context bindings)(planned-antecedents kb antecedents consequent context bindings est-override)A rule's antecedents in the order they should be solved, given the bindings the
head match already produced. Stored antecedent order is canonical order — chosen
so two spellings of one rule dedup to one sentex (sentex/canonicalize-rule) — and
canonical order is structural, so it bears no relation to what is cheap to run.
Reordering here changes cost, never the answer set: a conjunction is commutative,
and vaelii.impl.plan pins the two literals whose position is operational (the
evaluables and the recursive one).
Antecedents are substituted before planning, not after, so the planner costs
them against real values — count-at [parentOf Tom] is an exact count where
parentOf with an unknown-but-bound first argument is only an average branch.
Pushing the substituted literals is equivalent to pushing the originals, because
every binding map they are later substituted with extends this one.
est-override, when given, is passed through to plan/order — the executor
whose subgoals are answered by the prover registry costs them by the registry
(provers/est-goal) rather than by the index alone.
A rule's antecedents in the order they should be *solved*, given the bindings the head match already produced. Stored antecedent order is canonical order — chosen so two spellings of one rule dedup to one sentex (`sentex/canonicalize-rule`) — and canonical order is structural, so it bears no relation to what is cheap to run. Reordering here changes cost, never the answer set: a conjunction is commutative, and `vaelii.impl.plan` pins the two literals whose position *is* operational (the evaluables and the recursive one). Antecedents are substituted **before** planning, not after, so the planner costs them against real values — `count-at [parentOf Tom]` is an exact count where `parentOf` with an unknown-but-bound first argument is only an average branch. Pushing the substituted literals is equivalent to pushing the originals, because every binding map they are later substituted with extends this one. `est-override`, when given, is passed through to `plan/order` — the executor whose subgoals are answered by the prover registry costs them by the registry (`provers/est-goal`) rather than by the index alone.
(project-answer bindings answer-vars)A finished derivation's bindings, resolved and cut down to the variables the query
asked about. nil answer-vars projects nothing, for a caller driving the chainer
from a stack it built itself.
A derivation path accumulates one flat binding map, and every rule instance it
expands contributes its own variables to it — a stored rule is spelled ?var0 ?var1 …
and each instance is renamed apart again (freshen-rule), so a six-rule proof of a
two-variable query resolves fourteen names. Those are scratch: they are how the search
got there, not what it was asked. Projecting is what makes a solution a map over the
question rather than over the proof, and it is what lets two engines that reach the
same answer by different derivations return the same value.
Note the projection is by name, not by provenance. A query that itself writes ?var0
is asking about ?var0, and gets it — the canonical rule spelling is a spelling, and a
variable belongs to whoever wrote it.
A finished derivation's bindings, resolved and cut down to the variables the *query* asked about. `nil` `answer-vars` projects nothing, for a caller driving the chainer from a stack it built itself. **A derivation path accumulates one flat binding map**, and every rule instance it expands contributes its own variables to it — a stored rule is spelled `?var0 ?var1 …` and each instance is renamed apart again (`freshen-rule`), so a six-rule proof of a two-variable query resolves fourteen names. Those are scratch: they are how the search got there, not what it was asked. Projecting is what makes a solution a map over the question rather than over the proof, and it is what lets two engines that reach the same answer by different derivations return the same value. Note the projection is by name, not by provenance. A query that itself writes `?var0` is asking about `?var0`, and gets it — the canonical rule spelling is a spelling, and a variable belongs to whoever wrote it.
(prove kb rules-fn goals context)(prove kb rules-fn goals context bounds)A simple depth-first backward chainer using loop/recur over an explicit goal
stack. Returns a vector of fully-resolved solution binding maps for proving the
conjunction goals in context. Type-aware (specificity) and context-aware
(matches-visible); a per-path :seen set of goal-keys blocks a goal from
re-expanding itself through recursive rules, and a term-growth ceiling
(default-max-term-growth) blocks a subgoal whose arguments nest deeper than
anything its own path has met, by more than the allowance — the recursion a goal key
cannot see, since a rule wrapping a function around a head variable asks a fresh goal
per expansion.
Together the two make every search terminate on the data. Prefer right-recursive
rules — a left-recursive rule is pruned after its first expansion. rules-fn
maps a subgoal to candidate parsed rules.
Runs to completion; prove-from is the bounded/resumable variant this delegates
to (vaelii.core/prove-within builds the anytime contract on it), and prove-seq
is the same search driven lazily.
The 5-arg arity takes prove-from's bounds map (prove-seq's keys, plus
:max-results), so a caller can run this eager search with a registry leaf
({:leaf-solver provers/solve-goal :est-override (provers/registry-est-override kb ctx)})
— an antecedent answered by a prover, an evaluatable or a cached closure rather than only
a stored fact, the division vaelii.core/prove and vaelii.core/query run. The 4-arg
keeps the stored-fact leaf (nil bounds).
A simple depth-first backward chainer using loop/recur over an explicit goal
stack. Returns a vector of fully-resolved solution binding maps for proving the
conjunction `goals` in `context`. Type-aware (specificity) and context-aware
(matches-visible); a per-path :seen set of goal-keys blocks a goal from
re-expanding itself through recursive rules, and a term-growth ceiling
(`default-max-term-growth`) blocks a subgoal whose arguments nest deeper than
anything its own path has met, by more than the allowance — the recursion a goal key
cannot see, since a rule wrapping a function around a head variable asks a fresh goal
per expansion.
Together the two make every search terminate on the data. Prefer right-recursive
rules — a left-recursive rule is pruned after its first expansion. `rules-fn`
maps a subgoal to candidate parsed rules.
Runs to completion; `prove-from` is the bounded/resumable variant this delegates
to (`vaelii.core/prove-within` builds the anytime contract on it), and `prove-seq`
is the same search driven lazily.
The 5-arg arity takes `prove-from`'s `bounds` map (`prove-seq`'s keys, plus
`:max-results`), so a caller can run this eager search with a **registry leaf**
(`{:leaf-solver provers/solve-goal :est-override (provers/registry-est-override kb ctx)}`)
— an antecedent answered by a prover, an evaluatable or a cached closure rather than only
a stored fact, the division `vaelii.core/prove` and `vaelii.core/query` run. The 4-arg
keeps the stored-fact leaf (`nil` bounds).(prove-from kb
rules-fn
context
{:keys [deadline max-results max-depth max-term-growth leaf-solver
est-override]}
stack
solutions)The resumable core of prove: run the DFS from an explicit stack (and the
solutions gathered so far) under bounds, a map of optional caps —
:deadline an absolute System/nanoTime instant; stop once reached, checked
between steps and, through budget/*deadline*, inside a leaf's
walk (budget/interruptible)
:max-results stop once this many solutions are in hand
:max-depth do not expand a rule past this rule-expansion depth
:max-term-growth
do not expand a subgoal whose arguments nest compound terms this
many levels deeper than the deepest term its own path has already
met (term-depth, grown-term-base); default
default-max-term-growth. The half of the loop guard the seen
set cannot be: a rule nesting a function around a head variable
asks a fresh goal per expansion, and only the term's growth repeats
:leaf-solver how a goal is answered without expanding a rule — see
leaf-solutions. nil is the stored facts, which is what prove
means by a leaf
:est-override the cost model for a rule's antecedents, when the index model is the
wrong one for this executor's leaf — see planned-antecedents
Returns {:solutions <vector> :status <kw> :stack <frames>}. :status is
:complete when the search space is exhausted (:stack empty), else :timeout
or :capped with a non-empty :stack the caller resumes from. With bounds
nil this simply runs to completion, which is what an unbounded prove is.
Each frame carries a :depth (rule expansions taken to reach it); a fact match
keeps the depth and a rule expansion increments it, so :max-depth bounds
transformation depth — the search's reach through rules — not the goal-stack
size. The bound checks sit at the loop top, ahead of the frame work, so a run
can stop between any two steps and the stack it leaves behind is a faithful
continuation. A leaf the deadline stops inside is one step not taken: its frame goes
back on the stack marked :unbounded-leaf?, and the segment that resumes it runs that
leaf with no deadline, so a resume loop under a fixed budget gets past a walk longer
than the budget and terminates.
The resumable core of `prove`: run the DFS from an explicit `stack` (and the
`solutions` gathered so far) under `bounds`, a map of optional caps —
:deadline an absolute `System/nanoTime` instant; stop once reached, checked
between steps and, through `budget/*deadline*`, inside a leaf's
walk (`budget/interruptible`)
:max-results stop once this many solutions are in hand
:max-depth do not expand a rule past this rule-expansion depth
:max-term-growth
do not expand a subgoal whose arguments nest compound terms this
many levels deeper than the deepest term its own path has already
met (`term-depth`, `grown-term-base`); default
`default-max-term-growth`. The half of the loop guard the `seen`
set cannot be: a rule nesting a function around a head variable
asks a fresh goal per expansion, and only the term's growth repeats
:leaf-solver how a goal is answered *without* expanding a rule — see
`leaf-solutions`. nil is the stored facts, which is what `prove`
means by a leaf
:est-override the cost model for a rule's antecedents, when the index model is the
wrong one for this executor's leaf — see `planned-antecedents`
Returns `{:solutions <vector> :status <kw> :stack <frames>}`. `:status` is
`:complete` when the search space is exhausted (`:stack` empty), else `:timeout`
or `:capped` with a **non-empty** `:stack` the caller resumes from. With `bounds`
nil this simply runs to completion, which is what an unbounded `prove` is.
Each frame carries a `:depth` (rule expansions taken to reach it); a fact match
keeps the depth and a rule expansion increments it, so `:max-depth` bounds
*transformation* depth — the search's reach through rules — not the goal-stack
size. The bound checks sit at the loop top, ahead of the frame work, so a run
can stop between any two steps and the stack it leaves behind is a faithful
continuation. A leaf the deadline stops inside is one step not taken: its frame goes
back on the stack marked `:unbounded-leaf?`, and the segment that resumes it runs that
leaf with no deadline, so a resume loop under a fixed budget gets past a walk longer
than the budget and terminates.(prove-seq kb rules-fn goals context)(prove-seq kb rules-fn goals context bounds)The same search as prove, lazily — a seq of solution binding maps that costs one
solution per pull rather than the whole space up front.
prove-from is already resumable, so this needs no second engine: run it capped at one
result, hand back that solution, and resume from the :stack it left when the consumer
asks again. :capped is the only status that means more, and allowed to continue —
:complete is exhaustion and :timeout is a deadline the caller set, and both end the
seq.
bounds takes prove-from's keys except :max-results, which this drives itself; a
consumer bounds the result count by taking that many.
Laziness costs the search one scope per segment rather than one per run (see the
comment in prove-from): the transitive-closure memo starts empty on each pull, and
resident values are re-read rather than pinned across the whole seq. For a read that is
sound — a query mutates no belief, so there is no write for a pin to hold still against.
It is also, measurably, not paid for: over a 120-answer recursive chain, realizing
every answer through this costs what the eager loop costs (40.3 ms against 40.4 ms),
while taking one costs about half (19.0 ms against 35.0 ms) — and that chain is the
unfavourable shape, one whose search dives to its deepest answer before yielding a
first. Where answers come early the gap is a multiple, not a fraction. So prove
remains the call for wanting a vector back, not for wanting it cheaper.
The same search as `prove`, **lazily** — a seq of solution binding maps that costs one solution per pull rather than the whole space up front. `prove-from` is already resumable, so this needs no second engine: run it capped at one result, hand back that solution, and resume from the `:stack` it left when the consumer asks again. `:capped` is the only status that means *more, and allowed to continue* — `:complete` is exhaustion and `:timeout` is a deadline the caller set, and both end the seq. `bounds` takes `prove-from`'s keys except `:max-results`, which this drives itself; a consumer bounds the result count by taking that many. Laziness costs the search **one scope per segment** rather than one per run (see the comment in `prove-from`): the transitive-closure memo starts empty on each pull, and resident values are re-read rather than pinned across the whole seq. For a read that is sound — a query mutates no belief, so there is no write for a pin to hold still against. It is also, measurably, not paid for: over a 120-answer recursive chain, realizing *every* answer through this costs what the eager loop costs (40.3 ms against 40.4 ms), while taking one costs about half (19.0 ms against 35.0 ms) — and that chain is the unfavourable shape, one whose search dives to its deepest answer before yielding a first. Where answers come early the gap is a multiple, not a fraction. So `prove` remains the call for wanting a vector back, not for wanting it cheaper.
(raw-match kb sentence context)Match a literal in one literal context — no genlCx inheritance, no subtype
fan-out — over every argument arrangement its predicate licences (raw-match-with),
probing the stored index with match-one. Yields [handle bindings stored-sentex].
Match a literal in one **literal** context — no genlCx inheritance, no subtype fan-out — over every argument arrangement its predicate licences (`raw-match-with`), probing the stored index with `match-one`. Yields `[handle bindings stored-sentex]`.
(raw-match-with kb probe sentence)Match a literal by probe — (probe form) → a seq of [handle bindings …], one
literal context — over every argument arrangement the predicate licences: the mirror
for a symmetric predicate, the other arrangements of the commuting component for a
commutative one. Only fully-ground symmetric and commuting literals are stored
sorted (see vaelii.impl.sentex), so the fan is what makes lookup order-insensitive:
it retrieves (siblingOf Ann Carol) from the pattern (siblingOf ?x Carol) or
(siblingOf Carol ?x) alike, and keeps a fact reachable even if it was asserted
before its symmetric declaration.
Deduped by handle and bindings, not by handle. A palindrome — (sibOf Ann Ann),
or any pattern the mirror binds exactly as the direct probe did — is one answer. A
pattern whose arguments are both variables matches one stored fact twice,
differently: (sibOf ?a ?b) over a stored (sibOf Rex Tib) binds ?a Rex, ?b Tib
directly and ?a Tib, ?b Rex through the mirror, and those are two answers about one
handle. A dedup keyed on the handle alone drops the second, so a join led by such a
literal sees one orientation, and which literal leads is a plan decision.
Lazy through the fan: each probe filters against what the earlier probes emitted, and the set handed to the next is not built until a consumer walks past its own hits, so a consumer answered by the direct hits pays for no second probe and no set.
The one definition of the fan and the dedup: raw-match calls it with match-one, the
rete alpha matcher (vaelii.impl.rete) with its alpha-memory probe, so the two
retrieval paths cannot fan differently.
Match a literal by `probe` — `(probe form)` → a seq of `[handle bindings …]`, one literal context — over every argument arrangement the predicate licences: the mirror for a **symmetric** predicate, the other arrangements of the commuting component for a **commutative** one. Only fully-ground symmetric and commuting literals are stored sorted (see `vaelii.impl.sentex`), so the fan is what makes lookup order-insensitive: it retrieves `(siblingOf Ann Carol)` from the pattern `(siblingOf ?x Carol)` or `(siblingOf Carol ?x)` alike, and keeps a fact reachable even if it was asserted before its `symmetric` declaration. **Deduped by handle *and bindings*, not by handle.** A palindrome — `(sibOf Ann Ann)`, or any pattern the mirror binds exactly as the direct probe did — is one answer. A pattern whose arguments are both variables matches one stored fact **twice, differently**: `(sibOf ?a ?b)` over a stored `(sibOf Rex Tib)` binds `?a Rex, ?b Tib` directly and `?a Tib, ?b Rex` through the mirror, and those are two answers about one handle. A dedup keyed on the handle alone drops the second, so a join led by such a literal sees one orientation, and which literal leads is a plan decision. Lazy through the fan: each probe filters against what the earlier probes emitted, and the set handed to the next is not built until a consumer walks past its own hits, so a consumer answered by the direct hits pays for no second probe and no set. The one definition of the fan and the dedup: `raw-match` calls it with `match-one`, the rete alpha matcher (`vaelii.impl.rete`) with its alpha-memory probe, so the two retrieval paths cannot fan differently.
(reader-spelled-by kb sentence reader)The *spelled-by* binding that spells sentence as reader reads it, or nil when the
store's own spelling is the reader's.
The `*spelled-by*` binding that spells `sentence` as `reader` reads it, or nil when the store's own spelling is the reader's.
(representative-in kb visible? term)term's equality-class representative as visible? sees the merges — the global
one when nothing has merged term (the overwhelming case, one map lookup), when the
read is unscoped (visible? nil), or when the reader can see the term's whole class
anyway (tax/class-fully-visible?), which is every KB stating its merges where the
reader can see them. Only a class genuinely split by an invisible edge pays for
scoped-class.
`term`'s equality-class representative as `visible?` sees the merges — the global one when nothing has merged `term` (the overwhelming case, one map lookup), when the read is unscoped (`visible?` nil), or when the reader can see the term's whole class anyway (`tax/class-fully-visible?`), which is every KB stating its merges where the reader can see them. Only a class genuinely split by an invisible edge pays for `scoped-class`.
(representative-term kb visible? term)term with every non-variable symbol replaced by its class representative
(representative-in), recursively — so a merged symbol nested inside a compound is
rewritten at whatever depth it sits.
representative-in alone is a flat lookup: the closure is keyed by symbol, so handing
it a compound returns that compound unchanged and the caller silently compares
unnormalized forms. Every caller that may see a compound wants this one, and the
difference is congruence — with (sameAs Kilogram Kg) believed, (QuantityFn 5 Kilogram) and (QuantityFn 5 Kg) normalize to one term here and to two there.
Mention opacity. Two declarations make a position a mention — a term named as
syntax, rewritten by spelling (rewriteOf) only and never by a sameAs / equals
identity merge, so a quoted term does not fold onto its referent's class. A
quoting_function (Quote, Quasiquote) quotes its arguments; a modal_predicate
(believes, and whatever else is granted) quotes the proposition it attributes,
because an attitude is opaque: from Oedipus believes he married Jocasta and Jocasta is
his mother it does not follow that he believes he married his mother, and the asker's
merges are not his. What the agent's own context merges does apply, and applies where
the projection reads it (provers/BeliefProjectionProver). Gated on tax/mention-marks: a
KB declaring neither takes the plain walk unchanged, two prop reads at entry.
This covers ground congruence, which is what an identity merge does. The oriented
equational rewriting kb/rewrite-term* applies after it (rewrite/normalize-sentence)
is a walk over argument terms that does not read these marks, so a schematic equals
normalizes inside a quoted position as it does outside one. It skips an equality
relation's arguments, the one mention position both halves share.
`term` with every non-variable symbol replaced by its class representative (`representative-in`), **recursively** — so a merged symbol nested inside a compound is rewritten at whatever depth it sits. `representative-in` alone is a flat lookup: the closure is keyed by symbol, so handing it a compound returns that compound unchanged and the caller silently compares unnormalized forms. Every caller that may see a compound wants this one, and the difference is congruence — with `(sameAs Kilogram Kg)` believed, `(QuantityFn 5 Kilogram)` and `(QuantityFn 5 Kg)` normalize to one term here and to two there. **Mention opacity.** Two declarations make a position a *mention* — a term named as syntax, rewritten by *spelling* (`rewriteOf`) only and never by a `sameAs` / `equals` identity merge, so a quoted term does not fold onto its referent's class. A `quoting_function` (`Quote`, `Quasiquote`) quotes its arguments; a `modal_predicate` (`believes`, and whatever else is granted) quotes the **proposition** it attributes, because an attitude is opaque: from *Oedipus believes he married Jocasta* and *Jocasta is his mother* it does not follow that he believes he married his mother, and the asker's merges are not his. What the agent's *own* context merges does apply, and applies where the projection reads it (`provers/BeliefProjectionProver`). Gated on `tax/mention-marks`: a KB declaring neither takes the plain walk unchanged, two prop reads at entry. This covers ground congruence, which is what an identity merge does. The oriented equational rewriting `kb/rewrite-term*` applies after it (`rewrite/normalize-sentence`) is a walk over argument terms that does not read these marks, so a schematic `equals` normalizes inside a quoted position as it does outside one. It skips an equality relation's arguments, the one mention position both halves share.
(resolve-bindings bindings)Fully dereference every variable in a binding map so chained variables (?g -> ?x -> Tom) collapse to their ground value.
Fully dereference every variable in a binding map so chained variables (?g -> ?x -> Tom) collapse to their ground value.
(retired-for? kb visible merged? sentence)Does sentence name a term the reader has retired — i.e. is it not in normal form
for that reader? Asked term by term rather than by building the rewritten sentence,
since the answer is a disjunction and the first displaced symbol settles it, and gated
per symbol on merged? (one contains? against a snapshot held by the caller) so an
unmerged sentence never reaches the election. visible is the caller's delay over
the supporter memo, forced only by a symbol that got that far. Public for the reads
whose match shape without-retired cannot take — qcn-kb/refuted-pairs yields
[handle a b] triples with no sentex at index 2, so it filters with this directly.
A sentence that quotes takes the mention-aware read instead. Inside a quoted
position — a quoting_function's arguments, or the proposition an attitude attributes to
its agent — a symbol is retired by a spelling rename and not by a sameAs / equals
identity merge, which makes the flat per-symbol shortcut unsound there and would retire a
belief nobody renamed. Whether the sentence quotes at all is asked first
(any-mention-position?), so an ordinary sentence in a KB that merely grants believes
keeps the flat read.
An equality relation's arguments are mentions too (equality-mention-heads): a
sameAs merge does not restate (not (sameAs A B)), so the flat read, which would
call B retired, is confirmed against the structural walk before it drops the
sentence. A positive equation is never retired at all (equation?): migration
never restates one, so dropping it would leave a believed equation that no read
returns under any spelling.
Does `sentence` name a term the reader has retired — i.e. is it *not* in normal form for that reader? Asked term by term rather than by building the rewritten sentence, since the answer is a disjunction and the first displaced symbol settles it, and gated per symbol on `merged?` (one `contains?` against a snapshot held by the caller) so an unmerged sentence never reaches the election. `visible` is the caller's **delay** over the supporter memo, forced only by a symbol that got that far. Public for the reads whose match shape `without-retired` cannot take — `qcn-kb/refuted-pairs` yields `[handle a b]` triples with no sentex at index 2, so it filters with this directly. **A sentence that quotes takes the mention-aware read instead.** Inside a quoted position — a `quoting_function`'s arguments, or the proposition an attitude attributes to its agent — a symbol is retired by a *spelling* rename and not by a `sameAs` / `equals` identity merge, which makes the flat per-symbol shortcut unsound there and would retire a belief nobody renamed. Whether the sentence quotes at all is asked first (`any-mention-position?`), so an ordinary sentence in a KB that merely grants `believes` keeps the flat read. **An equality relation's arguments are mentions too** (`equality-mention-heads`): a `sameAs` merge does not restate `(not (sameAs A B))`, so the flat read, which would call `B` retired, is confirmed against the structural walk before it drops the sentence. A positive **equation** is never retired at all (`equation?`): migration never restates one, so dropping it would leave a believed equation that no read returns under any spelling.
(rewrite-rules-in kb visible?)The believed oriented rewrite rules the reader visible? sees (nil: every one). Every
normal form reads its rules here: normal-form, provers/EqualityProver and an
exception's goal rewrite.
The believed oriented rewrite rules the reader `visible?` sees (nil: every one). Every normal form reads its rules here: `normal-form`, `provers/EqualityProver` and an exception's goal rewrite.
(rule-believed? kb handle)May the rule at handle chain — is it believed?
A rule is a sentex, so the fourth invariant holds of it as it holds of a fact: a stored rule is not a believed one. Both chainers reach a rule through the rule index, which posts on storage and knows nothing of belief, so without this a rule whose support has gone on holding conclusions the KB no longer has grounds for — and a derived rule (one a generator stamped out, docs/generators.md) would never come back out of the KB at all, since retracting what licensed it is the only way it can leave.
A sentex the TMS holds no node for is available, not disbelieved: answering "not
believed" of an absence would be reading it as a verdict, where what it says is that
the network was never asked. For a rule that arm is defence rather than a live
case — core/assert-inert refuses a rule (:not-indexable), so a stored rule has
been through an entry point that premised it — and it is worth keeping only because a wrong
answer here is a rule that silently stops firing.
An inert rule is a different thing and is not what this arm is about: it is
believed like any other rule and gated by its :engines alone
(rules/forward-sentex? / backward-sentex?), which is what makes it documentation
rather than an absence (docs/inference.md).
May the rule at `handle` chain — is it believed? A rule is a sentex, so the fourth invariant holds of it as it holds of a fact: a *stored* rule is not a *believed* one. Both chainers reach a rule through the rule index, which posts on storage and knows nothing of belief, so without this a rule whose support has gone on holding conclusions the KB no longer has grounds for — and a **derived** rule (one a generator stamped out, docs/generators.md) would never come back out of the KB at all, since retracting what licensed it is the only way it can leave. A sentex the TMS holds no node for is available, not disbelieved: answering "not believed" of an absence would be reading it as a verdict, where what it says is that the network was never asked. For a **rule** that arm is defence rather than a live case — `core/assert-inert` refuses a rule (`:not-indexable`), so a stored rule has been through an entry point that premised it — and it is worth keeping only because a wrong answer here is a rule that silently stops firing. An **inert rule** is a different thing and is *not* what this arm is about: it is believed like any other rule and gated by its `:engines` alone (`rules/forward-sentex?` / `backward-sentex?`), which is what makes it documentation rather than an absence (docs/inference.md).
(rule-visible-from? kb context rule-ctx)May a rule stored in rule-ctx answer a goal asked from context?
A rule is a sentex, so it is inherited like any other: a context reasons with the
rules its genlCx ancestor set holds and no others. This is the backward dual of
forward chaining refusing to place a conclusion in a context that cannot see the
rule — without it a context proves (ancestorOf Tom Bob) from a rule some
sibling theory wrote, while the forward firing of that same rule correctly
evaporates for want of a placement, and the two chainers disagree about one KB.
An open ?ctx (or nil) is the unscoped path: such a query asks about the KB rather
than from a vantage, exactly as the closure reads read it.
May a rule stored in `rule-ctx` answer a goal asked from `context`? A rule is a sentex, so it is inherited like any other: a context reasons with the rules its `genlCx` ancestor set holds and no others. This is the backward dual of forward chaining refusing to place a conclusion in a context that cannot see the rule — without it a context proves `(ancestorOf Tom Bob)` from a rule some sibling theory wrote, while the *forward* firing of that same rule correctly evaporates for want of a placement, and the two chainers disagree about one KB. An open `?ctx` (or nil) is the unscoped path: such a query asks about the KB rather than from a vantage, exactly as the closure reads read it.
(same-class-in? kb a b context)Do a and b denote one thing as context sees the merges? The context-scoped
twin of tax/same-class?: two terms are one class here only when the edges that merged
them are visible up context's genlCx ancestor set, so a merge behind a supporter the reader
cannot see does not put them in one class for it. A nil or ?var context is unscoped
and gives the global answer tax/same-class? gives — the reads share representative-in,
which is one map lookup until an invisible edge actually splits the class.
Do `a` and `b` denote one thing as `context` sees the merges? The context-scoped twin of `tax/same-class?`: two terms are one class here only when the edges that merged them are visible up `context`'s `genlCx` ancestor set, so a merge behind a supporter the reader cannot see does not put them in one class for it. A nil or `?var` context is unscoped and gives the global answer `tax/same-class?` gives — the reads share `representative-in`, which is one map lookup until an *invisible* edge actually splits the class.
(solve-deferred kb g context)Extension binding-maps for a deferred antecedent g — already substituted, so its
inputs are ground (canonical order and the planner pin it after its binders), computed
by the prover registry through wiring/solve-goal. Nothing when the literal is
inapplicable (unbound inputs, a false test): a deferred literal that yields no solution
simply prunes the branch, the evaluable contract vaelii.impl.plan documents.
This lets this chainer discharge a different / evaluate / unknown antecedent by
computation; matching or rule expansion alone would silently prove nothing for it,
where ask honours it because the registry holds a prover for each, and forward
chaining honours it at the antecedent join. See docs/naf.md.
Extension binding-maps for a deferred antecedent `g` — already substituted, so its inputs are ground (canonical order and the planner pin it after its binders), computed by the prover registry through `wiring/solve-goal`. Nothing when the literal is inapplicable (unbound inputs, a false test): a deferred literal that yields no solution simply prunes the branch, the evaluable contract `vaelii.impl.plan` documents. This lets this chainer discharge a `different` / `evaluate` / `unknown` antecedent by computation; matching or rule expansion alone would silently prove nothing for it, where `ask` honours it because the registry holds a prover for each, and forward chaining honours it at the antecedent join. See docs/naf.md.
(spelling-planner kb)(fn [sentence context]) answering {spelling entries}: each spelling the readers of
sentence, written in context, read it in, with the marks that reader believes, or
nil when every reader believes every mark that sorts it (uniform-marks?) and so reads
the store's own spelling. The fn holds for its own lifetime
one memo of each predicate's marks and whether they are uniform, and one of each
[predicate context]'s readers: a walk over a predicate's rows reads both once.
`(fn [sentence context])` answering `{spelling entries}`: each spelling the readers of
`sentence`, written in `context`, read it in, with the marks that reader believes, or
nil when every reader believes every mark that sorts it (`uniform-marks?`) and so reads
the store's own spelling. The fn holds for its own lifetime
one memo of each predicate's marks and whether they are uniform, and one of each
`[predicate context]`'s readers: a walk over a predicate's rows reads both once.(spelling-readers kb context handles)The readers whose spellings of a fact stated in context can differ, given the
supporters handles of its predicate's marks: context and the contexts where it meets
the contexts that state a hiding defeat or except (hider-contexts,
tax/meet-closure), kept where they see context. A reader below context sees one
of these sets of hiders, so it reads as one of them does.
The readers whose spellings of a fact stated in `context` can differ, given the supporters `handles` of its predicate's marks: `context` and the contexts where it meets the contexts that state a hiding `defeat` or `except` (`hider-contexts`, `tax/meet-closure`), kept where they see `context`. A reader below `context` sees one of these sets of hiders, so it reads as one of them does.
(sub-predicates kb f context)The sub-predicate (genl spec) closure the matching fan-out walks for functor f,
from the vantage context — the global closure when the vantage is a variable or
nil. The single definition every matcher shares (match-pattern,
matches-hierarchical, the rete alpha matcher), so the fan cannot drift between
them: a genl edge invisible from the vantage does not connect a sub-predicate's
facts to the pattern, exactly as it does not appear in the closure reads.
The sub-predicate (genl spec) closure the matching fan-out walks for functor `f`, from the vantage `context` — the global closure when the vantage is a variable or nil. The **single definition every matcher shares** (`match-pattern`, `matches-hierarchical`, the rete alpha matcher), so the fan cannot drift between them: a genl edge invisible from the vantage does not connect a sub-predicate's facts to the pattern, exactly as it does not appear in the closure reads.
(substitute pattern bindings)Replace bound variables in a pattern with their values (recursively). A dotted
rest pattern (head ... . ?rest) is spliced: the substituted tail is concatenated
in, so (?pred . ?args) with ?args=(Tom Bob) becomes (parentOf Tom Bob).
Eager, and a PersistentList. This is the innermost function on every join, every
rule expansion and every proof hop, and what it builds goes straight into
sentex/canon, which flattens any sequential to a PersistentList anyway. Answering
with map's lazy seq would allocate a LazySeq and a Cons per element — each with
a lock the realizing thread takes — for a sequence three to five elements long that is
walked again a microsecond later. mapv fills one transient vector and
PersistentList/create conses it up in reverse, so a substituted literal costs two
eager passes and no lazy machinery at all.
Replace bound variables in a pattern with their values (recursively). A dotted rest pattern `(head ... . ?rest)` is spliced: the substituted tail is concatenated in, so `(?pred . ?args)` with `?args=(Tom Bob)` becomes `(parentOf Tom Bob)`. **Eager, and a `PersistentList`.** This is the innermost function on every join, every rule expansion and every proof hop, and what it builds goes straight into `sentex/canon`, which flattens any sequential to a `PersistentList` anyway. Answering with `map`'s lazy seq would allocate a `LazySeq` *and* a `Cons` per element — each with a lock the realizing thread takes — for a sequence three to five elements long that is walked again a microsecond later. `mapv` fills one transient vector and `PersistentList/create` conses it up in reverse, so a substituted literal costs two eager passes and no lazy machinery at all.
(subsuming-unify kb goal consequent)(subsuming-unify kb goal consequent bindings)(subsuming-unify kb goal consequent bindings context)Unify a query goal against a rule's consequent, honoring predicate
specificity: a consequent whose functor is a spec (sub-predicate/subtype, via
the genl closure) of the goal's functor still answers the goal, so its argument
lists unify and the goal variable binds to the more specific instance. This is the
backward dual of match1 — where a subtype fact satisfies a supertype antecedent,
here a subtype conclusion satisfies a supertype goal.
Equal functors (the common case), a variable goal functor, or a functor with no
sub-predicates all fall through to a plain unify over the whole sentences, so
nothing changes for a KB without predicate-genl edges, and a rule concluding a
supertype or an unrelated predicate is correctly rejected (the functors do not
unify).
Under a negation the fan reverses, exactly as it does in match1: a rule
concluding (not (animal ?x)) answers the goal (not (dog Tom)), because dog ⊑ animal entails ¬animal ⊑ ¬dog. Both sides must be negations; a negated goal
against a positive consequent falls through to the plain unify, which rejects it on
the functor.
Scoped in lockstep with match1 (its forward twin): with a context, the
predicate-genl closure is walked only through the edges that context can see. The
backward callers already scope the candidate rule set upstream
(concluding-rule-handles … context, via provers/candidate-rules), which reads the
same scoped closure — so passing the context here changes no answer today, and keeps
a future caller that skips that filter from subsuming through an invisible edge. The
arities without a context are unscoped, for a caller with no vantage in hand.
Unify a query `goal` against a rule's `consequent`, honoring **predicate specificity**: a consequent whose functor is a *spec* (sub-predicate/subtype, via the genl closure) of the goal's functor still answers the goal, so its argument lists unify and the goal variable binds to the more specific instance. This is the backward dual of `match1` — where a subtype *fact* satisfies a supertype antecedent, here a subtype *conclusion* satisfies a supertype goal. Equal functors (the common case), a variable goal functor, or a functor with no sub-predicates all fall through to a plain `unify` over the whole sentences, so nothing changes for a KB without predicate-genl edges, and a rule concluding a *supertype* or an unrelated predicate is correctly rejected (the functors do not unify). **Under a negation the fan reverses**, exactly as it does in `match1`: a rule concluding `(not (animal ?x))` answers the goal `(not (dog Tom))`, because `dog ⊑ animal` entails `¬animal ⊑ ¬dog`. Both sides must be negations; a negated goal against a positive consequent falls through to the plain `unify`, which rejects it on the functor. **Scoped in lockstep with `match1`** (its forward twin): with a `context`, the predicate-genl closure is walked only through the edges that context can see. The backward callers already scope the *candidate rule set* upstream (`concluding-rule-handles … context`, via `provers/candidate-rules`), which reads the same scoped closure — so passing the context here changes no answer today, and keeps a future caller that skips that filter from subsuming through an invisible edge. The arities without a context are unscoped, for a caller with no vantage in hand.
(super-predicates kb f context)The genl closure of f from the vantage context: sub-predicates mirrored,
and what a negative pattern fans over.
A genl edge carries the opposite way through a negation — dog ⊑ animal puts
(dog Muffet) under the pattern (animal ?x) and (not (animal Muffet)) under the
pattern (not (dog ?x)) — so the negative fan walks up where the positive one walks
down. The up set is bounded by the hierarchy's depth where the down set is a whole
subtree, which is why the negative fan is the cheaper of the two on a broad ontology
and the positive one is the fan the retrieval paths are written around. Shared by
match-pattern and the rete alpha matcher for the same reason sub-predicates is:
so the two cannot drift.
The **genl** closure of `f` from the vantage `context`: `sub-predicates` mirrored, and what a *negative* pattern fans over. A `genl` edge carries the opposite way through a negation — `dog ⊑ animal` puts `(dog Muffet)` under the pattern `(animal ?x)` and `(not (animal Muffet))` under the pattern `(not (dog ?x))` — so the negative fan walks up where the positive one walks down. The up set is bounded by the hierarchy's depth where the down set is a whole subtree, which is why the negative fan is the cheaper of the two on a broad ontology and the positive one is the fan the retrieval paths are written around. Shared by `match-pattern` and the rete alpha matcher for the same reason `sub-predicates` is: so the two cannot drift.
(supporter-believed? kb handle context)(supporter-believed? kb handle context defeats?)Is stored supporter handle believed from context — IN in the network, and not
hidden there by a believed except or a placed defeat in force at context, or by
resting only on a hidden handle (exc/excepted?, the read walk)? defeats? false
reads the excepts alone (exc/excepted-in-network?).
The taxonomy's visible? callback (kb/attach-visibility!), so it decides whether a
closure walk may cross an edge. Both kinds of hiding apply: a context that
disbelieves a genl edge must stop reaching over it, or believed? of the edge and
genl? / isa? / ask? over it answer differently about one KB from one context.
What the callback may ask, and why the recursion does not close. Every ancestor-set
read inside exc/excepted? goes through tax/context-up-global — exc/except-hidden-fn,
exc/visible-exception-index and the read walk's exc/reader-state each take it by name — so asking it from
inside a scoped walk reads the unfiltered genlCx closure and never re-enters the
filtered one. That holds for a :genlCx read as much as for a :genl one, and it is
the same reason exception evaluation reads that closure rather than context-up. The
read walk runs jtms/region-in, which reads justifications alone and requires no
taxonomy.
Assertion-context inheritance is still not answered here: taxonomy's scoped edge/cache readers already apply it, and genlCx declarations are forced universal.
Is stored supporter `handle` believed from `context` — IN in the network, and not hidden there by a believed `except` or a placed `defeat` in force at `context`, or by resting only on a hidden handle (`exc/excepted?`, the read walk)? `defeats?` false reads the excepts alone (`exc/excepted-in-network?`). The taxonomy's `visible?` callback (`kb/attach-visibility!`), so it decides whether a closure walk may cross an edge. Both kinds of hiding apply: a context that disbelieves a `genl` edge must stop reaching over it, or `believed?` of the edge and `genl?` / `isa?` / `ask?` over it answer differently about one KB from one context. **What the callback may ask, and why the recursion does not close.** Every ancestor-set read inside `exc/excepted?` goes through `tax/context-up-global` — `exc/except-hidden-fn`, `exc/visible-exception-index` and the read walk's `exc/reader-state` each take it by name — so asking it from inside a scoped walk reads the *unfiltered* genlCx closure and never re-enters the filtered one. That holds for a `:genlCx` read as much as for a `:genl` one, and it is the same reason exception evaluation reads that closure rather than `context-up`. The read walk runs `jtms/region-in`, which reads justifications alone and requires no taxonomy. Assertion-context inheritance is still not answered here: taxonomy's scoped edge/cache readers already apply it, and genlCx declarations are forced universal.
(supporter-visible? kb handle context)(supporter-visible? kb handle context defeats?)Is stored supporter handle believed, inherited, and not excepted from context?
defeats? false leaves the placed defeats unread (supporter-believed?), as a
firing's placement reads them.
Is stored supporter `handle` believed, inherited, and not excepted from `context`? `defeats?` false leaves the placed defeats unread (`supporter-believed?`), as a firing's placement reads them.
(term-depth form)How deeply form's arguments nest compound terms: 0 for a flat literal (p A), 1
for (p (SuccFn A)), 2 for (p (SuccFn (SuccFn A))). The second half of the loop
guard (default-max-term-growth): a goal key keeps its ground arguments, so a rule
that wraps a function around a head variable mints a fresh key per expansion and the
key alone never repeats. One pass over the arguments; a flat goal reads each once.
How deeply `form`'s arguments nest compound terms: 0 for a flat literal `(p A)`, 1 for `(p (SuccFn A))`, 2 for `(p (SuccFn (SuccFn A)))`. The second half of the loop guard (`default-max-term-growth`): a goal key keeps its ground arguments, so a rule that wraps a function around a head variable mints a fresh key per expansion and the key alone never repeats. One pass over the arguments; a flat goal reads each once.
(uniform-marks? kb entries)Does every reader believe every mark in entries (mark-entries): each has a
supporter held-everywhere?? The four permuting marks are read from every context
(docs/contexts.md, "A context outside the spindle"), so only a defeat or an except
makes two readers read one fact differently.
Does every reader believe every mark in `entries` (`mark-entries`): each has a supporter `held-everywhere?`? The four permuting marks are read from every context (docs/contexts.md, "A context outside the spindle"), so only a defeat or an except makes two readers read one fact differently.
(unify x y)(unify x y bindings)Unify x and y under bindings, returning an extended binding map or nil.
Supports dotted rest patterns: a sublist (. ?rest) binds ?rest to the whole
remaining sequence, so (?pred . ?args) unifies with (parentOf Tom Bob) giving
?pred=parentOf, ?args=(Tom Bob).
Unify x and y under `bindings`, returning an extended binding map or nil. Supports dotted rest patterns: a sublist `(. ?rest)` binds `?rest` to the whole remaining sequence, so `(?pred . ?args)` unifies with `(parentOf Tom Bob)` giving `?pred=parentOf`, `?args=(Tom Bob)`.
(visible-supporter-fn kb context)handle -> boolean, memoized: is the sentex handle believed, inherited by
context, and not hidden there by a visibility exception? nil when context is nil
or a ?var — the unscoped path, which every caller reads as no filter rather than
as nothing visible.
The dynamic var a context-scoped equality read hangs on: the equality partition records its supporters as handles, and only the record store knows where each was asserted.
`handle -> boolean`, memoized: is the sentex `handle` believed, inherited by `context`, and not hidden there by a visibility exception? nil when `context` is nil or a `?var` — the unscoped path, which every caller reads as *no filter* rather than as *nothing visible*. The dynamic var a **context-scoped equality** read hangs on: the equality partition records its supporters as handles, and only the record store knows where each was asserted.
(without-retired kb view-context matches)Drop the matches whose stored spelling view-context has retired — the
reader-scoped half of supersession.
jtms/superseded holds a spelling out of belief once its own context elects another,
and that is per datum: a sentex lives in one context, so one flag answers for one
context. Staleness is per reader. A fact stated above a merge is believed where it
lives — its own context was told nothing — while a context below the merge sees both it
and the twin migration placed there, and would otherwise report one fact twice, under
two names it knows denote one thing. This drops the spelling that reader has retired
and leaves the one it elected, which is what makes a count over an answer set mean
something (docs/equality.md).
Gated on the closure being non-empty, so a KB that has merged nothing — every KB
until somebody states an equality — pays one deref for the whole query, and one that
has pays a contains? per symbol of each match against a snapshot taken once here,
before anything else runs. The scoped-supporter memo is built behind a delay, since
most matches in a KB with a handful of merges name none of the merged terms and the
question never reaches it. A variable or nil view-context is the unscoped read and
filters nothing: it asks about the KB rather than from a vantage, exactly as the class
reads do.
Drop the matches whose stored spelling `view-context` has **retired** — the reader-scoped half of supersession. `jtms/superseded` holds a spelling out of belief once its own context elects another, and that is per *datum*: a sentex lives in one context, so one flag answers for one context. Staleness is per *reader*. A fact stated above a merge is believed where it lives — its own context was told nothing — while a context below the merge sees both it and the twin migration placed there, and would otherwise report one fact twice, under two names it knows denote one thing. This drops the spelling that reader has retired and leaves the one it elected, which is what makes a count over an answer set mean something (docs/equality.md). **Gated on the closure being non-empty**, so a KB that has merged nothing — every KB until somebody states an equality — pays one deref for the whole query, and one that has pays a `contains?` per symbol of each match against a snapshot taken once here, before anything else runs. The scoped-supporter memo is built behind a `delay`, since most matches in a KB with a handful of merges name none of the merged terms and the question never reaches it. A variable or nil `view-context` is the unscoped read and filters nothing: it asks about the KB rather than from a vantage, exactly as the class reads do.
(without-unbelieved-spellings kb view-context goal matches)Drop the matches of goal whose spelling view-context does not read: a row stored as
written that the marks the reader believes sort otherwise, a row read in an argument
order those marks do not license, and a row spelled by a reifiable_function mark the
reader takes the other way (reified-reading). A match of a permuting predicate stays
when the marks the reader believes spell the fact it reads to the stored row. Gated on
a permuting or reifiable mark stored at all, and per predicate on a mark some reader
does not believe (uniform-marks?); a variable or nil view-context filters nothing.
Drop the matches of `goal` whose spelling `view-context` does not read: a row stored as written that the marks the reader believes sort otherwise, a row read in an argument order those marks do not license, and a row spelled by a `reifiable_function` mark the reader takes the other way (`reified-reading`). A match of a permuting predicate stays when the marks the reader believes spell the fact it reads to the stored row. Gated on a permuting or reifiable mark stored at all, and per predicate on a mark some reader does not believe (`uniform-marks?`); a variable or nil `view-context` filters nothing.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |