Documentation

Studies.ChenVanDeemter2023

Chen and van Deemter (2023): Varieties of Specification #

This file formalizes the set-theoretic account of over- and under-specification in [CvD23]. A description is a bag of attribute–value pairs over the knowledge base of [DR95], and it is distinguishing when it holds of the referent and of no distractor. An over-specification is a distinguishing description that is not minimal, and it is real, numerical, nominal or duplicate-attribute according to which of its occurrences are superfluous; an under-specification, whose extension in the setting properly contains the referent, is mixed when some occurrence can be dropped without changing the extension and pure otherwise; a wrong description has a property false of the referent. The paper's four theorems hold for any knowledge base and nonempty set of distractors, and the worked examples of its running scene are classified.

Implementation notes #

Descriptions are multisets so that a property can occur twice. On a Finset description Distinguishing is Dale and Reiter's (distinguishing_val_iff).
A superfluous occurrence is one of a distinguishing description, as the paper defines it. The remark under its nominal over-specification that distinguishing need not be required separately holds only for properties true of the referent, so the definitions here carry it.
Minimality counts property occurrences, as MinimalFor on the multiset's cardinality among distinguishing descriptions.
The theorem that a duplicate-attribute over-specification is real or nominal uses that a knowledge base assigns one value per attribute, so a distinguishing description has one type.
The scenes carry the objects and colours of the paper's two figures. Sizes and orientations, which the figures do not label, are as the text's classifications require: only the target of the first scene is large, and in the second every small object is green and the target and one other desk face front.

References #

@[reducible, inline]

abbrev ChenVanDeemter2023.Description (A : Type u_4) (V : Type u_5) :

Type (max u_5 u_4)

A description, a bag of attribute–value pairs.

Equations

ChenVanDeemter2023.Description A V = Multiset (A × V)

Instances For

def ChenVanDeemter2023.extension {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : DaleReiter1995.KB E A V) (D : Description A V) (x : E) :

Every pair of the description holds of the entity.

Equations

ChenVanDeemter2023.extension kb D x = ∀ p ∈ D, DaleReiter1995.Applies kb x p

Instances For

@[instance_reducible]

instance ChenVanDeemter2023.instDecidableExtensionOfDecidableEq {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : DaleReiter1995.KB E A V) (D : Description A V) [DecidableEq V] (x : E) :

Decidable (extension kb D x)

Equations

ChenVanDeemter2023.instDecidableExtensionOfDecidableEq kb D x = id inferInstance

@[reducible, inline]

abbrev ChenVanDeemter2023.Distinguishing {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) :

The description holds of the referent and of no distractor.

Equations

ChenVanDeemter2023.Distinguishing kb r C D = Reference.Distinguishes (ChenVanDeemter2023.extension kb) C r D

Instances For

def ChenVanDeemter2023.IsMinimal {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) :

A distinguishing description with the fewest property occurrences.

Equations

ChenVanDeemter2023.IsMinimal kb r C D = MinimalFor (ChenVanDeemter2023.Distinguishing kb r C) Multiset.card D

Instances For

def ChenVanDeemter2023.OverSpecified {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) :

A distinguishing description that is not minimal.

Equations

ChenVanDeemter2023.OverSpecified kb r C D = (ChenVanDeemter2023.Distinguishing kb r C D ∧ ¬ChenVanDeemter2023.IsMinimal kb r C D)

Instances For

def ChenVanDeemter2023.UnderSpecified {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) :

The description holds of the referent and of some distractor.

Equations

ChenVanDeemter2023.UnderSpecified kb r C D = (ChenVanDeemter2023.extension kb D r ∧ ∃ c ∈ C, ChenVanDeemter2023.extension kb D c)

Instances For

@[instance_reducible]

instance ChenVanDeemter2023.instDecidableUnderSpecifiedOfDecidableEq {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) [DecidableEq V] :

Decidable (UnderSpecified kb r C D)

Equations

ChenVanDeemter2023.instDecidableUnderSpecifiedOfDecidableEq kb r C D = id inferInstance

def ChenVanDeemter2023.Wrong {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : DaleReiter1995.KB E A V) (r : E) (D : Description A V) :

Some property is false of the referent.

Equations

ChenVanDeemter2023.Wrong kb r D = ∃ p ∈ D, ¬DaleReiter1995.Applies kb r p

Instances For

@[instance_reducible]

instance ChenVanDeemter2023.instDecidableWrongOfDecidableEq {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : DaleReiter1995.KB E A V) (r : E) (D : Description A V) [DecidableEq V] :

Decidable (Wrong kb r D)

Equations

ChenVanDeemter2023.instDecidableWrongOfDecidableEq kb r D = id Multiset.decidableExistsMultiset

theorem ChenVanDeemter2023.distinguishing_val_iff {E : Type u_1} {A : Type u_2} {V : Type u_3} {kb : DaleReiter1995.KB E A V} {r : E} {C : Finset E} (hC : C.Nonempty) {L : DaleReiter1995.Description A V} :

Distinguishing kb r C L.val ↔ DaleReiter1995.Distinguishing kb r C L

On a set of pairs the notion is Dale and Reiter's.

theorem ChenVanDeemter2023.not_distinguishing_zero {E : Type u_1} {A : Type u_2} {V : Type u_3} {kb : DaleReiter1995.KB E A V} {r : E} {C : Finset E} (hC : C.Nonempty) :

¬Distinguishing kb r C 0

theorem ChenVanDeemter2023.Distinguishing.extension_referent {E : Type u_1} {A : Type u_2} {V : Type u_3} {kb : DaleReiter1995.KB E A V} {r : E} {C : Finset E} {D : Description A V} (hC : C.Nonempty) (h : Distinguishing kb r C D) :

extension kb D r

theorem ChenVanDeemter2023.Distinguishing.not_extension {E : Type u_1} {A : Type u_2} {V : Type u_3} {kb : DaleReiter1995.KB E A V} {r : E} {C : Finset E} {D : Description A V} (hC : C.Nonempty) (h : Distinguishing kb r C D) {c : E} (hc : c ∈ C) :

¬extension kb D c

theorem ChenVanDeemter2023.isMinimal_of_card_eq_one {E : Type u_1} {A : Type u_2} {V : Type u_3} {kb : DaleReiter1995.KB E A V} {r : E} {C : Finset E} {D : Description A V} (hC : C.Nonempty) (h : Distinguishing kb r C D) (h1 : Multiset.card D = 1) :

IsMinimal kb r C D

A distinguishing description with one occurrence is minimal.

theorem ChenVanDeemter2023.Applies.snd_eq {E : Type u_1} {A : Type u_2} {V : Type u_3} {kb : DaleReiter1995.KB E A V} {x : E} {p q : A × V} (hp : DaleReiter1995.Applies kb x p) (hq : DaleReiter1995.Applies kb x q) (h : p.1 = q.1) :

p.2 = q.2

A knowledge base assigns one value per attribute.

theorem ChenVanDeemter2023.UnderSpecified.not_wrong {E : Type u_1} {A : Type u_2} {V : Type u_3} {kb : DaleReiter1995.KB E A V} {r : E} {C : Finset E} {D : Description A V} (h : UnderSpecified kb r C D) :

¬Wrong kb r D

def ChenVanDeemter2023.Superfluous {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) (p : A × V) :

An occurrence of a distinguishing description whose removal leaves it distinguishing.

Equations

ChenVanDeemter2023.Superfluous kb r C D p = (ChenVanDeemter2023.Distinguishing kb r C D ∧ p ∈ D ∧ ChenVanDeemter2023.Distinguishing kb r C (Multiset.erase D p))

Instances For

@[instance_reducible]

instance ChenVanDeemter2023.instDecidableSuperfluous {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) (p : A × V) :

Decidable (Superfluous kb r C D p)

Equations

ChenVanDeemter2023.instDecidableSuperfluous kb r C D p = id inferInstance

def ChenVanDeemter2023.RealOverSpecified {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (t : A) (r : E) (C : Finset E) (D : Description A V) :

Some property other than the type is superfluous.

Equations

ChenVanDeemter2023.RealOverSpecified kb t r C D = ∃ p ∈ D, p.1 ≠ t ∧ ChenVanDeemter2023.Superfluous kb r C D p

Instances For

def ChenVanDeemter2023.NumericallyOverSpecified {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) :

A distinguishing description with no superfluous occurrence that is not minimal.

Equations

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

Instances For

def ChenVanDeemter2023.NominallyOverSpecified {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (t : A) (r : E) (C : Finset E) (D : Description A V) :

The type is superfluous and no other property is.

Equations

ChenVanDeemter2023.NominallyOverSpecified kb t r C D = ∃ p ∈ D, p.1 = t ∧ ChenVanDeemter2023.Superfluous kb r C D p ∧ ∀ q ∈ D, q ≠ p → ¬ChenVanDeemter2023.Superfluous kb r C D q

Instances For

def ChenVanDeemter2023.DuplicateOverSpecified {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) :

A property occurs twice and is superfluous.

Equations

ChenVanDeemter2023.DuplicateOverSpecified kb r C D = ∃ p ∈ D, 2 ≤ Multiset.count p D ∧ ChenVanDeemter2023.Superfluous kb r C D p

Instances For

def ChenVanDeemter2023.Mixed {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) :

An under-specification with an occurrence whose removal leaves its extension on the setting unchanged; the referent stays in the extension by under-specification, so only the distractors are checked.

Equations

ChenVanDeemter2023.Mixed kb r C D = (ChenVanDeemter2023.UnderSpecified kb r C D ∧ ∃ p ∈ D, ∀ c ∈ C, ChenVanDeemter2023.extension kb (Multiset.erase D p) c → ChenVanDeemter2023.extension kb D c)

Instances For

def ChenVanDeemter2023.PurelyUnderSpecified {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) :

An under-specification that is not mixed.

Equations

ChenVanDeemter2023.PurelyUnderSpecified kb r C D = (ChenVanDeemter2023.UnderSpecified kb r C D ∧ ¬ChenVanDeemter2023.Mixed kb r C D)

Instances For

@[instance_reducible]

instance ChenVanDeemter2023.instDecidableRealOverSpecified {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (t : A) (r : E) (C : Finset E) (D : Description A V) :

Decidable (RealOverSpecified kb t r C D)

Equations

ChenVanDeemter2023.instDecidableRealOverSpecified kb t r C D = id Multiset.decidableExistsMultiset

@[instance_reducible]

instance ChenVanDeemter2023.instDecidableNominallyOverSpecified {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (t : A) (r : E) (C : Finset E) (D : Description A V) :

Decidable (NominallyOverSpecified kb t r C D)

Equations

ChenVanDeemter2023.instDecidableNominallyOverSpecified kb t r C D = id Multiset.decidableExistsMultiset

@[instance_reducible]

instance ChenVanDeemter2023.instDecidableDuplicateOverSpecified {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) :

Decidable (DuplicateOverSpecified kb r C D)

Equations

ChenVanDeemter2023.instDecidableDuplicateOverSpecified kb r C D = id Multiset.decidableExistsMultiset

@[instance_reducible]

instance ChenVanDeemter2023.instDecidableMixed {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) :

Decidable (Mixed kb r C D)

Equations

ChenVanDeemter2023.instDecidableMixed kb r C D = id instDecidableAnd

@[instance_reducible]

instance ChenVanDeemter2023.instDecidablePurelyUnderSpecified {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] (kb : DaleReiter1995.KB E A V) (r : E) (C : Finset E) (D : Description A V) :

Decidable (PurelyUnderSpecified kb r C D)

Equations

ChenVanDeemter2023.instDecidablePurelyUnderSpecified kb r C D = id inferInstance

theorem ChenVanDeemter2023.Superfluous.not_isMinimal {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] {kb : DaleReiter1995.KB E A V} {r : E} {C : Finset E} {D : Description A V} {p : A × V} (h : Superfluous kb r C D p) :

¬IsMinimal kb r C D

theorem ChenVanDeemter2023.theorem1 {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] {kb : DaleReiter1995.KB E A V} {t : A} {r : E} {C : Finset E} {D : Description A V} :

(IsMinimal kb r C D → Distinguishing kb r C D) ∧ (RealOverSpecified kb t r C D → Distinguishing kb r C D) ∧ (NumericallyOverSpecified kb r C D → Distinguishing kb r C D) ∧ (NominallyOverSpecified kb t r C D → Distinguishing kb r C D) ∧ (DuplicateOverSpecified kb r C D → Distinguishing kb r C D)

Every kind of over-specification is distinguishing.

theorem ChenVanDeemter2023.theorem2 {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] {kb : DaleReiter1995.KB E A V} {r : E} {C : Finset E} {D : Description A V} (hC : C.Nonempty) (h : Distinguishing kb r C D) :

¬Mixed kb r C D ∧ ¬PurelyUnderSpecified kb r C D ∧ ¬Wrong kb r D

A distinguishing description is neither mixed, purely under-specified nor wrong.

theorem ChenVanDeemter2023.theorem3 {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] {kb : DaleReiter1995.KB E A V} {t : A} {r : E} {C : Finset E} (hC : C.Nonempty) :

List.Pairwise (fun (P Q : Description A V → Prop) => ∀ (D : Description A V), ¬(P D ∧ Q D)) [IsMinimal kb r C, RealOverSpecified kb t r C, NumericallyOverSpecified kb r C, NominallyOverSpecified kb t r C, Mixed kb r C, PurelyUnderSpecified kb r C, Wrong kb r]

The seven kinds of description exclude one another.

theorem ChenVanDeemter2023.theorem4 {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] {kb : DaleReiter1995.KB E A V} {t : A} {r : E} {C : Finset E} {D : Description A V} (hC : C.Nonempty) (h : DuplicateOverSpecified kb r C D) :

RealOverSpecified kb t r C D ∨ NominallyOverSpecified kb t r C D

A duplicate-attribute over-specification is real or nominal, since the type occurrences of a distinguishing description are one pair.

The scenes of the examples #

inductive ChenVanDeemter2023.Obj :

The objects of the two scenes.

greyDesk : Obj
redSofa : Obj
greenChair : Obj
greenSofa : Obj
blueChair : Obj
greenFan : Obj
greenDesk : Obj
greyChair : Obj
largeGreenChair : Obj
smallGreenChair : Obj
targetDesk : Obj
largeGreenDesk : Obj
smallGreenDesk : Obj
greyDesk' : Obj

Instances For

@[instance_reducible]

instance ChenVanDeemter2023.instDecidableEqObj :

DecidableEq Obj

Equations

ChenVanDeemter2023.instDecidableEqObj x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChenVanDeemter2023.instReprObj.repr :

Obj → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ChenVanDeemter2023.instReprObj :

Repr Obj

Equations

ChenVanDeemter2023.instReprObj = { reprPrec := ChenVanDeemter2023.instReprObj.repr }

inductive ChenVanDeemter2023.Attr :

The attributes, with type the head noun.

type : Attr
size : Attr
colour : Attr
orientation : Attr

Instances For

@[instance_reducible]

instance ChenVanDeemter2023.instDecidableEqAttr :

DecidableEq Attr

Equations

ChenVanDeemter2023.instDecidableEqAttr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChenVanDeemter2023.instReprAttr.repr :

Attr → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ChenVanDeemter2023.instReprAttr :

Repr Attr

Equations

ChenVanDeemter2023.instReprAttr = { reprPrec := ChenVanDeemter2023.instReprAttr.repr }

inductive ChenVanDeemter2023.Value :

The values.

chair : Value
sofa : Value
desk : Value
fan : Value
large : Value
small : Value
grey : Value
red : Value
green : Value
blue : Value
front : Value
side : Value

Instances For

@[instance_reducible]

instance ChenVanDeemter2023.instDecidableEqValue :

DecidableEq Value

Equations

ChenVanDeemter2023.instDecidableEqValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChenVanDeemter2023.instReprValue.repr :

Value → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ChenVanDeemter2023.instReprValue :

Repr Value

Equations

ChenVanDeemter2023.instReprValue = { reprPrec := ChenVanDeemter2023.instReprValue.repr }

def ChenVanDeemter2023.scene₁ :

DaleReiter1995.KB Obj Attr Value

The first scene, a large green chair among a grey desk, a red sofa, a green sofa, a blue chair, a green fan and a green desk.

Equations

Instances For

def ChenVanDeemter2023.distractors₁ :

Finset Obj

The distractors of the first scene.

Equations

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

Instances For

theorem ChenVanDeemter2023.scene₁_over :

The large one is minimal, the large green one a real over-specification, the green chair a numerical one, the large chair a nominal one, and the green chair that has the same colour as the fan, which expresses the colour twice, a duplicate-attribute and real one.

theorem ChenVanDeemter2023.scene₁_under :

PurelyUnderSpecified scene₁ Obj.greenChair distractors₁ {(Attr.type, Value.chair)} ∧ Wrong scene₁ Obj.greenChair {(Attr.size, Value.large), (Attr.colour, Value.blue), (Attr.type, Value.chair)}

The chair is purely under-specified, and a description calling the green chair blue, as the paper's the large blue chair in the middle does, is wrong.

def ChenVanDeemter2023.scene₂ :

DaleReiter1995.KB Obj Attr Value

The second scene, a small green front-facing desk among a grey chair, a large and a small green chair, a large green front-facing desk, a small green side-facing desk and a grey desk.

Equations

Instances For

def ChenVanDeemter2023.distractors₂ :

Finset Obj

The distractors of the second scene.

Equations

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

Instances For

theorem ChenVanDeemter2023.scene₂_under :

Mixed scene₂ Obj.targetDesk distractors₂ {(Attr.colour, Value.green), (Attr.size, Value.small), (Attr.type, Value.desk)} ∧ PurelyUnderSpecified scene₂ Obj.targetDesk distractors₂ {(Attr.orientation, Value.front), (Attr.type, Value.desk)}

The green small desk is mixed, since every small object is green, and the front-facing desk is purely under-specified.