vaelii.impl.special — com.vaelii/vaelii 0.1.0

The special-predicate dispatch table: what each functor the engine interprets means to the derived state around the store, stated once, with both halves of every meaning side by side.

A special predicate needs behaviour in four places — reflecting a stored sentex into the caches, the removal mirror, recover's cache-only replay, and wff's per-functor well-formedness check — and the compiler cross-checks none of them, so the enumeration lives once here: entries maps each functor to its arms,

:integrate (fn [kb sentex handle]) reflect a newly stored sentex into the caches :disintegrate (fn [kb sentex]) the mirror, reference-counted on (:id sentex) :rebuild (fn [tax sentex]) recover's cache-only replay — no re-check posting, no migration, no universal lifting, because the store already holds what those side effects produced :wff (fn [tax sentence]) structural well-formedness (vaelii.impl.wff keeps the check fns; the table points at them) :derived? bool the :integrate arm also runs on the derivation path (see integrate-transitive)

and check-entries refuses an asymmetric entry at namespace load, so an add-side arm without its removal and rebuild halves is a build failure rather than a cache that drifts on the first retraction or restart.

Because the arms are where a special predicate's whole behaviour lives, the machinery those behaviours need lives here too: the exception re-check queue the taxonomy arms post to, the universal-predicate lifting, and the equality migration. Third layer of the engine stack (kb <- checks <- special <- integrate <- chain <- settle): everything here reads kb and checks, and the store-mutation choke points in vaelii.impl.integrate sit directly above.

check-entries clj

(check-entries entries)

Refuse an ill-formed table at namespace load, so add/remove symmetry is a structural property rather than a review item.

Two shapes are refused. An entry with some of the cache arms — an :integrate whose :disintegrate or :rebuild is missing (or any other partial triple) is exactly the mirrored-cond drift this table exists to end: the cache would fill on assert and leak on retract, or come back wrong after recover. And an entry with no arm at all, which is a typo. Returns entries unchanged so it can wrap the def.

deduce-arg-types clj

(deduce-arg-types kb entailments handle context)

Materialize the entailments checks/constraint-entailments drew over a sentence stored at handle in context — {:new [handles] :violations [v]}.

Called from both stores of new content — assert and forward chaining's place-conclusion — because what a declaration says about an argument is a claim about the predicate, not about how a particular sentence arrived. Entailing only what a caller asserted would make belief depend on arrival order, exactly as lifting only asserted content would.

deduce-lifts clj

(deduce-lifts kb sentence handle context)

Deduce sentence (stored at handle in context) into UniverseContext if its predicate is decontextualized — {:new [handles] :violations [v]}, nil when the predicate carries no declaration.

Called from both stores of new content — assert and forward chaining's place-conclusion — because a decontextualized predicate is a claim about the predicate, not about how a particular sentence arrived. Lifting only what a caller asserted would make belief depend on arrival order: declare-then-derive would leave the conclusion unlifted while derive-then-declare lifted it through lift-existing, and the two orders are the same knowledge.

The gate is a single in-memory cache read, because every assert and every placed rule conclusion pays it to find out there is nothing to do.

derive-functional-equalities clj

(derive-functional-equalities kb sentence context handle)

(functional P) plus two symbol values for the same first argument derives (equals V1 V2) rather than throwing (docs/equality.md).

equals specifically, not sameAs: the value of a functional role need not be an individual — a birthplace, a measurement — and OWL's sameAs is individuals-only. equals is the one of the three that always type-checks here.

Making it a real justification is what makes it safe. The risk of auto-inference is that one wrong functional declaration silently merges two real individuals across the whole KB — so the merge is justified by [both facts, the declaration], why names exactly which declaration and which two facts caused it, and retracting any one of them runs the ordinary sweep and un-merges. An opaque merge would be dangerous; an inspectable, reversible one is knowledge.

Gated on the taxonomy's :functional mark before it reads the store. This runs on every asserted fact and the store read is a sentexes-matching over an unscoped context, so on a KB that declares nothing functional — the common case, and every bulk load — the mark is what stands between an assert and an index query per fact to learn what an O(1) set lookup answers. The mark is maintained by the same table entry that stores the declaration and replayed by recover, so it holds exactly when the query finds something; the unscoped arity is what keeps that equivalence, since the query under it names no context either. The handle comes from the store, because a justification needs the declaring sentex itself, and only the true branch pays for it.

derived-sentex-added clj

(derived-sentex-added kb sentex handle)

The derivation-path add choke point: everything that must happen because a derived sentex landed in the store — the closure-reaching integration above, and the exception re-check post, since a derived fact is a re-check trigger like an asserted one (an exception may be stated over a predicate that only ever arrives by inference — the cried-wolf case, where liar is concluded by another rule).

Lives here rather than beside sentex-added in vaelii.impl.integrate because the equality arms are themselves derivation sites: a migrated twin and a functional-inferred equals are derived sentexes, and hand-rolling this pair at those sites is exactly the copy-paste the choke points exist to end. Callers: forward chaining's place-conclusion, migrate-sentex, derive-equality.

disintegrate-sentex! clj

(disintegrate-sentex! kb sentex)

The mirror walk: reverse a departing sentex's cache effects through the :disintegrate column, or the matching structural arm. Every cache below is reference-counted on the departing sentex's id, so an entry survives while another sentex still asserts the same claim.

entail-existing clj

(entail-existing kb sentence dh)

When an (argIsa P n T) / (argGenl P n T) / (interArgIsa P n T m U) declaration arrives, draw what it now says about the (P …) sentexes already stored — so a declaration arriving after the facts reaches them exactly as one arriving before reaches the facts that follow. Same {:new :violations} result, so the types it mints are chaining seeds like any other new content. nil when sentence is not an argument constraint.

Two of interArgIsa's three arrival orders are covered here and at the door; the third — the trigger's type arriving after both the fact and the declaration — is the family's documented open-world non-reach (docs/taxonomy.md, "What each constraint does in each arrival order"), and argIsa has it too from the other side.

Sweeps what is stored, not what is believed, for lift-existing's reason: a type minted off a defeated fact is justified by that fact and so is defeated too — the JTMS already says what a disbelieved antecedent means — whereas skipping it would leave the type missing when the fact revives, which is belief depending on the order the defeat and the declaration arrived in.

The extent is read off the functor root, which is the precise answer to "every stored (P …)", and snapshotted before the first mint: a minted (T x) posts to the roots the walk is reading, and no index backend promises whether a posting read is a snapshot or a live view.

entries clj

The special-predicate dispatch table, as an ordered vector of [functor spec] pairs — ordered because rebuild-taxonomy replays it top to bottom and a rebuild arm may read what an earlier one wrote (metatype membership reads the marks; nothing else is order-sensitive today, and keeping the assert path's traditional order costs nothing). table below is the lookup view.

This vector is the functor enumeration: integrate, disintegrate, rebuild and wff all walk it, so a predicate added here is added to all four at once and check-entries refuses it half-done.

equate-existing clj

(equate-existing kb sentence)

When a (functional P) declaration arrives, derive the equalities P's already stored facts license — the other direction of derive-functional-equalities, which is a fact meeting the declaration. nil when sentence declares nothing functional.

A declaration has to reach the facts already stored exactly as it reaches the facts that follow, which is the rule entail-existing states for the argument constraints and holds here for the same reason: whether two spellings denote one woman is a question about the KB's content, and an answer that depended on whether the schema or the facts were loaded first would be an answer about the file. Written the ordinary way — declaration first, then the facts — this finds an empty extent and costs one functor-root read.

Each fact is handed to derive-functional-equalities, which asks the same question from the other side, so the two directions cannot drift about what a functional slot licenses or what justifies the merge: the equality names both facts and this declaration whichever way round it was reached, and retracting any of the three un-merges. Re-deriving is idempotent — same-class? skips a pair the closure already holds and has-justification? skips an argument it already has — so a slot filled by three values collapses to one class rather than to the first pair walked.

Sweeps what is stored rather than what is believed, for entail-existing's reason: an equality derived off a defeated fact rests on that fact and is defeated with it, where skipping it would leave the merge missing when the fact revives — belief depending on the order the defeat and the declaration arrived in. The extent is read off the functor root and snapshotted before the first merge, since migration writes twins to the roots the walk is reading.

inadmissible clj

(inadmissible kb sentence context)

The violation that stops sentence from being stored in context, or nil — naming, the definitional constraints, well-formedness, and edge stratification, as one value.

This is the triple place-conclusion runs over a rule's conclusion, and it holds of any content the engine mints on its own behalf: a (T x) can clash with a disjoint membership, a (genl X T) edge can close a taxonomy cycle or a cycle through negation, and a type used at the wrong arity is not a type membership at all. Three callers ask it — the argument-type entailment below, forward chaining, and abduction, which asks it before minting a hypothesis so that a sentence no assertion could legally make is never one the search assumes.

A value, never a throw. Two of its callers run after their triggering sentex is stored (that is what gives them a handle to be justified by) and inside a fixpoint, neither of which may abort halfway; the third would rather refuse a hypothesis than fail the query that wanted it.

index-exceptWhen-meta clj

(index-exceptWhen-meta kb meta-sentex)

Register the exceptWhen meta-sentex meta-sentex in the re-check index: post the rule it names under each predicate its query mentions and into the :rules roster, and queue the rule for a blanket re-check (a fact may already have arrived that its new exception blocks).

index-rule-sentex clj

(index-rule-sentex kb handle rule-sentex)

Index a rule handle by all of its predicates — both sets are complete, so rules-by-consequent answers "what could conclude P?" for a forward-only rule too.

Only the predicates are indexed. The record is the source of truth for what a rule may do: a set/*Rule wrapper canonicalizes into the sentex (see vaelii.impl.sentex), and :direction / :defeasible are read off it by every consumer. Nothing enumerates rules by defeasibility any more — defaults fire from the same agenda as strict rules — so there is no default-rule index to maintain.

A rule is not a table entry: its trigger is the shape of the sentence (any functor can head an implication), so it is the structural arm of the integrate-sentex walk below, and this is its add half.

integrate-sentex clj

(integrate-sentex kb sentex handle)

Reflect a newly stored sentex into the taxonomy / rule index / disjointness — the :integrate column of the table, walked, plus the structural arms above.

Returns {:new [handles] :superseded [[datum reason]] :violations [v]} for an equality sentex — the twins it created are chaining seeds and the violations are the caller's to report — and nil for everything else. (Only the equality arm has anything to say; every other arm mutates a cache and its return value is whatever that mutator handed back, so the result is normalized here rather than left for the caller to sort out.)

integrate-transitive clj

(integrate-transitive kb sentex handle)

The derivation-path subset of integrate-sentex: only the arms flagged :derived? — the genl / genlContext closure edges — run for a rule-derived conclusion, because the rest of integration either does not apply to a derived sentex or would re-enter assert from inside forward chaining. Without this on the derivation path, a rule concluding (genl a b) stored and believed the sentex while the taxonomy never learned the edge — and recover, which reads the store, then disagreed with the running KB about what the KB entailed. (A derived equality takes its own arm through derive-functional-equalities, which is the one derivation that concludes one.)

integrate-twin clj

(integrate-twin kb sentex handle)

Full integration for a migrated twin — a restated declaration or fact the equality migration derives (migrate-sentex). A twin must reach the same caches an asserted declaration would, or its class-representative spelling is stored and believed while the taxonomy never learns what it declares: a merged (disjoint dog cat) twin (disjoint canine cat) must reach add-disjoint, a (transitive containedBy) twin must reach mark-prop, and a migrated rule twin must reach the rule index or it never fires. So this runs the same arms integrate-sentex does — the fuller integration derived-sentex-added (the forward-chaining conclusion path) deliberately narrows to the genl closure edges.

The equality arm is skipped: a twin is never an equality sentex (those are held back from migration, kb/rewritable-sentex?), and running migrate-class from inside a migration would recurse. Then the same re-check post every derived sentex gets — a migrated fact / declaration arriving is a trigger like an asserted one.

Migration can run inside a forward-chaining pass (derive-functional-equalities infers an equality from a derived fact), so the table/structural arms can fire mid-fixpoint. That is safe: none of them re-enter assert or chain — they add cache entries, justifications, and re-check queue items — and the common functional merge is of two individual values, whose twins are facts that match no declaration arm at all.

migrate-sentex clj

(migrate-sentex kb sentex)

Restate one stored sentex under its terms' representatives — once per reader whose election differs, not once per sentex.

Returns {:new [handles] :superseded [[datum reason]] :violations [v]}. Five things are load-bearing:

• Re-canonicalized, not substituted. The twin is built by find-or-create from the rewritten sentence, so it goes back through the sentex constructor. A merge changes what a symmetric predicate's sorted argument order should be — (siblingOf lo mid) with lo retired in favour of a term sorting after mid has to come back as (siblingOf mid hi), not (siblingOf hi mid) — and a textual substitution would quietly store one fact under two handles.
• Justified, not asserted. The twin is a derivation from [the original, the equality], one justification per incident equality edge, so each merge is an independent witness and dropping the equality collects the twin through the ordinary dependency-directed sweep. Dedup falls out: when the rewritten form is already stored, find-or-create returns that handle and it simply gains a support.
• One twin per election, placed where the reader that elected it lives. A merge applies where it is visible, so a fact above one is read by contexts that inherit different sets of edges and elect different representatives (reader-contexts-for). The fact's own context is always a reader and takes the twin that supersedes the original; a reader below it that elects something else gets its own twin, placed in that reader's context — the restatement is the reader's, not the fact's, and putting it where the fact lives would publish it to contexts whose election it is not. Two readers electing the same form share one twin, at the more general of them.
• Checked, and dropped rather than thrown on failure. A merge can create a disjointness violation — (dog Rex) + (cat Fluffy) + a merge makes one individual both — so the same definitional checks place-conclusion runs guard this, and a failure is reported through violations. The original is then left believed: superseding a spelling whose restatement was refused would lose the caller's knowledge outright.
• A reader that changes nothing costs one rewrite. The overwhelming case is a single reader — the fact's own context — because it takes two contexts stating equalities for a second election to exist at all.

note-rule! clj

(note-rule! kb rule-sentex preds f)

Add (inc) or drop (dec) a rule in the two rosters visibility-seeds reads: the predicates it takes as antecedents, and the context it is stated in.

Both are kept here rather than derived on demand because both answer a question a genlContext edge asks and the index cannot: which predicates could a seed usefully have, and does this cone hold a rule at all. Maintained at the rule index/unindex choke points, beside :opposed at the store's, and rebuilt by recover because recovery replays rule indexing.

rebuild-taxonomy clj

(rebuild-taxonomy kb)

Rebuild the in-memory taxonomy from the durable store: the :rebuild column of the table, replayed in entry order over the stored declarations of each functor.

Drops every cache first: a rebuild that merged into the existing one could only ever add, so an entry whose sentex is gone would survive the recovery that was supposed to re-derive it.

recheck-every-exception clj

(recheck-every-exception kb)

Re-check every rule carrying an exception — the blanket trigger. Two channels take it: recover, where nothing about blocking survives a restart so every exception must be re-decided from scratch and there is no edge or fact to narrow by, and recheck-equality-edge on the sides where its own narrowing is blind — a class splitting, and a schematic rewrite arriving.

(A genlContext edge change does not come here: recheck-genlContext-edge narrows it to the excepted rules whose firings live in the moved visibility cone, the context-keyed twin of recheck-genl-edge's predicate keying.)

There is no triggering sentence here — the whole blocking state is being rebuilt — so this queues :all and every firing of every queued rule is re-evaluated.

recheck-except clj

(recheck-except kb except-sentex)

An (except (sentexHandle H)) fact arrived or left: queue every rule the visibility change touches, so settle (on arrival) sweeps a conclusion now resting on an invisible antecedent and retract! (on departure) re-derives one the fact can be seen for again. Two rule sets, because the two directions need different rules:

• the rules of firings that use H (jtms/dependents) — the conclusions to sweep when the except arrives; and
• the rules that could fire on H (rules-by-antecedent over H's predicate and its supertypes, the same fan matching does) — the conclusions to re-derive when the except leaves, since by then the firing that used H has been swept away and dependents no longer names it.

Queuing both on both directions over-approximates (the per-placement hidden-set test in chain/justification-excepted? and derive-conclusion's block narrow it), which is the safe direction — a spurious re-check costs one query, a missed one leaves a conclusion resting on an invisible fact or fails to bring one back.

recheck-except-cone clj

(recheck-except-cone kb)

A genlContext edge moved visibility for the contexts in context-down(sub), which changes not only what an exceptWhen query sees (recheck-genlContext-edge) but also which handles a believed except hides from a context in the cone — so a derivation it blocks or releases must be re-checked too. Re-queues every except's affected firings (recheck-except). Gated on the except root, so a KB using no except pays one count and stops; excepts are rare, so re-queuing all of them on a rare edge change is the cheap over-approximation.

recheck-on-sentence clj

(recheck-on-sentence kb sentence)

The re-check trigger for a whole sentence: its functor, and — for a negation — the functor of the positive body underneath, since (not (penguin X)) is content about penguin and an exception on penguin must see it come and go.

Both postings carry the whole sentence as the trigger, not the predicate they were keyed on: what narrows a firing is the arguments as well, and the negation is content about the same arguments as its body.

underlying-body, not positive-body: a genuinely negative sentence is exactly the interesting case here. (not (penguin X)) arriving is what defeats a believed (penguin X), and a re-check condition reading belief — an unknown, an aggregate's census — moves on the defeat with no fact having been stored or removed.

The body is read once and serves all three consumers: the predicate-keyed posting above, the declaration posting, and the qualitative trigger — each for the same reason, that a calculus, a declaration's subject and a predicate are named by what is under the not, never by the not.

refresh-supersessions clj

(refresh-supersessions kb)

(refresh-supersessions kb extra)

Reconcile the superseded set with the equality closure — the equality analogue of tax/refresh-beliefs, and called from the same place for the same reason.

resubsumption-seeds clj

(resubsumption-seeds kb removed)

The chaining seeds a teardown owes, given the removed sentexes its sweep collected — subsumption-seeds in the retraction direction.

A firing that matched by subsumption names one witness for the genl path it used (taxonomy/reach-support), so removing an edge on that path invalidates the justification and the dependency-directed sweep collects the conclusion. That is the point. But a reachability can outlive one of its supporters — the same edge asserted from a second context, or a second path around the one that went — and then the conclusion is still licensed and must come back. So the spec subtree under every removed edge goes back on the agenda and the rules fire again over it.

Revival is a re-derivation, at a fresh handle, exactly as it is under exceptWhen: the sweep deleted the conclusion, so there is no label to flip back. That is the price of naming a witness rather than every witness, and it is the same price the qualitative support pays for the same reason (docs/qcn.md) — carrying every route would be one justification per path through a hierarchy where paths multiply.

Two things make the reading exact.

It is taken before the teardown, while the taxonomy still holds the departing edge: specs is what decides which facts could have subsumed through it, and reading it afterwards asks the shrunken hierarchy a question about the whole one — with (genl dog mammal) gone, specs(mammal) no longer names dog, whose facts are exactly the ones that need re-joining.

And it is gated on the sweep having taken something besides the records asked for: a justification naming the departing edge is deleted with it, so a conclusion that survived kept another one and needs no re-derivation, and a conclusion that did not is in removed. So retracting an edge that licensed nothing — the common case — costs one functor read per removed record and no chaining at all.

subsumption-seeds clj

(subsumption-seeds kb sentence)

The stored facts a new (genl sub super) edge newly makes matchable, as chaining seeds — the taxonomy twin of lift-existing, and there for exactly the same reason.

Matching fans an antecedent's functor over its genl spec closure, so an edge arriving after the facts changes which antecedents they satisfy: (dog Fido) stored, then (genl dog animal), and a rule on (animal ?x) should fire. The semi-naive agenda never sees it — the arriving datum is the edge, and firing the rules keyed on genl is not the same thing as re-firing the rules the edge just connected. Without this the same three sentences derive a conclusion in one order and not the other, which is the one thing belief may not depend on (docs/nmtms.md).

The seeds are sub's whole spec subtree, because subsumption is transitive: an edge at the top of a hierarchy makes every fact below it matchable at the new supertype. Believed only — a disbelieved fact matches nothing, and it will seed the agenda itself when it revives. Cost is the subtree's extent, paid once per edge, and it is nothing on the ordinary load order (a hierarchy arrives before the facts under it, when the extent is empty).

The removal side is resubsumption-seeds below: a firing names the genl edges it subsumed through, so dropping one withdraws what it licensed — and the facts have to go back on the agenda when the reachability outlives the supporter that left.

table clj

entries as the lookup map the walks below dispatch through.

unindex-exceptWhen-meta clj

(unindex-exceptWhen-meta kb meta-sentex)

The mirror of index-exceptWhen-meta: withdraw the departing exceptWhen meta-sentex's postings, then re-post the rule from the predicates its remaining exceptions and NAF antecedents still need — a set re-add restores any shared predicate the blanket withdraw over-removed, and leaves the rule off the :rules roster exactly when nothing watches it any more. Queues the rule for re-check, since losing an exception may revive what it was blocking.

universal-context clj

visibility-seeds clj

(visibility-seeds kb sentence)

The stored facts a new (genlContext sub super) edge newly makes matchable, as chaining seeds — the context twin of subsumption-seeds, and there for exactly the same reason.

Matching fans an antecedent up the visibility cone, so an edge arriving after both the rule and the facts changes which facts the rule can see: (cFactP CA) in MidContext, a rule in LowContext, then (genlContext LowContext MidContext), and the rule should fire. The semi-naive agenda never sees it — the arriving datum is the edge, and firing the rules keyed on genlContext is not the same thing as re-joining the rules the edge just gave a wider view. Without this the same four sentences derive a conclusion in the orders that put the edge first and nothing in the others, which is the one thing belief may not depend on (docs/nmtms.md).

Both cones, because an edge pairs rules and facts in two directions. It is not only that a rule below can now see facts above: a rule stated above applies in every context that sees it, so the edge equally hands the general rule the specialized context's own facts, and places its conclusion there. Seeding is by fact, so the seeds are the believed sentexes of super's up-cone — seeing super means seeing everything super sees — together with those of sub's down-cone, the contexts a rule above is now inherited into. Taking one and not the other fixes half the orders and leaves the rest, which is worse than either: the shape that still fails is the narrower one, and so the easier to mistake for correct.

Enumerated from the rules, not from the cone, and the difference is asymptotic rather than a constant. Walking the cone and keeping the facts some rule could match costs one record fetch per sentex in the cone — so wiring N microtheories under a UniverseContext holding K facts is O(N·K) where the KB without this is O(N+K), and building a spindle D deep is O(D²) because each edge's up-cone is the whole chain above it. Measured: 3.9x on the first shape, 5x and climbing with depth on the second, and 1.8x on the starter load, which does wire contexts after filling them.

So it goes the other way. :rule-antecedents is the live roster of predicates some rule takes as an antecedent, kept O(1) at the rule index/unindex choke points beside :opposed; this walks those predicates' extents and keeps the facts whose context is in the cone. Cost is then proportional to the rule-relevant facts and independent of how much ontology the cone holds — a KB with no rules pays one map read, and the upper ontology sitting in UniverseContext is not walked because almost none of it is a rule antecedent. The cone is a set membership per candidate, so it costs nothing to ask about both cones.

And each half is gated on the other holding a rule, which is what makes the ordinary case free rather than merely cheap. Seeding super's facts is worth nothing unless some rule sits in sub's down-cone to newly see them, and seeding sub's facts nothing unless a rule sits in super's up-cone to be inherited into it. Wiring an empty microtheory under a full one — the commonest edge there is — holds no rule on the new side, so it seeds nothing at all, where without the gate it re-seeds the whole ontology above and re-joins rules that already fired on every fact of it. That is the difference between 3.9x on the shape and 1.0x, and it is not the enumeration but the chaining the seeds provoke. :rule-contexts answers it as a map read per context in the cone, and contexts are few.

The removal side needs no twin — dropping an edge narrows what a rule sees, and the ordinary dependency-directed sweep already withdraws a firing whose antecedent stopped being visible.

wff-problems clj

(wff-problems tax sentence)

Structural well-formedness problems for sentence (empty if OK) — the :wff column of the table, walked. A sentence whose functor has no entry (or no :wff arm) is structurally unconstrained here; its argument types are still checked by the argIsa constraints.

wff-violation clj

(wff-violation kb sentence)

The same check as a value, for content a rule derived rather than one a caller asserted: nil when sentence is well-formed, else a violation map in the shape checks/constraint-violation returns.

assert checks this on the way in, but a rule may conclude a special predicate — (implies (relates ?x ?y) (genl ?x ?y)) derives taxonomy edges — and the derivation path had no such check. A derived edge reaches the closure through integrate-transitive, so a rule could close a genl cycle that the same edge asserted directly would have been refused for, leaving genls/specs cyclic — and those are what matching, placement and stratification all read.

Dropped and reported rather than thrown, like every check on that path: chaining is a fixpoint and must not abort halfway through one.