KOS: DGB Operations

@cite{ginzburg-2012} 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 Core.Semantics.CommonGround
• §5. QUD downdate properties + non-resolve-cond well-formedness
• §6. Partition-based answerhood (PropResolvesQUD)

Answerhood

KOS's "fact resolves question" relation is the Core.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 Dialogue.KOS.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 Dialogue.KOS.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 Dialogue.KOS.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 Dialogue.KOS.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. For questions paired with focus-establishing constituents, use pushQudInfoStruc directly.

Equations

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

def Dialogue.KOS.DGB.pushQudInfoStruc {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (dgb : DGB P Fact QContent Cont) (is : InfoStruc QContent Cont) : DGB P Fact QContent Cont

Push a fully-formed InfoStruc (question + FECs) onto QUD. Used when the introducing utterance carries focus-establishing constituents that downstream NSU resolution will consume (Ch. 7).

Equations

• dgb.pushQudInfoStruc is = { spkr := dgb.spkr, addr := dgb.addr, facts := dgb.facts, moves := dgb.moves, pending := dgb.pending, qud := is :: dgb.qud }

def Dialogue.KOS.DGB.downdateQud {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Core.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 Dialogue.KOS.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 Dialogue.KOS.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 Dialogue.KOS.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 Dialogue.KOS.DGB.assertFact {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Core.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

def Dialogue.KOS.DGB.mapFacts {Participant : Type u_1} {Fact : Type u_2} {Fact' : Type u_3} {QContent : Type u_4} {Cont : Type} (f : Fact → Fact') (dgb : DGB Participant Fact QContent Cont) : DGB Participant Fact' QContent Cont

Map over a DGB's fact type, preserving structure.

Equations

• Dialogue.KOS.DGB.mapFacts f dgb = { spkr := dgb.spkr, addr := dgb.addr, facts := List.map f dgb.facts, pending := dgb.pending, qud := dgb.qud }

def Dialogue.KOS.DGB.mapQud {Participant : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {QContent' : Type u_4} {Cont : Type} (f : QContent → QContent') (dgb : DGB Participant Fact QContent Cont) : DGB Participant Fact QContent' Cont

Map over a DGB's question type, preserving structure (FECs are dropped since they reference the same Cont).

Equations

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

theorem Dialogue.KOS.DGB.mapFacts_length {Participant : Type u_1} {Fact : Type u_2} {Fact' : Type u_3} {QContent : Type u_4} {Cont : Type} (f : Fact → Fact') (dgb : DGB Participant Fact QContent Cont) : (mapFacts f dgb).facts.length = dgb.facts.length

Mapping facts preserves fact count.

@[implicit_reducible]

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

DGB with Set W facts projects to a context set. @cite{ginzburg-2012} Ch. 4: the DGB's FACTS field IS the common ground.

Equations

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

@[implicit_reducible]

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

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

Equations

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

theorem Dialogue.KOS.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) : Core.CommonGround.HasContextSet.toContextSet tis = Core.CommonGround.HasContextSet.toContextSet tis.dgb

TIS context set is extracted from the DGB.

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

Downdate never increases QUD size.

theorem Dialogue.KOS.downdateQud_removes_resolved {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Core.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 : Core.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

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

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

Equations

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

@[implicit_reducible]

instance Dialogue.KOS.instDecidableNonResolveCond {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Core.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 Dialogue.KOS.DGB.initial_nonResolveCond {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Core.Question.DecidableSupport Fact QContent] : initial.nonResolveCond

An empty DGB trivially satisfies non-resolve-cond.

theorem Dialogue.KOS.downdateQud_restores_nonResolveCond {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Core.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 Core/Discourse/QUD.lean (@cite{groenendijk-stokhof-1984}):

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 Dialogue.KOS.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

• Dialogue.KOS.PropResolvesQUD worlds fact q = ∀ w₁ ∈ List.filter (fun (w : W) => decide (fact w)) worlds, ∀ w₂ ∈ List.filter (fun (w : W) => decide (fact w)) worlds, q.sameAnswer w₁ w₂ = true

@[implicit_reducible]

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

Equations

• Dialogue.KOS.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.