The definitional checks — arg argument types, disjointness, functionality — plus ground-ness and the stratification glue over the rule index.
Second layer of the engine stack (kb <- checks <- special <- integrate <- chain
<- settle):
every check reads the KB (taxonomy, index, believed matches) and returns a value
or throws — nothing here writes. Both mutation paths consume these: assert
(vaelii.core) throws the value, the derivation path (vaelii.impl.chain) records
it in the violations ledger.
The definitional checks — arg argument types, disjointness, functionality — plus ground-ness and the stratification glue over the rule index. Second layer of the engine stack (kb <- checks <- special <- integrate <- chain <- settle): every check reads the KB (taxonomy, index, believed matches) and returns a value or throws — nothing here writes. Both mutation paths consume these: `assert` (vaelii.core) throws the value, the derivation path (vaelii.impl.chain) records it in the violations ledger.
Is the sentence being checked one the entry point will reify before storing it?
True while vaelii.core/check reads a fact the way assert would store it, and while
the forward chainer asks whether a conclusion naming an application with no constant
yet is admissible before it mints one (chain/reify-conclusion). assert mints
every ground application of a reifiable function to a constant before its checks run,
so an argument that is such an application is read there as that constant; neither
of the two callers has minted it yet, and under this binding the argument arm reads
the application as the constant would be read (minted-application-clash). False
everywhere else, where every reifiable application has already been replaced by its
constant.
Is the sentence being checked one the entry point will reify before storing it? True while `vaelii.core/check` reads a fact the way `assert` would store it, and while the forward chainer asks whether a conclusion naming an application with no constant yet is admissible before it mints one (`chain/reify-conclusion`). `assert` mints every ground application of a reifiable function to a constant before its checks run, so an argument that is such an application is read there as that constant; neither of the two callers has minted it yet, and under this binding the argument arm reads the application as the constant would be read (`minted-application-clash`). False everywhere else, where every reifiable application has already been replaced by its constant.
A volatile map bound by a pass that decides many convictions (refresh-argument-holds!,
held-argument-entries), holding what the pass reads once: each predicate's
declarations per context (literal-reader), the declaring super-predicates' memos
(declaration-reader), the reads no value enters (value-outside?), the reads
clash-possible? makes over every context, and the candidate tests and reads every
declaration shares (held-demand-test, declaration-candidates). The pass
gathers every candidate before it writes a hold. Nil reads them afresh and asks no
clash-possible?.
A volatile map bound by a pass that decides many convictions (`refresh-argument-holds!`, `held-argument-entries`), holding what the pass reads once: each predicate's declarations per context (`literal-reader`), the declaring super-predicates' memos (`declaration-reader`), the reads no value enters (`value-outside?`), the reads `clash-possible?` makes over every context, and the candidate tests and reads every declaration shares (`held-demand-test`, `declaration-candidates`). The pass gathers every candidate before it writes a hold. Nil reads them afresh and asks no `clash-possible?`.
Does a minted type give way to a more specific one the KB believes? With this on,
(animal Fred) minted off (parentOf Fred Mary) is withheld while (dog Fred) is
believed and comes back when it goes, which takes about a tenth of the records out of a
shipped load and changes no answer. On by default (docs/argtypes.md).
binding it is the ordinary way in, and VAELII_PRUNE_SUBSUMED_MINTS=0 sets the root
value off — the parity run that says pruning removes records rather than answers.
Does a minted type give way to a more specific one the KB believes? With this on, `(animal Fred)` minted off `(parentOf Fred Mary)` is withheld while `(dog Fred)` is believed and comes back when it goes, which takes about a tenth of the records out of a shipped load and changes no answer. On by default (docs/argtypes.md). `binding` it is the ordinary way in, and `VAELII_PRUNE_SUBSUMED_MINTS=0` sets the root value off — the parity run that says pruning removes records rather than answers.
Does the write entry point refuse an arbitrable clash as well? False by default, where
refuses-assert? decides. vaelii.core/try-assert binds it true, and
constraint-checks then refuses every violation the sentence or one of its
argument-type mints forms (docs/api.md, "Refusing a clash").
Does the write entry point refuse an arbitrable clash as well? False by default, where `refuses-assert?` decides. `vaelii.core/try-assert` binds it true, and `constraint-checks` then refuses every violation the sentence or one of its argument-type mints forms (docs/api.md, "Refusing a clash").
True reads every genlCx move whole, as before the moves were split by what each
reader gains (tax/context-move's :gains): the settle's merge and argument-type
sweeps (special/move-groups), its mint withdrawal, and the argument holds
(gained-ends-candidates) over every reader under a moved edge. The reference
genlcx_move_gain_test holds the split against.
True reads every `genlCx` move whole, as before the moves were split by what each reader gains (`tax/context-move`'s `:gains`): the settle's merge and argument-type sweeps (`special/move-groups`), its mint withdrawal, and the argument holds (`gained-ends-candidates`) over every reader under a moved edge. The reference `genlcx_move_gain_test` holds the split against.
(antisymmetric-converses kb sentence context)The believed [handle via] pairs whose sentence is the converse of (P a b) under an
(anti_symmetric P) mark: the facts (P b a) that, with the sentence, force (equals a b). Deduped on the converse's handle. via is the marked predicate the conviction reads
through, which the equality derivation names in its justification.
The converse is probed at the marked predicate and the mark is read up the hierarchy, as in
asymmetry-problems. matches-visible over the ground converse is the whole probe: it
fans down to sub-predicate spellings and folds a comparison predicate's converse, so no
exact-sentence filter applies. Ground binary sentences only.
The believed `[handle via]` pairs whose sentence is the converse of `(P a b)` under an `(anti_symmetric P)` mark: the facts `(P b a)` that, with the sentence, force `(equals a b)`. Deduped on the converse's handle. `via` is the marked predicate the conviction reads through, which the equality derivation names in its justification. The converse is probed at the marked predicate and the mark is read up the hierarchy, as in `asymmetry-problems`. `matches-visible` over the ground converse is the whole probe: it fans down to sub-predicate spellings and folds a comparison predicate's converse, so no exact-sentence filter applies. Ground binary sentences only.
The definitional violations that name other believed sentexes rather than a
malformed sentence, so settle can arbitrate them like any other contradiction.
The definitional violations that name **other believed sentexes** rather than a malformed sentence, so `settle` can arbitrate them like any other contradiction.
(arbitrable? v)Can settle arbitrate this violation instead of the caller refusing it — does it
name opposing believed sentexes to form a nogood with?
Can `settle` arbitrate this violation instead of the caller refusing it — does it name opposing believed sentexes to form a nogood with?
(arg-position-violation kb sentence context)(arg-position-violation kb sentence _context types)The :arg-position violation the stored declaration sentence commits in
context, or nil — a constraint on a position its predicate does not have
(position-problem, through checked-sentence as at the entry point). The reader is
vaelii.impl.integrity's stranded-declarations: a stranded declaration constrains
nothing and mints nothing, so it is a sweep question rather than a settle one
(docs/taxonomy.md).
The `:arg-position` violation the **stored declaration** `sentence` commits in `context`, or nil — a constraint on a position its predicate does not have (`position-problem`, through `checked-sentence` as at the entry point). The reader is `vaelii.impl.integrity`'s `stranded-declarations`: a stranded declaration constrains nothing and mints nothing, so it is a sweep question rather than a settle one (docs/taxonomy.md).
(argument-conviction kb sx)The argument conviction assert holds the stored sentex sx inert under, as a
violation value, or nil. For a fact, the first violation of argument-problem's arms
and then args-quoted-problem that held-inert? accepts, read from sx's own context
as constraint-checks reads a written fact. For a rule, rule-conviction. Nil for a
denial.
The argument conviction `assert` holds the stored sentex `sx` inert under, as a violation value, or nil. For a fact, the first violation of `argument-problem`'s arms and then `args-quoted-problem` that `held-inert?` accepts, read from `sx`'s own context as `constraint-checks` reads a written fact. For a rule, `rule-conviction`. Nil for a denial.
(arity-binding-clause pred via n)How a message says what length binds a predicate: is declared with 2 arguments for one carrying its own declaration, takes 2 arguments through parentOf for one whose length descends from a super-predicate.
Public and spelled once: arg-position-problem words a declaration naming a position
the length denies with it, and a caller describing a binding reads the same clause.
"is declared with" is false of a predicate that declared nothing and took its length
off a super, so the split is a claim about the KB rather than a phrasing.
How a message says what length binds a predicate: **is declared with 2 arguments** for one carrying its own declaration, **takes 2 arguments through parentOf** for one whose length descends from a super-predicate. Public and spelled once: `arg-position-problem` words a declaration naming a position the length denies with it, and a caller describing a binding reads the same clause. "is declared with" is false of a predicate that declared nothing and took its length off a super, so the split is a claim about the KB rather than a phrasing.
(check-application-inputs kb sentence context)Throw the first violation of a function's argument declarations inside sentence in
context — application-input-problem, asked of a fact before the reify pass.
assert mints every ground reifiable application into its constant before
constraint-checks runs, and the constant carries the function's result types, not
what the application was given: the inputs are gone by the time the arm that reads
them could look. So the assert path asks this first, over the sentence as written,
from the writer's vantage — the same reading constraint-checks gives an unreifiable
application after the pass, and the one check gives both, since check does not
mint. Asked before the mint, a refused sentence leaves no constant behind.
Nil for a sentence with no compound argument, before any reader is built.
Throw the first violation of a function's argument declarations inside `sentence` in `context` — `application-input-problem`, asked of a fact **before** the reify pass. `assert` mints every ground reifiable application into its constant before `constraint-checks` runs, and the constant carries the function's result types, not what the application was given: the inputs are gone by the time the arm that reads them could look. So the assert path asks this first, over the sentence as written, from the writer's vantage — the same reading `constraint-checks` gives an unreifiable application after the pass, and the one `check` gives both, since `check` does not mint. Asked before the mint, a refused sentence leaves no constant behind. Nil for a sentence with no compound argument, before any reader is built.
(check-closed-extent-stratified kb sentence context)Throw :not-stratified unless declaring (closed_extent_predicate P),
(closedExtentForArg P n v) or a binary spelling of the second leaves the rule set
stratified; nil for any other sentence. The walk starts at each stored rule the grant
governs (provers/closed-extent-rules: a closed (not (P …)) antecedent, or one inside
an unknown antecedent, an aggregate body or an exceptWhen query), in content
order, so two rules that each close a cycle give one refusal. It runs before anything
is written (docs/naf.md, "Stratification, from both arrival orders").
Throw `:not-stratified` unless declaring `(closed_extent_predicate P)`, `(closedExtentForArg P n v)` or a binary spelling of the second leaves the rule set stratified; nil for any other sentence. The walk starts at each stored rule the grant governs (`provers/closed-extent-rules`: a closed `(not (P …))` antecedent, or one inside an `unknown` antecedent, an aggregate body or an `exceptWhen` query), in content order, so two rules that each close a cycle give one refusal. It runs before anything is written (docs/naf.md, "Stratification, from both arrival orders").
(check-edge-stratified kb sentence context)Throw unless adding this taxonomy edge leaves the stored rule set stratified.
The genl assert is the operation at fault, so refusing the edge is the
consistent answer: it is what wff already does to an edge that would make the
taxonomy cyclic, and it keeps the invariant that stored state is always stratified
— which is what lets check-stratified look only for cycles through the rule being
added. Runs before the sentex is created and before the taxonomy is touched.
Throw unless adding this taxonomy edge leaves the stored rule set stratified. The `genl` assert is the operation at fault, so refusing the *edge* is the consistent answer: it is what `wff` already does to an edge that would make the taxonomy cyclic, and it keeps the invariant that stored state is always stratified — which is what lets `check-stratified` look only for cycles through the rule being added. Runs before the sentex is created and before the taxonomy is touched.
(check-encodable sentence)Reject a sentence carrying a value a stored sentence may not carry
(first-unstorable). An unserializable value stores in the in-memory backend and throws
at the first on-disk write, so refusing it makes the backends agree. A map or a set has no
canonical form and no content order, so it is refused and not canonicalized. Both throw
:not-encodable, carrying the offending value under :value.
Reject a sentence carrying a value a stored sentence may not carry (`first-unstorable`). An unserializable value stores in the in-memory backend and throws at the first on-disk write, so refusing it makes the backends agree. A map or a set has no canonical form and no content order, so it is refused and not canonicalized. Both throw `:not-encodable`, carrying the offending value under `:value`.
(check-except-target kb sentence)Refuse a visibility (except (sentexHandle H)) when no sentex is stored under H
(:unknown-handle). Handles are allocated in assertion order, so every except this
admits names a handle below its own, and the except graph assert builds is acyclic.
A target retracted after its except leaves the except naming nothing, and a handle is
never reissued (docs/contexts.md, except).
Refuse a visibility `(except (sentexHandle H))` when no sentex is stored under H (`:unknown-handle`). Handles are allocated in assertion order, so every except this admits names a handle below its own, and the except graph `assert` builds is acyclic. A target retracted after its except leaves the except naming nothing, and a handle is never reissued (docs/contexts.md, except).
(check-exceptWhen-stratified kb rule-handle exc context)Throw unless adding the exceptWhen exception with conjuncts exc to the stored rule
rule-handle leaves the rule set stratified.
The exception is a new negative edge from the rule to the predicates it reads
(rules/watched-predicates, and the predicate of a (not (P …)) a closed extent reads
as NAF, rules/closed-extent-query-predicates), so it can close a cycle through
negation exactly as a whole rule can (check-stratified). The pending node is the
rule's stored graph node augmented with the new negative edges;
stratification-readers swaps it in for the stored rule so the walk sees the edge.
Runs before the meta-sentex is stored, so a refused exception leaves nothing behind.
Throw unless adding the exceptWhen exception with conjuncts `exc` to the stored rule `rule-handle` leaves the rule set stratified. The exception is a new negative edge from the rule to the predicates it reads (`rules/watched-predicates`, and the predicate of a `(not (P …))` a closed extent reads as NAF, `rules/closed-extent-query-predicates`), so it can close a cycle through negation exactly as a whole rule can (`check-stratified`). The pending node is the rule's stored graph node augmented with the new negative edges; `stratification-readers` swaps it in for the stored rule so the walk sees the edge. Runs before the meta-sentex is stored, so a refused exception leaves nothing behind.
(check-generator! kb sentence context)The three refusals that are a generator's alone: a rule whose consequent is a rule
(docs/generators.md). Everything else it satisfies as a rule, through check-rule!,
which both storage entry points call, so a generated rule owes what an authored one owes.
set/backwardRule generator is refused at every level, since no
backward goal's answer is a rule; a wrapper around a middle level would otherwise be
minted and refused one firing later, in the ledger. :inert stays legal.exceptWhen on a generated rule. An exception is a meta-sentex the assert path
stores (assert-exceptWhen-meta!) and a firing does not, so the guard would be dropped.
An exceptWhen on the outermost rule is legal.The three refusals that are a **generator**'s alone: a rule whose consequent is a rule (docs/generators.md). Everything else it satisfies as a rule, through `check-rule!`, which both storage entry points call, so a generated rule owes what an authored one owes. - **Forward-only.** A `set/backwardRule` generator is refused at every level, since no backward goal's answer is a rule; a wrapper around a middle level would otherwise be minted and refused one firing later, in the ledger. `:inert` stays legal. - **No `exceptWhen` on a generated rule.** An exception is a meta-sentex the assert path stores (`assert-exceptWhen-meta!`) and a firing does not, so the guard would be dropped. An `exceptWhen` on the outermost rule is legal. - **No generator cycle.** A generator on a path of feeds back to itself is refused outright, as stratification refuses a cycle through negation.
(check-ground kb sentence context)Reject a non-rule sentence that still contains pattern variables: (mortal ?x) is an
open formula, and stored as a premise unify would match it against any goal. Universal
claims are written as rules (check-range-restricted).
Rule-ness is read off the canonicalized record, since implies, set/*Rule wrappers and
their nesting all canonicalize into :antecedent. A schematic equation
(equals (fatherOf (fatherOf ?x)) (grandfather_of ?x)) is the exception: its variables
belong to a term-rewriting schema and it is stored as an oriented rewrite rule
(docs/equality.md). check-sentex-ground is the same check over a built sentex, as a dump
import holds.
Reject a non-rule sentence that still contains pattern variables: `(mortal ?x)` is an open formula, and stored as a premise `unify` would match it against any goal. Universal claims are written as rules (`check-range-restricted`). Rule-ness is read off the canonicalized record, since `implies`, `set/*Rule` wrappers and their nesting all canonicalize into `:antecedent`. A schematic equation `(equals (fatherOf (fatherOf ?x)) (grandfather_of ?x))` is the exception: its variables belong to a term-rewriting schema and it is stored as an oriented rewrite rule (docs/equality.md). `check-sentex-ground` is the same check over a built sentex, as a dump import holds.
(check-length-binding policy sentence context)Throw when the length binding sentence states (sx/arity-binding) disagrees with
what the sentence alone shows. For an engine grammar term, a binding that does not
admit every length its shape admits (arity/admits-shape?) is :length-against-shape,
carrying :relation and :shape, whatever policy. For any other relation, a
binding against its spelling is nm/check-binding!'s, under the :naming policy
policy.
Throw when the length binding `sentence` states (`sx/arity-binding`) disagrees with what the sentence alone shows. For an engine grammar term, a binding that does not admit every length its shape admits (`arity/admits-shape?`) is `:length-against-shape`, carrying `:relation` and `:shape`, whatever `policy`. For any other relation, a binding against its spelling is `nm/check-binding!`'s, under the `:naming` policy `policy`.
(check-no-defeat sentence)Refuse a defeat literal anywhere nm/literals descends: a fact, a not, a rule's
antecedents and consequent, an exceptWhen query. Throws :derived-only.
The engine derives every (defeat (sentexHandle H)) (docs/nmtms.md): a placed nogood
stores one for its unique weakest member. A defeat written as a premise would remove a
handle from belief whatever its class, and a rule reading one would fire on a read-time
verdict. The check reads the sentence alone, so it refuses the same sentence in every
KB and every arrival order. Matching and asking (defeat ?h) are reads and pass no
check.
Refuse a `defeat` literal anywhere `nm/literals` descends: a fact, a `not`, a rule's antecedents and consequent, an `exceptWhen` query. Throws `:derived-only`. The engine derives every `(defeat (sentexHandle H))` (docs/nmtms.md): a placed nogood stores one for its unique weakest member. A defeat written as a premise would remove a handle from belief whatever its class, and a rule reading one would fire on a read-time verdict. The check reads the sentence alone, so it refuses the same sentence in every KB and every arrival order. Matching and asking `(defeat ?h)` are reads and pass no check.
(check-no-imperative sentence)Refuse a do/ imperative anywhere inside a rule — antecedent, consequent, or
exceptWhen query.
A rule is evaluated inside the forward-chaining fixpoint, and an imperative there
would run a number of times that depends on firing order while mutating the KB the
fixpoint is still computing over. Order independence and locality are the two
invariants the TMS is built on (docs/nmtms.md); a side effect inside the fixpoint
breaks both at once. So a do/ form is legal only at the top level of an assert,
where the caller decided when it happens (docs/labeling.md).
Walks the whole form rather than the three slots, so a nesting cannot smuggle one past — the check is about a fixpoint reaching it, not about where it was written.
Refuse a `do/` imperative anywhere inside a rule — antecedent, consequent, or `exceptWhen` query. A rule is evaluated inside the forward-chaining fixpoint, and an imperative there would run a number of times that depends on firing order while mutating the KB the fixpoint is still computing over. Order independence and locality are the two invariants the TMS is built on (docs/nmtms.md); a side effect inside the fixpoint breaks both at once. So a `do/` form is legal only at the top level of an `assert`, where the caller decided when it happens (docs/labeling.md). Walks the whole form rather than the three slots, so a nesting cannot smuggle one past — the check is about a fixpoint reaching it, not about where it was written.
(check-rule! kb sentence context)Every pre-storage check a rule must pass, as a step that writes nothing.
Both storage entry points read this list: core/assert for an authored rule and a
generator firing for a derived one (docs/generators.md), so neither drifts. assert also
runs it over all the conjuncts of a polycanonicalized rule before storing any of them,
because (implies A (and C1 C2)) is split into one rule per conjunct and a refusal on C2
must not leave C1 stored.
check-variable-constraints! refuses only under *refuse-clashes?* (try-assert);
assert stores a rule it convicts and holds it inert (hold-rule-conviction!). A
generator owes three more checks (check-generator!), run last so the unbound-variable
complaint comes first.
Every pre-storage check a rule must pass, as a step that writes nothing. Both storage entry points read this list: `core/assert` for an authored rule and a generator firing for a derived one (docs/generators.md), so neither drifts. `assert` also runs it over all the conjuncts of a polycanonicalized rule before storing any of them, because `(implies A (and C1 C2))` is split into one rule per conjunct and a refusal on C2 must not leave C1 stored. `check-variable-constraints!` refuses only under `*refuse-clashes?*` (`try-assert`); `assert` stores a rule it convicts and holds it inert (`hold-rule-conviction!`). A generator owes three more checks (`check-generator!`), run last so the unbound-variable complaint comes first.
(check-rule-shape sentence)The refusals of check-rule! that read nothing from the KB, in its order: a do/
imperative anywhere in the rule, an or no expansion removes, a consequent variable no
antecedent binds, an open NAF literal, and a variable antecedent functor on a rule that
is not :inert (an inert rule runs in neither engine, so the index owes it nothing).
check-rule! runs this first, and a dump import runs it over each rule frame, which
may not read the KB: a declaration or rule the frame depends on may arrive later in
the stream (docs/naming.md).
The refusals of `check-rule!` that read nothing from the KB, in its order: a `do/` imperative anywhere in the rule, an `or` no expansion removes, a consequent variable no antecedent binds, an open NAF literal, and a variable antecedent functor on a rule that is not `:inert` (an inert rule runs in neither engine, so the index owes it nothing). `check-rule!` runs this first, and a dump import runs it over each rule frame, which may not read the KB: a declaration or rule the frame depends on may arrive later in the stream (docs/naming.md).
(check-sentex-ground s sentence context)check-ground over s, the sentex already built from sentence in context: throw
:not-ground when s is not a rule and has a free variable, unless sentence is a
schematic equation or a defn* definition. A variable inside a (Quote …) or bound
by a quantifier is not free (sx/closed?).
`check-ground` over `s`, the sentex already built from `sentence` in `context`: throw `:not-ground` when `s` is not a rule and has a free variable, unless `sentence` is a schematic equation or a `defn*` definition. A variable inside a `(Quote …)` or bound by a quantifier is not free (`sx/closed?`).
(check-stratified kb sentence inner context)Throw unless adding this rule leaves the rule set stratified — see docs/exceptions.md. Runs before anything is stored, so a refused rule leaves no partial state behind.
Fast path: with no negative edge on the rule being added and none on any stored rule
(negative-edge-rules), the graph has no negative edge at all and no cycle through
negation is possible, so the walk is skipped entirely. That is every rule in an
ontology that uses no negative dependency — no exception, no unknown, no aggregate,
no closed-extent negative and no different — which is most of them.
Throw unless adding this rule leaves the rule set stratified — see docs/exceptions.md. Runs before anything is stored, so a refused rule leaves no partial state behind. Fast path: with no negative edge on the rule being added and none on any stored rule (`negative-edge-rules`), the graph has no negative edge at all and no cycle through negation is possible, so the walk is skipped entirely. That is every rule in an ontology that uses no negative dependency — no exception, no `unknown`, no aggregate, no closed-extent negative and no `different` — which is most of them.
(constraint-admission kb sentence context)The derivation path's constraint-checks: one pass over the definitional checks,
answering both halves as values, {:violation v} when sentence is inadmissible in
context, else {:entailments [...]}. Forward chaining must not throw, and no check
here throws.
An arbitrable violation is not a violation here: the conclusion is placed and settle
weighs the pair, which gives the loser a reason. Only what cannot be represented is
reported: a malformed sentence, or an argument constraint whose conviction rests on the
absence of a fact. An argument conviction assert holds inert (held-inert?) is not a
violation either, unless it convicts a function application's input
(check-application-inputs). The answer then carries it under :conviction as a
{:violation :detail} map, and the caller stores and holds the conclusion
(hold-argument-conviction!).
The derivation path's `constraint-checks`: one pass over the definitional checks,
answering both halves as values, `{:violation v}` when `sentence` is inadmissible in
`context`, else `{:entailments [...]}`. Forward chaining must not throw, and no check
here throws.
An arbitrable violation is not a violation here: the conclusion is placed and `settle`
weighs the pair, which gives the loser a reason. Only what cannot be represented is
reported: a malformed sentence, or an argument constraint whose conviction rests on the
absence of a fact. An argument conviction `assert` holds inert (`held-inert?`) is not a
violation either, unless it convicts a function application's input
(`check-application-inputs`). The answer then carries it under `:conviction` as a
`{:violation :detail}` map, and the caller stores and holds the conclusion
(`hold-argument-conviction!`).(constraint-checks kb sentence context)(constraint-checks kb sentence context strength)Throw the first definitional violation that refuses-assert?, as typed ex-info: the
assert path. Under *refuse-clashes?*, the first violation of any kind (refusal),
fact-clash-checks and declaration-clash-checks asked first, with strength the
write's (:default when not given).
A violation naming the other believed members of its nogood does not refuse: the sentence
is stored and settle decides the nogood. An argument conviction assert holds inert
(held-inert?) does not refuse either; it is returned under :conviction and the caller
holds the stored fact in the :out forced set (argument-conviction).
Returns {:entailments [...] :conviction v}: the entailments the argument constraints draw
over an admissible sentence (constraint-entailments), empty unless
*assertive-arg-types?*, and the held conviction or nil. With the entailment on, the
sentence and everything it entails (entailment-check) must be admissible, the second
asked only when the sentence itself passed.
Throw the first definitional violation that `refuses-assert?`, as typed ex-info: the
assert path. Under `*refuse-clashes?*`, the first violation of any kind (`refusal`),
`fact-clash-checks` and `declaration-clash-checks` asked first, with `strength` the
write's (`:default` when not given).
A violation naming the other believed members of its nogood does not refuse: the sentence
is stored and `settle` decides the nogood. An argument conviction `assert` holds inert
(`held-inert?`) does not refuse either; it is returned under `:conviction` and the caller
holds the stored fact in the `:out` forced set (`argument-conviction`).
Returns `{:entailments [...] :conviction v}`: the entailments the argument constraints draw
over an admissible sentence (`constraint-entailments`), empty unless
`*assertive-arg-types?*`, and the held conviction or nil. With the entailment on, the
sentence and everything it entails (`entailment-check`) must be admissible, the second
asked only when the sentence itself passed.The argument constraints this namespace answers for at the entry point, as a set —
declaration-queries' keys, which it queries, and the sugar-spellings it reads
through the declaration their forward rules store.
Public because it is one of the tables that reads the :argument-constraint family
as a family, and predicates/check-facets holds those to enumerating exactly it.
A spelling in the family and not here is one the entry point cannot query for and so never
convicts; a spelling here and not in the family is one nothing declares.
The argument constraints this namespace answers for at the entry point, as a set — `declaration-queries`' keys, which it queries, and the `sugar-spellings` it reads through the declaration their forward rules store. Public because it is one of the tables that reads the `:argument-constraint` family **as a family**, and `predicates/check-facets` holds those to enumerating exactly it. A spelling in the family and not here is one the entry point cannot query for and so never convicts; a spelling here and not in the family is one nothing declares.
(constraint-entailments kb sentence context)(constraint-entailments kb sentence context types decls)What sentence's visible argument declarations entail about its arguments in context:
a vec of {:assert <sentence> :because [decl-handle edge-handle …] :position n :kind <the declaring functor>}, empty when they entail nothing. Every entailing kind is read:
arg, argArg, genlArg, interArg, the covering forms, the homogeneity forms and,
over a natFormula fact, resultArg, whether written in context or inherited by it.
(arg parentOf 1 animal) over (parentOf Fred Mary) entails (animal Fred). An
interArg entails the target type only once the trigger is known. An individual in a
genlArg position is ineligible (genls-problem convicts it). One entry per applicable
declaration, with no narrowing for redundancy, since narrowing would make belief depend on
arrival order (docs/argtypes.md). The entailment is drawn over the stored spelling
(stored-spelling).
Reads only. The caller, special/deduce-arg-types, mints each entry as a derived sentex
justified by the triggering fact and :because, so retracting any of them takes the type back.
What `sentence`'s visible argument declarations entail about its arguments in `context`:
a vec of `{:assert <sentence> :because [decl-handle edge-handle …] :position n :kind <the
declaring functor>}`, empty when they entail nothing. Every entailing kind is read:
`arg`, `argArg`, `genlArg`, `interArg`, the covering forms, the homogeneity forms and,
over a `natFormula` fact, `resultArg`, whether written in `context` or inherited by it.
`(arg parentOf 1 animal)` over `(parentOf Fred Mary)` entails `(animal Fred)`. An
`interArg` entails the target type only once the trigger is known. An individual in a
`genlArg` position is ineligible (`genls-problem` convicts it). One entry per applicable
declaration, with no narrowing for redundancy, since narrowing would make belief depend on
arrival order (docs/argtypes.md). The entailment is drawn over the stored spelling
(`stored-spelling`).
Reads only. The caller, `special/deduce-arg-types`, mints each entry as a derived sentex
justified by the triggering fact and `:because`, so retracting any of them takes the type back.(constraint-violation kb sentence context)The definitional checks as a value alone: nil when sentence is admissible in
context, else {:violation :arg-type|:arg-genl|:arg-position |:arg-constraint-kind|:disjoint|:asymmetric|:functional|:anti-transitive :detail {...}}.
Every violation, arbitrable ones included — which is what separates this from
constraint-admission. The callers are the checks on content that is never stored
when it fails: special/inadmissible's default arity, read by what abduce may assume
and by a context-valued function's computed genlCx edge. Content the engine stores
on its own behalf (a lift's copy, a merge's twin, an argument-type mint) asks
derivation-violation instead, so its arbitrable clash is stored and decided at each
reader.
The definitional checks as a value alone: nil when `sentence` is admissible in
`context`, else `{:violation :arg-type|:arg-genl|:arg-position
|:arg-constraint-kind|:disjoint|:asymmetric|:functional|:anti-transitive
:detail {...}}`.
**Every** violation, arbitrable ones included — which is what separates this from
`constraint-admission`. The callers are the checks on content that is never stored
when it fails: `special/inadmissible`'s default arity, read by what `abduce` may assume
and by a context-valued function's computed `genlCx` edge. Content the engine stores
on its own behalf (a lift's copy, a merge's twin, an argument-type mint) asks
`derivation-violation` instead, so its arbitrable clash is stored and decided at each
reader.(conviction-watch v)The term whose memberships can lift the argument conviction v (a {:violation :detail} map), as the {:term} field a waiting entry carries: the convicted argument,
whose separating membership leaving, or whose membership arriving under quotedArg's
kind lattice, can lift the conviction.
Read off the conviction the entry is decided under, every time it is decided. A re-ask that is still convicted can be convicted on a different argument — an application with two targets outside the type names the first, and once that one is lifted it names the second — and an entry left watching the first would never be re-asked when the second is lifted, so the lifting order would decide whether the firing is ever placed.
The term whose memberships can lift the argument conviction `v` (a `{:violation
:detail}` map), as the `{:term}` field a waiting entry carries: the convicted argument,
whose separating membership leaving, or whose membership arriving under `quotedArg`'s
kind lattice, can lift the conviction.
Read off the conviction the entry is decided under, every time it is decided. A
re-ask that is still convicted can be convicted on a different argument — an
application with two targets outside the type names the first, and once that one is
lifted it names the second — and an entry left watching the first would never be
re-asked when the second is lifted, so the lifting order would decide whether the
firing is ever placed.The checks try-assert asks of a declaration that constrains stored facts, as
[violation check] in the order asked, each (check kb sentence context strength)
answering a violation or nil. A grammar entry's :clash-checks :declaration names
one by its violation (predicates/clash-checks).
The checks `try-assert` asks of a declaration that constrains stored facts, as `[violation check]` in the order asked, each `(check kb sentence context strength)` answering a violation or nil. A grammar entry's `:clash-checks` `:declaration` names one by its violation (`predicates/clash-checks`).
(declaration-entailments kb sentence context dh)(declaration-entailments kb sentence context dh src)constraint-entailments narrowed to the declaration stored at dh: the entries whose
:because leads with dh, drawn from that declaration's match alone. Every arm draws
one entry per match, so the other declarations on the predicate are not read, and their
types are not asked mintable-type? once per fact of a sweep over dh's extent.
With src, the handle of the fact stored in a context context sees, each :because
also names the genlCx edges context sees the fact through (visibility-support):
the entailments placed below the fact's own context (special/pair-placements).
`constraint-entailments` narrowed to the declaration stored at `dh`: the entries whose `:because` leads with `dh`, drawn from that declaration's match alone. Every arm draws one entry per match, so the other declarations on the predicate are not read, and their types are not asked `mintable-type?` once per fact of a sweep over `dh`'s extent. With `src`, the handle of the fact stored in a context `context` sees, each `:because` also names the `genlCx` edges `context` sees the fact through (`visibility-support`): the entailments placed below the fact's own context (`special/pair-placements`).
(derivation-violation kb sentence context)constraint-admission's violation half alone: nil when sentence is admissible in
context or its only violation is arbitrable, else the {:violation :detail} map.
The argument-type mint reads this, so a mint clashing with a believed membership is
placed and weighed at settle as a rule's conclusion is (docs/argtypes.md).
`constraint-admission`'s violation half alone: nil when `sentence` is admissible in
`context` or its only violation is arbitrable, else the `{:violation :detail}` map.
The argument-type mint reads this, so a mint clashing with a believed membership is
placed and weighed at settle as a rule's conclusion is (docs/argtypes.md).(edge-stratification-violation kb sentence)The same check as a value, for a genl edge a rule derived
rather than one a caller asserted: nil when the edge is admissible, else a
violation map in the shape constraint-violation returns.
A derived edge reaches the taxonomy through integrate-transitive, so a rule
concluding (genl a b) can close a cycle with no caller asserting anything.
Throwing there is the wrong shape — chaining is a fixpoint and must not abort
halfway through one — so this joins the definitional constraints on the derivation
path: the conclusion is dropped and reported in (core/violations kb). Dropping
it is what keeps the invariant intact, since an unstratified edge that was merely
reported would still be in the taxonomy.
The same check as a **value**, for a `genl` edge a rule *derived* rather than one a caller asserted: nil when the edge is admissible, else a violation map in the shape `constraint-violation` returns. A derived edge reaches the taxonomy through `integrate-transitive`, so a rule concluding `(genl a b)` can close a cycle with no caller asserting anything. Throwing there is the wrong shape — chaining is a fixpoint and must not abort halfway through one — so this joins the definitional constraints on the derivation path: the conclusion is dropped and reported in `(core/violations kb)`. Dropping it is what keeps the invariant intact, since an unstratified edge that was merely *reported* would still be in the taxonomy.
(edge-support kb pred via context)The handles of the genl edge supporters a declaration written of via travels down to
reach pred, empty when via is pred.
A derivation through a super-predicate's declaration rests on the fact, the declaration and
the subsumption that makes the fact one of the declaration's tuples, so it ends when the
edge is retracted. The argument-type entailment and the equality a descended
(functional P) mints (special/derive-functional-equalities) both read it. One supporter
per edge on a shortest visible path (tax/reach-support).
The handles of the `genl` edge supporters a declaration written of `via` travels down to reach `pred`, empty when `via` is `pred`. A derivation through a super-predicate's declaration rests on the fact, the declaration and the subsumption that makes the fact one of the declaration's tuples, so it ends when the edge is retracted. The argument-type entailment and the equality a descended `(functional P)` mints (`special/derive-functional-equalities`) both read it. One supporter per edge on a shortest visible path (`tax/reach-support`).
The checks try-assert asks of a fact a declaration constrains, as [violation check]
in the order asked, each (check kb sentence context strength) answering a violation or
nil. A grammar entry's :clash-checks :fact names one by its violation
(predicates/clash-checks).
The checks `try-assert` asks of a fact a declaration constrains, as `[violation check]` in the order asked, each `(check kb sentence context strength)` answering a violation or nil. A grammar entry's `:clash-checks` `:fact` names one by its violation (`predicates/clash-checks`).
(force-reach! kb pred)(force-reach! kb pred global?)Rewrite the forced memberships over what pred reaches after it joins or leaves the
forced-monotonic set (docs/nmtms.md, "The forced-monotonic set"), and answer the
handles of the rules in that reach, which a firing swept while it was held void is
restored from by a re-join. global? names a move of the baseline set (decide/global?): the reach is
every stored sentex mentioning pred (its literals, their denials, the rules reading
or concluding it) and their firings. A declaration elsewhere moves no denial's :out
membership, so its reach is the rules reading or concluding pred, the rules with a
variable consequent among them, and their firings: flat in pred's facts. Both read
every context, since the forced sets are network state, the union over every reader.
Rewrite the forced memberships over what `pred` reaches after it joins or leaves the forced-monotonic set (docs/nmtms.md, "The forced-monotonic set"), and answer the handles of the rules in that reach, which a firing swept while it was held void is restored from by a re-join. `global?` names a move of the baseline set (`decide/global?`): the reach is every stored sentex mentioning `pred` (its literals, their denials, the rules reading or concluding it) and their firings. A declaration elsewhere moves no denial's `:out` membership, so its reach is the rules reading or concluding `pred`, the rules with a variable consequent among them, and their firings: flat in `pred`'s facts. Both read every context, since the forced sets are network state, the union over every reader.
(force-sentex! kb sx)Write the :mono, :out and :held memberships of the stored sentex sx into the
network: :held for a rule holding an open application its own context respells
nowhere (nat/held-application?, docs/nat.md). The assert path calls it before the
premise mark, so a forced-out fact is never IN, even for one relabel. A membership
already right writes nothing.
Write the `:mono`, `:out` and `:held` memberships of the stored sentex `sx` into the network: `:held` for a rule holding an open application its own context respells nowhere (`nat/held-application?`, docs/nat.md). The assert path calls it before the premise mark, so a forced-out fact is never IN, even for one relabel. A membership already right writes nothing.
(force-sentexes! kb sxs)Rewrite the network's forced memberships for the stored sentexes sxs and the
firings each concludes or informs, from the forced-monotonic set as it stands. It logs nothing: the
chainer logs a convicted firing once, as its justification is added. The relabel each
set change runs is the whole recompute: nothing stored is written or deleted. Answers
whether any membership moved.
Rewrite the network's forced memberships for the stored sentexes `sxs` and the firings each concludes or informs, from the forced-monotonic set as it stands. It logs nothing: the chainer logs a convicted firing once, as its justification is added. The relabel each set change runs is the whole recompute: nothing stored is written or deleted. Answers whether any membership moved.
(force-stored! kb)Write every forced membership the stored content takes under the forced-monotonic set:
recover's pass, run once the taxonomy replay has rebuilt the forced-monotonic
properties. A stored denial of a forced-monotonic literal with no premise mark and no
support is the record an
older store kept inert, and it takes the :default premise mark it was written with
(docs/nmtms.md, "The forced-monotonic set"). A stored rule nat/held-application?
holds is forced :held again (docs/nat.md, "The corresponding predicate").
Write every forced membership the stored content takes under the forced-monotonic set: `recover`'s pass, run once the taxonomy replay has rebuilt the forced-monotonic properties. A stored denial of a forced-monotonic literal with no premise mark and no support is the record an older store kept inert, and it takes the `:default` premise mark it was written with (docs/nmtms.md, "The forced-monotonic set"). A stored rule `nat/held-application?` holds is forced `:held` again (docs/nat.md, "The corresponding predicate").
(forced-conclusion-entries kb)The :forced-conclusion violations of the stored firings forced-conclusion-violation
convicts over every reader, read off the stored state: the firings the network holds
void (the :void forced set), and the declared-firings, which a reader that sees the
declaration reads void. Each entry is the violation with :sentence the conclusion's
stored spelling, :context its context and :rule the rule's handle, and carries no
:run. Equal entries are one; the order is content order of the conclusion, its
context and the rule's sentence, never a handle's.
The `:forced-conclusion` violations of the stored firings `forced-conclusion-violation` convicts over every reader, read off the stored state: the firings the network holds void (the `:void` forced set), and the `declared-firings`, which a reader that sees the declaration reads void. Each entry is the violation with `:sentence` the conclusion's stored spelling, `:context` its context and `:rule` the rule's handle, and carries no `:run`. Equal entries are one; the order is content order of the conclusion, its context and the rule's sentence, never a handle's.
(forced-conclusion-violation kb rule-handle conseq)(forced-conclusion-violation kb rule-handle conseq on?)The :forced-conclusion violation of a firing of the rule stored at rule-handle that
concludes the ground sentence conseq, or nil when the firing is admitted. A firing
concluding a denial of a forced-monotonic? literal is convicted, and so is one
concluding a forced-monotonic literal unless its rule is a forced-rule? with no believed
exceptWhen. A convicted firing is stored and held void (the :void forced set), and
the violation names the rule's unforced-antecedents (docs/nmtms.md, "The
forced-monotonic set"). The 3-arity reads the conclusion forced-monotonic over every
reader: the entry forced-conclusion-entries reads for a firing void at some reader.
The 4-arity reads the conclusion under the forced-monotonic reading on? (network-void?).
The `:forced-conclusion` violation of a firing of the rule stored at `rule-handle` that concludes the ground sentence `conseq`, or nil when the firing is admitted. A firing concluding a denial of a `forced-monotonic?` literal is convicted, and so is one concluding a forced-monotonic literal unless its rule is a `forced-rule?` with no believed `exceptWhen`. A convicted firing is stored and held void (the `:void` forced set), and the violation names the rule's `unforced-antecedents` (docs/nmtms.md, "The forced-monotonic set"). The 3-arity reads the conclusion forced-monotonic over every reader: the entry `forced-conclusion-entries` reads for a firing void at some reader. The 4-arity reads the conclusion under the forced-monotonic reading `on?` (`network-void?`).
(forced-monotonic? kb literal)(forced-monotonic? kb literal on?)Is literal in the forced-monotonic set (decide/forced-literal?, docs/nmtms.md,
"The forced-monotonic set"): over every reader, or under the forced-monotonic reading
on?.
Is `literal` in the forced-monotonic set (`decide/forced-literal?`, docs/nmtms.md, "The forced-monotonic set"): over every reader, or under the forced-monotonic reading `on?`.
(forced-out? kb sx)Is the stored sentex sx held in the :out forced set: a fact or a rule the argument
family holds (argument/held?, argument-conviction), or a tuple whose length breaks
its functor's (arity/inert-tuple?, docs/taxonomy.md, "Arity")?
Is the stored sentex `sx` held in the `:out` forced set: a fact or a rule the argument family holds (`argument/held?`, `argument-conviction`), or a tuple whose length breaks its functor's (`arity/inert-tuple?`, docs/taxonomy.md, "Arity")?
(forced-premise? sx)Does a premise mark on the stored sentex sx confer :monotonic in the labeller (the
:mono forced set): sx is a genlCx edge, which caps no firing's class
(docs/reference.md, decisions 1 and 9). Every other forced-monotonic literal keeps the
strength it was written at and is never a loser (decide/verdict).
Does a premise mark on the stored sentex `sx` confer `:monotonic` in the labeller (the `:mono` forced set): `sx` is a `genlCx` edge, which caps no firing's class (docs/reference.md, decisions 1 and 9). Every other forced-monotonic literal keeps the strength it was written at and is never a loser (`decide/verdict`).
(forced-rule? kb rule-sentex)Is the stored rule rule-sentex one whose firings conclude a forced-monotonic literal as an
ordinary belief: not set/defaultRule, no unknown antecedent, and no
unforced-antecedents. Its exceptWhen exceptions are meta-sentexes, which
forced-conclusion-violation reads at the firing.
Is the stored rule `rule-sentex` one whose firings conclude a forced-monotonic literal as an ordinary belief: not `set/defaultRule`, no `unknown` antecedent, and no `unforced-antecedents`. Its `exceptWhen` exceptions are meta-sentexes, which `forced-conclusion-violation` reads at the firing.
(forcing-retraction-problem kb handle where)The :uncleared-forcing refusal of retracting the sentex at handle, as a value, or
nil: the handle states a forced-monotonic declaration whose predicate has no established unforced
semantics (uncleared-forcing). The test reads the declaration properties' supporters,
which are what the sentence alone puts there, and fetches no record. where names the
entry point.
The `:uncleared-forcing` refusal of retracting the sentex at `handle`, as a value, or nil: the handle states a forced-monotonic declaration whose predicate has no established unforced semantics (`uncleared-forcing`). The test reads the declaration properties' supporters, which are what the sentence alone puts there, and fetches no record. `where` names the entry point.
(functional-clashes kb sentence context)The believed [handle value via n] rows that fill a functional slot of sentence with
a value other than its own argument n (docs/equality.md, "functional infers
equality instead of throwing"). via is the marked predicate, the sentence's own or a
super-predicate the mark descends from (tax/props-over), and the slot is probed at
via, so a filler written at either spelling is found. (functional P) constrains
position 2 of an arity-2 sentence and (functionalInArg P n) position n; both are
read and their clashes unioned and deduped (first-per-slot). Empty, on one map read,
when nothing above the predicate is marked.
The believed `[handle value via n]` rows that fill a functional slot of `sentence` with a value other than its own argument `n` (docs/equality.md, "`functional` infers equality instead of throwing"). `via` is the marked predicate, the sentence's own or a super-predicate the mark descends from (`tax/props-over`), and the slot is probed at `via`, so a filler written at either spelling is found. `(functional P)` constrains position 2 of an arity-2 sentence and `(functionalInArg P n)` position `n`; both are read and their clashes unioned and deduped (`first-per-slot`). Empty, on one map read, when nothing above the predicate is marked.
(functional-declaration-supporters tax via n)The handles of every declaration constraining via at position n: the
(functional via) sentexes when n is 2 and the (functionalInArg via n) sentexes,
unioned, so a merge survives retracting either spelling.
The handles of every declaration constraining `via` at position `n`: the `(functional via)` sentexes when `n` is 2 and the `(functionalInArg via n)` sentexes, unioned, so a merge survives retracting either spelling.
(functional-filler sentence [_ _ _ n])The incoming filler a clash row is about: argument n of sentence.
The incoming filler a clash row is about: argument `n` of `sentence`.
The functors whose sentex, stated in a context a genlCx move gives a reader, changes
what the content the reader already saw means to it: a cached relation (a mark, a
declaration, a genl edge, an equality), a function's result declaration
(nat/result-types, which types every application of the function), an except, a
defeat and a definition (sx/defn-predicates). A gain stating none of them shows
the reader facts alone, and a sweep may read what those facts meet in place of what
the reader saw (plain-gain?).
The functors whose sentex, stated in a context a `genlCx` move gives a reader, changes what the content the reader already saw means to it: a cached relation (a mark, a declaration, a `genl` edge, an equality), a function's result declaration (`nat/result-types`, which types every application of the function), an `except`, a `defeat` and a definition (`sx/defn-predicates`). A gain stating none of them shows the reader facts alone, and a sweep may read what those facts meet in place of what the reader saw (`plain-gain?`).
(generator-cycle kb inner context)A description of the cycle adding this generator would close in the rule set, or nil:
the shortest path of feeds from inner over the stored generators back to inner, a
self-feed included. One generator feeds another when its innermost conclusion is a
predicate the other generates from. The walk is breadth-first over concluded
predicates, via mapping each one reached to the [predicate handle] step reaching it.
It starts at the arriving generator only, since every stored one passed it at its own
arrival (docs/generators.md).
A description of the cycle adding this generator would close in the rule set, or nil: the shortest path of feeds from `inner` over the stored generators back to `inner`, a self-feed included. One generator feeds another when its innermost conclusion is a predicate the other generates from. The walk is breadth-first over concluded predicates, `via` mapping each one reached to the `[predicate handle]` step reaching it. It starts at the arriving generator only, since every stored one passed it at its own arrival (docs/generators.md).
(held-argument-entries kb)The violations of the stored sentexes the argument family holds, read off the stored
state: :inert-argument for a fact and :inert-rule for a rule, :sentence the
stored spelling, :context its context and :detail its conviction
(held-conviction). The order is content order of the sentence and context, never a
handle's. The records are hinted a chunk ahead, and the convictions share one
*pass-reads*, as refresh-argument-holds! decides them.
The violations of the stored sentexes the argument family holds, read off the stored state: `:inert-argument` for a fact and `:inert-rule` for a rule, `:sentence` the stored spelling, `:context` its context and `:detail` its conviction (`held-conviction`). The order is content order of the sentence and context, never a handle's. The records are hinted a chunk ahead, and the convictions share one `*pass-reads*`, as `refresh-argument-holds!` decides them.
(held-conviction kb sx)The argument conviction the stored sentex sx is held inert under
(argument-conviction), or nil when the argument family does not hold it.
The argument conviction the stored sentex `sx` is held inert under (`argument-conviction`), or nil when the argument family does not hold it.
(hold-argument-conviction! kb h f)Record the fact at h, of functor f, as held for an argument conviction, before its
forced memberships are written (force-sentex!): the assert path's half of the verdict
constraint-checks answered under :conviction.
Record the fact at `h`, of functor `f`, as held for an argument conviction, before its forced memberships are written (`force-sentex!`): the assert path's half of the verdict `constraint-checks` answered under `:conviction`.
(hold-rule-conviction! kb sx)Record the new rule sx as held when rule-conviction convicts it, and write its
:out membership: the rule entry points' half of the verdict, run before the rule is
premised or justified, so a convicted rule is never IN.
Record the new rule `sx` as held when `rule-conviction` convicts it, and write its `:out` membership: the rule entry points' half of the verdict, run before the rule is premised or justified, so a convicted rule is never IN.
(mergeable-values? x y)Could a functional clash between x and y be resolved by merging them? Only when
both are non-variable symbols, since the equality partition holds symbols; any other
clash is a nogood the settle decides (docs/equality.md, "functional infers equality
instead of throwing").
Could a functional clash between `x` and `y` be resolved by merging them? Only when both are non-variable symbols, since the equality partition holds symbols; any other clash is a nogood the settle decides (docs/equality.md, "`functional` infers equality instead of throwing").
(network-void? kb rule-handle conseq)Is a firing of the rule at rule-handle concluding conseq held void in the network
(the :void forced set): convicted with the conclusion read on the baseline set
(decide/global-reading) and the antecedents on the union over every reader. A
conclusion forced-monotonic only by a declaration stated outside CxUniverse is valid in the
network, and the read walk voids the firing at a reader that sees the declaration
(exc/forced-void).
Is a firing of the rule at `rule-handle` concluding `conseq` held void in the network (the `:void` forced set): convicted with the conclusion read on the baseline set (`decide/global-reading`) and the antecedents on the union over every reader. A conclusion forced-monotonic only by a declaration stated outside CxUniverse is valid in the network, and the read walk voids the firing at a reader that sees the declaration (`exc/forced-void`).
(opposing-handles v)The believed sentexes a violation is against, as a vector of handles — empty when it names none.
Two spellings, one reading. The pairwise kinds name a single opposing sentex in
:opposing-handle and always did; :anti-transitive convicts a two-step chain and the
direct step together, so it names both other members in :opposing-handles (the
nogood is a triple, not a pair — docs/nmtms.md). Every consumer that weighs a
violation against what it opposes reads this rather than either key, so a kind naming
two is weighed exactly as one naming one is, and the published :opposing-handle on
the three older kinds is left where callers already read it.
The believed sentexes a violation is *against*, as a vector of handles — empty when it names none. Two spellings, one reading. The pairwise kinds name a single opposing sentex in `:opposing-handle` and always did; `:anti-transitive` convicts a two-step chain and the direct step **together**, so it names both other members in `:opposing-handles` (the nogood is a triple, not a pair — docs/nmtms.md). Every consumer that weighs a violation against what it opposes reads this rather than either key, so a kind naming two is weighed exactly as one naming one is, and the published `:opposing-handle` on the three older kinds is left where callers already read it.
(plain-gain? kb gain seen)May a sweep of a group of readers a genlCx move gives the contexts gain
(tax/context-move's :gains) read what the facts of gain meet in place of what the
readers saw? When gain states none of the gain-side-blockers, and no context the
readers see, seen, states an except: then every pair, meeting or verdict the move
changes for such a reader holds a fact stored in gain and visible to the reader. An
except the readers see can hide a fact of gain from them, which a sweep from
gain's side would read past.
May a sweep of a group of readers a `genlCx` move gives the contexts `gain` (`tax/context-move`'s `:gains`) read what the facts of `gain` meet in place of what the readers saw? When `gain` states none of the `gain-side-blockers`, and no context the readers see, `seen`, states an `except`: then every pair, meeting or verdict the move changes for such a reader holds a fact stored in `gain` and visible to the reader. An `except` the readers see can hide a fact of `gain` from them, which a sweep from `gain`'s side would read past.
(quantity-shape-problem sentence)The :not-well-formed problem a non-finite measure magnitude is refused with, or
nil. ##Inf and ##NaN are number?s, and a stored (QuantityIntervalFn 0 ##Inf Second) makes every duration and metric goal in its context throw a
NumberFormatException out of the magnitude arithmetic, with no :type. A variable
magnitude stays legal, since a rule antecedent binds it. assert, check and an
import read it.
The `:not-well-formed` problem a non-finite measure magnitude is refused with, or nil. `##Inf` and `##NaN` are `number?`s, and a stored `(QuantityIntervalFn 0 ##Inf Second)` makes every duration and metric goal in its context throw a NumberFormatException out of the magnitude arithmetic, with no `:type`. A variable magnitude stays legal, since a rule antecedent binds it. `assert`, `check` and an import read it.
(quoted-positions kb pred context)A test of the positions of pred a quotedArg or quotedArgAndRest declaration
visible from context types (mentioned-position), behind quoted-declared?: false
of every position where neither is stored.
A test of the positions of `pred` a `quotedArg` or `quotedArgAndRest` declaration visible from `context` types (`mentioned-position`), behind `quoted-declared?`: false of every position where neither is stored.
(refresh-argument-holds! kb read-under)Decide the argument holds again for every stored fact and rule a queued write can move
(argument/take!), with read-under the taxonomy generations a conviction is read under
(special/conviction-generations). The candidates are the tuples and rules a moved
declaration, definition, type_relation_predicate membership, genl edge, separation or
genlCx edge reaches (rules-on, lattice-candidates, constrained-functors,
definition-candidates), and under the constraint-only reading the facts naming a term
whose membership moved. A recover, a rebuilt relation, or a move at a value kind reads
every declaration whole. The candidates are read over every context, and each is decided
from its own (argument-conviction). The queue is taken once the lattice candidates are
read, so a shutdown that stops the write there leaves it in place. Answers the handles
taken out of :out (redecide-holds!), or nil when nothing was queued.
Decide the argument holds again for every stored fact and rule a queued write can move (`argument/take!`), with `read-under` the taxonomy generations a conviction is read under (`special/conviction-generations`). The candidates are the tuples and rules a moved declaration, definition, `type_relation_predicate` membership, `genl` edge, separation or `genlCx` edge reaches (`rules-on`, `lattice-candidates`, `constrained-functors`, `definition-candidates`), and under the constraint-only reading the facts naming a term whose membership moved. A recover, a rebuilt relation, or a move at a value kind reads every declaration whole. The candidates are read over every context, and each is decided from its own (`argument-conviction`). The queue is taken once the lattice candidates are read, so a shutdown that stops the write there leaves it in place. Answers the handles taken out of `:out` (`redecide-holds!`), or nil when nothing was queued.
(refuses-assert? v)Does violation v refuse its sentence at the write entry point? True unless v is
arbitrable (arbitrable?), :weighed? or one of declaration-kinds. A clash naming
the other believed members of its nogood is stored, and settle decides it and reports
it when every member is :monotonic. An argument conviction the entailing reading
draws a membership for is stored, and the settle weighs that membership
(entailment-covers?). A declaration a stored length strands is stored and constrains
nothing. A malformed sentence, any other argument conviction and a clash naming no
stored member refuse (docs/nmtms.md, "What a refusal may rest on"). A fact's own
argument conviction does not refuse at assert: constraint-checks stores the fact and
holds it inert (fact-refuses?).
Does violation `v` refuse its sentence at the write entry point? True unless `v` is arbitrable (`arbitrable?`), `:weighed?` or one of `declaration-kinds`. A clash naming the other believed members of its nogood is stored, and `settle` decides it and reports it when every member is `:monotonic`. An argument conviction the entailing reading draws a membership for is stored, and the settle weighs that membership (`entailment-covers?`). A declaration a stored length strands is stored and constrains nothing. A malformed sentence, any other argument conviction and a clash naming no stored member refuse (docs/nmtms.md, "What a refusal may rest on"). A fact's own argument conviction does not refuse at `assert`: `constraint-checks` stores the fact and holds it inert (`fact-refuses?`).
(rule-violation kb sentence context)check-rule! as a value in the form the derivation path files — a
{:violation :detail} map, or nil when the rule stands.
The mint's form of the same list, and the reason it is a value is the reason every
check on that path is: a firing runs inside the fixpoint, an exception escaping it
would leave belief half-computed, and which rule happened to fire first would decide
what the KB ends up believing. So a mint that cannot stand is dropped and recorded
(violations/report), never thrown.
Read through the throwing form rather than restating it, so the two cannot drift —
the same trick core/check plays to predict assert.
`check-rule!` as a **value** in the form the derivation path files — a
`{:violation :detail}` map, or nil when the rule stands.
The mint's form of the same list, and the reason it is a value is the reason every
check on that path is: a firing runs inside the fixpoint, an exception escaping it
would leave belief half-computed, and which rule happened to fire first would decide
what the KB ends up believing. So a mint that cannot stand is dropped and recorded
(`violations/report`), never thrown.
Read through the throwing form rather than restating it, so the two cannot drift —
the same trick `core/check` plays to predict `assert`.(subsumed-mint kb sentence context)(subsumed-mint kb sentence context ok?)The handle of the believed record that already says, more specifically, what the minted
sentence says in context, or nil.
Two shapes: a membership (t x) subsumed by a membership in a subtype of t, and a genl
edge subsumed by a route of two edges or more. Nil for anything else and nil with the
toggle off. The read is of belief, so withholding the mint while the specific membership
is believed is a function of the current state and arrival order cannot decide which
records the KB holds (every-arrival-order-reaches-the-same-belief). Answers are
unchanged either way (docs/argtypes.md). With ok?, the first subsuming record whose
handle ok? accepts: a stored mint asks for one that does not rest on it
(special/withdrawable-mint).
The handle of the believed record that already says, more specifically, what the minted `sentence` says in `context`, or nil. Two shapes: a membership `(t x)` subsumed by a membership in a subtype of `t`, and a `genl` edge subsumed by a route of two edges or more. Nil for anything else and nil with the toggle off. The read is of belief, so withholding the mint while the specific membership is believed is a function of the current state and arrival order cannot decide which records the KB holds (`every-arrival-order-reaches-the-same-belief`). Answers are unchanged either way (docs/argtypes.md). With `ok?`, the first subsuming record whose handle `ok?` accepts: a stored mint asks for one that does not rest on it (`special/withdrawable-mint`).
(subsumer-reads kb sentence context)The handles whose records subsumed-mint can fetch when asked about the minted
sentence in context: for (t x), the stored (p x) of each unary predicate p
holding x other than t; for (genl x t), every stored genl edge out of x and
the supporters of each edge out of x that context sees. A superset, read off the
index and the taxonomy with no subtype, visibility or belief test, for a caller hinting
a record store (special/subsumed-mint-blocks). Empty where subsumed-mint answers
nil without a read.
The handles whose records `subsumed-mint` can fetch when asked about the minted `sentence` in `context`: for `(t x)`, the stored `(p x)` of each unary predicate `p` holding `x` other than `t`; for `(genl x t)`, every stored `genl` edge out of `x` and the supporters of each edge out of `x` that `context` sees. A superset, read off the index and the taxonomy with no subtype, visibility or belief test, for a caller hinting a record store (`special/subsumed-mint-blocks`). Empty where `subsumed-mint` answers nil without a read.
The forced-monotonic declarations whose retraction is refused, each with the semantics the
declared predicate has no unforced reading of: [declaration-functor predicate] ->
missing semantics (docs/nmtms.md, "The forced-monotonic set").
The forced-monotonic declarations whose retraction is refused, each with the semantics the declared predicate has no unforced reading of: `[declaration-functor predicate]` -> missing semantics (docs/nmtms.md, "The forced-monotonic set").
(unforced-antecedents kb rule-sentex)(unforced-antecedents kb rule-sentex on?)The predicates of the stored rule rule-sentex's antecedents that are not
forced-monotonic? literals (over every reader, or under the forced-monotonic reading on?),
unknown antecedents aside, distinct and in antecedent order: the predicates a
(forced_monotonic_predicate P) declaration would make forced-monotonic for the rule's
firings to conclude a forced-monotonic literal.
The predicates of the stored rule `rule-sentex`'s antecedents that are not `forced-monotonic?` literals (over every reader, or under the forced-monotonic reading `on?`), `unknown` antecedents aside, distinct and in antecedent order: the predicates a `(forced_monotonic_predicate P)` declaration would make forced-monotonic for the rule's firings to conclude a forced-monotonic literal.
(visibility-support kb dh context)The genlCx edge supporters along one visible path from context to the context the
sentex stored at dh is written in, or empty when it is written in context. A
derivation drawn in context from a declaration or a fact it inherits rests on that path
as it rests on the genl edges edge-support names, so retracting an edge on the path
takes the derivation back and a surviving route draws it again
(special/rederive-descended).
The `genlCx` edge supporters along one visible path from `context` to the context the sentex stored at `dh` is written in, or empty when it is written in `context`. A derivation drawn in `context` from a declaration or a fact it inherits rests on that path as it rests on the `genl` edges `edge-support` names, so retracting an edge on the path takes the derivation back and a surviving route draws it again (`special/rederive-descended`).
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 |