The structural genlCx producer for reified-NAT contexts — docs/context-nat.md.
A (contextArgSubrelation F pos R) declaration says two F-contexts are ordered by the
sub-relation R at argument pos. Two F-contexts are ordered when they differ only
at declared positions and each differing argument of the sub is R-below the other's,
the product order. This namespace reads the declarations and the context NATs of F
from the store and materializes each such genlCx edge as a justified sentex in
CxUniverse, never a premise. R is resolved by a bounded oracle: a registered pure
comparator, else the genlCx closure for a sub-relation in closure-orders and each
believed stored (R a b) fact.
The structural genlCx producer for reified-NAT contexts — docs/context-nat.md. A `(contextArgSubrelation F pos R)` declaration says two `F`-contexts are ordered by the sub-relation `R` at argument `pos`. Two `F`-contexts are ordered when they differ only at declared positions and each differing argument of the sub is `R`-below the other's, the product order. This namespace reads the declarations and the context NATs of `F` from the store and **materializes** each such `genlCx` edge as a **justified** sentex in CxUniverse, never a premise. `R` is resolved by a bounded oracle: a registered pure comparator, else the `genlCx` closure for a sub-relation in `closure-orders` and each believed stored `(R a b)` fact.
(any-context-subrelations? kb)Presence check: does the KB declare any contextArgSubrelation? The producer is a no-op
otherwise — one O(1) functor count per assert, the shape res/any-corresponding-predicates?
has.
Presence check: does the KB declare any `contextArgSubrelation`? The producer is a no-op otherwise — one O(1) functor count per assert, the shape `res/any-corresponding-predicates?` has.
(reconcile-genlCx kb sentence moves)The structural-genlCx maintenance a just-asserted sentence and the belief moves of its
write (moves, reconcile-moves) call for: the arrival of sentence
(reconcile-arrival), a genlCx edge read with the moved edges once. 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` and the belief moves of its write (`moves`, `reconcile-moves`) call for: the arrival of `sentence` (`reconcile-arrival`), a `genlCx` edge read with the moved edges once. 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-moves kb {:keys [edges arrived derived] :as moves})The structural genlCx maintenance the belief moves moves call for, once the write that
moved them has settled. moves is what special/take-producer-moves! answers:
:edges, the genlCx edges the write's settles moved, each reconciled by
reconcile-edge-move; :arrived, handles revived, and :derived, handles derived by
functor, each read as an arrival when believed and of a functor declared-heads names.
Edges and sentences are read in content order. Local: the cost follows the moves and
the contexts they name, never the context-NAT population. Returns true when an edge
gained a justification, which the caller settles.
The structural genlCx maintenance the belief moves `moves` call for, once the write that moved them has settled. `moves` is what `special/take-producer-moves!` answers: `:edges`, the `genlCx` edges the write's settles moved, each reconciled by `reconcile-edge-move`; `:arrived`, handles revived, and `:derived`, handles derived by functor, each read as an arrival when believed and of a functor `declared-heads` names. Edges and sentences are read in content order. Local: the cost follows the moves and the contexts they name, never the context-NAT population. Returns true when an edge gained a justification, which the caller settles.
(reconcile-revivals kb moves removed)The structural genlCx maintenance a teardown owes once its belief has settled: the
belief moves of the teardown (moves, reconcile-moves), and the target of every
except or defeat among the removed sentences, whose belief or visibility the removal
gave back with no relabel. Behind nat/any-reified-constants?. Returns true when an edge
gained a justification, which the caller settles.
The structural genlCx maintenance a teardown owes once its belief has settled: the belief moves of the teardown (`moves`, `reconcile-moves`), and the target of every `except` or `defeat` among the `removed` sentences, whose belief or visibility the removal gave back with no relabel. Behind `nat/any-reified-constants?`. 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 |