RSA Model for Scope Freezing

RSA model showing that "frozen" scope readings can be rescued by world priors.

Architecture

1. Phenomena/ScopeFreezing: Provides examples with observed availability
2. Grammar (Minimalism/CCG): Both predict freezing for possessor, double-object, etc.
3. RSA: Takes grammar's parse, shows world priors can rescue frozen readings

The Key Claim

Grammar theories say: frozen = grammatically impossible (categorical) RSA says: frozen = strongly dispreferred (gradient, rescuable by context)

This module provides the domain types and meaning functions for the scope freezing RSA model.

inductive RSA.ScopeFreezing.World : Type

World state for two-quantifier sentences. w0: neither scope true, w1: inverse-only true, w2: both true

• w0 : World
• w1 : World
• w2 : World

instance RSA.ScopeFreezing.instDecidableEqWorld : DecidableEq World

Equations

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

def RSA.ScopeFreezing.instBEqWorld.beq : World → World → Bool

Equations

• RSA.ScopeFreezing.instBEqWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.ScopeFreezing.instBEqWorld : BEq World

Equations

• RSA.ScopeFreezing.instBEqWorld = { beq := RSA.ScopeFreezing.instBEqWorld.beq }

instance RSA.ScopeFreezing.instReprWorld : Repr World

Equations

• RSA.ScopeFreezing.instReprWorld = { reprPrec := RSA.ScopeFreezing.instReprWorld.repr }

def RSA.ScopeFreezing.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

def RSA.ScopeFreezing.instInhabitedWorld.default : World

Equations

• RSA.ScopeFreezing.instInhabitedWorld.default = RSA.ScopeFreezing.World.w0

instance RSA.ScopeFreezing.instInhabitedWorld : Inhabited World

Equations

• RSA.ScopeFreezing.instInhabitedWorld = { default := RSA.ScopeFreezing.instInhabitedWorld.default }

def RSA.ScopeFreezing.allWorlds : List World

Equations

• RSA.ScopeFreezing.allWorlds = [RSA.ScopeFreezing.World.w0, RSA.ScopeFreezing.World.w1, RSA.ScopeFreezing.World.w2]

def RSA.ScopeFreezing.surfaceTrue : World → Bool

Surface (exists>forall) truth conditions

Equations

• RSA.ScopeFreezing.surfaceTrue RSA.ScopeFreezing.World.w2 = true
• RSA.ScopeFreezing.surfaceTrue x✝ = false

def RSA.ScopeFreezing.inverseTrue : World → Bool

Inverse (forall>exists) truth conditions

Equations

• RSA.ScopeFreezing.inverseTrue RSA.ScopeFreezing.World.w1 = true
• RSA.ScopeFreezing.inverseTrue RSA.ScopeFreezing.World.w2 = true
• RSA.ScopeFreezing.inverseTrue x✝ = false

def RSA.ScopeFreezing.meaning (s : Semantics.Scope.ScopeConfig) (w : World) : Bool

Equations

• RSA.ScopeFreezing.meaning Semantics.Scope.ScopeConfig.surface w = RSA.ScopeFreezing.surfaceTrue w
• RSA.ScopeFreezing.meaning Semantics.Scope.ScopeConfig.inverse w = RSA.ScopeFreezing.inverseTrue w

inductive RSA.ScopeFreezing.Utterance : Type

• target : Utterance
• null : Utterance

instance RSA.ScopeFreezing.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

instance RSA.ScopeFreezing.instBEqUtterance : BEq Utterance

Equations

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

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

Equations

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

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

Equations

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

instance RSA.ScopeFreezing.instReprUtterance : Repr Utterance

Equations

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

instance RSA.ScopeFreezing.instInhabitedUtterance : Inhabited Utterance

Equations

• RSA.ScopeFreezing.instInhabitedUtterance = { default := RSA.ScopeFreezing.instInhabitedUtterance.default }

def RSA.ScopeFreezing.instInhabitedUtterance.default : Utterance

Equations

• RSA.ScopeFreezing.instInhabitedUtterance.default = RSA.ScopeFreezing.Utterance.target

def RSA.ScopeFreezing.allUtterances : List Utterance

Equations

• RSA.ScopeFreezing.allUtterances = [RSA.ScopeFreezing.Utterance.target, RSA.ScopeFreezing.Utterance.null]

def RSA.ScopeFreezing.allScopes : List Semantics.Scope.ScopeConfig

Equations

• RSA.ScopeFreezing.allScopes = [Semantics.Scope.ScopeConfig.surface, Semantics.Scope.ScopeConfig.inverse]

def RSA.ScopeFreezing.uttMeaning (s : Semantics.Scope.ScopeConfig) (u : Utterance) (w : World) : Bool

Equations

• RSA.ScopeFreezing.uttMeaning s RSA.ScopeFreezing.Utterance.null w = true
• RSA.ScopeFreezing.uttMeaning s RSA.ScopeFreezing.Utterance.target w = RSA.ScopeFreezing.meaning s w

def RSA.ScopeFreezing.uniformWorldPrior : World → ℚ

Equations

• RSA.ScopeFreezing.uniformWorldPrior x✝ = 1

def RSA.ScopeFreezing.rescueWorldPrior : World → ℚ

Rescue prior: strongly favor inverse-only world

Equations

• RSA.ScopeFreezing.rescueWorldPrior RSA.ScopeFreezing.World.w1 = 99 / 100
• RSA.ScopeFreezing.rescueWorldPrior x✝ = 1 / 200

Phenomena-Dependent Content

Definitions and theorems that depend on Phenomena types (Availability, Example, possessor_baseline, possessor_frozen, etc.) have been moved to Linglib.Phenomena.Quantification.Studies.RSAScopeFreezing.

This includes: interpPriorFromAvailability, interpPriorFromExample, baseline, frozen, grammarInterpPrior, and all associated theorems.