Documentation

Studies.GrusdtLassiterFranke2022

Grusdt, Lassiter, and Franke (2022): Rational Communication with Conditionals #

This file formalizes the toy example of section 2.3 of Grusdt, Lassiter and Franke, "Probabilistic modeling of rational communication with conditionals", together with the two arguments of section 5 that rest on its assertability conditions alone. A state is a probability measure on the four worlds that fix the truth of A and C; an utterance is assertable in a state by the conditions of Table 1, P(A ∧ C) ≥ θ for the conjunction, P(C) ≥ θ for the literal, P(C | A) ≥ θ for the conditional, and P(C) > 1/2 for likely C (Assertable); and the vanilla Rational Speech Act model of section 2.1, the library's RSA.speaker and its posterior at α = 1 without costs, runs over the three states of Table 2. Its predictions are derived: the extensions of Table 2(b), the speaker shares of Table 2(d), and the listener posteriors of Table 2(e), on which hearing if A then C favors the state where the conditional is the most informative assertable utterance over the one where the literal was available (l1_conditional_prefers_s2). Section 5's observations hold for every state: when antecedent and consequent are independent the conditional is assertable only where the literal is, so a speaker never prefers it, which is what lies behind the infelicity of missing-link conditionals (assertable_C_of_indep), and a speaker who can assert both if A then C and if not A then C could have asserted C outright (assertable_C_of_conditionals).

Implementation notes #

States are measures built from the cells of Table 2(a); the threshold is the paper's θ = 0.9. Section 5.3's argument takes P(A) = 1/2, but the theorem needs only that the antecedent and its negation both have positive probability. The causal Bayes-net prior of sections 2.4 to 3 and the simulation results over it, including the strength of conditional perfection in Figure 8, are not formalized; perfection_not_semantic records only that in the toy example the conditional is assertable at s2 while P(¬C | ¬A) falls short of the threshold, so any perfection reading there is pragmatic.

References #

[GLF22]

World states, utterances and assertability, section 2.2 #

def GrusdtLassiterFranke2022.A :

Set (Bool × Bool)

The event that A holds, on worlds (A, C) : Bool × Bool.

Equations

GrusdtLassiterFranke2022.A = {w : Bool × Bool | w.1 = true}

Instances For

def GrusdtLassiterFranke2022.C :

Set (Bool × Bool)

The event that C holds.

Equations

GrusdtLassiterFranke2022.C = {w : Bool × Bool | w.2 = true}

Instances For

theorem GrusdtLassiterFranke2022.A_eq :

A = ↑{(true, true), (true, false)}

theorem GrusdtLassiterFranke2022.C_eq :

C = ↑{(true, true), (false, true)}

theorem GrusdtLassiterFranke2022.A_inter_C_eq :

A ∩ C = ↑{(true, true)}

theorem GrusdtLassiterFranke2022.Ac_eq :

A ᶜ = ↑{(false, true), (false, false)}

theorem GrusdtLassiterFranke2022.Ac_inter_Cc_eq :

A ᶜ ∩ C ᶜ = ↑{(false, false)}

inductive GrusdtLassiterFranke2022.Utt :

The toy example's utterances, in Table 1's order of informativity, are the conjunction A and C, the literal C, the conditional if A then C, and likely C.

conjAC : Utt
C : Utt
conditional : Utt
likelyC : Utt

Instances For

@[instance_reducible]

instance GrusdtLassiterFranke2022.instDecidableEqUtt :

DecidableEq Utt

Equations

GrusdtLassiterFranke2022.instDecidableEqUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance GrusdtLassiterFranke2022.instFintypeUtt :

Fintype Utt

Equations

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

@[instance_reducible]

instance GrusdtLassiterFranke2022.instMeasurableSpaceUtt :

MeasurableSpace Utt

Equations

GrusdtLassiterFranke2022.instMeasurableSpaceUtt = ⊤

instance GrusdtLassiterFranke2022.instDiscreteMeasurableSpaceUtt :

DiscreteMeasurableSpace Utt

instance GrusdtLassiterFranke2022.instNonemptyUtt :

Nonempty Utt

noncomputable def GrusdtLassiterFranke2022.θ :

ℝ

The assertability threshold of Table 2, θ = 0.9.

Equations

GrusdtLassiterFranke2022.θ = 9 / 10

Instances For

def GrusdtLassiterFranke2022.Assertable (θ : ℝ) :

Utt → MeasureTheory.Measure (Bool × Bool) → Prop

By Table 1, an utterance is assertable in a state μ when the probability it conveys reaches the threshold, P(A ∧ C) ≥ θ, P(C) ≥ θ, P(C | A) ≥ θ, and likely C when P(C) > 1/2.

Equations

GrusdtLassiterFranke2022.Assertable θ GrusdtLassiterFranke2022.Utt.conjAC x✝ = (θ ≤ x✝.real (GrusdtLassiterFranke2022.A ∩ GrusdtLassiterFranke2022.C))
GrusdtLassiterFranke2022.Assertable θ GrusdtLassiterFranke2022.Utt.C x✝ = (θ ≤ x✝.real GrusdtLassiterFranke2022.C)
GrusdtLassiterFranke2022.Assertable θ GrusdtLassiterFranke2022.Utt.conditional x✝ = (θ ≤ x✝[|GrusdtLassiterFranke2022.A].real GrusdtLassiterFranke2022.C)
GrusdtLassiterFranke2022.Assertable θ GrusdtLassiterFranke2022.Utt.likelyC x✝ = (1 / 2 < x✝.real GrusdtLassiterFranke2022.C)

Instances For

theorem GrusdtLassiterFranke2022.real_cond (μ : MeasureTheory.Measure (Bool × Bool)) (S T : Set (Bool × Bool)) :

μ[|S].real T = μ.real (S ∩ T) / μ.real S

A conditional probability as a ratio of real masses.

Two consequences of the assertability conditions, section 5 #

Section 5.1: when antecedent and consequent are independent, the conditional is assertable only where the literal is, so an informative speaker never chooses it, and a listener who takes the two to be independent is surprised by it, the source of the infelicity of missing-link conditionals. Section 5.3: a speaker who can assert both if A then C and if not A then C could have asserted C outright.

theorem GrusdtLassiterFranke2022.assertable_C_of_indep {μ : MeasureTheory.Measure (Bool × Bool)} {t : ℝ} (hA : 0 < μ.real A) (hind : μ.real (A ∩ C) = μ.real A * μ.real C) (h : Assertable t Utt.conditional μ) :

Assertable t Utt.C μ

theorem GrusdtLassiterFranke2022.assertable_C_of_conditionals {μ : MeasureTheory.Measure (Bool × Bool)} [MeasureTheory.IsProbabilityMeasure μ] {t : ℝ} (hA : 0 < μ.real A) (hAc : 0 < μ.real A ᶜ) (h₁ : t ≤ μ[|A].real C) (h₂ : t ≤ μ[|A ᶜ].real C) :

Assertable t Utt.C μ

The toy example, section 2.3 and Table 2 #

inductive GrusdtLassiterFranke2022.State :

In the three states of Table 2(a), Alex and Chris come to the party independently in s1 and s3, and in s2 "usually not without each other".

s1 : State
s2 : State
s3 : State

Instances For

@[instance_reducible]

instance GrusdtLassiterFranke2022.instDecidableEqState :

DecidableEq State

Equations

GrusdtLassiterFranke2022.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance GrusdtLassiterFranke2022.instFintypeState :

Fintype State

Equations

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

@[instance_reducible]

instance GrusdtLassiterFranke2022.instMeasurableSpaceState :

MeasurableSpace State

Equations

GrusdtLassiterFranke2022.instMeasurableSpaceState = ⊤

instance GrusdtLassiterFranke2022.instDiscreteMeasurableSpaceState :

DiscreteMeasurableSpace State

instance GrusdtLassiterFranke2022.instNonemptyState :

Nonempty State

noncomputable def GrusdtLassiterFranke2022.State.cell :

State → Bool × Bool → NNReal

Table 2(a) gives the probability of each world (A, C) in each state.

Equations

GrusdtLassiterFranke2022.State.s1.cell (true, true) = 81 / 100
GrusdtLassiterFranke2022.State.s1.cell (true, false) = 9 / 100
GrusdtLassiterFranke2022.State.s1.cell (false, true) = 9 / 100
GrusdtLassiterFranke2022.State.s1.cell (false, false) = 1 / 100
GrusdtLassiterFranke2022.State.s2.cell (true, true) = 3 / 5
GrusdtLassiterFranke2022.State.s2.cell (true, false) = 1 / 20
GrusdtLassiterFranke2022.State.s2.cell (false, true) = 1 / 20
GrusdtLassiterFranke2022.State.s2.cell (false, false) = 3 / 10
GrusdtLassiterFranke2022.State.s3.cell (true, true) = 9 / 25
GrusdtLassiterFranke2022.State.s3.cell (true, false) = 6 / 25
GrusdtLassiterFranke2022.State.s3.cell (false, true) = 6 / 25
GrusdtLassiterFranke2022.State.s3.cell (false, false) = 4 / 25

Instances For

noncomputable def GrusdtLassiterFranke2022.State.dist (s : State) :

MeasureTheory.Measure (Bool × Bool)

A state as a probability measure on worlds.

Equations

s.dist = MeasureTheory.Measure.sum fun (w : Bool × Bool) => ↑(s.cell w) • MeasureTheory.Measure.dirac w

Instances For

theorem GrusdtLassiterFranke2022.State.dist_finset (s : State) (E : Finset (Bool × Bool)) :

s.dist ↑E = ∑ w ∈ E, ↑(s.cell w)

theorem GrusdtLassiterFranke2022.State.dist_real_finset (s : State) (E : Finset (Bool × Bool)) :

s.dist.real ↑E = ∑ w ∈ E, ↑(s.cell w)

theorem GrusdtLassiterFranke2022.State.sum_cell (s : State) :

∑ w : Bool × Bool, s.cell w = 1

instance GrusdtLassiterFranke2022.instIsProbabilityMeasureProdBoolDist (s : State) :

MeasureTheory.IsProbabilityMeasure s.dist

theorem GrusdtLassiterFranke2022.real_A (s : State) :

s.dist.real A = ↑(s.cell (true, true)) + ↑(s.cell (true, false))

theorem GrusdtLassiterFranke2022.real_C (s : State) :

s.dist.real C = ↑(s.cell (true, true)) + ↑(s.cell (false, true))

theorem GrusdtLassiterFranke2022.real_A_inter_C (s : State) :

s.dist.real (A ∩ C) = ↑(s.cell (true, true))

theorem GrusdtLassiterFranke2022.real_Ac (s : State) :

s.dist.real A ᶜ = ↑(s.cell (false, true)) + ↑(s.cell (false, false))

theorem GrusdtLassiterFranke2022.real_Ac_inter_Cc (s : State) :

s.dist.real (A ᶜ ∩ C ᶜ) = ↑(s.cell (false, false))

def GrusdtLassiterFranke2022.ext (u : Utt) :

The assertability extension of an utterance at the threshold θ.

Equations

GrusdtLassiterFranke2022.ext u = {s : GrusdtLassiterFranke2022.State | GrusdtLassiterFranke2022.Assertable GrusdtLassiterFranke2022.θ u s.dist}

Instances For

theorem GrusdtLassiterFranke2022.ext_likelyC :

ext Utt.likelyC = Set.univ

Likely C is assertable everywhere (Table 2(b)).

theorem GrusdtLassiterFranke2022.ext_conditional :

ext Utt.conditional = ↑{State.s1, State.s2}

The conditional is assertable in s1 and s2, where P(C | A) is 9/10 and 12/13, and not in s3, where it is 3/5 (Table 2(b)).

theorem GrusdtLassiterFranke2022.ext_C :

ext Utt.C = ↑{State.s1}

C is assertable in s1 only (Table 2(b)).

theorem GrusdtLassiterFranke2022.ext_conjAC :

ext Utt.conjAC = ∅

A and C is assertable nowhere (Table 2(b)).

Literal listener and speaker, Table 2(c) and (d) #

The vanilla model at α = 1 without costs, against the uniform prior over the three states: the literal listener conditions the prior on the extension, the speaker is RSA.speaker, and the pragmatic listener is the posterior of the speaker against the prior. A and C, assertable in no state, has the zero measure as its literal listener and drops out of the competition.

noncomputable def GrusdtLassiterFranke2022.prior :

MeasureTheory.Measure State

The uniform prior over the three states.

Equations

GrusdtLassiterFranke2022.prior = ProbabilityTheory.uniformOn Set.univ

Instances For

instance GrusdtLassiterFranke2022.instIsProbabilityMeasureStatePrior :

MeasureTheory.IsProbabilityMeasure prior

theorem GrusdtLassiterFranke2022.prior_singleton (s : State) :

prior {s} = 3⁻¹

theorem GrusdtLassiterFranke2022.prior_real_singleton (s : State) :

prior.real {s} = 1 / 3

noncomputable def GrusdtLassiterFranke2022.L0 :

ProbabilityTheory.Kernel Utt State

The literal listener conditions the prior on the utterance's extension.

Equations

GrusdtLassiterFranke2022.L0 = RSA.listener GrusdtLassiterFranke2022.prior (RSA.truthful GrusdtLassiterFranke2022.ext)

Instances For

instance GrusdtLassiterFranke2022.instIsFiniteKernelUttStateL0 :

ProbabilityTheory.IsFiniteKernel L0

theorem GrusdtLassiterFranke2022.L0_apply (u : Utt) :

L0 u = ProbabilityTheory.uniformOn (ext u)

The literal listener is uniform on the extension.

theorem GrusdtLassiterFranke2022.L0_real_likelyC (s : State) :

(L0 Utt.likelyC).real {s} = 1 / 3

theorem GrusdtLassiterFranke2022.L0_real_conjAC (s : State) :

(L0 Utt.conjAC).real {s} = 0

theorem GrusdtLassiterFranke2022.L0_real_conditional_s1 :

(L0 Utt.conditional).real {State.s1} = 1 / 2

theorem GrusdtLassiterFranke2022.L0_real_conditional_s2 :

(L0 Utt.conditional).real {State.s2} = 1 / 2

theorem GrusdtLassiterFranke2022.L0_real_conditional_s3 :

(L0 Utt.conditional).real {State.s3} = 0

theorem GrusdtLassiterFranke2022.L0_real_C_s1 :

(L0 Utt.C).real {State.s1} = 1

theorem GrusdtLassiterFranke2022.L0_real_C_s2 :

(L0 Utt.C).real {State.s2} = 0

theorem GrusdtLassiterFranke2022.L0_real_C_s3 :

(L0 Utt.C).real {State.s3} = 0

theorem GrusdtLassiterFranke2022.L0_ne_top (u : Utt) (s : State) :

(L0 u) {s} ≠ ⊤

noncomputable def GrusdtLassiterFranke2022.S1 :

ProbabilityTheory.Kernel State Utt

The speaker of Table 2(d) is RSA.speaker at α = 1 without costs.

Equations

GrusdtLassiterFranke2022.S1 = RSA.speaker 1 0 (⇑GrusdtLassiterFranke2022.L0) MeasureTheory.Measure.dirac

Instances For

instance GrusdtLassiterFranke2022.instIsFiniteKernelStateUttS1 :

ProbabilityTheory.IsFiniteKernel S1

theorem GrusdtLassiterFranke2022.S1_real (s : State) (u : Utt) :

(S1 s).real {u} = (L0 u).real {s} / ∑ u' : Utt, (L0 u').real {s}

theorem GrusdtLassiterFranke2022.S1_s1_C :

(S1 State.s1).real {Utt.C} = 6 / 11

In s1 the speaker says C with share 6/11, the conditional 3/11, and likely C 2/11 (Table 2(d)).

theorem GrusdtLassiterFranke2022.S1_s1_conditional :

(S1 State.s1).real {Utt.conditional} = 3 / 11

theorem GrusdtLassiterFranke2022.S1_s1_likelyC :

(S1 State.s1).real {Utt.likelyC} = 2 / 11

theorem GrusdtLassiterFranke2022.S1_s2_conditional :

(S1 State.s2).real {Utt.conditional} = 3 / 5

In s2 the speaker says the conditional with share 3/5, likely C 2/5, and C never (Table 2(d)).

theorem GrusdtLassiterFranke2022.S1_s2_likelyC :

(S1 State.s2).real {Utt.likelyC} = 2 / 5

theorem GrusdtLassiterFranke2022.S1_s2_C :

(S1 State.s2).real {Utt.C} = 0

theorem GrusdtLassiterFranke2022.S1_s3_likelyC :

(S1 State.s3).real {Utt.likelyC} = 1

In s3 the speaker says likely C with certainty (Table 2(d)).

theorem GrusdtLassiterFranke2022.S1_s3_conditional :

(S1 State.s3).real {Utt.conditional} = 0

theorem GrusdtLassiterFranke2022.S1_s3_C :

(S1 State.s3).real {Utt.C} = 0

The pragmatic listener, Table 2(e) #

noncomputable def GrusdtLassiterFranke2022.L1 :

ProbabilityTheory.Kernel Utt State

The pragmatic listener of Table 2(e) inverts S1 against the uniform prior.

Equations

GrusdtLassiterFranke2022.L1 = RSA.listener GrusdtLassiterFranke2022.prior ⇑GrusdtLassiterFranke2022.S1

Instances For

theorem GrusdtLassiterFranke2022.L1_real (u : Utt) (s : State) :

(L1 u).real {s} = (S1 s).real {u} / ∑ s' : State, (S1 s').real {u}

theorem GrusdtLassiterFranke2022.L1_conditional_s2 :

(L1 Utt.conditional).real {State.s2} = 11 / 16

Hearing the conditional, the listener puts 11/16 on s2, 5/16 on s1 and nothing on s3 (Table 2(e)).

theorem GrusdtLassiterFranke2022.L1_conditional_s1 :

(L1 Utt.conditional).real {State.s1} = 5 / 16

theorem GrusdtLassiterFranke2022.L1_conditional_s3 :

(L1 Utt.conditional).real {State.s3} = 0

theorem GrusdtLassiterFranke2022.L1_C_s1 :

(L1 Utt.C).real {State.s1} = 1

Hearing C, the listener identifies s1 (Table 2(e)).

theorem GrusdtLassiterFranke2022.L1_likelyC_s3 :

(L1 Utt.likelyC).real {State.s3} = 55 / 87

Hearing likely C, the listener puts 55/87 on s3, 22/87 on s2 and 10/87 on s1 (Table 2(e)).

theorem GrusdtLassiterFranke2022.L1_likelyC_s2 :

(L1 Utt.likelyC).real {State.s2} = 22 / 87

theorem GrusdtLassiterFranke2022.L1_likelyC_s1 :

(L1 Utt.likelyC).real {State.s1} = 10 / 87

theorem GrusdtLassiterFranke2022.l1_conditional_prefers_s2 :

(L1 Utt.conditional).real {State.s1} < (L1 Utt.conditional).real {State.s2}

Hearing if A then C, the listener prefers s2 to s1. The speaker in s1 would have said C (S1_s1_C), so the conditional signals the state where it is the most informative assertable utterance.

theorem GrusdtLassiterFranke2022.l1_likelyC_prefers_s3 :

(L1 Utt.likelyC).real {State.s1} < (L1 Utt.likelyC).real {State.s3}

Hearing likely C, the listener prefers s3 to s1, since in s1 and s2 a stronger utterance was available.

Conditional perfection #

The paper derives conditional perfection, hearing if A then C as if not A then not C, as a pragmatic inference, section 3. It is absent from the assertability semantics: at s2 the conditional is assertable while P(¬C | ¬A) = 6/7 falls short of θ.

theorem GrusdtLassiterFranke2022.perfection_not_semantic :

Assertable θ Utt.conditional State.s2.dist ∧ ¬θ ≤ State.s2.dist[|A ᶜ].real C ᶜ