2.1. Kind structure (R1, R2, R3, R19, R22)
R1 — Kinds are first-class and discriminate within a dimension. Two properties
of the same physical dimension can still be different kinds, and the type system
must keep them apart. Volumetric water content (Quantity vwc), gravimetric
water content (Quantity gwc), relative permittivity, reflectivity, and
emissivity are all dimension-one, yet Quantity vwc and Quantity gwc must be
different types — not interchangeable values. (QUDT's and SysML v2's QuantityKind is subsumed here as one such kind —
a scale-gated leaf — not as the root.) This reaches its limit on ISO 80000-11
Characteristic numbers, where all 115 kinds — every one a dimensionless ratio — share
dimension one, so the dimension functor collapses the entire part to a single point and
only the kind layer holds its members apart (see the ISO 80000-11 chapter). The
principled form of this within-dimension discrimination — naming a kind by the
system and component it is dedicated to, so volumetric and gravimetric water
content differ by their kind-of-property rather than by an identity string — is
Dybkær's dedicated kind-of-property (see the Dedicated kinds-of-property chapter).
R2 — Specialization is a lattice, with comparability but not identity. Width,
Height, and Diameter each specialize Length, and a kind may specialize several
parents at once — a lattice, not a tree. Specialization is a preorder (reflexive
and transitive) and induces a one-way coercion: a Quantity Width may be used
where a Quantity Length is wanted, never the reverse, and that up-cast is a
visible, deliberate loss of information — realized as Quantity.widen, the lift along a
proved Specializes, with the sum and the comparison of comparable kinds licensed at
the join (SpecializationLift). Width and Height remain mutually
comparable — they share the super-kind Length — while staying distinct kinds. This
requirement is now realized on the real standard: the ISO 80000-3 length family
(width, height, distance, radius, … of items 3-1.2 … 3-1.12, all of dimension L)
is specified as a specialization lattice over the general length kind, each species
individuated not by fiat but by an explicit measurement principle (see the
ISO 80000-3 chapter), and the same pattern recurs on Part 4's force family, Part 5's
thermodynamic potentials, and IEC 80000-6's AC power family — active, reactive, and
apparent power as species of one power kind, carrying three different unit strings
(W, var, VA) over one dimension (see the IEC 80000-6 chapter) — and on ISO 80000-7's
radiation trios, where radiant, luminous, and photon flux are one measurand in three
modes, the radiant and luminous members even sharing a dimension (see the
ISO 80000-7 chapter). ISO 80000-11 pushes this furthest: the same name recurs as a
different kind across its transport-phenomena clauses — the two Froude numbers, the five
Stokes numbers, the four Bejan numbers — each sub-suffixed sibling sharing both name and
dimension (one) with the others, so the measurement principle alone tells them apart (see
the ISO 80000-11 chapter).
R3 — General versus individual is type versus term. A kind is the general
notion (a type); a particular measured value is an individual (a term of that
type). Length is a type; the length of this pencil is a term of type
Quantity Length. The two are never conflated — the punning OWL permits between a
class and its instances is structurally impossible here.
R19 — A quantity characterizes an object; object identity is carried in the type.
R3 separates the general from the individual; R19 says whose individual. A measured
value characterizes some object — this pencil, oscillator A — and that object rides in
the type (IndividualQuantity o k R), so two same-kind quantities of different objects
are different types and ω_A · x_B is a compile-time error, not a naming convention.
Same kind, different object; the object axis is independent of the kind axis, which is
exactly what dissolves the tagging dilemma (a dimension tag can make masses
distinguishable or addable, never both — the object index makes them both). The object
is drawn from an arbitrary type, not from the nominal system carrier alone, so a host
library's own objects — the particles of a mechanical system, the cells of a mesh — are
admissible indices without that library changing; see the object type chapter for
what that costs and what it does not buy.
R22 — A quantity is dedicated to a named component of a named sort of system;
dedications of distinct sorts are provably distinct, and the particular is the object
index's. The sharpened successor of the part of R19 that "object identity" undersold,
minted from the ForPhysLib benchmark's two-rover construction (see Requirement
validation below): with one system there is no way to distinguish "the sum of the
parts" from "the sum of some masses of the right dimension", because every mass in
scope is a correct summand. DedicatedKind records the System — Component ; kind
triple with the System slot naming the sort — one catalogue entry for the fleet
(distinct_of_sort, dedicatedFor_congr) — and the object index is what makes
cross-system substitution — rover 1's total mass drawing on rover 2's wheel — a type
error rather than a modeling discipline.