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.
(arity-violation kb sentence context)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 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.
(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-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-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] :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] :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 / genlContext 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` / `genlContext` 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.
(functional-clashes kb sentence context)The believed [handle value] pairs that already fill P's 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.
The believed `[handle value]` pairs that already fill `P`'s 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.
(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 CoreContext 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 CoreContext 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.
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 |