Discourse State

Formalizes the discourse state model from @cite{farkas-bruce-2010} "On Reacting to Assertions and Polar Questions", which provides a unified framework for understanding how conversation advances through assertions and questions.

Key Concepts

Farkas & Bruce decompose the discourse state into five components:

Component	Description
dcS	Speaker's discourse commitments (not yet joint)
dcL	Listener's discourse commitments
cg	Common ground (joint commitments)
table	Stack of issues under discussion
ps	Projected set (derivable from cg + table)

Connection to RSA Models

Current RSA models for presupposition projection use the BeliefState slot for different components of the discourse state:

• @cite{scontras-tonhauser-2025}: BeliefState = dcS (speaker's private assumptions)
• @cite{warstadt-2022} / @cite{qing-goodman-lassiter-2016}: BeliefState = cg (common ground)

This module provides explicit types for these components, making the theoretical distinctions clear while maintaining computational compatibility with existing RSA infrastructure.

Architecture note

§ Bridge theorems (formerly Theories/Dialogue/FarkasAdapter.lean, dissolved per CLAUDE.md "no bridge files"): assertion vs acceptance properties — assert_adds_to_dcS, assert_preserves_cg, assert_not_stable, accept_adds_to_cg, accept_restores_stability.

inductive Dialogue.FarkasBruce.Participant : Type

Conversational participants.

Following Farkas & Bruce, we model two discourse roles: speaker and listener. These roles are relative to a given utterance (they can swap between turns).

• speaker : Participant
• listener : Participant

@[implicit_reducible]

instance Dialogue.FarkasBruce.instDecidableEqParticipant : DecidableEq Participant

Equations

• Dialogue.FarkasBruce.instDecidableEqParticipant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Dialogue.FarkasBruce.instReprParticipant.repr : Participant → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Dialogue.FarkasBruce.instReprParticipant : Repr Participant

Equations

• Dialogue.FarkasBruce.instReprParticipant = { reprPrec := Dialogue.FarkasBruce.instReprParticipant.repr }

def Dialogue.FarkasBruce.instInhabitedParticipant.default : Participant

Equations

• Dialogue.FarkasBruce.instInhabitedParticipant.default = Dialogue.FarkasBruce.Participant.speaker

@[implicit_reducible]

instance Dialogue.FarkasBruce.instInhabitedParticipant : Inhabited Participant

Equations

• Dialogue.FarkasBruce.instInhabitedParticipant = { default := Dialogue.FarkasBruce.instInhabitedParticipant.default }

inductive Dialogue.FarkasBruce.SentenceForm : Type

Sentence forms (clause types) that determine discourse effects.

Following Farkas & Bruce:

• Declaratives default-commit the speaker to the content
• Interrogatives raise an issue without commitment

• declarative : SentenceForm
• interrogative : SentenceForm

@[implicit_reducible]

instance Dialogue.FarkasBruce.instDecidableEqSentenceForm : DecidableEq SentenceForm

Equations

• Dialogue.FarkasBruce.instDecidableEqSentenceForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Dialogue.FarkasBruce.instReprSentenceForm : Repr SentenceForm

Equations

• Dialogue.FarkasBruce.instReprSentenceForm = { reprPrec := Dialogue.FarkasBruce.instReprSentenceForm.repr }

def Dialogue.FarkasBruce.instReprSentenceForm.repr : SentenceForm → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Dialogue.FarkasBruce.instInhabitedSentenceForm : Inhabited SentenceForm

Equations

• Dialogue.FarkasBruce.instInhabitedSentenceForm = { default := Dialogue.FarkasBruce.instInhabitedSentenceForm.default }

def Dialogue.FarkasBruce.instInhabitedSentenceForm.default : SentenceForm

Equations

• Dialogue.FarkasBruce.instInhabitedSentenceForm.default = Dialogue.FarkasBruce.SentenceForm.declarative

structure Dialogue.FarkasBruce.RaisedIssue (W : Type u_1) : Type u_1

An issue on the conversational table.

In Farkas & Bruce's model, the table is a stack of issues that need to be resolved before the conversation can return to a stable state.

For polar questions, alternatives is [p, ¬p]. For wh-questions, alternatives is the set of possible answers.

• form : SentenceForm

  The form of the sentence that raised this issue

• alternatives : List (Set W)

  The proposition(s) at issue

• source : Participant

  Who raised this issue

structure Dialogue.FarkasBruce.DiscourseState (W : Type u_1) : Type u_1

Discourse State following @cite{farkas-bruce-2010}.

This structure captures the conversational state at a given point in time. It's parameterized by the World type for type-safe propositions.

Note: We omit ps (projected set) because it's derivable from cg and table. The projected set contains worlds compatible with cg and at least one complete answer to each issue on the table.

• dcS : List (Set W)

  Speaker's discourse commitments (what speaker takes for granted)

• dcL : List (Set W)

  Listener's discourse commitments

• cg : List (Set W)

  Common ground (joint commitments)

• table : List (RaisedIssue W)

  The table: stack of issues under discussion

def Dialogue.FarkasBruce.DiscourseState.empty {W : Type u_1} : DiscourseState W

Empty/initial discourse state.

At the start of a conversation, there are no commitments and no issues on the table. This is a "stable" state in F&B's terminology.

Equations

• Dialogue.FarkasBruce.DiscourseState.empty = { dcS := [], dcL := [], cg := [], table := [] }

def Dialogue.FarkasBruce.DiscourseState.toContextSet {W : Type u_1} (ds : DiscourseState W) : Core.CommonGround.ContextSet W

Convert common ground to a ContextSet (worlds where all cg props hold).

Bridges to the existing Core.CommonGround infrastructure as the fold-intersection of the cg list.

Equations

• ds.toContextSet = List.foldr (fun (x1 x2 : Core.CommonGround.ContextSet W) => x1 ∩ x2) Set.univ ds.cg

def Dialogue.FarkasBruce.DiscourseState.compatible {W : Type u_1} (ds : DiscourseState W) (w : W) : Prop

World compatibility: thin alias for membership in toContextSet.

Equations

• ds.compatible w = (w ∈ ds.toContextSet)

def Dialogue.FarkasBruce.DiscourseState.isStable {W : Type u_1} (ds : DiscourseState W) : Prop

Check if the table is empty (stable state).

A discourse state is stable when the table is empty, meaning all issues have been resolved and there's nothing pending.

Equations

• ds.isStable = (ds.table.length = 0)

@[implicit_reducible]

instance Dialogue.FarkasBruce.DiscourseState.instDecidableIsStable {W : Type u_1} (ds : DiscourseState W) : Decidable ds.isStable

Equations

• ds.instDecidableIsStable = Dialogue.FarkasBruce.DiscourseState.instDecidableIsStable._aux_1 ds

def Dialogue.FarkasBruce.DiscourseState.speakerCompatible {W : Type u_1} (ds : DiscourseState W) (w : W) : Prop

Check if a world is compatible with speaker's commitments.

This is what @cite{scontras-tonhauser-2025} call "speakerCredence": the speaker only considers worlds compatible with their private assumptions.

Equations

• ds.speakerCompatible w = ∀ p ∈ ds.dcS, p w

def Dialogue.FarkasBruce.DiscourseState.listenerCompatible {W : Type u_1} (ds : DiscourseState W) (w : W) : Prop

Check if a world is compatible with listener's commitments.

Equations

• ds.listenerCompatible w = ∀ p ∈ ds.dcL, p w

def Dialogue.FarkasBruce.DiscourseState.addToCG {W : Type u_1} (ds : DiscourseState W) (p : Set W) : DiscourseState W

Add a proposition to the common ground.

This models acceptance of an assertion: the proposition moves from a participant's discourse commitments to the joint common ground.

Equations

• ds.addToCG p = { dcS := ds.dcS, dcL := ds.dcL, cg := p :: ds.cg, table := ds.table }

def Dialogue.FarkasBruce.DiscourseState.addToDcS {W : Type u_1} (ds : DiscourseState W) (p : Set W) : DiscourseState W

Add a proposition to speaker's discourse commitments.

This models the speaker asserting a proposition, which commits the speaker but doesn't yet affect the common ground.

Equations

• ds.addToDcS p = { dcS := p :: ds.dcS, dcL := ds.dcL, cg := ds.cg, table := ds.table }

def Dialogue.FarkasBruce.DiscourseState.addToDcL {W : Type u_1} (ds : DiscourseState W) (p : Set W) : DiscourseState W

Add a proposition to listener's discourse commitments.

Equations

• ds.addToDcL p = { dcS := ds.dcS, dcL := p :: ds.dcL, cg := ds.cg, table := ds.table }

def Dialogue.FarkasBruce.DiscourseState.pushIssue {W : Type u_1} (ds : DiscourseState W) (issue : RaisedIssue W) : DiscourseState W

Push an issue onto the table.

This models raising a question or making an assertion (which implicitly raises the issue of whether the content should be accepted).

Equations

• ds.pushIssue issue = { dcS := ds.dcS, dcL := ds.dcL, cg := ds.cg, table := issue :: ds.table }

def Dialogue.FarkasBruce.DiscourseState.popIssue {W : Type u_1} (ds : DiscourseState W) : DiscourseState W

Pop an issue from the table (when resolved).

Equations

• ds.popIssue = { dcS := ds.dcS, dcL := ds.dcL, cg := ds.cg, table := ds.table.tail }

def Dialogue.FarkasBruce.DiscourseState.assertDeclarative {W : Type u_1} (ds : DiscourseState W) (p : Set W) : DiscourseState W

Effect of a declarative assertion.

Following F&B: an assertion of p by the speaker:

1. Adds p to dcS (speaker's commitments)
2. Pushes the issue {p} onto the table

The listener can then respond by:

• Accepting (adds p to dcL and cg, pops table)
• Rejecting (adds ¬p to dcL, creating a conflict)
• Neither (leaving p "on the table")

Equations

• ds.assertDeclarative p = (ds.addToDcS p).pushIssue { form := Dialogue.FarkasBruce.SentenceForm.declarative, alternatives := [p] }

def Dialogue.FarkasBruce.DiscourseState.askPolarQuestion {W : Type u_1} (ds : DiscourseState W) (p : Set W) : DiscourseState W

Effect of a polar question.

Following F&B: a polar question about p:

1. Pushes the issue {p, ¬p} onto the table
2. Does not add commitments (questions don't commit)

Equations

• ds.askPolarQuestion p = ds.pushIssue { form := Dialogue.FarkasBruce.SentenceForm.interrogative, alternatives := [p, pᶜ] }

def Dialogue.FarkasBruce.DiscourseState.acceptTop {W : Type u_1} (ds : DiscourseState W) : DiscourseState W

Accept the top issue on the table.

This models the listener accepting an assertion (adding to dcL and cg) or answering a question (adding the chosen alternative to cg).

Equations

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

def Dialogue.FarkasBruce.DiscourseState.toCG {W : Type u_1} (ds : DiscourseState W) : Core.CommonGround.CG W

Convert the common ground component to a CG structure.

Equations

• ds.toCG = { propositions := ds.cg }

def Dialogue.FarkasBruce.DiscourseState.fromCG {W : Type u_1} (cg : Core.CommonGround.CG W) : DiscourseState W

Create a discourse state from a CG structure.

Sets cg, dcS, and dcL all to the CG propositions (everyone agrees).

Equations

• Dialogue.FarkasBruce.DiscourseState.fromCG cg = { dcS := cg.propositions, dcL := cg.propositions, cg := cg.propositions, table := [] }

Connection to RSA Presupposition Models

@cite{scontras-tonhauser-2025} @cite{warstadt-2022} @cite{qing-goodman-lassiter-2016}

RSA models for presupposition projection use different components of the discourse state as the latent variable that L1 infers:

@cite{scontras-tonhauser-2025}: Inferring dcS

The BeliefState type represents different possible values of dcS (what the speaker privately assumes). L1 infers which dcS best explains the speaker's utterance choice.

The speaker may assume things not yet in the common ground, which is why S&T prefer "private assumptions" over "common ground."

@cite{warstadt-2022} / @cite{qing-goodman-lassiter-2016}: Inferring cg

The Context type represents different possible values of cg (what's jointly accepted). L1 infers which cg state the speaker is acting on.

Accommodation is updating one's model of the common ground.

Assertion-vs-acceptance properties for assertDeclarative and acceptTop. These were previously hosted in a separate FarkasAdapter.lean "bridge file"; CLAUDE.md prohibits bridge files, so the content lives here alongside the operators it characterizes.

theorem Dialogue.FarkasBruce.DiscourseState.assert_adds_to_dcS {W : Type u_1} (ds : DiscourseState W) (p : Set W) : (ds.assertDeclarative p).dcS = p :: ds.dcS

Assertion adds to dcS, not directly to cg. This is the key F&B insight: assertion first commits the speaker, then the listener can accept (moving to cg) or reject.

theorem Dialogue.FarkasBruce.DiscourseState.assert_preserves_cg {W : Type u_1} (ds : DiscourseState W) (p : Set W) : (ds.assertDeclarative p).cg = ds.cg

Assertion does not immediately change the common ground.

theorem Dialogue.FarkasBruce.DiscourseState.assert_not_stable {W : Type u_1} (ds : DiscourseState W) (p : Set W) : ¬(ds.assertDeclarative p).isStable

Assertion is not stable: it pushes an issue onto the table.

theorem Dialogue.FarkasBruce.DiscourseState.accept_adds_to_cg {W : Type u_1} (ds : DiscourseState W) (p : Set W) : (ds.assertDeclarative p).acceptTop.cg = p :: ds.cg

Acceptance moves the proposition to the common ground.

theorem Dialogue.FarkasBruce.DiscourseState.accept_restores_stability {W : Type u_1} (ds : DiscourseState W) (p : Set W) (hStable : ds.isStable) : (ds.assertDeclarative p).acceptTop.isStable

After acceptance, the state returns to stable (table is popped).

@[implicit_reducible]

instance Dialogue.FarkasBruce.instHasContextSetDiscourseState {W : Type u_1} : Core.CommonGround.HasContextSet (DiscourseState W) W

F&B states project to a context set via cg-only intersection (toContextSet). Note: this projection deliberately ignores dcS/dcL and table — F&B's whole point is that assertion operates on those layers without (yet) reaching cg. As a consequence, F&B does NOT instantiate Assertable (assertion doesn't narrow the projected context set in one step). See the Assertable.lean module docstring.

Equations

• Dialogue.FarkasBruce.instHasContextSetDiscourseState = { toContextSet := Dialogue.FarkasBruce.DiscourseState.toContextSet }