vaelii.impl.jtms — com.vaelii/vaelii 0.24.0

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 or name it as their rule (: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). Because labels are computed from the current justification set rather than accumulated as events arrive, belief is order-independent. A contradiction takes nothing OUT here: the settle places it as a contradicts and a defeat, and the read walk hides the loser at the readers where the defeat is in force (vaelii.impl.except), so the network holds support labels only.

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 at a reader (vaelii.impl.decide); the network records no defeat, and nothing forces a datum OUT.

• 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 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.
  • 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 and stops answering queries, while everything derived from it stands. The nogood families detect over the IN label (network-in?), so a nogood with a superseded member keeps its placement, and the clash reports leave it out (docs/nmtms.md).

  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 blocked the map is derived — core recomputes it each settle from the equality closure — so belief stays order independent.

• forced — three sets the forced-monotonic roster writes (docs/nmtms.md, "The forced-monotonic roster"): :mono, premises whose class is :monotonic whatever strength they carry; :out, datums the fixpoint never adds, a premise included; and :void, justifications that support nothing and confer no class. Each is an attribute of the element it names, written by the caller with the element and rewritten when the roster moves (set-forced), so the stored content keeps the strength it was written at and every record a forced set governs stays stored.

• blocked — a set of justification ids whose rule's exception currently holds (exceptWhen, see docs/exceptions.md). A blocked justification is simply invalid, so it supports nothing and confers no defeat-class — which is what lets the ordinary dependency-directed sweep garbage-collect an excepted conclusion. 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. 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 are solely supported by the retraction, so they (and their non-premise justifications) are returned for the caller to delete from the stores.

This module owns the in-memory graph; the caller owns physical deletion, since only it holds the stores.

*dedup-cache* clj

{:tms tms :m mutable-HashMap-of-consequence→HashSet-of-just-keys}, or nil — the default, and has-justification? scans -supports as always.

A run-scoped index over the dedup question. A conclusion re-derived by k witnesses is asked about once per witness, and each ask scans every justification it already holds — Θ(k²) same-antecedents? comparisons per conclusion across a forward run, with a -justification fetch apiece (the W4 join pyramid at 1k: ~430k firings over ~66k conclusions, and the scan is the largest line in the profile). Bound by chain/chain for the length of a run, the first ask per conclusion builds its key set from -supports once and every later ask is one hash probe.

The binding carries the TMS it was built beside, and dedup-cache-for hands the map out only to that TMS: a nested run over a second KB (legal from a :on-progress callback) reaches these fns with the first KB's binding still in force, and handle spaces overlap, so an unscoped reuse would answer one KB's dedup question from the other's supports. Anything but the owning TMS bypasses to the reference scan.

Justification existence is structural, not belief: a label flip adds and removes nothing here, so no entry goes stale by belief moving — only by a justification being removed, which reaches the graph on exactly two paths (retract!, sweep!), and both clear the cache wholesale. add-justification extends the entry it passes through, so a bound cache never disagrees with the graph it mirrors. The keys are handle-content — no canonicalization — so there is no canon stamp to carry (observe/*handle-cache*, which has one, says what that kind of stamp is for; the :tms slot here is identity, not currency).

->just clj

(->just id informant antecedents consequence bindings)

(->just id informant antecedents consequence bindings strength)

Construct a Justification, defaulting strength to :monotonic — a bare monotone justification adds no defeasibility of its own, so conferred-class caps it at its weakest antecedent. A rule-handle informant is taken out of antecedents (without-informant).

add-justification clj

(add-justification tms just)

(add-justification tms just k)

Add just to the network. k, when given, is its justification-key, already built for the has-justification? that guarded the add.

add-premise clj

(add-premise tms datum)

(add-premise tms datum strength-kw)

Add datum as a premise at strength (default :default).

any-belief? clj

(any-belief? tms)

any-node? clj

(any-node? tms)

blocked clj

(blocked tms)

The justification ids currently blocked by their rule's exception.

classes-in-region clj

(classes-in-region tms region in)

The defeat-classes of the datums in holds inside region, where region and in are a grounded-in-region answer: the classes belief carries with that answer's extra forced OUT, the rest of the graph held at its current classes.

The least fixpoint region-classes computes during a relabel, over the same equation — a datum's class is the strongest of its premise strength and what each valid justification confers, and a justification confers the weakest of its own strength and its antecedents' classes. Every member starts at :default, the bottom, and the operator is monotone, so iterating to stability reaches the least fixpoint whatever the visit order. Built on the protocol reads, like grounded-in-region, so both network representations answer it without implementing a method.

The settle's reader of it is a nogood weighed at a vantage that withdraws part of what supports a member (docs/nmtms.md, "A defeat is scoped to its vantage").

consequence-closure clj

(consequence-closure tms seeds)

The forward consequence closure of seeds, seeds included: every datum a justification resting on one of them concludes, transitively. The region grounded-in-region labels, for a caller that needs the datums a forced-OUT set can move and not their labels.

create-tms clj

(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. It is 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 clj

(datums tms)

defeat-class clj

(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.

dependents clj

(dependents tms datum)

Justification ids that use datum as an antecedent (or a defeater).

depth clj

(depth tms datum)

dissoc-all clj

(dissoc-all m ks)

(apply dissoc m ks) in one transient pass. apply dissoc walks the map once per key with a full HAMT path copy each time, and ks here is the whole swept region of a retraction — which is a routine path rather than a rare one, since an exceptWhen block runs the sweep on ordinary fact arrival.

Public because the dense network sweeps the same region out of the same shape: its superseded is the one persistent map it keeps (docs/density.md), so vaelii.impl.dense-jtms drops a swept region from it through this rather than through a second copy of the reasoning.

drop-justification! clj

(drop-justification! tms jid)

Remove the one justification jid from the network, relabel the region it supported, and sweep what that leaves OUT. Returns retract!'s shape, for the caller to apply to its own stores; jid's own record is the caller's to delete, and is listed only in :removed-supports.

The one removal that names a justification rather than a datum. Every other one reaches a justification through a datum leaving — its consequence swept, or an antecedent or rule retracted — which is right whenever a justification is wrong because something it rests on went. A permuting mark leaving is the case where a justification is wrong about where it points: the firing still holds, but at a spelling the store stopped folding into its row (chain/reconcile-spellings!).

ensure-node clj

(ensure-node tms datum depth)

forced? clj

(forced? tms kind x)

Is x a member of forced set kind?

graph-just clj

(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 without the informant, 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.

grounded-in-region clj

(grounded-in-region tms extra)

(grounded-in-region tms extra belief-only)

(grounded-in-region tms extra belief-only invalid)

For extra — datums to force OUT — the forward consequence closure of extra (:region) and, within it, the datums that stay believed once extra is disbelieved (:in), the rest of the graph held at its current label.

Read region-local: belief for a datum outside the region is taken per-datum from in?, never materialized, so cost is proportional to the region and not to the KB — the property that keeps classify-local linear in the number of dilemmas rather than quadratic (grounded_in_region_test). The walk mirrors affected-region over the closure and the fixpoint mirrors region-fixpoint over it, both restricted to the region. Built on the protocol reads (in?, dependents, supports, justification, premise?, blocked, superseded?), so both network representations answer it identically without either implementing a method — the derived-read footing revived has.

The read behind the solve-free skeptical/credulous bracket (vaelii.impl.asp.label/classify-local, docs/labeling.md).

belief-only, when given, maps a justification to the antecedent, or the set of antecedents, it reads at its current label rather than the recomputed one, or nil: exc/belief-only-antecedent, for a reader's copy that rests on an equality hidden wherever the copy is read. invalid is a set of justification ids read as invalid, as a blocked one is: a guarded firing a reader re-asks and finds blocked.

has-justification? clj

(has-justification? tms informant antecedents consequence)

(has-justification? tms informant antecedents consequence k)

Is there already a support for consequence from informant over exactly these antecedents (as a set)? Guards against duplicate justifications. Answered from the dedup index when one is bound for this TMS — the same judgement, one hash probe — and by the supports scan otherwise. k, when given, is justification-key of the same informant and antecedents.

held clj

(held tms)

The hold open on tms, or nil.

hold! clj

(hold! tms h)

Open hold h (observe/new-hold) on tms, and answer whether it opened: false when a hold is open on it already. Until release!, every relabel records the labels it moves as they were before the hold's first move, and once observe/open-hold! registers h, a thread other than its owner reads belief, the blocked and superseded sets, and on the reference every read, from those. A settle holds its network this way, so a reader beside it reads the belief the settle began from until the settle publishes what it decided (vaelii.impl.settle/settle).

in-datums clj

(in-datums tms)

in? clj

(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.

justification clj

(justification tms jid)

justification-key clj

(justification-key informant antecedents)

The dedup key of a justification from informant over antecedents — just-key, for a caller that asks has-justification? and then adds the justification, and so would otherwise build the same set twice.

justifications clj

(justifications tms)

known-datum? clj

(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.

lowered-depths clj

(lowered-depths datum depth dependents antecedents consequence depth-of)

{node depth} for datum at depth and for every node downstream of it whose shallowest justification reads shallower once it is, walked shallowest first. Writes nothing. dependents names the justification ids citing a node, antecedents and consequence read one justification (nil for an id no longer stored), and depth-of is the stored depth.

network-in? clj

(network-in? tms datum)

Is datum IN in the network, a superseded spelling included? The families chain/place-nogoods! places detect their nogoods over this label, so a nogood with a superseded member keeps its placement (docs/nmtms.md).

premise-class clj

(premise-class tms datum)

The class datum's premise mark confers: :monotonic for a :mono member, its premise strength otherwise, nil for a datum that is no premise.

premise-strength clj

(premise-strength tms datum)

premise? clj

(premise? tms datum)

region-depths clj

(region-depths region
               premise?
               supports
               dependents
               antecedents
               consequence
               depth-of)

{node depth} for each node of region whose depth moves when the region is solved afresh, every node outside it held at its stored depth. region is closed under consequence (an affected region), so no node outside it reads one inside. Writes nothing; the accessors are lowered-depths', plus premise? and supports.

Knuth's generalization of Dijkstra's algorithm: a justification is queued once its last antecedent inside the region is final, and the queue pops shallowest first. A region node that no justification reaches from outside the region keeps its stored depth.

region-in clj

(region-in tms region scope base extra belief-only invalid)

The datums of scope, a part of region closed forward within it, that stay believed with extra forced OUT and invalid (justification ids) read as invalid, every datum of region outside scope read at its label in base and every datum outside region at its live one, added to base: grounded-in-region*'s fixpoint over scope.

relabel clj

(relabel tms)

Recompute every node's label and defeat-class, and clear the blocked and superseded sets — the whole-graph counterpart to the region relabels the assert / retract / settle path runs, for a caller that holds no smaller region. Nothing on the live paths calls it: the assert / retract / settle path relabels regions, and recover composes the region relabels its own rebuild runs (recovery/rebuild-tms), its settle re-deriving blocking wholesale. It is the differential oracle's whole-graph operation (strength_test, jtms_dense_oracle_test, jtms_blocked_test), which is why both representations implement it.

It clears blocked and superseded because both are derived from queries that are never stored — a whole-graph relabel cannot recover either and must not inherit a stale one.

release! clj

(release! tms h)

Close hold h on tms. A no-op for a hold that is not the one open.

reset-touched! clj

(reset-touched! tms)

Clear the accumulated touched sets (see touched / touched-in / touched-new). 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.

restrength-informant clj

(restrength-informant tms informant strength)

Set strength as the rule-contribution slot of every justification whose informant is informant, and relabel the region their consequences span.

A justification's :strength is the rule's contribution, read off the record at fire time (chain/rule-view-of) — a cache of provers/firing-strength. When that moves (a re-asserted rule's defeasibility resolves strict, or an exceptWhen arrives or leaves: special/restrength-firings!), the cache must move with it, or belief keeps the arrival order the slot resolution exists to remove: the same rule stated defeasible-then-strict and strict-then-defeasible would confer two different classes on conclusions already derived. The antecedent half of conferred-class is already read live at labelling time, so this one scalar is the only stored copy — updated here, then relabelled through the full affected region, since a class that rises can flip defeat decisions anywhere in the consumer ancestor set.

rests-on clj

(rests-on j)

Every handle justification j needs believed to be valid: its antecedents, plus its informant when that is a rule handle. The sweep preview, why-not's missing list, the visibility check and recovery's storedness check read this.

retract! clj

(retract! tms datum)

Dependency-directed retraction (drop premise / relabel / sweep). Returns {:removed-sentexes [datum...] :removed-justifications [jid...] :removed-supports [[consequence informant]...]}, the last absent when no justification went; a caller deletes the records and the justifications, and reads the supports without a justification fetch. Unknown datums no-op (empty result): retraction is idempotent.

revived clj

(revived tms)

(revived tms t)

The datums this window brought back: relabelled, believed now, not believed when the window opened, and already in the graph before it opened.

A revival is the one belief move nothing downstream of it has seen. A datum arriving is chained from as it arrives; a datum losing belief withdraws its conclusions through the justifications that name it. A datum that goes OUT and comes back has neither — no arrival to chain from, no justification to withdraw — and while it was OUT the belief-filtered matcher hid it, so a partner that arrived meanwhile joined against nothing. settle re-seeds these onto the agenda for exactly that reason.

The three window sets between them are the whole belief delta, and this is the corner of it that costs work rather than a report: touched minus touched-in is what gained belief, and minus touched-new is the part of that which is not a datum the writer has already chained from. A datum a forced-set change took OUT inside the window (-touched-out) is one too when it is believed again by the window's end, whether or not it was believed when the window opened: a partner arriving while it was OUT joined against nothing.

The two-arity takes touched as the caller already read it — settle reads the region once per pass and hands the value to everything in the pass that wants it, since the dense network materializes a fresh set on every read.

set-blocked clj

(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. 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.

set-forced clj

(set-forced tms kind xs on?)

Add each of xs to forced set kind (on? true) or take it out, and relabel the region the members that moved reach. :mono names premises whose class is :monotonic whatever strength they carry, :out datums never IN, and :void justifications that support nothing. A member may be written before its node or its justification exists, so the element never holds a label the set rules out.

snapshot clj

(snapshot tms)

The network as one canonical persistent map (see -snapshot). A testing and debugging surface — the differential oracle compares two implementations with it.

supersede clj

(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.

superseded clj

(superseded tms)

The datum -> reason map of spellings an equality merge has displaced.

superseded? clj

(superseded? tms datum)

supersession clj

(supersession tms datum)

Why datum is superseded — the representative that displaced it — or nil.

supports clj

(supports tms datum)

Justification ids that conclude datum (its supporting justifications).

suspend-premise clj

(suspend-premise tms datum)

Drop datum's premise mark and relabel its region without sweeping: a retraction's effect on belief, undone by add-premise at the same strength. Unknown datums no-op. Bare, not !: the node and its justifications stay. core/preview is the caller (docs/nmtms.md).

sweep! clj

(sweep! tms seeds)

Garbage-collect the consequence closure of seeds: every datum in it that is not a premise and is OUT 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 a derivation (region-fixpoint), so the conclusion is OUT 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 :in.

touch-mark clj

(touch-mark tms)

A mark of this point in the touched window, for a reader that asks the window more than once in it: touched-since answers what was recorded after it. Each reader keeps its own mark.

touched clj

(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.

touched-in clj

(touched-in tms)

The subset of touched whose label was IN when this window first relabelled it. With touched and current belief this set gives the label 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, since most of a relabelled region does not move. A superseded spelling keeps an IN label and is not believed (in?), so settle-finish drops the spellings superseded when the window opened before it reports belief.

"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.

touched-new clj

(touched-new tms)

The datums whose node this window created — the ones that had no label to move because they had no node. touched-in cannot say this: a brand-new datum and a stored one that has been OUT since the settle before both read as "not believed when the window opened", and they are the two halves revived has to keep apart.

touched-since clj

(touched-since tms mark)

The datums touched recorded after mark (touch-mark): a datum relabelled again since the mark is in it although touched held it already, which a set difference over touched would drop. A superset of what moved since the mark, as touched is of what moved in the window. The whole of touched for a mark the window outdated (reset-touched!) or a nil one.

with-dedup-cache clj macro

(with-dedup-cache tms & body)

Run body with the justification dedup index engaged for tms; an outer cache over the same TMS is reused rather than shadowed — the composition observe/with-handle-cache makes — and one over another TMS is shadowed by a fresh map. A no-op when observe/*chain-fast-paths* is bound false — the reference lever chain_fast_paths_test pulls.