The node engine's search policy — one additive estimate whose terms carry signs the
caller picks, so vaelii.impl.inference searches breadth-first, depth-first or best-first
without a second driver. The frontier is a priority queue precisely so that changing a
number is enough; this namespace is that number.
estimate(node) = Σ literal-cost(Lᵢ) what the conjunction costs
+ size-penalty × |literals| shorter conjunctions first
+ depth-sign × depth-weight × Σ dᵢ rewriting allowance left
+ tree-sign × tree-weight × tree-depth search-tree level
The base term is the KB's own cost model, not a second one. It is
plan/explain's per-literal estimate summed — the count-aware trie model with sideways
information passing that already orders every join in the engine, so a conjunction is
costed here exactly as core/query-plan reports it. One model, two readers; a node
ordering that disagreed with the plan it is about to run would be a cost model arguing
with itself.
The signs are the whole personality of the search. Σ dᵢ is what a node is still permitted to rewrite, so a negative depth sign prefers the node with the most room left and a positive one the node closest to spending it — a node nearly out of allowance is a node nearly ground, hence nearly answerable by facts alone. The tree term is the analogous choice over the search tree rather than the rewriting budget: positive is level order, negative is a dive.
Ordering is a cost decision and never a semantic one. Every tactician here
returns the same answer set; what differs is when. inference_tactics_test's
completeness sweep is the gate that keeps it that way, and the one mode that
deliberately returns fewer answers (:first-result?) says so in its own docstring and
is excluded from that sweep by name. The join inside a node is ordered by
plan/order alone and never by the strategy, for the same reason: a complete search
has to visit the same literals whatever order the nodes pop in.
See docs/inference.md.
The node engine's search **policy** — one additive estimate whose terms carry signs the
caller picks, so `vaelii.impl.inference` searches breadth-first, depth-first or best-first
without a second driver. The frontier is a priority queue precisely so that changing a
number is enough; this namespace is that number.
estimate(node) = Σ literal-cost(Lᵢ) what the conjunction costs
+ size-penalty × |literals| shorter conjunctions first
+ depth-sign × depth-weight × Σ dᵢ rewriting allowance left
+ tree-sign × tree-weight × tree-depth search-tree level
**The base term is the KB's own cost model, not a second one.** It is
`plan/explain`'s per-literal estimate summed — the count-aware trie model with sideways
information passing that already orders every join in the engine, so a conjunction is
costed here exactly as `core/query-plan` reports it. One model, two readers; a node
ordering that disagreed with the plan it is about to run would be a cost model arguing
with itself.
**The signs are the whole personality of the search.** Σ dᵢ is what a node is still
*permitted* to rewrite, so a negative depth sign prefers the node with the most room
left and a positive one the node closest to spending it — a node nearly out of
allowance is a node nearly ground, hence nearly answerable by facts alone. The tree
term is the analogous choice over the search tree rather than the rewriting budget:
positive is level order, negative is a dive.
**Ordering is a cost decision and never a semantic one.** Every tactician here
returns the same answer set; what differs is when. `inference_tactics_test`'s
completeness sweep is the gate that keeps it that way, and the one mode that
deliberately returns fewer answers (`:first-result?`) says so in its own docstring and
is excluded from that sweep by name. The join *inside* a node is ordered by
`plan/order` alone and never by the strategy, for the same reason: a complete search
has to visit the same literals whatever order the nodes pop in.
See docs/inference.md.(auto-strategy kb goals context depth)A tactician (or :portfolio) picked from the shape of the query, for a caller who
has no opinion. One index read and no search: the point is to cost less than the
first node expansion it is choosing for.
Opt-in (:auto?). A caller who names a strategy has already answered this.
A tactician (or `:portfolio`) picked from the *shape* of the query, for a caller who has no opinion. One index read and no search: the point is to cost less than the first node expansion it is choosing for. - no rewriting allowance at all — the root is the whole search, and ordering a frontier of one decides nothing; - a conjunction, or a single literal several rules conclude — more than one plausible route, which is what a portfolio is a bet on; - a single literal with one route — nothing to hedge, so dive. Opt-in (`:auto?`). A caller who names a strategy has already answered this.
(backchain-estimate kb goal context)(backchain-estimate kb
goal
context
{:keys [aggregate depth seen]
:or {aggregate :first depth 2 seen #{}}})What proving goal through the rules that conclude it is expected to cost, or
nil when no rule concludes it and the direct estimate is the whole story.
A literal whose only route is an expensive backchain is costed by the index at its own fan-out, which for a predicate with no stored facts at all is zero — the most expensive literal in the conjunction ranked as the cheapest. This asks the rules instead: unify the goal with each candidate consequent and cost that rule's antecedents, recursively.
:aggregate is the choice between two honest readings of several candidate rules.
:first takes the min — any one rule suffices, so the cheapest route is what the
goal costs. :all takes the sum — a complete search runs every candidate, so
they all get paid for.
Strictly more expensive to compute than a direct estimate, and recursive, which is why
it is opt-in (:estimate-backchain?), bounded by :depth, and consulted only for a
literal that still has rewriting allowance. seen caps it at a repeated goal
(res/goal-key, so two goals differing only in variable names are one), which is
what makes it terminate on a cyclic rule set.
What proving `goal` *through the rules that conclude it* is expected to cost, or **nil** when no rule concludes it and the direct estimate is the whole story. A literal whose only route is an expensive backchain is costed by the index at its own fan-out, which for a predicate with no stored facts at all is zero — the most expensive literal in the conjunction ranked as the cheapest. This asks the rules instead: unify the goal with each candidate consequent and cost that rule's antecedents, recursively. `:aggregate` is the choice between two honest readings of several candidate rules. `:first` takes the **min** — any one rule suffices, so the cheapest route is what the goal costs. `:all` takes the **sum** — a complete search runs every candidate, so they all get paid for. Strictly more expensive to compute than a direct estimate, and recursive, which is why it is opt-in (`:estimate-backchain?`), bounded by `:depth`, and consulted only for a literal that still has rewriting allowance. `seen` caps it at a repeated goal (`res/goal-key`, so two goals differing only in variable names are one), which is what makes it terminate on a cyclic rule set.
(base-estimate kb node context strat)The estimate's base term: what this node's conjunction costs to solve.
plan/explain in one call, summed — so each literal is estimated under the variables
the literals ahead of it bind, exactly as the join will run, and the number equals what
core/query-plan prints for the same conjunction.
With :estimate-backchain? set, a literal that still has rewriting allowance is costed
through its concluding rules instead, and falls back to the index model when no rule
concludes it.
The estimate's **base term**: what this node's conjunction costs to solve. `plan/explain` in one call, summed — so each literal is estimated under the variables the literals ahead of it bind, exactly as the join will run, and the number equals what `core/query-plan` prints for the same conjunction. With `:estimate-backchain?` set, a literal that still has rewriting allowance is costed through its concluding rules instead, and falls back to the index model when no rule concludes it.
(child-bias strat productive?)The additive bias this node's children carry into the frontier — zero unless the tactician has an opinion about a node that already produced answers.
A large additive number rather than a reordering: +bias sinks a child behind
everything in the frontier without dropping it, −bias hoists it above everything.
The bias applies to the children of a productive node only, which is the one
removal-versus-transformation distinction this engine has to offer — a node solves its
conjunction inline and rewrites it into children in the same step, so there are no two
classes of child to choose between, only two readings of a parent that is paying:
finish it, or chase it.
Complete either way — a biased child is expanded, just later or sooner — so both tacticians that use this are in the completeness sweep.
The additive bias this node's children carry into the frontier — zero unless the tactician has an opinion about a node that already produced answers. A **large** additive number rather than a reordering: `+bias` sinks a child behind everything in the frontier without dropping it, `−bias` hoists it above everything. The bias applies to the children of a *productive* node only, which is the one removal-versus-transformation distinction this engine has to offer — a node solves its conjunction inline and rewrites it into children in the same step, so there are no two classes of child to choose between, only two readings of a parent that is paying: finish it, or chase it. Complete either way — a biased child is expanded, just later or sooner — so both tacticians that use this are in the completeness sweep.
(complete? strat)Does this strategy return the whole answer set?
Every tactician only reorders, so the answer is yes unless :first-result? is on —
the one mode that stops the search rather than steering it.
Does this strategy return the whole answer set? Every tactician only reorders, so the answer is yes unless `:first-result?` is on — the one mode that stops the search rather than steering it.
The strategy a session runs under when a caller names none.
:ground-first, on the measurement (lein bench-tactics). It is the only
tactician that is best-or-tied on every column measured: 0.47× the default's time to a
first answer, 0.93× to fifty of them, the fastest node ordering on a needle at
every depth tried, and 1.00× on an exhaustive run, where nothing can differ. Preferring
the node closest to spending its rewriting allowance means preferring the node closest
to being ground, and a ground conjunction is one facts can answer.
:cost — both signs zero, the base term and the size penalty alone — is the identity
policy, and stays available for a caller who wants the ordering to follow the cost model
and nothing else.
The weights are large next to a typical base term on purpose: a sign that only broke
ties would not be a strategy. :breadth-bias scales the depth term alone, for tuning
the one weight that decides how far the search commits before it reconsiders.
The strategy a session runs under when a caller names none. **`:ground-first`, on the measurement** (`lein bench-tactics`). It is the only tactician that is best-or-tied on every column measured: 0.47× the default's time to a **first** answer, 0.93× to fifty of them, the fastest node ordering on a needle at every depth tried, and 1.00× on an exhaustive run, where nothing can differ. Preferring the node closest to spending its rewriting allowance means preferring the node closest to being ground, and a ground conjunction is one facts can answer. `:cost` — both signs zero, the base term and the size penalty alone — is the identity policy, and stays available for a caller who wants the ordering to follow the cost model and nothing else. The weights are large next to a typical base term on purpose: a sign that only broke ties would not be a strategy. `:breadth-bias` scales the depth term alone, for tuning the one weight that decides how far the search commits before it reconsiders.
(estimate kb strat node)What node is expected to cost, under strat. Lower pops first.
Runs once per node, at enqueue. That is the whole reason :estimate-backchain? is
off by default: the base term is index reads, and a sub-search per enqueued node would
make choosing what to expand cost more than expanding it.
What `node` is expected to cost, under `strat`. Lower pops first. Runs once per node, at enqueue. That is the whole reason `:estimate-backchain?` is off by default: the base term is index reads, and a sub-search per enqueued node would make choosing what to expand cost more than expanding it.
The most any one literal may contribute to the base term.
The index model answers a large finite number for a literal it cannot bound at all, and a conjunction of those must not sum into a cost that swamps the sign terms — the ordering would stop being a policy and become a saturation. Clamping per literal keeps the base term comparable with the weights below.
The most any one literal may contribute to the base term. The index model answers a large finite number for a literal it cannot bound at all, and a conjunction of those must not sum into a cost that swamps the sign terms — the ordering would stop being a policy and become a saturation. Clamping per literal keeps the base term comparable with the weights below.
(solved-form {:keys [literals]})The node's conjunction as it will actually be solved, paired with the rewriting allowance each literal still carries.
Nothing is applied here: a node's literals already carry every unifier taken to reach it, because a rewrite substitutes into them. The conjunction is the question as it now stands, which is what the estimate has to cost.
The node's conjunction as it will actually be solved, paired with the rewriting allowance each literal still carries. Nothing is applied here: a node's literals already carry every unifier taken to reach it, because a rewrite substitutes into them. The conjunction *is* the question as it now stands, which is what the estimate has to cost.
(strategy s)Normalize s — a tactician keyword, a full or partial strategy map, or nil — into the
map the engine reads. An explicit sign in the map overrides the tactician's, so a
caller may name a tactician and then bend one term of it.
Normalize `s` — a tactician keyword, a full or partial strategy map, or nil — into the map the engine reads. An explicit sign in the map overrides the tactician's, so a caller may name a tactician and then bend one term of it.
A tactician is a pair of signs and a child bias, nothing more.
:cost the cheapest conjunction first, and nothing else
:budget-first the node with the most rewriting allowance left
:ground-first the node closest to having spent it, hence nearest to ground —
the default, on the measurement (see defaults)
:breadth-first level order over the search tree
:depth-first the deepest node first — a dive
:removal-first a productive node's children sink: finish what is paying
:transformation-first a productive node's children rise: chase what is paying
The last two act through the child bias rather than the node estimate (child-bias),
because what they choose between is not two numbers on one node but which of two nodes
a parent's answers should recommend. All seven are complete: each reorders the
frontier and none of them drops a node.
A tactician is a pair of signs and a child bias, nothing more.
:cost the cheapest conjunction first, and nothing else
:budget-first the node with the most rewriting allowance left
:ground-first the node closest to having spent it, hence nearest to ground —
the default, on the measurement (see `defaults`)
:breadth-first level order over the search tree
:depth-first the deepest node first — a dive
:removal-first a productive node's children sink: finish what is paying
:transformation-first a productive node's children rise: chase what is paying
The last two act through the child bias rather than the node estimate (`child-bias`),
because what they choose between is not two numbers on one node but which of two nodes
a *parent's* answers should recommend. All seven are complete: each reorders the
frontier and none of them drops a node.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 |