A non-monotonic truth-maintenance system.
Each TMS node corresponds to a datum (a sentex handle) and records: its label (IN/OUT), whether it is a premise (and at what assumption strength), its derivation depth, the justifications that conclude it (:supports), and the justifications that use it as an antecedent (:consequences).
A node holds no reference to the sentex it labels — only its handle. The record store is where a sentex lives, so a copy here would be a second one to keep in step; and because this graph is always resident, a strong reference from it would hold every record in RAM, which on a paging backend defeats the paging entirely (measured: the nodes reached 50% of the record store). A caller that needs the sentence fetches it by handle.
Belief is a least fixpoint: a node is IN when it is a premise or has a valid justification (all antecedents IN) — EXCEPT that a node in the defeated set is forced OUT. Because labels are computed from the current justification set and the current defeated set rather than accumulated as events arrive, belief is order-independent: asserting a defeater later withdraws a previously-drawn conclusion, and removing the defeater revives it. That is the non-monotonic behaviour a plain monotone JTMS lacked.
Order independence. The same knowledge, given in any order, yields the same
beliefs. Every operation here recomputes labels from current state, so nothing
depends on arrival order. (The one place this can leak is a tie-break between
two equally-strong beliefs: keying it on handle id would smuggle assertion order
back in, so the contradiction layer keys it on content — see
vaelii.impl.solve/content-key.)
Locality. No operation recomputes the whole graph. A change can only affect nodes downstream of it, so every relabel is scoped to the affected region — the forward consequence closure of whatever changed — with the rest of the graph held fixed as the boundary. Cost is proportional to the region, not to the size of the KB, which is what lets belief maintenance scale.
These two pull against each other, and the reconciliation is the whole design:
a local fixpoint over the region, with boundary labels fixed, has a unique
solution, and it is the same one a global fixpoint would produce. See
relabel-region*.
strength — every premise carries a strength (:monotonic / :default); every
justification carries a strength too (:monotonic for a bare rule, :default for
a defeasible one), capping the class it confers. From these, relabel derives
each IN node's defeat-class (monotonic > default, see
vaelii.impl.strength). Strength propagates: a justification confers no more
than the weakest of its antecedents' classes, so a conclusion is never stronger
than what it rests on. That makes the class equation recursive, and
region-classes solves it as a least fixpoint inside the region relabel.
The class decides who loses a soft contradiction; the caller
(core) owns the contradiction layer and pushes the losers into the defeated set
with defeat.
defeated — a set of datums forced OUT by contradiction resolution. It is
derived (recomputed each settle by core), so clear-defeats! resets it and
revival is automatic.
superseded — a map datum -> reason of datums displaced by an equality
merge: the stale spelling of a fact whose terms have been rewritten to their
class representative (docs/equality.md). Three things make it its own state
rather than a reuse of defeated or blocked:
blocked names justifications, and a directly asserted (bornIn Dep Chicago) is a premise with no justification at all — region-fixpoint
seeds every premise IN unconditionally, so there is nothing for a block to
invalidate. Superseding has to act on the datum.defeated would be the wrong reason. A superseded spelling lost no
argument; it was restated, and why-not must be able to say so — hence the
map carries the displacing representative rather than being a bare set.:in for the purposes of valid?, because its rewritten twin is justified
by it: forcing it OUT structurally would invalidate the twin's own
justification and the merge would believe neither spelling. What
supersession removes is reported belief — in? and in-datums subtract
it — so the stale spelling stops matching, stops answering queries and stops
entering nogoods, while everything derived from it stands.Retention is the point: the spelling is the caller's premise, so unlike an
excepted conclusion it is never swept, and dropping the equality gives it back.
Like defeated and blocked the map is derived — core recomputes it each
settle from the equality closure — so belief stays order independent.
blocked — a set of justification ids whose rule's exception currently holds
(exceptWhen, see docs/exceptions.md). A blocked justification is not a
defeated conclusion: it is simply invalid, so it supports nothing, confers
no defeat-class, and does not make its consequence groundable — which is what
lets the ordinary dependency-directed sweep garbage-collect an excepted
conclusion instead of retaining it for revival. This module is pure and has no
KB, so it cannot run the exception query itself: the caller evaluates the
exception and hands the answer in with set-blocked, which relabels only the
region the change reaches. Like defeated, the set is derived — computed
from current state each settle, never accumulated — so belief stays order
independent.
Retraction is dependency-directed: drop the premise, relabel, then SWEEP the affected closure — datums that end up OUT with no valid support and are not defeated are solely supported by the retraction, so they (and their non-premise justifications) are returned for the caller to delete from the stores. A datum that is merely defeated keeps its support and is retained for later revival.
This module owns the in-memory graph; the caller owns physical deletion, since only it holds the stores.
A non-monotonic truth-maintenance system.
Each TMS *node* corresponds to a datum (a sentex handle) and records: its label
(IN/OUT), whether it is a premise (and at what assumption *strength*), its
derivation depth, the justifications that conclude it (:supports), and the
justifications that use it as an antecedent (:consequences).
A node holds **no reference to the sentex it labels** — only its handle. The record
store is where a sentex lives, so a copy here would be a second one to keep in step;
and because this graph is always resident, a strong reference from it would hold every
record in RAM, which on a paging backend defeats the paging entirely (measured: the
nodes reached 50% of the record store). A caller that needs the sentence fetches it
by handle.
Belief is a least fixpoint: a node is IN when it is a premise or has a valid
justification (all antecedents IN) — EXCEPT that a node in the *defeated* set is
forced OUT. Because labels are computed from the current justification set and
the current defeated set rather than accumulated as events arrive, belief is
order-independent: asserting a defeater later withdraws a previously-drawn
conclusion, and removing the defeater revives it. That is the non-monotonic
behaviour a plain monotone JTMS lacked.
## Two invariants
**Order independence.** The same knowledge, given in any order, yields the same
beliefs. Every operation here recomputes labels from current state, so nothing
depends on arrival order. (The one place this can leak is a *tie-break* between
two equally-strong beliefs: keying it on handle id would smuggle assertion order
back in, so the contradiction layer keys it on content — see
`vaelii.impl.solve/content-key`.)
**Locality.** No operation recomputes the whole graph. A change can only affect
nodes downstream of it, so every relabel is scoped to the *affected region* — the
forward consequence closure of whatever changed — with the rest of the graph held
fixed as the boundary. Cost is proportional to the region, not to the size of the
KB, which is what lets belief maintenance scale.
These two pull against each other, and the reconciliation is the whole design:
a local fixpoint over the region, with boundary labels fixed, has a *unique*
solution, and it is the same one a global fixpoint would produce. See
`relabel-region*`.
* strength — every premise carries a strength (:monotonic / :default); every
justification carries a *strength* too (:monotonic for a bare rule, :default for
a defeasible one), capping the class it confers. From these, `relabel` derives
each IN node's *defeat-class* (monotonic > default, see
vaelii.impl.strength). Strength **propagates**: a justification confers no more
than the weakest of its antecedents' classes, so a conclusion is never stronger
than what it rests on. That makes the class equation recursive, and
`region-classes` solves it as a least fixpoint inside the region relabel.
The class decides who loses a soft contradiction; the caller
(core) owns the contradiction layer and pushes the losers into the defeated set
with `defeat`.
* defeated — a set of datums forced OUT by contradiction resolution. It is
*derived* (recomputed each settle by core), so `clear-defeats!` resets it and
revival is automatic.
* superseded — a *map* `datum -> reason` of datums displaced by an equality
merge: the stale spelling of a fact whose terms have been rewritten to their
class representative (docs/equality.md). Three things make it its own state
rather than a reuse of `defeated` or `blocked`:
- `blocked` names *justifications*, and a directly asserted `(bornIn Dep
Chicago)` is a **premise with no justification at all** — `region-fixpoint`
seeds every premise IN unconditionally, so there is nothing for a block to
invalidate. Superseding has to act on the datum.
- `defeated` would be the wrong reason. A superseded spelling lost no
argument; it was restated, and `why-not` must be able to say so — hence the
map carries the displacing representative rather than being a bare set.
- It is **not** a forced OUT inside the fixpoint. A superseded datum stays in
`:in` for the purposes of `valid?`, because its rewritten twin is justified
*by it*: forcing it OUT structurally would invalidate the twin's own
justification and the merge would believe neither spelling. What
supersession removes is *reported* belief — `in?` and `in-datums` subtract
it — so the stale spelling stops matching, stops answering queries and stops
entering nogoods, while everything derived from it stands.
Retention is the point: the spelling is the **caller's premise**, so unlike an
excepted conclusion it is never swept, and dropping the equality gives it back.
Like `defeated` and `blocked` the map is *derived* — core recomputes it each
settle from the equality closure — so belief stays order independent.
* blocked — a set of *justification* ids whose rule's exception currently holds
(`exceptWhen`, see docs/exceptions.md). A blocked justification is not a
defeated conclusion: it is simply **invalid**, so it supports nothing, confers
no defeat-class, and does not make its consequence groundable — which is what
lets the ordinary dependency-directed sweep garbage-collect an excepted
conclusion instead of retaining it for revival. This module is pure and has no
KB, so it cannot run the exception query itself: the caller evaluates the
exception and hands the answer in with `set-blocked`, which relabels only the
region the change reaches. Like `defeated`, the set is *derived* — computed
from current state each settle, never accumulated — so belief stays order
independent.
Retraction is dependency-directed: drop the premise, relabel, then SWEEP the
affected closure — datums that end up OUT with no valid support and are not
defeated are solely supported by the retraction, so they (and their non-premise
justifications) are returned for the caller to delete from the stores. A datum that
is merely *defeated* keeps its support and is retained for later revival.
This module owns the in-memory graph; the caller owns physical deletion, since
only it holds the stores.(->just id informant antecedents consequence bindings)(->just id informant antecedents consequence bindings strength)Construct a Justification, defaulting strength to :monotonic and out to #{} (so a
bare monotone justification behaves exactly as before — it adds no defeasibility of its
own, and conferred-class caps it at its weakest antecedent).
Construct a Justification, defaulting `strength` to :monotonic and out to #{} (so a
bare monotone justification behaves exactly as before — it adds no defeasibility of its
own, and `conferred-class` caps it at its weakest antecedent).(add-justification tms just)(add-premise tms datum)(add-premise tms datum strength-kw)Add datum as a premise at strength (default :default).
Add `datum` as a premise at `strength` (default :default).
(block tms jids)Add jids to the blocked set (a delta on set-blocked, for a caller that knows
only what it just found rather than the whole answer). Reads and writes in one
step, so a delta cannot be computed against a set that has already moved.
Add `jids` to the blocked set (a delta on `set-blocked`, for a caller that knows only what it just found rather than the whole answer). Reads and writes in one step, so a delta cannot be computed against a set that has already moved.
(blocked tms)The justification ids currently blocked by their rule's exception.
The justification ids currently blocked by their rule's exception.
(blocked? tms jid)Is justification jid currently blocked?
Is justification `jid` currently blocked?
(clear-defeats! tms)Reset the derived defeated set and relabel — the basis for revival.
The region is the previously defeated nodes: lifting a forced OUT can only affect them and what follows from them, so a settle that defeated nothing last round does no work at all here.
Reset the derived defeated set and relabel — the basis for revival. The region is the *previously* defeated nodes: lifting a forced OUT can only affect them and what follows from them, so a settle that defeated nothing last round does no work at all here.
(create-tms)A fresh, empty truth-maintenance network — the reference implementation.
:in is the believed set and the authority on belief — nodes carry no label of
their own, so there is no second copy to drift. :groundable is the set that is
structurally derivable from the premises ignoring defeats: a defeated node that
is still groundable can revive, one that is not has lost its last derivation and
is swept. Both are maintained region-locally.
:blocked is the set of justification ids currently blocked by their rule's
exception; it starts empty and only a caller that has evaluated the exceptions can
fill it.
(Rules live in the stores as sentexes, not here.)
A fresh, empty truth-maintenance network — the reference implementation. `:in` is the believed set and the authority on belief — nodes carry no label of their own, so there is no second copy to drift. `:groundable` is the set that is *structurally* derivable from the premises ignoring defeats: a defeated node that is still groundable can revive, one that is not has lost its last derivation and is swept. Both are maintained region-locally. `:blocked` is the set of justification ids currently blocked by their rule's exception; it starts empty and only a caller that has evaluated the exceptions can fill it. (Rules live in the stores as sentexes, not here.)
(datums tms)(defeat tms datums)Force datums OUT (contradiction resolution) and relabel the region they affect.
Force `datums` OUT (contradiction resolution) and relabel the region they affect.
(defeat-class tms datum)The current defeat-class of an IN datum (monotonic / default), or nil
when the datum is OUT. Valid after relabel.
:classes holds only the datums above the lattice's bottom, so IN-ness is what
separates "OUT, hence no class" from "IN at the default class". An entry's mere
presence cannot carry both, since only one of them is information.
The current defeat-class of an IN datum (monotonic / default), or nil when the datum is OUT. Valid after `relabel`. `:classes` holds only the datums *above* the lattice's bottom, so IN-ness is what separates "OUT, hence no class" from "IN at the default class". An entry's mere presence cannot carry both, since only one of them is information.
(defeated tms)(defeated? tms datum)(dependents tms datum)Justification ids that use datum as an antecedent (or a defeater).
Justification ids that use `datum` as an antecedent (or a defeater).
(depth tms datum)(ensure-node tms datum depth)(graph-just j)The part of a justification the network is made of — everything except the
firing's :bindings.
Belief never reads the bindings: valid? needs the antecedents, conferred-class
the strength and the informant, and the region walks the consequence. The bindings
are the variable map of the firing that produced it, and only two readers want them
— re-evaluating an exceptWhen query and a NAF antecedent per firing — both of
which hold the KB and take the record from the store, where it is durable. So
the network keeps the graph and the store keeps the record, and the JTMS stops
holding a second copy of every justification. Measured (lein bench-jtms, a
rules-heavy corpus at 3.6 justifications per node): 80 of 277 B each.
It also normalizes — antecedents to a vector, out to a set, strength
defaulted — so that however a caller spells a justification, the two
representations store a value equal to each other's. :bindings is nil rather
than dropped, keeping the record shape fixed for every reader.
The part of a justification the **network** is made of — everything except the firing's `:bindings`. Belief never reads the bindings: `valid?` needs the antecedents, `conferred-class` the strength and the informant, and the region walks the consequence. The bindings are the variable map of the firing that produced it, and only two readers want them — re-evaluating an `exceptWhen` query and a NAF antecedent per firing — both of which hold the KB and take the **record** from the store, where it is durable. So the network keeps the graph and the store keeps the record, and the JTMS stops holding a second copy of every justification. Measured (`lein bench-jtms`, a rules-heavy corpus at 3.6 justifications per node): 80 of 277 B each. It also **normalizes** — antecedents to a vector, `out` to a set, strength defaulted — so that however a caller spells a justification, the two representations store a value equal to each other's. `:bindings` is nil rather than dropped, keeping the record shape fixed for every reader.
(has-justification? tms informant antecedents consequence)Is there already a support for consequence from informant over exactly these
antecedents (as a set)? Guards against duplicate justifications.
Is there already a support for `consequence` from `informant` over exactly these antecedents (as a set)? Guards against duplicate justifications.
(in-datums tms)(in? tms datum)Is datum believed? Structural support minus supersession: a datum the equality
layer has displaced keeps its place in the fixpoint (its twin is justified by it)
but is not believed, so it stops matching and stops answering queries.
Is `datum` believed? Structural support minus supersession: a datum the equality layer has displaced keeps its place in the fixpoint (its twin is justified by it) but is not believed, so it stops matching and stops answering queries.
(justification tms jid)(justifications tms)(known-datum? tms datum)Does the TMS hold a node for datum? False for an inert sentex
(core/assert-inert) — stored and indexed but never a TMS datum — which is how
retract! tells a belief-bearing retraction from a direct teardown.
Does the TMS hold a node for `datum`? False for an **inert** sentex (`core/assert-inert`) — stored and indexed but never a TMS datum — which is how `retract!` tells a belief-bearing retraction from a direct teardown.
(premise-strength tms datum)(premise? tms datum)(relabel tms)Recompute every node's label and defeat-class. This is the one whole-graph
operation, and it exists for recover, which rebuilds the network from the durable
store and therefore has no smaller region to start from. Nothing on the assert /
retract / settle path calls it.
It also clears the blocked set: blocking is derived from exception queries that are never stored, so a rebuild cannot recover it and must not inherit a stale one. Recovery lands unblocked, and the caller re-evaluates.
Recompute *every* node's label and defeat-class. This is the one whole-graph operation, and it exists for `recover`, which rebuilds the network from the durable store and therefore has no smaller region to start from. Nothing on the assert / retract / settle path calls it. It also **clears the blocked set**: blocking is derived from exception queries that are never stored, so a rebuild cannot recover it and must not inherit a stale one. Recovery lands unblocked, and the caller re-evaluates.
(reset-touched! tms)Clear the accumulated touched sets (see touched / touched-in). settle clears
them once it has read them, at the end — so the window a caller sees spans
everything since the last settle finished, which for edit is the whole deferred
batch and its one settle rather than the settle alone.
Clear the accumulated touched sets (see `touched` / `touched-in`). `settle` clears them once it has read them, at the *end* — so the window a caller sees spans everything since the last settle finished, which for `edit` is the whole deferred batch and its one settle rather than the settle alone.
(retract! tms datum)Dependency-directed retraction (drop premise / relabel / sweep). Returns {:removed-sentexes [datum...] :removed-justifications [jid...]}. Unknown datums no-op (empty result): retraction is idempotent.
Dependency-directed retraction (drop premise / relabel / sweep). Returns
{:removed-sentexes [datum...] :removed-justifications [jid...]}.
Unknown datums no-op (empty result): retraction is idempotent.(set-blocked tms jids)Replace the blocked set with jids — the justifications whose exception the caller
has just found to hold — and relabel the region the change reaches.
The set is replaced, not accumulated: the caller re-evaluates every exception it cares about and states the whole answer, exactly as core recomputes the defeated set each settle. Nothing here remembers that a justification was blocked a round ago, so belief cannot depend on the order the exceptions were discovered in.
The region is seeded from the consequences of the justifications whose blocked
status changed — blocking or unblocking j can only move j's conclusion and what
follows from it — so cost is proportional to that region, not to the graph, and a
call that changes nothing does no work at all. #{} unblocks everything.
Replace the blocked set with `jids` — the justifications whose exception the caller
has just found to hold — and relabel the region the change reaches.
The set is *replaced*, not accumulated: the caller re-evaluates every exception it
cares about and states the whole answer, exactly as core recomputes the defeated set
each settle. Nothing here remembers that a justification was blocked a round ago,
so belief cannot depend on the order the exceptions were discovered in.
The region is seeded from the **consequences of the justifications whose blocked
status changed** — blocking or unblocking j can only move j's conclusion and what
follows from it — so cost is proportional to that region, not to the graph, and a
call that changes nothing does no work at all. `#{}` unblocks everything.(snapshot tms)The network as one canonical persistent map (see -snapshot). A testing and
debugging surface — the differential oracle compares two implementations with it.
The network as one canonical persistent map (see `-snapshot`). A testing and debugging surface — the differential oracle compares two implementations with it.
(supersede tms m)Replace the superseded map with m ({datum reason}).
Replace, not accumulate, for the same reason set-blocked replaces: the caller
recomputes the whole answer from the current equality closure each settle, so a
supersession cannot outlive the merge that caused it and belief cannot depend on
the order the merges arrived in.
No relabel: supersession does not enter the fixpoint (see the namespace docstring),
it only subtracts from what in? reports, so there is no region to recompute.
**Replace** the superseded map with `m` (`{datum reason}`).
Replace, not accumulate, for the same reason `set-blocked` replaces: the caller
recomputes the whole answer from the current equality closure each settle, so a
supersession cannot outlive the merge that caused it and belief cannot depend on
the order the merges arrived in.
No relabel: supersession does not enter the fixpoint (see the namespace docstring),
it only subtracts from what `in?` reports, so there is no region to recompute.(superseded tms)The datum -> reason map of spellings an equality merge has displaced.
The `datum -> reason` map of spellings an equality merge has displaced.
(superseded? tms datum)(supersession tms datum)Why datum is superseded — the representative that displaced it — or nil.
Why `datum` is superseded — the representative that displaced it — or nil.
(supports tms datum)Justification ids that conclude datum (its supporting justifications).
Justification ids that conclude `datum` (its supporting justifications).
(suspend-premise tms datum)Drop datum's premise mark and relabel its region — a retraction's effect on
belief, and nothing else. Unknown datums no-op.
retract! is this plus the sweep, and the sweep is exactly the part that cannot be
put back: it deletes, so restoring the datum afterwards means re-deriving it at fresh
handles. Belief does not need it — a swept datum is OUT and ungroundable, so
dropping it moves no label — which is what makes the pair (suspend-premise, then
add-premise at the same strength) a reversible retraction. core/preview is the
caller: it answers what a removal would do to belief and then puts the premise back.
Bare, not !, because nothing is lost: the node, its justifications and its record
all stay exactly where they were.
Drop `datum`'s premise mark and relabel its region — a retraction's effect on **belief**, and nothing else. Unknown datums no-op. `retract!` is this plus the sweep, and the sweep is exactly the part that cannot be put back: it deletes, so restoring the datum afterwards means re-deriving it at fresh handles. Belief does not need it — a swept datum is OUT and ungroundable, so dropping it moves no label — which is what makes the pair (`suspend-premise`, then `add-premise` at the same strength) a reversible retraction. `core/preview` is the caller: it answers what a removal would do to belief and then puts the premise back. Bare, not `!`, because nothing is lost: the node, its justifications and its record all stay exactly where they were.
(sweep! tms seeds)Garbage-collect the consequence closure of seeds: every datum in it that is not
a premise and is no longer groundable is deleted, along with the justifications
touching it. Returns the same shape as retract!, for the caller to apply to its
own stores.
This is retract!'s sweep without the retraction. It exists because exceptWhen
removes a conclusion by invalidating its justification rather than by withdrawing a
premise: blocking suppresses groundability (region-fixpoint), so the conclusion is
ungroundable and this collects it exactly as a retraction would — the trade
docs/exceptions.md records under "Garbage collection, not defeat".
Labels must already be current — set-blocked relabels the same region — so this
only reads :groundable.
Garbage-collect the consequence closure of `seeds`: every datum in it that is not a premise and is no longer *groundable* is deleted, along with the justifications touching it. Returns the same shape as `retract!`, for the caller to apply to its own stores. This is `retract!`'s sweep without the retraction. It exists because `exceptWhen` removes a conclusion by invalidating its justification rather than by withdrawing a premise: blocking suppresses groundability (`region-fixpoint`), so the conclusion is ungroundable and this collects it exactly as a retraction would — the trade docs/exceptions.md records under "Garbage collection, not defeat". Labels must already be current — `set-blocked` relabels the same region — so this only reads `:groundable`.
What a truth-maintenance network must answer, independent of how it stores the
graph. Two implementations ship: RefTms here — an atom over one persistent map,
the reference — and vaelii.impl.dense-jtms, which holds the same graph in
bitmaps and primitive-keyed maps. Selected per KB (open-kb's :tms opt),
reference by default, and proven to answer identically by jtms_dense_oracle_test.
The seam is at the representation, not at the algorithm: both implementations run the same least-fixpoint relabel over the same affected region, because that is the semantics, not an implementation detail. What differs is where a node's premise flag, depth and adjacency live.
Every method is named with a leading -; the plain names (in?, add-premise, …)
are the public functions below, which dispatch here. Callers use those.
What a truth-maintenance network must answer, independent of how it stores the graph. Two implementations ship: `RefTms` here — an atom over one persistent map, the reference — and `vaelii.impl.dense-jtms`, which holds the same graph in bitmaps and primitive-keyed maps. Selected per KB (`open-kb`'s `:tms` opt), reference by default, and proven to answer identically by `jtms_dense_oracle_test`. The seam is at the *representation*, not at the algorithm: both implementations run the same least-fixpoint relabel over the same affected region, because that is the semantics, not an implementation detail. What differs is where a node's premise flag, depth and adjacency live. Every method is named with a leading `-`; the plain names (`in?`, `add-premise`, …) are the public functions below, which dispatch here. Callers use those.
(-node? tms datum)Is there a node for datum?
Is there a node for `datum`?
(-superseded tms)The datum -> reason supersession map.
The `datum -> reason` supersession map.
(-supersede tms m)Replace the supersession map (no relabel).
Replace the supersession map (no relabel).
(-justifications tms)Every live graph justification.
Every live graph justification.
(-justification tms jid)The graph justification (graph-just — no bindings), or nil.
The graph justification (`graph-just` — no bindings), or nil.
(-defeat-class tms datum)Defeat-class of an IN datum, nil when OUT.
Defeat-class of an IN datum, nil when OUT.
(-sweep tms seeds)Sweep the consequence closure of seeds.
Sweep the consequence closure of `seeds`.
(-reset-touched tms)Clear the touched sets.
Clear the touched sets.
(-add-premise tms datum strength)Mark datum a premise at strength.
Mark `datum` a premise at `strength`.
(-touched tms)Datums whose region was relabelled since the reset.
Datums whose region was relabelled since the reset.
(-datums tms)Seq of every datum with a node.
Seq of every datum with a node.
(-retract tms datum)Drop the premise, relabel, sweep; return the removals.
Drop the premise, relabel, sweep; return the removals.
(-snapshot tms)The whole network as one canonical persistent map — :nodes :justs :in :groundable :defeated :blocked :superseded :classes. This is the comparison
shape the differential oracle checks and the shape RefTms happens to store; a
dense implementation materializes it, so it is a debugging and testing surface,
never something an engine path calls.
The whole network as one canonical persistent map — `:nodes :justs :in :groundable :defeated :blocked :superseded :classes`. This is the *comparison* shape the differential oracle checks and the shape `RefTms` happens to store; a dense implementation materializes it, so it is a debugging and testing surface, never something an engine path calls.
(-blocked tms)The blocked justification-id set.
The blocked justification-id set.
(-defeat tms datums)Force datums OUT and relabel their region.
Force `datums` OUT and relabel their region.
(-relabel tms)Whole-graph relabel (recover only).
Whole-graph relabel (recover only).
(-dependents tms datum)Justification ids using datum as an antecedent.
Justification ids using `datum` as an antecedent.
(-premise? tms datum)Is datum a premise?
Is `datum` a premise?
(-defeated tms)The forced-OUT set.
The forced-OUT set.
(-ensure-node tms datum depth)Create the node if absent; lower its depth.
Create the node if absent; lower its depth.
(-clear-defeats tms)Empty the defeated set and relabel.
Empty the defeated set and relabel.
(-believed? tms datum)Is datum believed (IN, minus supersession)?
Is `datum` believed (IN, minus supersession)?
(-suspend-premise tms datum)Drop datum's premise mark and relabel — no sweep.
Drop `datum`'s premise mark and relabel — no sweep.
(-depth tms datum)Derivation depth, 0 when unknown.
Derivation depth, 0 when unknown.
(-believed tms)Seq of the believed datums, or nil when none.
Seq of the believed datums, or nil when none.
(-add-justification tms just)Record just and relabel what it moves.
Record `just` and relabel what it moves.
(-update-blocked tms f)Apply f to the blocked set as one atomic step.
Apply `f` to the blocked set as one atomic step.
(-set-blocked tms jids)Replace the blocked set and relabel what moved.
Replace the blocked set and relabel what moved.
(-supports tms datum)Justification ids concluding datum.
Justification ids concluding `datum`.
(-touched-in tms)Of those, the ones already believed when first relabelled.
Of those, the ones already believed when first relabelled.
(-premise-strength tms datum)Its assumption strength, or nil.
Its assumption strength, or nil.
(touched tms)The datums whose region has been relabelled since the last reset-touched! — a
superset of every datum whose belief could have flipped in that window. settle
reads it to tell tax/refresh-beliefs which handles moved, so a cache no moved
supporter touches is skipped.
Plus the datums a redundant justification landed on, which is the one entry here
whose belief provably did not move: the window is read as "what I published about
this datum may be out of date", and a second witness for an already-believed
conclusion moves that without moving a label (add-just* says why the alternative is
worse). Every consumer reads a superset, so an extra handle costs a re-derivation and
never an answer.
The datums whose region has been relabelled since the last `reset-touched!` — a superset of every datum whose belief could have flipped in that window. `settle` reads it to tell `tax/refresh-beliefs` which handles moved, so a cache no moved supporter touches is skipped. Plus the datums a **redundant** justification landed on, which is the one entry here whose belief provably did *not* move: the window is read as "what I published about this datum may be out of date", and a second witness for an already-believed conclusion moves that without moving a label (`add-just*` says why the alternative is worse). Every consumer reads a superset, so an extra handle costs a re-derivation and never an answer.
(touched-in tms)The subset of touched that was already believed when this window first
relabelled it. With touched and current belief that is the whole belief delta:
a datum in touched and IN now but not here came in, and one here that is OUT now
went out. The superset alone cannot say which — most of a relabelled region does
not move — so this is what a caller reporting consequences reads.
"When first relabelled" is what makes it a reading from before the window rather than from part-way through it: a datum relabelled twice keeps the earlier answer.
The subset of `touched` that was **already believed** when this window first relabelled it. With `touched` and current belief that is the whole belief delta: a datum in `touched` and IN now but not here came *in*, and one here that is OUT now went *out*. The superset alone cannot say which — most of a relabelled region does not move — so this is what a caller reporting consequences reads. "When first relabelled" is what makes it a reading from before the window rather than from part-way through it: a datum relabelled twice keeps the earlier answer.
(unblock tms jids)Remove jids from the blocked set.
Remove `jids` from the blocked set.
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 |