The two tuple families. The self and converse family: a ground binary self tuple under
irreflexive, and a tuple and its stored converse under anti_symmetric. The
tuple-mark family: the determinants under functional and functionalInArg, the
anti_transitive chains, the asymmetric converse pairs and the tuples a negates
declaration sets against each other. Both find their nogoods
from a stored tuple's own arguments and share the converse pairs, and each nogood is
placed as a conclusion (chain/place-tuples!). See docs/nmtms.md, "A nogood placed as
a conclusion".
The two tuple families. The self and converse family: a ground binary self tuple under `irreflexive`, and a tuple and its stored converse under `anti_symmetric`. The tuple-mark family: the determinants under `functional` and `functionalInArg`, the `anti_transitive` chains, the `asymmetric` converse pairs and the tuples a `negates` declaration sets against each other. Both find their nogoods from a stored tuple's own arguments and share the converse pairs, and each nogood is placed as a conclusion (`chain/place-tuples!`). See docs/nmtms.md, "A nogood placed as a conclusion".
(binary-tuple sx)[a b] for a stored fact sx whose sentence is a ground positive binary tuple with a
symbol functor, else nil. checks asks it of a sentence about to be written, as
{:sentence s}.
`[a b]` for a stored fact `sx` whose sentence is a ground positive binary tuple with a
symbol functor, else nil. `checks` asks it of a sentence about to be written, as
`{:sentence s}`.The self and converse family's entry in decide/registry. Its self tuples are read
off the self-tuple trie (self-tuples-under). Recover offers the stored facts of the
predicates under an anti_symmetric or asymmetric mark to note-converse!, and
queues the self tuples under an irreflexive mark. Each nogood of it is placed as a
conclusion (chain/place-tuples!).
The marks are read unscoped: a candidate row is a superset over every reader
(decide/unscoped-closures).
The self and converse family's entry in `decide/registry`. Its self tuples are read off the self-tuple trie (`self-tuples-under`). Recover offers the stored facts of the predicates under an `anti_symmetric` or `asymmetric` mark to `note-converse!`, and queues the self tuples under an `irreflexive` mark. Each nogood of it is placed as a conclusion (`chain/place-tuples!`). The marks are read unscoped: a candidate row is a superset over every reader (`decide/unscoped-closures`).
(convicting tax prop fs)(convicting tax prop fs context)The predicates carrying prop at or above every functor of fs over the unscoped
closure, or with context over what a reader there sees (tax/props-over), in content
order.
The predicates carrying `prop` at or above every functor of `fs` over the unscoped closure, or with `context` over what a reader there sees (`tax/props-over`), in content order.
(exempt-at? kb c ms up hidden?)Does a reader with ancestor set up read no nogood over the handles ms: two live
members of one determinant of c whose fillers are symbols one class at the reader
(same-class-at?, hidden? naming the handles the reader does not believe or see, or
nil). False for any other set.
Does a reader with ancestor set `up` read no nogood over the handles `ms`: two live members of one determinant of `c` whose fillers are symbols one class at the reader (`same-class-at?`, `hidden?` naming the handles the reader does not believe or see, or nil). False for any other set.
(held? tax c)Does the candidate index c keep a member of a determinant, a chain or a converse
pair, or does the taxonomy tax hold an irreflexive mark, which a stored self tuple
can stand under?
Does the candidate index `c` keep a member of a determinant, a chain or a converse pair, or does the taxonomy `tax` hold an `irreflexive` mark, which a stored self tuple can stand under?
(kind-of kb c ms)The kind the tuple nogood over the member handles ms reports under, read off the
candidate index c and the marks over the members' functors in the unscoped taxonomy:
:irreflexive for a self tuple under an irreflexive mark, :anti-transitive for a
chain under an anti_transitive one, :functional for a determinant pair, :negates
for a negates set, and for a
converse pair :anti-symmetric under an anti_symmetric mark, else :asymmetric under
an asymmetric one; the first in keyword order when the set has two. nil when no mark
convicts a tuple nogood c keeps over ms.
The kind the tuple nogood over the member handles `ms` reports under, read off the candidate index `c` and the marks over the members' functors in the unscoped taxonomy: `:irreflexive` for a self tuple under an `irreflexive` mark, `:anti-transitive` for a chain under an `anti_transitive` one, `:functional` for a determinant pair, `:negates` for a `negates` set, and for a converse pair `:anti-symmetric` under an `anti_symmetric` mark, else `:asymmetric` under an `asymmetric` one; the first in keyword order when the set has two. nil when no mark convicts a tuple nogood `c` keeps over `ms`.
The tuple-mark family's entry in decide/registry. Liveness reads the genlCx
closure, so a moved generation syncs ::live (sync-tuples). Each nogood of it is
placed as a conclusion (chain/place-tuples!).
The marks are read unscoped: a candidate row is a superset over every reader
(decide/unscoped-closures).
The tuple-mark family's entry in `decide/registry`. Liveness reads the `genlCx` closure, so a moved generation syncs `::live` (`sync-tuples`). Each nogood of it is placed as a conclusion (`chain/place-tuples!`). The marks are read unscoped: a candidate row is a superset over every reader (`decide/unscoped-closures`).
(member? kb c h)Is h a member of a tuple nogood: a stored self tuple (self-tuple?), or a member of a
converse pair or a chain or a live determinant member the candidate index c keeps?
Is `h` a member of a tuple nogood: a stored self tuple (`self-tuple?`), or a member of a converse pair or a chain or a live determinant member the candidate index `c` keeps?
(members kb w c)Every member of a tuple nogood: the stored self tuples under an irreflexive mark
(self-tuples), and every member the candidate index c keeps. w is
decide/unscoped-closures's.
Every member of a tuple nogood: the stored self tuples under an `irreflexive` mark (`self-tuples`), and every member the candidate index `c` keeps. `w` is `decide/unscoped-closures`'s.
(members-under kb w c ps)The members of the tuple nogoods whose functor is at or below one of the predicates
ps over the unscoped genl closure (w, decide/unscoped-closures): those a mark on one of
ps, or a genl edge whose lower end is one of ps, can give or take a route. The
members c keeps are read off their records, or off the stored facts of each predicate
at or below ps, whichever is fewer; the self tuples under an irreflexive mark off
those facts (self-tuples-under).
The members of the tuple nogoods whose functor is at or below one of the predicates `ps` over the unscoped `genl` closure (`w`, `decide/unscoped-closures`): those a mark on one of `ps`, or a `genl` edge whose lower end is one of `ps`, can give or take a route. The members `c` keeps are read off their records, or off the stored facts of each predicate at or below `ps`, whichever is fewer; the self tuples under an `irreflexive` mark off those facts (`self-tuples-under`).
(merges? a b h-mono? o-mono?)Does a converse pair over a and b merge the two terms instead of forming a nogood:
two symbols, both members :monotonic (h-mono?, o-mono?, each monotonic-member?
of a stored member).
Does a converse pair over `a` and `b` merge the two terms instead of forming a nogood: two symbols, both members `:monotonic` (`h-mono?`, `o-mono?`, each `monotonic-member?` of a stored member).
(monotonic-member? tms h)Is h a :monotonic member of a collision, which a merge needs of every member
(docs/reference.md, decision 6)? Its class, or its premise strength while a network
defeat decided before a restrengthening holds it OUT: a :monotonic member is never a
loser, so the next settle releases it.
Is `h` a `:monotonic` member of a collision, which a merge needs of every member (docs/reference.md, decision 6)? Its class, or its premise strength while a network defeat decided before a restrengthening holds it OUT: a `:monotonic` member is never a loser, so the next settle releases it.
(moved? c)Has the index queued a member whose nogoods the settle places again (take-moved!)?
Has the index queued a member whose nogoods the settle places again (`take-moved!`)?
(nogoods-holding kb c hs)The tuple nogoods c keeps with a member among the handles hs, each {:members #{h} :specs #{spec}}, one per member set: [:self] for a self tuple, [:conv] for a
converse pair, [:chain] for a chain, [:neg] for a negates set, and [:det key]
for two live members of determinant key with distinct fillers. A spec names the shape; routes reads the
marks that convict it.
The tuple nogoods `c` keeps with a member among the handles `hs`, each `{:members #{h}
:specs #{spec}}`, one per member set: `[:self]` for a self tuple, `[:conv]` for a
converse pair, `[:chain]` for a chain, `[:neg]` for a `negates` set, and `[:det key]`
for two live members of determinant `key` with distinct fillers. A spec names the shape; `routes` reads the
marks that convict it.(offer! kb w sx only)Offer the stored fact sx to the converse and tuple-mark candidates again, or with
only :converse to the converse ones alone: a mark or a predicate genl edge
arriving over stored tuples makes candidates their store did not read
(decide/offer!).
Offer the stored fact `sx` to the converse and tuple-mark candidates again, or with `only` `:converse` to the converse ones alone: a mark or a predicate `genl` edge arriving over stored tuples makes candidates their store did not read (`decide/offer!`).
(owned? tax members core)Is the placed nogood over members with antecedents but the genlCx edges core one
this family places (chain/place-tuples!): a ground among core supports a tuple
mark's flat-cache key?
Is the placed nogood over `members` with antecedents but the `genlCx` edges `core` one this family places (`chain/place-tuples!`): a ground among `core` supports a tuple mark's flat-cache key?
(routes kb w c {:keys [members specs]})Each way a mark convicts the tuple nogood ng (nogoods-holding) over the unscoped
taxonomy, as {:keys #{k} :links [[sub super]]} (tax/separation-routes' shape): a
mark on a predicate P at or above every member's functor, its flat-cache key, and the
subsumption from each functor to P. A self tuple reads the irreflexive marks, a
chain the anti_transitive ones, and a converse pair the asymmetric ones and the
anti_symmetric ones unless it merges (merges?,
special/derive-antisymmetric-equalities), and a negates set the declarations over
its functors (negates-routes). A determinant pair reads the determinant's
own functional and functionalInArg marks; two symbol fillers both :monotonic merge
(special/derive-functional-equalities) and give no route. Two symbol fillers one class
at a reader form no nogood there, which the read reads (exempt-at?). w is
decide/unscoped-closures's.
Each way a mark convicts the tuple nogood `ng` (`nogoods-holding`) over the unscoped
taxonomy, as `{:keys #{k} :links [[sub super]]}` (`tax/separation-routes`' shape): a
mark on a predicate `P` at or above every member's functor, its flat-cache key, and the
subsumption from each functor to `P`. A self tuple reads the `irreflexive` marks, a
chain the `anti_transitive` ones, and a converse pair the `asymmetric` ones and the
`anti_symmetric` ones unless it merges (`merges?`,
`special/derive-antisymmetric-equalities`), and a `negates` set the declarations over
its functors (`negates-routes`). A determinant pair reads the determinant's
own `functional` and `functionalInArg` marks; two symbol fillers both `:monotonic` merge
(`special/derive-functional-equalities`) and give no route. Two symbol fillers one class
at a reader form no nogood there, which the read reads (`exempt-at?`). `w` is
`decide/unscoped-closures`'s.(self-tuple? sx)Is the stored fact sx a ground positive binary tuple (p a a) (binary-tuple)?
Is the stored fact `sx` a ground positive binary tuple `(p a a)` (`binary-tuple`)?
(self-tuples-in kb w ctxs)The stored self tuples under an irreflexive mark stated in a context of ctxs, which
a genlCx move exposing those contexts can give a placement (special/drain-context-moves!' :reach).
The marks are read unscoped: a candidate row is a superset over every reader
(decide/unscoped-closures).
The stored self tuples under an `irreflexive` mark stated in a context of `ctxs`, which a `genlCx` move exposing those contexts can give a placement (`special/drain-context-moves!`' `:reach`). The marks are read unscoped: a candidate row is a superset over every reader (`decide/unscoped-closures`).
(take-moved! kb)The members whose tuple nogoods moved since the last call, and the queue emptied
(noted).
The members whose tuple nogoods moved since the last call, and the queue emptied (`noted`).
(under-marks tax qs)The predicates of qs on or below a predicate carrying a mark a tuple nogood is
convicted through (a mark-kinds :props set, a functionalInArg or a negates
declaration) over the
unscoped closure: the subtypes of the marked predicates, or one walk up from each of
qs that enters no type an earlier walk found below no mark
(tax/genls-global-meets?), whichever reads fewer. A genl edge below no mark gives
no tuple nogood a route.
The predicates of `qs` on or below a predicate carrying a mark a tuple nogood is convicted through (a `mark-kinds` `:props` set, a `functionalInArg` or a `negates` declaration) over the unscoped closure: the subtypes of the marked predicates, or one walk up from each of `qs` that enters no type an earlier walk found below no mark (`tax/genls-global-meets?`), whichever reads fewer. A `genl` edge below no mark gives no tuple nogood a route.
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 |