A backward chainer whose state is a set of nodes ordered by cost — not
vaelii.impl.chain's forward agenda, which is a queue of newly believed data
waiting to be matched against rules. This one runs from a query towards the facts,
and what its agenda holds is unfinished proofs.
The other backward chainer is path-structured, walking an explicit goal stack
(res/prove-from). Here
the unit is a node — a whole conjunction plus everything accumulated to reach it —
and expanding one is a single rewrite:
node: [ L₁ … Lᵢ … Lₙ ] σ
rule: A₁…Aₖ ⟹ C, with b = unify(Lᵢ, C)
child: [ b(L₁) … b(Aᵢ…) … b(Lₙ) ] σ ∪ b
The rule's antecedents under the head unifier are the residual — what is left to
prove if this rule is the one that fires — spliced in where Lᵢ was. Applied
repeatedly, that transformation is the whole search: every node is the query rewritten
through some sequence of rules, and a node whose conjunction solves against facts
alone is a completed proof.
Two things follow from the state being a value rather than a call stack. A stop
between two expansions leaves an agenda, not a continuation closure, so a bounded
run is budget/collect over the result stream and nothing else. And the tree is an
artifact that outlives the search, which is where dead ends and "why did this cost so
much" answers come from.
A third follows from the frontier being a priority queue: which node pops next is a
policy rather than a structure, and it lives in vaelii.impl.tactics — one additive
estimate whose signs the caller picks. Every tactician returns the same answer set;
what differs is when.
What it is good at, measured. The residual stays symbolic — (anc ?y ?z) is
not re-asked once per binding of ?y, it is rewritten once — so the node count is a
function of the rule graph and the depth bound, not of the data. Over a kinship DAG
the same seven nodes answer 16 leaves and 64 of them, and an open query runs 2-6x
faster than the DFS because each node's conjunction is one planned join rather than a
tuple-at-a-time walk. A bound query is the other way round (2-4x slower): the
rewrite ignores what the caller already knows and computes the relation, then filters.
A conjunctive query is 2-3x slower still, because a k-literal conjunction has more
ways to be rewritten than a single goal does.
What it cannot do. Termination here is the depth bound, and nothing else. The
DFS is data-driven — it substitutes as it goes, so a chain of length n terminates
after n steps whatever bound it was given — while a symbolic residual grows a conjunct
per rewrite and would grow forever. So *max-depth* is a real ceiling: a derivation
deeper than it is not found, and the depth a query needs is a property of the data.
Answer-set parity with prove therefore holds up to the bound and not past it, which
is why the selector defaults to :dfs (core/*query-engine*). Iterative deepening
is what would close that, and it is not built.
See docs/inference.md.
A **backward** chainer whose state is a set of nodes ordered by cost — not
`vaelii.impl.chain`'s *forward* agenda, which is a queue of newly believed data
waiting to be matched against rules. This one runs from a query towards the facts,
and what its agenda holds is unfinished proofs.
The other backward chainer is path-structured, walking an explicit goal stack
(`res/prove-from`). Here
the unit is a **node** — a whole conjunction plus everything accumulated to reach it —
and expanding one is a single rewrite:
node: [ L₁ … Lᵢ … Lₙ ] σ
rule: A₁…Aₖ ⟹ C, with b = unify(Lᵢ, C)
child: [ b(L₁) … b(Aᵢ…) … b(Lₙ) ] σ ∪ b
The rule's antecedents under the head unifier are the **residual** — what is left to
prove if this rule is the one that fires — spliced in where `Lᵢ` was. Applied
repeatedly, that transformation is the whole search: every node is the query rewritten
through some sequence of rules, and a node whose conjunction solves against facts
alone is a completed proof.
Two things follow from the state being a value rather than a call stack. A stop
between two expansions leaves an **agenda**, not a continuation closure, so a bounded
run is `budget/collect` over the result stream and nothing else. And the tree is an
artifact that outlives the search, which is where dead ends and "why did this cost so
much" answers come from.
A third follows from the frontier being a priority queue: **which** node pops next is a
policy rather than a structure, and it lives in `vaelii.impl.tactics` — one additive
estimate whose signs the caller picks. Every tactician returns the same answer set;
what differs is when.
**What it is good at, measured.** The residual stays *symbolic* — `(anc ?y ?z)` is
not re-asked once per binding of `?y`, it is rewritten once — so the node count is a
function of the rule graph and the depth bound, not of the data. Over a kinship DAG
the same seven nodes answer 16 leaves and 64 of them, and an open query runs 2-6x
faster than the DFS because each node's conjunction is one planned join rather than a
tuple-at-a-time walk. A **bound** query is the other way round (2-4x slower): the
rewrite ignores what the caller already knows and computes the relation, then filters.
A conjunctive query is 2-3x slower still, because a k-literal conjunction has more
ways to be rewritten than a single goal does.
**What it cannot do.** Termination here is the depth bound, and nothing else. The
DFS is data-driven — it substitutes as it goes, so a chain of length n terminates
after n steps whatever bound it was given — while a symbolic residual grows a conjunct
per rewrite and would grow forever. So `*max-depth*` is a real ceiling: a derivation
deeper than it is not found, and the depth a query needs is a property of the *data*.
Answer-set parity with `prove` therefore holds up to the bound and not past it, which
is why the selector defaults to `:dfs` (`core/*query-engine*`). Iterative deepening
is what would close that, and it is not built.
See docs/inference.md.(fn [kb strategy node] -> long), the number the frontier is ordered by.
tactics/estimate unless a caller substitutes one — the extension point a whole ordering policy
reaches through, which is why the frontier is a priority queue rather than a stack.
Whatever is bound here must be an ordering and not a filter: the search visits the
same nodes in every order, so a number that changed the answer set would be a number
that dropped one.
`(fn [kb strategy node] -> long)`, the number the frontier is ordered by. `tactics/estimate` unless a caller substitutes one — the extension point a whole ordering policy reaches through, which is why the frontier is a priority queue rather than a stack. Whatever is bound here must be an **ordering** and not a filter: the search visits the same nodes in every order, so a number that changed the answer set would be a number that dropped one.
How many rule expansions any one literal may be rewritten through, and nil by default.
It is the termination condition: a residual grows a conjunct per rewrite and the claimed-key
set cannot stop it. The bound is per literal, each conjunct carrying its own remaining
budget decremented only when it is rewritten, so the literal expanded first cannot spend the
whole allowance (res/prove-from carries one depth per frame).
There is no default because the depth a query needs is a property of the KB's derivation chains, and a wrong default loses answers. The caller says, or the search refuses to start.
How many rule expansions any one literal may be rewritten through, and **nil by default**. It is the termination condition: a residual grows a conjunct per rewrite and the claimed-key set cannot stop it. The bound is per literal, each conjunct carrying its own remaining budget decremented only when it is rewritten, so the literal expanded first cannot spend the whole allowance (`res/prove-from` carries one depth per frame). There is no default because the depth a query needs is a property of the KB's derivation chains, and a wrong default loses answers. The caller says, or the search refuses to start.
The strategy a session runs under when its caller names none — nil for
tactics/defaults. A tactician keyword or a strategy map (tactics/strategy).
The strategy a session runs under when its caller names none — nil for `tactics/defaults`. A tactician keyword or a strategy map (`tactics/strategy`).
(compare-tacticians kb goals context)(compare-tacticians kb
goals
context
{:keys [tacticians node-budget max-ms] :as opts})Run goals in context under each of several tacticians, each to completion (bounded),
and return one row per tactician: its search (tree-stats), its wall-clock :ms, its
:status and its :answers set. Every tactician reorders the frontier of a complete search,
so the answer sets must be identical, and a differing row is a bug the completeness sweep says
cannot happen. :first-result? is a strategy flag and no row carries it.
Bounded as search-tree is (:node-budget per run, optional :max-ms, reported per row as
:status). Each run is timed with System/currentTimeMillis. Pass the same
:leaf-solver / :est-override as query.
Run `goals` in `context` under each of several tacticians, each to completion (bounded), and return one row per tactician: its search (`tree-stats`), its wall-clock `:ms`, its `:status` and its `:answers` set. Every tactician reorders the frontier of a complete search, so the answer sets must be identical, and a differing row is a bug the completeness sweep says cannot happen. `:first-result?` is a strategy flag and no row carries it. Bounded as `search-tree` is (`:node-budget` per run, optional `:max-ms`, reported per row as `:status`). Each run is timed with `System/currentTimeMillis`. Pass the same `:leaf-solver` / `:est-override` as `query`.
The tacticians compare-tacticians runs when the caller names no subset: the shipped
default and three orderings that disagree with it and each other. Enough spread to show
the answer set is the same across genuinely different searches — the property the page
asserts rather than assumes.
The tacticians `compare-tacticians` runs when the caller names no subset: the shipped default and three orderings that disagree with it and each other. Enough spread to show the answer set is the *same* across genuinely different searches — the property the page asserts rather than assumes.
How many node expansions search-tree drives before it stops and reports the tree
bounded. This bounds the work, and it is separate from any cap the caller later
puts on the render: a depth bound alone does not stop a wide frontier — a converging
rule graph builds one well inside its depth — so an enormous KB could otherwise turn one
debug read into an unbounded search. A run that hits this has not lost answers the way
a depth bound does; it has only stopped drawing the tree past the budget.
How many node expansions `search-tree` drives before it stops and reports the tree **bounded**. This bounds the *work*, and it is separate from any cap the caller later puts on the *render*: a depth bound alone does not stop a wide frontier — a converging rule graph builds one well inside its depth — so an enormous KB could otherwise turn one debug read into an unbounded search. A run that hits this has not lost answers the way a depth bound does; it has only stopped drawing the tree past the budget.
The tacticians a portfolio races when the caller names none: the shipped ordering, a dive, and level order. Three orderings that disagree about everything, which is the only property a racer set needs.
The tacticians a portfolio races when the caller names none: the shipped ordering, a dive, and level order. Three orderings that disagree about everything, which is the only property a racer set needs.
(frontier-key node)What the frontier orders a cost tie by: the node's residual conjunction and the literal index a rewrite resumes from. Read from the node's own content, so two searches over the same knowledge fill the frontier the same way whatever order it arrived in.
What the frontier orders a cost tie by: the node's residual conjunction and the literal index a rewrite resumes from. Read from the node's own content, so two searches over the same knowledge fill the frontier the same way whatever order it arrived in.
(node-key {:keys [literals answer-terms guards derived from] :as _node})The key a node is claimed under: its literals, the depths they carry, the map back to the
asker's variables (:answer-terms), the set of pending guard identities, :derived and the
rewrite start. The literals are already canonical, so alpha-variant conjunctions are one key.
:answer-terms keeps apart two paths that ask the same question for different answers. A
guard's identity is its rule and its term map, never a count, since two distinct guarded
rules rewriting one goal to one residual would otherwise read as one node and drop every
answer only the second exception admits. :derived keeps apart paths that answered
different goals, one of which may have used a goal belief defeated; it is empty for a KB
with no defeat on the predicates in play.
The key a node is claimed under: its literals, the depths they carry, the map back to the asker's variables (`:answer-terms`), the set of pending guard identities, `:derived` and the rewrite start. The literals are already canonical, so alpha-variant conjunctions are one key. `:answer-terms` keeps apart two paths that ask the same question for different answers. A guard's identity is its rule and its term map, never a count, since two distinct guarded rules rewriting one goal to one residual would otherwise read as one node and drop every answer only the second exception admits. `:derived` keeps apart paths that answered different goals, one of which may have used a goal belief defeated; it is empty for a KB with no defeat on the predicates in play.
(portfolio-solutions kb goals context)(portfolio-solutions kb goals context opts)Race several tacticians over goals and return the union of their answers.
Each racer is a complete search, so the union equals any single racer's answer set and the
portfolio buys latency under a bound. Incomplete strategies are refused, since
:first-result? would enlarge the union. A query writes nothing, so each racer touches
its own session's atoms, and the shared literal cache is an atom whose worst case is
duplicated work; no writing search (abduction) is reachable from here. Each racer reads
the belief the caller reads. The union is deduped on the bindings, as step! is, since
two racers that reach one answer differ only in the :proof.
Race several tacticians over `goals` and return the union of their answers. Each racer is a complete search, so the union equals any single racer's answer set and the portfolio buys latency under a bound. Incomplete strategies are refused, since `:first-result?` would enlarge the union. A query writes nothing, so each racer touches its own session's atoms, and the shared literal cache is an atom whose worst case is duplicated work; no writing search (abduction) is reachable from here. Each racer reads the belief the caller reads. The union is deduped on the bindings, as `step!` is, since two racers that reach one answer differ only in the `:proof`.
(proof-tree kb {:keys [nodes]} node)Why this node's conjunction follows: the derivation the search took, read back out of the state. A vector, one tree per conjunct of the query:
{:goal S :via :rule :rule <handle> :sentence <the rule, as written>
:because [ <the same map, per antecedent> ]}
{:goal S :via :leaf} a literal the search never rewrote
:because reads as core/why does, but this reads a search about something merely derived
and why reads the JTMS about something the KB holds.
The proof is a replay of :parent-id: each node records the one rewrite that produced it
(the rule, the literal index it replaced, how many antecedents it spliced in), so the replay
starts with the root's conjuncts as leaves and turns one leaf per rewrite into a rule node.
A literal stands for every leaf the collapse folded onto it, and the rewrite's :slots says
where each spliced literal landed. A leaf is a literal handed to the leaf solver, which
reports bindings only, so no prover is recorded. Sentences carry the node's canonical
variables.
Why this node's conjunction follows: the derivation the search took, read back out of the
state. A vector, one tree per conjunct of the query:
{:goal S :via :rule :rule <handle> :sentence <the rule, as written>
:because [ <the same map, per antecedent> ]}
{:goal S :via :leaf} a literal the search never rewrote
`:because` reads as `core/why` does, but this reads a search about something merely derived
and `why` reads the JTMS about something the KB holds.
The proof is a replay of `:parent-id`: each node records the one rewrite that produced it
(the rule, the literal index it replaced, how many antecedents it spliced in), so the replay
starts with the root's conjuncts as leaves and turns one leaf per rewrite into a rule node.
A literal stands for every leaf the collapse folded onto it, and the rewrite's `:slots` says
where each spliced literal landed. A leaf is a literal handed to the leaf solver, which
reports bindings only, so no prover is recorded. Sentences carry the node's canonical
variables.(queue-pop q)[entry queue'], or nil when the queue is empty.
`[entry queue']`, or **nil** when the queue is empty.
(search-report kb goals context opts)One node-engine search over goals, driven to completion and reported:
{:answers <vector of binding maps, `solutions`' own>
:truncated? <bool> the depth bound stopped a rewrite the search would
otherwise have taken; `false` with an empty
`:unenumerated` means every answer within the bound
:time-to-first-answer-ms <double|nil> nil when there are no answers
:total-time-ms <double>
:stats <tree-stats>
:unenumerated <vector> the transitive predicates a goal asked with both
arguments open (`provers/*unenumerated*`)
:unenumerated-in-guards <vector> the subset recorded inside an `unknown` or
`exceptWhen` evaluation (`unenumerated`)}
:truncated? is conservative: true means a branch was stopped at the bound, and a shallower
branch may have answered it. A caller tuning :max-depth raises it until :truncated? is
false and the answers stop growing. It drives the single-strategy run solutions drives
(:auto? picks one ordering, never a race) with :track-truncation? on, which session
allocates only when asked.
One node-engine search over `goals`, driven to completion and reported:
{:answers <vector of binding maps, `solutions`' own>
:truncated? <bool> the depth bound stopped a rewrite the search would
otherwise have taken; `false` with an empty
`:unenumerated` means every answer within the bound
:time-to-first-answer-ms <double|nil> nil when there are no answers
:total-time-ms <double>
:stats <tree-stats>
:unenumerated <vector> the transitive predicates a goal asked with both
arguments open (`provers/*unenumerated*`)
:unenumerated-in-guards <vector> the subset recorded inside an `unknown` or
`exceptWhen` evaluation (`unenumerated`)}
`:truncated?` is conservative: `true` means a branch was stopped at the bound, and a shallower
branch may have answered it. A caller tuning `:max-depth` raises it until `:truncated?` is
false and the answers stop growing. It drives the single-strategy run `solutions` drives
(`:auto?` picks one ordering, never a race) with `:track-truncation?` on, which `session`
allocates only when asked.(search-seq sess)The session's solutions, lazily — one node expanded per pull, so a consumer that
stops reading stops the search. A node that completes nothing costs the consumer
nothing but does advance the search: one pull runs step! until a node yields, so a
wide unproductive stretch is inside one element. A deadline therefore cannot be
held between elements of this seq; search-within is the bounded drive.
The session's solutions, lazily — one node expanded per pull, so a consumer that stops reading stops the search. A node that completes nothing costs the consumer nothing but does advance the search: one pull runs `step!` until a node yields, so a wide unproductive stretch is inside one element. A **deadline** therefore cannot be held between elements of this seq; `search-within` is the bounded drive.
(search-tree kb goals context)(search-tree kb goals context {:keys [node-budget max-ms] :as opts})Run a bounded backward search for goals in context and return the tree the run built,
every node the frontier reached, as plain data a client can render without holding the
session. The read behind the inference debugger.
The work is bounded by :max-depth (required), a node-expansion budget (:node-budget,
default-node-budget) and a wall-clock :max-ms that reports :timeout. Pass the same
:leaf-solver / :est-override as query.
Returns {:goals :context :strategy :status :bounded? :answers :nodes :stats :unenumerated :unenumerated-in-guards}. :status is :complete, :bounded (the node budget) or
:timeout. :answers are query's under :proof? true, each tagged with the :node it
came off. :nodes is every node as node-data, in allocation order. Read-only
(portfolio-solutions).
Run a bounded backward search for `goals` in `context` and return the tree the run built,
every node the frontier reached, as plain data a client can render without holding the
session. The read behind the inference debugger.
The work is bounded by `:max-depth` (required), a node-expansion budget (`:node-budget`,
`default-node-budget`) and a wall-clock `:max-ms` that reports `:timeout`. Pass the same
`:leaf-solver` / `:est-override` as `query`.
Returns `{:goals :context :strategy :status :bounded? :answers :nodes :stats :unenumerated
:unenumerated-in-guards}`. `:status` is `:complete`, `:bounded` (the node budget) or
`:timeout`. `:answers` are `query`'s under `:proof? true`, each tagged with the `:node` it
came off. `:nodes` is every node as `node-data`, in allocation order. Read-only
(`portfolio-solutions`).(search-within sess budget)(search-within sess budget pending unbounded-first?)Drive sess under budget (:max-ms and :max-results) and return the partial-result
contract budget/collect returns (:results / :status / :count / :elapsed-ms /
:resume), the shape core/prove-within promises.
The bounds are checked before every node expansion, so the deadline stops the drive within
one expansion; budget/collect over search-seq would check only after a node yielded. The
session is the continuation: :resume drives it further under a fresh budget. Solutions
completed past a :max-results cap ride the continuation as pending. The order of checks
is collect's: cap, deadline, then work. The deadline also reaches a leaf's walk (step!'s
dl); a node stopped there returns to the frontier and the continuation expands it with no
deadline, so a resume loop under a fixed budget terminates.
Drive `sess` under `budget` (`:max-ms` and `:max-results`) and return the partial-result contract `budget/collect` returns (`:results` / `:status` / `:count` / `:elapsed-ms` / `:resume`), the shape `core/prove-within` promises. The bounds are checked before every node expansion, so the deadline stops the drive within one expansion; `budget/collect` over `search-seq` would check only after a node yielded. The session is the continuation: `:resume` drives it further under a fresh budget. Solutions completed past a `:max-results` cap ride the continuation as `pending`. The order of checks is `collect`'s: cap, deadline, then work. The deadline also reaches a leaf's walk (`step!`'s `dl`); a node stopped there returns to the frontier and the continuation expands it with no deadline, so a resume loop under a fixed budget terminates.
(session kb goals context)(session kb goals context {:keys [max-depth] :as opts})A search over goals (a vector of sentences) in context, ready to be stepped.
Everything the search knows is in here and nothing is captured in a closure: the frontier, the node registry, the results, the claimed keys, the counters. A caller may hold it, read it between steps, and hand it back.
A search over `goals` (a vector of sentences) in `context`, ready to be stepped. Everything the search knows is in here and nothing is captured in a closure: the frontier, the node registry, the results, the claimed keys, the counters. A caller may hold it, read it between steps, and hand it back.
(solutions kb goals context)(solutions kb goals context opts)Every solution of goals in context, as prove returns them — a vector of binding
maps over the query's variables, deduped.
opts carries :max-depth, the :strategy (tactics/strategy), :portfolio? to
race the default racers instead of running one ordering, and :auto? to let
tactics/auto-strategy pick from the structure of the query. An explicit :strategy
answers :auto?, so naming one turns the probe off. :max-results caps the answer
at that many, and every racer's run too, for an existence question
(core/query?, core/provable?), which reads only whether the vector is empty.
Neither :portfolio? nor an :auto? that picks one is an anytime mode: a race is
driven to completion before it can be unioned, so it has no partial answer to give.
core/prove-within drives search-seq directly and is unaffected.
Every solution of `goals` in `context`, as `prove` returns them — a vector of binding maps over the query's variables, deduped. `opts` carries `:max-depth`, the `:strategy` (`tactics/strategy`), `:portfolio?` to race the default racers instead of running one ordering, and `:auto?` to let `tactics/auto-strategy` pick from the structure of the query. An explicit `:strategy` answers `:auto?`, so naming one turns the probe off. `:max-results` caps the answer at that many, and every racer's run too, for an existence question (`core/query?`, `core/provable?`), which reads only whether the vector is empty. Neither `:portfolio?` nor an `:auto?` that picks one is an **anytime** mode: a race is driven to completion before it can be unioned, so it has no partial answer to give. `core/prove-within` drives `search-seq` directly and is unaffected.
(step! sess)(step! {:keys [kb context queue nodes counter stats seen strategy leaf-solver
est-override proof? defeated truncated unenumerated]
:as sess}
dl)Expand the cheapest node: solve its conjunction inline, claim and enqueue its children, and return the solutions it completed, a vector, empty when it completed none. nil when the frontier is empty, the only exhaustion signal.
Solutions are run past the node's guards, projected onto the query's variables and deduped
against everything already returned. A guard is asked here because the argument is
complete here. Whether the node produced anything is what the tactician's child bias reads
(tactics/child-bias). Under :first-result? a productive node builds no children.
dl is the System/nanoTime instant a leaf's walk stops at (budget/interruptible; the
1-arity has none). A node the deadline stops inside goes back on the frontier as it was and
the answer is ::budget/interrupted. A thread interrupted before the step throws
InterruptedException and expands nothing.
Expand the cheapest node: solve its conjunction inline, claim and enqueue its children, and return the solutions it completed, a vector, empty when it completed none. **nil** when the frontier is empty, the only exhaustion signal. Solutions are run past the node's guards, projected onto the query's variables and deduped against everything already returned. A guard is asked here because the argument is complete here. Whether the node produced anything is what the tactician's child bias reads (`tactics/child-bias`). Under `:first-result?` a productive node builds no children. `dl` is the `System/nanoTime` instant a leaf's walk stops at (`budget/interruptible`; the 1-arity has none). A node the deadline stops inside goes back on the frontier as it was and the answer is `::budget/interrupted`. A thread interrupted before the step throws `InterruptedException` and expands nothing.
(tree-stats {:keys [nodes claimed stats queue]})The search tree as data once (or while) it is running: how many nodes were built and expanded, how many arrivals the claimed-key set dropped, how many solutions were completed, and how deep the rewriting went.
The search tree as data once (or while) it is running: how many nodes were built and expanded, how many arrivals the claimed-key set dropped, how many solutions were completed, and how deep the rewriting went.
(unenumerated sess)sess's collector as provers/unenumerated-report's two keys: :unenumerated, the
transitive predicates whose closure a both-open goal in the search did not enumerate,
and :unenumerated-in-guards, those of them recorded inside an unknown or
exceptWhen evaluation, where the missed pair can admit an answer (docs/inference.md).
`sess`'s collector as `provers/unenumerated-report`'s two keys: `:unenumerated`, the transitive predicates whose closure a both-open goal in the search did not enumerate, and `:unenumerated-in-guards`, those of them recorded inside an `unknown` or `exceptWhen` evaluation, where the missed pair can admit an answer (docs/inference.md).
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 |