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.
A mutable {handle -> arrival} map — the position at which each datum joined this
run's agenda — or nil, and then nothing is suppressed.
This decides work, not belief. A rule a(x,y) <- b1(x,z), b2(z,y) is triggered
by its b1 datum at position 0 and by its b2 datum at position 1, and both
enumerate the same pair: the second runs the whole join, rebuilds the same
conclusion, resolves the same placement contexts, and is thrown away by
jtms/has-justification?. Ordering the agenda's datums lets one of the two skip the
work — the firing that survives is identical whichever side makes it (same
bindings, same antecedent set, same justification), so the derived set and its
supports are unchanged by construction. Nothing here is read when belief is
computed, and no tie-break anywhere keys on it: the engine's rule that belief never
tie-breaks on a handle is untouched, because this is not consulted about belief.
Arrival order, not handle order, and the difference is the whole correctness
argument. For a datum the run itself derives the two agree — handles are allocated
in creation order and a new conclusion is enqueued as it is placed — but a datum put
back on the agenda has an old handle and a fresh arrival: a fact revived from OUT,
a fact newly matchable under a derived genl edge (special/subsumption-seeds), a
seed list in whatever order jtms/in-datums produced. Keyed on arrival, such a
datum sorts after the partner that was already processed, so it is the one that
enumerates the pair, and the pair is enumerated. Keyed on the handle it would sort
before it and the pair would be lost.
A handle the run never enqueued has no arrival and is never suppressed against:
nothing else will enumerate its combinations, so they are all made here. That covers
the equality twins special/derive-functional-equalities places without enqueueing,
and every join run outside a chaining run at all. A disbelieved trigger declines
the filter outright, for the reason arrival-admit states.
Bound by chain for the length of a run, like the handle cache and the dedup index,
and it is the agenda that bounds its size. A java.util.HashMap rather than an atom
because the engine is single-writer and this is read once per candidate the join
yields.
A mutable `{handle -> arrival}` map — the position at which each datum joined this
run's agenda — or nil, and then nothing is suppressed.
**This decides work, not belief.** A rule `a(x,y) <- b1(x,z), b2(z,y)` is triggered
by its `b1` datum at position 0 and by its `b2` datum at position 1, and both
enumerate the same pair: the second runs the whole join, rebuilds the same
conclusion, resolves the same placement contexts, and is thrown away by
`jtms/has-justification?`. Ordering the agenda's datums lets one of the two skip the
work — the firing that survives is *identical* whichever side makes it (same
bindings, same antecedent set, same justification), so the derived set and its
supports are unchanged by construction. Nothing here is read when belief is
computed, and no tie-break anywhere keys on it: the engine's rule that belief never
tie-breaks on a handle is untouched, because this is not consulted about belief.
**Arrival order, not handle order**, and the difference is the whole correctness
argument. For a datum the run itself derives the two agree — handles are allocated
in creation order and a new conclusion is enqueued as it is placed — but a datum put
**back** on the agenda has an old handle and a fresh arrival: a fact revived from OUT,
a fact newly matchable under a derived `genl` edge (`special/subsumption-seeds`), a
seed list in whatever order `jtms/in-datums` produced. Keyed on arrival, such a
datum sorts *after* the partner that was already processed, so it is the one that
enumerates the pair, and the pair is enumerated. Keyed on the handle it would sort
before it and the pair would be lost.
A handle the run never enqueued has **no** arrival and is never suppressed against:
nothing else will enumerate its combinations, so they are all made here. That covers
the equality twins `special/derive-functional-equalities` places without enqueueing,
and every join run outside a chaining run at all. A **disbelieved** trigger declines
the filter outright, for the reason `arrival-admit` states.
Bound by `chain` for the length of a run, like the handle cache and the dedup index,
and it is the agenda that bounds its size. A `java.util.HashMap` rather than an atom
because the engine is single-writer and this is read once per candidate the join
yields.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.Whether a run generates each satisfying antecedent combination once rather than
once per side that can trigger it (see *agenda-arrivals*). On by default; bound
false to enumerate every trigger, which is the reference side the oracles compare
against (witness_order_test, rete_oracle_test). A pure cost decision: the
suppressed firings are duplicates of ones the run makes anyway, so the derived set
and its supports are the same either way.
Whether a run generates each satisfying antecedent combination **once** rather than once per side that can trigger it (see `*agenda-arrivals*`). On by default; bound **false** to enumerate every trigger, which is the reference side the oracles compare against (`witness_order_test`, `rete_oracle_test`). A pure cost decision: the suppressed firings are duplicates of ones the run makes anyway, so the derived set and its supports are the same either way.
(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.
(drop-refusal! kb rh entry)Retire one entry. A refusal is dead when it fires, when its rule goes, or when the
antecedents behind its bindings are no longer believed — the bindings are a snapshot,
and a refusal must not resurrect a firing whose support left. An :overflow record
holds no entries to drop.
Retire one entry. A refusal is dead when it fires, when its rule goes, or when the antecedents behind its bindings are no longer believed — the bindings are a snapshot, and a refusal must not resurrect a firing whose support left. An `:overflow` record holds no entries to drop.
(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 a visibility except hiding one of its
antecedents, or by anything its rule carries (rule-firing-blocked?)?
The conclusion's record names the placement context every check is evaluated in, and the informant names the rule.
Is justification `j` currently blocked — by a visibility `except` hiding one of its antecedents, or by anything its rule carries (`rule-firing-blocked?`)? The conclusion's record names the placement context every check is evaluated in, and the informant names the rule.
How many refused firings one rule's record keeps before it stops keeping them individually.
One entry per refused firing is bounded by what a rule did not derive, and a rule
excepted on a common condition can refuse far more than it places — so unlike blocking
it is not bounded by the store. Past this many entries the rule's record collapses to
:overflow and it takes the coarse fallback instead: a queued overflowed rule forces a
productive settle pass and is re-joined over its extent, which finds the same
releases at the cost the record exists to avoid. Correct on both sides of the line,
and the line is stated in docs/exceptions.md.
How many refused firings one rule's record keeps before it stops keeping them individually. One entry per refused firing is bounded by what a rule did **not** derive, and a rule excepted on a common condition can refuse far more than it places — so unlike blocking it is not bounded by the store. Past this many entries the rule's record collapses to `:overflow` and it takes the coarse fallback instead: a queued overflowed rule forces a productive settle pass and is re-joined over its extent, which finds the same releases at the cost the record exists to avoid. Correct on both sides of the line, and the line is stated in docs/exceptions.md.
(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.
(refusal-state kb rh entry)Re-decide one recorded refusal of rule rh, from scratch: :dead when there is no
longer a firing to make, :blocked when the condition that refused it still holds,
:free when it does not and the conclusion is owed a placement.
Nothing remembers the previous answer — the record says which firings to re-ask and
never what the answer is, exactly as exception-blocked-set re-decides every
candidate justification it looks at. Blocking would otherwise drift from belief.
The judgement is rule-firing-blocked?, the same one a placed firing's justification
is re-decided by, plus the visibility except check the justification path also runs.
Bindings are settled to the representatives pctx now elects first, for the reason
settled-bindings records: a snapshot asks about a spelling a merge has retired, and
the honest empty that comes back reads as not excepted.
Re-decide one recorded refusal of rule `rh`, from scratch: `:dead` when there is no longer a firing to make, `:blocked` when the condition that refused it still holds, `:free` when it does not and the conclusion is owed a placement. Nothing remembers the previous answer — the record says which firings to re-ask and never what the answer is, exactly as `exception-blocked-set` re-decides every candidate justification it looks at. Blocking would otherwise drift from belief. The judgement is `rule-firing-blocked?`, the same one a placed firing's justification is re-decided by, plus the visibility `except` check the justification path also runs. Bindings are settled to the representatives `pctx` now elects first, for the reason `settled-bindings` records: a snapshot asks about a spelling a merge has retired, and the honest empty that comes back reads as *not excepted*.
(refusals kb rh)What is recorded against rule rh: a set of refusal entries, :overflow, or nil.
settle reads this to decide which firings a queued rule owes a re-ask.
What is recorded against rule `rh`: a set of refusal entries, `:overflow`, or nil. `settle` reads this to decide which firings a queued rule owes a re-ask.
(release-refusal! kb rh entry)Re-derive the refused firing entry of rule rh and retire the entry, or retire it
without deriving anything when its support has left. Returns the handles the
re-derivation created, for the caller to put back on the agenda.
place-conclusion with the recorded bindings, never a fresh join — that is the
whole cost argument: re-deriving k recorded refusals is k placements, where seeding
chain with the rule handle joins it over the whole fact extent. The conclusion, its
placement context and its antecedent list are the ones the refused firing computed, so
the justification is the one that firing would have made; the depth is recomputed from
the antecedent facts, as a fresh firing would compute it.
Re-decided here rather than trusted from the caller's scan: the sweep runs in between, and a refusal whose support it collected must not be placed on the strength of an answer taken before it ran.
Re-derive the refused firing `entry` of rule `rh` and retire the entry, or retire it without deriving anything when its support has left. Returns the handles the re-derivation created, for the caller to put back on the agenda. **`place-conclusion` with the recorded bindings, never a fresh join** — that is the whole cost argument: re-deriving k recorded refusals is k placements, where seeding `chain` with the rule handle joins it over the whole fact extent. The conclusion, its placement context and its antecedent list are the ones the refused firing computed, so the justification is the one that firing would have made; the depth is recomputed from the antecedent facts, as a fresh firing would compute it. Re-decided here rather than trusted from the caller's scan: the sweep runs in between, and a refusal whose support it collected must not be placed on the strength of an answer taken before it ran.
(rerecord-refusals! kb)Rebuild the refusal record by re-firing every rule that can refuse a firing. Returns the chain result, or nil for a KB where no rule carries a re-checkable block condition.
recover's half of the record. A refused firing left no justification, so nothing in
the store holds it and replaying the stored justifications cannot bring it back — the
record is derived state and is rebuilt the way blocking is, by re-deciding rather than
by reading. Re-firing is what re-decides it: a firing that can be placed is placed and
deduped by has-justification?, and one that is refused re-records.
Run after the settle that establishes belief, since a refusal is a claim about what
the KB believes, and relabel deliberately lands unblocked. ! because it discards
the record it replaces.
Rebuild the refusal record by re-firing every rule that can refuse a firing. Returns the chain result, or nil for a KB where no rule carries a re-checkable block condition. `recover`'s half of the record. A refused firing left no justification, so nothing in the store holds it and replaying the stored justifications cannot bring it back — the record is derived state and is rebuilt the way blocking is, by re-deciding rather than by reading. Re-firing is what re-decides it: a firing that can be placed is placed and deduped by `has-justification?`, and one that is refused re-records. Run **after** the settle that establishes belief, since a refusal is a claim about what the KB believes, and `relabel` deliberately lands unblocked. `!` because it discards the record it replaces.
(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 |