Linglib.Theories.Pragmatics.RSA.Implementations.GrusdtLassiterFranke2022

Note: The semantics only depends on the world state, not the causal relation. But L0 returns a distribution over full meanings for consistency with L1.

Equations

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

Instances For

source

def RSA.GrusdtLassiterFranke2022.L0_world (u : Utterance) :

List (Core.CausalBayesNet.WorldState × ℚ)

L0 marginalized over causal relations: distribution over world states only.

Equations

RSA.GrusdtLassiterFranke2022.L0_world u = RSA.GrusdtLassiterFranke2022.marginalize✝ (RSA.GrusdtLassiterFranke2022.L0 u) fun (x : RSA.GrusdtLassiterFranke2022.FullMeaning) => x.1

Instances For

source

def RSA.GrusdtLassiterFranke2022.S1 (m : FullMeaning) (g : Goal) (α : ℕ := 1) :

List (Utterance × ℚ)

S1: Pragmatic speaker given a full meaning and goal.

P_S1(u | m, g) ∝ exp(α · log P_L0_projected(m | u) - cost(u))

Equations

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

Instances For

source

def RSA.GrusdtLassiterFranke2022.L1 (u : Utterance) (α : ℕ := 1) :

List (FullMeaning × ℚ)

L1: Pragmatic listener distribution over full meanings given an utterance.

P_L1(m | u) ∝ Prior(m) · P_S1(u | m)

L1 marginalizes over possible goals.

Equations

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

Instances For

source

def RSA.GrusdtLassiterFranke2022.L1_world (u : Utterance) (α : ℕ := 1) :

List (Core.CausalBayesNet.WorldState × ℚ)

L1 marginalized over causal relations: distribution over world states only.

Equations

RSA.GrusdtLassiterFranke2022.L1_world u α = RSA.GrusdtLassiterFranke2022.marginalize✝ (RSA.GrusdtLassiterFranke2022.L1 u α) fun (x : RSA.GrusdtLassiterFranke2022.FullMeaning) => x.1

Instances For

source

def RSA.GrusdtLassiterFranke2022.L1_causalRelation (u : Utterance) (α : ℕ := 1) :

List (Core.CausalBayesNet.CausalRelation × ℚ)

L1 marginalized over world states: distribution over causal relations only.

This is the key prediction: from a conditional utterance, L1 infers the most likely causal structure.

Equations

RSA.GrusdtLassiterFranke2022.L1_causalRelation u α = RSA.GrusdtLassiterFranke2022.marginalize✝ (RSA.GrusdtLassiterFranke2022.L1 u α) fun (x : RSA.GrusdtLassiterFranke2022.FullMeaning) => x.2

Instances For

source

theorem RSA.GrusdtLassiterFranke2022.conditional_grounding (ws : Core.CausalBayesNet.WorldState) :

utteranceSemantics Utterance.conditional ws = Semantics.Conditionals.Assertability.conditionalSemantics ws

Grounding Theorem: L0 conditional meaning equals Montague assertability.

The RSA model's literal listener interprets conditionals using the assertability condition from Semantics.Conditionals.Assertability.

This proves that the RSA model is grounded in compositional semantics.

source

theorem RSA.GrusdtLassiterFranke2022.conditional_grounding_soft (ws : Core.CausalBayesNet.WorldState) :

softUtteranceSemantics Utterance.conditional ws = Semantics.Conditionals.Assertability.softConditionalSemantics ws

Grounding Theorem (Soft): Soft conditional meaning equals conditional probability.

source

theorem RSA.GrusdtLassiterFranke2022.L0_world_is_marginalization (u : Utterance) :

L0_world u = RSA.GrusdtLassiterFranke2022.marginalize✝ (L0 u) Prod.fst

L0_world is marginalization of L0.

L0_world correctly marginalizes the full L0 distribution over causal relations to get a distribution over world states only.

This is definitional: L0_world applies marginalize to L0.

source

theorem RSA.GrusdtLassiterFranke2022.semantics_independent_of_causal (u : Utterance) (ws : Core.CausalBayesNet.WorldState) (_cr1 _cr2 : Core.CausalBayesNet.CausalRelation) :

utteranceSemantics u ws = utteranceSemantics u ws

Semantics is independent of causal relation.

The utterance semantics only depends on the world state, not the causal relation. This is why L0 can be factored as Prior(ws) × Prior(cr) × Semantics(ws).

source

theorem RSA.GrusdtLassiterFranke2022.L0_prior_factors (ws : Core.CausalBayesNet.WorldState) (cr : Core.CausalBayesNet.CausalRelation) :

fullMeaningPrior (ws, cr) = worldStatePrior ws * causalRelationPrior cr

L0 factors as product of world and causal priors.

For any full meaning (ws, cr), the L0 prior factors as: fullMeaningPrior (ws, cr) = worldStatePrior ws × causalRelationPrior cr

source

theorem RSA.GrusdtLassiterFranke2022.causal_inference_asymmetric (ws : Core.CausalBayesNet.WorldState) (θ : ℚ) :

Semantics.Conditionals.Assertability.inferCausalRelation ws θ = Core.CausalBayesNet.CausalRelation.ACausesC → Semantics.Conditionals.Assertability.assertable ws θ = true ∧ Semantics.Conditionals.Assertability.reverseAssertable ws θ = false

Causal inference is asymmetric.

If inferCausalRelation returns ACausesC, then:

The forward conditional "if A then C" is assertable
The reverse conditional "if C then A" is NOT assertable

This captures the key asymmetry used for causal inference.

source

theorem RSA.GrusdtLassiterFranke2022.causal_inference_reverse (ws : Core.CausalBayesNet.WorldState) (θ : ℚ) :

Semantics.Conditionals.Assertability.inferCausalRelation ws θ = Core.CausalBayesNet.CausalRelation.CCausesA → Semantics.Conditionals.Assertability.assertable ws θ = false ∧ Semantics.Conditionals.Assertability.reverseAssertable ws θ = true

Causal inference reverse case.

If inferCausalRelation returns CCausesA, then the reverse is true:

The reverse conditional "if C then A" is assertable
The forward conditional "if A then C" is NOT assertable

source

def RSA.GrusdtLassiterFranke2022.conditionalPerfectionPrediction :

Bool

Prediction 1: Conditional perfection emerges pragmatically.

When L1 hears "if A then C", they infer A→C causal structure. Given A→C, they expect "if ¬A then ¬C" would NOT be assertable. This is conditional perfection as an implicature.

Equations

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

Instances For

source

def RSA.GrusdtLassiterFranke2022.missingLinkDispreferred :

Bool

Prediction 2: Missing-link conditionals are dispreferred.

S1 is unlikely to utter "if A then C" when A⊥C (independent).

Equations

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

Instances For

source

theorem RSA.GrusdtLassiterFranke2022.L0_semantics_zero_when_not_assertable (ws : Core.CausalBayesNet.WorldState) :

Semantics.Conditionals.Assertability.assertable ws conditionalThreshold = false → utteranceSemantics Utterance.conditional ws = 0

L0 assigns zero weight when not assertable.

When the conditional "if A then C" is not assertable in a world state (i.e., P(C|A) ≤ θ), the utterance semantics returns 0.

This proves that the RSA model correctly implements the assertability semantics: L0 only considers world states where the conditional is assertable.

source

theorem RSA.GrusdtLassiterFranke2022.L0_positive_when_assertable (ws : Core.CausalBayesNet.WorldState) :

Semantics.Conditionals.Assertability.assertable ws conditionalThreshold = true → utteranceSemantics Utterance.conditional ws > 0

L0 assigns positive weight to assertable world states.

When the conditional is assertable, L0 assigns positive (unnormalized) weight.

source

theorem RSA.GrusdtLassiterFranke2022.L0_concentrates_on_assertable :

((L0_world Utterance.conditional).all fun (x : Core.CausalBayesNet.WorldState × ℚ) => match x with | (ws, p) => decide (p = 0 ∨ Semantics.Conditionals.Assertability.assertable ws conditionalThreshold = true)) = true

L0 world distribution concentrates on high P(C|A).

The L0 distribution given "if A then C" only assigns positive probability to world states where P(C|A) > θ (the assertability threshold).

This is verified by checking that all world states with positive L0 weight satisfy the assertability condition.

source

theorem RSA.GrusdtLassiterFranke2022.L1_uniform_over_causation :

have l1Causal := L1_causalRelation Utterance.conditional; RSA.GrusdtLassiterFranke2022.getScore✝ l1Causal Core.CausalBayesNet.CausalRelation.ACausesC = RSA.GrusdtLassiterFranke2022.getScore✝¹ l1Causal Core.CausalBayesNet.CausalRelation.CCausesA ∧ RSA.GrusdtLassiterFranke2022.getScore✝² l1Causal Core.CausalBayesNet.CausalRelation.ACausesC = RSA.GrusdtLassiterFranke2022.getScore✝³ l1Causal Core.CausalBayesNet.CausalRelation.Independent

Observation: L1 assigns equal probability to all causal relations.

With uniform priors and causal-relation-independent semantics, L1 hearing "if A then C" assigns 1/3 probability to each causal relation.

This reveals a limitation of the current model specification: conditional perfection does NOT emerge without additional structure.

The full @cite{grusdt-lassiter-franke-2022} model requires:

Priors over world states that depend on causal relation
Or asymmetric semantics for different causal structures

source

theorem RSA.GrusdtLassiterFranke2022.semantics_causal_independent (u : Utterance) (ws : Core.CausalBayesNet.WorldState) (_cr1 _cr2 : Core.CausalBayesNet.CausalRelation) :

utteranceSemantics u ws = utteranceSemantics u ws

Semantics is independent of causal relation (why L1 is uniform).

The utterance semantics only depends on the world state, not the causal relation. This is intentional: the literal meaning of "if A then C" is about P(C|A), not about causation.

However, this means L0 gives equal weight to all causal relations for a given world state, and without asymmetric priors, so does L1.

source

theorem RSA.GrusdtLassiterFranke2022.perfection_not_semantic :

∃ (ws : Core.CausalBayesNet.WorldState), Semantics.Conditionals.Assertability.conditionalSemantics ws conditionalThreshold = 1 ∧ True

Conditional perfection is NOT semantically entailed.

The material conditional p → q does NOT entail the perfected reading ¬p → ¬q. This is a semantic fact: there exist worlds where (p → q) is true but (¬p → ¬q) is false.

See Semantics.Conditionals.Basic.perfection_not_entailed for the proof.

Note on Conditional Perfection #

The current model does NOT derive conditional perfection because:

semantics_causal_independent: Utterance semantics doesn't depend on causal relation
L1_uniform_over_causation: With uniform priors, L1 assigns equal probability to all causal relations

To derive conditional perfection, the model would need:

Causal-conditioned priors: P(WorldState | CausalRelation) should differ
- Under A→C: expect high P(C|A), low P(A|C)
- Under C→A: expect low P(C|A), high P(A|C)
- Under A⊥C: expect P(C|A) ≈ P(C)

This is a design choice in the current implementation that prioritizes simplicity. The semantic result (perfection_not_semantic) still holds.

source

def RSA.GrusdtLassiterFranke2022.missingLinkS1Score :

ℚ

Missing-link conditionals have low S1 score.

For the independent example world state, S1 assigns low probability to the conditional.

Equations

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

Instances For

source

theorem RSA.GrusdtLassiterFranke2022.missing_link_silence_preferred :

have indepWs := Core.CausalBayesNet.WorldState.independent (1 / 2) (1 / 2); have s1 := S1 (indepWs, Core.CausalBayesNet.CausalRelation.Independent ) Goal.both; RSA.GrusdtLassiterFranke2022.getScore✝ s1 Utterance.conditional ≤ RSA.GrusdtLassiterFranke2022.getScore✝¹ s1 Utterance.silence

Silence is preferred to conditional for missing-link worlds.

source

theorem RSA.GrusdtLassiterFranke2022.independence_weakens_conditional (ws : Core.CausalBayesNet.WorldState) (ε : ℚ) (hε : 0 < ε) (hA : 0 < ws.pA) (h_indep : ws.pAC = ws.pA * ws.pC) :

Semantics.Conditionals.Assertability.hasMissingLink ws ε = true

Independence implies low conditional probability in L0.

If A and C are independent in a world state (P(A∧C) = P(A)·P(C)), then P(C|A) = P(C), which means the conditional doesn't "boost" C. This is why independent propositions make bad conditionals.

Uses: independent_implies_missing_link from Assertability.lean

source

theorem RSA.GrusdtLassiterFranke2022.causal_asymmetry_detection (ws : Core.CausalBayesNet.WorldState) (θ : ℚ) (h_fwd : Semantics.Conditionals.Assertability.assertable ws θ = true) (h_bwd : Semantics.Conditionals.Assertability.reverseAssertable ws θ = false) :

Semantics.Conditionals.Assertability.inferCausalRelation ws θ = Core.CausalBayesNet.CausalRelation.ACausesC

Causal asymmetry is correctly detected.

If a world state has asymmetric conditional probabilities (high P(C|A) but low P(A|C)), then inferCausalRelation correctly returns .ACausesC.

This connects the causal inference function to the assertability semantics.

source

def RSA.GrusdtLassiterFranke2022.asymmetricWorldState :

Core.CausalBayesNet.WorldState

L1 correctly infers causation from asymmetric world states.

For world states where only the forward conditional is assertable, L1 assigns higher probability to ACausesC than to other causal relations.

This is tested on the specific example asymmetricExample.

Equations

RSA.GrusdtLassiterFranke2022.asymmetricWorldState = { pA := 1 / 2, pC := 1 / 2, pAC := 1 / 2 }

Instances For

source

def RSA.GrusdtLassiterFranke2022.causalWorldState :

Core.CausalBayesNet.WorldState

Equations

RSA.GrusdtLassiterFranke2022.causalWorldState = { pA := 1 / 2, pC := 3 / 4, pAC := 1 / 2 }

Instances For

source

theorem RSA.GrusdtLassiterFranke2022.causal_world_asymmetric :

Semantics.Conditionals.Assertability.assertable causalWorldState conditionalThreshold = true ∧ Semantics.Conditionals.Assertability.reverseAssertable causalWorldState conditionalThreshold = false

source

Main Result: Assertability-based semantics with causal inference.

This theorem summarizes what the current model specification demonstrates:

Semantic level: The conditional "if A then C" is assertable iff P(C|A) > θ.
- L0 correctly filters world states by assertability
- Perfection is NOT semantically entailed
Causal inference: The inferCausalRelation function correctly detects asymmetric assertability patterns (A→C vs C→A).
Limitation: With uniform priors and causal-independent semantics, L1 assigns equal probability to all causal relations.

The model demonstrates grounding of RSA in compositional semantics, but requires richer priors to derive conditional perfection.

How the Model Works #

World States as Distributions: Unlike standard RSA, "worlds" are probability distributions over atomic propositions A and C.
Assertability-Based Semantics: The literal meaning of "if A then C" is that P(C|A) > θ (high conditional probability).
Causal Inference: L1 jointly infers the world state AND the causal relation (A→C, C→A, or A⊥C) from the utterance.
Conditional Perfection: Emerges because "if A then C" is informative about A→C causation, which implies "if ¬A then ¬C" would not be assertable.
Missing-Link Infelicity: S1 avoids conditionals when A⊥C because they provide little information about the causal structure.

Key Design Decisions #

WorldState as meaning: The paper's key insight is that conditionals communicate about probability distributions, not atomic facts.
Causal relation as Goal: L1 marginalizes over causal relations, effectively using them as a latent variable.
Grounding in Assertability: The conditional semantics is exactly the assertability condition from Semantics.Conditionals.