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.
Do the argument constraints entail as well as constrain?
On by default. The entailment is additive — it mints the type a declaration already constrains, as a justified, retractable sentex — and off leaves the constraint reading alone (docs/argtypes.md).
binding it is the ordinary way in. VAELII_ASSERTIVE_ARG_TYPES=0 sets the root
value off instead, which is what lets the whole suite be run under the constraint-only
reading — the parity gate that says the entailment is additive rather than a different
engine.
Do the argument constraints *entail* as well as constrain? **On by default.** The entailment is additive — it mints the type a declaration already constrains, as a justified, retractable sentex — and off leaves the constraint reading alone (docs/argtypes.md). `binding` it is the ordinary way in. `VAELII_ASSERTIVE_ARG_TYPES=0` sets the root value off instead, which is what lets the whole suite be run under the constraint-only reading — the parity gate that says the entailment is additive rather than a different engine.
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.
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.
(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 (the sentence's own where it carries the mark, a
super-predicate where the mark descends), which the equality derivation names in its
justification.
The converse is probed at the marked predicate and its mark read up the
hierarchy, exactly as asymmetry-problems and functional-clashes do and for the same
reason: (anti_symmetric parentOf) with (genl fatherOf parentOf) must convict a
fatherOf pair whichever spelling arrives last, so reading the mark off the exact
functor would leave the pair found or missed by arrival order.
matches-visible over the ground converse is the whole probe: it fans down to the
sub-predicate spellings (so (atOrAbove Alice Bob) finds a stored (atOrAboveStrict Alice Bob)) and folds a comparison predicate's converse internally, so no exact-sentence
filter is wanted here — one would drop exactly the descended pair the up-read exists to
catch. 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 (the sentence's own where it carries the mark, a super-predicate where the mark descends), which the equality derivation names in its justification. The converse is probed **at the marked predicate** and its mark read **up** the hierarchy, exactly as `asymmetry-problems` and `functional-clashes` do and for the same reason: `(anti_symmetric parentOf)` with `(genl fatherOf parentOf)` must convict a `fatherOf` pair whichever spelling arrives last, so reading the mark off the exact functor would leave the pair found or missed by arrival order. `matches-visible` over the ground converse is the whole probe: it fans **down** to the sub-predicate spellings (so `(atOrAbove Alice Bob)` finds a stored `(atOrAboveStrict Alice Bob)`) and folds a comparison predicate's converse internally, so no exact-sentence filter is wanted here — one would drop exactly the descended pair the up-read exists to catch. 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-violations kb sentence context)Every disjointness and cover clash sentence forms against believed content
visible from context — the nogood half of the membership checks, read by settle's
discovery. Empty when the sentence forms none. The tuple marks' nogoods are found
from a candidate index instead (vaelii.impl.decide).
Asked of a sentence that is itself stored and believed, which is what the discovery walks: the clashes it reports are with the other members of each nogood, since a term's own type is not disjoint from itself.
Plural: a term holding three mutually disjoint types forms three pairs, and stopping at
the first would report a set of pairs that depended on the order the argument root
handed the memberships back, which is arrival order. context is the asker; a caller
asking a stored sentex's question from a vantage passes the vantage.
**Every** disjointness and cover clash `sentence` forms against believed content visible from `context` — the nogood half of the membership checks, read by `settle`'s discovery. Empty when the sentence forms none. The tuple marks' nogoods are found from a candidate index instead (`vaelii.impl.decide`). Asked of a sentence that is itself **stored and believed**, which is what the discovery walks: the clashes it reports are with the *other* members of each nogood, since a term's own type is not disjoint from itself. Plural: a term holding three mutually disjoint types forms three pairs, and stopping at the first would report a set of pairs that depended on the order the argument root handed the memberships back, which is arrival order. `context` is the asker; a caller asking a stored sentex's question from a vantage passes the vantage.
(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.
It re-asks an entry point check of a stored declaration through the arm the entry point
reads, so the two cannot drift. The reader is vaelii.impl.quality: a declaration
stranded by an arity that arrived later constrains nothing, refuses nothing and mints
nothing, so it is a census question rather than a settle one (docs/taxonomy.md).
Only the position arm. declaration-problem also convicts a declaration disagreeing
with its predicate's relation_kind, and an arity arriving is not what makes that true,
so asking it here would report a second finding under the first one's trigger.
Both of interArg's positions are asked, as at the entry point, and the first that
convicts is the answer.
Through checked-sentence, like the entry point: a doubly negated
declaration is a declaration and is read as one, and a genuinely negative sentence keeps
its not, which matches neither arm below. A caller reading the record store hands in
a sentence the constructor already stripped to its positive body, so the pass costs it
nothing — the reason to spell it is that the arm is stated once and both entrances to it
must be the same entrance.
The `:arg-position` violation the **stored declaration** `sentence` commits in `context`, or nil — a constraint on a position its predicate does not have. It re-asks an entry point check of a stored declaration through the arm the entry point reads, so the two cannot drift. The reader is `vaelii.impl.quality`: a declaration stranded by an arity that arrived later constrains nothing, refuses nothing and mints nothing, so it is a census question rather than a settle one (docs/taxonomy.md). Only the position arm. `declaration-problem` also convicts a declaration disagreeing with its predicate's `relation_kind`, and an arity arriving is not what makes that true, so asking it here would report a second finding under the first one's trigger. Both of `interArg`'s positions are asked, as at the entry point, and the first that convicts is the answer. Through `checked-sentence`, like the entry point: a doubly negated declaration is a declaration and is read as one, and a genuinely negative sentence keeps its `not`, which matches neither arm below. A caller reading the record store hands in a sentence the constructor already stripped to its positive body, so the pass costs it nothing — the reason to spell it is that the arm is stated once and both entrances to it must be the same entrance.
(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 unless declaring (closed_extent_predicate P) leaves the rule set stratified.
The grant is what turns a closed (not (P …)) antecedent from a lookup into negation
as failure, so it adds a negative edge to every stored rule carrying one — and can close
a cycle through negation exactly as a genl edge arriving underneath stored rules can
(check-edge-stratified). Nil for anything that is not the declaration.
Complete without a wholesale walk: the edge it adds leaves precisely the rules with a
[:not P] antecedent, which the antecedent index names in one lookup, so each of those
is the start node and every cycle the grant could close passes through one of them.
Walked in content order, so two rules that each close a cycle give one refusal rather
than whichever was asserted first.
Runs before anything is written, so a refused grant leaves no mark, no posting and no cycle.
Throw unless declaring `(closed_extent_predicate P)` leaves the rule set stratified. The grant is what turns a closed `(not (P …))` antecedent from a lookup into negation as failure, so it adds a negative edge to every stored rule carrying one — and can close a cycle through negation exactly as a `genl` edge arriving underneath stored rules can (`check-edge-stratified`). Nil for anything that is not the declaration. Complete without a wholesale walk: the edge it adds leaves precisely the rules with a `[:not P]` antecedent, which the antecedent index names in one lookup, so each of those is the start node and every cycle the grant could close passes through one of them. Walked in content order, so two rules that each close a cycle give one refusal rather than whichever was asserted first. Runs before anything is written, so a refused grant leaves no mark, no posting and no cycle.
(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.
Unserializable: a function, an atom/ref, an open stream — anything nippy cannot freeze and thaw — stores in the in-memory backend and then throws at write time on the first on-disk backend, so the same assert would succeed or fail by backend. Refusing it here makes the backends agree: a stored sentence's values round-trip.
Uncanonical: a map or a set has no canonical form, so a sentence carrying one has
neither stable durable bytes nor a content order to tie-break on (first-unstorable).
Refused rather than canonicalized, because there is no ordering of an unordered
collection that is the sentence's — the fix is to write what the KB can order, a
sequential or a reified term.
Both throw :not-encodable, carrying the offending value under :value.
Reject a sentence carrying a value a stored sentence may not carry. **Unserializable**: a function, an atom/ref, an open stream — anything nippy cannot freeze and thaw — stores in the in-memory backend and then throws at write time on the first on-disk backend, so the same assert would succeed or fail by backend. Refusing it here makes the backends agree: a stored sentence's values round-trip. **Uncanonical**: a map or a set has no canonical form, so a sentence carrying one has neither stable durable bytes nor a content order to tie-break on (`first-unstorable`). Refused rather than canonicalized, because there is no ordering of an unordered collection that is the *sentence's* — the fix is to write what the KB can order, a sequential or a reified term. 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 new-exc-preds context)Throw unless adding an exceptWhen exception mentioning new-exc-preds to the stored
rule rule-handle leaves the rule set stratified.
The exception is a new negative edge from the rule to those 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 an exceptWhen exception mentioning `new-exc-preds` to the stored rule `rule-handle` leaves the rule set stratified. The exception is a new negative edge from the rule to those 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 must satisfy it satisfies as a rule, through the list below.
Forward-only. A generator's conclusion is a rule, and there is no backward goal
whose answer is one — concluding-rule-handles reads a goal's predicate, and a
generator's consequent predicate is implies, which names nothing a query asks for.
A set/backwardRule generator would therefore be stored claiming a capability it
cannot exercise, which is the accepted-and-inert state the indexability refusal
exists to keep out of the KB. :inert stays legal: it claims nothing. Asked of
every generator level, since a set/backwardRule around a middle level would be
minted as a backward generator and refused one firing later, in the ledger rather
than at the sentence.
No exceptWhen on a stamped rule. An exception is not a rule field — it is a
separate meta-sentex keyed by the rule's handle, split off and stored by the assert
path (assert-exceptWhen-meta!), which a firing does not run. So a stamped
exceptWhen would reach the store as nothing at all: the mint would be a rule whose
guard had silently evaporated, firing on exactly the bindings its author wrote it not
to. A guard that is dropped in silence is worse than one refused, so it is refused.
An exceptWhen on the outermost rule is a different and legal thing — it says
when not to stamp — and the message points there.
No generator cycle. A stamped rule whose conclusion feeds some generator's antecedent is a rule set that mints rules that mint rules, with no fixpoint anybody has bounded. Refused outright rather than capped, the same call stratification makes for a cycle through negation: the alternative is a KB whose size depends on how long the chainer was allowed to run.
Read by both storage entry points through check-rule!, so a generator a firing stamps
owes exactly what one an author wrote owes — which is the whole of what makes nesting
safe: the middle level is checked twice, once as a pattern and once as the rule it
became.
The three refusals that are a **generator**'s alone — a rule whose consequent is a rule (docs/generators.md). Everything else it must satisfy it satisfies as a rule, through the list below. **Forward-only.** A generator's conclusion is a rule, and there is no backward goal whose answer is one — `concluding-rule-handles` reads a goal's predicate, and a generator's consequent predicate is `implies`, which names nothing a query asks for. A `set/backwardRule` generator would therefore be stored claiming a capability it cannot exercise, which is the accepted-and-inert state the indexability refusal exists to keep out of the KB. `:inert` stays legal: it claims nothing. Asked of **every** generator level, since a `set/backwardRule` around a middle level would be minted as a backward generator and refused one firing later, in the ledger rather than at the sentence. **No `exceptWhen` on a stamped rule.** An exception is not a rule field — it is a separate meta-sentex keyed by the rule's handle, split off and stored by the assert path (`assert-exceptWhen-meta!`), which a firing does not run. So a stamped `exceptWhen` would reach the store as nothing at all: the mint would be a rule whose guard had silently evaporated, firing on exactly the bindings its author wrote it not to. A guard that is dropped in silence is worse than one refused, so it is refused. An `exceptWhen` on the **outermost** rule is a different and legal thing — it says when not to stamp — and the message points there. **No generator cycle.** A stamped rule whose conclusion feeds some generator's antecedent is a rule set that mints rules that mint rules, with no fixpoint anybody has bounded. Refused outright rather than capped, the same call stratification makes for a cycle through negation: the alternative is a KB whose size depends on how long the chainer was allowed to run. Read by both storage entry points through `check-rule!`, so a generator a *firing* stamps owes exactly what one an author wrote owes — which is the whole of what makes nesting safe: the middle level is checked twice, once as a pattern and once as the rule it became.
(check-ground kb sentence context)Reject a non-rule sentence that still contains pattern variables.
A fact asserts something; (mortal ?x) asserts nothing — it is an open formula, not
a sentence.
Stored as a premise it is worse than useless: unify matches it against any goal,
so it silently behaves as a universally quantified fact that nothing ever licensed.
Universal claims are written as rules, where check-range-restricted governs the
variables.
Rule-ness is read off the canonicalized record, not off the raw input: an
implies, a set/*Rule wrapper, and a nested combination of the two all
canonicalize into :antecedent, and pattern-matching the input would have to
re-derive that (and would miss a spelling).
A schematic equation (equals (fatherOf (fatherOf ?x)) (grandfather_of ?x)) is
the deliberate exception: its variables belong to a term-rewriting schema, not to an
open fact, so it is stored as an oriented rewrite rule rather than refused
(docs/equality.md, symbolic equational reasoning). It is not matched as a fact
under unify — its functor is equals, read by the equality machinery, not by the
fact prover for arbitrary goals.
check-sentex-ground is the same check over a sentex already built, which is what a
dump import holds.
Reject a non-rule sentence that still contains pattern variables. A fact asserts something; `(mortal ?x)` asserts nothing — it is an open formula, not a sentence. Stored as a premise it is worse than useless: `unify` matches it against any goal, so it silently behaves as a universally quantified fact that nothing ever licensed. Universal claims are written as rules, where `check-range-restricted` governs the variables. Rule-ness is read off the **canonicalized record**, not off the raw input: an `implies`, a `set/*Rule` wrapper, and a nested combination of the two all canonicalize into `:antecedent`, and pattern-matching the input would have to re-derive that (and would miss a spelling). A **schematic equation** `(equals (fatherOf (fatherOf ?x)) (grandfather_of ?x))` is the deliberate exception: its variables belong to a term-rewriting schema, not to an open fact, so it is stored as an oriented rewrite rule rather than refused (docs/equality.md, symbolic equational reasoning). It is not matched as a fact under `unify` — its functor is `equals`, read by the equality machinery, not by the fact prover for arbitrary goals. `check-sentex-ground` is the same check over a sentex already built, which is what a dump import holds.
(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.
Two entry points store a rule and this is the list both read. core/assert stores one
an author wrote; a generator firing stores one the KB derived
(docs/generators.md). What a rule has to be does not depend on which entry point it came
through, so a copy per entry point is the drift this exists to prevent — a check added at
the assert entry point that the mint never learned would let the fixpoint store what the
API refuses.
Factored out of the assert path so assert can also run it over all the
conjuncts of a polycanonicalized rule before storing any of them.
(implies A (and C1 C2)) is split into one rule per conjunct and then mapvd,
and a mapv is not a transaction: with the checks inline, a refusal on C2 leaves
C1 already stored, indexed, and chained from, while the caller sees a throw and
reasonably concludes nothing was asserted.
One arm here has no counterpart on the fact path at all —
check-variable-constraints!, which holds a rule's shared variables to the argument
constraints of every position they stand in. A ground argument is checked by
constraint-checks on the way in; a variable is checked here or nowhere, since the
term it will hold does not exist yet.
A generator owes three more (check-generator!), and they run last so the
sharper complaint comes first: a rule that is unbound and backward-only is refused
for the unbound variable, which is the one its author can act on.
Every pre-storage check a rule must pass, as a step that writes nothing. **Two entry points store a rule** and this is the list both read. `core/assert` stores one an author wrote; a generator firing stores one the KB derived (docs/generators.md). What a rule has to *be* does not depend on which entry point it came through, so a copy per entry point is the drift this exists to prevent — a check added at the assert entry point that the mint never learned would let the fixpoint store what the API refuses. Factored out of the assert path so `assert` can also run it over **all** the conjuncts of a polycanonicalized rule before storing *any* of them. `(implies A (and C1 C2))` is split into one rule per conjunct and then `mapv`d, and a `mapv` is not a transaction: with the checks inline, a refusal on C2 leaves C1 already stored, indexed, and chained from, while the caller sees a throw and reasonably concludes nothing was asserted. One arm here has no counterpart on the fact path at all — `check-variable-constraints!`, which holds a rule's shared variables to the argument constraints of every position they stand in. A ground argument is checked by `constraint-checks` on the way in; a variable is checked here or nowhere, since the term it will hold does not exist yet. A **generator** owes three more (`check-generator!`), and they run last so the sharper complaint comes first: a rule that is unbound *and* backward-only is refused for the unbound variable, which is the one its author can act on.
(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 still holds a pattern variable, unless
sentence is a schematic equation or a defn* definition.
`check-ground` over `s`, the sentex already built from `sentence` in `context`: throw `:not-ground` when `s` is not a rule and still holds a pattern variable, unless `sentence` is a schematic equation or a `defn*` definition.
(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 — a rule firing mid-fixpoint that aborted the run
would leave belief half-computed, and the project's stance is that contradictions
are soft. So the derivation path asks the question instead of being stopped by
the answer. No try/catch: the checks bottom out as values, so there is no thrown
answer to fish back out (and no whitelist of :types for a new check to miss).
An arbitrable violation is not a violation here at all. A firing has no caller
to refuse, so the two answers available are dropping the conclusion — no sentex, no
justification, and why-not reduced to :not-stored — or placing it and letting
settle weigh the pair like any other contradiction. Placing it is what gives the
loser a reason, so this reports only what genuinely cannot be represented: a
malformed sentence, or an argument constraint, whose conviction rests on the
absence of a fact rather than on a second one to weigh against.
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 — a rule firing mid-fixpoint that aborted the run
would leave belief half-computed, and the project's stance is that contradictions
are soft. So the derivation path asks the question instead of being stopped by
the answer. No try/catch: the checks bottom out as values, so there is no thrown
answer to fish back out (and no whitelist of `:type`s for a new check to miss).
An **arbitrable** violation is not a violation here at all. A firing has no caller
to refuse, so the two answers available are dropping the conclusion — no sentex, no
justification, and `why-not` reduced to `:not-stored` — or placing it and letting
`settle` weigh the pair like any other contradiction. Placing it is what gives the
loser a reason, so this reports only what genuinely cannot be represented: a
malformed sentence, or an argument constraint, whose conviction rests on the
*absence* of a fact rather than on a second one to weigh against.(constraint-checks kb sentence context)Throw the first definitional violation that refuses-assert?, as typed ex-info — the
assert path.
A violation naming the other believed members of its nogood does not refuse: the
sentence is stored and settle decides the nogood, whatever the members' classes. An
admitted clash is not reported here — settle discovers it from the relabelled
region, which is what makes the discovery route-agnostic and the answer the same in
every arrival order.
Returns the entailments the argument constraints draw over an admissible
sentence (constraint-entailments), for the caller to materialize once the sentex
it would be justified by exists. Empty unless *assertive-arg-types?*.
Two questions, not one, once the entailment is on. The sentence has to be
admissible and so does everything it entails (entailment-check) — the argument
declarations are read as definitions there, so admitting (parentOf Rex Mary) is
admitting (animal Rex), and a KB that cannot hold the second may not be left holding
the first. Asked second, and only when the sentence itself passed: a sentence already
refused needs no second reason, and the cascade is the more expensive read of the two.
Throw the first definitional violation that `refuses-assert?`, as typed ex-info — the assert path. A violation naming the other believed members of its nogood does not refuse: the sentence is stored and `settle` decides the nogood, whatever the members' classes. An admitted clash is **not** reported here — settle discovers it from the relabelled region, which is what makes the discovery route-agnostic and the answer the same in every arrival order. Returns the **entailments** the argument constraints draw over an admissible sentence (`constraint-entailments`), for the caller to materialize once the sentex it would be justified by exists. Empty unless `*assertive-arg-types?*`. **Two questions, not one, once the entailment is on.** The sentence has to be admissible and so does everything it entails (`entailment-check`) — the argument declarations are read as definitions there, so admitting `(parentOf Rex Mary)` is admitting `(animal Rex)`, and a KB that cannot hold the second may not be left holding the first. Asked second, and only when the sentence itself passed: a sentence already refused needs no second reason, and the cascade is the more expensive read of the two.
The argument constraints this namespace reads at the entry point, as a set — declaration- queries' keys.
Public because it is one of the rosters 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 reads at the entry point, as a set — `declaration- queries`' keys. Public because it is one of the rosters 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, genlArg, interArg, the covering forms and the
homogeneity forms, from a declaration written in context or inherited by it.
(arg parentOf 1 animal) over (parentOf Fred Mary) entails (animal Fred);
(genlArg partType 1 tangible) over (partType wheel_kind axle_kind) entails
(genl wheel_kind tangible); (interArg eats 1 carnivore 2 meat) over
(eats Rex Chunk) entails (meat Chunk) — but only once Rex is known to be a
carnivore, which is the condition the declaration is about. An individual in an
genlArg position is convicted by genls-problem rather than given an edge, so it is
ineligible here — said at the point it matters rather than relying on the check having
run first.
One entry per applicable declaration, with no narrowing for redundancy: see the commentary above for why every candidate narrowing would make belief depend on arrival order. Deduplication is the materializer's, where it is keyed on content.
Drawn over the spelling the store keeps (stored-spelling), not the one written: a
(symmetric P) fact names each argument at both positions, and which declaration a
mint rests on must not turn on how the fact was spelled.
Reads only. The caller decides whether to store, and the caller is
special/deduce-arg-types, which mints each one 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`, `genlArg`, `interArg`, the covering forms and the
homogeneity forms, from a declaration written in `context` or inherited by it.
`(arg parentOf 1 animal)` over `(parentOf Fred Mary)` entails `(animal Fred)`;
`(genlArg partType 1 tangible)` over `(partType wheel_kind axle_kind)` entails
`(genl wheel_kind tangible)`; `(interArg eats 1 carnivore 2 meat)` over
`(eats Rex Chunk)` entails `(meat Chunk)` — but only once `Rex` is known to be a
carnivore, which is the condition the declaration is *about*. An **individual** in an
`genlArg` position is convicted by `genls-problem` rather than given an edge, so it is
ineligible here — said at the point it matters rather than relying on the check having
run first.
One entry per applicable declaration, with no narrowing for redundancy: see the
commentary above for why every candidate narrowing would make belief depend on
arrival order. Deduplication is the materializer's, where it is keyed on content.
Drawn over the spelling the store keeps (`stored-spelling`), not the one written: a
`(symmetric P)` fact names each argument at both positions, and which declaration a
mint rests on must not turn on how the fact was spelled.
**Reads only.** The caller decides whether to store, and the caller is
`special/deduce-arg-types`, which mints each one 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 gates 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 gates 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,
which a membership arriving can place inside the declared type.
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,
which a membership arriving can place inside the declared type.
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.(declaration-entailments kb sentence context dh)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.
`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.
(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 declaration that rests on no edge.
Anything derived through a super-predicate's declaration rests on three things
rather than two: the fact, the declaration, and the subsumption that makes the fact
one of the declaration's tuples. Naming only the first two would leave the derivation
standing after the edge was retracted — a derived record supported by content that no
longer entails it, which is the exact failure justifying a derivation at all is meant
to prevent. Both descending derivations read it: the argument-type entailment below,
and the equality a descended (functional P) mints
(special/derive-functional-equalities).
One supporter per edge on a shortest visible path (tax/reach-support), which is
the witness rule everything else depending on a reachability takes: a justification is
a conjunction of supports, not a proof that no other route exists, so when the named
route goes what rested on it goes and is re-derived from whatever survives.
The handles of the `genl` edge supporters a declaration written of `via` travels down to reach `pred` — empty when `via` **is** `pred`, a declaration that rests on no edge. Anything **derived** through a super-predicate's declaration rests on three things rather than two: the fact, the declaration, and the subsumption that makes the fact one of the declaration's tuples. Naming only the first two would leave the derivation standing after the edge was retracted — a derived record supported by content that no longer entails it, which is the exact failure justifying a derivation at all is meant to prevent. Both descending derivations read it: the argument-type entailment below, and the equality a descended `(functional P)` mints (`special/derive-functional-equalities`). One supporter per edge on a shortest **visible** path (`tax/reach-support`), which is the witness rule everything else depending on a reachability takes: a justification is a conjunction of supports, not a proof that no other route exists, so when the named route goes what rested on it goes and is re-derived from whatever survives.
(force-reach! kb pred)Rewrite the forced memberships over what pred reaches — every stored sentex
mentioning it (its literals, their denials, the rules reading or concluding it) and
their firings — after pred joins or leaves the roster (docs/nmtms.md, "The
forced-monotonic roster"). Answers the handles of the rules in that reach, which a
firing swept while it was held void is restored from by a re-join.
Rewrite the forced memberships over what `pred` reaches — every stored sentex mentioning it (its literals, their denials, the rules reading or concluding it) and their firings — after `pred` joins or leaves the roster (docs/nmtms.md, "The forced-monotonic roster"). Answers the handles of the rules in that reach, which a firing swept while it was held void is restored from by a re-join.
(force-roster! kb)Write every forced membership the stored content takes under the roster:
recover's pass, run once the taxonomy replay has rebuilt the roster properties. A
stored denial of a roster 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 roster").
Write every forced membership the stored content takes under the roster: `recover`'s pass, run once the taxonomy replay has rebuilt the roster properties. A stored denial of a roster 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 roster").
(force-sentex! kb sx)Write the :mono and :out memberships of the stored sentex sx into the network.
The assert path calls it before the premise mark, so a forced-out denial is never IN,
even for one relabel. A membership already right writes nothing.
Write the `:mono` and `:out` memberships of the stored sentex `sx` into the network. The assert path calls it before the premise mark, so a forced-out denial 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 roster as it stands, and report each firing
newly held void. 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 roster as it stands, and report each firing newly held void. The relabel each set change runs is the whole recompute: nothing stored is written or deleted. Answers whether any membership moved.
(forced-conclusion-violation kb rule-handle conseq)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 roster literal unless its rule is a roster-rule? with no believed
exceptWhen. A convicted firing is stored, held void (the :void forced set) and
reported (docs/nmtms.md, "The forced-monotonic roster").
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 roster literal unless its rule is a `roster-rule?` with no believed `exceptWhen`. A convicted firing is stored, held void (the `:void` forced set) and reported (docs/nmtms.md, "The forced-monotonic roster").
(forced-monotonic? kb literal)Is literal on the forced-monotonic roster (decide/roster-literal?, docs/nmtms.md,
"The forced-monotonic roster").
Is `literal` on the forced-monotonic roster (`decide/roster-literal?`, docs/nmtms.md, "The forced-monotonic roster").
(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 roster 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 roster literal keeps the strength it was written at and is never a loser (`decide/verdict`).
(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 roster 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 roster 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] triples that already fill a functional slot for the
same first argument with something other than b — the clash a (functional P)
declaration turns into either a rejection or an equality.
via is the predicate carrying the mark this clash is against, which is the
sentence's own where it carries one and a super-predicate where the mark descends
(tax/props-over). Two fatherOf mothers for one child are two parentOf values,
so (functional parentOf) convicts them; reading the mark off the exact functor made
that bypassable through the sub-predicate entry point while the slot probe already fanned
down the hierarchy, so which spelling arrived second decided whether the clash
existed.
The slot is probed at the marked predicate: (parentOf a ?v) finds a filler
written either way through the matcher's fan, where (fatherOf a ?v) would miss one
written at the general spelling. Empty when nothing above the sentence's predicate is
marked — one map read on a KB that declares nothing functional, which is every bulk
load.
The quadruple carries the position, because functionalInArg moved it. A
(functional P) mark always constrains argument 2, so the arity-2 path reads its
incoming filler as (second (nm/args sentence)) and nothing had to say so; a
(functionalInArg P n) constrains argument n, and which argument the clash is about
is no longer a constant the caller can assume. Every consumer reads b off the
quadruple rather than off the sentence.
Both marks are consulted and their clashes unioned, so a predicate carrying
(functional P) and (functionalInArg P 2) yields one deduped clash resting on
both declarations — which is the behaviour derive-functional-equalities already
wants of two (functional P) sentexes in different contexts, applied one level up.
The believed `[handle value via]` triples that already fill a functional slot for the same first argument with something other than `b` — the clash a `(functional P)` declaration turns into either a rejection or an equality. `via` is the predicate carrying the mark this clash is against, which is the sentence's own where it carries one and a **super-predicate** where the mark descends (`tax/props-over`). Two `fatherOf` mothers for one child are two `parentOf` values, so `(functional parentOf)` convicts them; reading the mark off the exact functor made that bypassable through the sub-predicate entry point while the *slot probe* already fanned down the hierarchy, so which spelling arrived second decided whether the clash existed. The slot is probed **at the marked predicate**: `(parentOf a ?v)` finds a filler written either way through the matcher's fan, where `(fatherOf a ?v)` would miss one written at the general spelling. Empty when nothing above the sentence's predicate is marked — one map read on a KB that declares nothing functional, which is every bulk load. **The quadruple carries the position**, because `functionalInArg` moved it. A `(functional P)` mark always constrains argument 2, so the arity-2 path reads its incoming filler as `(second (nm/args sentence))` and nothing had to say so; a `(functionalInArg P n)` constrains argument `n`, and which argument the clash is about is no longer a constant the caller can assume. Every consumer reads `b` off the quadruple rather than off the sentence. Both marks are consulted and their clashes unioned, so a predicate carrying `(functional P)` **and** `(functionalInArg P 2)` yields one deduped clash resting on both declarations — which is the behaviour `derive-functional-equalities` already wants of two `(functional P)` sentexes in different contexts, applied one level up.
(functional-declaration-supporters tax via n)The handles of every declaration supporting a functional constraint on via at
position n — the (functional via) sentexes when n is 2, and the
(functionalInArg via n) sentexes always, unioned.
Both genuinely support the merge, so both belong in its antecedents: retracting one
leaves it standing on the other, which is the rule
a-merge-rests-on-every-functional-declaration-not-on-one-of-them pins for two
(functional P) sentexes and holds for the same reason across the two spellings.
The handles of every declaration supporting a functional constraint on `via` at position `n` — the `(functional via)` sentexes when `n` is 2, and the `(functionalInArg via n)` sentexes always, unioned. Both genuinely support the merge, so both belong in its antecedents: retracting one leaves it standing on the other, which is the rule `a-merge-rests-on-every-functional-declaration-not-on-one-of-them` pins for two `(functional P)` sentexes and holds for the same reason across the two spellings.
(functional-filler sentence [_ _ _ n])The incoming filler a clash quadruple is about — argument n of sentence.
The one reader for it, where three call sites would otherwise each spell
(second (nm/args sentence)), so the arg-2 assumption has exactly one place to live
and it is this function.
The incoming filler a clash quadruple is about — argument `n` of `sentence`. The one reader for it, where three call sites would otherwise each spell `(second (nm/args sentence))`, so the arg-2 assumption has exactly one place to live and it is this function.
(generator-cycle kb inner context)A description of the cycle adding this generator would put in the rule set, or nil.
The graph is generators only, and one hop: an edge runs from a generator to any generator that reads — in an antecedent it stamps from — the predicate its stamped rule concludes. A cycle there is a rule set that mints rules that mint rules, and unlike ordinary recursion nothing bounds it: each round adds rules rather than facts, and the next round's rules are the ones the last round wrote.
Refused outright rather than depth-capped. A cap would make the KB's contents a function of how long the chainer happened to run, and "how many rules does this KB have" would stop having an answer — the same call stratification makes for a cycle through negation (docs/exceptions.md). It is also why nesting is not a cap worth having: a nested generator stamps one level further before it stops, and what makes a rule set unbounded is the cycle, not the depth.
Both directions, because either can be the new edge: the arriving generator may stamp what a stored one reads, or read what a stored one stamps, and a self-loop is the case where it does both to itself. Checking only one direction would let the cycle in whenever the two generators were asserted in the other order — which is the order dependence every check here exists to keep out.
A description of the cycle adding this generator would put in the rule set, or nil. The graph is generators only, and one hop: an edge runs from a generator to any generator that reads — in an antecedent it stamps from — the predicate its stamped rule concludes. A cycle there is a rule set that mints rules that mint rules, and unlike ordinary recursion nothing bounds it: each round adds *rules* rather than facts, and the next round's rules are the ones the last round wrote. Refused outright rather than depth-capped. A cap would make the KB's contents a function of how long the chainer happened to run, and "how many rules does this KB have" would stop having an answer — the same call stratification makes for a cycle through negation (docs/exceptions.md). It is also why *nesting* is not a cap worth having: a nested generator stamps one level further before it stops, and what makes a rule set unbounded is the cycle, not the depth. **Both directions, because either can be the new edge**: the arriving generator may stamp what a stored one reads, or read what a stored one stamps, and a self-loop is the case where it does both to itself. Checking only one direction would let the cycle in whenever the two generators were asserted in the other order — which is the order dependence every check here exists to keep out.
(inert-denial? kb sentence)Is sentence a denial (not S) of a forced-monotonic? literal S. The labeller
holds such a denial OUT (the :out forced set): it is never believed, forms no nogood
and fires no rule (docs/nmtms.md, "The forced-monotonic roster").
Is `sentence` a denial `(not S)` of a `forced-monotonic?` literal `S`. The labeller holds such a denial OUT (the `:out` forced set): it is never believed, forms no nogood and fires no rule (docs/nmtms.md, "The forced-monotonic roster").
(mergeable-values? x y)Could a functional clash between x and y be resolved by concluding they name
one thing? Only when both are plain symbols: the equality closure is a partition
over symbols (wff refuses a compound, and a number or a string is not even an
indexable term), so (equals 1980 1990) is not a sentence the KB can hold.
This is the line between a clash that is knowledge and a clash that is an error.
Two spellings of a person may denote one woman; 1980 and 1990 are two numbers and
no merge can make them one, so a numeric functional clash is a nogood the settle
decides. A symbol clash merges only when both members are :monotonic
(docs/reference.md, decision 6).
Could a functional clash between `x` and `y` be *resolved* by concluding they name one thing? Only when both are plain symbols: the equality closure is a partition over symbols (`wff` refuses a compound, and a number or a string is not even an indexable term), so `(equals 1980 1990)` is not a sentence the KB can hold. This is the line between a clash that is knowledge and a clash that is an error. Two spellings of a person may denote one woman; 1980 and 1990 are two numbers and no merge can make them one, so a numeric functional clash is a nogood the settle decides. A symbol clash merges only when both members are `:monotonic` (docs/reference.md, decision 6).
(mintable-type? tax t)Is t a type a membership can be minted in — a name the genl hierarchy actually
holds?
A global read, like genls-problem's individual floor and for the same reason:
this asks what the name is, not what a context can see of it, and an entailment
drawn in a context that cannot see thing would be an entailment about nothing.
A name the hierarchy does not hold is not a type we invent a membership in — which
is where a structural constraint (an argument that must be a number, a string) lands
without needing a list of exemptions to keep in step. The answer is held per genl
generation (tax/genl?-global-held): a sweep asks it of one declaration's type once
per fact.
Is `t` a type a membership can be minted in — a name the genl hierarchy actually holds? A **global** read, like `genls-problem`'s individual floor and for the same reason: this asks what the name *is*, not what a context can see of it, and an entailment drawn in a context that cannot see `thing` would be an entailment about nothing. A name the hierarchy does not hold is not a type we invent a membership in — which is where a structural constraint (an argument that must be a number, a string) lands without needing a list of exemptions to keep in step. The answer is held per `genl` generation (`tax/genl?-global-held`): a sweep asks it of one declaration's type once per fact.
(mintable-types tax)mintable-type? as a fn of one type, for a caller asking about many types while the
hierarchy holds still: thing's subtypes are walked once (tax/specs-of-all, global
for mintable-type?'s reason) and each answer is a set lookup (docs/exceptions.md).
`mintable-type?` as a fn of one type, for a caller asking about many types while the hierarchy holds still: `thing`'s subtypes are walked once (`tax/specs-of-all`, global for `mintable-type?`'s reason) and each answer is a set lookup (docs/exceptions.md).
(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.
(refuses-assert? v)Does violation v refuse its sentence at the write entry point? True unless v is
arbitrable (arbitrable?): a clash naming the other believed members of its nogood is
stored, and settle decides it and reports it when every member is :monotonic. A
malformed sentence, an argument conviction and a clash naming no stored member refuse
(docs/nmtms.md, "What a refusal may rest on").
Does violation `v` refuse its sentence at the write entry point? True unless `v` is arbitrable (`arbitrable?`): a clash naming the other believed members of its nogood is stored, and `settle` decides it and reports it when every member is `:monotonic`. A malformed sentence, an argument conviction and a clash naming no stored member refuse (docs/nmtms.md, "What a refusal may rest on").
(roster-rule? kb rule-sentex)Is the stored rule rule-sentex one whose firings conclude a roster literal as an
ordinary belief: not set/defaultRule, no unknown antecedent, and every antecedent a
forced-monotonic? literal. 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 roster literal as an ordinary belief: not `set/defaultRule`, no `unknown` antecedent, and every antecedent a `forced-monotonic?` literal. Its `exceptWhen` exceptions are meta-sentexes, which `forced-conclusion-violation` reads at the firing.
(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)The handle of the believed record that already says, more specifically, what the
minted sentence says in context — or nil when nothing does.
The two shapes an argument declaration mints: 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, so a caller asks without
testing either first.
A read of belief, which is what makes it order-independent. Withholding the mint
while the specific membership is believed and drawing it again when that membership
leaves is a function of the current state, so the arrival order of the fact, the
declaration and the specific type cannot decide which records the KB ends up holding —
the property every-arrival-order-reaches-the-same-belief pins. What the KB answers
is untouched either way: subsumption reaches t from the specific type with or without
a record in between (docs/argtypes.md).
The handle of the believed record that already says, more specifically, what the minted `sentence` says in `context` — or nil when nothing does. The two shapes an argument declaration mints: 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, so a caller asks without testing either first. **A read of belief, which is what makes it order-independent.** Withholding the mint while the specific membership is believed and drawing it again when that membership leaves is a function of the current state, so the arrival order of the fact, the declaration and the specific type cannot decide which records the KB ends up holding — the property `every-arrival-order-reaches-the-same-belief` pins. What the KB *answers* is untouched either way: subsumption reaches `t` from the specific type with or without a record in between (docs/argtypes.md).
The roster 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 roster").
The roster 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 roster").
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 |