Kao, Bergen and Goodman (2014): Formalizing the Pragmatics of Metaphor Understanding

Kao, Bergen and Goodman model metaphor on the RSA kernel pipeline. A meaning pairs a category, the animal named or a person, with a vector of three features. The literal listener conditions the prior on the category named, a speaker whose goal is to communicate one feature is informative about that feature's value (eqs. 1 and 2), and the pragmatic listener marginalizes the goal. John is a shark can then convey scariness to a listener who does not believe John a shark.

Main results

• KaoBergenEtAl2014.nonliteral: a person with some value of the goal's feature is a possible meaning of the animal's name whenever some animal of positive prior shares the value.
• KaoBergenEtAl2014.category_odds: a goal ignores the category, so the listener's posterior odds between the animal and the person at a feature vector are their prior odds.
• KaoBergenEtAl2014.speaker_odds, KaoBergenEtAl2014.names_animal_iff: the speaker names the animal rather than the person exactly when the feature's value is likelier under the animal.

Implementation notes

• Priors are arguments. The category prior and the feature priors of Experiment 1b enter as one probability measure on meanings, and the goal prior as a probability measure on goals, uniform under a vague question and weighted toward the asked feature under a specific one.
• The model's numerical fits rest on the elicited priors of thirty-two animals, which the paper does not print, and are not stated.

References

• [KBG14]

inductive KaoBergenEtAl2014.Cat : Type

A referent is either the animal named or a person.

• animal : Cat
• person : Cat

@[instance_reducible]

instance KaoBergenEtAl2014.instDecidableEqCat : DecidableEq Cat

Equations

• KaoBergenEtAl2014.instDecidableEqCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KaoBergenEtAl2014.instReprCat.repr : Cat → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KaoBergenEtAl2014.instReprCat : Repr Cat

Equations

• KaoBergenEtAl2014.instReprCat = { reprPrec := KaoBergenEtAl2014.instReprCat.repr }

@[instance_reducible]

instance KaoBergenEtAl2014.instFintypeCat : Fintype Cat

Equations

• KaoBergenEtAl2014.instFintypeCat = { elems := { val := ↑KaoBergenEtAl2014.Cat.enumList, nodup := KaoBergenEtAl2014.Cat.enumList_nodup }, complete := KaoBergenEtAl2014.instFintypeCat._proof_1 }

@[instance_reducible]

instance KaoBergenEtAl2014.instMeasurableSpaceCat : MeasurableSpace Cat

Equations

• KaoBergenEtAl2014.instMeasurableSpaceCat = ⊤

instance KaoBergenEtAl2014.instDiscreteMeasurableSpaceCat : DiscreteMeasurableSpace Cat

instance KaoBergenEtAl2014.instNonemptyCat : Nonempty Cat

@[reducible, inline]

abbrev KaoBergenEtAl2014.Features : Type

The three features of the paper's example, each present or absent.

Equations

• KaoBergenEtAl2014.Features = (Bool × Bool × Bool)

@[reducible, inline]

abbrev KaoBergenEtAl2014.Meaning : Type

A meaning pairs the category with the feature vector.

Equations

• KaoBergenEtAl2014.Meaning = (KaoBergenEtAl2014.Cat × KaoBergenEtAl2014.Features)

inductive KaoBergenEtAl2014.Goal : Type

A goal names the feature to communicate, g_i(f) = f_i.

• f₁ : Goal
• f₂ : Goal
• f₃ : Goal

@[instance_reducible]

instance KaoBergenEtAl2014.instDecidableEqGoal : DecidableEq Goal

Equations

• KaoBergenEtAl2014.instDecidableEqGoal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KaoBergenEtAl2014.instReprGoal.repr : Goal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KaoBergenEtAl2014.instReprGoal : Repr Goal

Equations

• KaoBergenEtAl2014.instReprGoal = { reprPrec := KaoBergenEtAl2014.instReprGoal.repr }

@[instance_reducible]

instance KaoBergenEtAl2014.instFintypeGoal : Fintype Goal

Equations

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

@[instance_reducible]

instance KaoBergenEtAl2014.instMeasurableSpaceGoal : MeasurableSpace Goal

Equations

• KaoBergenEtAl2014.instMeasurableSpaceGoal = ⊤

instance KaoBergenEtAl2014.instDiscreteMeasurableSpaceGoal : DiscreteMeasurableSpace Goal

instance KaoBergenEtAl2014.instNonemptyGoal : Nonempty Goal

def KaoBergenEtAl2014.Goal.feature : Goal → Features → Bool

The value of the goal's feature.

Equations

• KaoBergenEtAl2014.Goal.f₁.feature (a, fst, snd) = a
• KaoBergenEtAl2014.Goal.f₂.feature (fst, b, snd) = b
• KaoBergenEtAl2014.Goal.f₃.feature (fst, fst_1, c) = c

def KaoBergenEtAl2014.project (g : Goal) (m : Meaning) : Bool

The projection of a goal (eq. 1) reads the goal's feature and ignores the category.

Equations

• KaoBergenEtAl2014.project g m = g.feature m.2

def KaoBergenEtAl2014.sem (u : Cat) : Set Meaning

An utterance is true of the meanings whose category it names.

Equations

• KaoBergenEtAl2014.sem u = {m : KaoBergenEtAl2014.Meaning | m.1 = u}

noncomputable def KaoBergenEtAl2014.L0 (μ : MeasureTheory.Measure Meaning) : ProbabilityTheory.Kernel Cat Meaning

The literal listener conditions the prior on the category named.

Equations

• KaoBergenEtAl2014.L0 μ = RSA.listener μ (RSA.truthful KaoBergenEtAl2014.sem)

instance KaoBergenEtAl2014.instIsFiniteKernelCatMeaningL0 (μ : MeasureTheory.Measure Meaning) : ProbabilityTheory.IsFiniteKernel (L0 μ)

noncomputable def KaoBergenEtAl2014.S1 (μ : MeasureTheory.Measure Meaning) (α : ℝ) (p : Meaning × Goal) : MeasureTheory.Measure Cat

The goal-indexed speaker (eq. 2) knows the value of her goal's feature and is informative about the literal listener's belief about it (eq. 1), at rationality α and no utterance cost.

Equations

• KaoBergenEtAl2014.S1 μ α p = (RSA.speaker α 0 (⇑((KaoBergenEtAl2014.L0 μ).map (KaoBergenEtAl2014.project p.2))) MeasureTheory.Measure.dirac) (KaoBergenEtAl2014.project p.2 p.1)

instance KaoBergenEtAl2014.instIsFiniteMeasureCatS1 (μ : MeasureTheory.Measure Meaning) (α : ℝ) (p : Meaning × Goal) : MeasureTheory.IsFiniteMeasure (S1 μ α p)

noncomputable def KaoBergenEtAl2014.L1 (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure Goal) [MeasureTheory.IsProbabilityMeasure ν] (α : ℝ) : ProbabilityTheory.Kernel Cat (Meaning × Goal)

The pragmatic listener over meaning and goal inverts the speaker against the product of the meaning prior and the goal prior; its first marginal is the meaning listener.

Equations

• KaoBergenEtAl2014.L1 μ ν α = RSA.listener (μ.prod ν) (KaoBergenEtAl2014.S1 μ α)

theorem KaoBergenEtAl2014.speaker_odds (μ : MeasureTheory.Measure Meaning) (α : ℝ) (g : Goal) (m : Meaning) : (S1 μ α (m, g)) {Cat.animal} * (((L0 μ).map (project g)) Cat.person) {project g m} ^ α = (S1 μ α (m, g)) {Cat.person} * (((L0 μ).map (project g)) Cat.animal) {project g m} ^ α

The speaker's odds for naming the animal rather than the person are the α-th power of the odds of the goal's feature value under the animal against the person.

theorem KaoBergenEtAl2014.names_animal_iff (μ : MeasureTheory.Measure Meaning) (α : ℝ) (g : Goal) (m : Meaning) (hα : 0 < α) (h0 : ∃ (u : Cat), (((L0 μ).map (project g)) u) {project g m} ≠ 0) : (S1 μ α (m, g)).real {Cat.person} < (S1 μ α (m, g)).real {Cat.animal} ↔ (((L0 μ).map (project g)) Cat.person) {project g m} < (((L0 μ).map (project g)) Cat.animal) {project g m}

The speaker names the animal rather than the person exactly when the goal's feature value is likelier under the animal than under the person.

theorem KaoBergenEtAl2014.listener_ne_zero_iff (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure Goal) [MeasureTheory.IsProbabilityMeasure ν] (α : ℝ) (hα : 0 < α) (u : Cat) (m : Meaning) : ((L1 μ ν α) u).fst {m} ≠ 0 ↔ μ {m} ≠ 0 ∧ ∃ (g : Goal), ν {g} ≠ 0 ∧ ∃ (m' : Meaning), g.feature m'.2 = g.feature m.2 ∧ m'.1 = u ∧ μ {m'} ≠ 0

A meaning is a possible interpretation of an utterance exactly when it has positive prior and some goal of positive prior has a feature value it shares with a meaning of positive prior bearing the category named.

theorem KaoBergenEtAl2014.nonliteral (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure Goal) [MeasureTheory.IsProbabilityMeasure ν] (α : ℝ) (hα : 0 < α) {g : Goal} (hν : ν {g} ≠ 0) {f f' : Features} (hp : μ {(Cat.person, f)} ≠ 0) (ha : μ {(Cat.animal, f')} ≠ 0) (hf : g.feature f' = g.feature f) : ((L1 μ ν α) Cat.animal).fst {(Cat.person, f)} ≠ 0

A person with the goal's feature value is a possible, nonliteral meaning of the animal's name whenever some animal of positive prior shares the value.

theorem KaoBergenEtAl2014.category_odds (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure Goal) [MeasureTheory.IsProbabilityMeasure ν] (α : ℝ) (u c c' : Cat) (f : Features) : ((L1 μ ν α) u).fst {(c, f)} * μ {(c', f)} = ((L1 μ ν α) u).fst {(c', f)} * μ {(c, f)}

Category inference is prior-driven. Since a goal projects the category away, the speaker behaves alike at the animal and at the person with the same features, and the listener's posterior odds between the two categories at a feature vector are their prior odds.