vaelii.impl.context-nat — com.vaelii/vaelii 0.24.0

The structural genlCx producer for reified-NAT contexts — docs/context-nat.md.

A (contextArgSubrelation F pos R) declaration says two F-contexts identical except at argument pos are ordered by the sub-relation R on that argument. This namespace reads the declarations and the context NATs of F from the store and materializes the genlCx edges they entail: for two siblings whose pos arguments stand in R, the more specific one (its argument R-below the other's) is deduced to genlCx the more general, as a justified sentex in CxUniverse. So the edge belief-follows for free — retract a context (its termOfUnit map), the declaration, or the R-evidence, and the ordinary JTMS relabel withdraws it. It is never a premise anyone asserted.

R is resolved by a bounded oracle, because the producer runs on the assert maintenance path and a genlCx edge feeds the taxonomy closure a relabel loop reads — so a prover search is out (docs/naf.md): either a registered pure structural comparator (the datetime one, keyed on subintervalOf over DatetimeFn terms) answers it, or a believed stored (R a b) fact does. A comparator answer is a pure function of the two expressions, already carried by the termOfUnit antecedents, so it needs no extra supporter; a stored fact contributes its own handle so defeating it withdraws the edge.

Materialization reuses the derived-sentex pattern special/deduce-lift uses: find-or-create-sentex, then special/derived-sentex-added to reach the genlCx closure and post the re-check triggers, then a JTMS justification under the contextArgSubrelation informant — and then, on the transition into belief, special/reconcile-context-edge, the same entry point the assert and rule-conclusion paths call. A genlCx edge widens which merges a context can see, and an edge nobody asserted widens it exactly as much as one somebody did (vaelii#56); the merge it yields is handed back up to core, which owns the follow-through.

any-context-subrelations? clj

(any-context-subrelations? kb)

Cheap gate: does the KB declare any contextArgSubrelation? The producer is a no-op otherwise — one O(1) functor count per assert, the shape nat/any-corresponding-predicates? has.

reconcile-genlCx clj

(reconcile-genlCx kb sentence)

The structural-genlCx maintenance a just-asserted sentence calls for, scoped to the sibling pairs it can have changed:

• a (contextArgSubrelation F …) declaration reconciles every pair of F's contexts;
• a (termOfUnit K E) map with K a cx/ constant — the mint of a context — reconciles the pairs K is in, since a new context is what creates a sibling pair;
• an (R a b) fact on a declared sub-relation reconciles the pairs whose ordered arguments are a below b, in the functions declared to order by R. A comparator dimension needs nothing but the contexts, but a dimension resolved by stored facts has the evidence arrive on its own schedule.

Any other fact, including one stored into a cx/ context that already exists, creates no pair and reconciles nothing. A no-op — one functor count — on a KB that declares no contextArgSubrelation.

Returns what the edges it computed merged — {:new :superseded :violations}, or nil when they merged nothing. A computed edge widens which merges a context can see exactly as a stated one does, and the caller owes it the same follow-through (core/assert).

reconcile-revivals clj

(reconcile-revivals kb)

Rebuild the structural genlCx edges for every declared contextArgSubrelation function — the build direction a belief revival needs, which reconcile-genlCx (only ever called from the assert choke-point) cannot serve.

Belief of a contextArgSubrelation declaration — or of a stored (R a b) evidence fact — can flip OUT→IN with no assert: retracting a monotonic defeater above it revives it. The JTMS revives a justification that already exists, but an edge the producer never built (because the declaration was OUT when the contexts were stored) has no justification to revive, so the edge would stay absent. A teardown therefore re-runs the producer once its belief has settled, and the withdraw direction the JTMS already handles meets a build direction here.

Idempotent (materialize-edge adds no duplicate justification) and local: scoped to the declared context functions, each reconciled only over its own contexts — bounded by the context-NAT population, never the whole graph. Behind the free in-memory context_denoting_function gate first — a KB with no cx/ context to order pays neither the any-context-subrelations? functor-count index read nor anything else, so the retract hot path is untouched on every KB that declares no context function (assert_cost_test).

Returns the merged {:new :superseded :violations} of whatever it rebuilt, or nil — a revived edge widens an ancestor set like any other, so the teardown owes it the same follow-through the assert path gives a computed edge.