The structural genlCx producer for reified-NAT contexts — docs/context-nat.md.
A (contextArgSubrelation F pos R) declaration says two F-contexts identical except
at argument pos are ordered by the sub-relation R on that argument. This namespace
reads the declarations and the context NATs of F from the store and materializes
the genlCx edges they entail: for two siblings whose pos arguments stand in R, the
more specific one (its argument R-below the other's) is deduced to genlCx the more
general, as a justified sentex in CxUniverse. So the edge belief-follows for free —
retract a context (its termOfUnit map), the declaration, or the R-evidence, and the
ordinary JTMS relabel withdraws it. It is never a premise anyone asserted.
R is resolved by a bounded oracle, because the producer runs on the assert
maintenance path and a genlCx edge feeds the taxonomy closure a relabel loop reads — so
a prover search is out (docs/naf.md): either a registered pure structural comparator
(the datetime one, keyed on subintervalOf over DatetimeFn terms) answers it, or a
believed stored (R a b) fact does. A comparator answer is a pure function of the two
expressions, already carried by the termOfUnit antecedents, so it needs no extra
supporter; a stored fact contributes its own handle so defeating it withdraws the edge.
Materialization reuses the derived-sentex pattern special/deduce-lift uses:
find-or-create-sentex, then special/derived-sentex-added to reach the genlCx closure
and post the re-check triggers, then a JTMS justification under the
contextArgSubrelation informant.
The structural genlCx producer for reified-NAT contexts — docs/context-nat.md. A `(contextArgSubrelation F pos R)` declaration says two `F`-contexts identical except at argument `pos` are ordered by the sub-relation `R` on that argument. This namespace reads the declarations and the context NATs of `F` from the store and **materializes** the `genlCx` edges they entail: for two siblings whose `pos` arguments stand in `R`, the more specific one (its argument `R`-below the other's) is deduced to `genlCx` the more general, as a **justified** sentex in CxUniverse. So the edge belief-follows for free — retract a context (its `termOfUnit` map), the declaration, or the `R`-evidence, and the ordinary JTMS relabel withdraws it. It is never a premise anyone asserted. `R` is resolved by a **bounded** oracle, because the producer runs on the assert maintenance path and a genlCx edge feeds the taxonomy closure a relabel loop reads — so a prover search is out (docs/naf.md): either a registered pure structural comparator (the datetime one, keyed on `subintervalOf` over `DatetimeFn` terms) answers it, or a believed stored `(R a b)` fact does. A comparator answer is a pure function of the two expressions, already carried by the `termOfUnit` antecedents, so it needs no extra supporter; a stored fact contributes its own handle so defeating it withdraws the edge. Materialization reuses the derived-sentex pattern `special/deduce-lift` uses: `find-or-create-sentex`, then `special/derived-sentex-added` to reach the genlCx closure and post the re-check triggers, then a JTMS justification under the `contextArgSubrelation` informant.
(any-context-subrelations? kb)Cheap gate: does the KB declare any contextArgSubrelation? The producer is a no-op
otherwise — one O(1) functor count per assert, the shape nat/any-corresponding-predicates?
has.
Cheap gate: does the KB declare any `contextArgSubrelation`? The producer is a no-op otherwise — one O(1) functor count per assert, the shape `nat/any-corresponding-predicates?` has.
(reconcile-genlCx! kb sentence context)The structural-genlCx maintenance a just-asserted sentence in context calls for,
scoped to what could have changed:
(contextArgSubrelation F …) declaration reconciles all of F's contexts;cx/ context reconciles that context's function — its arrival, or
the mint of a new context beside it, is what creates a sibling pair to order.A no-op — one functor count — on a KB that declares no contextArgSubrelation. Both
arrival orders reach the same fixpoint: a declaration arriving after the contexts sweeps
them (reconcile-function), and a context arriving after a declaration is swept when it
is stored into. Idempotent, so re-running orders the same edges without duplicating.
The structural-genlCx maintenance a just-asserted `sentence` in `context` calls for, scoped to what could have changed: - a `(contextArgSubrelation F …)` declaration reconciles all of `F`'s contexts; - a fact stored into a `cx/` context reconciles that context's function — its arrival, or the mint of a new context beside it, is what creates a sibling pair to order. A no-op — one functor count — on a KB that declares no `contextArgSubrelation`. Both arrival orders reach the same fixpoint: a declaration arriving after the contexts sweeps them (`reconcile-function`), and a context arriving after a declaration is swept when it is stored into. Idempotent, so re-running orders the same edges without duplicating.
(reconcile-revivals! kb)Rebuild the structural genlCx edges for every declared contextArgSubrelation
function — the build direction a belief revival needs, which reconcile-genlCx! (only
ever called from the assert choke-point) cannot serve.
Belief of a contextArgSubrelation declaration — or of a stored (R a b) evidence fact
— can flip OUT→IN with no assert: retracting a monotonic defeater above it revives it.
The JTMS revives a justification that already exists, but an edge the producer never
built (because the declaration was OUT when the contexts were stored) has no
justification to revive, so the edge would stay absent. A teardown therefore re-runs the
producer once its belief has settled, and the withdraw direction the JTMS already handles
meets a build direction here.
Idempotent (materialize-edge! adds no duplicate justification) and local: scoped to
the declared context functions, each reconciled only over its own contexts — bounded by
the context-NAT population, never the whole graph. Behind the free in-memory
contextDenotingFunction gate first — a KB with no cx/ context to order pays neither
the any-context-subrelations? functor-count index read nor anything else, so the retract
hot path is untouched on every KB that declares no context function
(assert_cost_test).
Rebuild the structural genlCx edges for **every** declared `contextArgSubrelation` function — the build direction a belief *revival* needs, which `reconcile-genlCx!` (only ever called from the assert choke-point) cannot serve. Belief of a `contextArgSubrelation` declaration — or of a stored `(R a b)` evidence fact — can flip OUT→IN with no assert: retracting a monotonic defeater above it revives it. The JTMS revives a *justification that already exists*, but an edge the producer never built (because the declaration was OUT when the contexts were stored) has no justification to revive, so the edge would stay absent. A teardown therefore re-runs the producer once its belief has settled, and the withdraw direction the JTMS already handles meets a build direction here. Idempotent (`materialize-edge!` adds no duplicate justification) and **local**: scoped to the declared context functions, each reconciled only over its own contexts — bounded by the context-NAT population, never the whole graph. Behind the **free** in-memory `contextDenotingFunction` gate first — a KB with no `cx/` context to order pays neither the `any-context-subrelations?` functor-count index read nor anything else, so the retract hot path is untouched on every KB that declares no context function (`assert_cost_test`).
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 |