Embedded Scalar Implicature Types

Shared types and definitions for modeling embedded scalar implicatures (the "Every student read some book" scenario). Used by both RSAExhExpressivity (comparing RSA vs EXH expressivity) and CompositionalRSA (extending RSA to local readings).

The Scenario

We model 2 students (Alice, Bob), each of whom either read "some but not all" (S) or "all" (A) books.

Definitions

• EmbeddedSIWorld: 4 world states (SS, SA, AS, AA)
• EmbeddedSIMessage: 2 messages (everySome, everyAll)
• embeddedMeaning: literal meaning function
• ExhScope: global vs local EXH scope
• globalExhMeaning, localExhMeaning: truth conditions under each scope
• exhScopedMeaning: scope-parameterized meaning

inductive RSA.Core.EmbeddedSI.EmbeddedSIWorld : Type

World states for the embedded SI scenario. Each student either read "some but not all" (S) or "all" (A).

• SS : EmbeddedSIWorld
• SA : EmbeddedSIWorld
• AS : EmbeddedSIWorld
• AA : EmbeddedSIWorld

instance RSA.Core.EmbeddedSI.instDecidableEqEmbeddedSIWorld : DecidableEq EmbeddedSIWorld

Equations

• RSA.Core.EmbeddedSI.instDecidableEqEmbeddedSIWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.Core.EmbeddedSI.instFintypeEmbeddedSIWorld : Fintype EmbeddedSIWorld

Equations

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

def RSA.Core.EmbeddedSI.instReprEmbeddedSIWorld.repr : EmbeddedSIWorld → ℕ → Std.Format

Equations

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

instance RSA.Core.EmbeddedSI.instReprEmbeddedSIWorld : Repr EmbeddedSIWorld

Equations

• RSA.Core.EmbeddedSI.instReprEmbeddedSIWorld = { reprPrec := RSA.Core.EmbeddedSI.instReprEmbeddedSIWorld.repr }

instance RSA.Core.EmbeddedSI.instBEqEmbeddedSIWorld : BEq EmbeddedSIWorld

Equations

• RSA.Core.EmbeddedSI.instBEqEmbeddedSIWorld = { beq := RSA.Core.EmbeddedSI.instBEqEmbeddedSIWorld.beq }

def RSA.Core.EmbeddedSI.instBEqEmbeddedSIWorld.beq : EmbeddedSIWorld → EmbeddedSIWorld → Bool

Equations

• RSA.Core.EmbeddedSI.instBEqEmbeddedSIWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive RSA.Core.EmbeddedSI.EmbeddedSIMessage : Type

Messages in the embedded SI scenario

• everySome : EmbeddedSIMessage
• everyAll : EmbeddedSIMessage

instance RSA.Core.EmbeddedSI.instDecidableEqEmbeddedSIMessage : DecidableEq EmbeddedSIMessage

Equations

• RSA.Core.EmbeddedSI.instDecidableEqEmbeddedSIMessage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.Core.EmbeddedSI.instFintypeEmbeddedSIMessage : Fintype EmbeddedSIMessage

Equations

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

instance RSA.Core.EmbeddedSI.instReprEmbeddedSIMessage : Repr EmbeddedSIMessage

Equations

• RSA.Core.EmbeddedSI.instReprEmbeddedSIMessage = { reprPrec := RSA.Core.EmbeddedSI.instReprEmbeddedSIMessage.repr }

def RSA.Core.EmbeddedSI.instReprEmbeddedSIMessage.repr : EmbeddedSIMessage → ℕ → Std.Format

Equations

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

instance RSA.Core.EmbeddedSI.instBEqEmbeddedSIMessage : BEq EmbeddedSIMessage

Equations

• RSA.Core.EmbeddedSI.instBEqEmbeddedSIMessage = { beq := RSA.Core.EmbeddedSI.instBEqEmbeddedSIMessage.beq }

def RSA.Core.EmbeddedSI.instBEqEmbeddedSIMessage.beq : EmbeddedSIMessage → EmbeddedSIMessage → Bool

Equations

• RSA.Core.EmbeddedSI.instBEqEmbeddedSIMessage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def RSA.Core.EmbeddedSI.embeddedMeaning : EmbeddedSIMessage → EmbeddedSIWorld → Bool

Literal meaning: when is each message true?

• "every some" is true in all worlds (some ⊆ all)
• "every all" is true only in AA

Equations

• RSA.Core.EmbeddedSI.embeddedMeaning RSA.Core.EmbeddedSI.EmbeddedSIMessage.everySome x✝ = true
• RSA.Core.EmbeddedSI.embeddedMeaning RSA.Core.EmbeddedSI.EmbeddedSIMessage.everyAll RSA.Core.EmbeddedSI.EmbeddedSIWorld.AA = true
• RSA.Core.EmbeddedSI.embeddedMeaning RSA.Core.EmbeddedSI.EmbeddedSIMessage.everyAll x✝ = false

inductive RSA.Core.EmbeddedSI.ExhScope : Type

Scope position for EXH

• global : ExhScope
• local_ : ExhScope

instance RSA.Core.EmbeddedSI.instDecidableEqExhScope : DecidableEq ExhScope

Equations

• RSA.Core.EmbeddedSI.instDecidableEqExhScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RSA.Core.EmbeddedSI.instReprExhScope.repr : ExhScope → ℕ → Std.Format

Equations

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

instance RSA.Core.EmbeddedSI.instReprExhScope : Repr ExhScope

Equations

• RSA.Core.EmbeddedSI.instReprExhScope = { reprPrec := RSA.Core.EmbeddedSI.instReprExhScope.repr }

def RSA.Core.EmbeddedSI.globalExhMeaning : EmbeddedSIWorld → Bool

Truth conditions under global EXH: "every student read some" ∧ ¬"every student read all"

True at: SS, SA, AS (not AA)

Equations

• RSA.Core.EmbeddedSI.globalExhMeaning RSA.Core.EmbeddedSI.EmbeddedSIWorld.SS = true
• RSA.Core.EmbeddedSI.globalExhMeaning RSA.Core.EmbeddedSI.EmbeddedSIWorld.SA = true
• RSA.Core.EmbeddedSI.globalExhMeaning RSA.Core.EmbeddedSI.EmbeddedSIWorld.AS = true
• RSA.Core.EmbeddedSI.globalExhMeaning RSA.Core.EmbeddedSI.EmbeddedSIWorld.AA = false

def RSA.Core.EmbeddedSI.localExhMeaning : EmbeddedSIWorld → Bool

Truth conditions under local EXH: "every student [read some but not all]"

True at: SS only

Equations

• RSA.Core.EmbeddedSI.localExhMeaning RSA.Core.EmbeddedSI.EmbeddedSIWorld.SS = true
• RSA.Core.EmbeddedSI.localExhMeaning RSA.Core.EmbeddedSI.EmbeddedSIWorld.SA = false
• RSA.Core.EmbeddedSI.localExhMeaning RSA.Core.EmbeddedSI.EmbeddedSIWorld.AS = false
• RSA.Core.EmbeddedSI.localExhMeaning RSA.Core.EmbeddedSI.EmbeddedSIWorld.AA = false

def RSA.Core.EmbeddedSI.exhScopedMeaning (scope : ExhScope) : EmbeddedSIWorld → Bool

EXH-with-scope: meaning depends on scope position

Equations

• RSA.Core.EmbeddedSI.exhScopedMeaning RSA.Core.EmbeddedSI.ExhScope.global = RSA.Core.EmbeddedSI.globalExhMeaning
• RSA.Core.EmbeddedSI.exhScopedMeaning RSA.Core.EmbeddedSI.ExhScope.local_ = RSA.Core.EmbeddedSI.localExhMeaning