KOS: DGB Operations

[Gin12] Ch. 4

Operations on the Dialogue Gameboard: pushing onto QUD, downdating resolved questions, recording moves, asserting facts. Plus the HasContextSet bridge connecting DGB facts to the standard common ground type, the non-resolve-cond well-formedness check, and the partition-based answerhood predicate PropResolvesQUD.

Structure

• §1. DGB structural lemmas (initial state)
• §2. DGB update operations: pushQud, downdateQud, addFact, recordMove, assertFact
• §3. DGB content mapping: mapFacts, mapQud
• §4. HasContextSet bridge to CommonGround
• §5. QUD downdate properties + non-resolve-cond well-formedness
• §6. Partition-based answerhood (PropResolvesQUD)

Answerhood

KOS's "fact resolves question" relation is the Question.Support typeclass (Prop-valued, mathlib-shaped). With QUD now storing InfoStruc QContent Cont (per Ch. 6 final), the support check on f ⊨ is.q projects through the InfoStruc's question field.

theorem Discourse.Gameboard.DGB.initial_no_moves {Participant : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} : initial.moves = []

An empty DGB has no moves.

theorem Discourse.Gameboard.DGB.initial_no_qud {Participant : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} : initial.qud = []

An empty DGB has empty QUD.

theorem Discourse.Gameboard.DGB.initial_no_latestMove {Participant : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} : initial.latestMove = none

An empty DGB has no latest move.

def Discourse.Gameboard.DGB.pushQud {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (dgb : DGB P Fact QContent Cont) (q : QContent) : DGB P Fact QContent Cont

Push a bare question onto the QUD stack, wrapping it in an InfoStruc with no FECs.

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 := Discourse.Gameboard.InfoStruc.fromQuestion q :: dgb.qud }

def Discourse.Gameboard.DGB.downdateQud {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Question.DecidableSupport Fact QContent] (dgb : DGB P Fact QContent Cont) : DGB P Fact QContent Cont

Remove resolved questions from QUD.

Ch. 4: QUD-downdate removes a question q from QUD when FACTS contextually entail an answer to q. Now QUD entries are InfoStrucs; the support check projects through is.q.

Equations

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

def Discourse.Gameboard.DGB.addFact {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (dgb : DGB P Fact QContent Cont) (p : Fact) : DGB P Fact QContent Cont

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 Discourse.Gameboard.DGB.recordMove {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (dgb : DGB P Fact QContent Cont) (m : IllocMove Fact QContent) : DGB P Fact QContent Cont

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 Discourse.Gameboard.DGB.pushPending {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (dgb : DGB P Fact QContent Cont) (lp : LocProp Cont) : DGB P Fact QContent Cont

Push a LocProp onto Pending (Ch. 6 ungrounded utterance).

Equations

• dgb.pushPending lp = { spkr := dgb.spkr, addr := dgb.addr, facts := dgb.facts, moves := dgb.moves, pending := lp :: dgb.pending, qud := dgb.qud }

def Discourse.Gameboard.DGB.assertFact {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Question.DecidableSupport Fact QContent] (dgb : DGB P Fact QContent Cont) (p : Fact) : DGB P Fact QContent Cont

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

@[implicit_reducible]

instance Discourse.Gameboard.instHasContextSetDGBSet {W : Type u_1} {Participant : Type u_2} {QContent : Type u_3} {Cont : Type} : CommonGround.HasContextSet (DGB Participant (Set W) QContent Cont) W

DGB with Set W facts projects to a context set. [Gin12] Ch. 4: the DGB's FACTS field IS the common ground.

Equations

• Discourse.Gameboard.instHasContextSetDGBSet = { toContextSet := fun (dgb : Discourse.Gameboard.DGB Participant (Set W) QContent Cont) (w : W) => ∀ p ∈ dgb.facts, p w }

@[implicit_reducible]

instance Discourse.Gameboard.instHasContextSetTISSet {W : Type u_1} {Participant : Type u_2} {QContent : Type u_3} {Cont : Type} : CommonGround.HasContextSet (TIS Participant (Set W) QContent Cont) W

TIS with Set W facts inherits the DGB's context set.

Equations

• Discourse.Gameboard.instHasContextSetTISSet = { toContextSet := fun (tis : Discourse.Gameboard.TIS Participant (Set W) QContent Cont) (w : W) => ∀ p ∈ tis.dgb.facts, p w }

theorem Discourse.Gameboard.tis_contextSet_eq_dgb {W : Type u_1} {Participant : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS Participant (Set W) QContent Cont) : CommonGround.HasContextSet.toContextSet tis = CommonGround.HasContextSet.toContextSet tis.dgb

TIS context set is extracted from the DGB.

theorem Discourse.Gameboard.downdateQud_length_le {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Question.DecidableSupport Fact QContent] (dgb : DGB P Fact QContent Cont) : dgb.downdateQud.qud.length ≤ dgb.qud.length

Downdate never increases QUD size.

theorem Discourse.Gameboard.downdateQud_removes_resolved {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Question.DecidableSupport Fact QContent] (dgb : DGB P Fact QContent Cont) (is : InfoStruc QContent Cont) (f : Fact) (hq : dgb.qud = [is]) (hf : f ∈ dgb.facts) (hr : Question.Support.supports f is.q) : dgb.downdateQud.qud = []

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

DGB Well-Formedness: Non-Resolve-Cond

[Gin12] 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 Discourse.Gameboard.DGB.nonResolveCond {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Question.DecidableSupport Fact QContent] (dgb : DGB P Fact QContent Cont) : Prop

The non-resolve-cond: no question on QUD is resolved by FACTS. [Gin12] ex. 100 (p. 111).

Equations

• dgb.nonResolveCond = ∀ is ∈ dgb.qud, ¬∃ f ∈ dgb.facts, Question.Support.supports f is.q

@[implicit_reducible]

instance Discourse.Gameboard.instDecidableNonResolveCond {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Question.DecidableSupport Fact QContent] (dgb : DGB P Fact QContent Cont) : Decidable dgb.nonResolveCond

Equations

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

theorem Discourse.Gameboard.DGB.initial_nonResolveCond {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Question.DecidableSupport Fact QContent] : initial.nonResolveCond

An empty DGB trivially satisfies non-resolve-cond.

theorem Discourse.Gameboard.downdateQud_restores_nonResolveCond {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Question.DecidableSupport Fact QContent] (dgb : DGB P Fact QContent Cont) : dgb.downdateQud.nonResolveCond

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

Partition-Based Support

Ch. 4 defines QUD-downdate in terms of FACTS resolving questions. The Support typeclass abstracts this. Here we connect it to the partition-based QUD W from Discourse/QUD.lean ([GS84]):

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

def Discourse.Gameboard.PropResolvesQUD {W : Type u_1} (worlds : List W) (fact : Set W) [DecidablePred fact] (q : QUD W) : Prop

A Set W resolves a QUD W if all fact-worlds are in the same partition cell. Prop-valued; Decidable via the bundled per-pair predicate decidability.

Equations

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

@[implicit_reducible]

instance Discourse.Gameboard.instDecidablePropResolvesQUD {W : Type u_1} (worlds : List W) (fact : Set W) [DecidablePred fact] (q : QUD W) : Decidable (PropResolvesQUD worlds fact q)

Equations

• Discourse.Gameboard.instDecidablePropResolvesQUD worlds fact q = id inferInstance

Worked partition consumers below construct their own DecidableSupport instances at the concrete fact-type (e.g. rainSupport uses RainProp.toProp, where DecidablePred is automatic). A generic Set W → DecidableSupport factory would have to choose Classical.decPred fact and the resulting kernel unfolding doesn't align cleanly between the supports and decSupports fields; consumers requiring it can construct the instance locally.