inductive PropertyKindCalculus.ScaleType : Type

The four operator-based scale types of Dybkær Fig. 12.21.

• nominal : ScaleType

  §12.4 nominal — only =, ≠ (classification; no order, no magnitude).

• ordinal : ScaleType

  §12.16 ordinal — adds <, > (rankable, but not subtractive).

• interval : ScaleType

  §12.19 interval — adds +, − (subtractive, but not divisible).

• ratio : ScaleType

  §12.20 ratio — adds ×, ÷ (divisible; an absolute zero).

@[instance_reducible]

instance PropertyKindCalculus.instDecidableEqScaleType : DecidableEq ScaleType

Equations

• PropertyKindCalculus.instDecidableEqScaleType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PropertyKindCalculus.instReprScaleType : Repr ScaleType

Equations

• PropertyKindCalculus.instReprScaleType = { reprPrec := PropertyKindCalculus.instReprScaleType.repr }

def PropertyKindCalculus.instReprScaleType.repr : ScaleType → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def PropertyKindCalculus.ScaleType.rank : ScaleType → Nat

Operator-richness rank: nominal ⊏ ordinal ⊏ interval ⊏ ratio.

Equations

• PropertyKindCalculus.ScaleType.nominal.rank = 0
• PropertyKindCalculus.ScaleType.ordinal.rank = 1
• PropertyKindCalculus.ScaleType.interval.rank = 2
• PropertyKindCalculus.ScaleType.ratio.rank = 3

@[instance_reducible]

instance PropertyKindCalculus.ScaleType.instLE : LE ScaleType

Equations

• PropertyKindCalculus.ScaleType.instLE = { le := fun (a b : PropertyKindCalculus.ScaleType) => a.rank ≤ b.rank }

theorem PropertyKindCalculus.ScaleType.le_def {a b : ScaleType} : a ≤ b ↔ a.rank ≤ b.rank

theorem PropertyKindCalculus.ScaleType.le_refl (a : ScaleType) : a ≤ a

theorem PropertyKindCalculus.ScaleType.le_trans {a b c : ScaleType} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c

theorem PropertyKindCalculus.ScaleType.le_antisymm {a b : ScaleType} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

Which operations are defined at each scale (cumulative)

def PropertyKindCalculus.ScaleType.AllowsOrder : ScaleType → Prop

<, > available from ordinal upward (§12.16).

Equations

• PropertyKindCalculus.ScaleType.nominal.AllowsOrder = False
• x✝.AllowsOrder = True

def PropertyKindCalculus.ScaleType.AllowsDifference : ScaleType → Prop

+, − available from interval upward (§12.19).

Equations

• PropertyKindCalculus.ScaleType.interval.AllowsDifference = True
• PropertyKindCalculus.ScaleType.ratio.AllowsDifference = True
• x✝.AllowsDifference = False

def PropertyKindCalculus.ScaleType.AllowsRatio : ScaleType → Prop

×, ÷ available only at ratio scale (§12.20).

Equations

• PropertyKindCalculus.ScaleType.ratio.AllowsRatio = True
• x✝.AllowsRatio = False

def PropertyKindCalculus.ScaleType.HasMagnitude (s : ScaleType) : Prop

§13.3.1 — a kind has magnitude (is a kind-of-quantity, not merely nominal) iff its scale is at least ordinal.

Equations

• s.HasMagnitude = (s ≠ PropertyKindCalculus.ScaleType.nominal)

theorem PropertyKindCalculus.ScaleType.allows_mono {a b : ScaleType} (h : a ≤ b) : (a.AllowsOrder → b.AllowsOrder) ∧ (a.AllowsDifference → b.AllowsDifference) ∧ (a.AllowsRatio → b.AllowsRatio)

Meta-theorem OWL2's reasoner cannot even phrase: a richer scale licenses every operation a poorer one does. (Monotonicity of operator availability.)