KOS: Conversational Rules on the TIS

@cite{ginzburg-2012} Ch. 4

The TIS-level conversational rules: ask, assert, accept, qspec, check, confirm, qcoord, factUpdateQudDowndate, greet. Each rule is a function TIS → … → TIS matching @cite{ginzburg-2012}'s precondition/ effect shape (the precondition is implicit in the input TIS state; the effect is the output TIS state).

Plus the M-Coherence apparatus (ex. 70 p. 96) that lifts a list of conversational rules into a relation on (DGB, move) pairs.

Core Rules

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

Genre relevance

genreRelevant (eq. 90 p. 105) lives in the sibling KOS/Genre.lean.

Grounding

The LocProp grounding/CRification protocol (Ch. 6 §6.5–6.7) lives in the sibling KOS/Grounding.lean.

def Dialogue.KOS.TIS.ask {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (q : QContent) : TIS P Fact QContent Cont

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 (Dialogue.KOS.IllocMove.ask q), priv := tis.priv }

def Dialogue.KOS.TIS.assertRule {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Core.Question.DecidableSupport Fact QContent] (tis : TIS P Fact QContent Cont) (p : Fact) : TIS P Fact QContent Cont

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 (Dialogue.KOS.IllocMove.assert p), priv := tis.priv }

def Dialogue.KOS.TIS.assertWithQUD {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Core.Question.DecidableSupport Fact QContent] (tis : TIS P Fact QContent Cont) (p : Fact) (aboutP : QContent) : TIS P Fact QContent Cont

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 (Dialogue.KOS.IllocMove.assert p), priv := tis.priv }

def Dialogue.KOS.TIS.accept {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (p : Fact) : TIS P Fact QContent Cont

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 (Dialogue.KOS.IllocMove.accept p), priv := tis.priv }

def Dialogue.KOS.TIS.qspec {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (q : QContent) : TIS P Fact QContent Cont

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 (Dialogue.KOS.IllocMove.ask q), priv := tis.priv }

def Dialogue.KOS.TIS.check {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (p : Fact) (aboutP : QContent) : TIS P Fact QContent Cont

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 (Dialogue.KOS.IllocMove.check p), priv := tis.priv }

def Dialogue.KOS.TIS.confirm {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Core.Question.DecidableSupport Fact QContent] (tis : TIS P Fact QContent Cont) (p : Fact) : TIS P Fact QContent Cont

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 (Dialogue.KOS.IllocMove.confirm p), priv := tis.priv }

def Dialogue.KOS.TIS.qcoord {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (q : QContent) : TIS P Fact QContent Cont

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 Dialogue.KOS.TIS.factUpdateQudDowndate {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Core.Question.DecidableSupport Fact QContent] (tis : TIS P Fact QContent Cont) (p : Fact) : TIS P Fact QContent Cont

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, priv := tis.priv }

def Dialogue.KOS.TIS.greet {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) : TIS P Fact QContent Cont

Greeting: conversation initialization.

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

Equations

• tis.greet = { dgb := tis.dgb.recordMove Dialogue.KOS.IllocMove.greet, priv := tis.priv }

theorem Dialogue.KOS.ask_pushes_qud {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (q : QContent) : (tis.ask q).dgb.qud = InfoStruc.fromQuestion q :: tis.dgb.qud

Ask pushes exactly one question onto QUD (wrapped in InfoStruc).

theorem Dialogue.KOS.ask_preserves_facts {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (q : QContent) : (tis.ask q).dgb.facts = tis.dgb.facts

Ask does not modify FACTS.

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

Ask records the move.

theorem Dialogue.KOS.assert_adds_fact {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Core.Question.DecidableSupport Fact QContent] (tis : TIS P Fact QContent Cont) (p : Fact) : p ∈ (tis.assertRule p).dgb.facts

Assert adds the fact to FACTS.

theorem Dialogue.KOS.assertWithQUD_adds_fact {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [Core.Question.DecidableSupport Fact QContent] (tis : TIS P Fact QContent Cont) (p : Fact) (aboutP : QContent) : p ∈ (tis.assertWithQUD p aboutP).dgb.facts

assertWithQUD adds the fact to FACTS.

theorem Dialogue.KOS.accept_preserves_qud {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (p : Fact) : (tis.accept p).dgb.qud = tis.dgb.qud

Accept adds a fact without changing QUD.

theorem Dialogue.KOS.accept_adds_fact {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (p : Fact) : (tis.accept p).dgb.facts = p :: tis.dgb.facts

Accept adds the fact to FACTS.

theorem Dialogue.KOS.qspec_pushes {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (q : QContent) : (tis.qspec q).dgb.qud = InfoStruc.fromQuestion q :: tis.dgb.qud

QSPEC pushes a subquestion.

theorem Dialogue.KOS.check_pushes_qud {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (p : Fact) (aboutP : QContent) : (tis.check p aboutP).dgb.qud = InfoStruc.fromQuestion aboutP :: tis.dgb.qud

Check pushes a question onto QUD.

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

Greeting requires empty moves (precondition check).

Move Coherence

@cite{ginzburg-2012} 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 Dialogue.KOS.ConvRule (P : Type u_1) (Fact : Type u_2) (QContent : Type u_3) (Cont : Type) : Type (max (max (max (max (max u_3 u_2) u_1) u_3) u_2) u_1)

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

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

def Dialogue.KOS.mCoherent {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (rules : List (ConvRule P Fact QContent Cont)) (dgb₀ : DGB P Fact QContent Cont) (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

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