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 Fido).
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 Fido)`. 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.
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 [:argument-root pos term] indexes exactly
that later position, so it answers the same pattern with a single set read.
When several arguments are known, candidate-handles intersects the functor root
with every ground argument root (sentexes-with-args, one set 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 `[:argument-root pos term]` indexes exactly that later position, so it answers the same pattern with a single set read. When several arguments are known, `candidate-handles` intersects the functor root with *every* ground argument root (`sentexes-with-args`, one set 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.
An optional observer of the DFS's dead ends — (fn [goal depth]) — or nil, the
default.
A dead end is a subgoal the search could neither match nor expand: no visible
believed fact unified with it, and no rule concluding it unified either. It is
reported only when the branch was not merely cut short — by the per-path loop
guard or by :max-depth — and that distinction is the whole of what makes the
callback worth having. A truncated branch is a search that ran out of budget; a
dead end is a search that ran out of knowledge, and only the second names something
the KB could be told (vaelii.impl.abduce, docs/abduction.md).
The goal handed over is already substituted under the frame's bindings, so what the
observer sees is the literal that failed. Its return value is ignored: this is a
sink, not a filter, so an observed run and an unobserved one take byte-identical
paths and abduce gets the very search prove runs rather than a variant of it.
Only the DFS reports. backward is lazy — its dead ends would be discovered
whenever a consumer happened to realize the seq, and the thread binding would
already be gone — so abduction rides prove, which is a loop.
nil costs one var deref per exhausted subgoal.
An optional observer of the DFS's **dead ends** — `(fn [goal depth])` — or nil, the default. A dead end is a subgoal the search could neither match nor expand: no visible believed fact unified with it, and no rule concluding it unified either. It is reported only when the branch was not merely **cut short** — by the per-path loop guard or by `:max-depth` — and that distinction is the whole of what makes the callback worth having. A truncated branch is a search that ran out of *budget*; a dead end is a search that ran out of *knowledge*, and only the second names something the KB could be told (`vaelii.impl.abduce`, docs/abduction.md). The goal handed over is already substituted under the frame's bindings, so what the observer sees is the literal that failed. Its return value is ignored: this is a **sink, not a filter**, so an observed run and an unobserved one take byte-identical paths and `abduce` gets the very search `prove` runs rather than a variant of it. Only the DFS reports. `backward` is lazy — its dead ends would be discovered whenever a consumer happened to realize the seq, and the thread binding would already be gone — so abduction rides `prove`, which is a loop. nil costs one var deref per exhausted subgoal.
An optional override for how the backward chainers evaluate a deferred
antecedent — (fn [kb goal context] -> seq of extension binding-maps). nil (the
default) uses the prover registry through wiring/solve-goal; a caller may bind this to
substitute a different evaluator (a test, a restricted registry). See
solve-deferred and docs/naf.md.
An optional **override** for how the backward chainers evaluate a deferred antecedent — `(fn [kb goal context] -> seq of extension binding-maps)`. nil (the default) uses the prover registry through `wiring/solve-goal`; a caller may bind this to substitute a different evaluator (a test, a restricted registry). See `solve-deferred` and docs/naf.md.
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 now lazy (lead-candidates), so it
short-circuits an existence check like the fan-out does while collapsing the fan-out's
product to one argument-root lookup — strictly cheaper, and flat where the fan-out is
O(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 now lazy (`lead-candidates`), so it short-circuits an existence check like the fan-out does while collapsing the fan-out's product to one argument-root lookup — strictly cheaper, and flat where the fan-out is O(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.
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.
(concluding-rule-handles kb pred)(concluding-rule-handles kb pred context)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 (small) spec closure and probe the consequent
index, so cost scales with the number of concluding rules, never the taxonomy. A
variable or non-symbol pred cannot be a type, so it degrades to the plain lookup.
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.
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 (small) spec closure and probe the consequent index, so cost scales with the number of concluding rules, never the taxonomy. A variable or non-symbol `pred` cannot be a type, so it degrades to the plain lookup. 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.
(excepted-handles kb view-context)The handles hidden from view-context by believed (except (sentexHandle H))
facts: an except asserted in a context view-context sees (its genlContext
up-closure) hides its target there and in every descendant. Empty — the common,
fast-path case — when nothing is excepted, or when view-context is a variable (an
except in some microtheory hides its target there and below, not from the more
general contexts above it, so an any-context read still sees it).
Storage-cheap: gated on the except functor root's cardinality, so a KB with no
except pays a single count and returns #{}.
The handles hidden from `view-context` by believed `(except (sentexHandle H))`
facts: an `except` asserted in a context `view-context` sees (its genlContext
up-closure) hides its target there and in every descendant. Empty — the common,
fast-path case — when nothing is excepted, or when `view-context` is a variable (an
`except` in some microtheory hides its target *there and below*, not from the more
general contexts above it, so an any-context read still sees it).
Storage-cheap: gated on the `except` functor root's cardinality, so a KB with no
`except` pays a single count and returns `#{}`.(form-variables form)Every variable anywhere in form, as a set.
Every variable anywhere in `form`, as a 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-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.
(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, and the answer variables — the query's own,
which every frame below inherits unchanged.
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.
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
seam, 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, and the **answer variables** — the query's own, which every frame below inherits unchanged. 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. 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 seam, 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 property read is global on purpose: a sentex has one key, so whether a predicate sorts its arguments cannot vary by who is asking — a reader-scoped read here would store one literal under two keys and break dedup, retraction, and the mirror probe at once.
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 property read is **global on purpose**: a sentex has one key, so whether a predicate sorts its arguments cannot vary by who is asking — a reader-scoped read here would store one literal under two keys and break dedup, retraction, and the mirror probe at once.
(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.
(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 Fido)) 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).
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 cone 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 Fido)`) 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). 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 cone once) would disagree.
(match1 kb antecedent fact)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 Fido). 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.
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 Fido)`. 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.
(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 one argument-root lookup plus
in-memory predicate/context filtering instead of the |specs| × |context-up|
product of trie walks. Falls back to matches-visible for any shape it does not
handle.
The set-algebra twin of `matches-visible` for a positive literal: the identical `[handle bindings stored]` set, but reached by one argument-root lookup plus in-memory predicate/context filtering instead of the `|specs| × |context-up|` product of trie walks. Falls back to `matches-visible` for any shape it does not handle.
(matches-visible kb sentence view-context)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 genlContext 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, and (since forward chaining joins through this) the derivation
side too.
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). The two 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 that is a thing retrieval_completeness_test checks — 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 it has always
been.
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 genlContext 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, and (since forward chaining joins through this) the derivation side too. 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`). The two 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 that is a thing `retrieval_completeness_test` checks — 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 it has always been.
(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).
(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)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, so recursion terminates. 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.
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, so recursion terminates. 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.
(prove-from kb
rules-fn
context
{:keys [deadline max-results max-depth 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
:max-results stop once this many solutions are in hand
:max-depth do not expand a rule past this rule-expansion depth
: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.
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
:max-results stop once this many solutions are in hand
:max-depth do not expand a rule past this rule-expansion depth
: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.(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 genlContext inheritance, no subtype
fan-out — trying both argument orders for a symmetric predicate. Only
fully-ground symmetric literals are stored sorted (see vaelii.impl.sentex), so the
mirrored probe 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. Results are deduped by handle, so a palindrome matches once.
Lazy through the mirror: lazy-cat defers the second probe and the seen set
that dedupes it, so a consumer answered by the direct hits never pays for either.
Match a literal in one **literal** context — no genlContext inheritance, no subtype fan-out — trying **both argument orders for a symmetric predicate**. Only fully-ground symmetric literals are stored sorted (see `vaelii.impl.sentex`), so the mirrored probe 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. Results are deduped by handle, so a palindrome matches once. Lazy through the mirror: `lazy-cat` defers the second probe *and* the `seen` set that dedupes it, so a consumer answered by the direct hits never pays for either.
(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`.
(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.
(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 genlContext up-cone 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 microtheory 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 `genlContext` up-cone 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 microtheory 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.
(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). Uses
*deferred-solver* if a caller has bound one, else the registry. 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). Uses `*deferred-solver*` if a caller has bound one, else the registry. 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.
(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).
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)`.
(subsuming-unify kb goal consequent)(subsuming-unify kb goal consequent bindings)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).
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).
(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: does context see the context the sentex handle
was asserted from? nil when context is nil or a ?var — the unscoped path, which
every caller reads as no filter rather than as nothing visible.
The seam 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: does `context` see the context the sentex `handle` was asserted from? nil when `context` is nil or a `?var` — the unscoped path, which every caller reads as *no filter* rather than as *nothing visible*. The seam 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-excepted kb view-context matches)Drop the [handle …] matches whose handle is hidden from view-context by a
believed except — the visibility-removal filter, a no-op (identical seq) when
nothing is excepted.
Drop the `[handle …]` matches whose handle is hidden from `view-context` by a believed `except` — the visibility-removal filter, a no-op (identical seq) when nothing is excepted.
(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.
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 |