6.3. Specialization and mutual comparability (OML / Dybkær §6)🔗

Definition6.3.1

Group: Specializes relates kinds to kinds. Flater (NIST TN 1943 §6.2) stresses the result is a lattice, not a tree. We generate it as the reflexive–transitive closure of an application-supplied direct-parent edge relation, so each "system of quantities" supplies its own hierarchy. (3)

Group member previews

Preview

Theorem 6.3.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 8

Reverse dependency previews

Preview

Theorem 6.3.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Specialization Specializes E is the reflexive–transitive closure of a direct-parent edge relation E over kind-of-property. Different E give different per-application hierarchies — the extensibility a fixed inductive would deny.

Lean code for Definition6.3.1●1 definition

inductive(2 constructors, Prop, 3 parameters)defined in PropertyKindCalculus/Specialization.lean

complete

inductive PropertyKindCalculus.Specializes
  (E :
    PropertyKindCalculus.KindOfProperty →
      PropertyKindCalculus.KindOfProperty → Prop) :
  PropertyKindCalculus.KindOfProperty →
    PropertyKindCalculus.KindOfProperty → Prop

inductive PropertyKindCalculus.Specializes
  (E :
    PropertyKindCalculus.KindOfProperty →
      PropertyKindCalculus.KindOfProperty →
        Prop) :
  PropertyKindCalculus.KindOfProperty →
    PropertyKindCalculus.KindOfProperty →
      Prop

Reflexive–transitive closure of a direct-parent edge relation `E`.

Constructors

PropertyKindCalculus.Specializes.refl
  {E :
    PropertyKindCalculus.KindOfProperty →
      PropertyKindCalculus.KindOfProperty → Prop}
  (a : PropertyKindCalculus.KindOfProperty) :
  PropertyKindCalculus.Specializes E a a

Reflexivity of the closure: every kind specializes itself.

PropertyKindCalculus.Specializes.step
  {E :
    PropertyKindCalculus.KindOfProperty →
      PropertyKindCalculus.KindOfProperty → Prop}
  {a b c : PropertyKindCalculus.KindOfProperty} :
  E a b →
    PropertyKindCalculus.Specializes E b c →
      PropertyKindCalculus.Specializes E a c

Prepend a direct-parent edge `E a b` to a specialization `b ⊑ c`.

Proof for Definition 6.3.1

uses 0

An inductive with refl and step constructors; of_edge lifts a single edge.

Theorem6.3.2

Group member previews

Preview

Definition 6.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

OwnerNicolas RouquettePriorityhighTagscapstoneproved

Specialization is a preorder. It is reflexive (the refl constructor) and transitive (Specializes.trans). Stating — let alone proving — an algebraic law of the taxonomy is exactly what an OWL2 reasoner cannot do; it checks consistency, not laws. Uses specialization.

Lean code for Theorem6.3.2●1 theorem

theoremdefined in PropertyKindCalculus/Specialization.lean

complete

theorem PropertyKindCalculus.Specializes.trans
  {E :
    PropertyKindCalculus.KindOfProperty →
      PropertyKindCalculus.KindOfProperty → Prop}
  {a b c : PropertyKindCalculus.KindOfProperty}
  (h₁ : PropertyKindCalculus.Specializes E a b)
  (h₂ : PropertyKindCalculus.Specializes E b c) :
  PropertyKindCalculus.Specializes E a c

theorem PropertyKindCalculus.Specializes.trans
  {E :
    PropertyKindCalculus.KindOfProperty →
      PropertyKindCalculus.KindOfProperty →
        Prop}
  {a b c :
    PropertyKindCalculus.KindOfProperty}
  (h₁ :
    PropertyKindCalculus.Specializes E a
      b)
  (h₂ :
    PropertyKindCalculus.Specializes E b
      c) :
  PropertyKindCalculus.Specializes E a c

Specialization is transitive (it is a preorder, together with `refl`).

Proof for Theorem 6.3.2

uses 0

Transitivity is by induction on the first derivation: refl returns the second derivation, step re-applies the constructor under the inductive hypothesis.

Definition6.3.3

Group member previews

Preview

Definition 6.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 6.3.4

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Two kinds are mutually comparable iff they share a common super-kind (\exists p,\ a \sqsubseteq p \wedge b \sqsubseteq p). This is how width and height stay comparable as lengths while remaining distinct sub-kinds. Uses specialization.

Lean code for Definition6.3.3●1 definition

defdefined in PropertyKindCalculus/Specialization.lean

complete

def PropertyKindCalculus.MutuallyComparable
  (E :
    PropertyKindCalculus.KindOfProperty →
      PropertyKindCalculus.KindOfProperty → Prop)
  (a b : PropertyKindCalculus.KindOfProperty) : Prop

def PropertyKindCalculus.MutuallyComparable
  (E :
    PropertyKindCalculus.KindOfProperty →
      PropertyKindCalculus.KindOfProperty →
        Prop)
  (a b :
    PropertyKindCalculus.KindOfProperty) :
  Prop

**Dybkær §6 / VIM4 2CD 1.2** (quantities of the same kind) — two kinds are
*mutually comparable* (belong to one broad kind) iff they share a common
super-kind. This is how `width` and `height` remain comparable as lengths even
though they are distinct sub-kinds.

Proof for Definition 6.3.3

uses 0

An existential over a shared upper bound.

Theorem6.3.4

Group member previews

Preview

Definition 6.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

OwnerNicolas RouquetteTagsproved

Mutual comparability is reflexive (refl) and symmetric (symm), and any specialization induces it (of_specializes). Uses mutual comparability.

Lean code for Theorem6.3.4●1 theorem

theoremdefined in PropertyKindCalculus/Specialization.lean

complete

theorem PropertyKindCalculus.MutuallyComparable.symm
  {E :
    PropertyKindCalculus.KindOfProperty →
      PropertyKindCalculus.KindOfProperty → Prop}
  {a b : PropertyKindCalculus.KindOfProperty}
  (h : PropertyKindCalculus.MutuallyComparable E a b) :
  PropertyKindCalculus.MutuallyComparable E b a

theorem PropertyKindCalculus.MutuallyComparable.symm
  {E :
    PropertyKindCalculus.KindOfProperty →
      PropertyKindCalculus.KindOfProperty →
        Prop}
  {a b :
    PropertyKindCalculus.KindOfProperty}
  (h :
    PropertyKindCalculus.MutuallyComparable
      E a b) :
  PropertyKindCalculus.MutuallyComparable
    E b a

Proof for Theorem 6.3.4

uses 0

Reflexivity takes the witness a itself; symmetry swaps the two halves of the conjunction.