A Property Kind Calculus for Measurement Metrology

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.