RFD 0017 — Refinement classification: where (primitive) vs iff (defined)

• State: committed
• Opened: 2026-06-05
• Decides: whether a concept’s refinement predicate (<: Parent where { P }, Refinement) is a necessary condition only (membership asserted; the predicate is an invariant) or a necessary-and-sufficient condition (membership derived; the substrate auto-classifies). Today every refinement is implicitly the latter. This RFD splits the surface so the modeler chooses explicitly: where { P } is primitive (description-logic ⊑; necessary-only; membership asserted), iff { P } is defined (DL ≡; necessary-and-sufficient; membership derived). Confirms dyn remains reserved exclusively for runtime trait objects (Built-in type forms, Out of scope (v0)). Relates to RFD 0006 (refinement-determined classification was cited there as canonical), RFD 0007 (three-valued refinement membership under OWA), RP-007 (spec/research/RP-007-narrowing-under-mutation.md; value-dependent narrowing soundness).

Question

concept Adult <: Person where { self.age >= 18 } — is an arbitrary Person with age >= 18 automatically an Adult, or must Adult-membership be asserted, with the predicate merely constraining who may be one?

Today the answer is “automatically.” The runtime computes extent(Adult) = { x : iof(x, Person) ∧ predicate(x) } (compiler/crates/oxc-runtime/src/lib.rs:1986-2008, the “refinement-honesty pass”); the book states it outright — “the refinement is the substrate’s source of truth for membership… the substrate derives the iof classification automatically” (mutate, constraint 2 on insert iof) — and rejects explicit insert iof(x, Adult) with OE0211. That is the DL defined-class (≡) reading, and it is the only reading the surface can express. There is no way to say “validate this predicate on every Adult, but membership is conferred, not inferred” — the DL primitive-class (⊑) reading, which is the common case in real ontologies.

Auto-classification by default, with no opt-out, is the wrong default for three reasons (Rationale). The question: what surface distinguishes the two, and what does each mean across the extent query, insert iof, construction, and mutation?

Context

The DL distinction. A primitive class C ⊑ D ⊓ P states necessary conditions: every C is a D satisfying P, but a D satisfying P is not thereby a C — membership is asserted (SubClassOf in OWL). A defined class C ≡ D ⊓ P states necessary and sufficient conditions: a D satisfies P iff it is a C — membership is inferred by the reasoner (EquivalentClasses; classification/realization). In real ontology engineering the overwhelming majority of named classes are primitive; defined classes are the deliberate minority written specifically to drive inference. Defaulting every where to defined inverts that.

What the substrate mechanizes vs. specifies. The Lean models the refinement predicate as a decidable fragment (spec/lean/Argon/Decidability/Fragment.lean) but leaves the instance-level value predicate D2Pred opaque (Fragment.lean:80-103: “we do not formalize the internal structure of QF-LIA formulas”). mutate emits only explicit assertIof/retractIof effects (spec/lean/Argon/Runtime/MutationSemantics.lean:104-115). The defined-class realization (iof(x,C) ↔ iof(x,parent) ∧ P(x)) exists as book prose + Rust runtime, not as a Lean theorem. So this is a clean point to fix the surface: the substrate has not committed to “all refinements are defined” — only the prose and one runtime pass have.

The corpus is entirely defined classes. Every where in a runnable example declares the refinement, never asserts iof to the refined type, and queries the derived extent: FullTime/Manager (examples/refinement_employment), ActiveAdult (examples/multi_field_refinement), Adult/Felon/SpecialClass feeding defeasible can_vote (examples/legal_norms_can_vote), FullTime over time (examples/temporal_promotion), Adult as-of (examples/temporal_as_of_surface). These are defined classes; migrating them where→iff is correctness, not churn. The sole where test that does not auto-classify hand-asserts alice iof Adult (compiler/crates/oxc-oxbin/tests/end_to_end_program.rs) — the natural primitive case.

No write-time enforcement exists today. The predicate is purely a query-time filter; construction, insert iof, and update perform no validation (oxc-runtime/src/lib.rs: Operation::Construct, Operation::InsertIof, Operation::Update). OE0210/OE0211 are declared in grammar.toml but never emitted. So a primitive where needs new enforcement machinery (its predicate must do something), and a defined iff needs OE0211 finally wired.

Decision

1. Two clause keywords; identical syntax, opposite membership semantics

where-clause ::= ('where' | 'iff') '{' refinement-pred (',' …)* '}'

The predicate grammar (refinement-pred ::= D1Pred | D2Pred, Refinement) is unchanged. The keyword alone selects the membership semantics:

• where { P } — primitive (DL ⊑). P is a necessary condition. Membership is asserted (by construction or insert iof). extent(C) is the set of entities asserted iof C (or iof a subtype) — identical to an unrefined subtype’s extent. P is enforced as an invariant at every membership-write point; it never widens the extent.
• iff { P } — defined (DL ≡). P is a necessary-and-sufficient condition. Membership is derived: extent(C) = { x : iof(x, parentᵢ) ∧ P(x) } over C’s <:-ancestors-including-self — the current runtime behavior, unchanged. Manual assertion is forbidden.

2. insert iof / construction / mutation, per kind

OE0211 (declared, previously unemitted) is narrowed to iff concepts — you cannot assert membership of a defined class because its membership is the predicate. For where, asserting membership is exactly how you become a member, so insert iof is permitted and the predicate gates it.

3. New diagnostic: OE0668 RefinementInvariantViolated

A membership-write that would place an entity in a primitive where-concept whose predicate it does not satisfy is rejected at runtime, surfaced as Result<_, Diagnostic> (the mutate-rejection channel mutate already promises). Three-valued, OWA-aligned (World assumptions (CWA / OWA), RFD 0007): reject only on positive evidence of violation (P evaluates to definite false); unknown — information absence, i.e. a referenced field with no recorded value — permits the write. A primitive invariant blocks the demonstrably-bad, not the merely-unproven — symmetric with iff’s rule that unknown does not grant membership.

Amendment (2026-06-11, audit ts-01 / PR #272). The original clause folded unevaluable (a v0.1-unsupported form or a type-mismatched operation) into unknown-permits. That fold was the ts-01 critical: predicates over Real/Decimal/Money/Date were “unevaluable” to the v0.1 evaluator and therefore silently never enforced. The ratified semantics split the bucket: unknown = missing field only (OWA information-absence; permits where, withholds iff membership). A predicate that cannot be evaluated — unsupported form, malformed wire data, type-mismatched comparison — is a loud error (RefinementUnevaluable at runtime; OE0660 refuses unsupported forms at build time), never a silent permit or a silently-empty extent. Three-valuedness is for the world’s incompleteness, not the evaluator’s.

4. dyn is reserved exclusively for trait objects

Confirmed (your call (c)). dyn is and stays the keyword for deferred runtime trait objects (&dyn Trait / Box<dyn Trait>, Built-in type forms, Out of scope (v0)) — dynamic dispatch + type erasure, orthogonal to whether membership is derived. The classification axis uses where/iff; the dispatch axis uses dyn. They may co-occur on a future concept and must not share a keyword.

5. Substrate scope

The Lean surface AST (ConceptDecl) and storage body (Storage.AxiomBody.ConceptDeclBody) carry the primitive/defined discriminator now — a shared @[language_interface] inductive RefinementKind, drift-gated against the Rust RefinementKind mirror — and the two membership semantics are documented in the substrate docstrings. The realization theorem for iff — iof(x,C) ↔ iof(x,parent) ∧ P(x), requiring the instance population + value-environment that State C A does not yet model — is not mechanized here; it is the value-dependent-membership case that RP-007 §1.2 hazard 2 / §4.5 scopes as open. It is left as a follow-up (RP-007-adjacent, #40), not claimed as done. This is honest staging, not a stub: the surface, elaboration, storage, and runtime are complete and proven-to-run (parser, elaborator, and five end-to-end runtime tests); the deep substrate theorem is research, exactly as RP-007 is.

Rationale

Why split at all (against auto-by-default). (1) Practice: most real classes are primitive; the common case should be the plain keyword. (2) No spooky inference: silent derivation of facts is un-Rust-like (the house aesthetic default); a modeler should opt into the reasoner minting memberships. (3) Soundness blast radius: value-dependent auto-classification is the source of RP-007’s hardest open hazard (a narrowing if x: VerifiedAdult invalidated by update x set { age = 10 }). Making it opt-in (iff) makes that hazard opt-in — the obligation narrows to exactly the concepts that asked for derivation.

Why iff. It is the membership biconditional: iof(x, Adult) ↔ iof(x, Person) ∧ age ≥ 18 reads directly as “Adult iff Person and age ≥ 18.” Necessary-and-sufficient is the literal meaning of “if and only if.” No other candidate (defined, :=, ≡) is as self-documenting at the use site, and it touches neither dyn nor = (taken by metaxis typed domains, Meta-calculus atom).

Why where for primitive. Rust’s where is a bound — a necessary constraint on a type, never a definition (fn f<T>() where T: Clone). Reusing it for “necessary condition on members” aligns with the Rust/Cargo aesthetic default and with DL ⊑. A where-refined concept reads as “a Person, further constrained to age ≥ 18” — a constraint, not a definition.

Why three independent principles agree (practice, no-spooky-inference, soundness-containment) plus two surface alignments (Rust where-bound, iff-as-biconditional) is why (a) — which keyword is primitive — has a correct answer rather than a coin-flip: where = primitive, iff = defined is over-determined.

Alternatives

• Keep auto-by-default; add a keyword for primitive. Rejected: inverts ontology practice, keeps the spooky default, and leaves the RP-007 hazard pervasive. Also incompatible with choosing iff (which must be the defined form — it claims sufficiency).
• Operator distinction <:+where vs =. (Adult = Person where {…}.) Mirrors DL ⊑/≡ exactly but a one-character carrier of enormous semantic weight is dangerous, and = already introduces metaxis typed domains.
• defined modifier on the concept. (pub defined kind Adult ….) Familiar to Protégé users but detached from the clause and heavier; loses the at-the-predicate self-documentation iff gives.
• Reuse dyn (dyn where). Rejected per call (c): collides with trait objects, and “dynamic dispatch” ≠ “derived membership.”
• Enforce primitive where purely via a separate check rule (status quo workaround: drop the predicate, add a constraint rule). Rejected as the only mechanism: it detaches the invariant from the concept’s identity and gives no surface to the necessary/sufficient choice. where-as-invariant and check-rules coexist; the former is a membership invariant local to the concept, the latter a global constraint.

Consequences

• Migration. All 8 example where sites → iff; the corpus tests, CLI pipeline tests, and runtime unit test that assert derived extents update accordingly. Primitive-where behavior (no auto-classify, asserted membership, OE0668 on insert-iof / construct / update, OE0211 on iff insert-iof, atomic rejection) is covered by five new end-to-end runtime tests. The oxbin round-trip fixture stays where-compatible.
• Wire format. ConceptDeclBody gains a classification discriminator; canonical-CBOR field order updated; decode_concept_decl back-compat: absent discriminator ⇒ iff is not assumed — pre-split artifacts are rebuilt (Argon is pre-1.0, in-process; no stored-artifact compatibility burden).
• OE0211 semantics change. Previously declared-but-unemitted “refined type”; now emitted, and only for iff. Any future code keying on “has refinement predicate ⇒ reject insert iof” must key on “is iff.”
• New runtime enforcement path (OE0668 RefinementInvariantViolated) for primitive where at construction / insert iof / dependent update.
• Rigidity (OE0210) remains out of scope here: it gates insert iof on anti-rigidity (a UFO meta-property carried as meta_property events, not in the ontology-neutral ConceptDeclBody). Still declared-but-unenforced after this RFD; a separate rigidity-enforcement effort owns it. Noted so the two insert iof gates (rigidity, classification) are not conflated.

Open questions

• iff realization soundness (follow-up, RP-007-adjacent #40): mechanize iof(x,C) ↔ iof(x,parent) ∧ P(x) in Lean, which requires extending the state model to carry the value environment — the RP-007 §4.5 sub-problem. Until then iff derivation is runtime-correct but not substrate-proven (parity with the pre-RFD status quo).
• update-time invariant scope. v0.1 re-checks a primitive where predicate only against the directly mutated entity/fields. Transitive invalidation (a mutation to entity y that changes an aggregate a where-predicate on x reads) is not chased; the predicate fragment (OE0660) forbids the aggregate/subquery forms that could create such coupling, so this is currently vacuous — revisit if the fragment widens.
• Should iff construction (insert C { … }) be sugar or an error? Decided: sugar (construct + set fields; classification derived). Revisit if it proves confusing that a constructed iff-C with predicate-violating fields silently is not in extent(C).