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. What the edge shows the contexts under it is the
settle's (special/drain-context-moves!), as for an edge somebody asserted (vaelii#56),
so the caller settles once an edge was built.
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. What the edge shows the contexts under it is the settle's (`special/drain-context-moves!`), as for an edge somebody asserted (vaelii#56), so the caller settles once an edge was built.
(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)The structural-genlCx maintenance a just-asserted sentence calls for, scoped to the
sibling pairs it can have changed:
(contextArgSubrelation F …) declaration reconciles every pair of F's contexts;(termOfUnit K E) map with K a cx/ constant — the mint of a context —
reconciles the pairs K is in, since a new context is what creates a sibling pair;(R a b) fact on a declared sub-relation reconciles the pairs whose ordered
arguments are a below b, in the functions declared to order by R. A comparator
dimension needs nothing but the contexts, but a dimension resolved by stored facts
has the evidence arrive on its own schedule.Any other fact, including one stored into a cx/ context that already exists, creates
no pair and reconciles nothing. A no-op — one functor count — on a KB that declares no
contextArgSubrelation.
Returns true when an edge gained a justification, which the caller settles.
The structural-genlCx maintenance a just-asserted `sentence` calls for, scoped to the sibling pairs it can have changed: - a `(contextArgSubrelation F …)` declaration reconciles every pair of `F`'s contexts; - a `(termOfUnit K E)` map with `K` a `cx/` constant — the mint of a context — reconciles the pairs `K` is in, since a new context is what creates a sibling pair; - an `(R a b)` fact on a **declared sub-relation** reconciles the pairs whose ordered arguments are `a` below `b`, in the functions declared to order by `R`. A comparator dimension needs nothing but the contexts, but a dimension resolved by stored facts has the evidence arrive on its own schedule. Any other fact, including one stored into a `cx/` context that already exists, creates no pair and reconciles nothing. A no-op — one functor count — on a KB that declares no `contextArgSubrelation`. Returns true when an edge gained a justification, which the caller settles.
(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 nat/any-reified-constants?
first, so a KB with no reified constant pays no any-context-subrelations? read.
Returns true when an edge gained a justification, which the caller settles.
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 `nat/any-reified-constants?` first, so a KB with no reified constant pays no `any-context-subrelations?` read. Returns true when an edge gained a justification, which the caller settles.
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 |