Compositional Lexical Uncertainty for Embedded Implicatures

Architecture

This extends lexical uncertainty to handle compositional utterances. Instead of refining whole-utterance meanings, we refine atomic lexical items and then compose meanings via Boolean connectives.

Innovation (@cite{bergen-levy-goodman-2016}, Section 5)

For compositional LU:

1. Atomic utterances have refinable meanings in the lexicon
2. Complex utterances are composed via ∨, ∧, ¬
3. Refinement operates BEFORE composition

This derives non-convex disjunctive implicatures:

• "one or three" → exactly 1 or exactly 3 (not 2)
• "warm or scalding" → warm-not-hot or scalding (not hot)

Hurford-Violating Disjunctions

When one disjunct entails the other (e.g., "some or all"), standard semantics predicts no difference from the weaker disjunct. But:

• "some" → not all (scalar implicature)
• "some or all" → speaker ignorant (no scalar implicature)

Compositional LU derives this by tracking which refinements are available.

Relationship to RSAConfig and PottsEtAl2016

The CompLUScenario type is conceptually subsumed by RSAConfig with Latent := Lexicon. The @cite{potts-etal-2016} study uses this standard mechanism to derive embedded SI predictions (DE blocking, UE enrichment) without the compositional utterance infrastructure here.

This file is retained for:

• CompUtt: Compositional utterance structure (atom, disj, conj, neg)
• AtomicLexicon: Refinable lexica operating at the atomic level
• violatesHurford: Hurford constraint checker for disjunctions
• EmbeddedSIPrediction: Structured tracking of embedded SI predictions (the @cite{potts-etal-2016} model demonstrates the negation case)

inductive CompUtt (Atom : Type) : Type

Compositional utterances built from atomic items and Boolean connectives.

This represents the syntactic structure that feeds into compositional semantics.

• atom {Atom : Type} : Atom → CompUtt Atom

  Atomic utterance (lexical item)

• disj {Atom : Type} : CompUtt Atom → CompUtt Atom → CompUtt Atom

  Disjunction

• conj {Atom : Type} : CompUtt Atom → CompUtt Atom → CompUtt Atom

  Conjunction

• neg {Atom : Type} : CompUtt Atom → CompUtt Atom

  Negation

instance instBEqCompUtt {Atom✝ : Type} [BEq Atom✝] : BEq (CompUtt Atom✝)

Equations

• instBEqCompUtt = { beq := instBEqCompUtt.beq }

def instBEqCompUtt.beq {Atom✝ : Type} [BEq Atom✝] : CompUtt Atom✝ → CompUtt Atom✝ → Bool

Equations

• instBEqCompUtt.beq (CompUtt.atom a) (CompUtt.atom b) = (a == b)
• instBEqCompUtt.beq (a ∨ᵤ a_1) (b ∨ᵤ b_1) = (instBEqCompUtt.beq a b && instBEqCompUtt.beq a_1 b_1)
• instBEqCompUtt.beq (a ∧ᵤ a_1) (b ∧ᵤ b_1) = (instBEqCompUtt.beq a b && instBEqCompUtt.beq a_1 b_1)
• instBEqCompUtt.beq (¬ᵤa) (¬ᵤb) = instBEqCompUtt.beq a b
• instBEqCompUtt.beq x✝¹ x✝ = false

def CompUtt.«term_∨ᵤ_» : Lean.TrailingParserDescr

Infix notation for disjunction

Equations

• CompUtt.«term_∨ᵤ_» = Lean.ParserDescr.trailingNode `CompUtt.«term_∨ᵤ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ᵤ ") (Lean.ParserDescr.cat `term 66))

def CompUtt.«term_∧ᵤ_» : Lean.TrailingParserDescr

Infix notation for conjunction

Equations

• CompUtt.«term_∧ᵤ_» = Lean.ParserDescr.trailingNode `CompUtt.«term_∧ᵤ_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ᵤ ") (Lean.ParserDescr.cat `term 71))

def CompUtt.«term¬ᵤ_» : Lean.ParserDescr

Prefix notation for negation

Equations

• CompUtt.«term¬ᵤ_» = Lean.ParserDescr.node `CompUtt.«term¬ᵤ_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬ᵤ") (Lean.ParserDescr.cat `term 75))

def CompUtt.atoms {Atom : Type} : CompUtt Atom → List Atom

Extract all atomic items from a compositional utterance

Equations

• (CompUtt.atom a).atoms = [a]
• (u₁ ∨ᵤ u₂).atoms = u₁.atoms ++ u₂.atoms
• (u₁ ∧ᵤ u₂).atoms = u₁.atoms ++ u₂.atoms
• (¬ᵤu).atoms = u.atoms

def CompUtt.complexity {Atom : Type} : CompUtt Atom → ℕ

Count the complexity (number of connectives)

Equations

• (CompUtt.atom a).complexity = 0
• (u₁ ∨ᵤ u₂).complexity = 1 + u₁.complexity + u₂.complexity
• (u₁ ∧ᵤ u₂).complexity = 1 + u₁.complexity + u₂.complexity
• (¬ᵤu).complexity = 1 + u.complexity

structure AtomicLexicon (Atom World : Type) : Type

An atomic lexicon maps atomic utterances to Boolean meanings.

This is the refinable part of the lexicon.

• meaning : Atom → World → Bool

  Meaning of each atomic item

def AtomicLexicon.interpret {A W : Type} (L : AtomicLexicon A W) : CompUtt A → W → Bool

Compose meanings of complex utterances from atomic meanings

Equations

• L.interpret (CompUtt.atom a) x✝ = L.meaning a x✝
• L.interpret (u₁ ∨ᵤ u₂) x✝ = (L.interpret u₁ x✝ || L.interpret u₂ x✝)
• L.interpret (u₁ ∧ᵤ u₂) x✝ = (L.interpret u₁ x✝ && L.interpret u₂ x✝)
• L.interpret (¬ᵤu) x✝ = !L.interpret u x✝

def AtomicLexicon.refines {A W : Type} (L' L : AtomicLexicon A W) : Prop

Check if one atomic lexicon refines another

Equations

• L'.refines L = ∀ (a : A) (w : W), L.meaning a w = false → L'.meaning a w = false

structure CompLUScenario : Type 1

Compositional Lexical Uncertainty Scenario.

Extends LU to handle compositional utterances where:

• Atomic items have refinable meanings
• Complex meanings are composed via Boolean connectives

• Atom : Type

  Type of atomic utterances

• World : Type

  Type of possible worlds

• baseLexicon : AtomicLexicon self.Atom self.World

  Base atomic lexicon (unrefined meanings)

• lexica : List (AtomicLexicon self.Atom self.World)

  Set of possible refined atomic lexica

• lexPrior : AtomicLexicon self.Atom self.World → ℚ

  Prior over lexica

• worldPrior : self.World → ℚ

  Prior over worlds

• utterances : List (CompUtt self.Atom)

  Set of available (complex) utterances

• worlds : List self.World

  Enumeration of worlds

• α : ℕ

  Rationality parameter

• atomBEq : BEq self.Atom
• worldBEq : BEq self.World

inductive ThreePointWorld : Type

Worlds for a 3-point scale (one, two, three).

• one : ThreePointWorld
• two : ThreePointWorld
• three : ThreePointWorld

def instReprThreePointWorld.repr : ThreePointWorld → ℕ → Std.Format

Equations

• instReprThreePointWorld.repr ThreePointWorld.one prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThreePointWorld.one")).group prec✝
• instReprThreePointWorld.repr ThreePointWorld.two prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThreePointWorld.two")).group prec✝
• instReprThreePointWorld.repr ThreePointWorld.three prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThreePointWorld.three")).group prec✝

instance instReprThreePointWorld : Repr ThreePointWorld

Equations

• instReprThreePointWorld = { reprPrec := instReprThreePointWorld.repr }

instance instBEqThreePointWorld : BEq ThreePointWorld

Equations

• instBEqThreePointWorld = { beq := instBEqThreePointWorld.beq }

def instBEqThreePointWorld.beq : ThreePointWorld → ThreePointWorld → Bool

Equations

• instBEqThreePointWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instDecidableEqThreePointWorld : DecidableEq ThreePointWorld

Equations

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

inductive NumeralAtom : Type

Atomic utterances for numerals.

• one_ : NumeralAtom
• two_ : NumeralAtom
• three_ : NumeralAtom

instance instReprNumeralAtom : Repr NumeralAtom

Equations

• instReprNumeralAtom = { reprPrec := instReprNumeralAtom.repr }

def instReprNumeralAtom.repr : NumeralAtom → ℕ → Std.Format

Equations

• instReprNumeralAtom.repr NumeralAtom.one_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NumeralAtom.one_")).group prec✝
• instReprNumeralAtom.repr NumeralAtom.two_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NumeralAtom.two_")).group prec✝
• instReprNumeralAtom.repr NumeralAtom.three_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NumeralAtom.three_")).group prec✝

def instBEqNumeralAtom.beq : NumeralAtom → NumeralAtom → Bool

Equations

• instBEqNumeralAtom.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instBEqNumeralAtom : BEq NumeralAtom

Equations

• instBEqNumeralAtom = { beq := instBEqNumeralAtom.beq }

instance instDecidableEqNumeralAtom : DecidableEq NumeralAtom

Equations

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

def numeralBaseLexicon : AtomicLexicon NumeralAtom ThreePointWorld

Base semantics for numerals: lower-bound (at-least) reading.

Equations

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

def numeralRefinedLexica : List (AtomicLexicon NumeralAtom ThreePointWorld)

Generate all valid refinements of the numeral lexicon.

For "one": can refine to {1}, {2}, {3}, {1,2}, {1,3}, {2,3}, {1,2,3} For "two": can refine to {2}, {3}, {2,3} For "three": only {3} (already maximally specific)

Equations

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

def mkNonConvexDisjScenario : CompLUScenario

Build scenario for non-convex disjunction implicatures.

Compares "one or two" vs "one or three".

Equations

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

def entails (S : CompLUScenario) (u₁ u₂ : CompUtt S.Atom) : Bool

Check if one utterance semantically entails another under base semantics.

Equations

• entails S u₁ u₂ = S.worlds.all fun (w : S.World) => !S.baseLexicon.interpret u₁ w || S.baseLexicon.interpret u₂ w

def violatesHurford (S : CompLUScenario) : CompUtt S.Atom → Bool

Hurford's constraint: a disjunction is odd if one disjunct entails the other.

"#Some or all of the students passed" violates Hurford because "all" ⊆ "some". But such sentences ARE felicitous and have ignorance implicatures!

Equations

• violatesHurford S (u₁ ∨ᵤ u₂) = (entails S u₁ u₂ || entails S u₂ u₁)
• violatesHurford S x✝ = false

structure EmbeddedSIPrediction : Type

Structure for tracking embedded implicature predictions.

This connects to Potts et al.'s "An experimental investigation of embedded scalar implicatures".

• context : String

  The embedding context (e.g., negation, conditional)

• scalarItem : String

  The scalar item

• localAvailable : Bool

  Whether local (embedded) reading is available

• globalAvailable : Bool

  Whether global reading is available

• preferLocal : Option Bool

  Predicted preference (local vs global)

instance instReprEmbeddedSIPrediction : Repr EmbeddedSIPrediction

Equations

• instReprEmbeddedSIPrediction = { reprPrec := instReprEmbeddedSIPrediction.repr }

def instReprEmbeddedSIPrediction.repr : EmbeddedSIPrediction → ℕ → Std.Format

Equations

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

def embeddedSIPredictions : List EmbeddedSIPrediction

Compositional LU predictions for various embedding contexts.

Key prediction: Local readings are available when the asymmetry in lexical refinements makes them pragmatically useful.

Equations

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