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), minCommonGenl and
maxCommonSpec (complete, read off the same closures), 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.
One alternative to avoid — 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.
Nothing here is declared per predicate, and the registry is deliberately unreachable
from vaelii.impl.predicates — which holds what is said about each term of the
engine's grammar, and holds nothing about who answers a goal. It is the completeness
argument above, one level down: a claim about a predicate is not a claim any single
component is competent to make. Three reasons, and they are why binding provers to
predicates in the declaration is the wrong shape rather than the missing half.
applicable? reads a goal's shape, not a predicate's name. EvaluableProver
reads the arguments in front of it; QuantityProver reads a unit table first;
ArgTypeProver answers a goal on any predicate carrying a declared argument type.
None of the three is "predicate P is answered by prover X", so none of them has an
entry to write.add-prover is public API, and it registers a prover with no declaration entry
at all. Nine ship in-tree opt-in — space, interval, stp, duration, sign,
orientation, relative, calendar, distance, each documenting its own
registration — and third-party ones are the point of the extension. A framework
requiring an entry either breaks those or grows an escape hatch that makes the entry
advisory, and an advisory entry is a hand-kept list again: the thing predicates exists to
stop being.sole-prover already answers the coordination question a per-predicate binding
would be reaching for, and answers it better. A prover declares a constant about its
own sources, and the engine asks once per goal whether anything shadows it. That is
a question about the KB, which moves when the KB does, rather than about the
vocabulary, which does not.What the declaration carries is narrower, and is a fact about the declaration rather
than about any prover: the :answers facet, meaning this term's arrival moves what a
level-6 query says about some predicate — which is what obliges it to post an exception
re-check, by its own arms or through special/declaration-subjects
(predicates/check-facets). That is the line the four functor lists in this file sit
on either side of, and it is the same line each time: a prover's shape table stays
with the prover, and its enrolment is the declaration's.
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), `minCommonGenl` and `maxCommonSpec` (complete, read off the same closures), `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. One alternative to avoid — *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. ## Why a prover is not a predicate's property Nothing here is declared per predicate, and the registry is deliberately unreachable from `vaelii.impl.predicates` — which holds what is *said* about each term of the engine's grammar, and holds nothing about who answers a goal. It is the completeness argument above, one level down: a claim about *a predicate* is not a claim any single component is competent to make. Three reasons, and they are why binding provers to predicates in the declaration is the wrong shape rather than the missing half. * **`applicable?` reads a goal's shape, not a predicate's name.** `EvaluableProver` reads the arguments in front of it; `QuantityProver` reads a unit table first; `ArgTypeProver` answers a goal on any predicate carrying a declared argument type. None of the three is "predicate P is answered by prover X", so none of them has an entry to write. * **`add-prover` is public API**, and it registers a prover with no declaration entry at all. Nine ship in-tree opt-in — `space`, `interval`, `stp`, `duration`, `sign`, `orientation`, `relative`, `calendar`, `distance`, each documenting its own registration — and third-party ones are the point of the extension. A framework requiring an entry either breaks those or grows an escape hatch that makes the entry advisory, and an advisory entry is a hand-kept list again: the thing `predicates` exists to stop being. * **`sole-prover` already answers the coordination question** a per-predicate binding would be reaching for, and answers it better. A prover declares a constant about its own sources, and the engine asks once per goal whether anything shadows it. That is a question about the KB, which moves when the KB does, rather than about the vocabulary, which does not. What the *declaration* carries is narrower, and is a fact about the declaration rather than about any prover: the `:answers` facet, meaning this term's arrival moves what a level-6 query says about some predicate — which is what obliges it to post an exception re-check, by its own arms or through `special/declaration-subjects` (`predicates/check-facets`). That is the line the four functor lists in this file sit on either side of, and it is the same line each time: a prover's **shape** table stays with the prover, and its **enrolment** is the declaration's.
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`).
nil, or a collector (unenumerated-collector) that TransitivePredicateProver adds a
predicate to when it does not enumerate the closure for a goal asked with both arguments
open. A read that reports the set binds it around each eager stretch of its search
(docs/anytime.md, "Where the collector lives").
nil, or a collector (`unenumerated-collector`) that `TransitivePredicateProver` adds a predicate to when it does not enumerate the closure for a goal asked with both arguments open. A read that reports the set binds it around each eager stretch of its search (docs/anytime.md, "Where the collector lives").
(admits-position? variable? declared n)Does positive position n exist in a well-formed application of a relation with this arity
shape? true when it does, false when it does not, nil when the KB has not said.
admitsArgnum, checks/arg-position-problem and quality's position census all read it, so
they cannot answer one position two ways. variable? is whether the relation reads a chain
of any length; declared is its exact declared arity or nil. A variable-arity relation
admits every positive position, a fixed-arity one one through its declared arity, and a
relation with neither leaves the question open.
Does positive position `n` exist in a well-formed application of a relation with this arity shape? `true` when it does, `false` when it does not, `nil` when the KB has not said. `admitsArgnum`, `checks/arg-position-problem` and `quality`'s position census all read it, so they cannot answer one position two ways. `variable?` is whether the relation reads a chain of any length; `declared` is its exact declared arity or nil. A variable-arity relation admits every positive position, a fixed-arity one one through its declared arity, and a relation with neither leaves the question open.
(aggregate-value kb goal op values context)The value an aggregate reduces to over values, or nil when there is none: over an
empty extent :count and :sum give 0 and the others nil, and a value list that is
neither all numbers nor measures of one dimension files an :aggregate violation and
gives nil.
The value an aggregate reduces to over `values`, or nil when there is none: over an empty extent `:count` and `:sum` give 0 and the others nil, and a value list that is neither all numbers nor measures of one dimension files an `:aggregate` violation and gives nil.
(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. A literal holding sx/no-match at a term
position (res/names-no-match?) names no term there, so only the stored-fact prover
reads it, and it matches nothing (docs/nat.md, Read path).
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. A literal holding `sx/no-match` at a term position (`res/names-no-match?`) names no term there, so only the stored-fact prover reads it, and it matches nothing (docs/nat.md, Read path).
(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 effect the
qualitative bound asks for. 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 effect the qualitative bound asks for. 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 also holds forward-only and inert rules). A
rule concluding a subtype answers a supertype goal (res/concluding-rule-handles), and
subsuming-unify binds the goal variable to the subtype instance. Each carries its
exceptWhen guard (parse-rule).
A rule is not a candidate when the asking context cannot see it (res/rule-visible-from?),
when the KB no longer believes it (res/rule-believed?), or when a believed visibility
except hides it from the asking context (exc/hidden-fn, built once per goal and nil when
nothing is hidden).
The result is in content order, [sentence context] under nm/compare-form, since the index
answers in handle order and prove-within's :max-results and the node engine's frontier
truncate on this list (docs/nmtms.md). The sentence is the key, so nothing is memoized;
:context joins it because one sentence stated in two contexts is two rules.
Rules concluding the goal's predicate or a spec of it, restricted to the backward-capable ones (the consequent index also holds forward-only and inert rules). A rule concluding a subtype answers a supertype goal (`res/concluding-rule-handles`), and `subsuming-unify` binds the goal variable to the subtype instance. Each carries its `exceptWhen` guard (`parse-rule`). A rule is not a candidate when the asking context cannot see it (`res/rule-visible-from?`), when the KB no longer believes it (`res/rule-believed?`), or when a believed visibility `except` hides it from the asking context (`exc/hidden-fn`, built once per goal and nil when nothing is hidden). The result is in content order, `[sentence context]` under `nm/compare-form`, since the index answers in handle order and `prove-within`'s `:max-results` and the node engine's frontier truncate on this list (docs/nmtms.md). The sentence is the key, so nothing is memoized; `:context` joins it because one sentence stated in two contexts is two rules.
(check-reasoner-name! nm)nm, or a refusal naming the reasoners there are. :unknown-option: naming a
reasoner that does not exist is a bad argument from a caller, never something a
sentence can be checked into.
`nm`, or a refusal naming the reasoners there are. `:unknown-option`: naming a reasoner that does not exist is a bad argument from a caller, never something a sentence can be checked into.
(closed-extent-for-arg? kb sentence context)Is the believed extent of sentence's predicate declared complete for this
sentence as read from context — is a (closedExtentForArg P n v) visible up its
genlCx ancestor set whose position n in sentence is ground and equal to v?
The taxonomy prop :closed-extent-arg is the presence check; the position and value
are read from the believed grants visible from context.
Is the believed extent of `sentence`'s predicate declared **complete for this sentence** as read from `context` — is a `(closedExtentForArg P n v)` visible up its `genlCx` ancestor set whose position `n` in `sentence` is ground and equal to `v`? The taxonomy prop `:closed-extent-arg` is the presence check; the position and value are read from the believed grants visible from `context`.
(closed-extent-for? kb sentence context)Is sentence's believed extent declared complete from context — by a
closed_extent_predicate grant on its predicate, or by a closedExtentForArg grant
whose position and value the sentence matches?
Is `sentence`'s believed extent declared complete from `context` — by a `closed_extent_predicate` grant on its predicate, or by a `closedExtentForArg` grant whose position and value the sentence matches?
(closed-extent-rules kb pred)The handles of the stored rules a closed-extent grant on pred makes read a
(not (pred …)) as negation as failure, deduplicated: each with a closed
(not (pred …)) antecedent (one [:not pred] antecedent-index lookup), and each
watched under not that re-checks a (not (pred …)) in an unknown antecedent, an
aggregate body or an exceptWhen query (negated-recheck-bodies). Read as stored,
whether a grant on pred stands or not.
The handles of the stored rules a closed-extent grant on `pred` makes read a `(not (pred …))` as negation as failure, deduplicated: each with a closed `(not (pred …))` antecedent (one `[:not pred]` antecedent-index lookup), and each watched under `not` that re-checks a `(not (pred …))` in an `unknown` antecedent, an aggregate body or an `exceptWhen` query (`negated-recheck-bodies`). Read as stored, whether a grant on `pred` stands or not.
(closed-extent-supports kb l)The handles each of which alone answers the ground (not (P …)) literal l at level 6
where it is visible, in any context and in the reading in force: each grant a
ClosedExtentProver answer rests on, (closed_extent_predicate P) or a
(closedExtentForArg P n v) whose argument n of (P …) is v, and each stored l.
Nil when no grant covers l, and nil when a prover other than ClosedExtentProver
and FactProver answers l in some context, since that answer names no handle.
The handles each of which alone answers the ground `(not (P …))` literal `l` at level 6 where it is visible, in any context and in the reading in force: each grant a `ClosedExtentProver` answer rests on, `(closed_extent_predicate P)` or a `(closedExtentForArg P n v)` whose argument `n` of `(P …)` is `v`, and each stored `l`. Nil when no grant covers `l`, and nil when a prover other than `ClosedExtentProver` and `FactProver` answers `l` in some context, since that answer names no handle.
(closed-extent? kb pred context)Is pred's believed extent declared complete as read from context — is
(closed_extent_predicate pred) visible up its genlCx ancestor set? See
docs/naf.md, "A closed extent".
Is `pred`'s believed extent declared **complete** as read from `context` — is `(closed_extent_predicate pred)` visible up its `genlCx` ancestor set? See docs/naf.md, "A closed extent".
(collecting-seq a f)The seq (f) returns, with *unenumerated* bound to collector a around the call and
around each pull, for a lazy read: a binding around the call alone has ended before a
pull runs the arm.
The seq `(f)` returns, with `*unenumerated*` bound to collector `a` around the call and around each pull, for a lazy read: a binding around the call alone has ended before a pull runs the arm.
The predicates CommonGenlProver answers, each to the taxonomy read that computes it.
The predicates `CommonGenlProver` answers, each to the taxonomy read that computes it.
(condition-normalizer kb context)A ground-goal -> ground-goal rewriting a block condition's substituted conjunct to the
normal form context answers under (every symbol to the representative that context
elects, then the schematic equations it can see), or nil when the KB holds no merge and no
equation. vaelii.impl.levels/engine-goal and kb/rewrite-goal prepare a level-6 read and
a query the same way.
Both the bindings a firing substituted in and the conjunct's own constants may name a
spelling a later merge retired, and an unrewritten goal then reads as not excepted and
not derivable. The rewrite is scoped to context: a merge it cannot see must not rename
the condition. One visibility predicate serves the whole conjunction. A goal
res/goal-held-as-spelled? exempts (different, a positive equation) is exempt here as in
kb/rewrite-goal.
A `ground-goal -> ground-goal` rewriting a block condition's substituted conjunct to the normal form `context` answers under (every symbol to the representative that context elects, then the schematic equations it can see), or nil when the KB holds no merge and no equation. `vaelii.impl.levels/engine-goal` and `kb/rewrite-goal` prepare a level-6 read and a query the same way. Both the bindings a firing substituted in and the conjunct's own constants may name a spelling a later merge retired, and an unrewritten goal then reads as *not excepted* and *not derivable*. The rewrite is scoped to `context`: a merge it cannot see must not rename the condition. One visibility predicate serves the whole conjunction. A goal `res/goal-held-as-spelled?` exempts (`different`, a positive equation) is exempt here as in `kb/rewrite-goal`.
(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.
Does the conjunctive level-6 body `conjuncts` have a solution under `bindings` in `context`? An empty conjunction has none.
(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 one joined evaluator unknown, thereExists, exceptWhen and an
aggregate's census read. Each conjunct, in planned-conjuncts order, is substituted
with what the conjuncts before it bound, put in norm's normal form when norm is
non-nil, and run through the registry. A closed negative conjunct over a predicate a
closed extent is declared on (rules/closed-extent-antecedents) runs after the
conjuncts that bind it, since ClosedExtentProver answers it only ground. Lazy throughout, so a caller taking one
solution enumerates no extent (docs/naf.md, "The conjunction is joined").
Lazy solutions of the conjunctive level-6 body `conjuncts`, extending `bindings`, in `context`: the one joined evaluator `unknown`, `thereExists`, `exceptWhen` and an aggregate's census read. Each conjunct, in `planned-conjuncts` order, is substituted with what the conjuncts before it bound, put in `norm`'s normal form when `norm` is non-nil, and run through the registry. A closed negative conjunct over a predicate a closed extent is declared on (`rules/closed-extent-antecedents`) runs after the conjuncts that bind it, since `ClosedExtentProver` answers it only ground. Lazy throughout, so a caller taking one solution enumerates no extent (docs/naf.md, "The conjunction is joined").
(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: is the answer something you look up, compute, or search for? Qualitative, not milliseconds.
:lookup: a bounded single-step retrieval (an O(1) ground test, a cached closure or
metadata read, or one index hit).:compute: a fixpoint over stored facts before the first answer (a closure).:search: recursive backward chaining.cost-rank gives the ordinal. The union path orders applicable provers by it, and
budget's :max-cost uses it as a ceiling. No registry member expands a rule, so :search
is unoccupied and :max-cost :compute and :search select the same provers; add-prover
can supply a searching one. Rule expansion is bounded by core/query's :max-depth.
First-answer cost tiers, cheapest first: is the answer something you look up, compute, or search for? Qualitative, not milliseconds. - `:lookup`: a bounded single-step retrieval (an O(1) ground test, a cached closure or metadata read, or one index hit). - `:compute`: a fixpoint over stored facts before the first answer (a closure). - `:search`: recursive backward chaining. `cost-rank` gives the ordinal. The union path orders applicable provers by it, and `budget`'s `:max-cost` uses it as a ceiling. No registry member expands a rule, so `:search` is unoccupied and `:max-cost :compute` and `:search` select the same provers; `add-prover` can supply a searching one. Rule expansion is bounded by `core/query`'s `:max-depth`.
The est-bindings an evaluatable reports while its inputs are unbound, and any prover
whose answer to an open argument is not complete. An evaluatable computes from ground
inputs and enumerates nothing, so on unbound inputs it can neither answer nor prune — the
most unselective a literal can be, and reported as such so the join planner
(vaelii.impl.plan, through est-goal) runs a generator that binds those inputs first
and the computation lands with everything ground. It is plan/unbounded, which the
unranked order also reads: a literal an :est-override costs at it waits for its
binders with the ranking off.
The `est-bindings` an evaluatable reports while its inputs are unbound, and any prover whose answer to an open argument is not complete. An evaluatable computes from ground inputs and enumerates nothing, so on unbound inputs it can neither answer nor prune — the most *unselective* a literal can be, and reported as such so the join planner (`vaelii.impl.plan`, through `est-goal`) runs a generator that binds those inputs first and the computation lands with everything ground. It is `plan/unbounded`, which the unranked order also reads: a literal an `:est-override` costs at it waits for its binders with the ranking off.
(definition-inconsistencies kb candidate-terms context max-results)Query-only definitional inconsistencies over the finite ground candidate-terms.
Returns one witness per [collection term] for which the definition provers can answer both
(collection term) and (not (collection term)): some own-or-spec sufficient condition
passes, the collection's own necessary condition fails, and no strict-genl necessary
fast-fails the positive query. Each witness carries every passing sufficient and failing
necessary declaration involved. The collections are those induced by defnSufficient
declarations and their genl ancestors. vaelii.impl.integrity/kb-integrity supplies
candidate-terms. Reads only.
Query-only definitional inconsistencies over the finite ground `candidate-terms`. Returns one witness per `[collection term]` for which the definition provers can answer both `(collection term)` and `(not (collection term))`: some own-or-spec sufficient condition passes, the collection's own necessary condition fails, and no strict-genl necessary fast-fails the positive query. Each witness carries every passing sufficient and failing necessary declaration involved. The collections are those induced by `defnSufficient` declarations and their `genl` ancestors. `vaelii.impl.integrity/kb-integrity` supplies `candidate-terms`. Reads only.
(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, mirroring solve-goal-with, which runs it
alone. With none, the engine unions partial provers over the index, whose model
vaelii.impl.plan uses instead (ArgTypeProver's constant 3 would replace a measurement).
The one partial estimate is deferred-est, from an applicable SupportingProver that
computes the goal from an open argument, (argN ?t 1 ?f) before ?f is bound, so the goal
waits for its binders.
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, mirroring `solve-goal-with`, which runs it alone. With none, the engine unions partial provers over the index, whose model `vaelii.impl.plan` uses instead (`ArgTypeProver`'s constant 3 would replace a measurement). The one partial estimate is `deferred-est`, from an applicable `SupportingProver` that computes the goal from an open argument, `(argN ?t 1 ?f)` before `?f` is bound, so the goal waits for its binders.
Predicates a prover computes from its ground arguments rather than looks up.
lessThan / greaterThan: variable-arity arithmetic comparisons, (lessThan 1 2 3)
states 1 < 2 < 3. greaterThan is folded to lessThan when stored (vaelii.impl.sentex)
and answered directly when asked.integer: the unary EDN-kind check, which lets the sign-refined integer collections in
core.txt resolve by evaluation (docs/defns.md).string, number, boolean, keyword, character: value kinds, answered only for a
literal argument (literal-value-kind). A symbol or compound is left to the other
provers.matchesPattern: (matchesPattern ?string ?pattern) holds when the whole of the string
matches the regular expression, both ground; false for a non-string subject. It runs
through bounded-matches?, so a backtracking pattern is a :pattern-too-costly refusal.The set is what EvaluableProver reads its arguments as, not a claim about what answers a
predicate; the :answers facet of each is checked against it by predicates_test.
Predicates a prover computes from its ground arguments rather than looks up. - `lessThan` / `greaterThan`: variable-arity arithmetic comparisons, `(lessThan 1 2 3)` states 1 < 2 < 3. `greaterThan` is folded to `lessThan` when stored (`vaelii.impl.sentex`) and answered directly when asked. - `integer`: the unary EDN-kind check, which lets the sign-refined integer collections in core.txt resolve by evaluation (docs/defns.md). - `string`, `number`, `boolean`, `keyword`, `character`: value kinds, answered only for a literal argument (`literal-value-kind`). A symbol or compound is left to the other provers. - `matchesPattern`: `(matchesPattern ?string ?pattern)` holds when the whole of the string matches the regular expression, both ground; false for a non-string subject. It runs through `bounded-matches?`, so a backtracking pattern is a `:pattern-too-costly` refusal. The set is what `EvaluableProver` reads its arguments as, not a claim about what answers a predicate; the `:answers` facet of each is checked against it by `predicates_test`.
(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. It answers by computing, in one
of two shapes:
:result): (pred a …) holds when f applied to the ground arguments
returns truthy. Every argument must be ground.:result names an output slot): (pred … ?out …) binds ?out to
(f <the other, ground arguments>). A ground output slot is checked against the value.opts (a map, or nil):
:result: :first, :last, or a 0-based index; its presence selects result-binding.:arity: the fn's input count (an int or a set), derived by reflection when omitted; a
variadic fn needs it stated.:cost: a cost-tiers keyword, :lookup by default.:completeness: 0..100, 100 by default (sole-prover still guards it). Use 50 for a
predicate a KB also stores facts under.Registered through add-prover, so it answers ask / query goals and discharges a
conjunct or antecedent in a query with a :max-depth. Forward materialization reaches
it through vaelii.impl.chain/deferred-antecedent?. The DFS prove does not, since its
leaf is the stored facts (docs/inference.md, query-engine section).
A `Prover` wrapping the plain Clojure fn `f` as the evaluatable predicate/function `pred`, the value `vaelii.core/add-evaluatable` registers. It answers by computing, in one of two shapes: - **check** (no `:result`): `(pred a …)` holds when `f` applied to the ground arguments returns truthy. Every argument must be ground. - **result-binding** (`:result` names an output slot): `(pred … ?out …)` binds `?out` to `(f <the other, ground arguments>)`. A ground output slot is checked against the value. `opts` (a map, or nil): - `:result`: `:first`, `:last`, or a 0-based index; its presence selects result-binding. - `:arity`: the fn's input count (an int or a set), derived by reflection when omitted; a variadic fn needs it stated. - `:cost`: a `cost-tiers` keyword, `:lookup` by default. - `:completeness`: 0..100, 100 by default (`sole-prover` still guards it). Use 50 for a predicate a KB also stores facts under. Registered through `add-prover`, so it answers `ask` / `query` goals and discharges a conjunct or antecedent in a `query` with a `:max-depth`. Forward materialization reaches it through `vaelii.impl.chain/deferred-antecedent?`. The DFS `prove` does not, since its leaf is the stored facts (docs/inference.md, query-engine section).
(evaluatable-est-override kb 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. A goal
costs what its EvaluatableFn's est-bindings gives under the plan's bindings
(est-under): deferred-est while an input is unbound, else one, so the binders run first.
Forward chaining (vaelii.impl.chain/planned-join) plans with this so a registered
evaluatable antecedent follows its binders, as the built-in deferred-predicates do by
canonical order. Scoped to evaluatables because forward chaining's leaf is the stored facts
(*matcher*). Nil when preds is empty.
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. A goal costs what its `EvaluatableFn`'s `est-bindings` gives under the plan's bindings (`est-under`): `deferred-est` while an input is unbound, else one, so the binders run first. Forward chaining (`vaelii.impl.chain/planned-join`) plans with this so a registered evaluatable antecedent follows its binders, as the built-in `deferred-predicates` do by canonical order. Scoped to evaluatables because forward chaining's leaf is the stored facts (`*matcher*`). Nil when `preds` is empty.
(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? The substituted conjuncts are put in context's
normal form (condition-normalizer) and joined by conjunction-solutions, stopping at
the first solution; nothing in the registry expands a rule. An unanswerable or empty
exception does not hold. See docs/exceptions.md, "The exception is a query, not a
literal".
Does `except` — a rule's `exceptWhen` query, a vector of literals — hold under `bindings`, evaluated in `context`? The substituted conjuncts are put in `context`'s normal form (`condition-normalizer`) and joined by `conjunction-solutions`, stopping at the first solution; nothing in the registry expands a rule. An unanswerable or empty exception does not hold. See docs/exceptions.md, "The exception is a query, not a literal".
(exception-visible-from? kb context entry)Does context see the exception entry (a rule-exception-entries element)?
An exceptWhen is a sentex, so a context reasons with the exceptions its genlCx
ancestor set holds and no others, exactly as it reasons with the rules
(res/rule-visible-from?). An exception stated in a context below the conclusion's
therefore blocks nothing in the conclusion's context. An open ?ctx or nil
context is the unscoped path and sees every exception.
Does `context` see the exception `entry` (a `rule-exception-entries` element)? An `exceptWhen` is a sentex, so a context reasons with the exceptions its `genlCx` ancestor set holds and no others, exactly as it reasons with the rules (`res/rule-visible-from?`). An exception stated in a context below the conclusion's therefore blocks nothing in the conclusion's context. An open `?ctx` or nil `context` is the unscoped path and sees every exception.
(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, over the
exceptions context sees. An ordinary rule (no exception) yields no conjunctions
and pays nothing past the watched-rule membership read.
Is a firing of rule `handle` blocked by any of its exceptWhen exceptions under `bindings`, evaluated in `context`? Block-if-**any**-conjunction-holds, over the exceptions `context` sees. An ordinary rule (no exception) yields no conjunctions and pays nothing past the watched-rule membership read.
The kinds ExpressionKindProver answers of a quoted form, as a set: the expression
lattice reflection.txt declares and the value kinds below it. Forward chaining
discharges an antecedent through the prover only when its functor is here
(support-answered-preds),
so a kind a KB adds below expression is answered by a query and not by a firing.
The kinds `ExpressionKindProver` answers of a quoted form, as a set: the expression lattice `reflection.txt` declares and the value kinds below it. Forward chaining discharges an antecedent through the prover only when its functor is here (`support-answered-preds`), so a kind a KB adds below `expression` is answered by a query and not by a firing.
(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?
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?
(firing-strength kb handle rsx watched? dropping-id)The class a firing of the rule rsx at handle confers on its conclusion, before its
antecedents cap it: :default for a set/defaultRule, and for a guarded rule, one
with an (unknown S) antecedent or an exceptWhen stored against it; :monotonic
otherwise. A guarded conclusion goes OUT when a blocker arrives, so it is never
:monotonic (docs/nmtms.md, "Strength propagates from the antecedents").
The exceptions are read as stored, belief unread, so the class is a function of the
stored content. watched? is reads/watched-rule?'s answer for handle, which the
chainer has already read for the rule fields (chain/rule-fields-of); dropping-id is an exception meta-sentex
on its way out, which the read leaves out.
The class a firing of the rule `rsx` at `handle` confers on its conclusion, before its antecedents cap it: `:default` for a `set/defaultRule`, and for a **guarded** rule, one with an `(unknown S)` antecedent or an `exceptWhen` stored against it; `:monotonic` otherwise. A guarded conclusion goes OUT when a blocker arrives, so it is never `:monotonic` (docs/nmtms.md, "Strength propagates from the antecedents"). The exceptions are read as stored, belief unread, so the class is a function of the stored content. `watched?` is `reads/watched-rule?`'s answer for `handle`, which the chainer has already read for the rule fields (`chain/rule-fields-of`); `dropping-id` is an exception meta-sentex on its way out, which the read leaves out.
(fn-prover spec)The Prover vaelii.core/prover builds from spec, a map of plain fns and constants;
the refusals and defaults are that fn's contract. A spec with :solve-with-support
builds a SupportingFnProver, whose solve is the bindings of :solve-with-support;
one with :solve builds a FnProver, which implements Prover alone. Each answer is
checked as it is realized.
The `Prover` `vaelii.core/prover` builds from `spec`, a map of plain fns and constants; the refusals and defaults are that fn's contract. A spec with `:solve-with-support` builds a `SupportingFnProver`, whose `solve` is the bindings of `:solve-with-support`; one with `:solve` builds a `FnProver`, which implements `Prover` alone. Each answer is checked as it is realized.
The heads whose application is a formula whatever its operands: the connectives, the rule and exception frames, and the quantifiers.
The heads whose application is a formula whatever its operands: the connectives, the rule and exception frames, and the quantifiers.
(held-contexts kb preds also)The contexts holding a stored fact on one of preds, either polarity, or one of the
sentexes the handles also name, as a set: each predicate's predicate-extent children,
with no record read, and one record fetch per handle of also.
Read from the store rather than from belief, which over-approximates in the safe direction: a context whose only such fact is defeated is listed, reads nothing, and answers nothing.
The contexts holding a stored fact on one of `preds`, either polarity, or one of the sentexes the handles `also` name, as a set: each predicate's predicate-extent children, with no record read, and one record fetch per handle of `also`. Read from the store rather than from belief, which over-approximates in the safe direction: a context whose only such fact is defeated is listed, reads nothing, and answers nothing.
(indeterminacy-supports kb term)The handles of the stored sentexes, in any context, that make term an indeterminate
term where they are visible: its SkolemFn minting expression and its memberships of
indeterminate_term or a subkind (indeterminate-term?'s two readings), sorted.
The handles of the stored sentexes, in any context, that make `term` an indeterminate term where they are visible: its `SkolemFn` minting expression and its memberships of `indeterminate_term` or a subkind (`indeterminate-term?`'s two readings), sorted.
(indeterminate-term? kb term context)Is term an unmerged indeterminate term in context: a skolem constant, read off
its SkolemFn minting expression, or a believed member of the indeterminate_term
category, subkinds included (docs/predall.md)? Public for vaelii.impl.predall's
predAllSpecified audit, which asks the same question of a filler.
Is `term` an unmerged **indeterminate term** in `context`: a skolem constant, read off its `SkolemFn` minting expression, or a believed member of the `indeterminate_term` category, subkinds included (docs/predall.md)? Public for `vaelii.impl.predall`'s `predAllSpecified` audit, which asks the same question of a filler.
(ingredient-contexts kb goal)The contexts holding a stored fact some answer of a computed prover to goal rests on:
prover-ingredient-contexts of every prover goal dispatches to at '?ctx other than the
stored-fact prover. A context outside the genlCx lattice sees only itself, so it
answers a computed goal only when it holds every ingredient; these are the contexts
vantage/readers adds for it.
The contexts holding a stored fact some answer of a computed prover to `goal` rests on: `prover-ingredient-contexts` of every prover `goal` dispatches to at `'?ctx` other than the stored-fact prover. A context outside the `genlCx` lattice sees only itself, so it answers a computed goal only when it holds every ingredient; these are the contexts `vantage/readers` adds for it.
(literal-value-kind x)The most specific value kind of x, or nil when x is no literal value.
The most specific value kind of `x`, or nil when `x` is no literal value.
The value kind of a literal value, most specific first: each kind with the EDN test a
value of it passes. A value denotes itself, so its kind is decidable from the value
alone. checks/value-kind classifies a value by the first test it passes, and
EvaluableProver answers a value-kind membership by the kind's own test, so integer
falls under number there by number?. A symbol is not a literal: a constant can
denote a value of any kind.
The value kind of a literal value, most specific first: each kind with the EDN test a value of it passes. A value denotes itself, so its kind is decidable from the value alone. `checks/value-kind` classifies a value by the first test it passes, and `EvaluableProver` answers a value-kind membership by the kind's own test, so `integer` falls under `number` there by `number?`. A symbol is not a literal: a constant can denote a value of any kind.
The measure-comparison predicates QuantityProver answers — check-only over two
ground measures, never stored (declared in measure.txt, computed here).
The measure-comparison predicates `QuantityProver` answers — check-only over two ground measures, never stored (declared in `measure.txt`, computed here).
(measure-with-support kb measure context)A ground measure as [[[dimension base-unit] lo-base hi-base] handles]:
normalize-quantity-with-support with its dimension paired with the unit its
magnitudes are in (base-unit-with-support), and the declarations of both reads. Two
measures compare only under one [dimension base-unit] key, so a unit with no
conversionFactor, its own base at factor 1, compares with itself and with no other
unit of its dimension.
A ground measure as `[[[dimension base-unit] lo-base hi-base] handles]`: `normalize-quantity-with-support` with its dimension paired with the unit its magnitudes are in (`base-unit-with-support`), and the declarations of both reads. Two measures compare only under one `[dimension base-unit]` key, so a unit with no `conversionFactor`, its own base at factor 1, compares with itself and with no other unit of its dimension.
(measure? x)Is x a ground measure term — (QuantityFn N Unit) or
(QuantityIntervalFn Lo Hi Unit), numeric magnitude(s) and a symbol unit? This is
the check-only condition: 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? This is the check-only condition: 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.
(measures-agree? kb a b context)Can the ground measures a and b denote one magnitude, read at context: both
measures, normalized under one [dimension base-unit] key (measure-with-support),
with bounds that meet within *quantity-tolerance*. Two points agree when they are
equal, a point and an interval when the interval holds the point, and two intervals
when they overlap. False for anything that is not a measure. The functional check
and the tuple placement read it, so a functional slot holding (QuantityFn 20 Kilogram) and (QuantityFn 20000 Gram) holds one value (docs/quantity.md).
Can the ground measures `a` and `b` denote one magnitude, read at `context`: both measures, normalized under one `[dimension base-unit]` key (`measure-with-support`), with bounds that meet within `*quantity-tolerance*`. Two points agree when they are equal, a point and an interval when the interval holds the point, and two intervals when they overlap. False for anything that is not a measure. The functional check and the tuple placement read it, so a functional slot holding `(QuantityFn 20 Kilogram)` and `(QuantityFn 20000 Gram)` holds one value (docs/quantity.md).
The argument constraints this prover answers along the genl closure, as a set —
meta-constraint-shape's keys.
Public because it is the second list that reads the :argument-constraint family
as a family, and predicates/check-facets holds it and checks/constraint- declaration-functors to enumerating exactly it. A spelling the entry point reads up
res/constraining-predicates and this table omits is one declaration meaning one thing
to assert and another to ask — which is what happened to quotedArg.
The argument constraints this prover answers along the `genl` closure, as a set — `meta-constraint-shape`'s keys. Public because it is the second list that reads the `:argument-constraint` family **as a family**, and `predicates/check-facets` holds it and `checks/constraint- declaration-functors` to enumerating exactly it. A spelling the entry point reads up `res/constraining-predicates` and this table omits is one declaration meaning one thing to `assert` and another to `ask` — which is what happened to `quotedArg`.
(negated-recheck-bodies kb rh)The symbol-headed bodies of the negated literals rule rh re-checks: in its unknown
antecedents, its aggregate bodies and the queries of its believed exceptWhen
meta-sentexes.
The symbol-headed bodies of the negated literals rule `rh` re-checks: in its `unknown` antecedents, its aggregate bodies and the queries of its believed exceptWhen meta-sentexes.
(nonempty-contexts kb preds g)The contexts a forward join asks the ground (nonempty C) g at, or nil for any other
goal: source-contexts over preds with the subtypes of C added, so every context
holding a member reads the answer, and the contexts stating a genl edge into one of
those subtypes are parties to the meet. The subtypes are read over every context, and
each context asks the answer from its own vantage.
The contexts a forward join asks the ground `(nonempty C)` `g` at, or nil for any other goal: `source-contexts` over `preds` with the subtypes of `C` added, so every context holding a member reads the answer, and the contexts stating a `genl` edge into one of those subtypes are parties to the meet. The subtypes are read over every context, and each context asks the answer from its own vantage.
(nonempty-source? kb s)Can s arriving, leaving or moving in belief move what a registered NonemptyProver
answers? True of a membership (T x) of a ground term in a constant type, of a
sentence installing a genl edge (tax/installed-edges) and of a genlCx edge. A
shape test and a scan of the registered supporters; no index read.
Can `s` arriving, leaving or moving in belief move what a registered `NonemptyProver` answers? True of a membership `(T x)` of a ground term in a constant type, of a sentence installing a `genl` edge (`tax/installed-edges`) and of a `genlCx` edge. A shape test and a scan of the registered supporters; no index read.
(nonempty-witness kb c context)The handles a believed member of the type c seen from context rests on, as a set,
or nil when c has none: the first in content order of the believed memberships (S x)
that res/matches-visible answers for (c ?x), S being c or a subtype, and for a
subtype the first believed supporter of each genl edge on one path from S up to c
(tax/genl-path-edges). A member whose path has an edge with no believed supporter
seen from context is passed over. Reads one count per subtype of c first
(reads/stored-count-with-functor), and the visible extent of c in full when one is
positive.
The handles a believed member of the type `c` seen from `context` rests on, as a set, or nil when `c` has none: the first in content order of the believed memberships `(S x)` that `res/matches-visible` answers for `(c ?x)`, `S` being `c` or a subtype, and for a subtype the first believed supporter of each `genl` edge on one path from `S` up to `c` (`tax/genl-path-edges`). A member whose path has an edge with no believed supporter seen from `context` is passed over. Reads one count per subtype of `c` first (`reads/stored-count-with-functor`), and the visible extent of `c` in full when one is positive.
(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), with the declarations
the conversion was read from. A point (QuantityFn N U) has lo-base = hi-base.
(dimensionOf U ?d), or U itself when the unit declares none, so two
measures in the same unit always compare and two distinct undeclared units do not.N × (conversionFactor U ?base ?factor), the factor defaulting to 1.
Every unit of one dimension must convert to a single base unit.Both reads go through table-read, so a unit declared twice and differently falls back to
being its own dimension and base. The handles are empty when the unit declares neither,
since an absence is not a sentex a retraction can take away; SupportingProver's
support-sources covers a declaration arriving later.
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), with the declarations the conversion was read from. A point `(QuantityFn N U)` has `lo-base = hi-base`. - Dimension is `(dimensionOf U ?d)`, or `U` itself when the unit declares none, so two measures in the same unit always compare and two distinct undeclared units do not. - Base magnitude is `N × (conversionFactor U ?base ?factor)`, the factor defaulting to `1`. Every unit of one dimension must convert to a single base unit. Both reads go through `table-read`, so a unit declared twice and differently falls back to being its own dimension and base. The handles are empty when the unit declares neither, since an absence is not a sentex a retraction can take away; `SupportingProver`'s `support-sources` covers a declaration arriving later.
(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`).
(placeable-prover? pr)Does every answer pr gives name the stored sentexes it rests on, one answer per
derivation, and rest on no absence? The stored-fact prover's answers each name a
match; ArgTypeProver's carry their usage and declaration (solve-with-support). Both
give one answer per genl route a subsumption crosses (subsumption-routes).
vaelii.impl.vantage asks it of every applicable prover to decide whether a literal is
inside post-hoc placement's domain. A walk over stored hops is outside it, since its
support names one chain where several chains may derive the pair. An answer resting on
an absence is outside it too: the unscoped pass sees facts a reader does not, so it can
lose an answer the reader gives.
Does every answer `pr` gives name the stored sentexes it rests on, one answer per derivation, and rest on no absence? The stored-fact prover's answers each name a match; `ArgTypeProver`'s carry their usage and declaration (`solve-with-support`). Both give one answer per `genl` route a subsumption crosses (`subsumption-routes`). `vaelii.impl.vantage` asks it of every applicable prover to decide whether a literal is inside post-hoc placement's domain. A walk over stored hops is outside it, since its support names one chain where several chains may derive the pair. An answer resting on an absence is outside it too: the unscoped pass sees facts a reader does not, so it can lose an answer the reader gives.
(plan kb goal context)The applicable provers for a goal, their estimates, and which of them actually run.
When one prover may answer the goal alone, every other applicable prover is shadowed:
reported, never invoked. Each entry carries :runs?, and a shadowed one carries
:shadowed-by naming the prover that displaced it. A prover that claims completeness 100
but does not run alone, because a source none of the applicable provers reads bears on the
goal, carries :guarded-by naming the channels (shadowing-channels). 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 which of them actually run. When one prover may answer the goal alone, every other applicable prover is shadowed: reported, never invoked. Each entry carries `:runs?`, and a shadowed one carries `:shadowed-by` naming the prover that displaced it. A prover that claims `completeness` 100 but does not run alone, because a source none of the applicable provers reads bears on the goal, carries `:guarded-by` naming the channels (`shadowing-channels`). Entries are in the order the engine would consult them: a single complete prover, else cheapest `cost` tier first.
(q= a b)Are two base magnitudes equal within *quantity-tolerance*? Normalization multiplies
by a stored (usually floating-point) conversion factor, so exact = would make one sum
unequal to itself written in another unit. The measure comparisons here and
duration's bound checks call it.
Are two base magnitudes equal within `*quantity-tolerance*`? Normalization multiplies by a stored (usually floating-point) conversion factor, so exact `=` would make one sum unequal to itself written in another unit. The measure comparisons here and `duration`'s bound checks call it.
(quoted-anywhere? kb)Does a stored sentex hold a quoting function's application (sx/quoting-functors)?
One term-index read per quoting function, belief unread (reads/as-stored-with-term).
Does a stored sentex hold a quoting function's application (`sx/quoting-functors`)? One term-index read per quoting function, belief unread (`reads/as-stored-with-term`).
(quoted-head? kb r)Does a stored sentex hold a quoted application (F (r …)) whose head is r, F a
quoting function? One term-index intersection per quoting function names the
candidates (reads/as-stored-with-terms), and each candidate's record is read for the
form; belief is unread.
Does a stored sentex hold a quoted application `(F (r …))` whose head is `r`, `F` a quoting function? One term-index intersection per quoting function names the candidates (`reads/as-stored-with-terms`), and each candidate's record is read for the form; belief is unread.
(reasoner nm)The prover the reasoner named nm registers, or check-reasoner-name!'s refusal.
The prover the reasoner named `nm` registers, or `check-reasoner-name!`'s refusal.
(reasoner-names)The names of the optional reasoners, sorted.
The names of the optional reasoners, sorted.
The reasoners a KB can register by name, and the var holding each one's constructor.
vaelii.core/reasoner documents each one.
The reasoners a KB can register by name, and the var holding each one's constructor. `vaelii.core/reasoner` documents each one.
(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 model is wrong for that leaf: a genl conjunct costs the cached
closure's size and not the stored edges the trie counts. A chainer whose leaf is the stored
facts passes nothing.
Memoized on the goal (est-goal reads only the goal; a query mutates nothing), or on the goal
and its bound variables for a goal at deferred-est (est-under). Without the memo
plan/order re-estimates every remaining literal on every pick, O(k²) registry sweeps for k
antecedents.
`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 model is wrong for that leaf: a `genl` conjunct costs the cached closure's size and not the stored edges the trie counts. A chainer whose leaf is the stored facts passes nothing. Memoized on the goal (`est-goal` reads only the goal; a query mutates nothing), or on the goal and its bound variables for a goal at `deferred-est` (`est-under`). Without the memo `plan/order` re-estimates every remaining literal on every pick, O(k²) registry sweeps for k antecedents.
(relation-moved-answers kb)The functors the registered ExpressionKindProver answers that what the KB states of a
relation can move: those at or above a kind stated-kinds gives, read globally because
the re-join reads every context. Nil when no ExpressionKindProver is registered.
The functors the registered `ExpressionKindProver` answers that what the KB states of a relation can move: those at or above a kind `stated-kinds` gives, read globally because the re-join reads every context. Nil when no `ExpressionKindProver` is registered.
(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. A computed answer never claims a precision it lacks — 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. A computed answer never claims a precision it lacks — 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-exception-entries kb handle)The believed exceptWhen exceptions of the rule at handle, each as
{:context c :handle h :query q}: q is one conjunction (a vector of literals) in the
rule's canonical variables, and c and h are its meta-sentex's context and handle.
The callers read it only for a rule in the watched-rule set.
The believed exceptWhen exceptions of the rule at `handle`, each as
`{:context c :handle h :query q}`: `q` is one conjunction (a vector of literals) in the
rule's canonical variables, and `c` and `h` are its meta-sentex's context and handle.
The callers read it only for a rule in the watched-rule set.(rule-exceptions kb handle)(rule-exceptions kb handle context)The conjunctions of rule-exception-entries, evaluated block-if-any-holds.
The two-argument arity reads every believed exception wherever it is stored, which
is the set a structural reader wants: the re-check index, the stratification graph
and the candidate narrowing all over-approximate safely. The three-argument arity
keeps only the exceptions context sees (exception-visible-from?), which is the
set a block decision in context reads.
The conjunctions of `rule-exception-entries`, evaluated block-if-**any**-holds. The two-argument arity reads every believed exception wherever it is stored, which is the set a structural reader wants: the re-check index, the stratification graph and the candidate narrowing all over-approximate safely. The three-argument arity keeps only the exceptions `context` sees (`exception-visible-from?`), which is the set a block decision in `context` reads.
(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.
(separation-est-override kb)An :est-override for vaelii.impl.plan/order that costs a disjoint literal by
DisjointnessProver's est-bindings, and returns nil for every other goal. Forward
chaining (vaelii.impl.chain/planned-join) answers the literal from the separations as
well as from the stored sentences, so its stored-row count is not its fan-out. A goal
with both ends open waits for a binder (chain/open-ends) and is answered from the
stored sentences alone, so it takes the index model's estimate, which costs no read of
the separation declarations.
An `:est-override` for `vaelii.impl.plan/order` that costs a `disjoint` literal by `DisjointnessProver`'s `est-bindings`, and returns nil for every other goal. Forward chaining (`vaelii.impl.chain/planned-join`) answers the literal from the separations as well as from the stored sentences, so its stored-row count is not its fan-out. A goal with both ends open waits for a binder (`chain/open-ends`) and is answered from the stored sentences alone, so it takes the index model's estimate, which costs no read of the separation declarations.
(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 (the completeness contract at the head of this file). Each channel is found by
differencing the complete prover against every other applicable prover.
:preserving: an (transitiveInArg P n R) declaration licenses a claim about a tuple in
no stored fact, rule conclusion or constraint network.:rules: a rule whose consequent unifies with the goal (concludes-goal?). A
set/backwardRule never fires forward and no registry member is one, so the claim must
be read in the scope that reaches the rule. Not narrowed to backward rules: a forward
rule is absorbed only if the fixpoint ran to it ({:chain? false}, :max-depth).:inverse: a declared (inverse P Q) for a goal about P, unless the calculus owning
P owns Q and its converse table implies the pair (unread-inverse?).:negates: a (not (Q …)) goal with Q at or below a side of a negates declaration
(NegatesProver).:calendar: an argument that is a calendar term ((YearFn 2000), DatetimeFn,
InstantFn), which carries its ordering in its fields (vaelii.impl.calendar). A pure
test on the goal's arguments.Absorbed, so not a channel: a stored fact, a merged term (rewritten into the goal first),
symmetric / transitive / reflexive over a calculus's own predicate, and arg type
inference and the metadata provers, which answer shapes no computed prover claims.
Cost: inherit/positions is behind a root-intersection presence check, tax/inverses-under
and tax/negates-over are one map read each, and datetime/time-term? reads the goal's
arguments. res/concludes? probes the consequent index per member of pred's spec closure
(O(specs) for a goal no rule concludes), and concludes-goal? then fetches concluding rules
until one unifies. cond-> evaluates every test.
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 (the completeness contract at the head of this file). Each channel is found by
differencing the complete prover against every other applicable prover.
- `:preserving`: an `(transitiveInArg P n R)` declaration licenses a claim about a tuple in
no stored fact, rule conclusion or constraint network.
- `:rules`: a rule whose consequent unifies with the goal (`concludes-goal?`). A
`set/backwardRule` never fires forward and no registry member is one, so the claim must
be read in the scope that reaches the rule. Not narrowed to backward rules: a forward
rule is absorbed only if the fixpoint ran to it (`{:chain? false}`, `:max-depth`).
- `:inverse`: a declared `(inverse P Q)` for a goal about `P`, unless the calculus owning
`P` owns `Q` and its converse table implies the pair (`unread-inverse?`).
- `:negates`: a `(not (Q …))` goal with `Q` at or below a side of a `negates` declaration
(`NegatesProver`).
- `:calendar`: an argument that is a calendar term (`(YearFn 2000)`, `DatetimeFn`,
`InstantFn`), which carries its ordering in its fields (`vaelii.impl.calendar`). A pure
test on the goal's arguments.
Absorbed, so not a channel: a stored fact, a merged term (rewritten into the goal first),
`symmetric` / `transitive` / `reflexive` over a calculus's own predicate, and `arg` type
inference and the metadata provers, which answer shapes no computed prover claims.
Cost: `inherit/positions` is behind a root-intersection presence check, `tax/inverses-under`
and `tax/negates-over` are one map read each, and `datetime/time-term?` reads the goal's
arguments. `res/concludes?` probes the consequent index per member of `pred`'s spec closure
(O(specs) for a goal no rule concludes), and `concludes-goal?` then fetches concluding rules
until one unifies. `cond->` evaluates every test.(shape-kinds x)The most specific expression kinds of the form x that its spelling decides, as a
set: variable, symbol, a value kind (literal-value-kind), or for a compound one
of open_formula / sentence under a formula-heads head, sentex_handle_term for
(sentexHandle N) with N a positive integer, non_atomic_expression beside
open_expression / closed_expression under any other symbol or variable head, and
ill_formed_expression beside the same under any other head. A variable inside a
nested (Quote …) or bound by a quantifier in x is not free (sx/unquoted-free-vars).
#{} for nil.
The most specific expression kinds of the form `x` that its spelling decides, as a
set: `variable`, `symbol`, a value kind (`literal-value-kind`), or for a compound one
of `open_formula` / `sentence` under a `formula-heads` head, `sentex_handle_term` for
`(sentexHandle N)` with N a positive integer, `non_atomic_expression` beside
`open_expression` / `closed_expression` under any other symbol or variable head, and
`ill_formed_expression` beside the same under any other head. A variable inside a
nested `(Quote …)` or bound by a quantifier in `x` is not free (`sx/unquoted-free-vars`).
`#{}` for nil.(sole-prover kb applicable goal context)The prover that may answer goal alone, or nil for the union path.
A prover claims completeness 100 for its goal shape, subsuming every prover whose sources
it reads. The engine then asks whether a source none of them reads exists
(shadowing-channels); if so, nobody runs alone. The guard lives here and not in each
prover, so a new channel is one edit and add-prover registrants are guarded. Guarding
only moves a goal from one prover to the union, which includes the claimant, so every
claimant is asked alike, including unstorable goal shapes (different, unknown,
thereExists, forall, aggregates).
The channels are read once per goal and only for a goal some prover claims. Each claimant's
estimate is taken once and carried, because sort-by re-evaluates its keyfn per comparison;
the sort is stable, so ties break on registry order. See docs/inference.md.
The prover that may answer `goal` **alone**, or nil for the union path. A prover claims `completeness` 100 for its goal shape, subsuming every prover whose sources it reads. The engine then asks whether a source none of them reads exists (`shadowing-channels`); if so, nobody runs alone. The guard lives here and not in each prover, so a new channel is one edit and `add-prover` registrants are guarded. Guarding only moves a goal from one prover to the union, which includes the claimant, so every claimant is asked alike, including unstorable goal shapes (`different`, `unknown`, `thereExists`, `forall`, aggregates). The channels are read once per goal and only for a goal some prover claims. Each claimant's estimate is taken once and carried, because `sort-by` re-evaluates its keyfn per comparison; the sort is stable, so ties break on registry order. See docs/inference.md.
(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-reporting-support kb goal context)solve-goal-with-support's answers as [bindings support reported?], reported? true
when a SupportingProver gave the answer. An empty support it reports means the answer
read nothing stored; an empty support from any other prover says nothing about what it
read, FactProver's among them.
`solve-goal-with-support`'s answers as `[bindings support reported?]`, `reported?` true when a `SupportingProver` gave the answer. An empty support it reports means the answer read nothing stored; an empty support from any other prover says nothing about what it read, `FactProver`'s among them.
(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, through
res/lazy-mapcat (mapcat would realize a chunk and call every applicable solve), so an
expensive prover is never invoked if the consumer stops early. The complete-prover branch
runs one prover. When several complete provers apply, the one with the fewest
est-bindings runs.
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, through `res/lazy-mapcat` (`mapcat` would realize a chunk and call every applicable `solve`), so an expensive prover is never invoked if the consumer stops early. The complete-prover branch runs one prover. When several complete provers apply, the one with the fewest `est-bindings` runs.
(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 any other prover (answers-with-support).
Forward chaining is the caller: a firing stores a conclusion that must be withdrawable, and
the handles must come with the bindings in one read. The dispatch is solve-goal's: the
sole complete prover, else the applicable provers cheapest-first, lazily. Deduped on the
pair, so one binding reached with different support survives as two justifications.
`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 any other prover (`answers-with-support`). Forward chaining is the caller: a firing stores a conclusion that must be withdrawable, and the handles must come with the bindings in one read. The dispatch is `solve-goal`'s: the sole complete prover, else the applicable provers cheapest-first, lazily. Deduped on the pair, so one binding reached with different support survives as two justifications.
(source-contexts kb preds)(source-contexts kb preds also)Every context worth answering a support-carrying goal at, given preds: the contexts
holding one of those facts (held-contexts), and the contexts where two or more of them meet
(tax/meet-closure). A caller passes the whole registry's sources (support-source-preds),
which over-approximates harmlessly and shares one read across a run.
A reading is what a reader sees through its genlCx ancestor set, so a context inheriting
two contexts closes a metric network neither closes alone (qcn-kb/reader-contexts). A
wildcard context would read every context into one reading that no reader has. Resident on
the KB's :qcn atom, keyed by the change clock. also names further handles whose contexts
are parties to the meet: declarations a reading needs beside its facts.
Every context worth answering a support-carrying goal at, given `preds`: the contexts holding one of those facts (`held-contexts`), and the contexts where two or more of them meet (`tax/meet-closure`). A caller passes the whole registry's sources (`support-source-preds`), which over-approximates harmlessly and shares one read across a run. A reading is what a reader sees through its `genlCx` ancestor set, so a context inheriting two contexts closes a metric network neither closes alone (`qcn-kb/reader-contexts`). A wildcard context would read every context into one reading that no reader has. Resident on the KB's `:qcn` atom, keyed by the change clock. `also` names further handles whose contexts are parties to the meet: declarations a reading needs beside its facts.
(stated-kind-handles kb g)The handles of the believed memberships (T r), at every context, of the symbol r
heading the compound the goal g quotes, when g is on an expression kind
(expression-kind-predicates); else nil. stated-kinds reads these beside the
prover's source functors, so a forward join asks g at their contexts too
(source-contexts's also).
The handles of the believed memberships `(T r)`, at every context, of the symbol `r` heading the compound the goal `g` quotes, when `g` is on an expression kind (`expression-kind-predicates`); else nil. `stated-kinds` reads these beside the prover's source functors, so a forward join asks `g` at their contexts too (`source-contexts`'s `also`).
(stated-kinds kb x context)The expression kinds of the compound x under a symbol head r that what the KB states
of r decides, as {kind handles}, each kind with the statements it rests on. When
r is a predicate and not a function (relation-kinds), x is a closed_predication,
or an open_predication when a variable is free in it. When r is a function and not
a predicate, a closed x is a non_atomic_term. When the argument count breaks r's
length (arity/broken-binding, read the same at every context), x is an
ill_formed_sentence for a predicate r and a closed x, an ill_formed and an
open_formula for a predicate r and an open x, and an ill_formed_expression
otherwise; the binding's grounds and route are among the handles. The map is empty for
any other x, and for an r the KB places under both kinds or neither.
The expression kinds of the compound `x` under a symbol head `r` that what the KB states
of `r` decides, as `{kind handles}`, each kind with the statements it rests on. When
`r` is a predicate and not a function (`relation-kinds`), `x` is a `closed_predication`,
or an `open_predication` when a variable is free in it. When `r` is a function and not
a predicate, a closed `x` is a `non_atomic_term`. When the argument count breaks `r`'s
length (`arity/broken-binding`, read the same at every context), `x` is an
`ill_formed_sentence` for a predicate `r` and a closed `x`, an `ill_formed` and an
`open_formula` for a predicate `r` and an open `x`, and an `ill_formed_expression`
otherwise; the binding's grounds and route are among the handles. The map is empty for
any other `x`, and for an `r` the KB places under both kinds or neither.(stored-exception-metas kb handle)The exceptWhen meta-sentexes stored naming the rule at handle, believed or not:
what rule-exception-entries reads before it filters by belief.
The exceptWhen meta-sentexes stored naming the rule at `handle`, believed or not: what `rule-exception-entries` reads before it filters by belief.
(subsumption-routes kb goal-functor stored-functor)Every route of [handle ctx] supporters that lets a fact spelled stored-functor
answer a literal on goal-functor, read globally: each genl route no other route
covers (tax/reach-supports), or the one signed route across genlInverse edges. A
route resting on an edge supporter a placed defeat or an except can hide somewhere
(exc/defeated-anywhere?, exc/closure-excepted-anywhere?) covers only the routes
resting on that supporter too, so a reader hiding it still reads a route it covered.
[[]], one route resting on nothing, when the functors are equal or no closure relates
them.
Every route of `[handle ctx]` supporters that lets a fact spelled `stored-functor` answer a literal on `goal-functor`, read globally: each `genl` route no other route covers (`tax/reach-supports`), or the one signed route across `genlInverse` edges. A route resting on an edge supporter a placed defeat or an except can hide somewhere (`exc/defeated-anywhere?`, `exc/closure-excepted-anywhere?`) covers only the routes resting on that supporter too, so a reader hiding it still reads a route it covered. `[[]]`, one route resting on nothing, when the functors are equal or no closure relates them.
(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-answers-reading kb src s)The functors answered by the registered SupportingProvers that read src, or nil
when none reads it: the answers the datum s, on src, can move. A supporter reads
a genl path up to the goal's predicate, so an edge s installs
(tax/installed-edges) moves only the answers at or above the edge's upper end,
read globally because the re-join reads every context. The test walks down from the
answers (tax/genls-global-among), so its cost does not grow with the depth of the
edge's upper end. A membership that can move a relation's kind
(relation-membership?) moves relation-moved-answers whatever its functor.
The functors answered by the registered `SupportingProver`s that read `src`, or nil when none reads it: the answers the datum `s`, on `src`, can move. A supporter reads a `genl` path up to the goal's predicate, so an edge `s` installs (`tax/installed-edges`) moves only the answers at or above the edge's upper end, read globally because the re-join reads every context. The test walks down from the answers (`tax/genls-global-among`), so its cost does not grow with the depth of the edge's upper end. A membership that can move a relation's kind (`relation-membership?`) moves `relation-moved-answers` whatever its functor.
(support-delta-source? kb src s)Does the datum s, on src, move a SupportingProver's answers only as a supporter
of them: is src a functor some registered supporter reads, not one a genl edge is
read off (tax/edge-installing-functors), and s not a membership moving a relation's
kind (relation-membership?)? Then an answer s makes newly given names s in its
support, by the protocol's second obligation (prover-types/SupportingProver), and
the re-join s owes keeps only the rows that rest on it (chain/run-owed-rejoin).
The caller asks it of a positive datum only: a negation defeats a row, and the answer
it widens rests on what remains.
Does the datum `s`, on `src`, move a `SupportingProver`'s answers only as a supporter of them: is `src` a functor some registered supporter reads, not one a `genl` edge is read off (`tax/edge-installing-functors`), and `s` not a membership moving a relation's kind (`relation-membership?`)? Then an answer `s` makes newly given names `s` in its support, by the protocol's second obligation (`prover-types/SupportingProver`), and the re-join `s` owes keeps only the rows that rest on it (`chain/run-owed-rejoin`). The caller asks it of a positive datum only: a negation defeats a row, and the answer it widens rests on what remains.
(support-est-override kb)An :est-override for vaelii.impl.plan/order that costs a literal a registered
SupportingProver answers by that prover's est-bindings, the largest where several
apply, and returns nil for every other goal so the index model ranks it.
Forward chaining (vaelii.impl.chain/planned-join) plans with this beside
evaluatable-est-override. The join answers such a literal by computation as well as
by matching, so its stored-row count is not its fan-out: includesInstant stores no rows
and reports deferred-est for an open argument, which places it after its binders.
An `:est-override` for `vaelii.impl.plan/order` that costs a literal a registered `SupportingProver` answers by that prover's `est-bindings`, the largest where several apply, and returns nil for every other goal so the index model ranks it. Forward chaining (`vaelii.impl.chain/planned-join`) plans with this beside `evaluatable-est-override`. The join answers such a literal by computation as well as by matching, so its stored-row count is not its fan-out: `includesInstant` stores no rows and reports `deferred-est` for an open argument, which places it after its binders.
(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.
(term-value-kind-goal? goal)Is goal a value-kind membership (k x), k one of value-kind-predicates, over a
ground x that is no literal value? EvaluableProver leaves it to the other provers,
since a constant or a function application can denote a value of any kind.
Is `goal` a value-kind membership `(k x)`, `k` one of `value-kind-predicates`, over a ground `x` that is no literal value? `EvaluableProver` leaves it to the other provers, since a constant or a function application can denote a value of any kind.
The relations the cached-closure TransitivityProver answers — genl / genlCx, held
out of the generic per-predicate transitive machinery. Defined once in the taxonomy.
Not enrolled in the declaration, because it already is: tax/closure-relations is the
entries whose :storage is [:edge …], and predicates_test asserts the two equal. An
alias where the prover reads it, over a second enumeration to keep in step.
The relations the cached-closure `TransitivityProver` answers — genl / genlCx, held out of the generic per-predicate transitive machinery. Defined once in the taxonomy. Not enrolled in the declaration, because it already is: `tax/closure-relations` is the entries whose `:storage` is `[:edge …]`, and `predicates_test` asserts the two equal. An alias where the prover reads it, over a second enumeration to keep in step.
(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)`?
(unenumerated-collector)A fresh collector for *unenumerated*: :all holds every predicate the arm recorded,
:guarded the subset recorded inside an unknown or exceptWhen evaluation.
A fresh collector for `*unenumerated*`: `:all` holds every predicate the arm recorded, `:guarded` the subset recorded inside an `unknown` or `exceptWhen` evaluation.
(unenumerated-report a)Collector a as {:unenumerated [P …] :unenumerated-in-guards [P …]}, each vector in
content order.
Collector `a` as `{:unenumerated [P …] :unenumerated-in-guards [P …]}`, each vector in
content order.The two predicates a measure is normalized through: what normalize-quantity reads, and
what a conclusion drawn from a measure comparison rests on besides the facts that bound the
measures. A prover's own source list, kept here and not as a :support-source field on the
declaration: neither predicate is grammar (both live in kb/upper/measure.txt), and
support-source-preds asks the registry live, so a prover added through add-prover
contributes its sources.
The two predicates a measure is normalized through: what `normalize-quantity` reads, and what a conclusion drawn from a measure comparison rests on besides the facts that bound the measures. A prover's own source list, kept here and not as a `:support-source` field on the declaration: neither predicate is grammar (both live in `kb/upper/measure.txt`), and `support-source-preds` asks the registry live, so a prover added through `add-prover` contributes its sources.
(value-definition kb v t context)(value-definition kb v t context frame-of)What the :monotonic definitions decide about the literal value v under the type t,
from context: :outside when a necessary condition of a strict supertype of t is
false on v, else :member when a sufficient condition of t or of a subtype of t
is true on v, else :outside when a necessary condition of t itself is false on
v, else nil. Only a condition condition-on-value evaluates decides, and nil for a
v that is no literal value. The order is the defn provers': a supertype's necessary
is checked first, and a sufficient admits against t's own necessary. The argument
checks read this (checks/value-outside?), and pass frame-of, a thunk answering
value-definition-frame of t and context, to share it across values.
What the `:monotonic` definitions decide about the literal value `v` under the type `t`, from `context`: `:outside` when a necessary condition of a strict supertype of `t` is false on `v`, else `:member` when a sufficient condition of `t` or of a subtype of `t` is true on `v`, else `:outside` when a necessary condition of `t` itself is false on `v`, else nil. Only a condition `condition-on-value` evaluates decides, and nil for a `v` that is no literal value. The order is the defn provers': a supertype's necessary is checked first, and a sufficient admits against `t`'s own necessary. The argument checks read this (`checks/value-outside?`), and pass `frame-of`, a thunk answering `value-definition-frame` of `t` and `context`, to share it across values.
(value-definition-frame kb t context)The half of value-definition no value enters, for the type t from context:
{:above :below :own}, the :monotonic necessary conditions of the strict supertypes
of t, the sufficient conditions of t and its subtypes, and t's own necessary
conditions, each in the order value-definition tries them. Nil when t is no symbol
or the store holds no definition.
The half of `value-definition` no value enters, for the type `t` from `context`:
`{:above :below :own}`, the `:monotonic` necessary conditions of the strict supertypes
of `t`, the sufficient conditions of `t` and its subtypes, and `t`'s own necessary
conditions, each in the order `value-definition` tries them. Nil when `t` is no symbol
or the store holds no definition.(value-definition-reaches? kb t context)Can a :monotonic definition decide a literal value under the type t, from context
(value-definition): does a visible :monotonic definition state a sufficient
condition of t or of a subtype, or a necessary condition of t or of a supertype?
Can a `:monotonic` definition decide a literal value under the type `t`, from `context` (`value-definition`): does a visible `:monotonic` definition state a sufficient condition of `t` or of a subtype, or a necessary condition of `t` or of a supertype?
The value kinds EvaluableProver answers for a literal argument, beside integer,
which it answers for any ground argument.
The value kinds `EvaluableProver` answers for a literal argument, beside `integer`, which it answers for any ground argument.
(with-unenumerated f)(f) with a fresh collector bound, as [result report], report being
unenumerated-report's. f must be eager, since the collector is a binding.
`(f)` with a fresh collector bound, as `[result report]`, `report` being `unenumerated-report`'s. `f` must be eager, since the collector is a binding.
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 |