Prototypes — Graded Category Membership

A prototype attaches a typicality grade (ℚ) to each member of a category. Higher values are more prototypical. Used wherever graded membership is needed (e.g. color-term typicality @cite{westerbeek-koolen-maes-2015}).

The TypicalityOrder wrapper carries the Preorder instance derived from typicality: (a : TypicalityOrder p) ≤ b ↔ p.typicality a ≤ p.typicality b. The wrapper pattern (cf. Core.Inheritance.IsAOrder) is needed because a single α may carry multiple unrelated prototype gradings.

structure Core.Prototype (α : Type) : Type

A prototype: a category with graded typicality over instances. Higher values = more prototypical.

• category : α
• typicality : α → ℚ

def Core.Prototype.AtLeastAsTypical {α : Type} (proto : Prototype α) (a b : α) : Prop

a is at least as typical as b in proto.

Equations

• proto.AtLeastAsTypical a b = (proto.typicality b ≤ proto.typicality a)

@[implicit_reducible]

instance Core.Prototype.instDecidableRelAtLeastAsTypical {α : Type} (proto : Prototype α) : DecidableRel proto.AtLeastAsTypical

Equations

• proto.instDecidableRelAtLeastAsTypical x✝¹ x✝ = Core.Prototype.instDecidableRelAtLeastAsTypical._aux_1 proto x✝¹ x✝

def Core.Prototype.MoreTypical {α : Type} (proto : Prototype α) (a b : α) : Prop

a is strictly more typical than b in proto.

Equations

• proto.MoreTypical a b = (proto.typicality b < proto.typicality a)

@[implicit_reducible]

instance Core.Prototype.instDecidableRelMoreTypical {α : Type} (proto : Prototype α) : DecidableRel proto.MoreTypical

Equations

• proto.instDecidableRelMoreTypical x✝¹ x✝ = Core.Prototype.instDecidableRelMoreTypical._aux_1 proto x✝¹ x✝

theorem Core.Prototype.atLeastAsTypical_refl {α : Type} (proto : Prototype α) (a : α) : proto.AtLeastAsTypical a a

theorem Core.Prototype.atLeastAsTypical_trans {α : Type} (proto : Prototype α) {a b c : α} (hab : proto.AtLeastAsTypical a b) (hbc : proto.AtLeastAsTypical b c) : proto.AtLeastAsTypical a c

def Core.TypicalityOrder {α : Type} : Prototype α → Type

A node type viewed as preordered by typicality under a particular prototype. Definitionally equal to α, but carries the Preorder instance. Mirrors Core.Inheritance.IsAOrder.

Equations

• Core.TypicalityOrder x✝ = α

def Core.TypicalityOrder.mk {α : Type} (proto : Prototype α) (a : α) : TypicalityOrder proto

Tag a value as inhabiting the typicality preorder of proto. The function-call wrapper avoids the elaboration pitfall where (a : TypicalityOrder proto) ascription gets unfolded to α during instance search.

Equations

• Core.TypicalityOrder.mk proto a = a

def Core.TypicalityOrder.val {α : Type} {proto : Prototype α} (a : TypicalityOrder proto) : α

Forget the typicality view, returning the underlying value.

Equations

• a.val = a

@[implicit_reducible]

instance Core.TypicalityOrder.preorder {α : Type} (proto : Prototype α) : Preorder (TypicalityOrder proto)

Preorder by typicality: a ≤ b iff b is at least as typical as a.

Equations

• Core.TypicalityOrder.preorder proto = { le := fun (a b : Core.TypicalityOrder proto) => proto.AtLeastAsTypical b a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[simp]

theorem Core.TypicalityOrder.le_def {α : Type} (proto : Prototype α) (a b : TypicalityOrder proto) : a ≤ b ↔ proto.AtLeastAsTypical b a

@[simp]

theorem Core.TypicalityOrder.val_mk {α : Type} (proto : Prototype α) (a : α) : (mk proto a).val = a