RFD 0005 — Relation subsumption

• State: committed
• Opened: 2026-05-28
• Decides: surface syntax for declaring that one relation subsumes another; the elaborator checks (endpoint covariance, cardinality refinement, metarel compatibility); the substrate impact; whether Argon adopts UML’s three-mechanism (subsetting / redefinition / specialization) story or collapses it into a single mechanism.

Question

Today, <: is a substrate-level subsumption operator admitted only on concept declarations (pub kind Adult <: Person). The substrate’s SubsumptionAxiomBody is generic over sub_id/super_id and would accept relation IDs without modification, but the surface grammar (§5.3 rel-decl) has no <: clause and the elaborator has no relation-side covariance machinery. Should Argon extend <: to relations? If so, what does the surface look like, what does the elaborator check, and how does this interact with UML’s three property-specialization mechanisms?

Context

Concrete modeler demand

The driving case (Luiz Almeida, 2026-05-28 design thread): a temporal-substrate model needs a sub-relation whose endpoints narrow and whose tuples flow into the parent.

pub type TimePoint <: TimeInterval;
pub type AbsoluteTimePoint <: TimePoint;

pub type TimeScale {
    timePoints: [TimePoint] from timeScaleHasTimePoint.range,
}

pub type IndefiniteTimeScale <: TimeScale {
    timePoints: [AbsoluteTimePoint]
        from indefiniteTimeScaleHasAbsoluteTimePoint.range,
}

pub rel timeScaleHasTimePoint(domain: TimeScale, range: TimePoint) [1] [1..*];
pub rel indefiniteTimeScaleHasAbsoluteTimePoint(
    domain: IndefiniteTimeScale,
    range:  AbsoluteTimePoint,
) [1] [1..*];

The intent: every tuple of indefiniteTimeScaleHasAbsoluteTimePoint is also a tuple of timeScaleHasTimePoint. Today there’s no way to express this; the modeler has to write a derive rule by hand, losing the structural property and the elaborator’s covariance check.

Substrate readiness

oxc-protocol::storage::SubsumptionAxiomBody:

#![allow(unused)]
fn main() {
pub struct SubsumptionAxiomBody {
    pub sub_id:   uuid::Uuid,    // generic — accepts concept or relation IDs
    pub super_id: uuid::Uuid,
}
}

The reasoner’s subsumption-closure logic (oxc-reasoning) parameterizes over symbol kind by construction. The substrate is ready; the surface and elaborator aren’t.

Parser asymmetry (the load-bearing gap)

oxc-parser/src/grammar.rs::concept_or_rel_decl already calls supertype_clause on the concept branch (lines 608–609), parsing <: via the existing LT_COLON / SPECIALIZES_KW machinery. The rel branch (lines 599–605) does not. The grammar’s SupertypeClause node is shared. Extending <: to relations reuses existing parser infrastructure; it does not introduce new syntax.

Argon’s existing position on shadowing and override

Three spec rules constrain the design space:

1. §3.4 name resolution does not walk <: chains. Resolution order is local → imports → auto-prelude → primordials. Verified in oxc-resolver/src/resolve.rs:207–255 — resolve_path walks module prefixes only.

2. §5.4 impl Type namespaces members as Type::name. Relations declared inside impl Person are reachable only as Person::ParentOf, not at module level. Verified in oxc-resolver/src/symbols.rs:57 — Item::ImplBlock(_) => return None. Impl-block contents don’t register top-level symbols.

3. §5.2 explicitly forbids implicit override. OE0206 InstantiationFieldShadows rejects iof-axis shadowing; OE0208 AmbiguousFieldFromMultipleParents rejects diamond ambiguity. Verbatim: “The substrate offers no automatic merge, override-by-position, or last-wins behavior — every collision is resolved explicitly.”

These three together eliminate the namespace problem UML’s {redefines} exists to solve: in Argon, Manager::subordinate and Employee::subordinate are already distinct qualified paths from the start.

UML’s three mechanisms and how they map

UML needs three mechanisms because UML conflates extent-level subsumption with namespace-level shadowing AND assumes properties propagate through the class hierarchy by name. Argon decouples all three concerns. One surface mechanism (<: on rel-decl) covers all three UML cases.

Decision

Surface

Extend rel-decl to admit a <: (or specializes) clause after the cardinality list:

rel-decl ::= attribute* 'pub'? <metarel-name> Ident generic-params?
              rel-param-list cardinality-list?
              supertype-clause?           // NEW
              rel-body? ';'?
supertype-clause ::= '<:' TypeExpr (',' TypeExpr)*
                  |  'specializes' TypeExpr (',' TypeExpr)*

The clause applies uniformly across every metarel-introducing keyword (rel, material, mediation, formal, …) — the production is shared with concept-decl’s supertype clause, identical to how SupertypeClause is currently defined in the ungrammar.

pub rel indefiniteTimeScaleHasAbsoluteTimePoint(
    domain: IndefiniteTimeScale,
    range:  AbsoluteTimePoint,
) [1] [1..*]
    <: timeScaleHasTimePoint;

Semantics

R1 <: R declares: every tuple of R1 is also a tuple of R. The reasoner’s subsumption-closure auto-derives

R(a₁, …, aₙ) :- R1(a₁, …, aₙ).

without an explicit derive rule. Queries against R see R1’s tuples; queries against R1 see only R1’s tuples.

Elaborator checks at the <: clause

1. Arity equality. R1 and R must have the same parameter count. Mismatch → OE0150 RelationSubsumptionArityMismatch.

2. Endpoint covariance. For each position i, R1.param[i].type <: R.param[i].type. Mismatch → OE0151 RelationSubsumptionEndpointVariance.

3. Cardinality refinement. For each slot i, R1.cardinality[i] must be no looser than R.cardinality[i]. Formal rule: [c..d] refines [a..b] iff c ≥ a and (d ≤ b or b = *). Mismatch → OE0152 RelationSubsumptionCardinalityViolation.

4. Metarel compatibility (MVP rule). meta(R1) == meta(R). Same metarel on both sides. Mismatch → OE0153 RelationSubsumptionMetarelMismatch. Cross-metarel subsumption (e.g., material <: formal if a vocabulary declares a metarel lattice) is deferred — see Open Questions.

5. Acyclicity. The relation subsumption graph must be acyclic. R1 <: R1 (direct or transitive) → OE0154 RelationSubsumptionCycle. Enforced by the same acyclic-DAG check used for concept subsumption.

Substrate impact

Zero new axiom kinds. The subsumption_axiom event with sub_id = R1’s NameRef and super_id = R’s NameRef carries the fact. The reasoner’s existing concept-subsumption closure generalizes by parameterizing over the symbol kind — relations are looked up via the same RelationCatalog machinery already used for storage.

Reasoner impact

oxc-reasoning::SemiNaiveExecutor extends its subsumption-closure pass to relation IDs. The existing concept-closure is parameterized on a SymbolKind enum; the implementation lifts the same Floyd-Warshall-style transitive closure over the subsumption DAG. Cost: O(|relations| · |subsumption_edges|) at module load.

Field-view propagation

A field declared via field: [T] from Rel.endpoint projects from Rel. When R1 <: R, a subtype concept may declare a field projecting from R1:

pub type TimeScale {
    timePoints: [TimePoint] from timeScaleHasTimePoint.range,
}
pub type IndefiniteTimeScale <: TimeScale {
    timePoints: [AbsoluteTimePoint]
        from indefiniteTimeScaleHasAbsoluteTimePoint.range,
}

The two fields are distinct projections per-concept; they share a name but live in different qualified namespaces (TimeScale::timePoints vs IndefiniteTimeScale::timePoints). Access from a TimeScale-typed binding projects the broader field; access from an IndefiniteTimeScale-typed binding projects the narrower one. Subsumption-closure ensures the narrower field’s tuples appear in the broader field’s view via the underlying relation <:.

Rationale

Why one mechanism, not three

UML’s {subsets} + {redefines} + implicit specialization is the right modeling vocabulary for a language whose properties propagate by name through the class hierarchy. Argon does not have that propagation:

• Name resolution doesn’t walk <:.
• impl Type namespacing creates distinct qualified paths from the start.
• §5.2 forbids implicit override.

Given these three, UML’s {redefines} solves a problem Argon doesn’t have. A subclass that wants to “redefine” a parent’s property declares its own relation in its own qualified namespace; the relation-level <: carries the extent containment; the modeler accesses through whichever qualified path is appropriate. No additional mechanism is required.

Why extend <: (not introduce a new operator)

The substrate’s subsumption relation is uniform across symbol kinds (concepts, relations, standpoints) — SubsumptionAxiomBody is already generic. Using <: consistently preserves that uniformity at the surface. Introducing a new operator (e.g., subsets, >:, #[subsets(...)]) would imply the substrate distinguishes mechanisms it does not in fact distinguish.

Why same-metarel for MVP

A vocabulary may eventually declare metarel-level subsumption (material <: formal); when that lands, the elaborator’s metarel-compatibility check follows the metarel lattice. For MVP, conservative same-metarel-required keeps the elaborator simple and matches the most common use cases. The conservative rule generalizes monotonically — relaxing it later does not break any existing models.

Alternatives considered

A. Three-mechanism mirror of UML

Add <: for subsetting AND a separate #[redefines(Parent::rel)] attribute (or redefines keyword) for namespace shadowing. Rejected. Argon’s name resolution + impl Type scoping eliminate the shadowing problem; a redefines mechanism would address a non-problem. Adds language surface for no semantic gain.

B. Implicit subsumption from endpoint typing

When a pub rel R1 has endpoints <: R’s endpoints, automatically infer R1 <: R. Rejected. Conflicts with Argon’s “no implicit override” policy (§5.2). Modeler intent must be explicit; covariant endpoint types alone do not signal a desire for tuple flow into the parent.

C. Derive-rule expansion

Tell modelers to write pub derive R(a, b) :- R1(a, b); by hand. Rejected. Loses the structural property (no covariance check), bloats the module with boilerplate, and gives the optimizer no opportunity to specialize storage layout for subsumption-closed relations.

D. Defer entirely to a follow-on

Don’t extend <: to relations now; revisit when more pressure builds. Rejected. The substrate already supports it. The grammar gap is forcing modelers (Luiz, OntoUML imports) to work around. The cost of landing is small (~1–2 days of focused work). Deferring accumulates technical debt and modeler confusion.

Consequences

What lands

What modelers gain

• Direct expression of UML {subsets} and OntoUML’s relation specialization patterns.
• Property narrowing in subtypes via paired relation+field declarations.
• Cleaner OntoUML import path (relation subsumption is a first-class OntoUML construct).
• Elaborator-verified endpoint covariance and cardinality refinement at declaration sites.

What modelers do NOT gain

• A separate redefines mechanism — Argon doesn’t need one (see Decision).
• Implicit override semantics — same name without <: remains unsupported; explicit qualification is the modeler’s tool.
• Cross-metarel subsumption (MVP) — initially restricted to same-metarel; lifted when metarel-lattice support lands.

Compatibility

Pure addition. No existing code changes behavior; the new clause is optional and absent in all today’s source. The subsumption_axiom wire format is unchanged.

Open questions

OQ1 — Field-level same-name across <:

When B <: A, both declaring a same-named field whose projection comes from <:-related relations (Luiz’s case), §5.2 has no explicit rule. Three readings:

• Permissive: allow whenever the underlying relations are in a subsumption relationship; the field views inherit the connection transitively.
• Strict: flag as shadowing per §5.2’s no-implicit-override policy; require explicit Parent::field qualification.
• Inherit the relation’s signal: treat the relation-level <: as the modeler’s explicit acknowledgment; no field-level signal required.

Recommend the third reading as the cleanest extension of §5.2 — the relation’s <: carries the intent through to the derived field views, no new field-level mechanism needed. Confirm before implementation.

OQ2 — Metarel lattice

Should metarels themselves admit <: (e.g., metarel material <: metarel formal in a vocabulary)? UFO’s relation taxonomy is layered; a vocabulary might want to express that material relations are a kind of formal relation. Deferring to a follow-on RFD; the conservative same-metarel rule in this RFD is forward-compatible.

OQ3 — N-ary relation subsumption

The covariance check (R1.param[i].type <: R.param[i].type for each i) generalizes to n-ary relations trivially. Verify the elaborator’s covariance pass handles ternary and higher relations without special-casing. Unlikely to be a problem — the per-position check is uniform — but the test suite should cover ternary cases explicitly.

OQ4 — Interaction with from Rel.endpoint field-view cardinality

When R1 <: R and a subtype declares a field f: [T] from R1.endpoint, what cardinality bound applies to f? The narrower relation’s slot bounds, or the broader’s? The narrower’s, almost certainly — the field is projecting from R1, not R — but verify the existing field-view elaboration respects this.

References

• §3.4 (name resolution), §5.2 (concept supertype clauses, OE0206/OE0208), §5.3 (relations), §5.4 (impl Type) — spec/reference/src/
• oxc-protocol/src/storage.rs:574–578 — SubsumptionAxiomBody
• oxc-resolver/src/{resolve.rs, symbols.rs} — name-resolution implementation
• oxc-parser/src/grammar.rs:599–672 — concept/rel decl parser and supertype_clause
• oxc-syntax/argon.ungrammar — typed AST shapes
• UML 2.5.1 §9.5 (Properties; subsetting and redefinition)
• Carvalho, V.A., Almeida, J.P.A., Guizzardi, G. (2017). Multi-level ontology-based conceptual modeling. Data & Knowledge Engineering 109, 3–24 — for the OntoUML relation-specialization patterns this RFD enables on import.