The nogood candidate index. Each family keeps its rows of one candidate index
(:nogood-candidates), which the placement detectors read; this namespace runs the
families as one index, holds the forced-monotonic set, and decides a placed nogood
from its members' classes (verdict). See docs/nmtms.md, "A nogood placed as a
conclusion".
The nogood candidate index. Each family keeps its rows of one candidate index (`:nogood-candidates`), which the placement detectors read; this namespace runs the families as one index, holds the forced-monotonic set, and decides a placed nogood from its members' classes (`verdict`). See docs/nmtms.md, "A nogood placed as a conclusion".
The baseline forced-monotonic set, {kind #{predicate …}}: every family's :grounds and every
held-members member, held on every KB whether or not it is stated.
The baseline forced-monotonic set, `{kind #{predicate …}}`: every family's `:grounds` and every
`held-members` member, held on every KB whether or not it is stated.(candidate-handles kb)Every handle some reader can read as a nogood member of a family.
Every handle some reader can read as a nogood member of a family.
(candidate? kb c h)Is h among candidate-handles of the candidate index c of kb?
Is `h` among `candidate-handles` of the candidate index `c` of `kb`?
(declared tax){[kind pred] {handle context}}: every predicate a believed declaration makes
forced-monotonic and the baseline set does not hold (global?), with its declarations. Empty on a
KB that declares only baseline members. Read KB-wide, the union over every reader,
which a read walk splits into the declarations its reader sees and misses.
`{[kind pred] {handle context}}`: every predicate a believed declaration makes
forced-monotonic and the baseline set does not hold (`global?`), with its declarations. Empty on a
KB that declares only baseline members. Read KB-wide, the union over every reader,
which a read walk splits into the declarations its reader sees and misses.(drop-memos)Empty sync-memo, and return nil. It is process-wide and holds the taxonomy value of
the last KB read, which holds references into that KB, so it keeps its records and index
reachable until another KB is read; vaelii.core/close! calls this last. A KB still
open recomputes its entry on its next read.
Empty `sync-memo`, and return nil. It is process-wide and holds the taxonomy value of the last KB read, which holds references into that KB, so it keeps its records and index reachable until another KB is read; `vaelii.core/close!` calls this last. A KB still open recomputes its entry on its next read.
(exempt-at? kb ms up hidden?)Does a reader with ancestor set up read no conviction of the placed nogood over the
member handles ms: a membership nogood whose separation a siblingDisjointException
it sees removes (membership/exempt-at?), a contradicted orthogonal whose separation
such an exception removes (related/exempt-at?),
or a determinant pair whose fillers it reads as one class (tuple/exempt-at?).
hidden? names the handles the reader does not believe or see, or is nil. False for
any other nogood.
Does a reader with ancestor set `up` read no conviction of the placed nogood over the member handles `ms`: a membership nogood whose separation a `siblingDisjointException` it sees removes (`membership/exempt-at?`), a contradicted `orthogonal` whose separation such an exception removes (`related/exempt-at?`), or a determinant pair whose fillers it reads as one class (`tuple/exempt-at?`). `hidden?` names the handles the reader does not believe or see, or is nil. False for any other nogood.
The two forced-monotonic properties.
The two forced-monotonic properties.
(forced-literal? tax literal)(forced-literal? _tax literal on?)Is literal in the forced-monotonic set: its functor is forced-monotonic? as
:forced-monotonic, or as :forced-between-predicates over a literal
nm/between-predicates?. The 2-arity reads the union over every reader; the
3-arity reads the forced-monotonic reading on? (global-reading, reader-reading).
Is `literal` in the forced-monotonic set: its functor is `forced-monotonic?` as `:forced-monotonic`, or as `:forced-between-predicates` over a literal `nm/between-predicates?`. The 2-arity reads the union over every reader; the 3-arity reads the forced-monotonic reading `on?` (`global-reading`, `reader-reading`).
(forced-monotonic? tax kind pred)(forced-monotonic? tax kind pred seen?)Does pred carry the forced-monotonic property kind (:forced-monotonic or
:forced-between-predicates). The 3-arity is the union over every reader: global?,
or a believed declaration in any context. The 4-arity is one reader's: global?, or
a declaration [handle context] seen? holds of.
Does `pred` carry the forced-monotonic property `kind` (`:forced-monotonic` or `:forced-between-predicates`). The 3-arity is the union over every reader: `global?`, or a believed declaration in any context. The 4-arity is one reader's: `global?`, or a declaration `[handle context]` `seen?` holds of.
(forced-predicates tax kind)Every predicate forced-monotonic? as kind, over every reader.
Every predicate `forced-monotonic?` as `kind`, over every reader.
(global-reading tax)The forced-monotonic reading (fn [kind pred]) every reader shares (global?).
The forced-monotonic reading `(fn [kind pred])` every reader shares (`global?`).
(global? _tax kind pred)Is pred in the baseline forced-monotonic set as kind: a baseline-forced member.
Every reader reads it forced-monotonic, and no declaration moves it. A declaration in
any context, CxUniverse's included, makes its predicate forced-monotonic at the readers
that believe it (forced-monotonic?, docs/nmtms.md, "The forced-monotonic set").
Is `pred` in the baseline forced-monotonic set as `kind`: a `baseline-forced` member. Every reader reads it forced-monotonic, and no declaration moves it. A declaration in any context, CxUniverse's included, makes its predicate forced-monotonic at the readers that believe it (`forced-monotonic?`, docs/nmtms.md, "The forced-monotonic set").
(handles-at c up)The candidates of c, as synced answers it, stated in a context of the ancestor set
up or in none: every handle a reader with ancestor set up can read as a nogood
member, which a genlCx edge's placement pass reads
(special/drain-context-moves!).
The candidates of `c`, as `synced` answers it, stated in a context of the ancestor set `up` or in none: every handle a reader with ancestor set `up` can read as a nogood member, which a `genlCx` edge's placement pass reads (`special/drain-context-moves!`).
The forced-monotonic predicates no family reads among its grounds, each with the reason it is forced-monotonic (docs/nmtms.md, "The forced-monotonic set").
The forced-monotonic predicates no family reads among its grounds, each with the reason it is forced-monotonic (docs/nmtms.md, "The forced-monotonic set").
(literal-declarations tax literal){handle context} of the stored declarations that make literal forced-monotonic and
are not global?: empty when the baseline set holds literal or no declaration
does.
`{handle context}` of the stored declarations that make `literal` forced-monotonic and
are not `global?`: empty when the baseline set holds `literal` or no declaration
does.(moves kb since)[c pos moved]: the candidate index as synced answers it, its journal position, and
the handles journaled since the position since (journal/since), which hold every
handle that entered or left the candidates since; nil when the journal does not reach
back to since, and a reader reads the index whole.
`[c pos moved]`: the candidate index as `synced` answers it, its journal position, and the handles journaled since the position `since` (`journal/since`), which hold every handle that entered or left the candidates since; nil when the journal does not reach back to `since`, and a reader reads the index whole.
(note-candidate! kb sx stored?)Keep :nogood-candidates in step with the fact sx arriving (stored? true) or
leaving. Runs at the store primitive and the removal choke point, after the index
write.
Keep `:nogood-candidates` in step with the fact `sx` arriving (`stored?` true) or leaving. Runs at the store primitive and the removal choke point, after the index write.
(offer! kb sxs)(offer! kb sxs only)Offer the stored facts sxs to the tuple candidates again (tuple/offer!), with
only :converse to the converse candidates alone.
Offer the stored facts `sxs` to the tuple candidates again (`tuple/offer!`), with `only` `:converse` to the converse candidates alone.
(placed-kind kb ms)The kind a nogood over the member handles ms placed as a conclusion reports under,
read off the members' sentences: :negation for a B beside (not B), the membership
family's kind (membership/kind-of), the related-types family's (related/kind-of),
the tuple families' (tuple/kind-of), the arity family's (arity/kind-of),
:inherited for a set the inherited detector found (inherited/inherited-clashes), or
nil for any other set.
The kind a nogood over the member handles `ms` placed as a conclusion reports under, read off the members' sentences: `:negation` for a `B` beside `(not B)`, the membership family's kind (`membership/kind-of`), the related-types family's (`related/kind-of`), the tuple families' (`tuple/kind-of`), the arity family's (`arity/kind-of`), `:inherited` for a set the inherited detector found (`inherited/inherited-clashes`), or nil for any other set.
(placements-owed? c)Is every placement owed: no placement pass has read the edge cursor since the
candidate index c was emptied (rebuild-candidates!, take-edge-cursor!)?
Is every placement owed: no placement pass has read the edge cursor since the candidate index `c` was emptied (`rebuild-candidates!`, `take-edge-cursor!`)?
(reader-reading tax seen?)The forced-monotonic reading (fn [kind pred]) of a reader that sees the declarations [handle context] seen? holds of (forced-monotonic?, 4-arity).
The forced-monotonic reading `(fn [kind pred])` of a reader that sees the declarations `[handle context]` `seen?` holds of (`forced-monotonic?`, 4-arity).
(rebuild-candidates! kb)Recompute :nogood-candidates from storage, for recover: each family computes its
rows off the store (:recovered), and no record is read for a family that stores no
fact it reads.
Recompute `:nogood-candidates` from storage, for `recover`: each family computes its rows off the store (`:recovered`), and no record is read for a family that stores no fact it reads.
Every family, each a map of the parts the candidate index runs, w an unscoped-closures map:
:grounds, {kind #{functor}}: the forced-monotonic literals the family reads as
stored grounds rather than as members, under the declaration kind that reads them
(:forced-between-predicates for a functor read only between predicate-spelled
arguments). Absent for a family that reads none.:note! (fn [kb w sx stored?]), at the store and removal choke points; absent for
a family the settle installs.:recovered (fn [kb w]): writes the rows the family computes off the store once
recover has emptied the index.:synced? (fn [tax c]) and :sync (fn [kb w c] c): rows derived from the
taxonomy, read again when it moved.:handles (fn [kb c]), every handle some reader can read as a member; :holds?
(fn [kb c h]) answers whether h is among them with a few map reads, or off the
index for a member the family reads there (the related-types family's cover pairs). Every update that
can move a handle into or out of it journals it (journal/note). Absent for the
negation family, whose members are an index family (reads/as-stored-opposed-in).
Every family places its nogoods as conclusions (chain/place-nogoods!).Every family, each a map of the parts the candidate index runs, `w` an `unscoped-closures` map:
* `:grounds`, `{kind #{functor}}`: the forced-monotonic literals the family reads as
stored grounds rather than as members, under the declaration kind that reads them
(`:forced-between-predicates` for a functor read only between predicate-spelled
arguments). Absent for a family that reads none.
* `:note!` `(fn [kb w sx stored?])`, at the store and removal choke points; absent for
a family the settle installs.
* `:recovered` `(fn [kb w])`: writes the rows the family computes off the store once
recover has emptied the index.
* `:synced?` `(fn [tax c])` and `:sync` `(fn [kb w c] c)`: rows derived from the
taxonomy, read again when it moved.
* `:handles` `(fn [kb c])`, every handle some reader can read as a member; `:holds?`
`(fn [kb c h])` answers whether `h` is among them with a few map reads, or off the
index for a member the family reads there (the related-types family's cover pairs). Every update that
can move a handle into or out of it journals it (`journal/note`). Absent for the
negation family, whose members are an index family (`reads/as-stored-opposed-in`).
Every family places its nogoods as conclusions (`chain/place-nogoods!`).(synced kb)The candidate index after each family's rows derived from the taxonomy are read again
where it moved (:synced?, :sync), and its candidates by the context they are stated
in read again off the journal (journal/indexed, read by handles-at).
The candidate index after each family's rows derived from the taxonomy are read again where it moved (`:synced?`, `:sync`), and its candidates by the context they are stated in read again off the journal (`journal/indexed`, read by `handles-at`).
(take-edge-cursor! kb)[since first?]: the genlCx generation the last call read when it has moved since,
else nil, so tax/moves-since reads the edges moved after it; and
first?, true when no call has read it since the candidate index was emptied
(rebuild-candidates!), so every placement may be owed. The settle's drain reads it
once a pass (special/drain-context-moves!).
`[since first?]`: the `genlCx` generation the last call read when it has moved since, else nil, so `tax/moves-since` reads the edges moved after it; and `first?`, true when no call has read it since the candidate index was emptied (`rebuild-candidates!`), so every placement may be owed. The settle's drain reads it once a pass (`special/drain-context-moves!`).
(unscoped-closures tax)The unscoped closures of tax, under their tax/…-global names, and tax itself as
:tax: the taxonomy a family keeps its rows through, handed to :note!, :recovered
and :sync. The rows are a superset over every reader, kept where no reader exists,
and each reader scopes what it reads.
The unscoped closures of `tax`, under their `tax/…-global` names, and `tax` itself as `:tax`: the taxonomy a family keeps its rows through, handed to `:note!`, `:recovered` and `:sync`. The rows are a superset over every reader, kept where no reader exists, and each reader scopes what it reads.
(verdict class-of forced? sentence-of members)The verdict on nogood members from class-of (handle -> defeat-class) and
forced? (handle -> boolean, is the member a forced-monotonic literal): {:defeat h}
for a unique weakest defeasible member that is not forced-monotonic, :dilemma for a
defeasible minimum two such members share, and :hard when no member outside the
forced-monotonic set is defeasible. A forced-monotonic member is never a loser, whatever
its class (docs/reference.md, item 7 of "The function"). sentence-of (handle -> sentence) reads each member's sentence: a member that is the denial (not S) of a
forced-monotonic member S, when it is the only such member, is the loser at any class
(docs/nmtms.md, "The forced-monotonic set").
The verdict on nogood `members` from `class-of` (`handle -> defeat-class`) and
`forced?` (`handle -> boolean`, is the member a forced-monotonic literal): `{:defeat h}`
for a unique weakest defeasible member that is not forced-monotonic, `:dilemma` for a
defeasible minimum two such members share, and `:hard` when no member outside the
forced-monotonic set is defeasible. A forced-monotonic member is never a loser, whatever
its class (docs/reference.md, item 7 of "The function"). `sentence-of` (`handle ->
sentence`) reads each member's sentence: a member that is the denial `(not S)` of a
forced-monotonic member `S`, when it is the only such member, is the loser at any class
(docs/nmtms.md, "The forced-monotonic set").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 |