Dale and Reiter, computational interpretations of the Gricean maxims (1995)

A referring expression is a distinguishing description: a set of attribute-value pairs that all hold of the intended referent and that together rule out every member of the contrast set, which makes finding one a set-cover problem and finding a shortest one NP-hard. Dale and Reiter compare four computational readings of Grice's brevity submaxim, Full Brevity (a shortest description), Dale's Greedy Heuristic, Reiter's Local Brevity rules and their own Incremental Algorithm, which walks a fixed preference list of attributes and keeps any value that rules out a distractor not yet ruled out. They argue for the last on cost and on two psycholinguistic observations: speakers include unnecessary modifiers, which only the greedy and incremental algorithms produce, and speakers begin an expression before they have finished scanning the distractors, which only the incremental algorithm allows.

We define distinguishing descriptions and the four readings with a finite contrast set, prove that a shortest description satisfies Reiter's two rules while the greedy and incremental algorithms return unnecessary pairs on the paper's own examples, and prove that Fig. 6's output rules out every distractor, never retracts a pair and, under §4.5's accuracy user model, is a distinguishing description.

Implementation notes

• Reiter's third rule, Lexical Preference, is not modelled.
• Fig. 6's FindBestValue recurses until the taxonomy has no more specific value; the descent is bounded by the domain's depth, which must cover the taxonomies' height.
• Fig. 3 leaves ties between equally discriminating properties open; greedy takes the first in the order of P.

References

• R. Dale and E. Reiter, Computational Interpretations of the Gricean Maxims in the Generation of Referring Expressions (1995)
• H. P. Grice, Logic and Conversation (1975)

Distinguishing descriptions (§2.2)

@[reducible, inline]

abbrev DaleReiter1995.KB (E : Type u_4) (A : Type u_5) (V : Type u_6) : Type (max (max u_4 u_5) u_6)

The value an entity has for an attribute in the host's knowledge base, if it has one (§4.1).

Equations

• DaleReiter1995.KB E A V = (E → A → Option V)

@[reducible, inline]

abbrev DaleReiter1995.Description (A : Type u_4) (V : Type u_5) : Type (max u_5 u_4)

The semantic content of a referring expression, a set of attribute-value pairs (§2.2).

Equations

• DaleReiter1995.Description A V = Finset (A × V)

def DaleReiter1995.Applies {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : KB E A V) (x : E) (p : A × V) : Prop

The pair holds of the entity.

Equations

• DaleReiter1995.Applies kb x p = (kb x p.1 = some p.2)

@[instance_reducible]

instance DaleReiter1995.instDecidableAppliesOfDecidableEq {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq V] (kb : KB E A V) (x : E) (p : A × V) : Decidable (Applies kb x p)

Equations

• DaleReiter1995.instDecidableAppliesOfDecidableEq kb x p = id inferInstance

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

Every pair of a description holds of the entity.

Equations

• DaleReiter1995.extension kb L x = ∀ p ∈ L, DaleReiter1995.Applies kb x p

@[instance_reducible]

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

Equations

• DaleReiter1995.instDecidableExtensionOfDecidableEq kb L x = id inferInstance

def DaleReiter1995.Distinguishing {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : KB E A V) (r : E) (C : Finset E) (L : Description A V) : Prop

A distinguishing description of r against the contrast set C holds of r and distinguishes it from C, so that every pair holds of r and every distractor fails some pair.

Equations

• DaleReiter1995.Distinguishing kb r C L = (DaleReiter1995.extension kb L r ∧ Reference.Distinguishes (DaleReiter1995.extension kb) C r L)

@[instance_reducible]

instance DaleReiter1995.instDecidableDistinguishingOfDecidableEq {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq V] (kb : KB E A V) (r : E) (C : Finset E) (L : Description A V) : Decidable (Distinguishing kb r C L)

Equations

• DaleReiter1995.instDecidableDistinguishingOfDecidableEq kb r C L = id inferInstance

theorem DaleReiter1995.distinguishing_iff {E : Type u_1} {A : Type u_2} {V : Type u_3} {kb : KB E A V} {r : E} {C : Finset E} {L : Description A V} : Distinguishing kb r C L ↔ (∀ p ∈ L, Applies kb r p) ∧ ∀ c ∈ C, ∃ p ∈ L, ¬Applies kb c p

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

The members of the contrast set a pair rules out (§2.2).

Equations

• DaleReiter1995.rulesOut kb C p = {x ∈ C | ¬DaleReiter1995.Applies kb x p}

theorem DaleReiter1995.distinguishing_iff_biUnion {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq E] [DecidableEq V] (kb : KB E A V) (r : E) (C : Finset E) (L : Description A V) : Distinguishing kb r C L ↔ (∀ p ∈ L, Applies kb r p) ∧ C ⊆ Finset.biUnion L (rulesOut kb C)

A description distinguishes when its pairs' rulesOut sets cover the contrast set, the set-cover problem of §2.2.

Four interpretations of brevity (§3.1)

@[reducible, inline]

abbrev DaleReiter1995.IsShortest {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : KB E A V) (r : E) (C : Finset E) (L : Description A V) : Prop

A distinguishing description of least cardinality, the Full Brevity reading (§3.1.1).

Equations

• DaleReiter1995.IsShortest kb r C L = MinimalFor (DaleReiter1995.Distinguishing kb r C) Finset.card L

theorem DaleReiter1995.isShortest_of_card_two {E : Type u_1} {A : Type u_2} {V : Type u_3} {kb : KB E A V} {r : E} {C : Finset E} {L : Description A V} (hL : Distinguishing kb r C L) (h2 : Finset.card L = 2) (h0 : ¬Distinguishing kb r C ∅) (h1 : ∀ (p : A × V), ¬Distinguishing kb r C {p}) : IsShortest kb r C L

A distinguishing description with two pairs is shortest once neither the empty description nor any single pair distinguishes.

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

A distinguishing description none of whose pairs can be dropped, Reiter's No Unnecessary Components rule (§3.1.3).

Equations

• DaleReiter1995.NoUnnecessary kb r C L = (DaleReiter1995.Distinguishing kb r C L ∧ ∀ p ∈ L, ¬DaleReiter1995.Distinguishing kb r C (Finset.erase L p))

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

A description with no unnecessary pair in which no set of pairs can be replaced by a single new pair, Reiter's Local Brevity rule (§3.1.3).

Equations

• DaleReiter1995.LocallyBrief kb r C L = (DaleReiter1995.NoUnnecessary kb r C L ∧ ∀ S ⊆ L, 2 ≤ Finset.card S → ∀ (p : A × V), ¬DaleReiter1995.Distinguishing kb r C (insert p (L \ S)))

@[instance_reducible]

instance DaleReiter1995.instDecidableNoUnnecessary {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : KB E A V) (r : E) (C : Finset E) (L : Description A V) [DecidableEq A] [DecidableEq V] : Decidable (NoUnnecessary kb r C L)

Equations

• DaleReiter1995.instDecidableNoUnnecessary kb r C L = id inferInstance

theorem DaleReiter1995.noUnnecessary_iff_minimal {E : Type u_1} {A : Type u_2} {V : Type u_3} {kb : KB E A V} {r : E} {C : Finset E} {L : Description A V} [DecidableEq A] [DecidableEq V] : NoUnnecessary kb r C L ↔ Minimal (Distinguishing kb r C) L

Reiter's first rule is subset-minimality among distinguishing descriptions.

theorem DaleReiter1995.IsShortest.noUnnecessary {E : Type u_1} {A : Type u_2} {V : Type u_3} {kb : KB E A V} {r : E} {C : Finset E} {L : Description A V} [DecidableEq A] [DecidableEq V] (h : IsShortest kb r C L) : NoUnnecessary kb r C L

A shortest description has no unnecessary pair, so Full Brevity never includes an unnecessary modifier (§3.2.1).

theorem DaleReiter1995.IsShortest.locallyBrief {E : Type u_1} {A : Type u_2} {V : Type u_3} {kb : KB E A V} {r : E} {C : Finset E} {L : Description A V} [DecidableEq A] [DecidableEq V] (h : IsShortest kb r C L) : LocallyBrief kb r C L

A shortest description is locally brief.

def DaleReiter1995.fullBrevitySteps (na nl : ℕ) : ℕ

Descriptions the exhaustive Full Brevity search checks, with na available attributes and a shortest description of nl pairs (§3.1.1).

Equations

• DaleReiter1995.fullBrevitySteps na nl = ∑ i ∈ Finset.Icc 1 nl, na.choose i

theorem DaleReiter1995.fullBrevitySteps_values : fullBrevitySteps 3 2 = 6 ∧ fullBrevitySteps 10 3 = 175 ∧ 6000 < fullBrevitySteps 20 4 ∧ 2000000 < fullBrevitySteps 50 5

The paper's four counts, six for §2.2's example, 175, over 6,000 and over 2,000,000.

def DaleReiter1995.greedyAux {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : KB E A V) [DecidableEq A] [DecidableEq V] : ℕ → Finset E → List (A × V) → Description A V → Option (Description A V)

Equations

• One or more equations did not get rendered due to their size.
• DaleReiter1995.greedyAux kb 0 x✝² x✝¹ x✝ = if x✝².Nonempty then none else some x✝

def DaleReiter1995.greedy {E : Type u_1} {A : Type u_2} {V : Type u_3} (kb : KB E A V) (C : Finset E) [DecidableEq A] [DecidableEq V] (P : List (A × V)) : Option (Description A V)

Fig. 3's Greedy Heuristic, which from the properties P true of the referent adds the one leaving the fewest distractors, the first in P on a tie, until none remain, and fails when P runs out.

Equations

• DaleReiter1995.greedy kb C P = DaleReiter1995.greedyAux kb P.length C P ∅

The Incremental Algorithm (§4, Fig. 6)

inductive DaleReiter1995.Knowledge : Type

The three values of Fig. 6's UserKnows (§4.1): the user knows the pair holds of the entity, knows it does not, or neither.

• holds : Knowledge
• fails : Knowledge
• unknown : Knowledge

@[instance_reducible]

instance DaleReiter1995.instDecidableEqKnowledge : DecidableEq Knowledge

Equations

• DaleReiter1995.instDecidableEqKnowledge x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DaleReiter1995.instReprKnowledge.repr : Knowledge → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DaleReiter1995.instReprKnowledge : Repr Knowledge

Equations

• DaleReiter1995.instReprKnowledge = { reprPrec := DaleReiter1995.instReprKnowledge.repr }

structure DaleReiter1995.Domain (E : Type u_4) (A : Type u_5) (V : Type u_6) : Type (max (max u_4 u_5) u_6)

The head-noun attribute, basic-level values, value taxonomies and user model the host system supplies (§4.1).

• type : A

  The attribute realized as the head noun (§2.2).

• depth : ℕ

  The depth of the value taxonomies, bounding findBestValue's descent.

• basicLevel : E → A → Option V

  The basic-level value of an attribute for an entity (BasicLevelValue).

• moreSpecific : E → A → V → Option V

  The child of a value in the attribute's taxonomy that still subsumes the entity's own value (MoreSpecificValue).

• userKnows : E → A → V → Knowledge

  What the user knows of the pair holding of the entity (UserKnows).

def DaleReiter1995.Domain.flat {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq V] (kb : KB E A V) (type : A) : Domain E A V

A domain without value taxonomies whose user knows a pair to hold exactly when it is accurate, the user model of §4.5.

Equations

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

theorem DaleReiter1995.Domain.flat_userKnows {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq V] {kb : KB E A V} {t : A} (x : E) (a : A) (v : V) : ((flat kb t).userKnows x a v = Knowledge.holds ↔ kb x a = some v) ∧ ((flat kb t).userKnows x a v = Knowledge.fails ↔ ∃ (w : V), kb x a = some w ∧ w ≠ v)

Under the accuracy user model, what the user knows is what the knowledge base records.

def DaleReiter1995.Domain.rulesOut {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) (C : Finset E) (a : A) (v : V) : Finset E

The remaining distractors the user knows not to bear the pair (Fig. 6, RulesOut).

Equations

• d.rulesOut C a v = {x ∈ C | d.userKnows x a v = DaleReiter1995.Knowledge.fails}

def DaleReiter1995.Domain.findBestValue {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) (r : E) (C : Finset E) (a : A) : ℕ → V → Option V

Fig. 6's FindBestValue, the initial value when the user knows it to hold of r, refined to a more specific value only when that rules out more distractors.

Equations

• One or more equations did not get rendered due to their size.
• d.findBestValue r C a 0 x✝ = if d.userKnows r a x✝ = DaleReiter1995.Knowledge.holds then some x✝ else none

theorem DaleReiter1995.Domain.findBestValue_userKnows {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) (r : E) (C : Finset E) (a : A) (n : ℕ) (v w : V) : d.findBestValue r C a n v = some w → d.userKnows r a w = Knowledge.holds

FindBestValue returns only values the user knows to hold of the referent.

def DaleReiter1995.Domain.withType {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] (r : E) (L : Description A V) : Description A V

Fig. 6's return, which always includes a head noun, the basic-level type added without a UserKnows check.

Equations

• d.withType r L = if ∃ p ∈ L, p.1 = d.type then L else match d.basicLevel r d.type with | none => L | some b => insert (d.type, b) L

theorem DaleReiter1995.Domain.withType_subset {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] (r : E) (L : Description A V) : L ⊆ d.withType r L

The return never retracts a pair.

theorem DaleReiter1995.Domain.withType_mem {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] (r : E) (L : Description A V) {p : A × V} (hp : p ∈ d.withType r L) : p ∈ L ∨ d.basicLevel r p.1 = some p.2

The return adds at most the basic-level head noun.

def DaleReiter1995.Domain.step {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] [DecidableEq E] (r : E) (a : A) (C : Finset E) (L : Description A V) : Finset E × Description A V

One attribute of Fig. 6's loop, whose best value is kept when it rules out a remaining distractor, those distractors being removed.

Equations

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

theorem DaleReiter1995.Domain.step_subset {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] [DecidableEq E] (r : E) (a : A) (C : Finset E) (L : Description A V) : L ⊆ (d.step r a C L).2

A step never retracts a pair (§4.3).

theorem DaleReiter1995.Domain.step_mem {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] [DecidableEq E] (r : E) (a : A) (C : Finset E) (L : Description A V) {p : A × V} (hp : p ∈ (d.step r a C L).2) : p ∈ L ∨ d.userKnows r p.1 p.2 = Knowledge.holds

A step adds only pairs the user knows to hold of the referent.

theorem DaleReiter1995.Domain.step_ruledOut {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] [DecidableEq E] (r : E) (a : A) (C : Finset E) (L : Description A V) {c : E} (hc : c ∈ C) (hc' : c ∉ (d.step r a C L).1) : ∃ p ∈ (d.step r a C L).2, d.userKnows c p.1 p.2 = Knowledge.fails

Every distractor a step removes is ruled out by the pair the step adds.

def DaleReiter1995.Domain.loop {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] [DecidableEq E] (r : E) : Finset E → List A → Description A V → Option (Description A V)

Fig. 6's loop over the preferred attributes.

Equations

• d.loop r x✝¹ [] x✝ = none
• d.loop r x✝¹ (a :: rest) x✝ = if (d.step r a x✝¹ x✝).1.Nonempty then d.loop r (d.step r a x✝¹ x✝).1 rest (d.step r a x✝¹ x✝).2 else some (d.withType r (d.step r a x✝¹ x✝).2)

def DaleReiter1995.Domain.makeReferringExpression {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] [DecidableEq E] (r : E) (C : Finset E) (P : List A) : Option (Description A V)

Fig. 6's MakeReferringExpression, the Incremental Algorithm over the preferred attributes P, failing when they run out before the contrast set does.

Equations

• d.makeReferringExpression r C P = d.loop r C P ∅

theorem DaleReiter1995.Domain.loop_spec {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] [DecidableEq E] (r : E) (P : List A) (C : Finset E) (L L' : Description A V) : d.loop r C P L = some L' → ∃ (L₀ : Description A V), L' = d.withType r L₀ ∧ L ⊆ L₀ ∧ (∀ c ∈ C, ∃ p ∈ L₀, d.userKnows c p.1 p.2 = Knowledge.fails) ∧ ∀ p ∈ L₀, p ∈ L ∨ d.userKnows r p.1 p.2 = Knowledge.holds

The loop returns through withType a description that never retracts a pair, rules out every remaining distractor and adds only pairs known to hold (§3.2.1's indelible generation, §4.3).

theorem DaleReiter1995.Domain.makeReferringExpression_rulesOut {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] [DecidableEq E] {r : E} {C : Finset E} {P : List A} {L : Description A V} (h : d.makeReferringExpression r C P = some L) (c : E) : c ∈ C → ∃ p ∈ L, d.userKnows c p.1 p.2 = Knowledge.fails

Fig. 6's output rules out every member of the contrast set (§4.3).

theorem DaleReiter1995.Domain.makeReferringExpression_mem {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] [DecidableEq E] {r : E} {C : Finset E} {P : List A} {L : Description A V} (h : d.makeReferringExpression r C P = some L) (p : A × V) : p ∈ L → d.userKnows r p.1 p.2 = Knowledge.holds ∨ d.basicLevel r p.1 = some p.2

Every pair of Fig. 6's output is known to the user to hold of the referent, except the head noun added at the end, which is the basic-level type (§4.3).

theorem DaleReiter1995.Domain.makeReferringExpression_type {E : Type u_1} {A : Type u_2} {V : Type u_3} (d : Domain E A V) [DecidableEq A] [DecidableEq V] [DecidableEq E] {r : E} {C : Finset E} {P : List A} {L : Description A V} (h : d.makeReferringExpression r C P = some L) (hb : (d.basicLevel r d.type).isSome = true) : ∃ (v : V), (d.type, v) ∈ L

Fig. 6's output carries a head noun whenever the referent has a basic-level type (§4.3).

theorem DaleReiter1995.Domain.flat_distinguishing {E : Type u_1} {A : Type u_2} {V : Type u_3} [DecidableEq A] [DecidableEq V] [DecidableEq E] {kb : KB E A V} {t : A} {r : E} {C : Finset E} {P : List A} {L : Description A V} (h : (flat kb t).makeReferringExpression r C P = some L) : Distinguishing kb r C L

Under the accuracy user model the output is a distinguishing description (§2.2).

The paper's examples

inductive DaleReiter1995.Attr : Type

The head noun and the perceptual properties, the attributes of the paper's examples.

• type : Attr
• property (d : Degree.PropertyDomain) : Attr

def DaleReiter1995.instDecidableEqAttr.decEq (x✝ x✝¹ : Attr) : Decidable (x✝ = x✝¹)

Equations

• DaleReiter1995.instDecidableEqAttr.decEq DaleReiter1995.Attr.type DaleReiter1995.Attr.type = isTrue ⋯
• DaleReiter1995.instDecidableEqAttr.decEq DaleReiter1995.Attr.type (DaleReiter1995.Attr.property d) = isFalse ⋯
• DaleReiter1995.instDecidableEqAttr.decEq (DaleReiter1995.Attr.property d) DaleReiter1995.Attr.type = isFalse ⋯
• DaleReiter1995.instDecidableEqAttr.decEq (DaleReiter1995.Attr.property a) (DaleReiter1995.Attr.property b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DaleReiter1995.instDecidableEqAttr : DecidableEq Attr

Equations

• DaleReiter1995.instDecidableEqAttr = DaleReiter1995.instDecidableEqAttr.decEq

def DaleReiter1995.instReprAttr.repr : Attr → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• DaleReiter1995.instReprAttr.repr DaleReiter1995.Attr.type prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Attr.type")).group prec✝

@[instance_reducible]

instance DaleReiter1995.instReprAttr : Repr Attr

Equations

• DaleReiter1995.instReprAttr = { reprPrec := DaleReiter1995.instReprAttr.repr }

@[instance_reducible]

instance DaleReiter1995.instFintypeAttr : Fintype Attr

Equations

• DaleReiter1995.instFintypeAttr = Fintype.ofEquiv (Unit ⊕ Degree.PropertyDomain) DaleReiter1995.Attr.proxyTypeEquiv

inductive DaleReiter1995.Value : Type

The values of the paper's examples.

• dog : Value
• cat : Value
• chihuahua : Value
• siameseCat : Value
• bird : Value
• cup : Value
• small : Value
• medium : Value
• large : Value
• black : Value
• white : Value
• red : Value
• green : Value
• blue : Value
• plastic : Value
• paper : Value

@[instance_reducible]

instance DaleReiter1995.instDecidableEqValue : DecidableEq Value

Equations

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

def DaleReiter1995.instReprValue.repr : Value → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• DaleReiter1995.instReprValue.repr DaleReiter1995.Value.dog prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Value.dog")).group prec✝
• DaleReiter1995.instReprValue.repr DaleReiter1995.Value.cat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Value.cat")).group prec✝
• DaleReiter1995.instReprValue.repr DaleReiter1995.Value.bird prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Value.bird")).group prec✝
• DaleReiter1995.instReprValue.repr DaleReiter1995.Value.cup prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Value.cup")).group prec✝
• DaleReiter1995.instReprValue.repr DaleReiter1995.Value.red prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Value.red")).group prec✝
• DaleReiter1995.instReprValue.repr DaleReiter1995.Value.blue prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Value.blue")).group prec✝

@[instance_reducible]

instance DaleReiter1995.instReprValue : Repr Value

Equations

• DaleReiter1995.instReprValue = { reprPrec := DaleReiter1995.instReprValue.repr }

@[instance_reducible]

instance DaleReiter1995.instFintypeValue : Fintype Value

Equations

• DaleReiter1995.instFintypeValue = { elems := { val := ↑DaleReiter1995.Value.enumList, nodup := DaleReiter1995.Value.enumList_nodup }, complete := DaleReiter1995.instFintypeValue._proof_1 }

The two dogs and the cat (§2.2, §4.4)

inductive DaleReiter1995.Animal : Type

The three animals of §2.2 and §4.4.

• object1 : Animal
• object2 : Animal
• object3 : Animal

@[instance_reducible]

instance DaleReiter1995.instDecidableEqAnimal : DecidableEq Animal

Equations

• DaleReiter1995.instDecidableEqAnimal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DaleReiter1995.instReprAnimal.repr : Animal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DaleReiter1995.instReprAnimal : Repr Animal

Equations

• DaleReiter1995.instReprAnimal = { reprPrec := DaleReiter1995.instReprAnimal.repr }

def DaleReiter1995.Animal.kb : KB Animal Attr Value

The most specific values the system knows (§4.4).

Equations

• DaleReiter1995.Animal.object1.kb DaleReiter1995.Attr.type = some DaleReiter1995.Value.chihuahua
• DaleReiter1995.Animal.object1.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.size) = some DaleReiter1995.Value.small
• DaleReiter1995.Animal.object1.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.black
• DaleReiter1995.Animal.object2.kb DaleReiter1995.Attr.type = some DaleReiter1995.Value.chihuahua
• DaleReiter1995.Animal.object2.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.size) = some DaleReiter1995.Value.large
• DaleReiter1995.Animal.object2.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.white
• DaleReiter1995.Animal.object3.kb DaleReiter1995.Attr.type = some DaleReiter1995.Value.siameseCat
• DaleReiter1995.Animal.object3.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.size) = some DaleReiter1995.Value.small
• DaleReiter1995.Animal.object3.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.black
• x✝¹.kb x✝ = none

def DaleReiter1995.Animal.basicLevel (x : Animal) : Attr → Option Value

The basic-level values of §2.2, dog, dog and cat.

Equations

• DaleReiter1995.Animal.object3.basicLevel DaleReiter1995.Attr.type = some DaleReiter1995.Value.cat
• x.basicLevel DaleReiter1995.Attr.type = some DaleReiter1995.Value.dog
• x.basicLevel x✝ = x.kb x✝

def DaleReiter1995.Animal.parent : Value → Option Value

The taxonomy of §4.4, the breeds below their basic-level types.

Equations

• DaleReiter1995.Animal.parent DaleReiter1995.Value.chihuahua = some DaleReiter1995.Value.dog
• DaleReiter1995.Animal.parent DaleReiter1995.Value.siameseCat = some DaleReiter1995.Value.cat
• DaleReiter1995.Animal.parent x✝ = none

def DaleReiter1995.Animal.domain : Domain Animal Attr Value

The domain of §4.4, in which the breeds are the only more specific values and the user knows a pair to hold exactly when it is accurate under the taxonomy.

Equations

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

def DaleReiter1995.Animal.contrast : Finset Animal

The contrast set.

Equations

• DaleReiter1995.Animal.contrast = {DaleReiter1995.Animal.object2, DaleReiter1995.Animal.object3}

theorem DaleReiter1995.Animal.black_dog_distinguishing : Distinguishing basicLevel object1 contrast {(Attr.type, Value.dog), (Attr.property Degree.PropertyDomain.color, Value.black)} ∧ Distinguishing basicLevel object1 contrast {(Attr.type, Value.dog), (Attr.property Degree.PropertyDomain.size, Value.small)}

The black dog and the small dog are distinguishing descriptions of Object1 (§2.2).

theorem DaleReiter1995.Animal.black_dog_isShortest : IsShortest basicLevel object1 contrast {(Attr.type, Value.dog), (Attr.property Degree.PropertyDomain.color, Value.black)}

No single pair distinguishes Object1, so the black dog is a shortest description (§3.1.1's six steps).

theorem DaleReiter1995.Animal.findBestValue_type : domain.findBestValue object1 contrast Attr.type 1 Value.dog = some Value.dog

The breed rules out no more distractors than the basic-level type, so FindBestValue keeps dog (§4.4).

theorem DaleReiter1995.Animal.makeReferringExpression_animal : domain.makeReferringExpression object1 contrast [Attr.type, Attr.property Degree.PropertyDomain.color, Attr.property Degree.PropertyDomain.size] = some {(Attr.type, Value.dog), (Attr.property Degree.PropertyDomain.color, Value.black)} ∧ domain.makeReferringExpression object1 contrast [Attr.type, Attr.property Degree.PropertyDomain.size, Attr.property Degree.PropertyDomain.color] = some {(Attr.type, Value.dog), (Attr.property Degree.PropertyDomain.size, Value.small)}

With the preference order type, colour, size the algorithm returns the black dog; with type, size, colour it returns the small dog (§4.4).

The seven cups (§3.1.2)

inductive DaleReiter1995.Cup : Type

The seven cups of §3.1.2.

• object1 : Cup
• object2 : Cup
• object3 : Cup
• object4 : Cup
• object5 : Cup
• object6 : Cup
• object7 : Cup

@[instance_reducible]

instance DaleReiter1995.instDecidableEqCup : DecidableEq Cup

Equations

• DaleReiter1995.instDecidableEqCup x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DaleReiter1995.instReprCup : Repr Cup

Equations

• DaleReiter1995.instReprCup = { reprPrec := DaleReiter1995.instReprCup.repr }

def DaleReiter1995.instReprCup.repr : Cup → ℕ → Std.Format

Equations

• DaleReiter1995.instReprCup.repr DaleReiter1995.Cup.object1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Cup.object1")).group prec✝
• DaleReiter1995.instReprCup.repr DaleReiter1995.Cup.object2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Cup.object2")).group prec✝
• DaleReiter1995.instReprCup.repr DaleReiter1995.Cup.object3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Cup.object3")).group prec✝
• DaleReiter1995.instReprCup.repr DaleReiter1995.Cup.object4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Cup.object4")).group prec✝
• DaleReiter1995.instReprCup.repr DaleReiter1995.Cup.object5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Cup.object5")).group prec✝
• DaleReiter1995.instReprCup.repr DaleReiter1995.Cup.object6 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Cup.object6")).group prec✝
• DaleReiter1995.instReprCup.repr DaleReiter1995.Cup.object7 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DaleReiter1995.Cup.object7")).group prec✝

def DaleReiter1995.Cup.kb : KB Cup Attr Value

Size, colour and material of each cup.

Equations

• DaleReiter1995.Cup.object1.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.size) = some DaleReiter1995.Value.large
• DaleReiter1995.Cup.object1.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.red
• DaleReiter1995.Cup.object1.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.material) = some DaleReiter1995.Value.plastic
• DaleReiter1995.Cup.object2.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.size) = some DaleReiter1995.Value.small
• DaleReiter1995.Cup.object2.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.red
• DaleReiter1995.Cup.object2.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.material) = some DaleReiter1995.Value.plastic
• DaleReiter1995.Cup.object3.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.size) = some DaleReiter1995.Value.small
• DaleReiter1995.Cup.object3.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.red
• DaleReiter1995.Cup.object3.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.material) = some DaleReiter1995.Value.paper
• DaleReiter1995.Cup.object4.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.size) = some DaleReiter1995.Value.medium
• DaleReiter1995.Cup.object4.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.red
• DaleReiter1995.Cup.object4.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.material) = some DaleReiter1995.Value.paper
• DaleReiter1995.Cup.object5.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.size) = some DaleReiter1995.Value.large
• DaleReiter1995.Cup.object5.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.green
• DaleReiter1995.Cup.object5.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.material) = some DaleReiter1995.Value.paper
• DaleReiter1995.Cup.object6.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.size) = some DaleReiter1995.Value.large
• DaleReiter1995.Cup.object6.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.blue
• DaleReiter1995.Cup.object6.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.material) = some DaleReiter1995.Value.paper
• DaleReiter1995.Cup.object7.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.size) = some DaleReiter1995.Value.large
• DaleReiter1995.Cup.object7.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.blue
• DaleReiter1995.Cup.object7.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.material) = some DaleReiter1995.Value.plastic
• x✝¹.kb x✝ = none

def DaleReiter1995.Cup.contrast : Finset Cup

The contrast set for Object1.

Equations

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

def DaleReiter1995.Cup.properties : List (Attr × Value)

Object1's properties in the paper's order.

Equations

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

theorem DaleReiter1995.Cup.greedy_cups : greedy kb contrast properties = some {(Attr.property Degree.PropertyDomain.material, Value.plastic), (Attr.property Degree.PropertyDomain.size, Value.large), (Attr.property Degree.PropertyDomain.color, Value.red)}

The greedy heuristic selects plastic first, then large and red, giving the large red plastic cup once the head noun is added (§3.1.2).

theorem DaleReiter1995.Cup.large_red_isShortest : IsShortest kb object1 contrast {(Attr.property Degree.PropertyDomain.size, Value.large), (Attr.property Degree.PropertyDomain.color, Value.red)}

The large red cup is the shortest description (§3.1.2).

theorem DaleReiter1995.Cup.greedy_not_noUnnecessary : Distinguishing kb object1 contrast {(Attr.property Degree.PropertyDomain.material, Value.plastic), (Attr.property Degree.PropertyDomain.size, Value.large), (Attr.property Degree.PropertyDomain.color, Value.red)} ∧ ¬NoUnnecessary kb object1 contrast {(Attr.property Degree.PropertyDomain.material, Value.plastic), (Attr.property Degree.PropertyDomain.size, Value.large), (Attr.property Degree.PropertyDomain.color, Value.red)}

The greedy result distinguishes Object1 but carries an unnecessary pair (§3.1.2, §3.2.1).

The white bird (§3.2.1)

inductive DaleReiter1995.Picture : Type

A picture of a white bird, a black cup and a white cup.

• bird : Picture
• blackCup : Picture
• whiteCup : Picture

@[instance_reducible]

instance DaleReiter1995.instDecidableEqPicture : DecidableEq Picture

Equations

• DaleReiter1995.instDecidableEqPicture x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DaleReiter1995.instReprPicture.repr : Picture → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DaleReiter1995.instReprPicture : Repr Picture

Equations

• DaleReiter1995.instReprPicture = { reprPrec := DaleReiter1995.instReprPicture.repr }

def DaleReiter1995.Picture.kb : KB Picture Attr Value

Type and colour of each object.

Equations

• DaleReiter1995.Picture.bird.kb DaleReiter1995.Attr.type = some DaleReiter1995.Value.bird
• DaleReiter1995.Picture.bird.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.white
• DaleReiter1995.Picture.blackCup.kb DaleReiter1995.Attr.type = some DaleReiter1995.Value.cup
• DaleReiter1995.Picture.blackCup.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.black
• DaleReiter1995.Picture.whiteCup.kb DaleReiter1995.Attr.type = some DaleReiter1995.Value.cup
• DaleReiter1995.Picture.whiteCup.kb (DaleReiter1995.Attr.property Degree.PropertyDomain.color) = some DaleReiter1995.Value.white
• x✝¹.kb x✝ = none

def DaleReiter1995.Picture.contrast : Finset Picture

The contrast set.

Equations

• DaleReiter1995.Picture.contrast = {DaleReiter1995.Picture.blackCup, DaleReiter1995.Picture.whiteCup}

theorem DaleReiter1995.Picture.makeReferringExpression_picture : (Domain.flat kb Attr.type).makeReferringExpression bird contrast [Attr.property Degree.PropertyDomain.color, Attr.type] = some {(Attr.property Degree.PropertyDomain.color, Value.white), (Attr.type, Value.bird)} ∧ (Domain.flat kb Attr.type).makeReferringExpression bird contrast [Attr.type, Attr.property Degree.PropertyDomain.color] = some {(Attr.type, Value.bird)}

The paper's speaker scans the black cup and says white, then scans the white cup and adds bird, which alone would have done (§3.2.1). The algorithm reproduces that output only with colour before type in the preference order; type first yields the bird.

theorem DaleReiter1995.Picture.white_bird_not_noUnnecessary : ¬NoUnnecessary kb bird contrast {(Attr.property Degree.PropertyDomain.color, Value.white), (Attr.type, Value.bird)} ∧ NoUnnecessary kb bird contrast {(Attr.type, Value.bird)}

The colour-first output contains an unnecessary modifier, the behaviour of Observation 1 that Full Brevity and Local Brevity never produce (§3.2.1).