Well-formedness checks for the special predicates: genl / genlContext (the type and
context hierarchies), disjoint / disjointMetatype, and argIsa (argument types).
Each returns a seq of problem strings; assert throws if any are present.
Ordinary sentences are checked for argument types by checks/constraint-checks.
The per-functor check fns are defined here; which functor gets which check is
not — that dispatch is one arm of the special-predicate table in
vaelii.impl.special, so the functor enumeration lives in exactly one place and
a predicate added to the table without a :wff arm is visibly missing rather
than silently unchecked. special/wff-problems is the walk.
Plus one check that is about a rule set rather than a sentence:
negation-cycle finds the cycle through negation that an exceptWhen exception
closes. Two things can close one — a rule arriving, and a genl edge arriving
underneath rules already stored — and checks runs the search on both paths (see
the section at the bottom, and docs/exceptions.md).
Well-formedness checks for the special predicates: genl / genlContext (the type and context hierarchies), disjoint / disjointMetatype, and argIsa (argument types). Each returns a seq of problem strings; `assert` throws if any are present. Ordinary sentences are checked for argument *types* by checks/constraint-checks. The per-functor check fns are defined here; **which functor gets which check is not** — that dispatch is one arm of the special-predicate table in `vaelii.impl.special`, so the functor enumeration lives in exactly one place and a predicate added to the table without a `:wff` arm is visibly missing rather than silently unchecked. `special/wff-problems` is the walk. Plus one check that is about a *rule set* rather than a sentence: `negation-cycle` finds the cycle through negation that an `exceptWhen` exception closes. Two things can close one — a rule arriving, and a `genl` edge arriving underneath rules already stored — and `checks` runs the search on both paths (see the section at the bottom, and docs/exceptions.md).
(arg-constraint-problems _ [f pred n type :as s])argIsa and argGenl — the two argument constraints — are structurally identical:
a predicate, a positive-integer position, and a type. They differ only in what
they demand of the argument sitting there, which is checks' business, not this
one's, so one check serves both and reads the functor out of the sentence for its
messages. Stating it twice would let the two drift.
The constrained relation is not held to a spelling. A function has argument
positions exactly as a predicate does — (argIsa Milli 1 unit_of_measure_no_prefix)
says what the argument of a NAT (Milli Meter) must be, which is the same kind of
claim resultIsa makes about its result — and a function is CapitalCamelCase, which
is also how an individual is spelled. So no spelling test can separate the relation
this check wants to admit from the term it would want to refuse, and refusing on the
capital costs the whole vocabulary of function argument types. The position and the
type argument are still checked, because those are decidable from the sentence.
A constraint on a term that never heads a sentence is inert, which is the cheaper
side of the open-world trade this project takes everywhere else.
A relation may also be denoted rather than named — (argIsa (TypeCapableFn skillCapableOf) 1 intelligent_agent) constrains the relation that NAT denotes — so a
non-atomic term is a first argument too. What is left to refuse is a first argument
that is no kind of term at all: a number, a string, a keyword.
`argIsa` and `argGenl` — the two argument constraints — are structurally identical: a predicate, a positive-integer position, and a type. They differ only in what they *demand* of the argument sitting there, which is `checks`' business, not this one's, so one check serves both and reads the functor out of the sentence for its messages. Stating it twice would let the two drift. **The constrained relation is not held to a spelling.** A *function* has argument positions exactly as a predicate does — `(argIsa Milli 1 unit_of_measure_no_prefix)` says what the argument of a NAT `(Milli Meter)` must be, which is the same kind of claim `resultIsa` makes about its result — and a function is CapitalCamelCase, which is also how an individual is spelled. So no spelling test can separate the relation this check wants to admit from the term it would want to refuse, and refusing on the capital costs the whole vocabulary of function argument types. The position and the *type* argument are still checked, because those are decidable from the sentence. A constraint on a term that never heads a sentence is inert, which is the cheaper side of the open-world trade this project takes everywhere else. A relation may also be **denoted rather than named** — `(argIsa (TypeCapableFn skillCapableOf) 1 intelligent_agent)` constrains the relation that NAT denotes — so a non-atomic term is a first argument too. What is left to refuse is a first argument that is no kind of term at all: a number, a string, a keyword.
(arg-preserving-problems tax [f pred n rel :as s])argPreserving / argPreservingInverse — a predicate, a positive-integer
position, and the relation the argument is preserved along. Structurally the arg
constraints' shape, plus the one restriction that is the whole point of the
declaration: the relation must be transitive.
vaelii.impl.inherit walks the named relation to a fixpoint, so a declaration over
a relation nobody said composes gets transitivity manufactured for it — two hops of
begat licensing a claim that only one hop was ever evidence for. An argIsa on
argument 3 cannot express that: argIsa is open-world, so it bites only for a
relation that happens to carry some other type and waves through the one that
carries none, which is the common authoring order (name the relation, type it
later). So it is refused here, where the other special predicates' structural
rules live, and refused identically either way.
The fix for a refusal is to declare (transitive R) first — or to name one of the
two hierarchies the engine closes itself (inherit/virtual-relations).
The inheriting relation is held to what arg-constraint-problems holds its own
first argument to, and for the same reasons: a function is spelled like an
individual, a relation may be denoted by a NAT rather than named, and a declaration
about a term that never heads a sentence is inert. Refusing the CapitalCamelCase
spelling while admitting the NAT — which is what a nm/individual? test does, since
a compound is not an individual — refuses the conventional spelling and waves the
exotic one through. The preserved-along relation is stricter, and stays a
symbol: fact-reach walks it by building (R x ?v), which a non-atomic term does
not make a sentence of, and usable-relation? has no transitivity to read off one.
`argPreserving` / `argPreservingInverse` — a predicate, a positive-integer position, and the relation the argument is preserved along. Structurally the arg constraints' shape, plus the one restriction that is the whole point of the declaration: **the relation must be transitive.** `vaelii.impl.inherit` walks the named relation to a fixpoint, so a declaration over a relation nobody said composes gets transitivity manufactured for it — two hops of `begat` licensing a claim that only one hop was ever evidence for. An `argIsa` on argument 3 cannot express that: argIsa is open-world, so it bites only for a relation that happens to carry some *other* type and waves through the one that carries none, which is the common authoring order (name the relation, type it later). So it is refused here, where the other special predicates' structural rules live, and refused identically either way. The fix for a refusal is to declare `(transitive R)` first — or to name one of the two hierarchies the engine closes itself (`inherit/virtual-relations`). The **inheriting** relation is held to what `arg-constraint-problems` holds its own first argument to, and for the same reasons: a function is spelled like an individual, a relation may be denoted by a NAT rather than named, and a declaration about a term that never heads a sentence is inert. Refusing the CapitalCamelCase spelling while admitting the NAT — which is what a `nm/individual?` test does, since a compound is not an individual — refuses the conventional spelling and waves the exotic one through. The **preserved-along** relation is stricter, and stays a symbol: `fact-reach` walks it by building `(R x ?v)`, which a non-atomic term does not make a sentence of, and `usable-relation?` has no transitivity to read off one.
(correspondence-problems _ [f fname pred pos :as s])(functionCorrespondingPredicate F P N) says the function F and the predicate P
state the same relationship, N naming the argument of P that carries F's value.
F is a function name — a MotherFn-shaped constant, an individual by the naming
invariants — so the individual refusal falls on P alone. N is optional and
1-based; omitted, the value takes P's last argument, which is the shape nearly
every correspondence has. Whether N is in range is not knowable here: it is
checked against the application's arity, which no declaration states.
`(functionCorrespondingPredicate F P N)` says the function `F` and the predicate `P` state the same relationship, `N` naming the argument of `P` that carries `F`'s value. `F` is a function name — a `MotherFn`-shaped constant, an individual by the naming invariants — so the individual refusal falls on `P` alone. `N` is optional and 1-based; omitted, the value takes `P`'s last argument, which is the shape nearly every correspondence has. Whether `N` is in range is not knowable here: it is checked against the *application*'s arity, which no declaration states.
(cycle-description cycle)Render a negation-cycle path as one line, for an error message.
Render a `negation-cycle` path as one line, for an error message.
(different-problems _ [_ & args])different is not assertible. It is negation as failure over the equality
closure, answered by a prover and never stored: an assertible one would be OWL's
differentFrom, a positive commitment that a later sameAs would contradict, and
docs/equality.md deliberately does not build it. Stored as a premise it would also
be silently ignored, since the prover is authoritative and never reads facts.
`different` is **not assertible**. It is negation as failure over the equality closure, answered by a prover and never stored: an assertible one would be OWL's `differentFrom`, a positive commitment that a later `sameAs` would contradict, and docs/equality.md deliberately does not build it. Stored as a premise it would also be silently ignored, since the prover is authoritative and never reads facts.
(disjoint-problems tax [_ a b :as s])(disjointMetatype-problems _ [_ m :as s])(equality-problems tax [f a b :as s])rewriteOf / sameAs / equals relate symbols: the closure is a partition
over terms, so a compound argument is refused — with two carve-outs, one for each
kind of compound equality that does reduce to machinery that exists.
(rewriteOf T E) with a compound E is not term equality at all — it is a
NAT reify-to-term declaration (docs/nat.md), whose second argument is a quoted NAT
expression, not a term to merge. Waved through (only the target T need be a
symbol) and skipped by the equality integrate arm.
(equals L R) with a variable-bearing compound side is a schematic
equational rule — an oriented rewrite fatherOf∘fatherOf → grandfatherOf, not a
merge (docs/equality.md, symbolic equational reasoning). Its sides are compounds
by design, so the compound refusal is waived; instead it must be orientable
into a terminating rewrite (rewrite/orient), or it is refused here before
anything is stored. A ground (equals (F a) (F b)) is not schematic — it
reifies to symbols first (docs/nat.md) — and a compound that reifies to no symbol
(a NAUT measure) still hits the refusal below.
rewriteOf carries two further restrictions. It is directional, so a self-edge
(the degenerate cycle, and what a sloppy import pipeline actually emits) and a
longer cycle both leave the class with no head and are refused like a genl
cycle. And both sides must be the same role — predicate-with-predicate,
type-with-type, individual-with-individual (roles-clash?): rewriting a term of
one kind into another is meaningless (merging Fido into dog) and a likely
import bug. Unlike round one, a predicate or a type is now a legal rewriteOf
target — the merge moves its trie keys, functor root, rule-index postings and
genl closure with it (docs/equality.md). sameAs / equals stay
individuals-only (OWL); rewriteOf is the spelling relation, so it is the one
that carries vocabulary alignment across predicates and types. (sameAs A A) is
fine — OWL makes sameAs reflexive.
`rewriteOf` / `sameAs` / `equals` relate **symbols**: the closure is a partition over terms, so a compound argument is refused — with two carve-outs, one for each kind of compound equality that *does* reduce to machinery that exists. * `(rewriteOf T E)` with a **compound** `E` is not term equality at all — it is a NAT reify-to-term declaration (docs/nat.md), whose second argument is a quoted NAT expression, not a term to merge. Waved through (only the target `T` need be a symbol) and skipped by the equality integrate arm. * `(equals L R)` with a **variable-bearing** compound side is a **schematic equational rule** — an oriented rewrite `fatherOf∘fatherOf → grandfatherOf`, not a merge (docs/equality.md, symbolic equational reasoning). Its sides are compounds by design, so the compound refusal is waived; instead it must be **orientable** into a terminating rewrite (`rewrite/orient`), or it is refused here before anything is stored. A ground `(equals (F a) (F b))` is *not* schematic — it reifies to symbols first (docs/nat.md) — and a compound that reifies to no symbol (a NAUT measure) still hits the refusal below. `rewriteOf` carries two further restrictions. It is directional, so a self-edge (the degenerate cycle, and what a sloppy import pipeline actually emits) and a longer cycle both leave the class with no head and are refused like a `genl` cycle. And **both sides must be the same role** — predicate-with-predicate, type-with-type, individual-with-individual (`roles-clash?`): rewriting a term of one kind into another is meaningless (merging `Fido` into `dog`) and a likely import bug. Unlike round one, a predicate or a type *is* now a legal `rewriteOf` target — the merge moves its trie keys, functor root, rule-index postings and `genl` closure with it (docs/equality.md). `sameAs` / `equals` stay individuals-only (OWL); `rewriteOf` is the spelling relation, so it is the one that carries vocabulary alignment across predicates and types. `(sameAs A A)` is fine — OWL makes `sameAs` reflexive.
(function-decl-problems _ [f fname :as s])reifiableFunction / unreifiableFunction declare a NAT function's kind. Their
one argument is a function name — a FruitFn-shaped constant, which reads as an
individual by the naming invariants, so prop-problems (which refuses an
individual) is the wrong check. All that matters here is the arity and that the
name is a symbol.
`reifiableFunction` / `unreifiableFunction` declare a NAT function's kind. Their one argument is a *function name* — a `FruitFn`-shaped constant, which reads as an individual by the naming invariants, so `prop-problems` (which refuses an individual) is the wrong check. All that matters here is the arity and that the name is a symbol.
(genl-problems tax [_ sub super :as s])(genlContext-problems _tax [_ sub super :as s])(inter-arg-constraint-problems _ [f pred n type m utype :as s])interArgIsa — the conditional argument constraint: a predicate, a trigger position
and type, and a target position and type. (interArgIsa eats 1 carnivore 2 meat).
The same latitude on the constrained relation arg-constraint-problems argues for, and
for the same reasons: a function has argument positions too, and a relation may be
denoted by a non-atomic term rather than named. Both positions and both types are
checked, since those are decidable from the sentence.
The two positions may be the same. (interArgIsa P 1 dog 1 mammal) says a first
argument that is a dog is also a mammal — the awkward spelling of a genl edge, but a
true claim the check will enforce, so there is nothing here to refuse. What the
positions may not be is absent or non-positive.
`interArgIsa` — the conditional argument constraint: a predicate, a trigger position and type, and a target position and type. `(interArgIsa eats 1 carnivore 2 meat)`. The same latitude on the constrained relation `arg-constraint-problems` argues for, and for the same reasons: a function has argument positions too, and a relation may be denoted by a non-atomic term rather than named. Both positions and both types are checked, since those are decidable from the sentence. **The two positions may be the same.** `(interArgIsa P 1 dog 1 mammal)` says a first argument that is a dog is also a mammal — the awkward spelling of a `genl` edge, but a true claim the check will enforce, so there is nothing here to refuse. What the positions may not be is absent or non-positive.
(inverse-problems _ [_ p q :as s])(naf-problems _ [f & _args])unknown, thereExists and the five aggregates are not assertible. They
are query operators — closed-world negation, existential closure, and a reduction
over a query's solutions — answered by a prover and never stored (docs/naf.md,
docs/aggregate.md). (unknown S) states no fact: it is a test on what the KB
derives, so stored as a premise it would be a fact with a made-up predicate that
nothing consults. (agg/count 3 ?v S) states no fact for the sharper reason
that it states a stale one: a count is a function of what is believed now, so
storing one would put a computed value under truth maintenance with no way to
invalidate it (docs/aggregate.md, "Query-only"). Belongs in a rule antecedent or
a query goal, not an assertion.
`unknown`, `thereExists` and the five **aggregates** are **not assertible**. They are query operators — closed-world negation, existential closure, and a reduction over a query's solutions — answered by a prover and never stored (docs/naf.md, docs/aggregate.md). `(unknown S)` states no fact: it is a *test* on what the KB derives, so stored as a premise it would be a fact with a made-up predicate that nothing consults. `(agg/count 3 ?v S)` states no fact for the sharper reason that it states a *stale* one: a count is a function of what is believed now, so storing one would put a computed value under truth maintenance with no way to invalidate it (docs/aggregate.md, "Query-only"). Belongs in a rule antecedent or a query goal, not an assertion.
(negation-cycle tax concluders rule)Search the rule dependency graph for a cycle through negation created by adding
rule node rule, and describe it — a vector of strings naming the nodes and
edges around the cycle — or nil if there is none.
A rule node is {:id :label :antecedent-preds :exception-preds}; concluders
maps a predicate to the rule nodes concluding it, and must include rule itself
under its own consequent, since a rule being asserted is not stored yet and a
self-referential exception (a rule excepting on what it concludes) is exactly a
one-rule cycle.
Only cycles through rule are looked for. Every rule assert and every genl edge
assert runs this check, so the stored graph is already free of them and whatever
is being added can only close a cycle that passes through it. For a rule that
start node is the rule itself; for a taxonomy edge, which passes through no
single rule, the caller starts the walk at each rule carrying an exception —
complete, because every cycle through negation crosses a negative edge and
negative edges leave excepted rules only.
The search state is [rule negative?] rather than the rule alone: a node reached
with and without a negative edge behind it are different states, since only the
negative one closes a bad cycle — that is what keeps positive recursion (which
reaches the start with negative? false, and stops there) accepted. Rules are
few, so a plain DFS with no cleverness is right.
Search the rule dependency graph for a cycle through negation created by adding
rule node `rule`, and describe it — a vector of strings naming the nodes and
edges around the cycle — or nil if there is none.
A rule node is `{:id :label :antecedent-preds :exception-preds}`; `concluders`
maps a predicate to the rule nodes concluding it, and must include `rule` itself
under its own consequent, since a rule being asserted is not stored yet and a
self-referential exception (a rule excepting on what it concludes) is exactly a
one-rule cycle.
Only cycles through `rule` are looked for. Every rule assert and every genl edge
assert runs this check, so the stored graph is already free of them and whatever
is being added can only close a cycle that passes through it. For a *rule* that
start node is the rule itself; for a *taxonomy edge*, which passes through no
single rule, the caller starts the walk at each rule carrying an exception —
complete, because every cycle through negation crosses a negative edge and
negative edges leave excepted rules only.
The search state is `[rule negative?]` rather than the rule alone: a node reached
with and without a negative edge behind it are different states, since only the
negative one closes a bad cycle — that is what keeps positive recursion (which
reaches the start with `negative?` false, and stops there) accepted. Rules are
few, so a plain DFS with no cleverness is right.(prop-problems _ [f pred :as s])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 |