inductive Semantics.Dynamic.State.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

instance Semantics.Dynamic.State.instDecidableEqParticipant : DecidableEq Participant

Equations

• Semantics.Dynamic.State.instDecidableEqParticipant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Dynamic.State.instReprParticipant : Repr Participant

Equations

• Semantics.Dynamic.State.instReprParticipant = { reprPrec := Semantics.Dynamic.State.instReprParticipant.repr }

def Semantics.Dynamic.State.instReprParticipant.repr : Participant → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.State.instBEqParticipant : BEq Participant

Equations

• Semantics.Dynamic.State.instBEqParticipant = { beq := Semantics.Dynamic.State.instBEqParticipant.beq }

def Semantics.Dynamic.State.instBEqParticipant.beq : Participant → Participant → Bool

Equations

• Semantics.Dynamic.State.instBEqParticipant.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Dynamic.State.instInhabitedParticipant : Inhabited Participant

Equations

• Semantics.Dynamic.State.instInhabitedParticipant = { default := Semantics.Dynamic.State.instInhabitedParticipant.default }

def Semantics.Dynamic.State.instInhabitedParticipant.default : Participant

Equations

• Semantics.Dynamic.State.instInhabitedParticipant.default = Semantics.Dynamic.State.Participant.speaker

inductive Semantics.Dynamic.State.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

instance Semantics.Dynamic.State.instDecidableEqSentenceForm : DecidableEq SentenceForm

Equations

• Semantics.Dynamic.State.instDecidableEqSentenceForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Dynamic.State.instReprSentenceForm : Repr SentenceForm

Equations

• Semantics.Dynamic.State.instReprSentenceForm = { reprPrec := Semantics.Dynamic.State.instReprSentenceForm.repr }

def Semantics.Dynamic.State.instReprSentenceForm.repr : SentenceForm → ℕ → Std.Format

Equations

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

def Semantics.Dynamic.State.instBEqSentenceForm.beq : SentenceForm → SentenceForm → Bool

Equations

• Semantics.Dynamic.State.instBEqSentenceForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Dynamic.State.instBEqSentenceForm : BEq SentenceForm

Equations

• Semantics.Dynamic.State.instBEqSentenceForm = { beq := Semantics.Dynamic.State.instBEqSentenceForm.beq }

instance Semantics.Dynamic.State.instInhabitedSentenceForm : Inhabited SentenceForm

Equations

• Semantics.Dynamic.State.instInhabitedSentenceForm = { default := Semantics.Dynamic.State.instInhabitedSentenceForm.default }

def Semantics.Dynamic.State.instInhabitedSentenceForm.default : SentenceForm

Equations

• Semantics.Dynamic.State.instInhabitedSentenceForm.default = Semantics.Dynamic.State.SentenceForm.declarative

structure Semantics.Dynamic.State.Issue (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 (BProp W)

  The proposition(s) at issue

• source : Participant

  Who raised this issue

structure Semantics.Dynamic.State.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 (BProp W)

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

• dcL : List (BProp W)

  Listener's discourse commitments

• cg : List (BProp W)

  Common ground (joint commitments)

• table : List (Issue W)

  The table: stack of issues under discussion

def Semantics.Dynamic.State.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

• Semantics.Dynamic.State.DiscourseState.empty = { dcS := [], dcL := [], cg := [], table := [] }

def Semantics.Dynamic.State.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).

This bridges to the existing Core.CommonGround infrastructure.

Equations

• ds.toContextSet w = ((ds.cg.all fun (p : BProp W) => p w) = true)

def Semantics.Dynamic.State.DiscourseState.compatible {W : Type u_1} (ds : DiscourseState W) (w : W) : Bool

World compatibility: w is compatible with the discourse state if w satisfies all common ground propositions.

Equations

• ds.compatible w = ds.cg.all fun (p : BProp W) => p w

def Semantics.Dynamic.State.DiscourseState.isStable {W : Type u_1} (ds : DiscourseState W) : Bool

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.isEmpty

def Semantics.Dynamic.State.DiscourseState.speakerCompatible {W : Type u_1} (ds : DiscourseState W) (w : W) : Bool

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 = ds.dcS.all fun (p : BProp W) => p w

def Semantics.Dynamic.State.DiscourseState.listenerCompatible {W : Type u_1} (ds : DiscourseState W) (w : W) : Bool

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

Equations

• ds.listenerCompatible w = ds.dcL.all fun (p : BProp W) => p w

def Semantics.Dynamic.State.DiscourseState.addToCG {W : Type u_1} (ds : DiscourseState W) (p : BProp 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 Semantics.Dynamic.State.DiscourseState.addToDcS {W : Type u_1} (ds : DiscourseState W) (p : BProp 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 Semantics.Dynamic.State.DiscourseState.addToDcL {W : Type u_1} (ds : DiscourseState W) (p : BProp 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 Semantics.Dynamic.State.DiscourseState.pushIssue {W : Type u_1} (ds : DiscourseState W) (issue : Issue 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 Semantics.Dynamic.State.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 Semantics.Dynamic.State.DiscourseState.assertDeclarative {W : Type u_1} (ds : DiscourseState W) (p : BProp 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 := Semantics.Dynamic.State.SentenceForm.declarative, alternatives := [p] }

def Semantics.Dynamic.State.DiscourseState.askPolarQuestion {W : Type u_1} (ds : DiscourseState W) (p : BProp 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 := Semantics.Dynamic.State.SentenceForm.interrogative, alternatives := [p, Core.Proposition.Decidable.pnot W p] }

def Semantics.Dynamic.State.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 Semantics.Dynamic.State.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 Semantics.Dynamic.State.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

• Semantics.Dynamic.State.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.