Reified-NAT contexts and structural genlCx

• Covers: how a ground application in a sentex's context slot reifies to a context — a cx/ constant a sentex can be stored in and a genlCx node — when a read names that context through the application, how a declared argument ordering makes one such context a computed spec of another with nobody asserting the edge, and when the orphan sweep collects one.
• Not here: object-denoting NATs, which reify to a nat/ constant that is a term and never a context → nat.md; the genlCx closure the produced edges feed → contexts.md; the lexical conventions the roles rest on → naming.md.
• Assumes: sentex, context, genlCx, reification, the termOfUnit map → glossary.md, nat.md, contexts.md.

A context is normally a Cx-prefixed name — CxTime, CxUniverse. A reified-NAT context is denoted instead by a function application: (CxTimeFn CxMonad (DatetimeFn "2000")) is "the year 2000, along the CxMonad dimension". The value of it is that the context hierarchy can then be computed: (CxTimeFn CxMonad (DatetimeFn "2000-01")) is a spec (sub-)context of the year — January 2000 is inside 2000 — so a fact asserted in the year is visible from the month, and nobody asserts that genlCx edge. This is the shape Cyc gives a context keyed by a term (its MtTimeWithGranularityDimFn and kin).

An object NAT is the other case: a nat/ constant is a term, refused as a context by the naming and genlCx well-formedness checks (nat.md). A context NAT carries a distinct namespace so that refusal stays exact.

The representation: reify the outer function, keep the argument structural

Position picks the namespace. A ground application in a sentex's context slot reifies — like any NAT, before the index sees it — to an opaque cx/-namespaced constant, whatever is declared about its head:

(assert kb '(holiday NewYear) '(CxTimeFn CxMonad (DatetimeFn "2000")))
;; stored: the sentex's context slot is a bare symbol  cx/a…
;; map:    (termOfUnit cx/a… (CxTimeFn CxMonad (DatetimeFn "2000")))

The write reads no declaration (nat/context-application?), so the stored set is a function of the offered set: a fact stored before, after or without any declaration about CxTimeFn lands in the same cx/ context. A non-ground slot (CxTimeFn CxMonad ?x) is refused for :shape, since the sentence alone shows it names no context, and so is a query context.

A read names the context through the application only while CxUniverse believes (result CxTimeFn context) (nat/context-function-believed?): the declaration that CxTimeFn's applications are contexts. context is the CxCore type, and result is the ordinary result declaration (argtypes.md), so one declaration says what the function denotes in both positions. Otherwise the read refuses the slot for :shape, and the message names the missing (result CxTimeFn context). A fact stored while CxUniverse does not believe the declaration is inert: the fact sits in its cx/ context, a read naming that constant answers it, and a read naming the application refuses until CxUniverse believes the declaration.

The check reads the declaration in CxUniverse, the context every reader reads the slot's termOfUnit map in (nat.md). A declaration stated in CxUniverse or in a context CxUniverse sees, such as CxCore, admits the slot. A declaration stated in an unwired context or in a spec of CxUniverse admits no read, and an except or a denial at CxUniverse hides the declaration (res/supporter-visible?). An except in a sub-context leaves the declaration believed at CxUniverse, and the slot reads. The check does not read the context the slot names: a cx/ context no genlCx edge names sees nothing but itself (contexts.md), so a check read there would refuse every read of an unwired context NAT.

Only the outer function reifies. Its arguments are left alone by the mint, so an unreifiable_function argument — (DatetimeFn "2000") — stays structural inside the stored expression, exactly as (QuantityFn 5 Meter) does in an object NAT (nat.md, reifiable vs unreifiable). That is what lets the producer below read the time term's shape to decide containment: reifying it away would collapse "2000" into an opaque atom and lose the very structure the ordering needs.

Reifying the outer function is what keeps "a context slot is a bare symbol" true everywhere — the trie index, sentexes-in-context, matches-visible, the genlCx graph nodes all key on a symbol, and none of them changes. The alternative, a compound in the context slot, would touch every one of those; the reified constant is one token by the time they see it.

The cx/ namespace carries the context role

Role-reading is spelling-only and never consults belief (naming.md), so a reified context cannot be marked a context by a (context K) fact a context? would have to look up, and the mint writes none: a (result F context) is not materialized on a cx/ constant. It is marked by its namespace: naming/context? is true for a cx/ symbol as it is for a Cx… name, and false for a nat/ object constant. term-role follows, and so — because they call context? — do the two checks that refuse an object NAT:

• wff/genlCx-problems admits a cx/ constant as a genlCx argument;
• naming/problems* admits it as a sentex's context slot.

nat/reified-nat-symbol? recognizes both namespaces (everything that asks "is this an opaque reified constant" — display, the K → E lookup — wants both); reified-context-symbol? and reified-object-symbol? are the discriminants where the kind matters (the orphan sweep below).

One constant per expression per namespace

The termOfUnit map is 1:1 within a namespace. One expression written in a context slot and in argument position maps twice: to a cx/ constant K′ from the slot, and to a nat/ constant K from the argument when its head is a reifiable_function (nat.md). Every read from expression to constant takes the namespace it wants (nat/in-namespace?, which splits the map by naming/context?): dedup-constant, rewrite-target, the collision grouping behind merge-colliding-nats!, and the applications a late result or correspondence declaration reaches. So the two constants are no collision, and neither read resolves to the other's constant. A function that is no reifiable_function leaves its argument-position application structural, as an unreifiable_function does. A rewriteOf target resolves a context slot only when it is a context by spelling, and a correspondence value never does: the value of a corresponding predicate names an object.

An argument-position application of a function declared (result F context) is a context by content. Its nat/ constant K is minted with the result types every object constant gets, so (context K) is stored and believed, and nothing refuses or contradicts it: no stored disjointness separates context from what a nat/ constant is, and a clash read off the spelling is not placed. The constant is a term in a sentence, so the naming check refuses it in a context slot and wff/genlCx-problems refuses it as a genlCx argument. Nothing equates K with K′.

Write and read are symmetric

The context slot is not on the sentence-reify walk — it is a separate argument to assert — so maybe-reify-context reifies it explicitly: on the write path (assert, minting) and on every read entry point (ist-goal, dedup-only, never minting, behind the declaration check above). A query scoped to (CxTimeFn …) therefore resolves to the same cx/ constant the write minted and meets the facts stored there; a never-seen NAT context resolves to the no-match sentinel and the read is scoped to nothing, answering empty rather than minting a context to ask about. assert-inert, which never mints, resolves the slot the same way and refuses one with no stored constant (:unminted-nat). check reads the slot as the cx/ constant assert stores in, the stored one or the one the expression's content names, and mints none (nat/context-for-check), so check reports what assert refuses for a compound slot as for a symbol.

The structural genlCx producer

(contextArgSubrelation F pos R) declares the ordering: two F-contexts identical except at argument pos are ordered by the sub-relation R on that argument — the one whose argument is R-below the other's is the spec, and genlCx the more general.

(assert kb '(result CxTimeFn context) 'CxUniverse)
(assert kb '(unreifiable_function DatetimeFn) 'CxUniverse)
(assert kb '(contextArgSubrelation CxTimeFn 2 subintervalOf) 'CxUniverse)  ; arg 2 = the datetime

vaelii.impl.context-nat reads the declarations and the context NATs of F from the store, groups the contexts into siblings (same expression but for argument pos), and for each sibling pair whose pos arguments stand in R materializes the genlCx edge. The edge is a justified derived sentex, made the way special/deduce-lift makes a decontextualized copy — find-or-create-sentex, special/derived-sentex-added (which reaches the genlCx closure and posts the re-check triggers), then a JTMS justification under the contextArgSubrelation informant. It is never a premise anyone asserted.

Justified is the whole point: the edge belief-follows for free. Retract a context (its termOfUnit map), the declaration, or — for the stored-fact oracle below — the R-fact, and the ordinary JTMS relabel withdraws the edge and sees? flips. Nothing hunts it down, and the taxonomy's depth/SCC potential and witness support are the derivation path's, not a second mechanism (contexts.md, the consumers).

A computed edge widens what a merge can see, exactly as a stated one does. A genlCx edge is not only a visibility fact: it decides which sentexes an equality restates and which pairs a functional / functionalInArg / anti_symmetric mark can reconcile (equality.md, the third and fourth arrival orders). Those three reconcilers were written out at the assert entry point and at the rule-conclusion entry point and at no third one, so a calendar edge posted the re-check triggers and ran no merge at all — whether two fillers of one functional slot merged came down to whether the year's fact was written before January existed (vaelii#56). The producer settles once it has built an edge, and the settle's drain runs the sweeps for it as for an asserted or a concluded edge (contexts.md). The producer is idempotent, and a declaration or a revival re-runs it over every pair of a function's contexts; a second route to an edge already believed moves no label and is no move.

Every arrival order converges. Three things can arrive last, and each has an arm. A declaration arriving after the contexts sweeps every pair of them (reconcile-function); a context arriving after a declaration is swept when it is minted, over the pairs it is in; and an (R a b) evidence fact arriving after both sweeps the pairs ordered a below b in the functions declared to order by R (functions-ordered-by), which is the arm a comparator dimension never needs and a stored-fact one cannot do without. A fact stored into a context that already exists creates no pair and sweeps nothing, so its cost does not grow with the context's siblings (lein perf's context-nat-existing-context); a mint costs one oracle call per sibling. The maintenance hook sits beside the correspondence reconcile at the tail of assert and behind the same gate, nat/any-reified-constants?: the in-memory reifiable_function marks, then one O(1) termOfUnit functor count, since a context slot mints with no declaration. A KB that has minted nothing pays that count and neither the hook nor the any-context-subrelations? index read.

The bounded R oracle — no proof inside the relabel loop

The producer feeds the genlCx closure, which a relabel loop reads, so it may not start a prover search to decide R (naf.md). R is resolved only by a bounded oracle:

• a registered pure structural comparator, keyed on the sub-relation — the datetime one answers subintervalOf between two DatetimeFn terms by reading their shape; or
• a believed stored (R a b) fact, when no comparator applies.

A comparator answer is a pure function of the two expressions, already carried by the termOfUnit antecedents, so it contributes no extra supporter; a stored fact contributes its own handle, so defeating it withdraws the edge.

The calendar dimension

vaelii.impl.datetime is the first shipped dimension, and it reads two spellings of one interval.

DatetimeFn is an unreifiable_function taking a reduced-precision ISO 8601 string: "2000" the year, "2000-01" its January, "2000-01-15" a day, down through hour, minute, second. YearFn / MonthFn / DayFn are the calendar constructors over the same three coarsest fields, written as numbers rather than as a string — (YearFn 2000), (MonthFn 2000 1), (DayFn 2000 1 15). Each takes one field per argument, coarsest first, so its arity is its precision and there is no string to parse or to mis-parse; each is unreifiable for the reason DatetimeFn is, since the fields are exactly what the ordering reads and a minted constant would hide them.

Containment is field nesting — a more-precise interval is inside a less-precise one it shares every field with, whichever spelling each was written in:

(MonthFn 2000 1)  ⊆ (YearFn 2000)     ; January is inside the year
(DayFn 2000 1 15) ⊆ (MonthFn 2000 1)  ; the day is inside January
(MonthFn 2000 2)  ⊄ (MonthFn 2000 1)  ; siblings nest neither way
"2000-01"         ⊆ (YearFn 2000)     ; the two spellings order against each other
"2001"            ⊄ "2000"            ; different year
"2000"            ⊄ "2000-01"         ; the year is the COARSER interval, so it contains the month

subinterval? reads each term to a vector of integer fields and tests prefix equality — pure, total (it declines any term that is neither), and bounded, so the producer may call it inside the settle loop. One field vector for both spellings is the whole of the bridge between them: the comparator never learns which constructor it was handed, so (MonthFn 2000 1) and (DatetimeFn "2000-01") name the same interval, and a KB told the year one way and the month the other still orders the two contexts. Fields are numeric, so "2000-1", "2000-01" and (MonthFn 2000 1) are one month.

Three constructors and not six: a year, a month and a day are the granularities somebody writes a holiday or a policy for, and each finer field is a spelling ISO already gives. The three are declared in resources/kb/upper/CxTime.txt — they are about time, and CxTime is the upper context that owns time — each with a (result … temporal), so a calendar term is an interval and not an instant. That is also why it cannot stand in an instantBefore, and why the moments it lies between are a separate term with a separate constructor: see What this does not cover.

Orphan collection: a context is a place as well as a name

A context NAT is collected at the gate an object NAT is (nat.md, "Rename and remove") — remove-orphaned-nats! on the retract! / edit! sweep, over the region the teardown removed. The liveness question is what differs, because a cx/ constant is somewhere sentexes are as well as something sentences name. It is orphaned when all three of these are empty:

• its extent — nothing is stored in its context slot;
• its mentions — no stored sentence names it as a term;
• its edges — no stored genlCx edge mentions it.

Stored, not believed, for the reason an object NAT's uses are counted that way: a defeated fact still sits in the slot and a relabel can restore it.

A computed edge is not one of the three. The structural edges above are derived from the two contexts' own termOfUnit maps, so reading one as a reference makes an ordered pair immortal — each end held up by an edge read off the other. The discriminant is authorship, as it is for an object NAT's materialized result types: the producer deduces under the contextArgSubrelation informant and nothing else does, so an edge that is no premise and whose every support carries that informant is the engine's own wiring. An edge somebody asserted is a premise and holds its contexts up; one a rule concluded carries that rule's informant and holds them up too.

The map is a context's whole bookkeeping — the mint writes no result types for one — so the collection retracts the termOfUnit and stops there. The computed edges are derived, so withdrawing that one premise takes them through the ordinary dependency-directed sweep, and their removal is what puts the far end of each edge in the next round's candidate set. A chain of ordered contexts collapses by the rule that collapsed the first, and an object NAT standing inside a collected context's expression is the round after that.

An empty context goes even while a spec of it is live, and that is the reading and not an edge case: a year holding nothing, named by nothing and wired only by what the producer computed answers no reader, and stating a fact for it again re-mints it and recomputes the edge down to its January.

What triggers it, and what it costs

The sweep is the teardown's, so a removal is what makes a candidate. A context is referenced two ways, and nat/orphans-named-by reads both off each removed sentex: in its sentence, at any nesting, and as its own context slot — which is how the last fact leaving an empty context is the removal that orphans it. Whichever of the three sources goes last is the retraction that collects, and the end state is the same in every order.

Each candidate costs one count-in-context, an O(1) secondary-root read on every backend (indexing.md), and — only when that is zero — one inverted-term-index read over the constant's own footprint. So a live context holding a million facts costs a count rather than a million record fetches. The sweep sits behind nat/any-reified-constants?, so a KB that has minted no constant pays one termOfUnit functor count per teardown and nothing else.

Nothing here can reach a context that is not a cx/ constant. The three query contexts (contexts.md) are Cx… names for a way of reading, refused at every write entry point and never minted, so no termOfUnit maps one and the candidate set cannot hold one — a query holding one holds a symbol the sweep cannot name. An agent or channel context (koinii.md) is a Cx… name computed from an id, in the same position. In a fork the sweep runs through the ordinary retract!, which tombstones an inherited record rather than deleting it, so a context the fork empties is collected in the fork's view and stands in the base (overlay.md, base immutability).

Re-minting after a sweep

Re-minting a swept expression dedups to one constant, exactly as it does when nothing was collected: the mint's dedup probe reads the termOfUnit map, the map is gone, so a fresh constant is minted and every later occurrence of the expression finds that one. The KB that results is indistinguishable from one the sweep never touched — one constant per expression, the same computed edges, the same answers through the compound context at every read entry point.

The cx/ symbol and the handle are not part of that, and nothing may read them as though they were. A reified constant is opaque and minted per KB, handles are allocated in assertion order, and belief may never tie-break on one — so a caller holding the old symbol across a sweep holds a name for nothing, and gets its answer back by naming the expression, which is the only spelling the map is keyed by.

What this does not cover

• One dimension ships. The calendar — DatetimeFn / YearFn / MonthFn / DayFn under subintervalOf — is the worked example; other dimensions are added by declaring a (result F context), a contextArgSubrelation, and either registering a comparator or asserting the R facts.
• A calendar term's endpoints are somebody else's job. (YearFn 2000) is a temporal, so it takes the interval relations and not instantBefore, which is a claim about moments. The moments it lies between are computed — half-open, so 2000 ends where 2001 begins — by the calendar clock, which answers startOf / endOf with an (InstantFn Y M D h m s) term and stores nothing (time.md, "The calendar clock"). Nothing here reads them: the two mechanisms share the field reader in vaelii.impl.datetime and nothing else, and they agree exactly — b's fields being a prefix of a's is the same claim as a's bounds lying inside b's, so the genlCx edge this page produces and the subintervalOf the clock answers hold of the same pairs.

Where it lives

• vaelii.impl.nat — context-namespace, the cx/ mint path (mint-nat! takes the namespace and skips result-types for a context), maybe-reify-context, context-application? (what the context-slot shape check admits — a ground application, so the check does not depend on the naming policy or on a declaration), context-function-believed? and readable-context-application? (what a read admits), context-for-check (the context check reads a slot as, minting nothing), in-namespace? (the per-namespace split of the map), the reified-context-symbol? / reified-object-symbol? discriminants, and the orphan question's context arm — orphan?'s extent gate, computed-genlCx-edge? (the authorship test), and orphans-named-by's reading of a removed sentex's context slot.
• vaelii.impl.naming — context? (the cx/ namespace).
• vaelii.core — the context-arg reify in assert and the read entry points (ist-goal), and the context-slot shape checks (context-shape-problem on a write, read-context-shape-problem on a read).
• vaelii.impl.nat-maintenance — the producer's call site on the assert path (reconcile-assert), its revival re-run on retract! / edit! (reconcile-revivals!), the merges a computed or revived edge licenses, and collect-orphans!, which collects both kinds of constant at one gate.
• vaelii.impl.wff — the contextArgSubrelation well-formedness check.
• vaelii.impl.context-nat — the producer, the comparator registry, and functions-ordered-by, the evidence-arrived-last arm of the stored-fact oracle.
• vaelii.impl.datetime — the calendar containment comparator, over the ISO strings and the three calendar constructors alike, and beside it the half-open bounds the calendar clock reads a term's two moments out of (time.md).
• resources/kb/CxCore.txt — contextArgSubrelation, and result's comment on (result F context), documented in the KB's own representation.
• resources/kb/upper/CxTime.txt — YearFn / MonthFn / DayFn, each with its result.