@[reducible, inline]

abbrev RSA.TesslerGoodman2022.Height : Type

Discretized height values (in inches, scaled). Heights range from "short" (0) to "tall" (10) in discrete steps. Now backed by the canonical Degree 10 type with LinearOrder and BoundedOrder.

Equations

• RSA.TesslerGoodman2022.Height = Core.Scale.Degree 10

inductive RSA.TesslerGoodman2022.ComparisonClass : Type

Comparison classes for scalar adjectives.

The key distinction in the paper:

• SUBORDINATE: Compare to the kind itself (e.g., basketball players)
• SUPERORDINATE: Compare to the broader category (e.g., people in general)

Example: "tall basketball player"

• Subordinate: tall compared to basketball players
• Superordinate: tall compared to people in general

The paper shows that listeners infer which comparison class is intended.

• subordinate : ComparisonClass
• superordinate : ComparisonClass

def RSA.TesslerGoodman2022.instReprComparisonClass.repr : ComparisonClass → ℕ → Std.Format

Equations

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

instance RSA.TesslerGoodman2022.instReprComparisonClass : Repr ComparisonClass

Equations

• RSA.TesslerGoodman2022.instReprComparisonClass = { reprPrec := RSA.TesslerGoodman2022.instReprComparisonClass.repr }

instance RSA.TesslerGoodman2022.instDecidableEqComparisonClass : DecidableEq ComparisonClass

Equations

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

instance RSA.TesslerGoodman2022.instBEqComparisonClass : BEq ComparisonClass

Equations

• RSA.TesslerGoodman2022.instBEqComparisonClass = { beq := RSA.TesslerGoodman2022.instBEqComparisonClass.beq }

def RSA.TesslerGoodman2022.instBEqComparisonClass.beq : ComparisonClass → ComparisonClass → Bool

Equations

• RSA.TesslerGoodman2022.instBEqComparisonClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.TesslerGoodman2022.instFintypeComparisonClass : Fintype ComparisonClass

Equations

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

inductive RSA.TesslerGoodman2022.Kind : Type

Kinds (nominals) that can be modified by adjectives.

Each kind has:

• An associated HEIGHT DISTRIBUTION (expectations)
• A default comparison class preference

The paper focuses on kinds with ATYPICAL expectations:

• Basketball players: expected to be TALL
• Jockeys: expected to be SHORT

These create asymmetries in comparison class inference.

• person : Kind
• basketballPlayer : Kind
• jockey : Kind

instance RSA.TesslerGoodman2022.instReprKind : Repr Kind

Equations

• RSA.TesslerGoodman2022.instReprKind = { reprPrec := RSA.TesslerGoodman2022.instReprKind.repr }

def RSA.TesslerGoodman2022.instReprKind.repr : Kind → ℕ → Std.Format

Equations

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

instance RSA.TesslerGoodman2022.instDecidableEqKind : DecidableEq Kind

Equations

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

instance RSA.TesslerGoodman2022.instBEqKind : BEq Kind

Equations

• RSA.TesslerGoodman2022.instBEqKind = { beq := RSA.TesslerGoodman2022.instBEqKind.beq }

def RSA.TesslerGoodman2022.instBEqKind.beq : Kind → Kind → Bool

Equations

• RSA.TesslerGoodman2022.instBEqKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.TesslerGoodman2022.instFintypeKind : Fintype Kind

Equations

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

inductive RSA.TesslerGoodman2022.Utterance : Type

Utterances about height

• tall : Utterance
• short : Utterance
• silent : Utterance

def RSA.TesslerGoodman2022.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

instance RSA.TesslerGoodman2022.instReprUtterance : Repr Utterance

Equations

• RSA.TesslerGoodman2022.instReprUtterance = { reprPrec := RSA.TesslerGoodman2022.instReprUtterance.repr }

instance RSA.TesslerGoodman2022.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

instance RSA.TesslerGoodman2022.instBEqUtterance : BEq Utterance

Equations

• RSA.TesslerGoodman2022.instBEqUtterance = { beq := RSA.TesslerGoodman2022.instBEqUtterance.beq }

def RSA.TesslerGoodman2022.instBEqUtterance.beq : Utterance → Utterance → Bool

Equations

• RSA.TesslerGoodman2022.instBEqUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.TesslerGoodman2022.instFintypeUtterance : Fintype Utterance

Equations

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

def RSA.TesslerGoodman2022.personHeightPrior (h : Height) : ℚ

Height prior for generic people (baseline). Normal distribution centered at h5.

Equations

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

def RSA.TesslerGoodman2022.basketballHeightPrior (h : Height) : ℚ

Height prior for basketball players. Shifted RIGHT - basketball players are taller on average. Peak at h7 instead of h5.

Equations

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

def RSA.TesslerGoodman2022.jockeyHeightPrior (h : Height) : ℚ

Height prior for jockeys. Shifted LEFT - jockeys are shorter on average. Peak at h3 instead of h5.

Equations

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

def RSA.TesslerGoodman2022.heightPriorGivenKind (k : Kind) : Height → ℚ

Height prior given kind: P(h | k)

Equations

• RSA.TesslerGoodman2022.heightPriorGivenKind RSA.TesslerGoodman2022.Kind.person = RSA.TesslerGoodman2022.personHeightPrior
• RSA.TesslerGoodman2022.heightPriorGivenKind RSA.TesslerGoodman2022.Kind.basketballPlayer = RSA.TesslerGoodman2022.basketballHeightPrior
• RSA.TesslerGoodman2022.heightPriorGivenKind RSA.TesslerGoodman2022.Kind.jockey = RSA.TesslerGoodman2022.jockeyHeightPrior

def RSA.TesslerGoodman2022.comparisonClassPrior (k : Kind) : ComparisonClass → ℚ

Comparison class prior given kind: P(c | k).

The paper assumes a BASELINE preference for SUBORDINATE comparison class (compare to the specific kind), with some probability of SUPERORDINATE (compare to people in general).

For "basketball player":

• Default: compare to basketball players (subordinate)
• Alternative: compare to people (superordinate)

Equations

• One or more equations did not get rendered due to their size.
• RSA.TesslerGoodman2022.comparisonClassPrior RSA.TesslerGoodman2022.Kind.person = fun (x : RSA.TesslerGoodman2022.ComparisonClass) => 1

def RSA.TesslerGoodman2022.tallThreshold (c : ComparisonClass) (k : Kind) : ℕ

The EFFECTIVE THRESHOLD for "tall" depends on the comparison class.

• Subordinate (basketball players): threshold is HIGHER (need to be tall even for a basketball player)
• Superordinate (people): threshold is at POPULATION MEAN

This is the key semantic insight: the comparison class shifts the threshold.

Equations

• RSA.TesslerGoodman2022.tallThreshold RSA.TesslerGoodman2022.ComparisonClass.superordinate k = 5
• RSA.TesslerGoodman2022.tallThreshold RSA.TesslerGoodman2022.ComparisonClass.subordinate RSA.TesslerGoodman2022.Kind.person = 5
• RSA.TesslerGoodman2022.tallThreshold RSA.TesslerGoodman2022.ComparisonClass.subordinate RSA.TesslerGoodman2022.Kind.basketballPlayer = 7
• RSA.TesslerGoodman2022.tallThreshold RSA.TesslerGoodman2022.ComparisonClass.subordinate RSA.TesslerGoodman2022.Kind.jockey = 3

def RSA.TesslerGoodman2022.shortThreshold (c : ComparisonClass) (k : Kind) : ℕ

The EFFECTIVE THRESHOLD for "short" depends on the comparison class.

Equations

• RSA.TesslerGoodman2022.shortThreshold c k = RSA.TesslerGoodman2022.tallThreshold c k

def RSA.TesslerGoodman2022.tallMeaning (c : ComparisonClass) (k : Kind) (h : Height) : Bool

Meaning of "tall" given comparison class and kind.

[[tall]](c, k)(h) = 1 iff height(h) > threshold(c, k)

Equations

• RSA.TesslerGoodman2022.tallMeaning c k h = decide (Core.Scale.Degree.toNat h > RSA.TesslerGoodman2022.tallThreshold c k)

def RSA.TesslerGoodman2022.shortMeaning (c : ComparisonClass) (k : Kind) (h : Height) : Bool

Meaning of "short" given comparison class and kind.

[[short]](c, k)(h) = 1 iff height(h) < threshold(c, k)

Equations

• RSA.TesslerGoodman2022.shortMeaning c k h = decide (Core.Scale.Degree.toNat h < RSA.TesslerGoodman2022.shortThreshold c k)

def RSA.TesslerGoodman2022.meaning (u : Utterance) (c : ComparisonClass) (k : Kind) (h : Height) : Bool

Full meaning function: utterance x comparison class x kind -> height -> Bool

Equations

• RSA.TesslerGoodman2022.meaning RSA.TesslerGoodman2022.Utterance.tall c k h = RSA.TesslerGoodman2022.tallMeaning c k h
• RSA.TesslerGoodman2022.meaning RSA.TesslerGoodman2022.Utterance.short c k h = RSA.TesslerGoodman2022.shortMeaning c k h
• RSA.TesslerGoodman2022.meaning RSA.TesslerGoodman2022.Utterance.silent c k h = true

def RSA.TesslerGoodman2022.allHeights : List Height

All heights

Equations

• RSA.TesslerGoodman2022.allHeights = Core.Scale.allDegrees 10

theorem RSA.TesslerGoodman2022.person_thresholds_equal : tallThreshold ComparisonClass.subordinate Kind.person = tallThreshold ComparisonClass.superordinate Kind.person

For generic "person", subordinate and superordinate thresholds are identical. This means the comparison class makes no difference for "person".

theorem RSA.TesslerGoodman2022.basketball_subordinate_higher : tallThreshold ComparisonClass.subordinate Kind.basketballPlayer > tallThreshold ComparisonClass.superordinate Kind.basketballPlayer

For basketball players, subordinate threshold is higher than superordinate. This is because basketball players are tall, so "tall for a basketball player" requires a higher degree than "tall for a person".

theorem RSA.TesslerGoodman2022.jockey_subordinate_lower : tallThreshold ComparisonClass.subordinate Kind.jockey < tallThreshold ComparisonClass.superordinate Kind.jockey

For jockeys, subordinate threshold is lower than superordinate. This is because jockeys are short, so "tall for a jockey" requires a lower degree than "tall for a person".

theorem RSA.TesslerGoodman2022.tall_superordinate_less_restrictive_basketball : tallThreshold ComparisonClass.superordinate Kind.basketballPlayer < tallThreshold ComparisonClass.subordinate Kind.basketballPlayer

"tall" with superordinate comparison is true for MORE heights than with subordinate comparison for basketball players. This makes "tall" MORE INFORMATIVE (less restrictive) with superordinate, driving the pragmatic inference.

theorem RSA.TesslerGoodman2022.short_subordinate_more_inclusive_basketball : shortThreshold ComparisonClass.subordinate Kind.basketballPlayer > shortThreshold ComparisonClass.superordinate Kind.basketballPlayer

"short" with subordinate comparison covers MORE heights for basketball players than with superordinate comparison. Heights below 7 (subordinate) vs heights below 5 (superordinate).

Why the Polarity x Expectations Interaction Works

The Informativity Argument

For "tall basketball player" with SUBORDINATE comparison (to basketball players):

1. Threshold is HIGH (theta = 7 for basketball players)
2. Most basketball players are already tall (peak at h7)
3. "Tall" is TRUE for few basketball players (heights > 7 are fewer)
4. So "tall" is barely informative - true of a narrow range

For "tall basketball player" with SUPERORDINATE comparison (to people):

1. Threshold is LOWER (theta = 5 for people)
2. Most basketball players exceed this (they're tall for people)
3. "Tall" is TRUE for most basketball players
4. Speaker prefers this -> Listener infers superordinate

The Opposite for "Short"

For "short basketball player" with SUBORDINATE comparison:

1. Threshold is HIGH (theta = 7)
2. "Short" means height < 7 (many basketball players qualify!)
3. "Short" is INFORMATIVE about the individual

For "short basketball player" with SUPERORDINATE comparison:

1. Threshold is LOWER (theta = 5)
2. "Short" means height < 5 (almost no basketball players!)
3. This is TRIVIALLY FALSE for most basketball players
4. Speaker wouldn't use this -> Listener infers subordinate

Relation to @cite{lassiter-goodman-2017}

What LG2017 Covers

• Threshold inference: P(theta | "tall")
• Context-sensitivity via different HEIGHT PRIORS
• Same semantics, different interpretations

What TG2022 Adds

• Comparison class inference: P(c | "tall", k)
• KIND-specific expectations
• Polarity x expectations interaction

The Key Extension

LG2017: Different comparison classes = different HEIGHT PRIORS

P_L1(h, theta | "tall", basketball) uses P(h | basketball)
P_L1(h, theta | "tall", jockey) uses P(h | jockey)

TG2022: Listener INFERS which comparison class speaker intended

P_L1(h, c | "tall", basketball) reasons about P(c | basketball)

The comparison class is no longer fixed by context - it's inferred! This allows for the polarity x expectations interaction.

Unified Model

A full model would combine both:

P_L1(h, theta, c | u, k) proportional to P_S1(u | h, theta, c) * P(h | k) * P(theta) * P(c | k)

For simplicity, we assume the threshold is implicitly determined by the comparison class (theta = tallThreshold c k), avoiding the extra variable.

Comparison Class as Nested Restriction

@cite{tessler-goodman-2022}'s comparison class hierarchy is structurally a NestedRestriction: subordinate (restricted) ⊆ superordinate (unrestricted). This connects comparison class inference to the same nesting pattern used by @cite{ritchie-schiller-2024}'s domain restriction possibilities (DDRPs).

The downstream applications differ — threshold derivation vs. quantifier domain filtering — but the nesting structure is identical: going up the scale from subordinate to superordinate gives a superset of the reference population.

instance RSA.TesslerGoodman2022.instLinearOrderComparisonClass : LinearOrder ComparisonClass

Equations

• RSA.TesslerGoodman2022.instLinearOrderComparisonClass = LinearOrder.lift' RSA.TesslerGoodman2022.ComparisonClass.toFin✝ RSA.TesslerGoodman2022.ComparisonClass.toFin_injective✝

instance RSA.TesslerGoodman2022.instOrderTopComparisonClass : OrderTop ComparisonClass

Equations

• RSA.TesslerGoodman2022.instOrderTopComparisonClass = { top := RSA.TesslerGoodman2022.ComparisonClass.superordinate, le_top := RSA.TesslerGoodman2022.instOrderTopComparisonClass._proof_1 }

def RSA.TesslerGoodman2022.isTypical (k : Kind) (h : Height) : Bool

A reference population: which heights are typical for a given kind. For each kind, isTypical k h returns whether height h is in the kind's typical range (nonzero prior weight).

Equations

• RSA.TesslerGoodman2022.isTypical k h = decide (RSA.TesslerGoodman2022.heightPriorGivenKind k h > 0)

def RSA.TesslerGoodman2022.compClassRestriction (k : Kind) : Core.NestedRestriction ComparisonClass Height

The comparison class hierarchy for a given kind induces a nested restriction on heights: subordinate filters to heights typical of the kind, while superordinate includes all heights.

This is a NestedRestriction ComparisonClass Height: going from subordinate to superordinate widens the reference population.

Equations

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

def RSA.TesslerGoodman2022.basketballRestriction : Core.NestedRestriction ComparisonClass Height

Basketball player comparison class restriction: subordinate filters to heights with nonzero basketball prior (heights 2–10).

Equations

• RSA.TesslerGoodman2022.basketballRestriction = RSA.TesslerGoodman2022.compClassRestriction RSA.TesslerGoodman2022.Kind.basketballPlayer

def RSA.TesslerGoodman2022.jockeyRestriction : Core.NestedRestriction ComparisonClass Height

Jockey comparison class restriction: subordinate filters to heights with nonzero jockey prior (heights 0–8).

Equations

• RSA.TesslerGoodman2022.jockeyRestriction = RSA.TesslerGoodman2022.compClassRestriction RSA.TesslerGoodman2022.Kind.jockey

def RSA.TesslerGoodman2022.personRestriction : Core.NestedRestriction ComparisonClass Height

Person comparison class restriction: subordinate = superordinate (all heights have nonzero prior), so restriction is vacuous.

Equations

• RSA.TesslerGoodman2022.personRestriction = RSA.TesslerGoodman2022.compClassRestriction RSA.TesslerGoodman2022.Kind.person

theorem RSA.TesslerGoodman2022.basketball_threshold_shift_consistent : tallThreshold ComparisonClass.subordinate Kind.basketballPlayer > tallThreshold ComparisonClass.superordinate Kind.basketballPlayer

For basketball players, the subordinate threshold is higher than the superordinate threshold. This is consistent with the nesting: subordinate restricts to basketball players (who are tall), so "tall" requires a higher bar to be informative within that restricted population.

theorem RSA.TesslerGoodman2022.jockey_threshold_shift_consistent : tallThreshold ComparisonClass.subordinate Kind.jockey < tallThreshold ComparisonClass.superordinate Kind.jockey

For jockeys, the subordinate threshold is lower than the superordinate threshold. Subordinate restricts to jockeys (who are short), so "tall" requires a lower bar within that restricted population.

theorem RSA.TesslerGoodman2022.compClass_nesting (k : Kind) (h : Height) : (compClassRestriction k).region ComparisonClass.subordinate h = true → (compClassRestriction k).region ComparisonClass.superordinate h = true

The nesting property holds: subordinate region ⊆ superordinate region. This is true for all kinds by construction.