Relations

Like concepts, relations are introduced by a vocabulary-defined metarel — there is no built-in rel keyword at lexer level. Stdlib ships a generic metarel std::core::rel<E1, E2>(E1, E2) for ontology-uncommitted relations; vocabulary packages can ship richer metarels (mediation, material, etc.) or re-export the generic.

// Same terminator rule as a concept (Vocabulary concepts and the generic `type` metatype): the `{ }` rel-body self-
// terminates; the bodyless form requires a ';' (`OE0011` if absent).
rel-decl         ::= attribute* 'pub'? <metarel-name> Ident '(' rel-param-list ')'
                      cardinality-list? rel-supertype? ( rel-body | ';' )
rel-supertype    ::= ('<:' | 'specializes') TypeExpr (',' TypeExpr)*
rel-param        ::= 'mut'? Ident ':' TypeExpr        // RFD 0076 — `mut` only in the named form
cardinality-list ::= cardinality+                       // one slot per endpoint
cardinality      ::= '[' range ']'
range            ::= Nat '..' Nat | Nat '..' '*' | Nat '..=' Nat | Nat
                  // In cardinality position, `..` is INCLUSIVE on both ends
                  // (UML convention): `[1..1]` means exactly one, `[0..*]`
                  // means zero or more. Distinct from Rust range semantics.
rel-body         ::= '{' field-list '}'

The leading identifier (after pub) is contextually a metarel-introducing keyword, resolved per Name resolution against the pub metarel declarations visible in scope — declared in this package or imported from a vocabulary package; rel is not ambient — the std::core baseline is brought in by use std::core::{rel} or a [package].prelude entry (RFD 0038). An unresolved introducer is refused with OE0606 UnknownMetarel. The parser disambiguates concept-decl (no (...) after the new name) from relation-decl (has (...)).

Three surface forms (using the std::core baseline, brought into scope via use std::core::{type, rel};):

use std::core::{type, rel};
// Form A — anonymous binary field on a concept
pub type Person { children: [Person] }

// Form B — named relation with optional navigation views
pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*];
pub type Person {
    parents:  [Person] from ParentOf.parent,
    children: [Person] from ParentOf.child,
}

// Form C — n-ary relation with intrinsic property body
pub rel Marriage(spouse_a: Person, spouse_b: Person) [0..1] [0..1] {
    since:  Date,
    status: MarriageStatus,
}
pub rel Transaction(seller: Person, buyer: Person, item: Asset) {
    amount: Money,
    at:     DateTime,
}

Cardinality (positional, UML association-end convention). For a relation with endpoints e₁, e₂, …, eₙ, the i-th cardinality slot bounds the number of distinct eᵢ for each fixed combination of all the other endpoints — the UML association-end multiplicity. (Equivalently: hold every endpoint but the i-th fixed, and the slot bounds how many distinct eᵢ may complete the tuple.) Omitted slots default to 0..*. For binary relations the slots read left-to-right; pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*] reads “each child has 1..1 parents (slot 1 bounds the parents per fixed child); each parent has 0..* children (slot 2 bounds the children per fixed parent).” For n-ary relations the same per-position rule holds against the fixed combination of the others; pub rel Transaction(seller, buyer, item) [0..*] [0..*] [0..1] reads “for each (buyer, item) pair, 0..* sellers; for each (seller, item) pair, 0..* buyers; and for each (seller, buyer) pair, 0..1 items.”

Relation subsumption (<: / specializes). A relation declaration may name one or more superrelations after its endpoints, in either glyph — <: or the keyword synonym specializes (they are exact synonyms; a declaration reads identically under either). A superrelation clause makes the child’s extent flow into the parent’s: every tuple of the child is, by that edge, a tuple of the parent, so the parent’s closed extent (and every navigation view and rule over it) includes the child’s. The clause takes an optional parenthesized filler list stating, for each parent end by name, what fills it — parentEnd = value:

use std::core::{type, rel};
pub type Person;
pub type City;
pub rel Loc(p: Person, c: City);

// Bare form — pair the child's ends onto the parent by position.
pub rel Home(p: Person, c: City) <: Loc;

// Named filler list — each parent end paired, by name, with the child end
// at the same position. This means EXACTLY what the bare form means: both
// record the same identity mapping, and the bare form desugars to this one
// list at a single point, so there is one downstream representation, not two.
pub rel Residence(p: Person, c: City) <: Loc(p = p, c = c);

// `specializes` is the exact keyword synonym of `<:`.
pub rel Domicile(p: Person, c: City) specializes Loc(p = p, c = c);

Each filler is one of three shapes, all keyed by a parent end: parentEnd = childEnd (pair the parent end with a child end); parentEnd = <literal> (a constant pin, fixing that parent end to a value); or parentEnd = childEnd as ParentSort (a cast, widening a child end to a parent supersort). A mapping whose every parent end is paired with the child end at the same position is the identity mapping; anything else — a rename that permutes ends, a constant pin, or a widening — is a non-identity mapping. Both are evaluated: a child tuple contributes its mapped image to the parent’s extent, threading child ends into the parent’s positions by name, filling pinned positions with their constant, and admitting cast ends at the parent sort. The parent’s closed extent — and every navigation, rule, and query over it — sees the mapped image, so the child is a live member of its parent’s family.

A constant pin fixes a parent end the child has no end for. This is the worked example for the whole mechanism. WagesUSA records only a person and an amount; its images join IncomeItem with the currency pinned to USD. ForeignIncome is an identity member alongside it, so the parent family carries both a pinned image and a pass-through tuple:

use std::core::{type, rel};
pub type Person;
pub type Currency;
pub const USD: Currency;
pub const EUR: Currency;
pub rel IncomeItem(mut p: Person, mut amount: Int, mut c: Currency);
// Constant pin: the parent's `c` end is fixed to a literal rather than
// paired from a child end.
pub rel WagesUSA(mut p: Person, mut amount: Int) <: IncomeItem(p = p, amount = amount, c = USD);
// Identity member: every end paired to the child end at the same name.
pub rel ForeignIncome(mut p: Person, mut amount: Int, mut c: Currency) <: IncomeItem(p = p, amount = amount, c = c);

pub fact Person(alice);
pub fact Person(bob);
pub fact Currency(USD);
pub fact Currency(EUR);
pub fact WagesUSA(alice, 500);
pub fact ForeignIncome(bob, 300, EUR);

// The parent-union query over the whole family.
pub derive anyIncome(p, a, c) :- IncomeItem(p, a, c);
// A query that pins the currency: only USD-imaged rows answer it.
pub derive usdIncome(p, a) :- IncomeItem(p, a, USD);

WagesUSA(alice, 500) is an IncomeItem with its currency filled by the pin; ForeignIncome(bob, 300, EUR) passes through unchanged. anyIncome reads the parent family and sees both:

anyIncome(alice, 500, USD)
anyIncome(bob, 300, EUR)

The pinned query IncomeItem(p, a, USD) fixes the currency, so it matches the pinned image but prunes the EUR tuple — usdIncome yields only alice:

usdIncome(alice, 500)

pub const declares a named individual constant. pub const USD: Currency; declares the individual USD with concept sort Currency: when the ascribed type resolves to a declared concept, the ascription lowers to the same classification assertion pub fact Currency(USD); emits, so the constant resolves as a classified individual wherever an individual is written — a constant pin (c = USD), a rule-body value position (s == USD), a fact argument. Individual identity is the global bare-name hash, so writing the explicit pub fact Currency(USD); alongside the const (as the examples here do) re-asserts the same one row — a relation extent is a set, and re-assertion is harmless. A const whose ascribed type is not a declared concept (a primordial like Int, a struct/enum) declares the bare name only; no classification is asserted. The initializer form const X: T = …; does not execute yet and refuses (OE1355).

Retraction runs the mapping in reverse of assertion: delete WagesUSA(alice, 500) withdraws the child, and its USD image disappears from IncomeItem (a two-support image survives until its last contributing child is retracted).

That last clause is worth showing, because a family image is a derived conclusion held by set-union support, not a stored tuple. When two different members pin the same parent tuple, the image carries two independent supports and is one row that survives until the last support is retracted:

use std::core::{type, rel};
pub type Person;
pub type Currency;
pub const USD: Currency;
pub rel IncomeItem(mut p: Person, mut amount: Int, mut c: Currency);
// Two members that both pin the currency to USD — different relations, same image.
pub rel WagesUSA(mut p: Person, mut amount: Int)  <: IncomeItem(p = p, amount = amount, c = USD);
pub rel SalaryUSA(mut p: Person, mut amount: Int) <: IncomeItem(p = p, amount = amount, c = USD);

pub fact Person(alice);
pub fact Currency(USD);
pub fact WagesUSA(alice, 500);
pub fact SalaryUSA(alice, 500);

pub mutate dropWages()  { delete WagesUSA(alice, 500) }
pub mutate dropSalary() { delete SalaryUSA(alice, 500) }

pub derive anyIncome(p, a, c) :- IncomeItem(p, a, c);
pub derive totalIncome(p, t) :- p: Person, t = sum(a for p2 in Person, IncomeItem(p2, a, _), p2 == p);

WagesUSA(alice, 500) and SalaryUSA(alice, 500) both image onto IncomeItem(alice, 500, USD) — one row, two supports:

anyIncome(alice, 500, USD)

Run dropWages: one support is gone, but SalaryUSA still contributes, so the image survives unchanged —

anyIncome(alice, 500, USD)

Then run dropSalary: the last contributing child is retracted, and only now does the image withdraw —

(no rows)

Propositions, not events

A relation extent is a set of propositions, not a log of events. Two child facts whose translations produce the identical parent tuple are the same proposition asserted twice; the family holds it as one row carrying two supports. This is correct set semantics and the single most common source of aggregate surprise, so it is worth pinning precisely with three runs of the IncomeItem model above.

Identical fact twice — one row. WagesUSA(alice, 500) and SalaryUSA(alice, 500) both translate to IncomeItem(alice, 500, USD). An aggregate over the family folds that one row once. totalIncome sums the amount over IncomeItem per person:

totalIncome(alice, 500)

— 500, not 1000, even though two child facts were asserted. That is the right answer for the proposition “alice has USD income of 500”: the two children merge into one row carrying two supports, and (per the retraction above) the row survives until the last supporter is withdrawn.

Distinct amounts — two rows. Change one fact to SalaryUSA(alice, 501). The translations now differ (500 vs 501), so they are two propositions, two parent rows, and the aggregate sums both:

totalIncome(alice, 1001)

Event identity — two rows. If the two children stand for distinct events — two separate payments that happen to share amount and currency — the identical-tuple merge silently undercounts every multiplicity-sensitive aggregate over the family (sum, count, avg; min/max are unaffected because they ignore duplicates). The fix is in the model, not the query: give the parent a distinguishing end (a source or category end, an event id) so the two events map to two different parent tuples. Add an event-id end e to IncomeItem and each member, assert WagesUSA(alice, 500, 1) and SalaryUSA(alice, 500, 2), and the two events stay apart:

totalIncome(alice, 1000)

Pins-merge corollary. Pinning an end away is the usual way a modeler creates a collision: two members that both pin c = USD and expose the same remaining ends have byte-identical translations, so their rows always merge. Two distinct members in exactly this shape — the WagesUSA / SalaryUSA pair above — are flagged by the collision-capable-siblings warning (OW0741): it names both members and the parent and states the one-row merge consequence, so the aggregate surprise is caught at the declaration rather than discovered in a query. It is a warning, not a refusal (the merge is correct set semantics) and is suppressible where the merge is intended; the fix, when it is not, is to keep or add a distinguishing end so the two members stop pinning the distinction away.

The family-query provenance surface — the generalized specializes(k(…), Parent(…)) query and its Parent(…) via k sugar — carries the mapping through φ: a via family query reaches a non-identity mapped member, reads that member’s own extent, and presents the parent-framed rows with the pinned/renamed/cast ends filled and the answering member bound to k. The generalized specializes form with an explicit member frame still refuses (OE1416) for a non-identity member, because that form ties the member frame positionally to the member’s own ends — sound only for an equal-arity identity member; it points the modeler at via. The parent-union query above reads the closed extent and sees the mapped image directly.

A reorder routes the child’s ends to swapped parent ends by name. BackEdge(u, v, w) reverses an Edge’s endpoints:

use std::core::{type, rel};
pub type Node;
pub rel Edge(mut src: Node, mut dst: Node, mut w: Int);
// Reorder: parent end `src` is fed by child end `v`, `dst` by child end `u`.
pub rel BackEdge(mut u: Node, mut v: Node, mut w: Int) <: Edge(src = v, dst = u, w = w);

pub fact Node(n1);
pub fact Node(n2);
pub fact BackEdge(n1, n2, 7);
pub derive anyEdge(s, t, w) :- Edge(s, t, w);

BackEdge(n1, n2, 7) contributes the reversed Edge:

anyEdge(n2, n1, 7)

A cast widens a child end to a parent supersort; it is identity on the value (the value carries no sort tag), admitting the narrower child end at the parent’s declared sort:

use std::core::{type, rel};
pub type Agent;
pub type Person <: Agent;
pub type City;
pub rel Loc(a: Agent, c: City);
// Cast: the child end filling parent end `a` is widened to the supersort.
pub rel Home(p: Person, c: City) <: Loc(a = p as Agent, c = c);

pub fact Person(bob);
pub fact City(paris);
pub fact Home(bob, paris);
pub derive anyLoc(a, c) :- Loc(a, c);

anyLoc(bob, paris)

A filler that names a parent end the parent does not declare refuses with OE1411; a mapping that fills a parent end twice, or leaves one uncovered, refuses with OE1412. A mapping this build cannot yet resolve to parent positions — a filler list against a cross-module parent whose declared ends are not visible in the child’s file — refuses with OE1410 MappedSubsumptionNotYetEvaluable rather than being recorded under-resolved. (The negative-polarity dual — refuting a parent family when a non-identity edge would have to flow the refutation down to the child, which needs the mapping’s ill-defined inverse — is refused separately at the read path with OE1413.)

Why the filler list is keyed by parent end. Prefer the named filler list over the bare form on any relation whose parent ends share a sort — and note that its key names the parent end, not a position. Bare subsumption pairs the child’s ends onto the parent by position, recording that pairing nowhere in the child’s source. When two parent ends have the same sort, reordering them is a change the sort-covariance gate cannot catch — every position still type-checks — and the child declaration is byte-identical before and after, so a bare pairing flips with no diff at the site where the child is declared. Consider a transfer whose ends are both Account:

use std::core::{type, rel};
pub type Account;
// Parent ends both `Account`. Bare pairing sends the child's first end to
// `payer`, its second to `payee` — but that pairing lives only in the
// positions, not in the child's text.
pub rel Transfer(payer: Account, payee: Account);
pub rel WireTransfer(src: Account, dst: Account) <: Transfer;

Reorder the parent’s ends to Transfer(payee, payer) and this same child still compiles: src now lands on payee and dst on payer, silently reversing every transfer’s direction with no change visible at the WireTransfer declaration. The named filler list states the pairing at the child site, keyed to the parent’s end names:

use std::core::{type, rel};
pub type Account;
pub rel Transfer(payer: Account, payee: Account);
pub rel WireTransfer(src: Account, dst: Account) <: Transfer(payer = src, payee = dst);

Because each filler names the parent end it fills, the correspondence is anchored to names, not positions: it re-anchors under a parent-end reorder instead of silently re-pairing. Reorder the parent to Transfer(payee, payer) and payer = src still routes src to payer — the mapping’s meaning is unchanged; only the parent position it resolves to moves. That re-anchored mapping is now a permutation of the parent’s positions, and this stage evaluates it, so the reordered edge compiles clean and its images join the family correctly:

use std::core::{type, rel};
pub type Account;
// Parent ends reordered vs. the block above; the child is byte-identical.
pub rel Transfer(payee: Account, payer: Account);
pub rel WireTransfer(src: Account, dst: Account) <: Transfer(payer = src, payee = dst);

pub fact Account(acc_a);
pub fact Account(acc_b);
pub fact WireTransfer(acc_a, acc_b);
pub derive allTransfers(payer, payee) :- Transfer(payer, payee);

The mechanical guarantee is completed by a meaning guarantee. In the upright parent (Transfer(payer, payee)) WireTransfer(acc_a, acc_b) records acc_a as the payer; reorder the parent to Transfer(payee, payer) with the child byte-identical, and acc_a is still the payer — the filler payer = src re-anchors to the parent’s payer end wherever it now sits, and the evaluator applies the resolved permutation. The stored tuple’s positional layout follows the parent’s new order (so the raw row reads Transfer(acc_b, acc_a) — payee first now), but the account each parent end names is invariant:

# parent declared Transfer(payer, payee):  allTransfers(acc_a, acc_b)   → payer = acc_a
# parent declared Transfer(payee, payer):  allTransfers(acc_b, acc_a)   → payer = acc_a

A same-sort parent-end reorder therefore can never change a mapping’s meaning — not merely “not silently”, but not at all: the mapping is re-anchored by parent end name and evaluated through that re-anchoring, so who the child records as the payer is the same before and after the reorder. That end-to-end invariance is the acceptance criterion for keying fillers by parent end name.

When two paths disagree — the divergent-map diamond. A relation can reach the same ancestor through more than one subsumption path. When every path composes to the same mapping onto that ancestor, the diamond is harmless — a fact frames to one ancestor row whichever path is read — and it compiles. When two paths compose to different mappings, there is no single answering frame, and the declaration is refused. Here D reaches A straight through Left but end-swapped through Right:

use std::core::{type, rel};
pub type Person;
pub rel A(x: Person, y: Person);
pub rel Left(a: Person, b: Person) <: A(x = a, y = b);
pub rel Right(a: Person, b: Person) <: A(x = b, y = a);
pub rel D(p: Person, q: Person) <: Left(a = p, b = q), Right(a = p, b = q);

A D(alice, bob) fact would land at A(x = alice, y = bob) through Left and at A(x = bob, y = alice) through Right — two different ancestor rows — and a family query over A follows only the first path, silently dropping the other. The refusal names the child, the ancestor, and both composed framings in parent-name-keyed filler form:

OE1424: subsumption of `D` reaches ancestor `A` through paths whose composed mappings DIFFER — via D → Left → A: (x = p, y = q); via D → Right → A: (x = q, y = p). A `D` fact would occupy two different rows in `A`, and a family query (`via D`) would silently report only one framing (the closure follows the first path). Fix: reconcile the fillers so both paths compose to the SAME mapping onto `A`, or remove one subsumption edge. If both images are genuinely wanted, that is a feature request — the mapped-relation-subsumption design record keeps both-images open as future work.

Fix it by making the two compositions agree, or by removing one edge; if the child genuinely belongs at both ancestor rows, that is a feature request the design record keeps open as future work.

Relation-end mutability (mut, RFD 0076). Every relation end is immutable unless declared mut — the same rule, and the same modifier placement, as concept fields (RFD 0006): mut is written immediately before the end name, only in the named-end form of a concrete relation declaration. An anonymous-end mut or a mut inside a metarel signature is refused with OE0013 (mutability is declared per concrete relation end; there is no metarel-level mut). The analogy with fields stops at the declaration posture — a relation assertion is an immutable proposition and there is no relation-end update; mut governs which assertion history is legal:

use std::core::{type, rel};
pub type Person;
pub type Organization;
pub type Marriage;

// A material relation: both ends vary over time, so both opt in.
pub rel worksFor(mut employee: Person, mut employer: Organization) [0..*] [0..1];

// A mediation-shaped relation: a particular marriage cannot involve
// different spouses (`spouse` keeps the immutable default), while a
// surviving person may participate in another marriage later. The
// exact `[2]` bracket makes the initialization minimum atomic: because
// an immutable fiber freezes at its first asserting transaction, BOTH
// spouse tuples must be asserted together (`OE1398` refuses an
// under-filled initialization — the frozen set could never grow to
// complete it).
pub rel bindsSpouse(mut marriage: Marriage, spouse: Person) [0..1] [2];

The write path enforces the declaration per endpoint fiber (hold every other endpoint fixed — the same fixed-complement reading as cardinality): a matched delete R(args) on a relation with any effectively-immutable end refuses with OE1402 (deleting one tuple removes one value from every fiber, so direct retraction needs every end mut; an unmatched delete stays an idempotent no-op); for an immutable end, the first transaction asserting a fiber freezes its complete value set, and a later transaction inserting a new value there refuses with OE1403 (re-asserting an active tuple stays idempotent; a fresh dependent context initializes its own fiber). The legal removal of an immutable binding is retracting its dependent context — the individuals at the other positions — whose kernel RetractIndividuals effect cascades the incident relation retractions, refusing with OE1404 when the set would strand an immutable end’s surviving context; the capability-gated forget erasure runs the same dependent-context gate over its target’s incident tuples (on every standpoint plane the erasure sweeps), so physical erasure cannot stand in for a refused cascade. Correcting a mis-recorded binding — one that was never true — is a separate belief-time channel, the capability-gated amend verb (the record-exit, described below); it is distinct from ending a binding whose world changed (the world-exit cascade). Two declaration gates complete the picture: effective mutability is conjunctive over relation subsumption — a child may tighten a parent mut end by omitting mut, but declaring mut where any transitive superrelation keeps the position immutable refuses with OE0268 — and an end may stay immutable only when every member of its dependent context is an identity-bearing individual (a primordial-, value-, or reference-sorted context member has no lifetime whose retraction could release the binding; refused with OE0267, mark that end mut) — and the same OE0267 refuses the sole end of a unary relation, whose dependent context is empty outright (no other position exists, so no retraction could ever release the binding and the fact would be permanently frozen). The reflection plane exposes the effective bit as the total, catalog-closed armMutability(relation, index, is_mut) atom, one row per declared end.

The gates read the closed extent, not just the tuples a statement names. An insert into a subrelation contributes a row to every transitive superrelation, so an immutable parent fiber initialized through one route (a direct parent insert or a child’s) refuses growth from every other route — direct, sibling child, or child under a parent-initialized fiber — with the same OE1403 (a child re-asserting the parent’s already-active value still initializes its own fiber and is admitted). The closure spans planes too: the freeze witness reads the relation’s retained history as a single global extent — folded on the fixed complement with no standpoint axis — so an insert whose value is new for a fiber any plane initialized refuses with the same OE1403, whichever plane the initializing fact lived on. This global reading is strictly stricter than a per-plane witness (it over-refuses a value new only to a different plane, and never admits an illegal one); per-plane scoping of both the freeze witness and the cardinality gate — so a standpoint’s composed view freezes and counts only against its own retained history — is designed but not yet shipped. And a pub derive whose head names a declared relation feeds that relation’s extent, so a premise mutation that would make an immutable derived binding disappear while its dependent context survives, or grow an already-initialized immutable derived fiber, refuses the whole transaction with OE1397 — the transaction’s net rule-derived extent delta is checked atomically before anything commits; declared relation heads do not bypass mutability merely because no source delete/insert names them directly (pure derive/query heads with no relation declaration carry no end-mutability metadata and are unaffected). The initialization set itself remains governed by the declared cardinality: because an immutable fiber freezes at its first asserting transaction, a declared minimum of two or more is decidable exactly there — an initialization establishing fewer distinct values refuses with OE1398 (the frozen set could never grow to complete it) on every route: a direct insert, a subrelation insert initializing the parent fiber, a rule-derived initialization, and a static fact set (refused at ox check / ox build). A mutable end’s minimum keeps the deferred OW1342 recorded-not-enforced posture. And because the ArgUFO audit story rests on armMutability being total, the name is reserved: a user declaration named armMutability refuses with OE0704 — a same-module derive of that name would otherwise mask the catalog rows and let the very module under a forbidden-opt-out audit discharge it vacuously.

A gallery, end by end. mut is read per fiber — fix the other end and ask whether that value set may still change after its first assertion.

pub type Kid; pub type Toy; pub type Person; pub type Passport;

// Transferable ownership — a pure association, like `worksFor`. Giving a
// toy away is a `delete` + `insert`, and `delete` needs every end `mut`.
pub rel ownedBy(mut toy: Toy, mut owner: Kid) [0..*] [0..1];

// Provenance: this toy was made *for* this kid. The recipient is
// constitutive; the kid's side still grows as they receive more toys.
pub rel madeFor(mut toy: Toy, recipient: Kid) [0..*] [0..1];

// Birth: a child's birth-mother never changes; a mother's set of
// children grows with each birth.
pub rel bornTo(mut child: Person, mother: Person) [0..*] [1];

// Issuance: a passport is issued to one person forever; a person
// accumulates passports over a lifetime.
pub rel issuedTo(mut passport: Passport, holder: Person) [0..*] [1];

Fix a child and their birth-mother is one frozen value (immutable mother); fix a mother and her children accumulate (mut child) — the same shape as madeFor and issuedTo, one end constitutive of the tuple and the other accumulating history. A transferable association like ownedBy is all-mut by necessity: rebinding requires delete, and a matched delete removes a value from every fiber. Choosing mut reduces to three questions per relation: (1) will a tuple ever be deleted while both individuals still exist? — then every end is mut (an association: ownedBy, worksFor); (2) otherwise, which end is fixed the moment the tuple exists and which keeps accumulating? — the constitutive end stays immutable, the accumulating end gets mut (bornTo, madeFor, issuedTo, bindsSpouse); (3) is the only honest exit the disappearance of a participant? — then the cascade does the work and the end needs no mut. On these relations the gates read: insert bornTo with a second birth-mother for a recorded child refuses OE1403 (a second birth-mother contradicts frozen information rather than adding to it); delete issuedTo while holder and passport both survive refuses OE1402; retracting the passport cascades the frozen binding and the holder survives; retracting the holder alone refuses OE1404 while the passport’s context survives.

The choice between bindsSpouse and worksFor(mut, mut) is a modeling posture, not two kinds of fact. bindsSpouse reifies the relator — the marriage is an entity whose relata are constitutive, so its ends are immutable and its lifecycle runs through retract-and-cascade — while worksFor(mut, mut) deliberately does not reify: it tracks only the current association, a coarser view whose tuples are rebindable snapshots (history stays queryable bitemporally). A domain that cares about the employment itself declares an EmploymentContract and gives its relation immutable ends, making a job change the retraction of one contract and the creation of another — the marriage’s shape. What this design adds is that the schema now states which posture each relation takes; before, every relation silently behaved like the coarse view.

Correcting the record — amend (RFD 0076). Immutability protects two different things the write path used to conflate: the world cannot rebind an immutable end, and the record cannot be silently rewritten. Ending a binding because a participant ceases is a world-exit — the cascade (retract the dependent context, the incident tuples fall away, history retains the binding, and the vacated value can never be reused). Discovering that a binding was never true — a mis-recorded assertion, false when it was made — is a record-exit, and it is what amend performs: the assertion is withdrawn as false ab initio, releasing the freeze contribution it should never have made, while the bitemporal history retains what-was-believed-when (the correction is auditable, not an erasure). amend R(args); is the primitive (withdraw when the true value is unknown; positive evidence is withdrawn, so the proposition returns to unknown, not refuted); amend R(args) => R(args'); is the atomic composite (withdraw and assert the corrected proposition against one transaction-time view — all-or-nothing). It is a distinct verb from delete on purpose: delete is the valid-time ender (the binding stops being true now), amend is the belief-time corrector (the binding was never true). amend is capability-gated at the source level exactly as forget is: a mutate body using it refuses to build (OE1405 AmendWithoutCapability) unless the enclosing mutate declaration grants #[allow_amend]; correction authority is further authorized per invoking principal, target-scoped, at the serving layer.

pub type Person;
// Birth: a child's birth-mother never changes (immutable `mother`), but a
// mis-recorded mother is corrected at belief time.
pub rel bornTo(mut child: Person, mother: Person) [0..*] [1];

#[allow_amend]
pub mutate correct_birth_mother(child: Person, wrong: Person, right: Person) {
    // The record was wrong from the start: `child` was never born to `wrong`.
    // Withdrawing `bornTo(child, wrong)` releases the frozen `mother` fiber,
    // so the corrected `bornTo(child, right)` is admitted where a plain
    // `insert` would refuse `OE1403`.
    amend bornTo(child, wrong) => bornTo(child, right);
}

#[allow_amend]
pub mutate rescind_birth_mother(child: Person, wrong: Person) {
    // Truth not yet known: withdraw the false assertion alone. The `mother`
    // fiber re-initializes as if it had never been frozen at `wrong`.
    amend bornTo(child, wrong);
}

The amendment gates read one net corrected view of the whole transaction — the retained assert-polarity history minus the tuples this transaction amends, with corrected assertions and any lifecycle effects overlaid — so a correction cannot launder a companion cascade (the corrected tuple is live in the view the dependent-context gate reads). Two amendment-specific refusals complete the surface: amending one of several tuples in a fiber whose declared minimum exceeds one, when the surviving corrected set would drop below that minimum, refuses with OE1407 AmendmentBelowMinimum (distinct from OE1398, which refuses an under-filled initialization — OE1407 refuses an under-filling correction of an already-established fiber); and amend R(args) naming a tuple that is live but has no directly-asserted (or refuted) event — a purely rule-derived conclusion — refuses with OE1406 AmendmentTargetNotAsserted (you amend premises, not conclusions; dependency maintenance recomputes the consequence). On an all-mut relation amend is admitted (its freeze-release is vacuous there, but the false-ab-initio marking still differs from delete’s valid-time close). A tuple with neither an event nor a live row is the idempotent no-op, as an unmatched delete is.

The declaration-plane gates (OE0267/OE0268) are enforced by oxc-check in its end_mutability classifier, run over each relation declaration in the check pass; the write-path gates (OE1402–OE1404) are enforced by oxc-runtime in its end_mutability module.

Anonymous-field cardinality default. A field declared with the inline anonymous-relation form field: [T] (Form A) synthesizes a binary relation with default cardinality 0..* and Set semantics. The bounded spellings — field: [T; n..m], ordered-list opt-in field: [T; n..m, ordered] (lowering to List<T>), and the [T; <=1] singleton hint (OW2402, suggesting T? / Option<T>) — are reserved surface: no enforcement is wired yet, so a cardinality bound on a list type refuses by name (OE0014) rather than being silently discarded. Use a plain [T] until write-path enforcement lands.

Anonymous fields are structural shorthand: they do not engage the metarel calculus. No metarel name is attached; the synthesized relation is accessed only via dot-traversal. This is symmetric with struct/enum, which are likewise language-level structural and carry no metatype. Named relations (Forms B and C) require a metarel-introducing keyword in scope.

[T] on struct vs concept. On a struct or enum field, [T] is plain List<T> — no synthesized relation, no closure traversal, no metarel. On an ontologically-classified concept (declared under a metatype), [T] is Form A — a synthesized binary relation supporting closure traversal (alice.children+(b)). The difference is whether the enclosing declaration is data (struct/enum) or ontology (declared under a metatype — type or a vocabulary introducer).

When to upgrade Form A to Form B or C. Promote an anonymous field to a named relation when any of: (a) the relation needs to be classified under a metarel (mediation, material, …) so the substrate can reason over its properties; (b) the relation carries intrinsic data of its own (since: Date, amount: Money); or (c) the relation must be referenced as a first-class predicate from rule bodies (derive ancestor(d, a) :- ParentOf(d, a), …). When none of those apply, Form A is the right choice.

Generic relation-property characteristics. A named relation (rel or metarel) may carry the standard relation-algebra property characteristics (the OWL object-property characteristics) — PL/DB-neutral, describing the shape of the relation’s extent with enforcement, not an ontological commitment. All four are shipped by the std::rel standard-library package and must be brought into scope — use std::rel::{transitive, irreflexive, asymmetric, functional} (nothing is ambient — Name resolution / RFD 0038). #[transitive] is a genuine declarative macro (it expands to the closure derive). #[irreflexive] and #[asymmetric] are genuine procedural macros (RFD 0040): they re-emit the relation and paste the guarding check’s internal __{rel}_{prop} head via concat_idents. They read the relation’s name, so they apply to a rel; on a metarel they decline (the invocation is refused, OE0723). #[functional] is likewise a genuine procedural macro (RFD 0040 P2): BOTH its rel and metarel arms re-emit the decorated declaration and paste a __{rel}_functional check that fires when a source maps to two distinct targets (OE1361) — the same check-based enforcement as its siblings. A rel whose explicit target cardinality permits more than one target contradicts #[functional] and is refused (OE1378). A characteristic applied without its import is refused — OE0705 for every macro (#[transitive]/#[irreflexive]/#[asymmetric]/#[functional]; OE1362 is retired). Multiple characteristics compose on one declaration (re-emitting $item verbatim, a stacked sibling and the user’s brackets/generics/body all survive).

use std::rel::{transitive, irreflexive, asymmetric, functional};

#[transitive]
#[irreflexive]
#[asymmetric]
pub rel is_proper_part_of(part: Top, whole: Top);

#[functional]
pub rel inheres_in(burden: Aspect, bearer: ConcreteIndividual);  // each aspect inheres in one bearer

Enforcement applies to the declared relation’s own extent. Propagation of a property borne by a metarel to the relations it classifies is out of scope (Out of scope). A characteristic applied without importing it from std::rel is refused — OE0705 for every macro (#[transitive]/#[irreflexive]/#[asymmetric]/#[functional]; all genuine macros, not directives). #[functional] applies to both a binary rel and a binary metarel (each arm pastes the source-maps-two-targets check); #[irreflexive]/#[asymmetric] apply only to a rel and decline on a metarel (the invocation is refused, OE0723). On a non-relation declaration (a concept, a rule) the invocation likewise fails to match and is refused (OE0723). (The ontology-specific relation properties — MLT’s #[partitions], #[categorizes], etc. — are vocabulary decorators and live in their packages, distinct from this generic family.)