KOS Conversational Rules

@cite{ginzburg-2012} Ch. 4

Conversational rules govern how dialogue gameboards evolve during conversation. @cite{ginzburg-2012} Ch. 4 defines these as precondition/effect pairs (record types with pre and effects fields).

Core Rules (@cite{ginzburg-2012} Ch. 4, pp. 72–112)

1. Greeting / CounterGreeting — conversation initialization (pp. 74–76, ex. 17/20b)
2. Initiating Move — refined Free Speech with genre relevance (p. 108, ex. 94)
3. Ask QUD-incrementation — question pushes onto QUD (p. 95, ex. 66)
4. Assert QUD-incrementation — assertion pushes About(p) onto QUD (p. 95, ex. 66)
5. QSPEC — subquestion accommodation (p. 95, ex. 66)
6. QCoord — successive question coordination (p. 99, ex. 77)
7. Accept — addressee grounds an assertion (p. 95, ex. 66)
8. Check — addressee requests confirmation (p. 95, ex. 68)
9. Confirm — speaker confirms in response to check (p. 95, ex. 68)
10. Fact update/QUD-downdate — accept triggers fact addition + QUD removal (p. 95; p. 103, ex. 85)

Answerhood

The Answerhood typeclass abstracts the resolves-relation between facts and questions — connecting to partition-based QUD W from Core/Discourse/QUD.lean and to inquisitive Issue W.

Genre (@cite{ginzburg-2012} §4.6)

Genres are TTR record types classifying conversations by their characteristic structure. Activity relevance (GenreRelevant, p. 105, ex. 90) constrains which initiating moves are felicitous.

class Theories.Pragmatics.Dialogue.KOS.Answerhood (Fact QContent : Type) : Type

Whether a fact resolves a question.

This abstracts the answerhood relation between accumulated facts and QUD entries. Concrete instances connect to:

• Partition-based answerhood (QUD M): a fact determines a unique cell
• String-based answerhood: pattern matching on content strings
• Propositional answerhood (BProp W): a fact entails a question's answer

Ch. 4: "q is resolved relative to a DGB dgb iff the FACTS in dgb contextually entail an answer to q."

• resolves : Fact → QContent → Bool

def Theories.Pragmatics.Dialogue.KOS.allResolved {Fact QContent : Type} [Answerhood Fact QContent] (facts : List Fact) (qud : List QContent) : Bool

Whether all questions in a QUD stack are resolved by the current facts.

Equations

• Theories.Pragmatics.Dialogue.KOS.allResolved facts qud = qud.all fun (q : QContent) => facts.any fun (f : Fact) => Theories.Pragmatics.Dialogue.KOS.Answerhood.resolves f q

def Theories.Pragmatics.Dialogue.KOS.DGB.pushQud {P Fact QContent : Type} (dgb : DGB P Fact QContent) (q : QContent) : DGB P Fact QContent

Push a question onto the QUD stack.

Ch. 4: when a question is asked, it becomes the maximal element of QUD.

Equations

• dgb.pushQud q = { spkr := dgb.spkr, addr := dgb.addr, facts := dgb.facts, moves := dgb.moves, pending := dgb.pending, qud := q :: dgb.qud }

def Theories.Pragmatics.Dialogue.KOS.DGB.downdateQud {P Fact QContent : Type} [Answerhood Fact QContent] (dgb : DGB P Fact QContent) : DGB P Fact QContent

Remove resolved questions from QUD.

Ch. 4: QUD-downdate removes a question q from QUD when FACTS contextually entail an answer to q.

Equations

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

def Theories.Pragmatics.Dialogue.KOS.DGB.addFact {P Fact QContent : Type} (dgb : DGB P Fact QContent) (p : Fact) : DGB P Fact QContent

Add a fact to the DGB's FACTS.

Equations

• dgb.addFact p = { spkr := dgb.spkr, addr := dgb.addr, facts := p :: dgb.facts, moves := dgb.moves, pending := dgb.pending, qud := dgb.qud }

def Theories.Pragmatics.Dialogue.KOS.DGB.recordMove {P Fact QContent : Type} (dgb : DGB P Fact QContent) (m : IllocMove Fact QContent) : DGB P Fact QContent

Record a move in the DGB's MOVES list.

Equations

• dgb.recordMove m = { spkr := dgb.spkr, addr := dgb.addr, facts := dgb.facts, moves := dgb.moves ++ [m], pending := dgb.pending, qud := dgb.qud }

def Theories.Pragmatics.Dialogue.KOS.DGB.assertFact {P Fact QContent : Type} [Answerhood Fact QContent] (dgb : DGB P Fact QContent) (p : Fact) : DGB P Fact QContent

Assert: add fact to FACTS, record the move, and downdate QUD.

Ch. 4 (p. 95, ex. 66): assertion adds content to FACTS, pushes About(p,?) onto QUD, and any resolved question is removed.

Equations

• dgb.assertFact p = (dgb.addFact p).downdateQud

def Theories.Pragmatics.Dialogue.KOS.TIS.ask {P Fact QContent : Type} (tis : TIS P Fact QContent) (q : QContent) : TIS P Fact QContent

Ask rule: a question utterance pushes onto QUD and records the move.

Ch. 4, "Ask QUD-incrementation" (p. 95, ex. 66).

Equations

• tis.ask q = { dgb := (tis.dgb.pushQud q).recordMove (Theories.Pragmatics.Dialogue.KOS.IllocMove.ask q), private_ := tis.private_ }

def Theories.Pragmatics.Dialogue.KOS.TIS.assertRule {P Fact QContent : Type} [Answerhood Fact QContent] (tis : TIS P Fact QContent) (p : Fact) : TIS P Fact QContent

Assert rule (simplified): assertion adds to FACTS and downdates.

This version does not push About(p) onto QUD. For the full Assert protocol with QUD-incrementation, use TIS.assertWithQUD.

Equations

• tis.assertRule p = { dgb := (tis.dgb.assertFact p).recordMove (Theories.Pragmatics.Dialogue.KOS.IllocMove.assert p), private_ := tis.private_ }

def Theories.Pragmatics.Dialogue.KOS.TIS.assertWithQUD {P Fact QContent : Type} [Answerhood Fact QContent] (tis : TIS P Fact QContent) (p : Fact) (aboutP : QContent) : TIS P Fact QContent

Assert QUD-incrementation: the full Assert protocol.

Ch. 4 (p. 95, ex. 66): when A asserts p:

1. p is added to FACTS
2. About(p) — a polar question "whether p" — is pushed onto QUD
3. QUD is downdated (resolved questions removed)

The aboutP parameter converts the asserted fact to its corresponding question, since this conversion is domain-specific.

Equations

• tis.assertWithQUD p aboutP = { dgb := ((tis.dgb.addFact p).pushQud aboutP).downdateQud.recordMove (Theories.Pragmatics.Dialogue.KOS.IllocMove.assert p), private_ := tis.private_ }

def Theories.Pragmatics.Dialogue.KOS.TIS.accept {P Fact QContent : Type} (tis : TIS P Fact QContent) (p : Fact) : TIS P Fact QContent

Accept rule: addressee grounds an assertion — adds fact to own FACTS.

Ch. 4, "Accept" (p. 95, ex. 66 step 4a).

Known simplification: the book's Accept rule (ex. 42) swaps spkr/addr in the effects (the acceptor becomes the new speaker). We don't model this because our worked examples don't track individual participants.

Equations

• tis.accept p = { dgb := (tis.dgb.addFact p).recordMove (Theories.Pragmatics.Dialogue.KOS.IllocMove.accept p), private_ := tis.private_ }

def Theories.Pragmatics.Dialogue.KOS.TIS.qspec {P Fact QContent : Type} (tis : TIS P Fact QContent) (q : QContent) : TIS P Fact QContent

QSPEC rule: a subquestion refines a QUD entry.

Precondition: q₂ influences some q₁ on QUD (q₂ is a subquestion). Effect: push q₂ onto QUD (it becomes the new MaxQud).

Ch. 4, "QSPEC" (p. 95, ex. 66 step 2).

Equations

• tis.qspec q = { dgb := (tis.dgb.pushQud q).recordMove (Theories.Pragmatics.Dialogue.KOS.IllocMove.ask q), private_ := tis.private_ }

def Theories.Pragmatics.Dialogue.KOS.TIS.check {P Fact QContent : Type} (tis : TIS P Fact QContent) (p : Fact) (aboutP : QContent) : TIS P Fact QContent

Check rule: addressee requests confirmation of an assertion.

Ch. 4 (p. 95, ex. 68): a Check move pushes a polar question about the asserted content onto QUD.

Equations

• tis.check p aboutP = { dgb := (tis.dgb.pushQud aboutP).recordMove (Theories.Pragmatics.Dialogue.KOS.IllocMove.check p), private_ := tis.private_ }

def Theories.Pragmatics.Dialogue.KOS.TIS.confirm {P Fact QContent : Type} [Answerhood Fact QContent] (tis : TIS P Fact QContent) (p : Fact) : TIS P Fact QContent

Confirm rule: speaker confirms in response to a check.

Ch. 4 (p. 95, ex. 68 step 2).

Known simplification: the book's Confirm rule (ex. 43) swaps spkr/addr, as with Accept. See TIS.accept for details.

Equations

• tis.confirm p = { dgb := (tis.dgb.assertFact p).recordMove (Theories.Pragmatics.Dialogue.KOS.IllocMove.confirm p), private_ := tis.private_ }

def Theories.Pragmatics.Dialogue.KOS.TIS.qcoord {P Fact QContent : Type} (tis : TIS P Fact QContent) (q : QContent) : TIS P Fact QContent

QCoord rule: successive question coordination.

Ch. 4, ex. 77 (p. 99): allows a speaker to follow up an initial question with a non-influencing question, where the initial question remains QUD-maximal.

Effect: push q onto QUD without displacing the current maximal question.

Equations

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

def Theories.Pragmatics.Dialogue.KOS.TIS.factUpdateQudDowndate {P Fact QContent : Type} [Answerhood Fact QContent] (tis : TIS P Fact QContent) (p : Fact) : TIS P Fact QContent

Fact update/QUD-downdate: combined rule.

Ch. 4, ex. 85 (p. 103): when Accept occurs, FACTS is updated and resolved questions are downdated from QUD.

Equations

• tis.factUpdateQudDowndate p = { dgb := (tis.dgb.addFact p).downdateQud, private_ := tis.private_ }

def Theories.Pragmatics.Dialogue.KOS.TIS.greet {P Fact QContent : Type} (tis : TIS P Fact QContent) : TIS P Fact QContent

Greeting: conversation initialization.

Ch. 4 (p. 75, ex. 17): precondition is MOVES = ⟨⟩.

Equations

• tis.greet = { dgb := tis.dgb.recordMove Theories.Pragmatics.Dialogue.KOS.IllocMove.greet, private_ := tis.private_ }

theorem Theories.Pragmatics.Dialogue.KOS.ask_pushes_qud {P Fact QContent : Type} (tis : TIS P Fact QContent) (q : QContent) : (tis.ask q).dgb.qud = q :: tis.dgb.qud

Ask pushes exactly one question onto QUD.

theorem Theories.Pragmatics.Dialogue.KOS.ask_preserves_facts {P Fact QContent : Type} (tis : TIS P Fact QContent) (q : QContent) : (tis.ask q).dgb.facts = tis.dgb.facts

Ask does not modify FACTS.

theorem Theories.Pragmatics.Dialogue.KOS.ask_records_move {P Fact QContent : Type} (tis : TIS P Fact QContent) (q : QContent) : (tis.ask q).dgb.moves = tis.dgb.moves ++ [IllocMove.ask q]

Ask records the move.

theorem Theories.Pragmatics.Dialogue.KOS.assert_adds_fact {P Fact QContent : Type} [Answerhood Fact QContent] (tis : TIS P Fact QContent) (p : Fact) : p ∈ (tis.assertRule p).dgb.facts

Assert adds the fact to FACTS.

theorem Theories.Pragmatics.Dialogue.KOS.assertWithQUD_adds_fact {P Fact QContent : Type} [Answerhood Fact QContent] (tis : TIS P Fact QContent) (p : Fact) (aboutP : QContent) : p ∈ (tis.assertWithQUD p aboutP).dgb.facts

assertWithQUD adds the fact to FACTS.

theorem Theories.Pragmatics.Dialogue.KOS.accept_preserves_qud {P Fact QContent : Type} (tis : TIS P Fact QContent) (p : Fact) : (tis.accept p).dgb.qud = tis.dgb.qud

Accept adds a fact without changing QUD.

theorem Theories.Pragmatics.Dialogue.KOS.accept_adds_fact {P Fact QContent : Type} (tis : TIS P Fact QContent) (p : Fact) : (tis.accept p).dgb.facts = p :: tis.dgb.facts

Accept adds the fact to FACTS.

theorem Theories.Pragmatics.Dialogue.KOS.qspec_pushes {P Fact QContent : Type} (tis : TIS P Fact QContent) (q : QContent) : (tis.qspec q).dgb.qud = q :: tis.dgb.qud

QSPEC pushes a subquestion.

theorem Theories.Pragmatics.Dialogue.KOS.check_pushes_qud {P Fact QContent : Type} (tis : TIS P Fact QContent) (p : Fact) (aboutP : QContent) : (tis.check p aboutP).dgb.qud = aboutP :: tis.dgb.qud

Check pushes a question onto QUD.

theorem Theories.Pragmatics.Dialogue.KOS.greet_precond_empty_moves {P Fact QContent : Type} (tis : TIS P Fact QContent) (h : tis.dgb.moves = []) : tis.greet.dgb.moves = [IllocMove.greet]

Greeting requires empty moves (precondition check).

theorem Theories.Pragmatics.Dialogue.KOS.downdateQud_length_le {P Fact QContent : Type} [Answerhood Fact QContent] (dgb : DGB P Fact QContent) : dgb.downdateQud.qud.length ≤ dgb.qud.length

Downdate never increases QUD size.

theorem Theories.Pragmatics.Dialogue.KOS.downdateQud_removes_resolved {P Fact QContent : Type} [Answerhood Fact QContent] (dgb : DGB P Fact QContent) (q : QContent) (f : Fact) (hq : dgb.qud = [q]) (hf : f ∈ dgb.facts) (hr : Answerhood.resolves f q = true) : dgb.downdateQud.qud = []

If a fact resolves the only question on QUD, downdate removes it.

Move Coherence

ex. 70 (p. 96) defines M(ove)-Coherence: a move m₁ is coherent with respect to a DGB dgb₀ iff there exists a conversational rule c₁ mapping dgb₀ to dgb₁ such that dgb₁.LatestMove = m₁.

Pairwise and sequential M-Coherence extend this to move pairs and sequences.

@[reducible, inline]

abbrev Theories.Pragmatics.Dialogue.KOS.ConvRule (P Fact QContent : Type) : Type

A conversational rule: a function from DGB to DGB.

Ch. 4 summary (p. 112): "a mapping that indicates how one DGB can be modified by a conversationally related action."

Equations

• Theories.Pragmatics.Dialogue.KOS.ConvRule P Fact QContent = (Theories.Pragmatics.Dialogue.KOS.DGB P Fact QContent → Theories.Pragmatics.Dialogue.KOS.DGB P Fact QContent)

def Theories.Pragmatics.Dialogue.KOS.mCoherent {P Fact QContent : Type} (rules : List (ConvRule P Fact QContent)) (dgb₀ : DGB P Fact QContent) (m : IllocMove Fact QContent) : Prop

A move is M-Coherent with respect to a DGB if some conversational rule produces a DGB whose latest move is that move.

ex. 70a (p. 96).

Equations

• Theories.Pragmatics.Dialogue.KOS.mCoherent rules dgb₀ m = ∃ rule ∈ rules, (rule dgb₀).latestMove = some m

def Theories.Pragmatics.Dialogue.KOS.genreRelevant {P Fact QContent : Type} (genre : GenreType QContent) (dgb : DGB P Fact QContent) (m : IllocMove Fact QContent) : Bool

A move is genre-relevant if the outcome of adding it to the DGB can be anticipated to conclude as a conversation of the genre type.

ex. 90 (p. 105): "m0 is relevant to G0 in dgb0 for A iff A believes that outcome(dgb0 ⊕ₘₒᵥₑₛ m0, G0) will be fulfilled."

Equations

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

instance Theories.Pragmatics.Dialogue.KOS.instAnswerhoodString : Answerhood String String

String-based answerhood: a fact resolves a question if they match.

Equations

• Theories.Pragmatics.Dialogue.KOS.instAnswerhoodString = { resolves := fun (fact question : String) => fact == question }

theorem Theories.Pragmatics.Dialogue.KOS.inquiry_step1_qud : Theories.Pragmatics.Dialogue.KOS.tis₁✝.dgb.qud = ["Bo is here"]

After Ask, QUD contains the question.

theorem Theories.Pragmatics.Dialogue.KOS.inquiry_step1_facts : Theories.Pragmatics.Dialogue.KOS.tis₁✝.dgb.facts = []

After Ask, FACTS are unchanged.

theorem Theories.Pragmatics.Dialogue.KOS.inquiry_step1_moves : Theories.Pragmatics.Dialogue.KOS.tis₁✝.dgb.moves = [IllocMove.ask "Bo is here"]

After Ask, the move is recorded.

theorem Theories.Pragmatics.Dialogue.KOS.inquiry_step2_has_fact : "Bo is here" ∈ Theories.Pragmatics.Dialogue.KOS.tis₂✝.dgb.facts

After Assert, the fact is in FACTS.

theorem Theories.Pragmatics.Dialogue.KOS.inquiry_step2_qud_empty : Theories.Pragmatics.Dialogue.KOS.tis₂✝.dgb.qud = []

After Assert, QUD is empty (the question was resolved).

theorem Theories.Pragmatics.Dialogue.KOS.inquiry_step3_facts : Theories.Pragmatics.Dialogue.KOS.tis₃✝.dgb.facts = ["Bo is here", "Bo is here"]

After Accept, the fact appears twice (once from assert, once from accept).

theorem Theories.Pragmatics.Dialogue.KOS.inquiry_cycle_qud : Theories.Pragmatics.Dialogue.KOS.tis₀✝.dgb.qud = [] ∧ Theories.Pragmatics.Dialogue.KOS.tis₁✝.dgb.qud = ["Bo is here"] ∧ Theories.Pragmatics.Dialogue.KOS.tis₂✝.dgb.qud = []

The full inquiry cycle: QUD starts empty, gets a question, then empties.

theorem Theories.Pragmatics.Dialogue.KOS.inquiry_cycle_moves : Theories.Pragmatics.Dialogue.KOS.tis₃✝.dgb.moves = [IllocMove.ask "Bo is here", IllocMove.assert "Bo is here", IllocMove.accept "Bo is here"]

Moves accumulate through the inquiry cycle.

instance Theories.Pragmatics.Dialogue.KOS.instAnswerhoodString_1 : Answerhood String String

Equations

• Theories.Pragmatics.Dialogue.KOS.instAnswerhoodString_1 = { resolves := fun (fact question : String) => fact == question }

theorem Theories.Pragmatics.Dialogue.KOS.check_pushes : Theories.Pragmatics.Dialogue.KOS.checkTIS₂✝.dgb.qud = ["Bo is in Essen"]

After Check, QUD has the polar question.

theorem Theories.Pragmatics.Dialogue.KOS.confirm_resolves : Theories.Pragmatics.Dialogue.KOS.checkTIS₃✝.dgb.qud = []

After Confirm, the fact is in FACTS and QUD is resolved.

Partition-Based Answerhood

Ch. 4 defines QUD-downdate in terms of FACTS resolving questions. The Answerhood typeclass above abstracts this. Here we connect it to the partition-based QUD W from Core/Discourse/QUD.lean (@cite{groenendijk-stokhof-1984}):

A BProp W fact resolves a QUD W question when the fact determines a unique cell — all worlds where the fact holds are in the same partition cell.

def Theories.Pragmatics.Dialogue.KOS.bpropResolvesQUD {W : Type} [BEq W] (worlds : List W) (fact : BProp W) (q : QUD W) : Bool

A BProp W resolves a QUD W if all fact-worlds are in the same partition cell.

Equations

• Theories.Pragmatics.Dialogue.KOS.bpropResolvesQUD worlds fact q = (List.filter fact worlds).all fun (w₁ : W) => (List.filter fact worlds).all fun (w₂ : W) => q.sameAnswer w₁ w₂

def Theories.Pragmatics.Dialogue.KOS.answerhoodFromPartition {W : Type} [BEq W] (worlds : List W) : Answerhood (BProp W) (QUD W)

Answerhood instance: BProp W resolves QUD W over a fixed world list.

Equations

• Theories.Pragmatics.Dialogue.KOS.answerhoodFromPartition worlds = { resolves := Theories.Pragmatics.Dialogue.KOS.bpropResolvesQUD worlds }

def Theories.Pragmatics.Dialogue.KOS.bpropResolvesIssue {W : Type} (worlds : List W) (fact : BProp W) (q : Discourse.Issue W) : Bool

A BProp W resolves a Discourse.Issue W if it settles some alternative.

@cite{ciardelli-groenendijk-roelofsen-2018}: resolving an issue means establishing enough information to determine which alternative holds.

Equations

• Theories.Pragmatics.Dialogue.KOS.bpropResolvesIssue worlds fact q = q.alternatives.any fun (alt : Discourse.InfoState W) => Discourse.propEntails fact alt worlds

def Theories.Pragmatics.Dialogue.KOS.answerhoodFromIssue {W : Type} (worlds : List W) : Answerhood (BProp W) (Discourse.Issue W)

Answerhood instance: BProp W resolves Discourse.Issue W.

Equations

• Theories.Pragmatics.Dialogue.KOS.answerhoodFromIssue worlds = { resolves := Theories.Pragmatics.Dialogue.KOS.bpropResolvesIssue worlds }

inductive Theories.Pragmatics.Dialogue.KOS.RainWorld : Type

Three-world scenario: is it raining?

• sunny : RainWorld
• rainy : RainWorld
• cloudy : RainWorld

instance Theories.Pragmatics.Dialogue.KOS.instReprRainWorld : Repr RainWorld

Equations

• Theories.Pragmatics.Dialogue.KOS.instReprRainWorld = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprRainWorld.repr }

def Theories.Pragmatics.Dialogue.KOS.instReprRainWorld.repr : RainWorld → ℕ → Std.Format

Equations

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

instance Theories.Pragmatics.Dialogue.KOS.instDecidableEqRainWorld : DecidableEq RainWorld

Equations

• Theories.Pragmatics.Dialogue.KOS.instDecidableEqRainWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Theories.Pragmatics.Dialogue.KOS.instBEqRainWorld : BEq RainWorld

Equations

• Theories.Pragmatics.Dialogue.KOS.instBEqRainWorld = { beq := Theories.Pragmatics.Dialogue.KOS.instBEqRainWorld.beq }

def Theories.Pragmatics.Dialogue.KOS.instBEqRainWorld.beq : RainWorld → RainWorld → Bool

Equations

• Theories.Pragmatics.Dialogue.KOS.instBEqRainWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Theories.Pragmatics.Dialogue.KOS.isRainingQ : QUD RainWorld

"Is it raining?" — partition into rainy vs non-rainy.

Equations

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

def Theories.Pragmatics.Dialogue.KOS.itIsRaining : BProp RainWorld

"It is raining" — true only in the rainy world.

Equations

• Theories.Pragmatics.Dialogue.KOS.itIsRaining Theories.Pragmatics.Dialogue.KOS.RainWorld.rainy = true
• Theories.Pragmatics.Dialogue.KOS.itIsRaining w = false

def Theories.Pragmatics.Dialogue.KOS.itIsSunny : BProp RainWorld

"It is sunny" — true only in the sunny world.

Equations

• Theories.Pragmatics.Dialogue.KOS.itIsSunny Theories.Pragmatics.Dialogue.KOS.RainWorld.sunny = true
• Theories.Pragmatics.Dialogue.KOS.itIsSunny w = false

theorem Theories.Pragmatics.Dialogue.KOS.raining_resolves_raining : bpropResolvesQUD Theories.Pragmatics.Dialogue.KOS.rainWorlds✝ itIsRaining isRainingQ = true

"It is raining" resolves "Is it raining?"

theorem Theories.Pragmatics.Dialogue.KOS.sunny_resolves_raining : bpropResolvesQUD Theories.Pragmatics.Dialogue.KOS.rainWorlds✝ itIsSunny isRainingQ = true

"It is sunny" also resolves "Is it raining?"

theorem Theories.Pragmatics.Dialogue.KOS.rain_ask_qud : Theories.Pragmatics.Dialogue.KOS.rainTIS₁✝.dgb.qud = [isRainingQ]

After asking, QUD has the partition question.

theorem Theories.Pragmatics.Dialogue.KOS.rain_assert_resolves : Theories.Pragmatics.Dialogue.KOS.rainTIS₂✝.dgb.qud = []

After asserting "It is raining", QUD is empty (resolved).

instance Theories.Pragmatics.Dialogue.KOS.instAnswerhoodString_2 : Answerhood String String

Equations

• Theories.Pragmatics.Dialogue.KOS.instAnswerhoodString_2 = { resolves := fun (fact question : String) => fact == question }

theorem Theories.Pragmatics.Dialogue.KOS.awq_resolves_original_question : Theories.Pragmatics.Dialogue.KOS.awq₂✝.dgb.qud = []

After assertWithQUD, the question from Ask is resolved (fact matches).

theorem Theories.Pragmatics.Dialogue.KOS.awq_has_fact : "Bo is here" ∈ Theories.Pragmatics.Dialogue.KOS.awq₂✝.dgb.facts

The fact is in FACTS after assertWithQUD.

theorem Theories.Pragmatics.Dialogue.KOS.assertive_moves_mind_to_world {Fact QContent : Type} (p : Fact) : (IllocMove.assert p).directionOfFit = Core.Discourse.DirectionOfFit.mindToWorld ∧ (IllocMove.accept p).directionOfFit = Core.Discourse.DirectionOfFit.mindToWorld ∧ (IllocMove.confirm p).directionOfFit = Core.Discourse.DirectionOfFit.mindToWorld

All assertive-class moves (assert, accept, confirm) share mind-to-world fit: the speaker takes responsibility for truth.

theorem Theories.Pragmatics.Dialogue.KOS.directive_moves_world_to_mind {Fact QContent : Type} (q : QContent) (p : Fact) : (IllocMove.ask q).directionOfFit = Core.Discourse.DirectionOfFit.worldToMind ∧ (IllocMove.check p).directionOfFit = Core.Discourse.DirectionOfFit.worldToMind

Directive moves (ask, check) share world-to-mind fit: the speaker wants the addressee to act.

Utterance Integration: Grounding vs CRification

@cite{ginzburg-2012} Ch. 6 (§6.5–6.7): when an utterance enters Pending, the addressee either grounds it (all contextual parameters resolved → content enters FACTS) or CRifies it (some parameter unresolved → a clarification request question is pushed onto QUD).

This is the LocProp-level protocol that replaces the string-based IS.integrateUtterance from @cite{ginzburg-cooper-2004}.

def Theories.Pragmatics.Dialogue.KOS.LocProp.isFullyResolved {Cont : Type} (lp : LocProp Cont) : Bool

Whether a LocProp has all contextual parameters resolved. A fully resolved LocProp can be grounded directly.

Equations

• lp.isFullyResolved = List.isEmpty lp.cparams

def Theories.Pragmatics.Dialogue.KOS.LocProp.canGround {Cont : Type} (lp : LocProp Cont) : Bool

Whether a LocProp can be grounded (= fully resolved).

Equations

• lp.canGround = lp.isFullyResolved

inductive Theories.Pragmatics.Dialogue.KOS.IntegrationResult (Cont QContent : Type) : Type

The result of integrating a LocProp into a DGB. Either grounded (content → FACTS) or CRified (CR question → QUD).

• grounded {Cont QContent : Type} (content : Cont) : IntegrationResult Cont QContent

  All cparams resolved: content enters FACTS.

• crification {Cont QContent : Type} (crQuestion : QContent) (unresolvedParam : CParam) : IntegrationResult Cont QContent

  Some cparam unresolved: CR question pushed onto QUD.

def Theories.Pragmatics.Dialogue.KOS.instReprIntegrationResult.repr {Cont✝ QContent✝ : Type} [Repr Cont✝] [Repr QContent✝] : IntegrationResult Cont✝ QContent✝ → ℕ → Std.Format

Equations

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

instance Theories.Pragmatics.Dialogue.KOS.instReprIntegrationResult {Cont✝ QContent✝ : Type} [Repr Cont✝] [Repr QContent✝] : Repr (IntegrationResult Cont✝ QContent✝)

Equations

• Theories.Pragmatics.Dialogue.KOS.instReprIntegrationResult = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprIntegrationResult.repr }

def Theories.Pragmatics.Dialogue.KOS.IntegrationResult.isGrounded {Cont QContent : Type} : IntegrationResult Cont QContent → Bool

Is this integration result a grounding?

Equations

• (Theories.Pragmatics.Dialogue.KOS.IntegrationResult.grounded a).isGrounded = true
• (Theories.Pragmatics.Dialogue.KOS.IntegrationResult.crification a a_1).isGrounded = false

def Theories.Pragmatics.Dialogue.KOS.integrateLocProp {Cont QContent : Type} (lp : LocProp Cont) (toCR : CParam → QContent) : IntegrationResult Cont QContent

Integrate a LocProp: ground if resolved, CRify otherwise.

The toCR function converts an unresolved parameter to a clarification question — this is domain-specific (e.g., "Who do you mean by 'Bo'?").

Equations

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

theorem Theories.Pragmatics.Dialogue.KOS.resolved_always_grounds {Cont QContent : Type} (lp : LocProp Cont) (toCR : CParam → QContent) (h : lp.isFullyResolved = true) : (integrateLocProp lp toCR).isGrounded = true

A fully resolved LocProp always grounds.

theorem Theories.Pragmatics.Dialogue.KOS.no_coercion_fallback {Cont QContent : Type} (lp : LocProp Cont) (toCR : CParam → QContent) (p : CParam) (ps : CParamSet) (h : lp.cparams = p :: ps) : (integrateLocProp lp toCR).isGrounded = false

If there are no coercion options and the LocProp has unresolved params, integration produces a CRification — there is no silent fallback.

DGB Well-Formedness: Non-Resolve-Cond

@cite{ginzburg-2012} ex. 100 (p. 111): the DGB includes a well-formedness constraint non-resolve-cond requiring that no question on QUD is already resolved by FACTS. This prevents trivially answered questions from lingering on QUD — they should be downdated.

def Theories.Pragmatics.Dialogue.KOS.DGB.nonResolveCond {P Fact QContent : Type} [Answerhood Fact QContent] (dgb : DGB P Fact QContent) : Bool

The non-resolve-cond: no question on QUD is resolved by FACTS. @cite{ginzburg-2012} ex. 100 (p. 111).

Equations

• dgb.nonResolveCond = dgb.qud.all fun (q : QContent) => !dgb.facts.any fun (f : Fact) => Theories.Pragmatics.Dialogue.KOS.Answerhood.resolves f q

theorem Theories.Pragmatics.Dialogue.KOS.DGB.initial_nonResolveCond {P Fact QContent : Type} [Answerhood Fact QContent] : initial.nonResolveCond = true

An empty DGB trivially satisfies non-resolve-cond.

theorem Theories.Pragmatics.Dialogue.KOS.downdateQud_restores_nonResolveCond {P Fact QContent : Type} [Answerhood Fact QContent] (dgb : DGB P Fact QContent) : dgb.downdateQud.nonResolveCond = true

After QUD-downdate, non-resolve-cond holds: all remaining questions are unresolved by FACTS.