Well-formedness checks for the special predicates: genl / genlCx (the type and
context hierarchies), disjoint / disjoint_metatype, and arg (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 / genlCx (the type and context hierarchies), disjoint / disjoint_metatype, and arg (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] _context)arg and genlArg — 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 — (arg 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 result 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 — (arg (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` and `genlArg` — 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 — `(arg 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 `result` 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** — `(arg (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] _context)transitiveInArg / transitiveInArgInverse — 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 arg on
argument 3 cannot express that: arg 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.
`transitiveInArg` / `transitiveInArgInverse` — 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 `arg` on argument 3 cannot express that: arg 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.
(brave-cautious-problems _ [f & args] _context)bravely and cautiously are not assertible. Each is a read on the current
dilemmas — (cautiously S) is S in every optimal labeling, (bravely S) in some —
answered by the brave/cautious prover (add-reasoner kb :brave-cautious) and never
stored. Stored as a premise it would be a computed value with no way to keep it current,
the same reason the aggregates and unknown are refused; and the prover is authoritative
and never reads such a fact. Ask it instead.
`bravely` and `cautiously` are **not assertible**. Each is a *read* on the current dilemmas — `(cautiously S)` is S in every optimal labeling, `(bravely S)` in some — answered by the brave/cautious prover (`add-reasoner kb :brave-cautious`) and never stored. Stored as a premise it would be a computed value with no way to keep it current, the same reason the aggregates and `unknown` are refused; and the prover is authoritative and never reads such a fact. Ask it instead.
(commutative-in-arg-and-rest-problems _ s _context)commutativeInArgAndRest — a predicate and a positive-integer position, and nothing
else. functional-in-arg-problems above is the shape, and the position is held to the
same positive integer for the same reason: argument positions are one-based throughout,
so position 0 names no slot.
A position past the predicate's declared arity is not refused, exactly as
functionalInArg's is not. The declaration may legitimately arrive before the arity
does, so refusing it against a visible arity would make the KB depend on which of the
two was written first — and a tail starting past the end simply forms no component, so
a literal at that arity is left alone (sentex/commuting-components). The refusal
says the mark marks a relation, since a commuting mark may name a function.
`commutativeInArgAndRest` — a predicate and a positive-integer position, and nothing else. `functional-in-arg-problems` above is the shape, and the position is held to the same positive integer for the same reason: argument positions are one-based throughout, so position 0 names no slot. **A position past the predicate's declared arity is not refused**, exactly as `functionalInArg`'s is not. The declaration may legitimately arrive before the arity does, so refusing it against a visible arity would make the KB depend on which of the two was written first — and a tail starting past the end simply forms no component, so a literal at that arity is left alone (`sentex/commuting-components`). The refusal says the mark marks a relation, since a commuting mark may name a function.
(commutative-in-args-problems _ [f pred & positions :as s] _context)commutativeInArgs — a predicate and at least two distinct positive-integer
positions.
Two positions, not one. A component of one position licences no permutation, so a
one-position declaration would be stored, believed and inert. That is also why the
arity is checked here and commutativeInArgAndRest's is not: a tail is open-ended and
may reach two positions at a higher arity, where a named set is everything it will
ever name.
Distinct positions, for the same reason read the other way: (commutativeInArgs P 1 1) names one slot twice and so names one position, which is the case above wearing a
longer spelling.
A position past the declared arity is not refused — commutative-in-arg-and-rest-problems
gives the argument.
`commutativeInArgs` — a predicate and at least two distinct positive-integer positions. **Two positions, not one.** A component of one position licences no permutation, so a one-position declaration would be stored, believed and inert. That is also why the arity is checked here and `commutativeInArgAndRest`'s is not: a tail is open-ended and may reach two positions at a higher arity, where a named set is everything it will ever name. **Distinct positions**, for the same reason read the other way: `(commutativeInArgs P 1 1)` names one slot twice and so names one position, which is the case above wearing a longer spelling. A position past the declared arity is not refused — `commutative-in-arg-and-rest-problems` gives the argument.
(context-arg-subrelation-problems _ [f fname pos rel :as s] _context)(contextArgSubrelation F pos R) declares the structural genlCx ordering for a
context-denoting function F (docs/context-nat.md): two F-contexts identical except
at argument pos are ordered by the sub-relation R on that argument — the more
specific one (its arg pos R-below the other's) genlCx the more general.
F is a function name (a Cx*Fn-shaped constant, an individual by the naming
invariants), pos a 1-based positive integer over F's arguments, and R a predicate
name. Whether pos is in F's arity is not knowable here — no declaration states an
application's arity — so it is left to the producer, which simply finds no sibling pair
to order when pos is out of range.
`(contextArgSubrelation F pos R)` declares the structural genlCx ordering for a context-denoting function `F` (docs/context-nat.md): two `F`-contexts identical except at argument `pos` are ordered by the sub-relation `R` on that argument — the more specific one (its arg `pos` `R`-below the other's) `genlCx` the more general. `F` is a function name (a `Cx*Fn`-shaped constant, an individual by the naming invariants), `pos` a 1-based positive integer over `F`'s arguments, and `R` a predicate name. Whether `pos` is in `F`'s arity is not knowable here — no declaration states an application's arity — so it is left to the producer, which simply finds no sibling pair to order when `pos` is out of range.
(correspondence-problems _ [f fname pred pos :as s] _context)(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.
(covering-constraint-problems _ [f pred a b :as s] _context)The covering argument constraints — args / argsGenl name a relation and a type,
argAndRest / argAndRestGenl a relation, a positive-integer start position, and a
type. The same latitude on the constrained relation arg-constraint-problems argues
for, and the same position and type checks, differing only in whether a start position
is present. args is argAndRest at start 1, so one check reads both arities and
takes the type from whichever position holds it.
The homogeneity constraints interArgs / interArgAndRest have the same two shapes —
a relation and a type, or a relation, a start and a type — and are read here too.
The covering argument constraints — `args` / `argsGenl` name a relation and a type, `argAndRest` / `argAndRestGenl` a relation, a positive-integer start position, and a type. The same latitude on the constrained relation `arg-constraint-problems` argues for, and the same position and type checks, differing only in whether a start position is present. `args` is `argAndRest` at start 1, so one check reads both arities and takes the type from whichever position holds it. The homogeneity constraints `interArgs` / `interArgAndRest` have the same two shapes — a relation and a type, or a relation, a start and a type — and are read here too.
(covering-problems tax [f whole & parts :as s] _context)covering and partition — a whole followed by two or more distinct parts.
What is checked is what the declaration cannot mean. A missing (genl part whole)
edge is not among it: the declaration states that edge rather than requiring one, so
demanding it here would refuse every cover written before its parts and make the answer
a function of assertion order. What is refused is a shape no edge could be installed
for — a part that is the whole, and a part the closure already places above the whole,
where the edge would close a cycle genl-problems refuses in as many words. A part
disjoint from the whole is stored, and the clash is reported (the header note).
The cycle read is global, as genl-problems' is (E17_ROSTER): the edge the cover
installs closes a cycle in the whole edge set whichever context holds the edge above
it, so a part a sibling context places above the whole is refused here as the bare
genl would be.
`covering` and `partition` — a whole followed by two or more distinct parts. What is checked is what the declaration *cannot* mean. A missing `(genl part whole)` edge is not among it: the declaration states that edge rather than requiring one, so demanding it here would refuse every cover written before its parts and make the answer a function of assertion order. What is refused is a shape no edge could be installed for — a part that is the whole, and a part the closure already places above the whole, where the edge would close a cycle `genl-problems` refuses in as many words. A part disjoint from the whole is stored, and the clash is reported (the header note). The cycle read is global, as `genl-problems`' is (E17_ROSTER): the edge the cover installs closes a cycle in the whole edge set whichever context holds the edge above it, so a part a sibling context places above the whole is refused here as the bare `genl` would be.
(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] _context)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.
(equality-problems tax [f a b :as s] _context)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 → grandfather_of, 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 structural NAT 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 Muffet into dog) and a likely
import bug. A predicate or a type is a legal rewriteOf
target — the merge moves its trie keys, predicate extent, 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 → grandfather_of`, 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 structural NAT 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 `Muffet` into `dog`) and a likely import bug. A predicate or a type *is* a legal `rewriteOf` target — the merge moves its trie keys, predicate extent, 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] _context)reifiable_function / unreifiable_function declare a NAT function's kind. Their
one argument is a function name — a FruitFn-shaped constant, which is indistinguishable from 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.
`reifiable_function` / `unreifiable_function` declare a NAT function's kind. Their one argument is a *function name* — a `FruitFn`-shaped constant, which is indistinguishable from 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.
(functional-in-arg-problems _ s _context)functionalInArg — a predicate and a positive-integer position, and nothing else.
arg-preserving-problems above is the near neighbour and the difference is the third
argument it has and this does not: transitiveInArg names a relation the argument is
preserved along, and has to refuse a non-transitive one because inherit would walk
it to a fixpoint and manufacture transitivity for it. functionalInArg licenses
nothing and walks nothing — it refuses tuples — so there is no relation to name and no
such restriction to impose. The two share a name shape and sit on opposite sides of
the prover/checker divide; props-over's docstring draws the same line.
The position is held to a positive integer for the reason
arg-preserving-problems holds its own: argument positions are one-based throughout,
so (functionalInArg P 0) names no slot. That an n exceeding the predicate's
declared arity is not refused here is deliberate and matches arity's own
open-worldness — the declaration may legitimately arrive before the arity does, and a
position past the end simply never matches a tuple.
The predicate is held to what prop-problems holds its subject to rather than to
arg-preserving-problems' looser symbol-or-compound test: this mark is read off a
sentence's functor, and a functor is a symbol.
`functionalInArg` — a predicate and a positive-integer position, and nothing else. `arg-preserving-problems` above is the near neighbour and the difference is the third argument it has and this does not: `transitiveInArg` names a relation the argument is preserved *along*, and has to refuse a non-transitive one because `inherit` would walk it to a fixpoint and manufacture transitivity for it. `functionalInArg` licenses nothing and walks nothing — it refuses tuples — so there is no relation to name and no such restriction to impose. The two share a name shape and sit on opposite sides of the prover/checker divide; `props-over`'s docstring draws the same line. The position is held to a **positive** integer for the reason `arg-preserving-problems` holds its own: argument positions are one-based throughout, so `(functionalInArg P 0)` names no slot. That an `n` exceeding the predicate's declared arity is not refused here is deliberate and matches `arity`'s own open-worldness — the declaration may legitimately arrive before the arity does, and a position past the end simply never matches a tuple. The predicate is held to what `prop-problems` holds its subject to rather than to `arg-preserving-problems`' looser symbol-or-compound test: this mark is read off a sentence's functor, and a functor is a symbol.
(genl-negation-cycle tax readers sub super)The cycle through negation the edge (genl sub super) closes, described as
negation-cycle describes one, or nil. tax holds the edge already; readers is the
stored graph's (checks/stratification-readers).
The edge adds the graph edges from each rule reading a predicate at or above super
to each rule concluding a spec of sub, so a cycle the edge closes uses one of them.
The walk starts at the rules reading a predicate in genls-global(super), in content
order, and goes against the graph's edges (negation-walk). It closes at a rule
concluding a spec of sub when a negative edge is on the path or the edge from the
start is negative. It reads only the rules those starts reach, and finds only cycles
through the new edge, so a cycle already stored refuses no edge that does not reach it.
A genlCx edge needs no walk: the graph's edges read the genl closure alone.
The cycle through negation the edge `(genl sub super)` closes, described as `negation-cycle` describes one, or nil. `tax` holds the edge already; `readers` is the stored graph's (`checks/stratification-readers`). The edge adds the graph edges from each rule reading a predicate at or above `super` to each rule concluding a spec of `sub`, so a cycle the edge closes uses one of them. The walk starts at the rules reading a predicate in `genls-global(super)`, in content order, and goes against the graph's edges (`negation-walk`). It closes at a rule concluding a spec of `sub` when a negative edge is on the path or the edge from the start is negative. It reads only the rules those starts reach, and finds only cycles through the new edge, so a cycle already stored refuses no edge that does not reach it. A `genlCx` edge needs no walk: the graph's edges read the `genl` closure alone.
(inter-arg-constraint-problems _ [f pred n type m utype :as s] _context)interArg — the conditional argument constraint: a predicate, a trigger position
and type, and a target position and type. (interArg 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. (interArg 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.
`interArg` — the conditional argument constraint: a predicate, a trigger position and type, and a target position and type. `(interArg 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.** `(interArg 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.
(naf-problems _ [f & _args] _context)unknown, thereExists, forall and the five aggregates are not assertible:
they are query operators, answered by a prover and never stored. A stored (unknown S) would be a fact nothing consults, since the prover answers it; a stored count
would be stale (docs/aggregate.md, "Not assertible, and nothing is stored").
`unknown`, `thereExists`, `forall` and the five **aggregates** are **not assertible**: they are query operators, answered by a prover and never stored. A stored `(unknown S)` would be a fact nothing consults, since the prover answers it; a stored count would be stale (docs/aggregate.md, "Not assertible, and nothing is stored").
(negation-cycle tax readers 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 :consequent-pred :concludes-any?}; readers maps a predicate to the rule nodes reading it, and must
include rule itself under each predicate it reads, 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 a check, so whatever is being added can only close a cycle that passes
through it. The walk runs from rule against the edges and closes on reaching it
again with a negative edge on the way (negation-walk).
Which cycle is returned, when several pass through rule, is decided by content:
the walk takes each upward closure in content order, and readers must answer each
predicate's rules in content order (checks/stratification-readers does).
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 :consequent-pred
:concludes-any?}`; `readers` maps a predicate to the rule nodes reading it, and must
include `rule` itself under each predicate it reads, 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 a check, so whatever is being added can only close a cycle that passes
through it. The walk runs from `rule` against the edges and closes on reaching it
again with a negative edge on the way (`negation-walk`).
Which cycle is returned, when several pass through `rule`, is decided by content:
the walk takes each upward closure in content order, and `readers` must answer each
predicate's rules in content order (`checks/stratification-readers` does).(type-pair-problems _ [f a b :as s] _context)(orthogonal a b) and (siblingDisjointException a b) — two arguments, neither an
individual. One type named twice is not refused here: a type subsumes itself, so the
declaration contradicts the taxonomy, and decide.related reports that clash as it
reports one over two genl-related types.
`(orthogonal a b)` and `(siblingDisjointException a b)` — two arguments, neither an individual. One type named twice is not refused here: a type subsumes itself, so the declaration contradicts the taxonomy, and `decide.related` reports that clash as it reports one over two genl-related types.
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 |