Engelhardt et al. (2006): Do Speakers and Listeners Observe the Gricean Maxim of Quantity?

This file formalizes the reading of the maxim of Quantity for referring expressions in [EBF06]. A description of an object in a display under-describes when it does not identify the object and over-describes when its modifier is not needed to identify it, and the instructions of the paper's experiments are classified this way over its one-referent and two-referent displays. Identification is Reference.Distinguishes against every other object of the display.

Implementation notes

• A display is five objects, each a kind with the object it rests on, so that the towel is ambiguous between the towel under the apple and the empty one and the other towel excludes the former.
• Over-description is measured against the bare noun, the paper's one contrast. The production rates, ratings and fixation data are not formalized.
• The examples are Data.Examples.EngelhardtEtAl2006.

References

• [EBF06]
• [Gri75]

inductive EngelhardtEtAl2006.Kind : Type

The kinds of object in a display, the apple to be moved, the frog, and the two kinds of destination.

• apple : Kind
• frog : Kind
• towel : Kind
• box : Kind

@[instance_reducible]

instance EngelhardtEtAl2006.instDecidableEqKind : DecidableEq Kind

Equations

• EngelhardtEtAl2006.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance EngelhardtEtAl2006.instReprKind : Repr Kind

Equations

• EngelhardtEtAl2006.instReprKind = { reprPrec := EngelhardtEtAl2006.instReprKind.repr }

def EngelhardtEtAl2006.instReprKind.repr : Kind → ℕ → Std.Format

Equations

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

structure EngelhardtEtAl2006.Object : Type

An object of a display, with its kind and the object it rests on or in, if any.

• kind : Kind
• support : Option (Fin 5)

def EngelhardtEtAl2006.instDecidableEqObject.decEq (x✝ x✝¹ : Object) : Decidable (x✝ = x✝¹)

Equations

• EngelhardtEtAl2006.instDecidableEqObject.decEq { kind := a, support := a_1 } { kind := b, support := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance EngelhardtEtAl2006.instDecidableEqObject : DecidableEq Object

Equations

• EngelhardtEtAl2006.instDecidableEqObject = EngelhardtEtAl2006.instDecidableEqObject.decEq

def EngelhardtEtAl2006.instReprObject.repr : Object → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance EngelhardtEtAl2006.instReprObject : Repr Object

Equations

• EngelhardtEtAl2006.instReprObject = { reprPrec := EngelhardtEtAl2006.instReprObject.repr }

@[reducible, inline]

abbrev EngelhardtEtAl2006.Display : Type

A display of five objects, the target first and the object it rests on second.

Equations

• EngelhardtEtAl2006.Display = (Fin 5 → EngelhardtEtAl2006.Object)

def EngelhardtEtAl2006.oneReferent : Display

The one-referent display, an apple on a towel, a frog, an empty towel and an empty box.

Equations

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

def EngelhardtEtAl2006.twoReferent : Display

The two-referent display, an apple on a towel, a second apple by itself, an empty towel and an empty box.

Equations

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

Descriptions and the maxim

inductive EngelhardtEtAl2006.Description : Type

A referring expression of the instructions, a bare noun, a noun with a prepositional-phrase modifier naming what the referent rests on, or the other noun, which excludes the object the target rests on.

• bare (k : Kind) : Description
• on (k loc : Kind) : Description
• other (k : Kind) : Description

def EngelhardtEtAl2006.instDecidableEqDescription.decEq (x✝ x✝¹ : Description) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• EngelhardtEtAl2006.instDecidableEqDescription.decEq (EngelhardtEtAl2006.Description.bare a) (EngelhardtEtAl2006.Description.bare b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• EngelhardtEtAl2006.instDecidableEqDescription.decEq (EngelhardtEtAl2006.Description.bare k) (EngelhardtEtAl2006.Description.on k_1 loc) = isFalse ⋯
• EngelhardtEtAl2006.instDecidableEqDescription.decEq (EngelhardtEtAl2006.Description.bare k) (EngelhardtEtAl2006.Description.other k_1) = isFalse ⋯
• EngelhardtEtAl2006.instDecidableEqDescription.decEq (EngelhardtEtAl2006.Description.on k loc) (EngelhardtEtAl2006.Description.bare k_1) = isFalse ⋯
• EngelhardtEtAl2006.instDecidableEqDescription.decEq (EngelhardtEtAl2006.Description.on k loc) (EngelhardtEtAl2006.Description.other k_1) = isFalse ⋯
• EngelhardtEtAl2006.instDecidableEqDescription.decEq (EngelhardtEtAl2006.Description.other k) (EngelhardtEtAl2006.Description.bare k_1) = isFalse ⋯
• EngelhardtEtAl2006.instDecidableEqDescription.decEq (EngelhardtEtAl2006.Description.other k) (EngelhardtEtAl2006.Description.on k_1 loc) = isFalse ⋯
• EngelhardtEtAl2006.instDecidableEqDescription.decEq (EngelhardtEtAl2006.Description.other a) (EngelhardtEtAl2006.Description.other b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance EngelhardtEtAl2006.instDecidableEqDescription : DecidableEq Description

Equations

• EngelhardtEtAl2006.instDecidableEqDescription = EngelhardtEtAl2006.instDecidableEqDescription.decEq

@[instance_reducible]

instance EngelhardtEtAl2006.instReprDescription : Repr Description

Equations

• EngelhardtEtAl2006.instReprDescription = { reprPrec := EngelhardtEtAl2006.instReprDescription.repr }

def EngelhardtEtAl2006.instReprDescription.repr : Description → ℕ → Std.Format

Equations

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

def EngelhardtEtAl2006.Description.kind : Description → Kind

The noun of a description.

Equations

• (EngelhardtEtAl2006.Description.bare k).kind = k
• (EngelhardtEtAl2006.Description.on k loc).kind = k
• (EngelhardtEtAl2006.Description.other k).kind = k

def EngelhardtEtAl2006.Description.bareOf (d : Description) : Description

The bare noun a description is measured against.

Equations

• d.bareOf = EngelhardtEtAl2006.Description.bare d.kind

def EngelhardtEtAl2006.extension (D : Display) (t : Fin 5) : Description → Fin 5 → Prop

The description holds of an object of the display, other read relative to the target t.

Equations

• EngelhardtEtAl2006.extension D t (EngelhardtEtAl2006.Description.bare k) x✝ = ((D x✝).kind = k)
• EngelhardtEtAl2006.extension D t (EngelhardtEtAl2006.Description.on k loc) x✝ = ((D x✝).kind = k ∧ ∃ (j : Fin 5), (D x✝).support = some j ∧ (D j).kind = loc)
• EngelhardtEtAl2006.extension D t (EngelhardtEtAl2006.Description.other k) x✝ = ((D x✝).kind = k ∧ (D t).support ≠ some x✝)

@[instance_reducible]

instance EngelhardtEtAl2006.instDecidableExtension (D : Display) (t : Fin 5) (d : Description) (i : Fin 5) : Decidable (extension D t d i)

Equations

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

@[reducible, inline]

abbrev EngelhardtEtAl2006.Identifies (D : Display) (t r : Fin 5) (d : Description) : Prop

The description lets the addressee identify the intended referent r against every other object of the display.

Equations

• EngelhardtEtAl2006.Identifies D t r d = Reference.Distinguishes (EngelhardtEtAl2006.extension D t) (Finset.univ.erase r) r d

def EngelhardtEtAl2006.OverDescribes (D : Display) (t r : Fin 5) (d : Description) : Prop

The description identifies r with a modifier its bare noun does not need.

Equations

• EngelhardtEtAl2006.OverDescribes D t r d = (d ≠ d.bareOf ∧ EngelhardtEtAl2006.Identifies D t r d ∧ EngelhardtEtAl2006.Identifies D t r d.bareOf)

@[instance_reducible]

instance EngelhardtEtAl2006.instDecidableOverDescribes (D : Display) (t r : Fin 5) (d : Description) : Decidable (OverDescribes D t r d)

Equations

• EngelhardtEtAl2006.instDecidableOverDescribes D t r d = id inferInstance

theorem EngelhardtEtAl2006.oneReferent_target : Identifies oneReferent 0 0 (Description.bare Kind.apple) ∧ OverDescribes oneReferent 0 0 (Description.on Kind.apple Kind.towel)

With one apple, the apple identifies it and the apple on the towel over-describes it.

theorem EngelhardtEtAl2006.twoReferent_target : ¬Identifies twoReferent 0 0 (Description.bare Kind.apple) ∧ Identifies twoReferent 0 0 (Description.on Kind.apple Kind.towel) ∧ ¬OverDescribes twoReferent 0 0 (Description.on Kind.apple Kind.towel)

With two apples, the apple under-describes and the modifier is required.

theorem EngelhardtEtAl2006.destinations (D : Display) : D ∈ [oneReferent, twoReferent] → ¬Identifies D 0 3 (Description.bare Kind.towel) ∧ Identifies D 0 3 (Description.other Kind.towel) ∧ ¬OverDescribes D 0 3 (Description.other Kind.towel) ∧ Identifies D 0 4 (Description.bare Kind.box)

In either display the towel under-describes the empty towel, as the apple already rests on a towel, the other towel identifies it without over-describing, and the box is identified bare.

The instructions

structure EngelhardtEtAl2006.Instruction : Type

An instruction, Put the apple … in/on the …, with its target and destination descriptions.

• target : Description
• destination : Description

@[instance_reducible]

instance EngelhardtEtAl2006.instDecidableEqInstruction : DecidableEq Instruction

Equations

• EngelhardtEtAl2006.instDecidableEqInstruction = EngelhardtEtAl2006.instDecidableEqInstruction.decEq

def EngelhardtEtAl2006.instDecidableEqInstruction.decEq (x✝ x✝¹ : Instruction) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance EngelhardtEtAl2006.instReprInstruction : Repr Instruction

Equations

• EngelhardtEtAl2006.instReprInstruction = { reprPrec := EngelhardtEtAl2006.instReprInstruction.repr }

def EngelhardtEtAl2006.instReprInstruction.repr : Instruction → ℕ → Std.Format

Equations

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

def EngelhardtEtAl2006.targetTable : List (String × Description)

The target descriptions as named in the rows.

Equations

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

def EngelhardtEtAl2006.destinationTable : List (String × Description)

The destination descriptions as named in the rows.

Equations

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

def EngelhardtEtAl2006.Instruction.ofDatum (ex : Datum) : Option Instruction

An instruction from an example row.

Equations

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

theorem EngelhardtEtAl2006.ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (ex.feature? "target").isSome = true → (Instruction.ofDatum ex).isSome = true

def EngelhardtEtAl2006.instructions : List Instruction

The four instructions of the paper's table.

Equations

• EngelhardtEtAl2006.instructions = List.filterMap EngelhardtEtAl2006.Instruction.ofDatum EngelhardtEtAl2006.Examples.all

def EngelhardtEtAl2006.Instruction.Matching (ins : Instruction) : Prop

The destination matches the target's current location, a towel.

Equations

• ins.Matching = (ins.destination.kind = EngelhardtEtAl2006.Kind.towel)

def EngelhardtEtAl2006.Instruction.goal (ins : Instruction) : Fin 5

The intended destination in either display: the empty towel or the box.

Equations

• ins.goal = if ins.destination.kind = EngelhardtEtAl2006.Kind.towel then 3 else 4

theorem EngelhardtEtAl2006.instructions_destination (D : Display) : D ∈ [oneReferent, twoReferent] → ∀ ins ∈ instructions, (Identifies D 0 ins.goal ins.destination ↔ ins.destination ≠ Description.bare Kind.towel) ∧ ¬OverDescribes D 0 ins.goal ins.destination

Over either display, the destination of an instruction is identified exactly when it is not the bare towel, and is never over-described.

theorem EngelhardtEtAl2006.instructions_oneReferent (ins : Instruction) : ins ∈ instructions → Identifies oneReferent 0 0 ins.target ∧ (OverDescribes oneReferent 0 0 ins.target ↔ ins.target ≠ Description.bare Kind.apple)

Over the one-referent display every target is identified and the modified target is an over-description.

theorem EngelhardtEtAl2006.instructions_twoReferent (ins : Instruction) : ins ∈ instructions → (Identifies twoReferent 0 0 ins.target ↔ ins.target ≠ Description.bare Kind.apple) ∧ ¬OverDescribes twoReferent 0 0 ins.target

Over the two-referent display the bare target is an under-description and the modifier is required.