Forward chaining: the semi-naive fixpoint, one agenda for bare and defeasible
rules alike, with the definitional checks re-run on the derivation path and the
exceptWhen guard consulted before a conclusion is placed.
Fifth layer of the engine stack (kb <- checks <- special <- integrate <- chain
<- settle): a firing joins antecedents against stored facts (kb), checks its
conclusion (checks), and reflects what it places into the caches through the
derivation-path choke point (special). Belief settling happens after a run,
in vaelii.impl.settle — nothing here defeats or arbitrates.
Forward chaining: the semi-naive fixpoint, one agenda for bare and defeasible rules alike, with the definitional checks re-run on the derivation path and the `exceptWhen` guard consulted before a conclusion is placed. Fifth layer of the engine stack (kb <- checks <- special <- integrate <- chain <- settle): a firing joins antecedents against stored facts (kb), checks its conclusion (checks), and reflects what it places into the caches through the derivation-path choke point (special). Belief settling happens *after* a run, in `vaelii.impl.settle` — nothing here defeats or arbitrates.
How the forward join looks up the stored facts satisfying a non-trigger
antecedent — (fn [kb pattern context] -> seq of [handle bindings …]), returning
exactly what res/match-pattern does.
The default is res/match-pattern (the count-aware trie), which is the reference
path and leaves forward chaining unchanged. vaelii.impl.rete binds this to a RAM
alpha-memory matcher that answers the same set through an index on argument values,
so a non-trigger antecedent with a leading variable — (parentOf ?x Pi) — is a
hash lookup rather than a full functor scan. The set it returns is identical
(proven by the rete oracle), so every downstream behaviour is the reference's; only
the candidate lookup changes. This is the sole seam the incremental matcher needs,
because the trigger match (match1) is already selective and everything else —
placement, exceptions, the definitional checks, justification dedup — is reused
verbatim. See docs/inference.md, "Incremental rule matching".
How the forward join looks up the stored facts satisfying a **non-trigger** antecedent — `(fn [kb pattern context] -> seq of [handle bindings …])`, returning exactly what `res/match-pattern` does. The default is `res/match-pattern` (the count-aware trie), which is the reference path and leaves forward chaining unchanged. `vaelii.impl.rete` binds this to a RAM alpha-memory matcher that answers the same set through an index on argument values, so a non-trigger antecedent with a leading variable — `(parentOf ?x Pi)` — is a hash lookup rather than a full functor scan. The *set* it returns is identical (proven by the rete oracle), so every downstream behaviour is the reference's; only the candidate lookup changes. This is the sole seam the incremental matcher needs, because the trigger match (`match1`) is already selective and everything else — placement, exceptions, the definitional checks, justification dedup — is reused verbatim. See docs/inference.md, "Incremental rule matching".
Per-run cache of {calculus-name -> #{context}} — the readers of a calculus, which
are the networks an entailed antecedent is solved against.
Collecting them walks the calculus's own extent, the same order as reading one
network, and where its facts span microtheories a genlContext closure besides, so it
is cached for the length of a chaining run rather than recomputed per antecedent per
binding. Bound by chain; nil outside one, where it simply recomputes.
Per-run cache of `{calculus-name -> #{context}}` — the readers of a calculus, which
are the networks an entailed antecedent is solved against.
Collecting them walks the calculus's own extent, the same order as reading one
network, and where its facts span microtheories a `genlContext` closure besides, so it
is cached for the length of a chaining run rather than recomputed per antecedent per
binding. Bound by `chain`; nil outside one, where it simply recomputes.{:literal <antecedent> :moved {context (:all | #{pair})}}, or nil.
What makes a re-join semi-naive. A qualitative fact re-joins every rule mentioning
its calculus, and joining over every pair the network entails means the nth arriving
fact redoes what the (n-1)th already did. Bound by rejoin-qualitative to the pairs
that have moved since the last such re-join (qcn-kb/join-delta), it narrows the
enumeration of one antecedent — the named literal — and leaves the rest full.
One antecedent, because that is the delta rule: for a rule with two qualitative
antecedents, narrowing both at once would drop every firing pairing a moved binding with
an unmoved one. So rejoin-qualitative runs the join once per qualitative antecedent,
each with a different one narrowed, and the overlap re-derives conclusions the TMS
dedups.
Read by literal rather than by position: plan/order reorders the antecedents, so a
position means nothing by the time the join runs. Two identical antecedents in one rule
are both narrowed, which is the same set — they bind identically.
`{:literal <antecedent> :moved {context (:all | #{pair})}}`, or nil.
What makes a re-join **semi-naive**. A qualitative fact re-joins every rule mentioning
its calculus, and joining over every pair the network entails means the nth arriving
fact redoes what the (n-1)th already did. Bound by `rejoin-qualitative` to the pairs
that have moved since the last such re-join (`qcn-kb/join-delta`), it narrows the
enumeration of **one** antecedent — the named literal — and leaves the rest full.
One antecedent, because that is the delta rule: for a rule with two qualitative
antecedents, narrowing both at once would drop every firing pairing a moved binding with
an unmoved one. So `rejoin-qualitative` runs the join once per qualitative antecedent,
each with a different one narrowed, and the overlap re-derives conclusions the TMS
dedups.
Read by literal rather than by position: `plan/order` reorders the antecedents, so a
position means nothing by the time the join runs. Two identical antecedents in one rule
are both narrowed, which is the same set — they bind identically.(chain kb seed opts)Semi-naive fixpoint forward chaining seeded with seed, strict and defeasible
rules together on the one agenda.
opts may carry an :on-progress callback, called about four times a second
(:progress-every-ms) with
{:derived n :pending n} — what the run has concluded, and how much agenda is left. A
fixpoint has no total to count towards (the agenda grows as it derives), so those two
numbers are the honest reading of where a run is; both are O(1) to take. The callback
may throw, which aborts the run — the one interruption point chaining has, and how a
loader cancels one. What had already been derived stays: the conclusions are placed as
they are made, so an aborted fixpoint is a KB holding a prefix of the run, not a corrupt
one.
Reporting happens at two points, and it takes both to keep a bar moving: at the agenda
loop, which sees the run between datums, and at each rule firing (*tick*), which is
inside the one datum that can run for minutes. The remaining silent stretch is a single
unproductive join — a match search that yields nothing for a long time never reaches a
firing — which is bounded by the extent it is scanning rather than by the corpus.
Semi-naive fixpoint forward chaining seeded with `seed`, strict and defeasible
rules together on the one agenda.
`opts` may carry an **`:on-progress`** callback, called about four times a second
(`:progress-every-ms`) with
`{:derived n :pending n}` — what the run has concluded, and how much agenda is left. A
fixpoint has no total to count towards (the agenda grows as it derives), so those two
numbers are the honest reading of where a run is; both are O(1) to take. The callback
may **throw**, which aborts the run — the one interruption point chaining has, and how a
loader cancels one. What had already been derived stays: the conclusions are placed as
they are made, so an aborted fixpoint is a KB holding a prefix of the run, not a corrupt
one.
Reporting happens at two points, and it takes both to keep a bar moving: at the agenda
loop, which sees the run between datums, and at each rule firing (`*tick*`), which is
inside the one datum that can run for minutes. The remaining silent stretch is a single
*unproductive* join — a match search that yields nothing for a long time never reaches a
firing — which is bounded by the extent it is scanning rather than by the corpus.(chain-all kb seed opts)One fixpoint from seed, strict and defeasible rules on the same agenda (there
is no separate defaults phase — see fire-rules-for).
Opens a new run in chain-stats — violations recorded during the run carry its
id — and stashes the result there, warning when the run was truncated. The ledger
accumulates across runs rather than resetting per run, so a bulk load's drops
stay observable one assert later; and because internal callers discard the
:truncated? flag, the :warn log is how a depth-capped chain's lost conclusions
surface.
One fixpoint from `seed`, strict and defeasible rules on the same agenda (there is no separate defaults phase — see `fire-rules-for`). Opens a new run in `chain-stats` — violations recorded during the run carry its id — and stashes the result there, warning when the run was truncated. The ledger **accumulates** across runs rather than resetting per run, so a bulk load's drops stay observable one assert later; and because internal callers discard the `:truncated?` flag, the :warn log is how a depth-capped chain's lost conclusions surface.
max-depth bounds derivation depth to catch productive infinite recursion; max-derivations is a hard backstop on a single chain run.
max-depth bounds derivation depth to catch productive infinite recursion; max-derivations is a hard backstop on a single chain run.
(exception-holds? kb except bindings pctx)Does except — a rule's exception, a vector of literals — hold under bindings,
evaluated in pctx, the context the conclusion would be placed in?
Three properties make this cheap, and each is load-bearing:
sentex constructor), so substitution leaves a ground question. The conjuncts
therefore share nothing and need no join — each is an independent existence check,
and all must hold.first stops
the query at its first result rather than enumerating an extent.argIsa, where an argument whose type is
unknown cannot violate a constraint: blocking on "cannot tell" would let a
missing fact silently suppress knowledge.An empty / absent exception never holds, so an ordinary rule takes no cost here.
Defined in vaelii.impl.provers because the backward chainers need exactly the same
judgement; pctx here is the conclusion's placement context, where backward passes
the query's.
Does `except` — a rule's exception, a vector of literals — hold under `bindings`, evaluated in `pctx`, the context the conclusion would be placed in? Three properties make this cheap, and each is load-bearing: * **Closed.** Every exception variable is bound by an antecedent (enforced in the `sentex` constructor), so substitution leaves a *ground* question. The conjuncts therefore share nothing and need no join — each is an independent existence check, and **all** must hold. * **One answer suffices.** The levels stack is lazy throughout, so `first` stops the query at its first result rather than enumerating an extent. * **An unanswerable exception does not hold**, and the rule fires. That is the open-world reading, and it matches `argIsa`, where an argument whose type is unknown cannot violate a constraint: blocking on "cannot tell" would let a missing fact silently suppress knowledge. An empty / absent exception never holds, so an ordinary rule takes no cost here. Defined in `vaelii.impl.provers` because the backward chainers need exactly the same judgement; `pctx` here is the conclusion's placement context, where backward passes the query's.
(justification-excepted? kb j)Is justification j currently blocked — by its rule's exceptWhen exception, by an
(unknown S) antecedent whose S is now derivable, by an aggregate antecedent
whose count has moved, by a visibility except hiding one of its antecedents from
the conclusion's context, or by the qualitative network it joined on having become
unsatisfiable?
The context is the conclusion's, not the rule's: an exceptWhen query and a NAF
literal are about the conclusion (one invisible from where it lives has no business
blocking it), and a visibility except is precisely about where a fact can be seen —
a derivation resting on an antecedent the conclusion's context cannot see is invalid
there. Nothing is cached: this re-runs the checks every time, which is what keeps
blocking from drifting out of step with belief.
Is justification `j` currently blocked — by its rule's `exceptWhen` exception, by an `(unknown S)` antecedent whose `S` is now derivable, by an **aggregate** antecedent whose count has moved, by a visibility `except` hiding one of its antecedents from the conclusion's context, or by the qualitative network it joined on having become unsatisfiable? The context is the **conclusion's**, not the rule's: an exceptWhen query and a NAF literal are *about* the conclusion (one invisible from where it lives has no business blocking it), and a visibility `except` is precisely about where a fact can be seen — a derivation resting on an antecedent the conclusion's context cannot see is invalid there. Nothing is cached: this re-runs the checks every time, which is what keeps blocking from drifting out of step with belief.
(naf-blocks? kb naf-antes bindings pctx)Is a firing blocked by any of its unknown antecedents naf-antes — is any inner
query derivable under bindings, in pctx? Block-if-any: each (unknown S)
independently requires S absent, so one derivable S withdraws the conclusion.
Is a firing blocked by any of its `unknown` antecedents `naf-antes` — is any inner query derivable under `bindings`, in `pctx`? Block-if-**any**: each `(unknown S)` independently requires `S` absent, so one derivable `S` withdraws the conclusion.
(post-join-bindings kb literals bindings pctx)Extend bindings with what a firing's post-join literals compute (rules/post-join -literals), or nil when one of them has no answer.
This is where an aggregate antecedent is actually evaluated: not in the join, which
does not yet know where the conclusion lands, but per placement context — the same
answer exceptWhen and unknown give to the same question, and the one that makes
the three chainers agree. Each literal is solved through the prover registry under
the bindings the previous ones produced, so an aggregate feeds the comparison on its
own count.
Each keeps the context it would have had in the join. An aggregate runs in
pctx, because a census is of what that context believes. A comparison runs in the
wildcard, because arithmetic holds as arithmetic rather than as knowledge asserted
somewhere — the same reason solve-deferred uses it. Moving a literal later must
not quietly move it to another context.
Nil is a block, and it means one of two things that the caller need not
distinguish: the literal has no answer at all (a min over an empty group, a
comparison that came out false), or its output was already bound — by an earlier
antecedent, or by the firing this is re-checking — and the recomputed value no
longer matches it.
Extend `bindings` with what a firing's post-join literals compute (`rules/post-join -literals`), or nil when one of them has no answer. This is where an aggregate antecedent is actually evaluated: not in the join, which does not yet know where the conclusion lands, but per placement context — the same answer `exceptWhen` and `unknown` give to the same question, and the one that makes the three chainers agree. Each literal is solved through the prover registry under the bindings the previous ones produced, so an aggregate feeds the comparison on its own count. **Each keeps the context it would have had in the join.** An aggregate runs in `pctx`, because a census is of what that context believes. A comparison runs in the wildcard, because arithmetic holds as arithmetic rather than as knowledge asserted somewhere — the same reason `solve-deferred` uses it. Moving a literal later must not quietly move it to another context. Nil is a **block**, and it means one of two things that the caller need not distinguish: the literal has no answer at all (a `min` over an empty group, a comparison that came out false), or its output was already bound — by an earlier antecedent, or by the firing this is re-checking — and the recomputed value no longer matches it.
(rule-view-of kb handle rsx)The chainer's view of a rule sentex. :strength is the justification class its
firings confer, read off the record's :defeasible — the same authority the
direction is read from, so a rule needs no separate index to know how it fires.
The chainer's view of a rule sentex. `:strength` is the justification class its firings confer, read off the record's `:defeasible` — the same authority the direction is read from, so a rule needs no separate index to know how it fires.
(solve-rule kb antecedents)(solve-rule kb antecedents b0)(solve-rule kb antecedents b0 consequent-pred)Full join of a rule's antecedents against current facts (used when a rule is
added), in cost order. The seeded arity starts from b0 instead of the empty
binding map, which is how why-not reconstructs a firing backwards from its
conclusion; consequent-pred (the rule's consequent functor, nil if unknown) lets
the planner keep the recursive literal in place.
Full join of a rule's antecedents against current facts (used when a rule is added), in cost order. The seeded arity starts from `b0` instead of the empty binding map, which is how `why-not` reconstructs a firing backwards from its conclusion; `consequent-pred` (the rule's consequent functor, nil if unknown) lets the planner keep the recursive literal in place.
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 |