The membership families: two memberships of one term whose types a separation holds
apart (disjoint), a membership beside a denial of a supertype of its type
(supertype), and a membership under a cover's whole beside a denial of each part
(covering), placed as nogoods (chain/place-memberships!). See docs/nmtms.md, "A
nogood placed as a conclusion".
The membership families: two memberships of one term whose types a separation holds apart (`disjoint`), a membership beside a denial of a supertype of its type (`supertype`), and a membership under a cover's whole beside a denial of each part (`covering`), placed as nogoods (`chain/place-memberships!`). See docs/nmtms.md, "A nogood placed as a conclusion".
(exempt-at? tax recs members up)Does a reader with ancestor set up read no separation of the membership nogood
members while the KB stores a siblingDisjointException: two memberships of one term
whose types tax/disjoint? over up does not separate, or two or more memberships of
one term refuting a cover through a separation the reader reads no cover refutation of
(cover-convicted-at?). An exception the reader sees removes a separation its
placement reads, the one read below a placement that seeing more takes away
(docs/taxonomy.md). False for any other nogood.
Does a reader with ancestor set `up` read no separation of the membership nogood `members` while the KB stores a `siblingDisjointException`: two memberships of one term whose types `tax/disjoint?` over `up` does not separate, or two or more memberships of one term refuting a cover through a separation the reader reads no cover refutation of (`cover-convicted-at?`). An exception the reader sees removes a separation its placement reads, the one read below a placement that seeing more takes away (docs/taxonomy.md). False for any other nogood.
The membership family's entry in decide/registry. Recover keeps the entries of the
terms recovered-terms names that held? holds, with no separation read: the first
read after it tests every pair once (sync-memberships).
The membership family's entry in `decide/registry`. Recover keeps the entries of the terms `recovered-terms` names that `held?` holds, with no separation read: the first read after it tests every pair once (`sync-memberships`).
(kind-of w recs ms)The kind of the membership nogood over the member handles ms, read off their
sentences and the unscoped genl closure in w (decide/unscoped-closures):
:disjoint for two memberships of one term in distinct types a declaration separates
(tax/pair-separated?), :supertype for one membership of a term beside one denial of
a strict supertype of its type, :cover for any other membership of a term beside
denials of it and for two or more memberships of a term in distinct types (a cover
refuted through a separation's denial), else nil.
The kind of the membership nogood over the member handles `ms`, read off their sentences and the unscoped `genl` closure in `w` (`decide/unscoped-closures`): `:disjoint` for two memberships of one term in distinct types a declaration separates (`tax/pair-separated?`), `:supertype` for one membership of a term beside one denial of a strict supertype of its type, `:cover` for any other membership of a term beside denials of it and for two or more memberships of a term in distinct types (a cover refuted through a separation's denial), else nil.
(moved? c)Has the index queued a term whose nogoods the settle places again, or the lower end of a
genl edge they are read against (take-moved!, take-edge-moved!)?
Has the index queued a term whose nogoods the settle places again, or the lower end of a `genl` edge they are read against (`take-moved!`, `take-edge-moved!`)?
(nogoods-of c x)Term x's nogoods under the candidate index c, each {:members #{h} :kind k}.
Term `x`'s nogoods under the candidate index `c`, each `{:members #{h} :kind k}`.
(nogoods-terms c)The kept terms holding a nogood under the candidate index c.
The kept terms holding a nogood under the candidate index `c`.
(reaches-lows? w recs under? {:keys [members]})Can a genl edge with its lower end at a type under? (under-lows) holds of move the
routes or the placements of the nogood ng (routes, chain/route-placements): is a
type of its members, or a part of a cover over a whole above a held type, one of them?
Every route and link of ng reads only the upward closures of those types and of the
types above them, and a path through an edge starts at or below its lower end, so an
edge move changes no route, link witness or placement of a nogood this answers false
of. True when the members are not one term's.
Can a `genl` edge with its lower end at a type `under?` (`under-lows`) holds of move the routes or the placements of the nogood `ng` (`routes`, `chain/route-placements`): is a type of its members, or a part of a cover over a whole above a held type, one of them? Every route and link of `ng` reads only the upward closures of those types and of the types above them, and a path through an edge starts at or below its lower end, so an edge move changes no route, link witness or placement of a nogood this answers false of. True when the members are not one term's.
(routes w recs {:keys [members kind]})Each way the declarations convict the membership nogood ng, over the unscoped closures
w (decide/unscoped-closures): {:keys #{k} :links [[sub super]] :pair [x y]}, the
flat-cache keys read, the genl subsumptions climbed and the separated pair, as
tax/separation-routes answers for a :disjoint one. A :cover one takes
cover-routes, and so does a :disjoint one's pair of memberships, since term-nogoods
keeps a cover they refute as the one nogood. A :supertype one takes the subsumption
from the held type to the denied type with no key, a :strict-links too, since a
:default edge does not contrapose, and each cover route. A link that climbs from a
held type to the type the nogood reads it in is a :climbs, and a :strict-links, of
its route (docs/inference.md, "An edge's reading"). Empty when the members are not one term's. A route is a superset over
every reader, and the placement decides which contexts see it.
Each way the declarations convict the membership nogood `ng`, over the unscoped closures
`w` (`decide/unscoped-closures`): `{:keys #{k} :links [[sub super]] :pair [x y]}`, the
flat-cache keys read, the `genl` subsumptions climbed and the separated pair, as
`tax/separation-routes` answers for a `:disjoint` one. A `:cover` one takes
`cover-routes`, and so does a `:disjoint` one's pair of memberships, since `term-nogoods`
keeps a cover they refute as the one nogood. A `:supertype` one takes the subsumption
from the held type to the denied type with no key, a `:strict-links` too, since a
`:default` edge does not contrapose, and each cover route. A link that climbs from a
held type to the type the nogood reads it in is a `:climbs`, and a `:strict-links`, of
its route (docs/inference.md, "An edge's reading"). Empty when the members are not one term's. A route is a superset over
every reader, and the placement decides which contexts see it.(take-edge-moved! kb){:terms #{x} :lows #{t}}, the terms queued since the last call because a genl edge
moved with their nogoods unmoved, and the lower ends of the edges moved, with both
emptied (place-term, sync-memberships). Such a term's nogoods need placing again
only where reaches-lows? holds.
`{:terms #{x} :lows #{t}}`, the terms queued since the last call because a `genl` edge
moved with their nogoods unmoved, and the lower ends of the edges moved, with both
emptied (`place-term`, `sync-memberships`). Such a term's nogoods need placing again
only where `reaches-lows?` holds.(take-moved! kb)The queues since the last call, emptied, as {:terms {x #{h}} :members {x #{h}}}.
:members holds each term whose nogoods moved, with the members of its nogoods before
and after the move (place-term). :terms adds each term of a placement that left,
with the placement's members (note-placement-left!).
The queues since the last call, emptied, as `{:terms {x #{h}} :members {x #{h}}}`.
`:members` holds each term whose nogoods moved, with the members of its nogoods before
and after the move (`place-term`). `:terms` adds each term of a placement that left,
with the placement's members (`note-placement-left!`).(terms-of kb c hs)The terms of the memberships and denials among the handles hs that the candidate
index c keeps.
The terms of the memberships and denials among the handles `hs` that the candidate index `c` keeps.
(terms-under kb w c ends)The kept terms with a nogood (::ngs) holding a type at or below one of the types
ends over the unscoped genl closure (w, decide/unscoped-closures), in a membership or a
denial (listed-under): those whose nogoods a separation over ends arriving can give
a route.
The kept terms with a nogood (`::ngs`) holding a type at or below one of the types `ends` over the unscoped `genl` closure (`w`, `decide/unscoped-closures`), in a membership or a denial (`listed-under`): those whose nogoods a separation over `ends` arriving can give a route.
(terms-under-edges kb w c lows)The kept terms with a nogood whose routes climb a genl edge with its lower end at one
of the types lows: those holding a type at or below one of them, and those holding a
type at or below the whole of a cover with a part at or below one
(cover-wholes-under). An edge's defeat class moving moves which placements a cover
refuted through a separation's denial reads (chain/route-placements), with no
membership and no declaration moving.
The kept terms with a nogood whose routes climb a `genl` edge with its lower end at one of the types `lows`: those holding a type at or below one of them, and those holding a type at or below the whole of a cover with a part at or below one (`cover-wholes-under`). An edge's defeat class moving moves which placements a cover refuted through a separation's denial reads (`chain/route-placements`), with no membership and no declaration moving.
(under-lows w lows)(fn [t]): is the type t at or below one of the types lows over the unscoped closure
in w (decide/unscoped-closures)? Each type's answer is held for the life of the fn,
which reads one still taxonomy.
`(fn [t])`: is the type `t` at or below one of the types `lows` over the unscoped closure in `w` (`decide/unscoped-closures`)? Each type's answer is held for the life of the fn, which reads one still taxonomy.
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 |