The definitional checks — argIsa 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 — argIsa 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.
Does the assert path hand a disjointness or functionality clash to settle as
a nogood instead of throwing?
Off by default, which leaves assert refusing exactly what it refuses today: a
disjoint or functional clash at any strength. On, the three checks read one rule —
refuse only against :monotonic content, arbitrate against a :default claim — and
(dog Rex) beside (cat Rex) becomes a represented dilemma rather than a throw.
The derivation path does not consult this and never did: a rule firing has no caller
to refuse, so an arbitrable violation there is always placed and arbitrated (which is
what gives the loser a why-not). This var is only about whether a writer is told
no, and that is a policy question rather than an engine one.
binding it is the ordinary way in; VAELII_ARBITRATE_CONSTRAINTS=1 sets the root
value, which is what lets the whole suite be run under it. A KB that names a
:constraints policy of its own overrides both — kb/constraint-policies names them
and arbitrating? is the one read of either.
Does the **assert** path hand a disjointness or functionality clash to `settle` as a nogood instead of throwing? **Off by default**, which leaves `assert` refusing exactly what it refuses today: a disjoint or functional clash at any strength. On, the three checks read one rule — refuse only against `:monotonic` content, arbitrate against a `:default` claim — and `(dog Rex)` beside `(cat Rex)` becomes a represented dilemma rather than a throw. The derivation path does not consult this and never did: a rule firing has no caller to refuse, so an arbitrable violation there is always placed and arbitrated (which is what gives the loser a `why-not`). This var is only about whether a *writer* is told no, and that is a policy question rather than an engine one. `binding` it is the ordinary way in; `VAELII_ARBITRATE_CONSTRAINTS=1` sets the root value, which is what lets the whole suite be run under it. A KB that names a `:constraints` policy of its own overrides both — `kb/constraint-policies` names them and `arbitrating?` is the one read of either.
Do the argument constraints entail as well as constrain?
Off by default. A KB that derives types it cannot retract cleanly is worse than one that derives none, and entailing changes what a KB contains rather than only what it answers — so it is opt-in, and off leaves the constraint reading alone (docs/argtypes.md).
binding it is the ordinary way in. VAELII_ASSERTIVE_ARG_TYPES=1 sets the root
value instead, which is what lets the whole suite be run under it — the parity gate
that says the entailment is additive rather than a different engine.
Do the argument constraints *entail* as well as constrain? **Off by default.** A KB that derives types it cannot retract cleanly is worse than one that derives none, and entailing changes what a KB *contains* rather than only what it answers — so it is opt-in, and off leaves the constraint reading alone (docs/argtypes.md). `binding` it is the ordinary way in. `VAELII_ASSERTIVE_ARG_TYPES=1` sets the root value instead, which is what lets the whole suite be run under it — the parity gate that says the entailment is additive rather than a different engine.
The definitional violations that name a pair of believed sentexes rather than a
malformed sentence, so settle can arbitrate them like any other contradiction.
The definitional violations that name a pair of believed sentexes rather than a malformed sentence, so `settle` can arbitrate them like any other contradiction.
(arbitrable-violations kb sentence context)Every definitional clash sentence forms against believed content visible from
context — the nogood half of the checks, read by settle's discovery. Empty when
the sentence is admissible outright.
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 pair, since a sentence never opposes itself (a term's own type is not disjoint from itself, its own value is not a second value, and its own converse is a different tuple).
Plural, and that is the point. constraint-problem stops at the first violation
because a refusal needs only one reason. A pair is not a reason — it is a fact about
two sentexes — and a term holding three mutually disjoint types forms three of them,
so stopping at the first would report a set of pairs that depended on the order the
argument root handed the memberships back. That order is handle order, which is
arrival order, which is the one thing belief may not depend on.
Only the three arbitrable arms run. The argument constraints cannot produce a pair, and on this path the sentence is already stored — so whatever they would say about it was said when it was written.
**Every** definitional clash `sentence` forms against believed content visible from `context` — the nogood half of the checks, read by `settle`'s discovery. Empty when the sentence is admissible outright. 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 pair, since a sentence never opposes itself (a term's own type is not disjoint from itself, its own value is not a second value, and its own converse is a different tuple). Plural, and that is the point. `constraint-problem` stops at the first violation because a refusal needs only one reason. A pair is not a reason — it is a fact about two sentexes — and a term holding three mutually disjoint types forms three of them, so stopping at the first would report a set of pairs that depended on the order the argument root handed the memberships back. That order is handle order, which is arrival order, which is the one thing belief may not depend on. Only the three arbitrable arms run. The argument constraints cannot produce a pair, and on this path the sentence is already stored — so whatever they would say about it was said when it was written.
(arbitrable? v)Can settle arbitrate this violation instead of the caller refusing it — does it
name an opposing believed sentex to form a nogood with?
Can `settle` arbitrate this violation instead of the caller refusing it — does it name an opposing believed sentex to form a nogood with?
(arbitrating? kb)Does kb arbitrate a definitional clash against defeasible content rather than
refusing it at the door — and let a declaration reach back over stored content?
The KB's own :constraints policy decides when it has one (kb/constraint-policies
names them); a KB that named none reads the process default, so
VAELII_ARBITRATE_CONSTRAINTS=1 still moves a whole suite and a binding still moves
one call.
Does `kb` arbitrate a definitional clash against defeasible content rather than refusing it at the door — and let a declaration reach back over stored content? The KB's own `:constraints` policy decides when it has one (`kb/constraint-policies` names them); a KB that named none reads the process default, so `VAELII_ARBITRATE_CONSTRAINTS=1` still moves a whole suite and a `binding` still moves one call.
(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.
arity-violation's twin, one level up: that one asks whether a stored fact is the
wrong length, this one whether a stored declaration names a position the length
leaves it without. Both re-ask a door check of content already admitted, and both go
through the arm the door itself reads so the two cannot drift.
The reader is vaelii.impl.quality, not settle. A declaration stranded by an arity
that arrived later is inert — it constrains nothing, refuses nothing and mints
nothing — so unlike a wrong-length fact there is no admitted content to name and no
newly to report: it reads the same an hour later, which makes it a census question
rather than a settle one. docs/taxonomy.md records that split.
Only the position arm. declaration-problem also convicts a declaration disagreeing
with its predicate's relationKind, 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 interArgIsa's positions are asked, as at the door, and the first that
convicts is the answer.
Through checked-sentence, like the twin and like the door: 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. `arity-violation`'s twin, one level up: that one asks whether a stored *fact* is the wrong length, this one whether a stored *declaration* names a position the length leaves it without. Both re-ask a door check of content already admitted, and both go through the arm the door itself reads so the two cannot drift. The reader is `vaelii.impl.quality`, not `settle`. A declaration stranded by an arity that arrived later is **inert** — it constrains nothing, refuses nothing and mints nothing — so unlike a wrong-length fact there is no admitted content to name and no *newly* to report: it reads the same an hour later, which makes it a census question rather than a settle one. `docs/taxonomy.md` records that split. Only the position arm. `declaration-problem` also convicts a declaration disagreeing with its predicate's `relationKind`, 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 `interArgIsa`'s positions are asked, as at the door, and the first that convicts is the answer. Through `checked-sentence`, like the twin and like the door: 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, because a binding is described in more than one place and a
reader carries the vocabulary from one description to the next. Both of this
namespace's doors word it — a wrong-length sentence (arity-problem) and a declaration
naming a position the length denies (arg-position-problem) — and
settle/report-arity-reach! words the same binding for the facts one arriving late
convicts. "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: a
reader told it goes looking for a declaration nobody wrote, and one binding wearing two
descriptions reads as two problems. door_and_report_test is the roster that holds
every reader's message to this clause.
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, because a binding is described in more than one place and a reader carries the vocabulary from one description to the next. Both of this namespace's doors word it — a wrong-length sentence (`arity-problem`) and a declaration naming a position the length denies (`arg-position-problem`) — and `settle/report-arity-reach!` words the same binding for the facts one arriving late convicts. "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: a reader told it goes looking for a declaration nobody wrote, and one binding wearing two descriptions reads as two problems. `door_and_report_test` is the roster that holds every reader's message to this clause.
(arity-violation kb sentence context)(arity-violation kb sentence context types)The arity violation sentence commits in context, or nil — that one arm, asked of
content already stored.
The retroactive report's probe (settle/report-arity-reach!). A declaration arriving
after the facts it convicts was never seen by the check that runs on the way in, so
the facts are re-asked here — the same arity-problem the door reads, so the two
cannot drift about what a wrong arity is.
Nothing else in the arm's family is asked: the sentence is stored, so whatever the other checks would say about it was said when it was written, and only the arity declaration is what just arrived.
No :opposing-class, unlike every problem constraint-problem hands back. A class
is what a caller weighs two sides with, and this caller weighs nothing — stamping one
would advertise an arbitration that deliberately does not happen.
The four-argument form takes the membership reader rather than building one. A reader memoizes per context for the life of one caller, and the sweep asks this of every fact of a whole spec subtree — so building one per fact throws the memo away once per question and pays the retrieval every time. The caller holds one reader per context it meets instead.
The arity violation `sentence` commits in `context`, or nil — that one arm, asked of content **already stored**. The retroactive report's probe (`settle/report-arity-reach!`). A declaration arriving after the facts it convicts was never seen by the check that runs on the way in, so the facts are re-asked here — the same `arity-problem` the door reads, so the two cannot drift about what a wrong arity is. Nothing else in the arm's family is asked: the sentence is stored, so whatever the other checks would say about it was said when it was written, and only the *arity* declaration is what just arrived. **No `:opposing-class`**, unlike every problem `constraint-problem` hands back. A class is what a caller weighs two sides with, and this caller weighs nothing — stamping one would advertise an arbitration that deliberately does not happen. The four-argument form takes the membership reader rather than building one. A reader memoizes per context for the life of one caller, and the sweep asks this of every fact of a whole spec subtree — so building one per fact throws the memo away once per question and pays the retrieval every time. The caller holds one reader per context it meets instead.
(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-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-concluders 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-concluders` 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 doors 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 doors 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 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)) (grandfatherOf ?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.
Reject a non-rule sentence that still contains pattern variables. A fact asserts something; `(mortal ?x)` asserts nothing — it is an open 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)) (grandfatherOf ?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-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 doors 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 door it came
through, so a copy per door is the drift this exists to prevent — a check added at
the assert door 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 left
C1 already stored, indexed, and chained from, while the caller saw a throw and
reasonably concluded nothing had been asserted.
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 doors 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 door it came through, so a copy per door is the drift this exists to prevent — a check added at the assert door 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 left C1 already stored, indexed, and chained from, while the caller saw a throw and reasonably concluded nothing had been asserted. 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-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 exception on the rule being added and none on any stored rule, 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 exceptions, 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 exception on the rule being added and none on any stored rule, 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 exceptions, 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 as typed ex-info — the assert path.
Not every violation refuses. One that names an opposing believed sentex is a
nogood, and whether the writer is told no is refuses-assert?'s question: against
known-true content, yes (admitting it would store what the KB can never believe);
against a defeasible claim, the sentence is admitted and settle arbitrates the pair
it forms. 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?*.
Throw the first definitional violation as typed ex-info — the assert path. Not every violation refuses. One that names an opposing *believed* sentex is a nogood, and whether the writer is told no is `refuses-assert?`'s question: against known-true content, yes (admitting it would store what the KB can never believe); against a defeasible claim, the sentence is admitted and `settle` arbitrates the pair it forms. 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?*`.
(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 argIsa|argGenl|interArgIsa}, empty when they entail nothing.
(argIsa parentOf 1 animal) over (parentOf Fred Mary) entails (animal Fred);
(argGenl partType 1 physical_object) over (partType wheel_kind axle_kind) entails
(genl wheel_kind physical_object); (interArgIsa 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
argGenl 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.
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, the declaration] — so retracting either 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 argIsa|argGenl|interArgIsa}`, empty when they entail nothing.
`(argIsa parentOf 1 animal)` over `(parentOf Fred Mary)` entails `(animal Fred)`;
`(argGenl partType 1 physical_object)` over `(partType wheel_kind axle_kind)` entails
`(genl wheel_kind physical_object)`; `(interArgIsa 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
`argGenl` 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.
**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, the declaration]` — so retracting either 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 :arity|:arg-type|:arg-genl|:arg-position |:arg-constraint-kind|:disjoint|:asymmetric|:functional :detail {...}}.
Every violation, arbitrable ones included — which is what separates this from
constraint-admission. The callers are the paths that mint content nobody asked
for and that has somewhere else to be: the decontextualization lift's copy, the
equality migration's twin, and the gate on what abduce may assume. None of those
is a rule firing with a conclusion to stand behind — a lift can decline to copy, a
merge can decline to restate, an abducer can decline to hypothesize — so where a
firing arbitrates, they refuse, and the refusal is reported rather than thrown.
The definitional checks as a value alone: nil when `sentence` is admissible in
`context`, else `{:violation :arity|:arg-type|:arg-genl|:arg-position
|:arg-constraint-kind|:disjoint|:asymmetric|:functional :detail {...}}`.
**Every** violation, arbitrable ones included — which is what separates this from
`constraint-admission`. The callers are the paths that *mint* content nobody asked
for and that has somewhere else to be: the decontextualization lift's copy, the
equality migration's twin, and the gate on what `abduce` may assume. None of those
is a rule firing with a conclusion to stand behind — a lift can decline to copy, a
merge can decline to restate, an abducer can decline to hypothesize — so where a
firing arbitrates, they refuse, and the refusal is reported rather than thrown.(edge-stratification-violation kb sentence)The same check as a value, for a genl / genlCx 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` / `genlCx` 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.
(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 door 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 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 door 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.
(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.
(membership-arity kb f context)The arity a one-place membership functor f declares of its argument, or nil — one of
the three spellings itself, or a collection the taxonomy makes a genl of one.
Public for the reason predicate-type-arities is, and in its place: settle's
retroactive arity report triggers on an arriving declaration and has to recognise the
same ones this door does. Reading the raw map there and the closure here is the drift
its own docstring warns about, so the closure read is the shared one.
Read through the closure because the readers read through one. membered-arity
answers off (:closures (types pred)), so (genl myBinPred binaryPredicate) beside
(myBinPred fatherOf) makes fatherOf binary to everything that reads a declaration.
Matching the three literal functors here made the writer of one blind to exactly that
spelling: the disagreeing edge lands, and the reader then convicts facts under it. A
roster read twice is a roster that drifts, and these are its two reads.
The literal is asked first and answers all but the unusual case; only a one-place
sentence whose functor is not already one of the three pays the cached genls behind
it. Content-ordered, so a functor made a genl of two of them — itself incoherent —
picks the same one every run.
The arity a one-place membership functor `f` declares of its argument, or nil — one of the three spellings itself, or a collection the taxonomy makes a `genl` of one. Public for the reason `predicate-type-arities` is, and in its place: `settle`'s retroactive arity report triggers on an arriving declaration and has to recognise the same ones this door does. Reading the raw map there and the closure here is the drift its own docstring warns about, so the closure read is the shared one. **Read through the closure because the readers read through one.** `membered-arity` answers off `(:closures (types pred))`, so `(genl myBinPred binaryPredicate)` beside `(myBinPred fatherOf)` makes `fatherOf` binary to everything that *reads* a declaration. Matching the three literal functors here made the *writer* of one blind to exactly that spelling: the disagreeing edge lands, and the reader then convicts facts under it. A roster read twice is a roster that drifts, and these are its two reads. The literal is asked first and answers all but the unusual case; only a one-place sentence whose functor is not already one of the three pays the cached `genls` behind it. Content-ordered, so a functor made a `genl` of two of them — itself incoherent — picks the same one every run.
(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 stays the hard rejection it has always been.
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 stays the hard rejection it has always been.
What each predicate-type membership says the arity is. The arity sentexes and
these memberships derive each other through the CxCore rules, so a declared
predicate normally has both — but a {:chain? false} assert or a KB loaded without
the rules has only what was written, so both spellings are read.
Public because settle's retroactive arity report triggers on an arriving arity
declaration, and these memberships are the second way to write one — a roster read
twice is a roster that drifts.
What each predicate-type membership says the arity is. The `arity` sentexes and
these memberships derive each other through the CxCore rules, so a declared
predicate normally has both — but a `{:chain? false}` assert or a KB loaded without
the rules has only what was written, so both spellings are read.
Public because `settle`'s retroactive arity report triggers on an arriving *arity
declaration*, and these memberships are the second way to write one — a roster read
twice is a roster that drifts.(refuses-assert? kb v)Does this violation refuse the sentence on the assert path?
:asymmetric reads the class either way — that is the line it draws, and the one the
other two are generalized to. :disjoint and :functional refuse unconditionally
until kb's constraint policy (arbitrating?) opts into the same rule. Everything
else is a malformed sentence or an open-world judgement and refuses outright.
Does this violation refuse the sentence on the **assert** path? `:asymmetric` reads the class either way — that is the line it draws, and the one the other two are generalized to. `:disjoint` and `:functional` refuse unconditionally until `kb`'s constraint policy (`arbitrating?`) opts into the same rule. Everything else is a malformed sentence or an open-world judgement and refuses outright.
(rule-violation kb sentence context)check-rule! as a value in the shape 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 shape 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`.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 |