The representation seam of the truth-maintenance system: the Tms protocol
alone, with no implementation.
It lives in its own namespace, apart from vaelii.impl.jtms (the reference
network) and vaelii.impl.dense-jtms (the dense one), for two reasons. Both
implementations depend on it and neither on the other, so the seam is the one
thing they share. And it is large — forty-odd methods, each documented — which
makes the generated protocol map big enough that re-evaluating the form (as
cloverage does, form by form, to instrument a namespace) overflows the JVM's
64 KB per-method bytecode limit; isolated here, the protocol is loaded but not
instrumented while the whole of vaelii.impl.jtms still is (scripts/coverage.sh).
The representation seam of the truth-maintenance system: the `Tms` protocol alone, with no implementation. It lives in its own namespace, apart from `vaelii.impl.jtms` (the reference network) and `vaelii.impl.dense-jtms` (the dense one), for two reasons. Both implementations depend on it and neither on the other, so the seam is the one thing they share. And it is large — forty-odd methods, each documented — which makes the generated protocol map big enough that re-evaluating the form (as cloverage does, form by form, to instrument a namespace) overflows the JVM's 64 KB per-method bytecode limit; isolated here, the protocol is loaded but not instrumented while the whole of `vaelii.impl.jtms` still is (scripts/coverage.sh).
What a truth-maintenance network must answer, independent of how it stores the
graph. Two implementations ship: RefTms in vaelii.impl.jtms — 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),
dense by default since 0.9.0, 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.
Four obligations. Miss one and a network is wrong, not slow — belief is the last thing in the engine that may drift silently, since a bad label does not throw, it just answers a query differently. Each names the gate that holds it, because an obligation with no gate is a comment.
The same fixpoint over the same region. A datum is believed when it is a
premise or has a valid justification (all antecedents believed), minus the
defeated set; the label is recomputed over the forward consequence closure of
whatever changed, with the rest held fixed as boundary. That is the semantics
of belief here (docs/nmtms.md), not a strategy an implementation may improve on:
the region fixpoint is equal to the global one because a least fixpoint with the
boundary fixed is unique, and uniqueness is also the whole of why locality costs
no order independence. An implementation may move where the graph lives; it may
not move what is believed. Gate: jtms_dense_oracle_test, which compares the
entire -snapshot after every step of a randomized operation stream — not a
sampled read, because a divergence in :groundable is invisible to -believed?
until a retraction three operations later collects the wrong node.
A mutation is atomic to a concurrent reader. A reader sees the state wholly
before or wholly after a relabel, never half of one — the single-writer contract
owes the incidental reader that much (a web browser over a REPL's KB,
docs/storage.md). How is not the obligation and the two differ: the reference
by compare-and-set on its state atom, the dense network by taking its
StampedLock for writing. Gate: jtms_atomicity_test, whose atomicity half runs
against both networks for exactly this reason.
The flips are inside the published window, and the window inside the region.
-touched is not diagnostics: preview, the consequence report and the change
feed all read it instead of diffing the believed set, which would be O(KB) per
write (docs/preview.md, docs/feed.md). A window that missed a flip serves a stale
report; one that outran its own region would say the operation was not local after
all. The containment is deliberately one-way — the window is a superset of
the flip set (defenses.md) — so this obligation is containment and never equality.
Gate: the oracle test checks both containments on both networks after every
step, and jtms_locality_test measures the published window across graph sizes
on both — a region widened back to the whole graph answers identically, so a
comparison of labels alone would pass it.
No store, by construction. Every method here takes the network plus integers
and plain values. Nothing in the seam can carry a record store, an index or a KB,
and no implementation may acquire one. Two things rest on that and neither is
optional. A node holds no reference to the sentex it labels — the network is
always resident, so a strong reference would pin every record in RAM and defeat a
paging backend entirely (measured: the nodes reached 50% of the record store).
And the class fixpoint's per-node strength read is a memory read on every
representation, which is what makes locality a claim about all of them rather than
about the one whose reads happen to be free — on a disk store that read would be a
lock and a slot decode, on a server store a round trip, per in-region node per
worklist pop. Gate: the shape of this protocol, plus both implementations' ns
forms, which name no store. A store-backed network would break the structural
guarantee and inherit an obligation nothing here gates: it would owe a
read-counting one of its own.
One claim is deliberately not on that list, because nothing at this seam can hold
it: the cost of the in-region work itself. Obligation 3 says a small region was asked
for and obligation 4 says nothing was paid per boundary node, and neither says the
small region was cheap — a structure whose every write rebuilds a whole container
satisfies both and still grows with the KB, at a scale no unit test reaches
(docs/defenses.md argues it under Locality is a claim about every representation).
It is held by lein bench-jtms and by review. It is written down here anyway,
because an implementation that is never told about a claim cannot be held to it.
Every method is named with a leading -; the plain names (in?, add-premise, …)
are the public functions in vaelii.impl.jtms, which dispatch here. Callers use those.
What a truth-maintenance network must answer, independent of how it stores the graph. Two implementations ship: `RefTms` in `vaelii.impl.jtms` — 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), dense by default since 0.9.0, 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. ## What an implementation owes Four obligations. Miss one and a network is *wrong*, not slow — belief is the last thing in the engine that may drift silently, since a bad label does not throw, it just answers a query differently. Each names the gate that holds it, because an obligation with no gate is a comment. 1. **The same fixpoint over the same region.** A datum is believed when it is a premise or has a valid justification (all antecedents believed), minus the defeated set; the label is recomputed over the forward consequence closure of whatever changed, with the rest held fixed as boundary. That is the *semantics* of belief here (docs/nmtms.md), not a strategy an implementation may improve on: the region fixpoint is equal to the global one because a least fixpoint with the boundary fixed is unique, and uniqueness is also the whole of why locality costs no order independence. An implementation may move where the graph lives; it may not move what is believed. Gate: `jtms_dense_oracle_test`, which compares the entire `-snapshot` after **every** step of a randomized operation stream — not a sampled read, because a divergence in `:groundable` is invisible to `-believed?` until a retraction three operations later collects the wrong node. 2. **A mutation is atomic to a concurrent reader.** A reader sees the state wholly before or wholly after a relabel, never half of one — the single-writer contract owes the incidental reader that much (a web browser over a REPL's KB, docs/storage.md). *How* is not the obligation and the two differ: the reference by compare-and-set on its state atom, the dense network by taking its `StampedLock` for writing. Gate: `jtms_atomicity_test`, whose atomicity half runs against both networks for exactly this reason. 3. **The flips are inside the published window, and the window inside the region.** `-touched` is not diagnostics: `preview`, the consequence report and the change feed all read it instead of diffing the believed set, which would be O(KB) per write (docs/preview.md, docs/feed.md). A window that missed a flip serves a stale report; one that outran its own region would say the operation was not local after all. The containment is deliberately one-way — the window is a **superset** of the flip set (defenses.md) — so this obligation is containment and never equality. Gate: the oracle test checks both containments on both networks after every step, and `jtms_locality_test` measures the published window across graph sizes on both — a region widened back to the whole graph answers identically, so a comparison of labels alone would pass it. 4. **No store, by construction.** Every method here takes the network plus integers and plain values. Nothing in the seam can carry a record store, an index or a KB, and no implementation may acquire one. Two things rest on that and neither is optional. A node holds **no reference to the sentex it labels** — the network is always resident, so a strong reference would pin every record in RAM and defeat a paging backend entirely (measured: the nodes reached 50% of the record store). And the class fixpoint's per-node strength read is a *memory* read on every representation, which is what makes locality a claim about all of them rather than about the one whose reads happen to be free — on a disk store that read would be a lock and a slot decode, on a server store a round trip, per in-region node per worklist pop. Gate: the shape of this protocol, plus both implementations' `ns` forms, which name no store. A store-backed network would break the structural guarantee and inherit an obligation nothing here gates: it would owe a read-counting one of its own. One claim is deliberately **not** on that list, because nothing at this seam can hold it: the cost of the in-region work itself. Obligation 3 says a small region was asked for and obligation 4 says nothing was paid per boundary node, and neither says the small region was *cheap* — a structure whose every write rebuilds a whole container satisfies both and still grows with the KB, at a scale no unit test reaches (docs/defenses.md argues it under *Locality is a claim about every representation*). It is held by `lein bench-jtms` and by review. It is written down here anyway, because an implementation that is never told about a claim cannot be held to it. Every method is named with a leading `-`; the plain names (`in?`, `add-premise`, …) are the public functions in `vaelii.impl.jtms`, 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.
(-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.
Set `strength` as the rule-contribution slot of every justification whose informant is `informant`, and relabel the region their consequences span.
(-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.
(-any-node? tms)Is there any node at all? A boolean that must not
materialize the datum seq — (first (-datums …)) drains the whole dense bitmap
into boxed Longs, so callers on a render/poll path use this instead.
Is there any node at all? A boolean that must not materialize the datum seq — `(first (-datums …))` drains the whole dense bitmap into boxed Longs, so callers on a render/poll path use this instead.
(-defeat tms datums)Force datums OUT and relabel their region.
Force `datums` OUT and relabel their region.
(-relabel tms)Whole-graph relabel — no engine path calls it; see
vaelii.impl.jtms/relabel.
Whole-graph relabel — no engine path calls it; see `vaelii.impl.jtms/relabel`.
(-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.
(-touched-new tms)Datums whose node this window created.
Datums whose node this window created.
(-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.
(-any-belief? tms)Is any datum believed (IN, minus supersession)? Like
-any-node?, terminates at the first believed datum rather than draining -believed.
Is any datum believed (IN, minus supersession)? Like `-any-node?`, terminates at the first believed datum rather than draining `-believed`.
(-premise-strength tms datum)Its assumption strength, or nil.
Its assumption strength, or nil.
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 |