RSA Analysis of Hurford's Constraint

@cite{hurford-1974} @cite{singh-2008} @cite{potts-levy-2015}

Models Hurford's constraint as a consequence of speaker rationality in RSA.

Hurford's constraint: "#A or B" is infelicitous when A ⊆ B or B ⊆ A.

In RSA, felicity = speaker rationality. A speaker wouldn't say "A or B" if:

1. One disjunct is redundant (B⊆A makes B add nothing)
2. A simpler utterance (just "A") conveys the same information

The rescue by exhaustification works because:

• exh(some) = "some but not all" ⊈ "all"
• Now the disjunction is informative: it covers mutually exclusive cases

Status

The ℚ-based RSA evaluation infrastructure (RSA.Eval, boolToRat, LURSA) has been removed. Type definitions and semantic characterizations of redundancy are preserved. RSA computations (L1, S1) need to be re-implemented using the new RSAConfig framework.

Model

• Worlds: {none, someNotAll, all}
• Utterances: "some", "all", "some or all", null
• Lexica: L_base (some = ≥1), L_refined (some = some-but-not-all)

inductive RSA.Hurford.HWorld : Type

World states for Hurford scenarios.

We use a coarse 3-world model:

• none: Nothing of interest happened
• someNotAll: Some but not all (the "middle" reading)
• all_: All (the strong reading)

• none : HWorld
• someNotAll : HWorld
• all_ : HWorld

instance RSA.Hurford.instDecidableEqHWorld : DecidableEq HWorld

Equations

• RSA.Hurford.instDecidableEqHWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.Hurford.instReprHWorld : Repr HWorld

Equations

• RSA.Hurford.instReprHWorld = { reprPrec := RSA.Hurford.instReprHWorld.repr }

def RSA.Hurford.instReprHWorld.repr : HWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• RSA.Hurford.instReprHWorld.repr RSA.Hurford.HWorld.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.Hurford.HWorld.none")).group prec✝
• RSA.Hurford.instReprHWorld.repr RSA.Hurford.HWorld.all_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.Hurford.HWorld.all_")).group prec✝

def RSA.Hurford.instBEqHWorld.beq : HWorld → HWorld → Bool

Equations

• RSA.Hurford.instBEqHWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.Hurford.instBEqHWorld : BEq HWorld

Equations

• RSA.Hurford.instBEqHWorld = { beq := RSA.Hurford.instBEqHWorld.beq }

def RSA.Hurford.instInhabitedHWorld.default : HWorld

Equations

• RSA.Hurford.instInhabitedHWorld.default = RSA.Hurford.HWorld.none

instance RSA.Hurford.instInhabitedHWorld : Inhabited HWorld

Equations

• RSA.Hurford.instInhabitedHWorld = { default := RSA.Hurford.instInhabitedHWorld.default }

inductive RSA.Hurford.HUtterance : Type

Utterances for Hurford disjunction scenarios.

Key utterances:

• some_: "Mary read some of the books"
• all_: "Mary read all of the books"
• someOrAll: "Mary read some or all of the books"
• null: Null/silence alternative

• some_ : HUtterance
• all_ : HUtterance
• someOrAll : HUtterance
• null : HUtterance

instance RSA.Hurford.instDecidableEqHUtterance : DecidableEq HUtterance

Equations

• RSA.Hurford.instDecidableEqHUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.Hurford.instReprHUtterance : Repr HUtterance

Equations

• RSA.Hurford.instReprHUtterance = { reprPrec := RSA.Hurford.instReprHUtterance.repr }

def RSA.Hurford.instReprHUtterance.repr : HUtterance → ℕ → Std.Format

Equations

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

instance RSA.Hurford.instBEqHUtterance : BEq HUtterance

Equations

• RSA.Hurford.instBEqHUtterance = { beq := RSA.Hurford.instBEqHUtterance.beq }

def RSA.Hurford.instBEqHUtterance.beq : HUtterance → HUtterance → Bool

Equations

• RSA.Hurford.instBEqHUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.Hurford.instInhabitedHUtterance : Inhabited HUtterance

Equations

• RSA.Hurford.instInhabitedHUtterance = { default := RSA.Hurford.instInhabitedHUtterance.default }

def RSA.Hurford.instInhabitedHUtterance.default : HUtterance

Equations

• RSA.Hurford.instInhabitedHUtterance.default = RSA.Hurford.HUtterance.some_

def RSA.Hurford.lexBaseMeaning : HUtterance → HWorld → Bool

Base lexicon: "some" = at-least-one (weak reading).

Under this lexicon:

• "some" is true in {someNotAll, all_}
• "all" is true only in {all_}
• "some or all" = "some" ∨ "all" = "some" (since all⊆some)

This makes "some or all" redundant -- a Hurford violation.

Equations

• RSA.Hurford.lexBaseMeaning RSA.Hurford.HUtterance.some_ RSA.Hurford.HWorld.none = false
• RSA.Hurford.lexBaseMeaning RSA.Hurford.HUtterance.some_ RSA.Hurford.HWorld.someNotAll = true
• RSA.Hurford.lexBaseMeaning RSA.Hurford.HUtterance.some_ RSA.Hurford.HWorld.all_ = true
• RSA.Hurford.lexBaseMeaning RSA.Hurford.HUtterance.all_ RSA.Hurford.HWorld.all_ = true
• RSA.Hurford.lexBaseMeaning RSA.Hurford.HUtterance.all_ x✝ = false
• RSA.Hurford.lexBaseMeaning RSA.Hurford.HUtterance.someOrAll RSA.Hurford.HWorld.none = false
• RSA.Hurford.lexBaseMeaning RSA.Hurford.HUtterance.someOrAll RSA.Hurford.HWorld.someNotAll = true
• RSA.Hurford.lexBaseMeaning RSA.Hurford.HUtterance.someOrAll RSA.Hurford.HWorld.all_ = true
• RSA.Hurford.lexBaseMeaning RSA.Hurford.HUtterance.null x✝ = true

def RSA.Hurford.lexRefinedMeaning : HUtterance → HWorld → Bool

Refined lexicon: "some" = some-but-not-all (exhaustified reading).

Under this lexicon:

• "some" is true only in {someNotAll}
• "all" is true only in {all_}
• "some or all" is now informative: covers {someNotAll, all_}

This rescues the Hurford violation -- the disjunction is no longer redundant.

Equations

• RSA.Hurford.lexRefinedMeaning RSA.Hurford.HUtterance.some_ RSA.Hurford.HWorld.none = false
• RSA.Hurford.lexRefinedMeaning RSA.Hurford.HUtterance.some_ RSA.Hurford.HWorld.someNotAll = true
• RSA.Hurford.lexRefinedMeaning RSA.Hurford.HUtterance.some_ RSA.Hurford.HWorld.all_ = false
• RSA.Hurford.lexRefinedMeaning RSA.Hurford.HUtterance.all_ RSA.Hurford.HWorld.all_ = true
• RSA.Hurford.lexRefinedMeaning RSA.Hurford.HUtterance.all_ x✝ = false
• RSA.Hurford.lexRefinedMeaning RSA.Hurford.HUtterance.someOrAll RSA.Hurford.HWorld.none = false
• RSA.Hurford.lexRefinedMeaning RSA.Hurford.HUtterance.someOrAll RSA.Hurford.HWorld.someNotAll = true
• RSA.Hurford.lexRefinedMeaning RSA.Hurford.HUtterance.someOrAll RSA.Hurford.HWorld.all_ = true
• RSA.Hurford.lexRefinedMeaning RSA.Hurford.HUtterance.null x✝ = true

def RSA.Hurford.someOrAllTrueWorlds_base : List HWorld

Worlds where "some or all" is true under base lexicon

Equations

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

def RSA.Hurford.someTrueWorlds_base : List HWorld

Worlds where "some" is true under base lexicon

Equations

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

theorem RSA.Hurford.base_redundancy : someOrAllTrueWorlds_base = someTrueWorlds_base

Under base lexicon, "some or all" and "some" have the same extension. This is the semantic redundancy that causes Hurford violations.

def RSA.Hurford.someOrAllTrueWorlds_refined : List HWorld

Worlds where "some or all" is true under refined lexicon

Equations

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

def RSA.Hurford.someTrueWorlds_refined : List HWorld

Worlds where "some" is true under refined lexicon

Equations

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

theorem RSA.Hurford.refined_disjunction_informative : someOrAllTrueWorlds_refined.length > someTrueWorlds_refined.length

Under refined lexicon, "some or all" covers more worlds than "some" alone. This is why the disjunction is informative and the Hurford violation is rescued.

theorem RSA.Hurford.hurford_model_captures_rescue : someOrAllTrueWorlds_refined.length > someTrueWorlds_refined.length ∧ someOrAllTrueWorlds_base = someTrueWorlds_base

Connection to empirical Hurford data.

The model predicts:

1. Hurford violations (e.g., "American or Californian") = low S1 probability because the disjunction is redundant under the natural reading

2. Rescued cases (e.g., "some or all") = higher S1 probability when the listener interprets with the refined lexicon (exh applied)

The prediction: felicitous iff the disjunction is informative under some lexicon.

inductive RSA.Hurford.HyponymWorld : Type

Worlds for hyponymy scenario

• neither : HyponymWorld
• americanOnly : HyponymWorld
• californian : HyponymWorld

instance RSA.Hurford.instDecidableEqHyponymWorld : DecidableEq HyponymWorld

Equations

• RSA.Hurford.instDecidableEqHyponymWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RSA.Hurford.instReprHyponymWorld.repr : HyponymWorld → ℕ → Std.Format

Equations

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

instance RSA.Hurford.instReprHyponymWorld : Repr HyponymWorld

Equations

• RSA.Hurford.instReprHyponymWorld = { reprPrec := RSA.Hurford.instReprHyponymWorld.repr }

def RSA.Hurford.instBEqHyponymWorld.beq : HyponymWorld → HyponymWorld → Bool

Equations

• RSA.Hurford.instBEqHyponymWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.Hurford.instBEqHyponymWorld : BEq HyponymWorld

Equations

• RSA.Hurford.instBEqHyponymWorld = { beq := RSA.Hurford.instBEqHyponymWorld.beq }

def RSA.Hurford.instInhabitedHyponymWorld.default : HyponymWorld

Equations

• RSA.Hurford.instInhabitedHyponymWorld.default = RSA.Hurford.HyponymWorld.neither

instance RSA.Hurford.instInhabitedHyponymWorld : Inhabited HyponymWorld

Equations

• RSA.Hurford.instInhabitedHyponymWorld = { default := RSA.Hurford.instInhabitedHyponymWorld.default }

inductive RSA.Hurford.HyponymUtterance : Type

Utterances for hyponymy scenario

• american : HyponymUtterance
• californian : HyponymUtterance
• americanOrCalifornian : HyponymUtterance
• null : HyponymUtterance

instance RSA.Hurford.instDecidableEqHyponymUtterance : DecidableEq HyponymUtterance

Equations

• RSA.Hurford.instDecidableEqHyponymUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.Hurford.instReprHyponymUtterance : Repr HyponymUtterance

Equations

• RSA.Hurford.instReprHyponymUtterance = { reprPrec := RSA.Hurford.instReprHyponymUtterance.repr }

def RSA.Hurford.instReprHyponymUtterance.repr : HyponymUtterance → ℕ → Std.Format

Equations

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

instance RSA.Hurford.instBEqHyponymUtterance : BEq HyponymUtterance

Equations

• RSA.Hurford.instBEqHyponymUtterance = { beq := RSA.Hurford.instBEqHyponymUtterance.beq }

def RSA.Hurford.instBEqHyponymUtterance.beq : HyponymUtterance → HyponymUtterance → Bool

Equations

• RSA.Hurford.instBEqHyponymUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def RSA.Hurford.instInhabitedHyponymUtterance.default : HyponymUtterance

Equations

• RSA.Hurford.instInhabitedHyponymUtterance.default = RSA.Hurford.HyponymUtterance.american

instance RSA.Hurford.instInhabitedHyponymUtterance : Inhabited HyponymUtterance

Equations

• RSA.Hurford.instInhabitedHyponymUtterance = { default := RSA.Hurford.instInhabitedHyponymUtterance.default }

def RSA.Hurford.lexHyponymMeaning : HyponymUtterance → HyponymWorld → Bool

Lexicon for hyponymy: Californian ⊆ American (no refinement possible).

Equations

• RSA.Hurford.lexHyponymMeaning RSA.Hurford.HyponymUtterance.american RSA.Hurford.HyponymWorld.neither = false
• RSA.Hurford.lexHyponymMeaning RSA.Hurford.HyponymUtterance.american RSA.Hurford.HyponymWorld.americanOnly = true
• RSA.Hurford.lexHyponymMeaning RSA.Hurford.HyponymUtterance.american RSA.Hurford.HyponymWorld.californian = true
• RSA.Hurford.lexHyponymMeaning RSA.Hurford.HyponymUtterance.californian RSA.Hurford.HyponymWorld.californian = true
• RSA.Hurford.lexHyponymMeaning RSA.Hurford.HyponymUtterance.californian x✝ = false
• RSA.Hurford.lexHyponymMeaning RSA.Hurford.HyponymUtterance.americanOrCalifornian RSA.Hurford.HyponymWorld.neither = false
• RSA.Hurford.lexHyponymMeaning RSA.Hurford.HyponymUtterance.americanOrCalifornian RSA.Hurford.HyponymWorld.americanOnly = true
• RSA.Hurford.lexHyponymMeaning RSA.Hurford.HyponymUtterance.americanOrCalifornian RSA.Hurford.HyponymWorld.californian = true
• RSA.Hurford.lexHyponymMeaning RSA.Hurford.HyponymUtterance.null x✝ = true

def RSA.Hurford.americanOrCalifornianTrueWorlds : List HyponymWorld

Worlds where "American or Californian" is true

Equations

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

def RSA.Hurford.americanTrueWorlds : List HyponymWorld

Worlds where "American" alone is true

Equations

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

theorem RSA.Hurford.hyponym_always_redundant : americanOrCalifornianTrueWorlds = americanTrueWorlds

For hyponymy, the disjunction is always redundant -- no rescue possible.