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/genlCx,
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/genlCx, 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.
The most reach members one KB's closure cache holds before it is dropped
wholesale. Members, not entries, and that is the whole of the design: an entry here is
a whole reach set, so ten entries can be ten members or a million, and a bound counting
entries would bound nothing. A single reach larger than this is never stored — it is
the case the bound exists for — and a total that reaches it drops the map rather than
evicting entry by entry, the wholesale clearing literal-cache and observe take and
for the reason they give.
Dynamic so a test can drive the bound rather than build a corpus large enough to reach it — the bound is a decision, and one nothing exercises is one nothing checks.
The most reach **members** one KB's closure cache holds before it is dropped wholesale. Members, not entries, and that is the whole of the design: an entry here is a whole reach set, so ten entries can be ten members or a million, and a bound counting entries would bound nothing. A single reach larger than this is never stored — it is the case the bound exists for — and a total that reaches it drops the map rather than evicting entry by entry, the wholesale clearing `literal-cache` and `observe` take and for the reason they give. Dynamic so a test can drive the bound rather than build a corpus large enough to reach it — the bound is a decision, and one nothing exercises is one nothing checks.
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, and the
rounding grid a computed magnitude is snapped to follows the rebinding
(tolerance-scale).
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, and the rounding grid a computed magnitude is snapped to follows the rebinding (`tolerance-scale`).
(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)base-unit-with-support's unit alone, for a caller with no use for the declaration
behind it.
`base-unit-with-support`'s unit alone, for a caller with no use for the declaration behind it.
(base-unit-with-support kb unit context)The base unit unit converts to, and the declaration that says so: [base handles].
The second argument of its conversionFactor, or unit itself when it declares none
and is therefore its own base — the latter with empty support, for
normalize-quantity-with-support's reason.
Exactly the unit normalize-quantity's magnitudes come back in, because the two read
one declaration through the same table-read: 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, and the declaration that says so: `[base handles]`. The second argument of its `conversionFactor`, or `unit` itself when it declares none and is therefore its own base — the latter with empty support, for `normalize-quantity-with-support`'s reason. Exactly the unit `normalize-quantity`'s magnitudes come back in, because the two read one declaration through the same `table-read`: 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 genlCx up-cone like everything
else. Nor is a rule the KB no longer believes (res/rule-believed?) — the
consequent index posts on storage, so belief is asked of the record here exactly as
forward chaining asks it of a trigger.
In content order, [sentence context] under nm/compare-form. The index answers
in handle-set order, which is assertion order, and two consumers truncate on this
list: prove-within's :max-results stops the DFS partway through the rules it would
have expanded, and the node engine's frontier is filled from children, which walks it.
So without an order here the same knowledge in two arrival orders answers a capped query
with two different answer sets — order independence, broken by the one thing that is
never allowed to break it (docs/nmtms.md).
The key needs no memo, which is why there is none: the sentence is the key, already
a field on the record, and compare-form walks two forms in place rather than printing
either. So the sort builds one two-element vector per candidate and allocates nothing
else — against a print-key per rule, which would be a String per candidate per
comparison were it not decorated first. :context joins it because one sentence stated
in two contexts is two rules, and a key that could not tell them apart would drop the
tie back onto the handle.
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 `genlCx` up-cone like everything else. Nor is a rule the KB no longer believes (`res/rule-believed?`) — the consequent index posts on storage, so belief is asked of the record here exactly as forward chaining asks it of a trigger. **In content order**, `[sentence context]` under `nm/compare-form`. The index answers in handle-set order, which is assertion order, and two consumers *truncate* on this list: `prove-within`'s `:max-results` stops the DFS partway through the rules it would have expanded, and the node engine's frontier is filled from `children`, which walks it. So without an order here the same knowledge in two arrival orders answers a capped query with two different answer sets — order independence, broken by the one thing that is never allowed to break it (docs/nmtms.md). The key needs no memo, which is why there is none: the sentence **is** the key, already a field on the record, and `compare-form` walks two forms in place rather than printing either. So the sort builds one two-element vector per candidate and allocates nothing else — against a `print-key` per rule, which would be a String per candidate per comparison were it not decorated first. `:context` joins it because one sentence stated in two contexts is two rules, and a key that could not tell them apart would drop the tie back onto the handle.
(closed-extent? kb pred context)Is pred's believed extent declared complete as read from context — is
(closedExtentPredicate pred) visible up its genlCx cone?
Scoped, like abduciblePredicate and modalPredicate and for their reason: this is a
policy of the context that grants it, not a claim about the predicate that holds
wherever it is mentioned. One theory may be willing to read a vocabulary's extent as
complete where another, reading the same predicate, will not.
Is `pred`'s believed extent declared **complete** as read from `context` — is `(closedExtentPredicate pred)` visible up its `genlCx` cone? Scoped, like `abduciblePredicate` and `modalPredicate` and for their reason: this is a *policy* of the context that grants it, not a claim about the predicate that holds wherever it is mentioned. One theory may be willing to read a vocabulary's extent as complete where another, reading the same predicate, will not.
(conjunction-derivable? kb conjuncts bindings context)(conjunction-derivable? kb conjuncts bindings context norm)Does the conjunctive level-6 body conjuncts have a solution under bindings in
context? An empty conjunction has none: nothing can make it derivable, which is
the reading an empty exception has always taken.
Does the conjunctive level-6 body `conjuncts` have a solution under `bindings` in `context`? An **empty** conjunction has none: nothing can make it derivable, which is the reading an empty exception has always taken.
(conjunction-solutions kb conjuncts bindings context)(conjunction-solutions kb conjuncts bindings context norm)Lazy solutions of the conjunctive level-6 body conjuncts, extending bindings, in
context — the joined NAF evaluator, and the only one.
Each conjunct is substituted with what the conjuncts before it bound, put in the normal
form the context answers under (norm, or nil for none), and run through the registry;
the solutions thread on. Four properties, and the last is the one reading the
conjuncts independently cannot give:
res/lazy-mapcat throughout, so a caller taking one
solution never enumerates an extent.(unknown (thereExists ?c (and (childOf Tom ?c) (sick ?c)))) asks for one
witness satisfying both — which is what its author means, and what reading the
conjuncts independently could not say (docs/naf.md, docs/defenses.md).A ground conjunction is the degenerate case and is unchanged by the join: every
conjunct substitutes to a ground goal, each contributes {} or nothing, and the
result is exactly the independent existence checks an exceptWhen has always been.
Lazy solutions of the conjunctive level-6 body `conjuncts`, extending `bindings`, in
`context` — **the** joined NAF evaluator, and the only one.
Each conjunct is substituted with what the conjuncts before it bound, put in the normal
form the context answers under (`norm`, or nil for none), and run through the registry;
the solutions thread on. Four properties, and the last is the one reading the
conjuncts independently cannot give:
* **All must hold.** A conjunction is derivable only if every conjunct is, which a
join says by having no solution the moment one of them contributes none.
* **One answer suffices.** `res/lazy-mapcat` throughout, so a caller taking one
solution never enumerates an extent.
* **No backchaining.** The registry expands no rule, so this reaches genl
specificity, the genlCx closure, the transitive / symmetric / inverse metadata,
disjointness and the evaluables, and never starts a proof search from inside the
relabel loop.
* **The conjuncts may share a variable.** A quantifier binds it and the join carries
it, so `(unknown (thereExists ?c (and (childOf Tom ?c) (sick ?c))))` asks for one
witness satisfying both — which is what its author means, and what reading the
conjuncts independently could not say (docs/naf.md, docs/defenses.md).
A **ground** conjunction is the degenerate case and is unchanged by the join: every
conjunct substitutes to a ground goal, each contributes `{}` or nothing, and the
result is exactly the independent existence checks an `exceptWhen` has always been.(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.
(evaluatable pred f)(evaluatable pred
f
{:keys [result arity]
cost-tier :cost
complete :completeness
:or {cost-tier :lookup complete 100}})A Prover wrapping the plain Clojure fn f as the evaluatable predicate/function
pred — the value vaelii.core/add-evaluatable registers. Answers a goal by
computing, never by looking one up, in one of two shapes:
:result) — (pred a …) holds when f applied to the ground
arguments returns truthy, like lessThan. Every argument must be ground.:result names an output slot) — (pred … ?out …) binds ?out
to (f <the other, ground arguments>), like evaluate. A ground output slot is
checked against the computed value instead of bound.opts (a map, or nil):
:result — :first (the evaluate convention), :last, or a 0-based index;
its presence selects the result-binding shape.:arity — the fn's input count (an int or a set of them), for applicable?
to dispatch on; derived from f by reflection when omitted, which a
variadic fn needs stated.:cost — a cost-tiers keyword; :lookup by default.:completeness — 0..100; 100 by default, the authoritative-computation claim the
built-in evaluables make (sole-prover still guards it against a
shadowing rule/inverse the KB adds). Drop it to 50 for a predicate a
KB also stores facts under, so the computed answers augment the
stored ones instead of standing alone.Registered through add-prover, so a wrapped fn is an ordinary member of the registry:
it answers a direct ask / query goal, and — because the node engine's leaf is
the registry — it discharges a conjunct or a rule antecedent inside a query with a
:max-depth, appearing as a :leaf in a {:proof? true} derivation. Forward
materialization reaches it too: vaelii.impl.chain/deferred-antecedent? treats a
registered evaluatable as a deferred antecedent, computing it through this registry the
way it computes the built-in vaelii.impl.sentex/deferred-predicates, so ask agrees
with query on a forward rule with an evaluatable antecedent. One path does not reach
it, by the existing engine's design rather than this wrapper's: the DFS prove, whose
leaf is the stored facts. See the query-engine section of docs/inference.md.
A `Prover` wrapping the plain Clojure fn `f` as the evaluatable predicate/function
`pred` — the value `vaelii.core/add-evaluatable` registers. Answers a goal by
**computing**, never by looking one up, in one of two shapes:
* **check** (no `:result`) — `(pred a …)` holds when `f` applied to the ground
arguments returns truthy, like `lessThan`. Every argument must be ground.
* **result-binding** (`:result` names an output slot) — `(pred … ?out …)` binds `?out`
to `(f <the other, ground arguments>)`, like `evaluate`. A ground output slot is
checked against the computed value instead of bound.
`opts` (a map, or nil):
* `:result` — `:first` (the `evaluate` convention), `:last`, or a 0-based index;
its presence selects the result-binding shape.
* `:arity` — the fn's **input** count (an int or a set of them), for `applicable?`
to dispatch on; derived from `f` by reflection when omitted, which a
variadic fn needs stated.
* `:cost` — a `cost-tiers` keyword; `:lookup` by default.
* `:completeness` — 0..100; **100** by default, the authoritative-computation claim the
built-in evaluables make (`sole-prover` still guards it against a
shadowing rule/inverse the KB adds). Drop it to 50 for a predicate a
KB also stores facts under, so the computed answers *augment* the
stored ones instead of standing alone.
Registered through `add-prover`, so a wrapped fn is an ordinary member of the registry:
it answers a direct `ask` / `query` goal, and — because the node engine's leaf **is**
the registry — it discharges a conjunct or a rule antecedent inside a `query` with a
`:max-depth`, appearing as a `:leaf` in a `{:proof? true}` derivation. **Forward
materialization reaches it too**: `vaelii.impl.chain/deferred-antecedent?` treats a
registered evaluatable as a deferred antecedent, computing it through this registry the
way it computes the built-in `vaelii.impl.sentex/deferred-predicates`, so `ask` agrees
with `query` on a forward rule with an evaluatable antecedent. One path does not reach
it, by the existing engine's design rather than this wrapper's: the DFS `prove`, whose
leaf is the stored facts. See the query-engine section of docs/inference.md.(evaluatable-est-override preds)An :est-override for vaelii.impl.plan/order that costs only preds — a KB's
registered evaluatable functors (evaluatable-preds) — and returns nil for every
other goal so the index model ranks the rest. A goal still carrying an unbound input
is reported as maximally unselective (deferred-est) and a fully ground one as the
single answer it computes, so the planner runs the generators that bind its inputs
first and the computation lands with everything ground.
Forward chaining (vaelii.impl.chain/planned-join) plans with this so a registered
evaluatable antecedent is pinned after its binders — the self-deferral the built-in
evaluables get for free from canonical antecedent order, which the static
deferred-predicates set drives and a per-KB evaluatable is not in. Scoped to the
evaluatables on purpose: forward chaining's leaf is the stored facts (*matcher*),
for which the index model is the right cost, so every other goal is left to it.
Nil when preds is empty, so planned-join passes no override and plans exactly as
before.
An `:est-override` for `vaelii.impl.plan/order` that costs only `preds` — a KB's registered evaluatable functors (`evaluatable-preds`) — and returns nil for every other goal so the index model ranks the rest. A goal still carrying an unbound input is reported as maximally unselective (`deferred-est`) and a fully ground one as the single answer it computes, so the planner runs the generators that bind its inputs first and the computation lands with everything ground. Forward chaining (`vaelii.impl.chain/planned-join`) plans with this so a registered evaluatable antecedent is pinned after its binders — the self-deferral the built-in evaluables get for free from canonical antecedent order, which the static `deferred-predicates` set drives and a per-KB evaluatable is not in. Scoped to the evaluatables on purpose: forward chaining's leaf is the stored facts (`*matcher*`), for which the index model is the right cost, so every other goal is left to it. Nil when `preds` is empty, so `planned-join` passes no override and plans exactly as before.
(evaluatable-preds kb)The set of predicate functors a KB has registered as evaluatables through
vaelii.core/add-evaluatable — the EvaluatableFn provers in its registry.
Forward chaining reads this to treat a registered evaluatable the way it treats the
built-in vaelii.impl.sentex/deferred-predicates: computed from the bindings the
other antecedents produced, through the registry, never looked up as a stored fact.
The built-ins are a static set because they are always present; the evaluatables are
per-KB, so this set is read off the KB's live registry. Empty for a KB with no
registered evaluatables — the default registry has none.
The set of predicate functors a KB has registered as evaluatables through `vaelii.core/add-evaluatable` — the `EvaluatableFn` provers in its registry. Forward chaining reads this to treat a registered evaluatable the way it treats the built-in `vaelii.impl.sentex/deferred-predicates`: **computed** from the bindings the other antecedents produced, through the registry, never looked up as a stored fact. The built-ins are a static set because they are always present; the evaluatables are per-KB, so this set is read off the KB's live registry. Empty for a KB with no registered evaluatables — the default registry has none.
(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 and the conjuncts
share nothing. They are still run through conjunction-solutions, the joined
evaluator an unknown's query takes: on a ground conjunction a join is the
independent existence check, and one evaluator is what keeps the two from drifting.conjunction-solutions is lazy throughout, 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 arg, 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 and the conjuncts share nothing. They are still run through `conjunction-solutions`, the joined evaluator an `unknown`'s query takes: on a ground conjunction a join *is* the independent existence check, and one evaluator is what keeps the two from drifting. * **One answer suffices.** `conjunction-solutions` is lazy throughout, 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 genlCx 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 `arg`, 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.
(fact-prover? pr)Is this the stored-fact prover — the one that answers by matching the store, and whose answers therefore each name a sentex with a context?
vaelii.impl.vantage asks it of every applicable prover to decide whether a literal is
inside post-hoc placement's domain. A goal only this one answers is a goal every answer
to which can be placed, because every answer came from somewhere; a goal any other
prover also answers has answers computed rather than stored — a closure walk, an
evaluable, an inferred argument type — and those name no context to place by.
Is this *the* stored-fact prover — the one that answers by matching the store, and whose answers therefore each name a sentex with a context? `vaelii.impl.vantage` asks it of every applicable prover to decide whether a literal is inside post-hoc placement's domain. A goal only this one answers is a goal every answer to which can be placed, because every answer came from somewhere; a goal any *other* prover also answers has answers computed rather than stored — a closure walk, an evaluable, an inferred argument type — and those name no context to place by.
The measure-comparison predicates QuantityProver answers — check-only over two
ground measures, never stored (declared in the upper CxMeasure, computed here).
The measure-comparison predicates `QuantityProver` answers — check-only over two ground measures, never stored (declared in the upper CxMeasure, 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.
A magnitude is a finite number: ##Inf and ##NaN read as not-a-measure, the
same answer assert gives them (:not-well-formed), so the magnitude arithmetic
never sees one.
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. A magnitude is a **finite** number: `##Inf` and `##NaN` read as not-a-measure, the same answer `assert` gives them (`:not-well-formed`), so the magnitude arithmetic never sees one.
(normalize-quantity kb measure context)normalize-quantity-with-support's [dimension lo-base hi-base] alone, for a caller
with no use for the declarations behind it.
`normalize-quantity-with-support`'s `[dimension lo-base hi-base]` alone, for a caller with no use for the declarations behind it.
(normalize-quantity-with-support kb measure context)Resolve a ground measure to [[dimension lo-base hi-base] handles] — its dimension and
its magnitude bounds converted direct-to-base (one multiply, no chaining), together
with the declarations the conversion was read from. 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-read, 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.
The handles are empty when the unit declares neither, and that is not a gap: the two
fallbacks are what the absence of a declaration means, and an absence is not a sentex
a retraction can take away. A declaration arriving later does change the answer, and it
is SupportingProver's support-sources that puts it in front of the rules concerned
rather than a handle here.
Resolve a ground measure to `[[dimension lo-base hi-base] handles]` — its dimension and its magnitude bounds converted **direct-to-base** (one multiply, no chaining), together with the declarations the conversion was read from. 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-read`, 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. The handles are **empty** when the unit declares neither, and that is not a gap: the two fallbacks are what the *absence* of a declaration means, and an absence is not a sentex a retraction can take away. A declaration arriving later does change the answer, and it is `SupportingProver`'s `support-sources` that puts it in front of the rules concerned rather than a handle here.
(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-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.
The grid is *quantity-tolerance*'s own (tolerance-scale), so rebinding the
tolerance moves the rounding with the comparisons rather than leaving the two on
different policies.
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. The grid is `*quantity-tolerance*`'s own (`tolerance-scale`), so rebinding the tolerance moves the rounding with the comparisons rather than leaving the two on different policies.
(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).
Four channels, each found by differencing: run the complete prover alone, run every other applicable prover, and see what only the second answers.
:preserving — an (transitiveInArg 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.:calendar — an argument that is a calendar term: (YearFn 2000),
(MonthFn 2000 1), a DatetimeFn string, an InstantFn moment. Such a term carries
its own ordering in its fields, and a term that appears in no stored fact appears in
no closure and in no constraint network either — so a calculus reading the store
entails nothing about the pair while correctly claiming to subsume every prover that
reads what it reads. The structure is the source it does not read
(vaelii.impl.calendar). A pure test on the goal's own arguments, and the cheapest
of the four: no index read, and no read at all for a goal naming no such term.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;arg 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 three of the four: inherit/positions is behind a
root-intersection gate on any declaration naming this predicate,
tax/inverses-under is one map read on a KB declaring no inverses, and
datetime/time-term? reads the goal's own arguments.
concluding-rule-handles is the one that is not — it probes the consequent index once
per member of pred's spec closure, so this is O(specs) index reads per goal however
few rules conclude anything, and cond-> evaluates every test rather than stopping at
the first channel found. Its own docstring carries the number.
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).
Four channels, each found by differencing: run the complete prover alone, run every
other applicable prover, and see what only the second answers.
* **`:preserving`** — an `(transitiveInArg 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`.
* **`:calendar`** — an argument that is a **calendar term**: `(YearFn 2000)`,
`(MonthFn 2000 1)`, a `DatetimeFn` string, an `InstantFn` moment. Such a term carries
its own ordering *in its fields*, and a term that appears in no stored fact appears in
no closure and in no constraint network either — so a calculus reading the store
entails nothing about the pair while correctly claiming to subsume every prover that
reads what it reads. The structure is the source it does not read
(`vaelii.impl.calendar`). A pure test on the goal's own arguments, and the cheapest
of the four: no index read, and no read at all for a goal naming no such term.
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;
* `arg` 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 three of the four: `inherit/positions` is behind a
root-intersection gate on any declaration naming this predicate,
`tax/inverses-under` is one map read on a KB declaring no inverses, and
`datetime/time-term?` reads the goal's own arguments.
`concluding-rule-handles` is the one that is not — it probes the consequent index once
per member of `pred`'s spec closure, so this is O(specs) index reads per goal however
few rules conclude anything, and `cond->` evaluates every test rather than stopping at
the first channel found. Its own docstring carries the number.(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, forall, 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. So is each claimant's estimate: sort-by re-evaluates its
keyfn on every comparison, and an estimate is a real count over the taxonomy
rather than a constant, so it is taken once per prover and carried. The sort is
stable and the estimate is a function of the goal and the KB, so a tie still breaks
on registry order and not on when the comparison happened.
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`, `forall`, 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. So is each claimant's estimate: `sort-by` re-evaluates its keyfn on **every comparison**, and an estimate is a real count over the taxonomy rather than a constant, so it is taken once per prover and carried. The sort is stable and the estimate is a function of the goal and the KB, so a tie still breaks on registry order and not on when the comparison happened.
(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.
(solve-goal-with-support kb goal context)solve-goal's support-carrying twin: each solution as [bindings support], where
support is the handles of the stored sentexes the answer was read from
(SupportingProver), empty for a prover that reads nothing stored.
Forward chaining is the caller. A backward chainer discharges an antecedent and forgets it; a forward firing stores a conclusion, and what it stored has to be withdrawable — so the join needs the handles the answer rested on, and needs them beside the bindings they came with rather than by asking a second time (a second read is a second moment, and the two could disagree).
Same dispatch as solve-goal, so the two agree about which prover answers: the sole
complete prover when there is one, else the applicable provers cheapest-first, lazily,
deduped. Deduped on the pair, so one binding reached by two provers with different
support survives as both — two routes to one conclusion are two justifications, which is
what the TMS already reads them as.
`solve-goal`'s support-carrying twin: each solution as `[bindings support]`, where `support` is the handles of the stored sentexes the answer was read from (`SupportingProver`), empty for a prover that reads nothing stored. Forward chaining is the caller. A backward chainer discharges an antecedent and forgets it; a forward firing *stores* a conclusion, and what it stored has to be withdrawable — so the join needs the handles the answer rested on, and needs them beside the bindings they came with rather than by asking a second time (a second read is a second moment, and the two could disagree). Same dispatch as `solve-goal`, so the two agree about which prover answers: the sole complete prover when there is one, else the applicable provers cheapest-first, lazily, deduped. Deduped on the **pair**, so one binding reached by two provers with different support survives as both — two routes to one conclusion are two justifications, which is what the TMS already reads them as.
(source-contexts kb preds)Every context worth answering a support-carrying goal at, given preds — the contexts
holding one of those facts, and the contexts where two or more of them meet
(tax/meet-closure).
A caller passes the whole registry's sources (support-source-preds) rather than one
prover's, which over-approximates in the harmless direction: a context that holds only
some other prover's source reads nothing here and answers nothing, and the one read is
shared across every computed antecedent of a run.
qcn-kb/reader-contexts written for a prover that is not a calculus, and the same
argument holds it: a reading is what a reader sees, and a reader sees the whole
genlCx cone above it — so a context inheriting two contexts closes a metric network
neither closes alone, and that entailment exists for no other reader. Answering the
goal at a wildcard context instead would read every context's facts into one reading,
which is not any reader's, and would license a firing on facts no context sees together.
The contexts are read from the store rather than from belief, which over-approximates in the safe direction: a context whose only such fact is defeated is enumerated, reads nothing, and answers nothing.
Resident on the KB's :qcn atom, stamped with the change clock, since collecting
them is a record fetch per stored fact of every predicate named.
Every context worth answering a support-carrying goal at, given `preds` — the contexts holding one of those facts, and the contexts where two or more of them meet (`tax/meet-closure`). A caller passes the whole registry's sources (`support-source-preds`) rather than one prover's, which over-approximates in the harmless direction: a context that holds only some *other* prover's source reads nothing here and answers nothing, and the one read is shared across every computed antecedent of a run. `qcn-kb/reader-contexts` written for a prover that is not a calculus, and the same argument holds it: a reading is what a **reader** sees, and a reader sees the whole `genlCx` cone above it — so a context inheriting two contexts closes a metric network neither closes alone, and that entailment exists for no other reader. Answering the goal at a *wildcard* context instead would read every context's facts into one reading, which is not any reader's, and would license a firing on facts no context sees together. The contexts are read from the store rather than from belief, which over-approximates in the safe direction: a context whose only such fact is defeated is enumerated, reads nothing, and answers nothing. **Resident** on the KB's `:qcn` atom, stamped with the change clock, since collecting them is a record fetch per stored fact of every predicate named.
(support-answered-preds kb)The functors a registered SupportingProver answers — the antecedents forward chaining
discharges through solve-goal-with-support so the firing carries what the answer rested
on.
The functors a registered `SupportingProver` answers — the antecedents forward chaining discharges through `solve-goal-with-support` so the firing carries what the answer rested on.
(support-source-preds kb)The functors a registered SupportingProver reads. A datum on one of these moves an
answer no antecedent of the rule names, so it re-joins the rules carrying a
support-answered-preds antecedent (chain/fire-rules-for) rather than triggering them
— which is what makes such a firing independent of whether the table or the facts
arrived first.
The functors a registered `SupportingProver` *reads*. A datum on one of these moves an answer no antecedent of the rule names, so it re-joins the rules carrying a `support-answered-preds` antecedent (`chain/fire-rules-for`) rather than triggering them — which is what makes such a firing independent of whether the table or the facts arrived first.
A prover whose answer is a function of stored facts rather than of the goal's own arguments alone, and which can say which facts — the unit table a measure comparison normalizes through, the constraints a metric bound is closed out of, the lengths a duration sums.
A separate protocol rather than a sixth Prover method, because implementing it is a
choice: EvaluableProver computes (lessThan 3 5) from the numbers in front of it and
has no support to report, while QuantityProver reads a conversionFactor row before
it can compare two masses. Only the second is here.
Forward chaining is what needs it. A rule antecedent discharged by a prover
contributes no matched fact, so a firing that rested on one lists the rule and whatever
the other antecedents matched — and a conversionFactor row behind the answer is
supported by nothing the JTMS can reach. Retracting it then leaves the conclusion
believed. solve-with-support closes that: each answer carries the handles it was read
from, the join adds them to the firing's antecedents, and the ordinary relabel withdraws
the conclusion when any of them goes. It is the same contract
qcn-kb/solve-with-support and inherit/solve-with-support already meet for a
qualitative and an inherited antecedent.
support-functors the functors this prover answers with support, as a set
support-sources the functors it reads to answer them, as a set
solve-with-support the solutions of Prover/solve, each as [bindings support]
support-sources is what keeps the firing order-independent. A rule whose antecedent
this prover answers is triggered by the facts its other antecedents match, and a
conversionFactor row is not one of them — so a unit table stated after the rule and
the facts would never reach a join, and the same three sentences would derive a
conclusion or not depending on which arrived last. Naming the sources puts such a datum
in front of the rules carrying a support-functors antecedent, re-joined in full
(chain/rejoin-in-full), exactly as a (symmetric P) declaration is.
Two obligations on an implementer, and both are what makes the seam sound:
solve-with-support answers exactly what solve answers. The bindings are the
same solutions in the same order; only the support rides alongside. A prover whose
two methods disagreed would make a rule fire differently forward and backward.An answer with empty support is one nothing stored licensed — the diagonal of a
metric network, an arithmetic identity — and the forward join drops it rather than
building a justification that names the rule alone while looking as though it named the
facts (qcn-kb/solve-with-support gives the qualitative version of the same case).
A prover whose answer is a function of **stored facts** rather than of the goal's own arguments alone, and which can say which facts — the unit table a measure comparison normalizes through, the constraints a metric bound is closed out of, the lengths a duration sums. A separate protocol rather than a sixth `Prover` method, because implementing it is a choice: `EvaluableProver` computes `(lessThan 3 5)` from the numbers in front of it and has no support to report, while `QuantityProver` reads a `conversionFactor` row before it can compare two masses. Only the second is here. **Forward chaining is what needs it.** A rule antecedent discharged by a prover contributes no matched fact, so a firing that rested on one lists the rule and whatever the *other* antecedents matched — and a `conversionFactor` row behind the answer is supported by nothing the JTMS can reach. Retracting it then leaves the conclusion believed. `solve-with-support` closes that: each answer carries the handles it was read from, the join adds them to the firing's antecedents, and the ordinary relabel withdraws the conclusion when any of them goes. It is the same contract `qcn-kb/solve-with-support` and `inherit/solve-with-support` already meet for a qualitative and an inherited antecedent. support-functors the functors this prover answers with support, as a set support-sources the functors it *reads* to answer them, as a set solve-with-support the solutions of `Prover/solve`, each as `[bindings support]` `support-sources` is what keeps the firing order-independent. A rule whose antecedent this prover answers is triggered by the facts its *other* antecedents match, and a `conversionFactor` row is not one of them — so a unit table stated after the rule and the facts would never reach a join, and the same three sentences would derive a conclusion or not depending on which arrived last. Naming the sources puts such a datum in front of the rules carrying a `support-functors` antecedent, re-joined in full (`chain/rejoin-in-full`), exactly as a `(symmetric P)` declaration is. Two obligations on an implementer, and both are what makes the seam sound: * **`solve-with-support` answers exactly what `solve` answers.** The bindings are the same solutions in the same order; only the support rides alongside. A prover whose two methods disagreed would make a rule fire differently forward and backward. * **The support is enough to have produced the answer on its own.** It may over-approximate — a reading taken over a set of declarations names all of them — but it may never omit a fact the answer moved with, since that is the fact whose retraction would leave a stale conclusion standing. An answer with **empty** support is one nothing stored licensed — the diagonal of a metric network, an arithmetic identity — and the forward join drops it rather than building a justification that names the rule alone while looking as though it named the facts (`qcn-kb/solve-with-support` gives the qualitative version of the same case).
(solve-with-support prover kb goal context)(support-functors prover)(support-sources prover)The relations the cached-closure TransitivityProver answers — genl / genlCx, held
out of the generic per-predicate transitive machinery. Defined once in the taxonomy.
The relations the cached-closure `TransitivityProver` answers — genl / genlCx, held out of the generic per-predicate transitive machinery. Defined once in the taxonomy.
(transitive-prover? pr)Does this prover compute a transitive closure — genl/genlCx through the cached
taxonomy, or a predicate declared (transitive P)?
Does this prover compute a transitive closure — genl/genlCx through the cached taxonomy, or a predicate declared `(transitive P)`?
The two predicates a measure is normalized through — what normalize-quantity reads,
and therefore what a conclusion drawn from a measure comparison rests on besides the
facts that bound the measures.
The two predicates a measure is normalized through — what `normalize-quantity` reads, and therefore what a conclusion drawn from a measure comparison rests on besides the facts that bound the measures.
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 |