Erk & Herbelot 2024 — How to Marry a Star

@cite{erk-herbelot-2024}

Erk, K. & Herbelot, A. (2024). How to Marry a Star: Probabilistic Constraints for Meaning in Context. Journal of Semantics 40, 549–583.

Core Mechanism

A Situation Description System (SDS) pairs a DRS with a directed graphical model over latent concepts, semantic roles, and scenarios. Word meaning in context is modeled as a distribution over concepts, computed via Product of Experts:

P(concept | context) ∝ P_selectional(concept | role) × P_scenario(concept | frame)

Key Predictions

1. Agreement (both factors prefer same concept) → confident disambiguation
2. Conflict (factors prefer different concepts) → pun/zeugma/ambiguity
3. Dominance (one factor much stronger) → that factor determines reading

Structure of This File

• §1: Concept types for the paper's running examples
• §2: Selectional constraints only (§4 of paper)
• §3: Selectional + scenario constraints (§5 of paper)
• §4: Context variations on "marry a star"
• §5: Multi-word and chained disambiguation
• §6: Constraint strength interaction
• §7: Concept features projected into DRS (§6 of paper)
• §8: Fine-grained sense distinctions (§7 of paper)
• §9: Connection to copredication

inductive Phenomena.Polysemy.Studies.ErkHerbelot2024.BatConcept : Type

Concepts for "bat": animal vs sports equipment.

• animal : BatConcept
• equipment : BatConcept

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprBatConcept.repr : BatConcept → ℕ → Std.Format

Equations

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

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprBatConcept : Repr BatConcept

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprBatConcept = { reprPrec := Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprBatConcept.repr }

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqBatConcept.beq : BatConcept → BatConcept → Bool

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqBatConcept.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqBatConcept : BEq BatConcept

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqBatConcept = { beq := Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqBatConcept.beq }

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqBatConcept : DecidableEq BatConcept

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqBatConcept x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Phenomena.Polysemy.Studies.ErkHerbelot2024.StarConcept : Type

Concepts for "star": famous person vs celestial body.

• celebrity : StarConcept
• celestial : StarConcept

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprStarConcept : Repr StarConcept

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprStarConcept = { reprPrec := Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprStarConcept.repr }

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprStarConcept.repr : StarConcept → ℕ → Std.Format

Equations

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

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqStarConcept : BEq StarConcept

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqStarConcept = { beq := Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqStarConcept.beq }

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqStarConcept.beq : StarConcept → StarConcept → Bool

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqStarConcept.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqStarConcept : DecidableEq StarConcept

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqStarConcept x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Phenomena.Polysemy.Studies.ErkHerbelot2024.PortConcept : Type

Concepts for "port": harbor, wine, or computer port.

• harbor : PortConcept
• wine : PortConcept
• computer : PortConcept

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprPortConcept.repr : PortConcept → ℕ → Std.Format

Equations

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

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprPortConcept : Repr PortConcept

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprPortConcept = { reprPrec := Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprPortConcept.repr }

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqPortConcept.beq : PortConcept → PortConcept → Bool

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqPortConcept.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqPortConcept : BEq PortConcept

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqPortConcept = { beq := Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqPortConcept.beq }

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqPortConcept : DecidableEq PortConcept

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqPortConcept x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

"A bat was sleeping"

SLEEP provides a strong selectional preference for animate subjects. With no scenario constraint (neutral context), selectional dominates.

def Phenomena.Polysemy.Studies.ErkHerbelot2024.batSleeping : Semantics.Probabilistic.SDS.Core.DisambiguationScenario BatConcept

Equations

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

"A player was holding a bat"

HOLD has weak selectional preference (both concepts are holdable), but "player" activates a SPORTS scenario that favors equipment.

def Phenomena.Polysemy.Studies.ErkHerbelot2024.playerHoldingBat : Semantics.Probabilistic.SDS.Core.DisambiguationScenario BatConcept

Equations

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

"The astronomer married the star"

The paper's signature example. Selectional and scenario constraints pull in opposite directions, producing a tie that predicts the pun reading.

def Phenomena.Polysemy.Studies.ErkHerbelot2024.astronomerMarriedStar : Semantics.Probabilistic.SDS.Core.DisambiguationScenario StarConcept

Equations

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

def Phenomena.Polysemy.Studies.ErkHerbelot2024.neutralMarryStar : Semantics.Probabilistic.SDS.Core.DisambiguationScenario StarConcept

Neutral context: selectional dominates → CELEBRITY.

Equations

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

def Phenomena.Polysemy.Studies.ErkHerbelot2024.producerMarryStar : Semantics.Probabilistic.SDS.Core.DisambiguationScenario StarConcept

Hollywood context: both factors agree → CELEBRITY reinforced.

Equations

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

def Phenomena.Polysemy.Studies.ErkHerbelot2024.alienMarryStar : Semantics.Probabilistic.SDS.Core.DisambiguationScenario StarConcept

Sci-fi context: selectional weakened, scenario pulls to celestial.

Equations

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

Comparison of Contexts

Context	P(CELEBRITY)	Reading
Neutral	0.90	Selectional wins
Astronomer	0.50	Tie → pun
Producer	0.99	Agreement
Alien	0.39	Scenario wins

"The sailor liked the port"

Three-way ambiguity. LIKE is neutral; "sailor" activates NAUTICAL frame. HARBOR wins, WINE remains plausible (sailors drink!), COMPUTER unlikely.

def Phenomena.Polysemy.Studies.ErkHerbelot2024.sailorLikedPort : Semantics.Probabilistic.SDS.Core.DisambiguationScenario PortConcept

Equations

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

"The coach told the star to play"

Multiple context words ("coach" + "play") reinforce SPORTS frame. TELL selects animate recipient. Both factors agree → confident CELEBRITY.

def Phenomena.Polysemy.Studies.ErkHerbelot2024.coachToldStar : Semantics.Probabilistic.SDS.Core.DisambiguationScenario StarConcept

Equations

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

Varying Scenario Strength

"The child saw the bat" with parameterized scenario strength. SAW is perceptually neutral; the scenario from CHILD varies.

def Phenomena.Polysemy.Studies.ErkHerbelot2024.childSawBat (scenarioStrength : ℚ) : Semantics.Probabilistic.SDS.Core.DisambiguationScenario BatConcept

Equations

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

Feature Projection

@cite{mcrae-etal-2005}: concepts have features with associated probabilities. After disambiguation, features are projected as additional DRS conditions.

For "a bat was sleeping":

• Posterior: P(ANIMAL) = 0.95
• Feature can_fly: P(can_fly | ANIMAL) = 1.0, P(can_fly | EQUIPMENT) = 0.0
• Projected: P(can_fly | context) = 0.95 × 1.0 + 0.05 × 0.0 = 0.95

inductive Phenomena.Polysemy.Studies.ErkHerbelot2024.BatFeature : Type

• canFly : BatFeature
• isBlack : BatFeature
• hasWings : BatFeature
• isWooden : BatFeature
• isLong : BatFeature

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprBatFeature : Repr BatFeature

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprBatFeature = { reprPrec := Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprBatFeature.repr }

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprBatFeature.repr : BatFeature → ℕ → Std.Format

Equations

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

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqBatFeature.beq : BatFeature → BatFeature → Bool

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqBatFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqBatFeature : BEq BatFeature

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqBatFeature = { beq := Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqBatFeature.beq }

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqBatFeature : DecidableEq BatFeature

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqBatFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Polysemy.Studies.ErkHerbelot2024.batFeatures : Semantics.Probabilistic.SDS.Core.ConceptFeature BatConcept BatFeature

Equations

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

inductive Phenomena.Polysemy.Studies.ErkHerbelot2024.StarFeature : Type

After "the astronomer married the star" (tie), features are mixed.

• isHuman : StarFeature
• isCelestialBody : StarFeature
• emitsLight : StarFeature

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprStarFeature.repr : StarFeature → ℕ → Std.Format

Equations

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

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprStarFeature : Repr StarFeature

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprStarFeature = { reprPrec := Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprStarFeature.repr }

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqStarFeature.beq : StarFeature → StarFeature → Bool

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqStarFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqStarFeature : BEq StarFeature

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqStarFeature = { beq := Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqStarFeature.beq }

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqStarFeature : DecidableEq StarFeature

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqStarFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Polysemy.Studies.ErkHerbelot2024.starFeatures : Semantics.Probabilistic.SDS.Core.ConceptFeature StarConcept StarFeature

Equations

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

The "argument" Example (Table 3)

"She seems to revel in arguments and loses no opportunity to declare her political principles."

Three annotators rated 5 WordNet senses on a 1–5 scale. Annotators systematically disagree, reflecting genuine uncertainty about word meaning in context.

inductive Phenomena.Polysemy.Studies.ErkHerbelot2024.ArgumentSense : Type

WordNet senses of "argument" used in the paper.

• evidence : ArgumentSense
• quarrel : ArgumentSense
• proCon : ArgumentSense
• parameter : ArgumentSense
• logicalReasoning : ArgumentSense

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprArgumentSense.repr : ArgumentSense → ℕ → Std.Format

Equations

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

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprArgumentSense : Repr ArgumentSense

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprArgumentSense = { reprPrec := Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprArgumentSense.repr }

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqArgumentSense.beq : ArgumentSense → ArgumentSense → Bool

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqArgumentSense.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqArgumentSense : BEq ArgumentSense

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqArgumentSense = { beq := Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqArgumentSense.beq }

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqArgumentSense : DecidableEq ArgumentSense

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqArgumentSense x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Phenomena.Polysemy.Studies.ErkHerbelot2024.SenseRating : Type

Graded sense applicability rating from a single annotator.

• sense : ArgumentSense
• rating : ℕ

  Rating on 1–5 scale (5 = fits completely, 1 = does not fit at all)

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprSenseRating : Repr SenseRating

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprSenseRating = { reprPrec := Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprSenseRating.repr }

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprSenseRating.repr : SenseRating → ℕ → Std.Format

Equations

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

def Phenomena.Polysemy.Studies.ErkHerbelot2024.annotator1 : List SenseRating

Table 3: three annotators' ratings for "argument" in the sentence above.

Equations

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

def Phenomena.Polysemy.Studies.ErkHerbelot2024.annotator2 : List SenseRating

Equations

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

def Phenomena.Polysemy.Studies.ErkHerbelot2024.annotator3 : List SenseRating

Equations

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

theorem Phenomena.Polysemy.Studies.ErkHerbelot2024.parameter_rejected : Option.map (fun (x : SenseRating) => x.rating) (List.filter (fun (x : SenseRating) => x.sense == ArgumentSense.parameter) annotator1).head? = some 1 ∧ Option.map (fun (x : SenseRating) => x.rating) (List.filter (fun (x : SenseRating) => x.sense == ArgumentSense.parameter) annotator2).head? = some 1 ∧ Option.map (fun (x : SenseRating) => x.rating) (List.filter (fun (x : SenseRating) => x.sense == ArgumentSense.parameter) annotator3).head? = some 1

All annotators agree that parameter does not apply.

theorem Phenomena.Polysemy.Studies.ErkHerbelot2024.quarrel_rated_high : Option.map (fun (x : SenseRating) => x.rating) (List.filter (fun (x : SenseRating) => x.sense == ArgumentSense.quarrel) annotator1).head? = some 5

At least one annotator gives quarrel the top rating.

SDS and Copredication

Copredication (from Phenomena.Polysemy.Data) is a degenerate case of SDS where both concepts have non-zero posterior under different selectional constraints applied simultaneously.

"The book is heavy and interesting":

• "heavy" selects PHYSICAL → P(PHYSICAL | heavy) is high
• "interesting" selects INFORMATIONAL → P(INFORMATIONAL | interesting) is high
• Both aspects are active → copredication is acceptable

SDS predicts this: there is no scenario conflict (both aspects coexist in normal contexts), and neither selectional constraint zeros out the other aspect's concept.

theorem Phenomena.Polysemy.Studies.ErkHerbelot2024.copredication_both_aspects_active : bookHeavyInteresting.judgment = Acceptability.acceptable

Copredication is acceptable when both aspects survive selectional filtering. This connects Polysemy.Data.bookHeavyInteresting to SDS: the acceptability follows from both concepts having non-zero posterior.

SDS and Humor: Formal Correspondence with @cite{kao-levy-goodman-2016}

Both frameworks capture the same phenomenon from different angles:

@cite{kao-levy-goodman-2016}	SDS
Multiple meanings m_a, m_b	Multiple concepts c_1, c_2
Words w supporting meanings	Constraints from predicates/context
Ambiguity (entropy)	Posterior uncertainty
Distinctiveness (KL div)	Conflict between factors

Kao's Distinctiveness measures whether different words support different meanings. SDS Conflict measures whether selectional and scenario factors prefer different concepts.

These are equivalent when we identify:

• Selectional constraints ≈ evidence from predicate words
• Scenario constraints ≈ evidence from context words

def Phenomena.Polysemy.Studies.ErkHerbelot2024.posteriorUncertainty {α : Type u_1} {Θ : Type u_2} [Semantics.Probabilistic.SDS.Core.SDSConstraintSystem α Θ] [BEq Θ] (sys : α) : ℚ

Posterior uncertainty: Gini impurity as entropy proxy for the posterior.

Corresponds to Kao's "ambiguity" measure.

• Returns 0 when one concept has probability 1 (no ambiguity)
• Returns near 0.5 for two-concept systems at maximum ambiguity

Equations

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

def Phenomena.Polysemy.Studies.ErkHerbelot2024.isTied {α : Type u_1} {Θ : Type u_2} [Semantics.Probabilistic.SDS.Core.SDSConstraintSystem α Θ] (sys : α) (c1 c2 : Θ) (tolerance : ℚ := 1 / 10) : Bool

Two concepts are "tied" when their posteriors are approximately equal. Corresponds to high ambiguity in Kao's model.

Equations

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

def Phenomena.Polysemy.Studies.ErkHerbelot2024.isPredictedPun {α : Type u_1} {Θ : Type u_2} [Semantics.Probabilistic.SDS.Core.SDSConstraintSystem α Θ] [BEq Θ] (sys : α) (uncertaintyThreshold : ℚ := 4 / 10) : Bool

A sentence is predicted to be a pun when:

1. High posterior uncertainty (ambiguity) — both meanings plausible
2. Conflict between factors (distinctiveness) — different support for each

Equations

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

def Phenomena.Polysemy.Studies.ErkHerbelot2024.predictedFunniness {α : Type u_1} {Θ : Type u_2} [Semantics.Probabilistic.SDS.Core.SDSConstraintSystem α Θ] [BEq Θ] (sys : α) : ℚ

Funniness prediction based on conflict degree.

Kao found that distinctiveness (not ambiguity) predicts fine-grained funniness. conflictDegree serves the same role.

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.predictedFunniness sys = if Semantics.Probabilistic.SDS.Core.hasConflict sys = true then Semantics.Probabilistic.SDS.Core.conflictDegree sys else 0

inductive Phenomena.Polysemy.Studies.ErkHerbelot2024.HareHairConcept : Type

Concepts for the hare/hair ambiguity

• hare : HareHairConcept
• hair : HareHairConcept

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprHareHairConcept.repr : HareHairConcept → ℕ → Std.Format

Equations

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

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprHareHairConcept : Repr HareHairConcept

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprHareHairConcept = { reprPrec := Phenomena.Polysemy.Studies.ErkHerbelot2024.instReprHareHairConcept.repr }

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqHareHairConcept : BEq HareHairConcept

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqHareHairConcept = { beq := Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqHareHairConcept.beq }

def Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqHareHairConcept.beq : HareHairConcept → HareHairConcept → Bool

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instBEqHareHairConcept.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqHareHairConcept : DecidableEq HareHairConcept

Equations

• Phenomena.Polysemy.Studies.ErkHerbelot2024.instDecidableEqHareHairConcept x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Polysemy.Studies.ErkHerbelot2024.magicianHareSDS : Semantics.Probabilistic.SDS.Core.DisambiguationScenario HareHairConcept

"The magician got so mad he pulled his hare out" as SDS.

Selectional: "pulled out" slightly prefers hair (idiomatic), but magician context activates MAGIC frame favoring rabbits.

Equations

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

theorem Phenomena.Polysemy.Studies.ErkHerbelot2024.sds_conflict_iff_different_argmax {C : Type} [BEq C] (sys : Semantics.Probabilistic.SDS.Core.DisambiguationScenario C) : Semantics.Probabilistic.SDS.Core.hasConflict sys = true ↔ ∃ (c1 : C), ∃ (c2 : C), Semantics.Probabilistic.SDS.Core.listArgmax sys.concepts sys.selectional = some c1 ∧ Semantics.Probabilistic.SDS.Core.listArgmax sys.concepts sys.scenario = some c2 ∧ (c1 != c2) = true

SDS conflict corresponds exactly to different argmax across factors.

For a disambiguation scenario, hasConflict is true iff the selectional and scenario factors have different argmax concepts. This is the formal content of the SDS↔Kao distinctiveness correspondence.

Summary: SDS and Humor

Concept	@cite{kao-levy-goodman-2016}	SDS
Latent variable	Meaning m	Concept c
Evidence integration	P(m|w) via Bayes	Product of Experts
Uncertainty	Ambiguity (entropy)	Posterior uncertainty
Distinct support	Distinctiveness (KL div)	Conflict (argmax difference)
Humor prediction	Amb ↑ AND Dist ↑	Uncertainty ↑ AND Conflict

Both formalize the same intuition: Puns arise when different sources of evidence point to different interpretations.

• In Kao: different words support different meanings
• In SDS: selectional and scenario factors prefer different concepts

TODO: Full formalization requires formalizing Kao's generative model (KaoModel) with relatedness : W → M → ℚ, defining kaoToSDS translation, and proving quantitative bounds distinctiveness(model) ≥ f(conflictDegree(kaoToSDS model)). This needs Real.log from Mathlib for KL divergence.