Belief settling: relabel the TMS, resolve soft contradictions on the one axis
(defeat-class), report the represented dilemmas, and run the exceptWhen
re-check queue to a joint fixpoint with belief.
Top engine layer (kb <- checks <- special <- integrate <- chain <- settle <- vaelii.core): settling reads believed content (kb), garbage-collects what a newly blocked justification was supporting (integrate's removal choke point tears it down), and re-derives what a released exception was suppressing (chain fires it again).
Belief settling: relabel the TMS, resolve soft contradictions on the one axis (defeat-class), report the represented dilemmas, and run the `exceptWhen` re-check queue to a joint fixpoint with belief. Top engine layer (kb <- checks <- special <- integrate <- chain <- settle <- vaelii.core): settling reads believed content (kb), garbage-collects what a newly blocked justification was supporting (integrate's removal choke point tears it down), and re-derives what a released exception was suppressing (chain fires it again).
How many candidate instances one settle's exposure pass will enumerate for the
extent-sweeping routes — a separating declaration, a metatype membership, a genl
edge, and a genlContext edge each implicate every instance below their types (or
in their cone), and on a large corpus that is the extent, not the region. A
sweep cut short files a single :exposure-truncated entry naming its trigger, so
the cap is never silent. The membership route is exact and unbudgeted — it is
O(1) per moved membership, and it is the route ordinary writes take.
How many candidate instances one settle's exposure pass will enumerate for the extent-sweeping routes — a separating declaration, a metatype membership, a genl edge, and a genlContext edge each implicate every instance below their types (or in their cone), and on a large corpus that is the extent, not the region. A sweep cut short files a single `:exposure-truncated` entry naming its trigger, so the cap is never silent. The membership route is exact and unbudgeted — it is O(1) per moved membership, and it is the route ordinary writes take.
Discover definitional clashes incrementally — the default, and what a KB runs.
Incremental discovery is three narrowings of one exhaustive question, which pairs of
believed sentexes clash: only the settle's moved region and the pairs already known
are examined (clash-candidates), only a sentex that could pair at all is checked
(could-clash?), and a known pair neither of whose members moved is carried forward
rather than re-derived (clash-nogoods). Each is a claim that what it skips could
not have changed the answer — and a wrong one is a silently different answer, never
a crash: a dilemma that goes unreported, or a defeat that is not applied.
Bound to false, every believed sentex is a candidate on every settle and nothing is
carried, which is the definition the three narrowings approximate. That is the
reference clash_oracle_test proves them against, and it is O(believed) checks per
settle — a measurement harness, not a mode to run a KB in.
Discover definitional clashes **incrementally** — the default, and what a KB runs. Incremental discovery is three narrowings of one exhaustive question, *which pairs of believed sentexes clash*: only the settle's moved region and the pairs already known are examined (`clash-candidates`), only a sentex that could pair at all is checked (`could-clash?`), and a known pair neither of whose members moved is carried forward rather than re-derived (`clash-nogoods`). Each is a claim that what it skips could not have changed the answer — and a wrong one is a silently *different* answer, never a crash: a dilemma that goes unreported, or a defeat that is not applied. Bound to `false`, every believed sentex is a candidate on every settle and nothing is carried, which is the definition the three narrowings approximate. That is the reference `clash_oracle_test` proves them against, and it is O(believed) checks per settle — a measurement harness, not a mode to run a KB in.
Memoize the P/¬P pairing per opposed body — the default, and what a KB runs.
Incremental pairing is one narrowing of an exhaustive question, which believed
negations pair with which believed positives: only the opposed bodies this settle
could have moved are re-derived (moved-bodies), and every other body's answer is
carried forward from the last settle verbatim. It is a claim that what it skips could
not have changed the answer — and a wrong one is a silently different answer, never a
crash: a dilemma that goes unreported, or a defeat that is not applied.
Bound to false, every opposed body is re-derived on every call and nothing is carried,
which is the definition the narrowing approximates. That is the reference
negation_oracle_test proves it against, and it is O(standing contradictions) belief
queries per settle round — a measurement harness, not a mode to run a KB in. The
separation is 12x on lein perf's negation-arbitration.
Memoize the P/¬P pairing **per opposed body** — the default, and what a KB runs. Incremental pairing is one narrowing of an exhaustive question, *which believed negations pair with which believed positives*: only the opposed bodies this settle could have moved are re-derived (`moved-bodies`), and every other body's answer is carried forward from the last settle verbatim. It is a claim that what it skips could not have changed the answer — and a wrong one is a silently *different* answer, never a crash: a dilemma that goes unreported, or a defeat that is not applied. Bound to `false`, every opposed body is re-derived on every call and nothing is carried, which is the definition the narrowing approximates. That is the reference `negation_oracle_test` proves it against, and it is O(standing contradictions) belief queries per settle *round* — a measurement harness, not a mode to run a KB in. The separation is 12x on `lein perf`'s `negation-arbitration`.
Is this settle restoring a KB rather than reacting to a change to one?
Bound by core/recover, and it turns the exposure pass off. That pass reports the
disjointness clashes the settle's moved region newly makes jointly visible — two
memberships each admissible where written, contradictory from a context below both —
and on a rebuild the claim is vacuous: nothing is newly visible, the whole KB is
arriving at once because it was already there. Left on, the region is every stored
sentex and a bounded incremental check becomes an unbounded full audit: 27% of an
OpenCyc import, silently, because the membership route is exact and unbudgeted (one
probe per membership) and a rebuild's region holds every membership there is.
Which is not to say the audit is worthless — it is the same question asked of the
whole KB rather than of a change to it. But it is a choice, and paying it inside
every recover and reindex is not one anybody made.
Is this settle **restoring** a KB rather than reacting to a change to one? Bound by `core/recover`, and it turns the exposure pass off. That pass reports the disjointness clashes the settle's moved region *newly* makes jointly visible — two memberships each admissible where written, contradictory from a context below both — and on a rebuild the claim is vacuous: nothing is newly visible, the whole KB is arriving at once because it was already there. Left on, the region is every stored sentex and a bounded incremental check becomes an unbounded full audit: 27% of an OpenCyc import, silently, because the membership route is exact and unbudgeted (one probe per membership) and a rebuild's region holds every membership there is. Which is not to say the audit is worthless — it is the same question asked of the whole KB rather than of a change to it. But it is a *choice*, and paying it inside every `recover` and `reindex` is not one anybody made.
Does a settle delete what a newly-blocked justification was solely supporting?
True everywhere except inside core/preview, which has to hand the KB back exactly
as it found it: the sweep is the one settle effect a rollback cannot undo at the same
handles, since putting a deleted conclusion back means deriving it again and a
re-derivation lands on a fresh handle. Suppressing it costs nothing semantically —
a swept datum is already OUT and ungroundable, so leaving it stored moves no label
and it still matches nothing. The rollback runs with the sweep back on, which is
what collects a conclusion the preview's own removals brought into being.
Does a settle **delete** what a newly-blocked justification was solely supporting? True everywhere except inside `core/preview`, which has to hand the KB back exactly as it found it: the sweep is the one settle effect a rollback cannot undo at the same handles, since putting a deleted conclusion back means deriving it again and a re-derivation lands on a fresh handle. Suppressing it costs nothing semantically — a swept datum is already OUT and ungroundable, so leaving it stored moves no label and it still matches nothing. The rollback runs with the sweep back **on**, which is what collects a conclusion the preview's own removals brought into being.
The companion of *touched-sink*: which of those datums were believed before
(jtms/touched-in). A caller binding both learns which way each one moved, which the
region alone cannot say — most of a relabelled region does not move at all.
core/edit's consequence report binds both. preview binds only the region, because
its rollback lets it read belief-before off the restored KB instead.
The companion of `*touched-sink*`: which of those datums were **believed before** (`jtms/touched-in`). A caller binding both learns which way each one moved, which the region alone cannot say — most of a relabelled region does not move at all. `core/edit`'s consequence report binds both. `preview` binds only the region, because its rollback lets it read belief-before off the restored KB instead.
An atom holding a set, or nil. When bound, every settle folds the datums whose
region it relabelled into it before clearing them — the affected region of whatever
the caller just did, which would otherwise be discarded at the end of each settle.
core/preview binds it and diffs belief over that set alone.
An atom holding a set, or nil. When bound, every settle folds the datums whose region it relabelled into it before clearing them — the affected region of whatever the caller just did, which would otherwise be discarded at the end of each settle. `core/preview` binds it and diffs belief over that set alone.
(exposed-clashes kb)Every jointly-visible disjointness clash the KB currently holds — the whole-KB question, asked on demand and returning its answer rather than filing it.
The settle pass beside this one answers a different question: what did the change
just made newly expose. That is what makes it incremental and what makes it
vacuous on a rebuild (*rebuilding?*), and it leaves nobody able to ask the standing
question — of an imported KB, whose ledger arrives empty, least of all. So it is
asked here instead, and by a caller who chose to.
Complete by construction, and cheaper than the incremental pass would be at this size. A term is a candidate iff it holds two believed memberships, so every candidate is found by walking the memberships themselves — no extent sweeps, hence no instance budget and no truncation to report. The sweeps exist only to work out which instances a changed declaration or edge implicates; when every membership is already in hand they can only re-find what is already there. Cost is the believed memberships, plus a pair test per term holding several, over probes memoized for the whole call.
Returns the same entry shape violations reports ({:violation :disjoint :detail {...}}), so a caller renders both with one renderer. Reads only: nothing is stored,
nothing is filed, and belief does not move.
Every jointly-visible disjointness clash the KB **currently** holds — the whole-KB
question, asked on demand and returning its answer rather than filing it.
The settle pass beside this one answers a different question: what did the change
just made *newly* expose. That is what makes it incremental and what makes it
vacuous on a rebuild (`*rebuilding?*`), and it leaves nobody able to ask the standing
question — of an imported KB, whose ledger arrives empty, least of all. So it is
asked here instead, and by a caller who chose to.
**Complete by construction, and cheaper than the incremental pass would be at this
size.** A term is a candidate iff it holds two believed memberships, so every
candidate is found by walking the memberships themselves — no extent sweeps, hence
no instance budget and no truncation to report. The sweeps exist only to work out
which *instances* a changed declaration or edge implicates; when every membership is
already in hand they can only re-find what is already there. Cost is the believed
memberships, plus a pair test per term holding several, over probes memoized for the
whole call.
Returns the same entry shape `violations` reports (`{:violation :disjoint :detail
{...}}`), so a caller renders both with one renderer. Reads only: nothing is stored,
nothing is filed, and belief does not move.(rechain-exception-rules kb rule-handles)Re-derive what a released exception was suppressing.
Revival under exceptWhen costs a re-derivation, not a flipped bit: the
conclusion was deleted, so there is nothing to relabel back into belief and the rule
has to fire again. Re-firing a rule whose conclusion still stands is a no-op
(has-justification? dedups it), and re-firing one whose exception still holds is a
no-op too (derive-conclusion checks before placing).
Cheap per rule, but not cheap per call: seeding chain with a rule handle joins
that rule over the whole fact extent, so re-chaining a rule that released nothing
costs one firing — and one level-6 exception query — per fact it has ever matched.
Handing it every rule the pass touched is therefore quadratic in a rule's firing
count all on its own, which is why the caller passes the released rules rather than
the queued ones.
chain, not chain-all: the violations ledger is scoped to the caller's run and
must not be cleared from inside settling.
Re-derive what a released exception was suppressing. Revival under `exceptWhen` costs a **re-derivation**, not a flipped bit: the conclusion was deleted, so there is nothing to relabel back into belief and the rule has to fire again. Re-firing a rule whose conclusion still stands is a no-op (`has-justification?` dedups it), and re-firing one whose exception still holds is a no-op too (`derive-conclusion` checks before placing). Cheap per rule, but **not** cheap per call: seeding `chain` with a rule handle joins that rule over the whole fact extent, so re-chaining a rule that released nothing costs one firing — and one level-6 exception query — per fact it has ever matched. Handing it every rule the pass touched is therefore quadratic in a rule's firing count all on its own, which is why the caller passes the *released* rules rather than the queued ones. `chain`, not `chain-all`: the violations ledger is scoped to the caller's run and must not be cleared from inside settling.
(rechain-seeds kb seeds)Re-derive from seeds — datum handles a teardown put back on the agenda. The one
caller is special/resubsumption-seeds: a firing names one witness for the genl
path it subsumed through, so removing that witness sweeps the conclusion even when
the reachability survives, and the facts under the edge have to be re-joined to get
it back. Filtered to what is still stored and believed, since the sweep that
produced them may also have collected some.
chain, not chain-all, for the same reason rechain-exception-rules uses it: the
violations ledger is scoped to the caller's run and must not be cleared from inside
settling.
Re-derive from `seeds` — datum handles a teardown put back on the agenda. The one caller is `special/resubsumption-seeds`: a firing names *one* witness for the `genl` path it subsumed through, so removing that witness sweeps the conclusion even when the reachability survives, and the facts under the edge have to be re-joined to get it back. Filtered to what is still stored and believed, since the sweep that produced them may also have collected some. `chain`, not `chain-all`, for the same reason `rechain-exception-rules` uses it: the violations ledger is scoped to the caller's run and must not be cleared from inside settling.
(settle kb)Settle belief (settle*), then hand the region it moved to whoever is listening.
Returns the unsatisfiable clashes, as settle* does. Delivery is here rather than
inside settle-finish because a listener may write, and a write inside a relabel
would relabel mid-relabel: by the time this runs the fixpoint is reached, the caches
are reconciled, the readings are recorded and the touched set is cleared, so a
listener's assert starts a fresh settle like any other caller's. A KB nobody is
listening to pays one deref (feed/deliver!).
Settle belief (`settle*`), then hand the region it moved to whoever is listening. Returns the unsatisfiable clashes, as `settle*` does. Delivery is here rather than inside `settle-finish` because a listener may **write**, and a write inside a relabel would relabel mid-relabel: by the time this runs the fixpoint is reached, the caches are reconciled, the readings are recorded and the touched set is cleared, so a listener's `assert` starts a fresh settle like any other caller's. A KB nobody is listening to pays one deref (`feed/deliver!`).
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 |