Pluggable provers for the query engine. A prover answers a goal and declares how it expects to perform, so the engine can choose among applicable provers:
applicable? can it answer this goal at all?
est-bindings ~how many solution bindings it will produce
cost a qualitative first-answer cost tier (see cost-tiers)
completeness 0..100 — see the contract below
solve the solutions, as raw binding maps
ask runs the cheapest complete prover alone (fewest est-bindings);
otherwise it unions the applicable provers cheapest first by cost tier.
Built-in provers: transitivity (genl/genlContext,
complete via the cached closures), disjointness (complete), different (the
unique-name assumption read off the equality closure — ground only, see
docs/equality.md), facts (the index), and rules (backward chaining through the same
engine).
For this goal shape, my answers are a superset of what every other prover reading the same sources would answer. That is the reading that licenses running alone, and it is a claim a prover is competent to make about itself.
The tempting alternative — nothing else can answer this goal — is a claim about a
predicate, and it stops being true the moment a KB adds a second way to reach that
predicate. Whether such a way exists is not a question any one prover can answer,
because it is about the sources it does not read. So the engine asks it, once
per goal, in sole-prover: a claimant runs alone only when shadowing-channels is
empty. A prover therefore declares a constant and reasons only about its own
sources, and a prover registered through add-prover is guarded without its author
knowing the mechanism exists.
A computed prover normally earns the claim it makes: the closure provers are built
out of the very facts FactProver would return and out of the derivations a rule
contributes, and a calculus reads both into its network — converse and composition
included — before entailing anything.
Pluggable provers for the query engine. A prover answers a goal and declares how it expects to perform, so the engine can choose among applicable provers: applicable? can it answer this goal at all? est-bindings ~how many solution bindings it will produce cost a qualitative first-answer cost tier (see `cost-tiers`) completeness 0..100 — see the contract below solve the solutions, as raw binding maps `ask` runs the cheapest *complete* prover alone (fewest `est-bindings`); otherwise it unions the applicable provers cheapest first by `cost` tier. Built-in provers: transitivity (genl/genlContext, complete via the cached closures), disjointness (complete), `different` (the unique-name assumption read off the equality closure — ground only, see docs/equality.md), facts (the index), and rules (backward chaining through the same engine). ## What completeness 100 claims **For this goal shape, my answers are a superset of what every other prover reading the same sources would answer.** That is the reading that licenses running alone, and it is a claim a prover is competent to make about itself. The tempting alternative — *nothing else can answer this goal* — is a claim about a predicate, and it stops being true the moment a KB adds a second way to reach that predicate. Whether such a way exists is not a question any one prover can answer, because it is about the sources it does **not** read. So the engine asks it, once per goal, in `sole-prover`: a claimant runs alone only when `shadowing-channels` is empty. A prover therefore declares a constant and reasons only about its own sources, and a prover registered through `add-prover` is guarded without its author knowing the mechanism exists. A computed prover normally earns the claim it makes: the closure provers are built out of the very facts `FactProver` would return and out of the derivations a rule contributes, and a calculus reads both into its network — converse and composition included — before entailing anything.
Absolute tolerance for measure equality. Cross-unit normalization multiplies a
magnitude by a stored (usually floating-point) conversion factor, so exact = would
make 5 Kilogram and 5000 Gram unequal on a last-bit rounding difference. Two base
magnitudes count as equal when they differ by at most this much, and strict < / >
demand a gap wider than it — so exactly one of <, =, > holds for any pair.
Absolute (not relative) and small; rebind for a coarser or finer policy.
Absolute tolerance for measure equality. Cross-unit normalization multiplies a magnitude by a stored (usually floating-point) conversion factor, so exact `=` would make `5 Kilogram` and `5000 Gram` unequal on a last-bit rounding difference. Two base magnitudes count as equal when they differ by at most this much, and strict `<` / `>` demand a gap wider than it — so exactly one of `<`, `=`, `>` holds for any pair. Absolute (not relative) and small; rebind for a coarser or finer policy.
(aggregate-value kb goal op values context)The value an aggregate reduces to over values, or nil when there is none.
The empty extent is where the five differ, and deliberately: count is 0 and sum is 0 — the identity of each reduction, and a true answer about an empty group — while min, max and avg over nothing have no answer at all and yield no binding. A zero minimum would be a claim about a group that has no members, and an average over nothing is a division by zero however it is dressed up.
A non-numeric value under sum / min / max / avg is an error, not a silent
skip: a count of names is meaningful, an average of them is not, and quietly
dropping the non-numbers would answer a different question than the one asked. It
is recorded in the violations ledger and yields nothing — count is unaffected,
since counting is the one reduction that does not read the values.
The value an aggregate reduces to over `values`, or nil when there is none. The empty extent is where the five differ, and deliberately: **count is 0 and sum is 0** — the identity of each reduction, and a true answer about an empty group — while **min, max and avg over nothing have no answer at all** and yield no binding. A zero minimum would be a claim about a group that has no members, and an average over nothing is a division by zero however it is dressed up. A non-numeric value under `sum` / `min` / `max` / `avg` is an **error, not a silent skip**: a count of names is meaningful, an average of them is not, and quietly dropping the non-numbers would answer a different question than the one asked. It is recorded in the violations ledger and yields nothing — `count` is unaffected, since counting is the one reduction that does not read the values.
(applicable-provers kb provers goal context)The applicable provers for goal, in registry order.
One function rather than three copies of the same filterv: solve-goal-with
decides what runs, est-goal decides whether a complete estimate exists, and plan
reports both — so a sweep that drifted between them would make the diagnostic lie
about the dispatch it is there to explain.
The applicable provers for `goal`, in registry order. One function rather than three copies of the same `filterv`: `solve-goal-with` decides what runs, `est-goal` decides whether a complete estimate exists, and `plan` reports both — so a sweep that drifted between them would make the diagnostic lie about the dispatch it is there to explain.
(ask kb goal context)Answer goal in context; solution binding maps projected to the goal's
variables (a ground goal yields [{}] when provable, [] otherwise).
Answer `goal` in `context`; solution binding maps projected to the goal's
variables (a ground goal yields [{}] when provable, [] otherwise).(ask-capped kb goal context max-cost)ask, but only provers at or below the max-cost tier participate (nil = all).
A goal answerable only by a dropped tier yields nothing — the honest effect of the
qualitative bound. Lazy, for vaelii.core/ask-within to budget/collect.
`ask`, but only provers at or below the `max-cost` tier participate (nil = all). A goal answerable only by a dropped tier yields nothing — the honest effect of the qualitative bound. Lazy, for `vaelii.core/ask-within` to `budget/collect`.
(base-unit-of kb unit context)The base unit unit converts to — the second argument of its conversionFactor, or
unit itself when it declares none and is therefore its own base. Exactly the unit
normalize-quantity's magnitudes come back in, because the two read one declaration
through the same table-agreed: a unit whose factor is declined for disagreeing has its
base declined with it, so the answer is never rendered in a unit the arithmetic did not
happen in.
The base unit `unit` converts to — the second argument of its `conversionFactor`, or `unit` itself when it declares none and is therefore its own base. Exactly the unit `normalize-quantity`'s magnitudes come back in, because the two read one declaration through the same `table-agreed`: a unit whose factor is declined for disagreeing has its base declined with it, so the answer is never rendered in a unit the arithmetic did not happen in.
(candidate-rules kb goal context)Rules concluding the goal's predicate or a spec of it, restricted to the
backward-capable ones — the consequent index is complete, so it also holds
forward-only and inert rules. A rule concluding a subtype answers a supertype goal
(res/concluding-rule-handles intersects specs with the consequent index), and
subsuming-unify binds the goal variable to the subtype instance.
Each carries its exceptWhen guard (parse-rule), so a rule that would conclude
the goal but whose exception holds is discarded after the argument is built —
matching what forward chaining does before placing the conclusion.
A rule the asking context cannot see is not a candidate (res/rule-visible-from?):
a rule is a sentex, inherited by the ordinary genlContext up-cone like everything
else.
Rules concluding the goal's predicate **or a spec of it**, restricted to the backward-capable ones — the consequent index is complete, so it also holds forward-only and inert rules. A rule concluding a subtype answers a supertype goal (`res/concluding-rule-handles` intersects `specs` with the consequent index), and `subsuming-unify` binds the goal variable to the subtype instance. Each carries its `exceptWhen` guard (`parse-rule`), so a rule that would conclude the goal but whose exception holds is discarded *after* the argument is built — matching what forward chaining does before placing the conclusion. A rule the asking context cannot see is not a candidate (`res/rule-visible-from?`): a rule is a sentex, inherited by the ordinary `genlContext` up-cone like everything else.
(cost-capped-provers kb goal context max-cost)The registry minus provers whose cost tier exceeds max-cost (a tier keyword,
see cost-tiers); a nil max-cost keeps them all. This is budget's :max-cost
applied to the query engine — under time pressure, keep the cheap tiers and drop the
closures. :lookup is therefore the only ceiling that currently narrows anything:
:search is unoccupied (cost-tiers), so it and :compute keep the whole registry.
A max-cost that is not one of the three is refused, rather than read as no
ceiling at all: a caller writing :cheap for :lookup is asking to exclude the
expensive tier, and the one reading of a typo that is certainly wrong is to run it.
The registry minus provers whose `cost` tier exceeds `max-cost` (a tier keyword, see `cost-tiers`); a nil `max-cost` keeps them all. This is `budget`'s `:max-cost` applied to the query engine — under time pressure, keep the cheap tiers and drop the closures. `:lookup` is therefore the only ceiling that currently narrows anything: `:search` is unoccupied (`cost-tiers`), so it and `:compute` keep the whole registry. A `max-cost` that is not one of the three is **refused**, rather than read as no ceiling at all: a caller writing `:cheap` for `:lookup` is asking to exclude the expensive tier, and the one reading of a typo that is certainly wrong is to run it.
First-answer cost tiers, cheapest first — one question: is the answer something you look up, compute, or search for? Qualitative, not milliseconds: they name the shape of the work. A per-prover millisecond estimate would be a constant standing in for a number no implementation can compute, and a real wall-clock budget cannot be gated against that.
:lookup a bounded single-step retrieval — an O(1) ground test, a cached closure / metadata read, or one index hit (lazy to the first result) :compute a fixpoint over stored facts before the first answer (a closure) :search recursive backward chaining — open-ended proof search
cost-rank turns a tier into its ordinal. The union path orders applicable
provers by this rank (cheapest first, so a consumer taking one answer never pays
for a search when a lookup answers); budget's :max-cost uses it as a ceiling —
:lookup runs bounded retrieval only, :compute allows a closure but no search.
:search is unoccupied, and by construction: no member of the registry expands a
rule, so nothing here opens a proof search and :max-cost :compute and :max-cost :search currently select the same provers. The tier stays because the ceiling is a
claim about what a prover may cost, not a census of the shipped ones — an application
prover that backchains belongs in it, and add-prover can supply one. Rule expansion
itself is priced by the engine that does it (core/query's :max-depth), which is a
bound rather than a tier.
First-answer cost tiers, cheapest first — one question: is the answer something
you **look up**, **compute**, or **search for**? Qualitative, not milliseconds:
they name the *shape* of the work. A per-prover millisecond estimate would be a
constant standing in for a number no implementation can compute, and a real
wall-clock budget cannot be gated against that.
:lookup a bounded single-step retrieval — an O(1) ground test, a cached
closure / metadata read, or one index hit (lazy to the first result)
:compute a fixpoint over stored facts before the first answer (a closure)
:search recursive backward chaining — open-ended proof search
`cost-rank` turns a tier into its ordinal. The union path orders applicable
provers by this rank (cheapest first, so a consumer taking one answer never pays
for a search when a lookup answers); `budget`'s `:max-cost` uses it as a ceiling —
`:lookup` runs bounded retrieval only, `:compute` allows a closure but no search.
**`:search` is unoccupied**, and by construction: no member of the registry expands a
rule, so nothing here opens a proof search and `:max-cost :compute` and `:max-cost
:search` currently select the same provers. The tier stays because the ceiling is a
claim about *what a prover may cost*, not a census of the shipped ones — an application
prover that backchains belongs in it, and `add-prover` can supply one. Rule expansion
itself is priced by the engine that does it (`core/query`'s `:max-depth`), which is a
bound rather than a tier.(est-goal kb goal context)How many bindings the registry expects to produce for goal, or nil when it
has no authoritative answer.
Only a complete prover's estimate is returned, and deliberately so. This mirrors
solve-goal-with: when a complete prover exists the engine runs it alone, so its
estimate is the whole cost of the goal. When none does, the engine unions partial
provers over the index, and their estimates are guesses about a fan-out the index
models better — so nil, and vaelii.impl.plan uses its own count-aware model
instead. Returning a partial prover's number here would replace a measurement with
a constant (ArgTypeProver answers 3 for everything).
How many bindings the registry expects to produce for `goal`, or **nil** when it has no authoritative answer. Only a *complete* prover's estimate is returned, and deliberately so. This mirrors `solve-goal-with`: when a complete prover exists the engine runs it *alone*, so its estimate is the whole cost of the goal. When none does, the engine unions partial provers over the index, and their estimates are guesses about a fan-out the index models better — so nil, and `vaelii.impl.plan` uses its own count-aware model instead. Returning a partial prover's number here would replace a measurement with a constant (`ArgTypeProver` answers 3 for everything).
Predicates a prover computes from ground numeric arguments rather than looks up.
Both are variable arity — (lessThan 1 2 3) reads as the chain 1 < 2 < 3.
greaterThan is folded to lessThan when stored (see vaelii.impl.sentex), but a
caller may still ask it directly, so both are answered here.
Predicates a prover computes from ground numeric arguments rather than looks up. Both are **variable arity** — `(lessThan 1 2 3)` reads as the chain 1 < 2 < 3. `greaterThan` is folded to `lessThan` when *stored* (see `vaelii.impl.sentex`), but a caller may still ask it directly, so both are answered here.
(exception-holds? kb except bindings context)Does except — a rule's exceptWhen query, a vector of literals — hold under
bindings, evaluated in context?
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.solve-goal-with is lazy, so take 1 stops the query at
its first result instead of 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 or absent exception never holds, so an ordinary
rule pays nothing here. See docs/exceptions.md.
Does `except` — a rule's `exceptWhen` query, a vector of literals — hold under `bindings`, evaluated in `context`? 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.** `solve-goal-with` is lazy, so `take 1` stops the query at its first result instead of enumerating an extent. * **No backchaining.** Nothing in the registry expands a rule, so an exception can reach through genl specificity, the genlContext closure, the transitive / symmetric / inverse metadata, disjointness and the evaluables — but never invokes an unbounded proof search from inside the relabel loop. **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 or absent exception never holds, so an ordinary rule pays nothing here. See docs/exceptions.md.
(exceptions-block? kb handle bindings context)Is a firing of rule handle blocked by any of its exceptWhen exceptions under
bindings, evaluated in context? Block-if-any-conjunction-holds. An ordinary
rule (no exception) yields no conjunctions and pays nothing past the roster gate.
Is a firing of rule `handle` blocked by any of its exceptWhen exceptions under `bindings`, evaluated in `context`? Block-if-**any**-conjunction-holds. An ordinary rule (no exception) yields no conjunctions and pays nothing past the roster gate.
The measure-comparison predicates QuantityProver answers — check-only over two
ground measures, never stored (declared in the upper MeasureContext, computed here).
The measure-comparison predicates `QuantityProver` answers — check-only over two ground measures, never stored (declared in the upper MeasureContext, computed here).
(measure? x)Is x a ground measure term — (QuantityFn N Unit) or
(QuantityIntervalFn Lo Hi Unit), numeric magnitude(s) and a symbol unit? The
check-only gate: a comparison is claimed only when both arguments are ground
measures, so (sameQuantity ?x M) is refused, never enumerated.
Public because it is the shared answer to "is this a measure?": every prover that reads one — the comparison here, the durations, the metric temporal network — must agree on the question, and three copies of this could not be kept agreeing.
Is `x` a ground measure term — `(QuantityFn N Unit)` or `(QuantityIntervalFn Lo Hi Unit)`, numeric magnitude(s) and a symbol unit? The check-only gate: a comparison is claimed only when *both* arguments are ground measures, so `(sameQuantity ?x M)` is refused, never enumerated. Public because it is the shared answer to "is this a measure?": every prover that reads one — the comparison here, the durations, the metric temporal network — must agree on the question, and three copies of this could not be kept agreeing.
(normalize-quantity kb measure context)Resolve a ground measure to [dimension lo-base hi-base] — its dimension and its
magnitude bounds converted direct-to-base (one multiply, no chaining). A point
(QuantityFn N U) has lo-base = hi-base; an interval keeps both bounds.
(dimensionOf U ?d), or U itself when the unit declares none —
so two measures in the same unit are always comparable (their dimension is that
unit) while two distinct undeclared units are not (their dimensions differ). A
declared dimensionOf is what lets separate units share one dimension and compare.N × (conversionFactor U ?base ?factor), the factor
defaulting to 1 when the unit declares none (it is then its own base). Every unit
of one dimension must convert to a single base unit for the magnitudes to line up
— the direct-to-base contract, no transitive chaining.A unit the KB declares twice over and differently has declared nothing: both reads
go through table-agreed, so such a unit falls back to being its own dimension and its
own base rather than converting by whichever declaration is indexed first. Nothing is
answered wrongly and nothing is answered differently in another load order — the price
is that the unit compares only against itself, which is what a KB that cannot say how
long a Furlong is has actually told the engine.
Resolve a ground measure to `[dimension lo-base hi-base]` — its dimension and its magnitude bounds converted **direct-to-base** (one multiply, no chaining). A point `(QuantityFn N U)` has `lo-base = hi-base`; an interval keeps both bounds. * **Dimension** is `(dimensionOf U ?d)`, or **U itself** when the unit declares none — so two measures in the *same unit* are always comparable (their dimension is that unit) while two distinct undeclared units are not (their dimensions differ). A declared `dimensionOf` is what lets separate units share one dimension and compare. * **Base magnitude** is `N × (conversionFactor U ?base ?factor)`, the factor defaulting to `1` when the unit declares none (it is then its own base). Every unit of one dimension must convert to a *single* base unit for the magnitudes to line up — the direct-to-base contract, no transitive chaining. A unit the KB declares **twice over and differently** has declared nothing: both reads go through `table-agreed`, so such a unit falls back to being its own dimension and its own base rather than converting by whichever declaration is indexed first. Nothing is answered wrongly and nothing is answered differently in another load order — the price is that the unit compares only against itself, which is what a KB that cannot say how long a Furlong is has actually told the engine.
(parse-rule kb rule-sentex context)A rule sentex as the chainers' parsed map — antecedents, consequent, the exceptWhen
guard if it has one, and the rule's own :handle, which is what an executor
accumulating supports records (vaelii.impl.inference).
A rule sentex as the chainers' parsed map — antecedents, consequent, the `exceptWhen` guard if it has one, and the rule's own `:handle`, which is what an executor accumulating supports records (`vaelii.impl.inference`).
(plan kb goal context)The applicable provers for a goal, their estimates, and — the part a reader debugging a missing answer needs first — which of them actually run.
Applicable is not the same as consulted. When one prover may answer the goal alone
every other applicable prover is shadowed: reported, never invoked, contributing
nothing. A plan that listed them without saying so reads as a union that is not
happening. So each entry carries :runs?, and a shadowed one carries
:shadowed-by naming the prover that displaced it.
The converse case is reported too, and from outside it is the one that looks like a
bug. A prover can claim completeness 100 and still not run alone, because a source
none of the applicable provers reads bears on this goal — so every claimant runs in
the union instead. Those entries carry :guarded-by naming the channels
(shadowing-channels), which is the difference between the union is happening and
the union is happening for this reason.
Entries are in the order the engine would consult them: a single complete prover,
else cheapest cost tier first.
The applicable provers for a goal, their estimates, and — the part a reader debugging a missing answer needs first — **which of them actually run**. Applicable is not the same as consulted. When one prover may answer the goal alone every other applicable prover is *shadowed*: reported, never invoked, contributing nothing. A plan that listed them without saying so reads as a union that is not happening. So each entry carries `:runs?`, and a shadowed one carries `:shadowed-by` naming the prover that displaced it. The converse case is reported too, and from outside it is the one that looks like a bug. A prover can claim `completeness` 100 and still not run alone, because a source none of the applicable provers reads bears on this goal — so every claimant runs in the union instead. Those entries carry `:guarded-by` naming the channels (`shadowing-channels`), which is the difference between *the union is happening* and *the union is happening for this reason*. Entries are in the order the engine would consult them: a single complete prover, else cheapest `cost` tier first.
(applicable? prover kb goal context)(completeness prover kb goal context)(cost prover kb goal context)(est-bindings prover kb goal context)(solve prover kb goal context)(registry kb)(registry-est-override kb context)est-goal as the :est-override a backward chainer plans with (res/prove-from,
res/initial-prove-stack) — for an executor whose leaf is the registry, and only
such an executor.
The index is the wrong cost model for that leaf: a genl conjunct is answered from the
cached closure, so what it costs is the closure's size, not the handful of stored edges
the trie can count — and the index model would rank the literal that fans out over a
whole type hierarchy as the cheapest in the conjunction. A chainer whose leaf is the
stored facts passes nothing here, because for that leaf the index model is right.
Memoized on the goal, which is sound in both directions: est-goal reads only the
goal (kb and context are fixed for the run, and its bound argument is ignored — a
complete prover's estimate is the whole cost of the goal, not of a partial binding),
and a query mutates nothing that could make an entry stale. Without the memo
plan/order re-estimates every remaining literal on every pick, so a k-antecedent
rule pays a full registry applicable? sweep plus a candidate-rule re-parse O(k²)
times.
`est-goal` as the `:est-override` a backward chainer plans with (`res/prove-from`, `res/initial-prove-stack`) — for an executor whose **leaf is the registry**, and only such an executor. The index is the wrong cost model for that leaf: a `genl` conjunct is answered from the cached closure, so what it costs is the closure's size, not the handful of stored edges the trie can count — and the index model would rank the literal that fans out over a whole type hierarchy as the *cheapest* in the conjunction. A chainer whose leaf is the stored facts passes nothing here, because for that leaf the index model is right. Memoized on the goal, which is sound in both directions: `est-goal` reads only the goal (kb and context are fixed for the run, and its `bound` argument is ignored — a complete prover's estimate is the whole cost of the goal, not of a partial binding), and a query mutates nothing that could make an entry stale. Without the memo `plan/order` re-estimates every remaining literal on every pick, so a k-antecedent rule pays a full registry `applicable?` sweep plus a candidate-rule re-parse O(k²) times.
(render-quantity lo hi unit)The measure the bounds [lo hi] in unit denote: a point when they coincide, an
interval when they do not. That is what keeps a computed answer honest — an
over-approximation renders as an interval and says so, rather than picking a figure
out of a range it only bounded.
The measure the bounds `[lo hi]` in `unit` denote: a **point** when they coincide, an **interval** when they do not. That is what keeps a computed answer honest — an over-approximation renders as an interval and says so, rather than picking a figure out of a range it only bounded.
(round-magnitude x)Snap a computed magnitude to the tolerance grid, and hand back a long when what is
left is a whole number. Two reasons, and only the second is cosmetic: a sum of
converted magnitudes carries float noise that would render as 2.5000000000000004,
and a rendered (QuantityFn 9000.0 Second) is not = to the (QuantityFn 9000 Second) a caller would write, so a bound answer would not compare equal to the
obvious way of writing it.
Snap a computed magnitude to the tolerance grid, and hand back a long when what is left is a whole number. Two reasons, and only the second is cosmetic: a sum of converted magnitudes carries float noise that would render as `2.5000000000000004`, and a rendered `(QuantityFn 9000.0 Second)` is not `=` to the `(QuantityFn 9000 Second)` a caller would write, so a bound answer would not compare equal to the obvious way of writing it.
(rule-exceptions kb handle)The exceptWhen exceptions currently in force for the rule at handle — a seq of
conjunctions (each a vector of literals), evaluated block-if-any-holds.
An exception is a separate belief-following meta-sentex (exceptWhen Q (sentexHandle handle)): the rule and its exceptions are distinct assertions, so a rule and its
unexcepted twin share one handle and asserting or retracting an exception amends the
rule in place. Each such meta-sentex contributes one conjunction; multiple ones are
independent "unless" clauses (birds fly unless penguins, unless ostriches — block
if either holds), while the conjuncts within one exception all must hold. The
query is stored in the rule's canonical variable names (aligned when the exception
was asserted), so a firing's bindings substitute straight in.
Believed only: a defeated or retracted exceptWhen stops blocking, exactly as a
cached relation follows belief. Gated on the exception-rule roster by the callers,
so an ordinary rule never reaches the term-index lookup.
The exceptWhen exceptions currently in force for the rule at `handle` — a seq of **conjunctions** (each a vector of literals), evaluated block-if-**any**-holds. An exception is a separate belief-following meta-sentex `(exceptWhen Q (sentexHandle handle))`: the rule and its exceptions are distinct assertions, so a rule and its unexcepted twin share one handle and asserting or retracting an exception amends the rule in place. Each such meta-sentex contributes one conjunction; multiple ones are independent "unless" clauses (birds fly unless penguins, unless ostriches — block if either holds), while the conjuncts *within* one exception all must hold. The query is stored in the rule's canonical variable names (aligned when the exception was asserted), so a firing's bindings substitute straight in. Believed only: a defeated or retracted `exceptWhen` stops blocking, exactly as a cached relation follows belief. Gated on the exception-rule roster by the callers, so an ordinary rule never reaches the term-index lookup.
(rule-guard kb rule-sentex context)The firing guard for a rule handle, or nil when the rule carries no exception.
A guard is a predicate on a firing's completed bindings that is true when the firing is permitted — false exactly when one of the rule's exceptions holds. Attaching it to the parsed rule map is what lets the backward chainers construct the argument and then discard it, which is the same decision forward chaining makes before placing a conclusion.
Backward there is no placement context, so the exception is evaluated in the query's context — the nearest analogue to "where the conclusion would live", and the context the caller is asking from.
The firing guard for a rule handle, or nil when the rule carries no exception. A guard is a predicate on a firing's completed bindings that is **true when the firing is permitted** — false exactly when one of the rule's exceptions holds. Attaching it to the parsed rule map is what lets the backward chainers construct the argument and then discard it, which is the same decision forward chaining makes before placing a conclusion. Backward there is no placement context, so the exception is evaluated in the **query's** context — the nearest analogue to "where the conclusion would live", and the context the caller is asking from.
(shadowing-channels kb goal context)The ways this KB could reach goal that a computed prover does not read — the
set a conditionally-complete prover checks before claiming its answers are a
superset of everyone else's (see the completeness contract at the head of this file).
Three channels, each found by differencing: run the complete prover alone, run every other applicable prover, and see what only the second answers.
:preserving — an (argPreserving P n R) declaration licenses a claim about a
tuple that appears in no stored fact, in no rule conclusion and in no constraint
network, so nothing computed from those three can contain it.:rules — a rule concluding the goal's predicate, or a spec of it. A forward
rule's conclusion is stored when it fires and so is absorbed, but a
set/backwardRule never fires forward: its conclusion exists only while a
backchainer is looking for it, and no member of the registry is one. So a complete
prover here is claiming a superset of what the registry answers, while the rule is
reached by an executor above it — and the claim has to be read in that scope or it
over-reaches: it would let a computed answer stand in for a leaf the node engine or
prove is about to expand a rule under. Not narrowed to backward-only rules: a
forward rule is absorbed only if the fixpoint actually ran to it, which
{:chain? false} and :max-depth can both prevent, and being wrong here costs a
union rather than an answer.:inverse — a declared (inverse P Q) where the goal is about P. A
calculus applies its algebra's own converse within its vocabulary, and the
taxonomy closures are keyed on their own functor, so neither reads a partner
predicate stored under a different name. Measured the same way, on genl and on
partOfRegion.What is absorbed, and it is worth being exact since a missing entry here is a missing answer:
symmetric / transitive / reflexive over a predicate a calculus owns are the
algebra's own composition and converse;argIsa type inference and the metadata provers answer goal shapes no computed
prover claims, so they are never shadowed in the first place.Cheap by construction on the two that could be hot: inherit/positions is behind a
root-intersection gate on any declaration naming this predicate, and
tax/inverse-of is a cached taxonomy read. concluding-rule-handles is the one
that touches the index, and it is the spec closure probed against the consequent
index — bounded by the concluding-rule count, never the taxonomy.
The ways this KB could reach `goal` that a **computed** prover does not read — the
set a conditionally-complete prover checks before claiming its answers are a
superset of everyone else's (see the completeness contract at the head of this file).
Three channels, each found by differencing: run the complete prover alone, run every
other applicable prover, and see what only the second answers.
* **`:preserving`** — an `(argPreserving P n R)` declaration licenses a claim about a
tuple that appears in no stored fact, in no rule conclusion and in no constraint
network, so nothing computed from those three can contain it.
* **`:rules`** — a rule concluding the goal's predicate, or a spec of it. A *forward*
rule's conclusion is stored when it fires and so is absorbed, but a
`set/backwardRule` never fires forward: its conclusion exists only while a
backchainer is looking for it, and no member of the registry is one. So a complete
prover here is claiming a superset of what the *registry* answers, while the rule is
reached by an executor above it — and the claim has to be read in that scope or it
over-reaches: it would let a computed answer stand in for a leaf the node engine or
`prove` is about to expand a rule under. Not narrowed to backward-only rules: a
forward rule is absorbed only if the fixpoint actually ran to it, which
`{:chain? false}` and `:max-depth` can both prevent, and being wrong here costs a
union rather than an answer.
* **`:inverse`** — a declared `(inverse P Q)` where the goal is about `P`. A
calculus applies its algebra's own converse *within its vocabulary*, and the
taxonomy closures are keyed on their own functor, so neither reads a partner
predicate stored under a different name. Measured the same way, on `genl` and on
`partOfRegion`.
What is **absorbed**, and it is worth being exact since a missing entry here is a
missing answer:
* a **stored fact** is what the closures are built out of and what a calculus reads
into its network;
* a **merged term** is rewritten into the goal before any prover sees it, so an
equality reaches a computed prover already applied;
* `symmetric` / `transitive` / `reflexive` over a predicate a calculus owns are the
algebra's own composition and converse;
* `argIsa` type inference and the metadata provers answer goal shapes no computed
prover claims, so they are never shadowed in the first place.
Cheap by construction on the two that could be hot: `inherit/positions` is behind a
root-intersection gate on any declaration naming this predicate, and
`tax/inverse-of` is a cached taxonomy read. `concluding-rule-handles` is the one
that touches the index, and it is the spec closure probed against the consequent
index — bounded by the concluding-rule count, never the taxonomy.(sole-prover kb applicable goal context)The prover that may answer goal alone, or nil for the union path.
Two conditions, and they are asked of different parties. A prover claims
completeness 100 — for this goal shape, my answers subsume every prover whose
sources I read — which is a claim it is competent to make about itself. The engine
then asks the question no single prover can: is there a source none of them reads
(shadowing-channels)? If so, nobody runs alone, whatever they claimed.
Putting the guard here rather than in each prover is what makes it hold. A fourth
channel is one edit instead of one per claimant; a prover registered through
add-prover is guarded without its author knowing the mechanism exists; and no
prover has to reason about sources outside its own.
Guarding is safe in one direction only, and it is the safe one: it can move a
goal from one prover to the union, never the reverse, and the union path includes the
claimant — so a guard that fires unnecessarily costs a lazy prover that may never be
forced, while one that fails to fire loses an answer. That asymmetry is why the
channels are asked of every claimant alike, including the ones whose goal shape is
unstorable (different, unknown, thereExists, an aggregate): they need no
exemption, because for them no channel ever bears.
The channels are read once per goal — they are a property of the goal and the KB, not of the prover asking.
The prover that may answer `goal` **alone**, or nil for the union path. Two conditions, and they are asked of different parties. A prover claims `completeness` 100 — *for this goal shape, my answers subsume every prover whose sources I read* — which is a claim it is competent to make about itself. The engine then asks the question no single prover can: **is there a source none of them reads** (`shadowing-channels`)? If so, nobody runs alone, whatever they claimed. Putting the guard here rather than in each prover is what makes it hold. A fourth channel is one edit instead of one per claimant; a prover registered through `add-prover` is guarded without its author knowing the mechanism exists; and no prover has to reason about sources outside its own. Guarding is **safe in one direction only, and it is the safe one**: it can move a goal from one prover to the union, never the reverse, and the union path includes the claimant — so a guard that fires unnecessarily costs a lazy prover that may never be forced, while one that fails to fire loses an answer. That asymmetry is why the channels are asked of every claimant alike, including the ones whose goal shape is unstorable (`different`, `unknown`, `thereExists`, an aggregate): they need no exemption, because for them no channel ever bears. The channels are read **once per goal** — they are a property of the goal and the KB, not of the prover asking.
(solve-goal kb goal context)Raw solution bindings for goal in context via the applicable provers.
Raw solution bindings for `goal` in `context` via the applicable provers.
(solve-goal-with kb provers goal context)Raw solution bindings for goal in context from an explicit prover list.
Lazy: provers are ordered by cost tier and expanded one at a time, so the
cheapest first-answer prover is consulted first and an expensive one is never
invoked at all if the consumer stops early. (The complete-prover branch runs one
prover, so its laziness is whatever that prover returns.)
When several complete provers apply — rare, since the complete provers claim
pairwise-disjoint goal shapes — the one with the fewest est-bindings runs, a
real count rather than a constant.
res/lazy-mapcat, not mapcat: the ordinary one would realize a whole chunk of
the prover list and so call every applicable prover's solve before yielding
the first solution — which is precisely the cost the cheapest-first ordering is
there to avoid.
Raw solution bindings for `goal` in `context` from an explicit prover list. Lazy: provers are ordered by `cost` tier and expanded one at a time, so the cheapest first-answer prover is consulted first and an expensive one is never invoked at all if the consumer stops early. (The complete-prover branch runs one prover, so its laziness is whatever that prover returns.) When several *complete* provers apply — rare, since the complete provers claim pairwise-disjoint goal shapes — the one with the fewest `est-bindings` runs, a real count rather than a constant. `res/lazy-mapcat`, not `mapcat`: the ordinary one would realize a whole chunk of the prover list and so call *every* applicable prover's `solve` before yielding the first solution — which is precisely the cost the cheapest-first ordering is there to avoid.
(transitive-prover? pr)Does this prover compute a transitive closure — genl/genlContext through the cached
taxonomy, or a predicate declared (transitive P)?
Does this prover compute a transitive closure — genl/genlContext through the cached taxonomy, or a predicate declared `(transitive P)`?
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 |