vaelii.impl.inference — com.vaelii/vaelii 0.1.0

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.

*estimate* clj

(fn [kb strategy node] -> long), the number the frontier is ordered by.

tactics/estimate unless a caller substitutes one — the seam 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.

*max-depth* clj

How many rule expansions any one literal may be rewritten through — and nil by default, on purpose.

This is not a tuning knob but the termination condition: a residual grows a conjunct per rewrite and the claimed-key set cannot stop it, because each rewrite yields a longer conjunction and so a key nothing has claimed. Per literal, not per node — a conjunction's conjuncts each carry their own remaining budget, decremented only for the one actually rewritten, so the literal expanded first cannot spend the whole allowance (res/prove-from carries one depth per frame and does let it).

There is no default because there is no defensible one. The depth a query needs is a property of the data — of how long a derivation chain the KB happens to contain — so a number chosen here is a number chosen without looking at the thing it bounds. A default would be silently wrong for every KB but the one it was picked on, and wrong in the direction that loses answers rather than the one that costs time. So the caller says, or the search refuses to start. Iterative deepening is what would let the engine find the number itself, and it is not built.

*strategy* clj

The strategy a session runs under when its caller names none — nil for tactics/defaults. A tactician keyword or a strategy map (tactics/strategy).

backchain clj

(backchain kb goal context leaf-solver)

(backchain kb goal context leaf-solver opts)

Answer goal by rule expansion, with every literal the search will not rewrite handed to leaf-solver.

This is what ask uses for the rule half of its answer, and why the node engine is a reasonable thing to put there rather than a path-structured search. A converging rule graph asks one subgoal from many branches; a path engine re-derives it per branch and needs a per-query memo to claw that back, while here the claimed-key set drops the second arrival before it is ever enqueued. The sharing is the search's own structure rather than a cache laid beside it.

The leaf solver must not itself backchain, and provers/solve-goal does not: nothing in the registry expands a rule. That is what makes the division clean — this engine expands the rules, the leaf answers everything that is not a rule — and it is load-bearing rather than incidental. A leaf that started its own backward search would run the engine's rewriting plus a nested search per binding under it, which measured 24-73x slower than the divided arrangement on the same queries.

The claimed-key set is what makes the sharing free: a converging rule graph asks one subgoal from many branches, and a path engine re-derives it per branch, while here the second arrival is dropped before it is ever enqueued.

What it costs is this engine's termination: *max-depth* is a real ceiling, so a derivation deeper than it is not found. See docs/inference.md.

default-racers clj

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.

empty-queue clj

(empty-queue)

node-key clj

(node-key {:keys [literals answer-terms guards from] :as _node})

The key a node is claimed under: its literals, the depths they carry, the map back to the asker's variables, how many guards are pending, and the rewrite window.

The literals need no renaming here — they are already canonical, which is the point of canonicalizing them, and two alpha-variant conjunctions are one key without anything further being done about it.

:answer-terms is what keeps apart two paths that ask the same question on behalf of different answers: the same conjunction, but one path's ?var0 is the asker's ?x and the other's is ?y — or one path has already fixed ?x to Tom and the other has not. Collapsing those loses an answer set. The guard count keeps apart two paths where one carries an exceptWhen the other does not: same conjunction, different answers again.

portfolio-solutions clj

(portfolio-solutions kb goals context)

(portfolio-solutions kb goals context opts)

Race several tacticians over goals and return the union of their answers.

The union equals any single racer's answer set. Each racer is a complete search, so the portfolio is a bet that one ordering finds the answer sooner, never a way to find more answers — a racer that contributed an answer no other racer found would be a bug in the others. What it buys is latency under a bound, where the ordering that suits this query gets there before the deadline and the others do not.

Read-only by construction. Racing is safe here only because a query in this engine writes nothing: every racer touches its own session's atoms, the KB not at all, and the shared literal cache is an atom whose worst case under a race is duplicated work. A search that wrote — an abducing one, which asserts its assumptions — must never be raced under the single-writer contract, and is not reachable from here.

Incomplete strategies are refused rather than raced: :first-result? would make the union larger than a racer's own answer set and turn the paragraph above into a lie.

proof-tree clj

(proof-tree kb {:keys [nodes]} node)

Why this node's conjunction follows — the derivation the search actually took, read back out of the state rather than recorded beside it. 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 and the recursion read the way core/why does, so a proof of an ephemeral answer and a proof of a stored belief are one shape to learn. They answer different questions all the same: why reads the JTMS about something the KB holds, this reads a search about something it merely derived.

How it is rebuilt. Every node records the one rewrite that produced it — the rule, the literal index it replaced, and how many antecedents it spliced in — and the session already holds every node. So the proof is a replay of :parent-id: start with the root's conjuncts as leaves, and let each rewrite turn one leaf into a rule node whose children are the residual that took its place. Nothing is re-derived, no unification is redone, and the search pays one small map per node whether or not anybody asks.

A leaf is a literal the search handed to its leaf solver. Which prover answered it is not recorded, because the leaf solver is a parameter and reports only bindings — the tree is the rewriting the engine did, and it stops where the engine stopped.

Sentences carry the node's canonical variables, not a solution's values: a proof is about the derivation, which is one tree however many answers came off it.

queue-pop clj

(queue-pop q)

[entry queue'], or nil when the queue is empty.

queue-push clj

(queue-push q est id)

search-seq clj

(search-seq sess)

The session's solutions, lazily — one node expanded per pull, so a bounded consumer (budget/collect) stops the search where it stops reading. A node that completes nothing costs the consumer nothing but does advance the search.

session clj

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

solutions clj

(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 shape of the query. An explicit :strategy answers :auto?, so naming one turns the probe off.

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

(step! {:keys [kb context queue nodes counter stats seen strategy leaf-solver
               proof?]
        :as sess})

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, which is 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 rather than at the rewrite that inherited it, because this is the moment the argument is complete — which is the same moment prove reaches by pushing a marker behind the antecedents, arrived at without needing the marker.

Whether the node produced anything is what the tactician's child bias reads (tactics/child-bias): a parent that is paying can recommend its children either way, and the bias is how it says so. Under :first-result? a productive node builds no children at all — the one strategy that stops the search rather than steering it.

tree-stats clj

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