vaelii.impl.inherit — com.vaelii/vaelii 0.1.0

Argument-position preservation — when a claim about one term licenses the same claim about another.

(largerThan dog cat) says something about two kinds. Whether it also says something about a golden retriever and a maine coon is not decidable from the sentence: it depends on whether the relation distributes over the kinds' members. Some relations do (disjoint — subtypes of disjoint types are disjoint) and some emphatically do not (a chihuahua is a dog, a maine coon is a cat, and the maine coon is bigger). So it is declared, per predicate, per argument position:

(argPreserving        P n R)   ; a stored (P … w …) licenses (P … a …) when (R a w)
(argPreservingInverse P n R)   ; …licenses it when (R w a)

R is any transitive relation — genl and genlContext through their cached closures, or a predicate declared (transitive R) walked over stored facts. A declaration over anything else is refused at assert (wff/arg-preserving-problems): the reach is walked to a fixpoint, so a relation that was never said to compose would have transitivity manufactured for it, and (argIsa argPreserving 3 transitivePredicate) cannot say so — argIsa is open-world, and an untyped relation cannot violate it. Naming the relation is what keeps this from being a genl special case: an argument can equally be preserved along partOf, connectedTo, or anything else transitive. The inverse form exists so the other direction never requires declaring an inverse predicate that has no other purpose.

Several declarations may name one argument position; their reaches union, since each independently licenses the claim.

Preservation stays on one side of the type/instance line

genl relates types, so (largerThan dog cat) preserved along genl reaches golden_retriever and maine_coon and stops there. It says nothing about Rex and Whiskers, and that is not a gap here to fill: relationKind is a disjointMetatype over typeRelationPredicate and instanceRelationPredicate, so one predicate symbol relates kinds or instances and never both. A largerThan that inherited across the line would be a predicate of both kinds at once, which the KB's own meta-ontology refuses.

Preservation moves an argument along a relation, leaving the predicate and the level it lives at alone. Crossing the line is a different claim — it links two predicates and has a quantifier reading to pin down (every member? some member?) — and the vocabulary for it is (typeToInstancePred TypePred InstancePred), which the engine does not yet act on.

Specificity, and why it is not the deleted axis

The interesting case is a claim that inherits and a more specific claim that disagrees. (typicallyLargerThan dog cat) reaches [chihuahua maine_coon]; (typicallyLargerThan maine_coon chihuahua) is stated directly. The stated one wins, and the general one simply does not fire for that pair — undercutting, not defeat. Nothing is derived, so there is nothing to arbitrate.

That matters, because docs/nmtms.md deleted genl-based specificity as an arbitration axis on the grounds that it was inference about the knowledge rather than from it: it scored a type by the size of its up-closure, a numeric proxy that tied silently whenever the exception was not keyed on a narrower type. Nothing here reconstructs an ordering. Two claims are compared along the very relation the inheritance travels down — [maine_coon chihuahua] is below [cat dog] because (genl maine_coon cat) and (genl chihuahua dog) are edges the KB holds. Claims that are genuinely incomparable are not ranked at all; they come back :ambiguous, which is the same answer the engine gives every other unresolvable clash.

Strict versus typical, for free

A :monotonic claim is never undercut. Strength already propagates from a justification's antecedents, so (largerThan dog cat) asserted {:strength :monotonic} inherits as known-true and a contrary specific claim is a contradiction — checks/asymmetry-problem refuses it — while (typicallyLargerThan dog cat) at the default :default inherits defeasibly and yields to the specific claim. One declaration, both behaviours, and the difference is stated where it belongs: on the claim, not on the vocabulary.

Ground goals only. An open argument is left to the fact and rule provers, in the shape different and the NAF operators already use — enumerating it would mean walking the inverse reach of every stored witness, which is a different and much larger question than the one a closed goal asks.

*memo* clj

A per-question cache for the two reads every layer here repeats — an atom of {[:positions pred context] -> …, [:reach rel inverse? x context] -> set}, or nil for no memoization.

Answering one ground goal asks for a predicate's declared positions from applicable?, verdict, surviving and claims, and for a term's reach once per preserved position and then again per pair of claims inside undercut?. Neither answer can change while the question is being answered — a query never mutates belief — so the memo is created fresh per top-level question and needs no invalidation protocol at all. with-memo reuses an outer one when a caller has already opened it, which is the discipline observe/*reach-memo* follows for the transitive closure.

*retrieval* clj

Which of the two paths finds the claims: :auto weighs the extent against the product per goal, :extent and :product force one. The forcing values exist so a test can hold the two against each other on the same KB — they answer the identical claim set by construction (both filter matches-visible by the same in-product?), and inherit_oracle_test is the claim that they do.

claims clj

(claims kb goal context)

Every believed claim bearing on the ground goal (P a1 … an), each tagged with the argument tuple it is stated at and whether it argues :for or :against.

Against comes from two places: an explicit (not (P …)) at a tuple in range, and — when P is declared asymmetric — the converse (P … y … x …), since a relation that cannot hold both ways is denied by its own mirror. The converse is only read for a binary goal, which is the only arity for which asymmetric means anything.

Every probe is made, and one tuple can yield several claims. A tuple where both P and (not P) are believed is a contradiction the KB already reports through (contradictions kb); taking whichever probe answered first would have this read it as a clean :for and hand verdict a decision that the engine, looking at the same two sentexes, refuses to make. Collecting both sends it to verdict as the :ambiguous it is. The price is two probes per tuple rather than short-circuiting on the positive (three for an asymmetric predicate) — the two :against sources are kept separately rather than folded, since they can be believed at different strengths and undercut? reads that per claim.

The converse probe is skipped at a self tuple [a a], where it would read the very sentex the positive probe just read and file it as opposition. That is one fact disputing itself, not two claims disagreeing, and it is the one shape where collecting both polarities would manufacture the dilemma rather than report it. ((P a a) under an asymmetric P is wrong — asymmetry implies irreflexivity — but it is wrong in a way contradictions does not report either, so answering :ambiguous here would be this function inventing a verdict on its own.)

declarations clj

The two declaration functors, mapped to whether they read R backwards.

declared clj

(declared kb)

Every declaration's [P R] pair — the predicate that inherits, and the relation it inherits along — read off the functor roots rather than through matches-visible.

Deliberately not context-scoped and not belief-filtered, because the callers are vaelii.impl.special's exception re-check triggers, and a trigger must be conservative in the direction the answer is: a declaration this edge cannot see still qualifies a rule in some context that can, and a missed trigger leaves a conclusion blocked (or unblocked) on evidence that has since moved. Over-queueing costs a level-6 query at the next settle; under-queueing is a wrong belief.

Costs one set-cardinality read per functor on a KB that declares none, which is nearly all of them, and the callers are additionally gated on some rule carrying an exceptWhen at all — so the record fetches here are paid only by a KB using both features.

declared-about? clj

(declared-about? kb pred)

Could any stored declaration name pred? The declaration functors' roots intersected with the argument root at position 1, where a declaration's predicate sits — one set intersection per functor, against a root that is empty for nearly every KB and tiny for the rest.

This is a gate, not an answer: it is neither belief-filtered nor context-scoped, so a true says only that the real read is worth making. A false is exact, because a declaration naming pred would be in that intersection whatever anyone believes about it. That is also what makes it the right question for a conservative caller that wants no answer at all, only "could preservation be in play here": settle/cross-argument-predicate? reads it to decide whether an exception conjunct's arguments may be compared with a trigger's, where an under-selection is a missed withdrawal.

It earns its place on the query path rather than the assert path. positions is read by ArgPreservingProver.applicable? and by provers/shadowing-channels, so it runs for every goal's functor in the KB, and each real read is two matches-visible calls. Ungated, one declaration anywhere made a genl goal cost 2.8x what it costs in a KB with none — a tax every query pays for a feature almost none of them use.

Two stages, because the two questions have different prices and different answers. The cardinality read is O(1) and false for nearly every KB there is, so it comes first and nothing else runs; the intersection is a real (if small) index read and only a KB that declares something ever pays it.

ground-goal? clj

(ground-goal? goal)

A closed positive literal this can speak about.

A negated goal is left alone: (not (P a b)) asks whether the claim is refuted, and an inheritance that only ever licenses claims has nothing to say about that — :against here means "not licensed", the open-world reading, not "licensed to be false".

positions clj

(positions kb pred context)

[{:n :rel :inverse?} …] — the preserved argument positions declared for pred, visible from context, whose relation is one this may actually walk. Empty (the overwhelmingly common case) means the predicate inherits nothing and every consumer here is a no-op.

Several declarations may name one position; they are not collapsed here, because their reaches union (reach) rather than compete.

Realized rather than lazy, and memoized on [pred context]: four layers of one question ask for this, and each computation is two matches-visible calls.

Behind a root-intersection gate on any declaration naming pred at all, so a predicate nobody declared about — which is every predicate but a handful, in every KB — pays one intersection against an empty root rather than two index lookups. The same shape of gate special.clj puts in front of the exception re-check triggers, for the same reason.

surviving clj

(surviving kb goal context)

The believed claims bearing on goal that a strictly more specific one has not displaced, each carrying its :polarity and :class. The raw material both consumers read: the prover turns it into a verdict, and checks/asymmetry-problem asks the narrower question of whether any survivor is known-true.

usable-relation? clj

(usable-relation? tax rel context)

May a declaration's R be walked? Either the engine owns its closure, or the KB says it composes. Read at use and not only at assert, so retracting (transitive R) stops the inheritance it licensed the way retracting anything else here does — the declaration is stored, but a relation nobody currently says is transitive is one whose reach we have no right to close. Read from context, like the declaration itself: a transitivity claim some invisible microtheory makes is not a licence this one holds.

verdict clj

(verdict kb goal context)

What the preserved claims say about the ground goal:

:for — some claim reaches it and nothing surviving disagrees :against — the surviving claims deny it :ambiguous — surviving claims disagree at incomparable specificity, which is a dilemma and is deliberately not decided here nil — nothing bears on it, or the predicate declares no preserved position

Claims displaced by a strictly more specific one drop out first; that is where a general default yields to a specific statement without either being defeated.

virtual-relations clj

The relations witness-terms walks from a cached closure of the engine's own rather than from stored (R a b) facts — the type hierarchy and the context hierarchy. Both are transitive by construction, so there is no (transitive R) declaration to demand of them and none possible; every other relation must carry one, which is what wff/arg-preserving-problems reads this set to decide.

with-memo clj macro

(with-memo & body)

Answer body under a memo, reusing the enclosing one when there is one.

witness-terms clj

(witness-terms kb {:keys [rel inverse?]} x context)

The terms a claim's argument may be stated of for it to reach x at this position: {w : (rel x w)} for argPreserving, {w : (rel w x)} for the inverse form. Reflexive, so x itself is always among them and a directly-stated claim is found by the same walk as an inherited one.

One declaration's reach. Callers want a position's, which is the union over the declarations made at it — reach.

The genl walk is scoped to context, exactly as fact-reach is: a claim travels along the edges the asking context can see and no others, or a microtheory would inherit (largerThan dog cat) down to a subtype some invisible theory declared. genlContext stays global — the context closure is (docs/taxonomy.md, the stated exception), and a preservation along it is a claim about the topology, which is universal.

Memoized on [rel inverse? x context] for the life of one question. The virtual relations read a cached closure and would survive without it; a fact-relation is the one that must not be re-walked, since each walk costs a matches-visible per node and undercut? asks for the same term's reach once per pair of claims.