Dialogue gameboard operations

This file defines the updates of the dialogue gameboard of Ginzburg's theory of dialogue, KoS: pushing a question with its focus-establishing constituents onto QUD, adding a fact, recording a move or a pending utterance, changing the turn, and QUD-downdate, which removes from QUD every question that some fact resolves. A gameboard satisfies non-resolve-cond when no fact resolves a question under discussion; downdate establishes the condition and is idle exactly on the gameboards that satisfy it, and pushing a question keeps it exactly when no fact resolves that question, which is Ginzburg's Question Introduction Appropriateness Condition. Contextual instantiation witnesses some of an utterance's contextual parameters, and the utterances it produces are exactly Ginzburg's contextual extensions.

A gameboard whose facts have common grounds has the meet of them as its common ground, and adding a fact is Stalnakerian assertion of it; a gameboard whose questions have issues has the issue of MaxQUD.

Main definitions

• Discourse.LocutionaryProposition.instantiate: contextual instantiation of an utterance.
• Discourse.Gameboard.pushQud, Discourse.Gameboard.addFact, Discourse.Gameboard.recordMove, Discourse.Gameboard.swapTurn: updates of a gameboard.
• Discourse.Gameboard.NonResolveCond, Discourse.Gameboard.downdateQud: non-resolve-cond and QUD-downdate.

Main results

• Discourse.LocutionaryProposition.exists_eq_instantiate_iff: contextual instantiation yields exactly the contextual extensions.
• Discourse.Gameboard.downdateQud_eq_self_iff, Discourse.Gameboard.nonResolveCond_pushQud_iff.
• Discourse.Gameboard.commonGround_addFact: adding a fact meets the common ground with it.

Implementation notes

• Resolution is an explicit relation R : D.Fact → D.Question → Prop, not an instance on the domain: resolvedness is "not purely semantic" but agent-relative, so the types of facts and questions do not determine it.
• The downdate is that of Ginzburg's (44). His Appendix B version lets NonResolve return any sub-poset of QUD free of resolved questions, and also removes a question once a fact resolves whether the participant wishes to discuss it.
• Ginzburg states non-resolve-cond as resolution by FACTS as a whole, where (44) and (52) quantify over its members; NonResolveCond follows the members, so that downdate establishes it.

References

• [Gin12]

def Discourse.LocutionaryProposition.instantiate {G : GrammaticalDomain} {C : Type u} (u : LocutionaryProposition G C) (s : Finset G.Label) : LocutionaryProposition G C

Contextual instantiation ([Gin12] (48) p. 178): the parameters labelled in s have been witnessed and leave the utterance's contextual parameters.

Equations

• u.instantiate s = { form := u.form, category := u.category, content := u.content, parameters := u.parameters \ s, constituents := u.constituents }

@[simp]

theorem Discourse.LocutionaryProposition.parameters_instantiate {G : GrammaticalDomain} {C : Type u} (u : LocutionaryProposition G C) (s : Finset G.Label) : (u.instantiate s).parameters = u.parameters \ s

@[simp]

theorem Discourse.LocutionaryProposition.form_instantiate {G : GrammaticalDomain} {C : Type u} (u : LocutionaryProposition G C) (s : Finset G.Label) : (u.instantiate s).form = u.form

@[simp]

theorem Discourse.LocutionaryProposition.category_instantiate {G : GrammaticalDomain} {C : Type u} (u : LocutionaryProposition G C) (s : Finset G.Label) : (u.instantiate s).category = u.category

@[simp]

theorem Discourse.LocutionaryProposition.content_instantiate {G : GrammaticalDomain} {C : Type u} (u : LocutionaryProposition G C) (s : Finset G.Label) : (u.instantiate s).content = u.content

@[simp]

theorem Discourse.LocutionaryProposition.constituents_instantiate {G : GrammaticalDomain} {C : Type u} (u : LocutionaryProposition G C) (s : Finset G.Label) : (u.instantiate s).constituents = u.constituents

@[simp]

theorem Discourse.LocutionaryProposition.instantiate_empty {G : GrammaticalDomain} {C : Type u} (u : LocutionaryProposition G C) : u.instantiate ∅ = u

theorem Discourse.LocutionaryProposition.instantiate_instantiate {G : GrammaticalDomain} {C : Type u} (u : LocutionaryProposition G C) (s t : Finset G.Label) : (u.instantiate s).instantiate t = u.instantiate (s ∪ t)

theorem Discourse.LocutionaryProposition.exists_eq_instantiate_iff {G : GrammaticalDomain} {C : Type u} (w u : LocutionaryProposition G C) : (∃ (s : Finset G.Label), w = u.instantiate s) ↔ w.form = u.form ∧ w.category = u.category ∧ w.content = u.content ∧ w.constituents = u.constituents ∧ w.parameters ⊆ u.parameters

Contextual instantiation yields exactly the contextual extensions of [Gin12] (47) p. 178: the utterances agreeing on every field but the contextual parameters, of which they leave fewer unwitnessed.

def Discourse.Gameboard.initial {D : Domain} (speaker addressee : D.Participant) : Gameboard D

The gameboard of a conversation with no moves yet, speaker addressing addressee.

Equations

• Discourse.Gameboard.initial speaker addressee = { speaker := speaker, addressee := addressee }

def Discourse.Gameboard.latestMove {D : Domain} (d : Gameboard D) : Option (LocutionaryProposition D.toGrammaticalDomain D.Content)

The latest move.

Equations

• d.latestMove = d.moves.getLast?

def Discourse.Gameboard.maxQud {D : Domain} (d : Gameboard D) : Option D.Question

The question of MaxQUD.

Equations

• d.maxQud = Option.map (fun (x : Discourse.InformationStructure D.toGrammaticalDomain D.Question) => x.question) d.qud.head?

def Discourse.Gameboard.latestContent {D : Domain} (d : Gameboard D) : Option D.Content

The content of the latest move.

Equations

• d.latestContent = Option.map (fun (x : Discourse.LocutionaryProposition D.toGrammaticalDomain D.Content) => x.content) d.latestMove

def Discourse.Gameboard.pushQud {D : Domain} (d : Gameboard D) (i : InformationStructure D.toGrammaticalDomain D.Question) : Gameboard D

Push a question with its focus-establishing constituents onto QUD, as MaxQUD.

Equations

• d.pushQud i = { speaker := d.speaker, addressee := d.addressee, facts := d.facts, moves := d.moves, pending := d.pending, qud := i :: d.qud }

def Discourse.Gameboard.addFact {D : Domain} (d : Gameboard D) (p : D.Fact) : Gameboard D

Add a fact to FACTS.

Equations

• d.addFact p = { speaker := d.speaker, addressee := d.addressee, facts := insert p d.facts, moves := d.moves, pending := d.pending, qud := d.qud }

def Discourse.Gameboard.recordMove {D : Domain} (d : Gameboard D) (m : LocutionaryProposition D.toGrammaticalDomain D.Content) : Gameboard D

Record a move as the latest in MOVES.

Equations

• d.recordMove m = { speaker := d.speaker, addressee := d.addressee, facts := d.facts, moves := d.moves ++ [m], pending := d.pending, qud := d.qud }

def Discourse.Gameboard.pushPending {D : Domain} (d : Gameboard D) (m : LocutionaryProposition D.toGrammaticalDomain D.Content) : Gameboard D

Push an ungrounded utterance onto PENDING, as MaxPending.

Equations

• d.pushPending m = { speaker := d.speaker, addressee := d.addressee, facts := d.facts, moves := d.moves, pending := m :: d.pending, qud := d.qud }

def Discourse.Gameboard.swapTurn {D : Domain} (d : Gameboard D) : Gameboard D

The addressee takes the turn.

Equations

• d.swapTurn = { speaker := d.addressee, addressee := d.speaker, facts := d.facts, moves := d.moves, pending := d.pending, qud := d.qud }

@[simp]

theorem Discourse.Gameboard.facts_initial {D : Domain} (s a : D.Participant) : (initial s a).facts = ∅

@[simp]

theorem Discourse.Gameboard.moves_initial {D : Domain} (s a : D.Participant) : (initial s a).moves = []

@[simp]

theorem Discourse.Gameboard.qud_initial {D : Domain} (s a : D.Participant) : (initial s a).qud = []

@[simp]

theorem Discourse.Gameboard.latestMove_initial {D : Domain} (s a : D.Participant) : (initial s a).latestMove = none

@[simp]

theorem Discourse.Gameboard.facts_addFact {D : Domain} (d : Gameboard D) (p : D.Fact) : (d.addFact p).facts = insert p d.facts

@[simp]

theorem Discourse.Gameboard.swapTurn_pushQud {D : Domain} (d : Gameboard D) (i : InformationStructure D.toGrammaticalDomain D.Question) : d.swapTurn.pushQud i = (d.pushQud i).swapTurn

@[simp]

theorem Discourse.Gameboard.swapTurn_recordMove {D : Domain} (d : Gameboard D) (m : LocutionaryProposition D.toGrammaticalDomain D.Content) : d.swapTurn.recordMove m = (d.recordMove m).swapTurn

@[simp]

theorem Discourse.Gameboard.latestMove_recordMove {D : Domain} (d : Gameboard D) (m : LocutionaryProposition D.toGrammaticalDomain D.Content) : (d.recordMove m).latestMove = some m

def Discourse.Gameboard.NonResolveCond {D : Domain} (d : Gameboard D) (R : D.Fact → D.Question → Prop) : Prop

non-resolve-cond ([Gin12] (100) p. 111) holds when no fact resolves a question under discussion, R being the resolution relation.

Equations

• d.NonResolveCond R = ∀ i ∈ d.qud, ¬∃ f ∈ d.facts, R f i.question

@[instance_reducible]

instance Discourse.Gameboard.instDecidableNonResolveCondOfDecidableRelFactQuestion {D : Domain} (d : Gameboard D) (R : D.Fact → D.Question → Prop) [DecidableRel R] : Decidable (d.NonResolveCond R)

Equations

• d.instDecidableNonResolveCondOfDecidableRelFactQuestion R = Discourse.Gameboard.instDecidableNonResolveCondOfDecidableRelFactQuestion._aux_1 d R

theorem Discourse.Gameboard.nonResolveCond_initial {D : Domain} (R : D.Fact → D.Question → Prop) (s a : D.Participant) : (initial s a).NonResolveCond R

theorem Discourse.Gameboard.nonResolveCond_pushQud_iff {D : Domain} (d : Gameboard D) (R : D.Fact → D.Question → Prop) {i : InformationStructure D.toGrammaticalDomain D.Question} : (d.pushQud i).NonResolveCond R ↔ (¬∃ f ∈ d.facts, R f i.question) ∧ d.NonResolveCond R

The Question Introduction Appropriateness Condition ([Gin12] (52) p. 89): pushing a question keeps non-resolve-cond exactly when no fact resolves it.

def Discourse.Gameboard.downdateQud {D : Domain} (d : Gameboard D) (R : D.Fact → D.Question → Prop) [DecidableRel R] : Gameboard D

QUD-downdate removes from QUD every question that some fact resolves (NonResolve, [Gin12] (44) p. 86).

Equations

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

@[simp]

theorem Discourse.Gameboard.facts_downdateQud {D : Domain} (d : Gameboard D) (R : D.Fact → D.Question → Prop) [DecidableRel R] : (d.downdateQud R).facts = d.facts

@[simp]

theorem Discourse.Gameboard.mem_qud_downdateQud {D : Domain} (d : Gameboard D) (R : D.Fact → D.Question → Prop) [DecidableRel R] {i : InformationStructure D.toGrammaticalDomain D.Question} : i ∈ (d.downdateQud R).qud ↔ i ∈ d.qud ∧ ¬∃ f ∈ d.facts, R f i.question

theorem Discourse.Gameboard.length_qud_downdateQud_le {D : Domain} (d : Gameboard D) (R : D.Fact → D.Question → Prop) [DecidableRel R] : (d.downdateQud R).qud.length ≤ d.qud.length

theorem Discourse.Gameboard.nonResolveCond_downdateQud {D : Domain} (d : Gameboard D) (R : D.Fact → D.Question → Prop) [DecidableRel R] : (d.downdateQud R).NonResolveCond R

theorem Discourse.Gameboard.downdateQud_eq_self_iff {D : Domain} (d : Gameboard D) (R : D.Fact → D.Question → Prop) [DecidableRel R] : d.downdateQud R = d ↔ d.NonResolveCond R

Downdate is idle exactly on gameboards satisfying non-resolve-cond.

@[instance_reducible]

instance Discourse.Gameboard.instHasCommonGround {D : Domain} {W : Type u_1} [HasCommonGround D.Fact W] : HasCommonGround (Gameboard D) W

A gameboard whose facts have common grounds has their meet as its common ground.

Equations

• Discourse.Gameboard.instHasCommonGround = { commonGround := fun (d : Discourse.Gameboard D) => ⨅ p ∈ d.facts, commonGround p }

theorem Discourse.Gameboard.commonGround_addFact {D : Domain} (d : Gameboard D) {W : Type u_1} [HasCommonGround D.Fact W] (p : D.Fact) : commonGround (d.addFact p) = commonGround p ⊓ commonGround d

Adding a fact to FACTS meets the common ground with the fact's, Stalnakerian assertion when facts are sets of worlds.

@[simp]

theorem Discourse.Gameboard.commonGround_initial {D : Domain} {W : Type u_1} [HasCommonGround D.Fact W] (s a : D.Participant) : commonGround (initial s a) = ⊤

@[instance_reducible]

instance Discourse.Gameboard.instHasIssue {D : Domain} {W : Type u_1} [HasIssue D.Question W] : HasIssue (Gameboard D) W

The issue of a gameboard is that of MaxQUD, the trivial issue when QUD is empty ([Gin12] §4.3.3 p. 68).

Equations

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

@[simp]

theorem Discourse.Gameboard.toIssue_pushQud {D : Domain} (d : Gameboard D) {W : Type u_1} [HasIssue D.Question W] (i : InformationStructure D.toGrammaticalDomain D.Question) : HasIssue.toIssue (d.pushQud i) = HasIssue.toIssue i.question

@[simp]

theorem Discourse.Gameboard.toIssue_addFact {D : Domain} (d : Gameboard D) {W : Type u_1} [HasIssue D.Question W] (p : D.Fact) : HasIssue.toIssue (d.addFact p) = HasIssue.toIssue d

@[simp]

theorem Discourse.Gameboard.toIssue_initial {D : Domain} {W : Type u_1} [HasIssue D.Question W] (s a : D.Participant) : HasIssue.toIssue (initial s a) = ⊤