Ginzburg (2012): The Interactive Stance

This file formalizes the conversational rules of [Gin12] over the dialogue gameboard Gameboard: each participant's turn holder and addressee, the commonly accepted FACTS, the MOVES made, the questions under discussion and, once metacommunication enters, the ungrounded utterances PENDING. A rule is a partial map from gameboards meeting its preconditions to updated gameboards (Rule.apply: the inventory of Appendix B, with the utterance, question or turn a nondeterministic rule chooses made an argument), a conversation composes rules (run), and an utterance is coherent when some rule makes it the latest move (Coherent). Asking a question keeps non-resolve-cond exactly when no fact resolves it, the Question Introduction Appropriateness Condition, and FACTS update restores the condition (askQud_nonResolveCond_iff, factUpdate_nonResolveCond); a genre makes an initiating move a relevant Free Speech move (IsInitiating, coherent_of_isInitiating); self-repair is Parameter Identification with the turn held (parameterIdentification_eq_repair_swapTurn); and each clarification rule makes the clarified constituent of the maximal pending utterance the focus-establishing constituent of MaxQUD (focusEstablishing_parameterIdentification, focusEstablishing_parameterFocussing, focusEstablishing_repair).

The worked traces of Ch. 4 reach the tabulated gameboards (Ex66.trace, Ex66.trace68_table, Ex79.trace), and after "Is George here? / Is WHO here?" the two participants' gameboards differ in QUD and PENDING although both processed the same utterances (George.differ). The turn each rule leaves is a general property of the inventory: the clarification rules pass it to the clarifier, repair keeps it, and QSPEC leaves it open (speaker_parameterIdentification, speaker_repair, speaker_qspec); the rows of Chs. 1 and 8 record who holds the turn after a clarification request, a self-repair and a bare follow-up question, as the rules predict (rows_turn).

Implementation notes

• The schematic content types of the traces (Content, Clarifiable) fix exactly the aboutness, influence and resolution relations each trace's side conditions require. Utterances are written orthographically, and the categories and contextual parameters are those the examples need (grammar).
• Contextual Instantiation takes the labels of the parameters it witnesses rather than the witnessing record, so the utterance it produces is a contextual extension of MaxPending by LocutionaryProposition.exists_eq_instantiate_iff.
• Three of the book's tables misprint: trace (66) labels the QUD update after B's question "Assert QUD-incrementation" where it is Ask QUD-incrementation; trace (68) ends with QUD := ⟨q0⟩ although no q0 occurs, and Fact update/QUD-downdate leaves QUD empty; Table 7.4 heads the Answers block with 413 while its cells sum to 403, the figure the total of Table 7.3 needs.
• Appendix B's backwards-looking appropriateness repair ((29) p. 375) makes the pending utterance the focus-establishing constituent, where its statement in the text ((31) p. 287) and every other clarification rule make it the clarified constituent; the rule follows (31).
• Ask and Assert QUD-incrementation push their question with no focus-establishing constituent, as in Ch. 4; the Ch. 7 version that pairs a wh-question with its wh-phrase (p. 241) is not modelled.
• The clarification-request forms of §6.2.1 and the non-sentential-utterance classes of Tables 7.3–7.4 are recorded as taxonomies (CRForm, NSUClass, NSUClass.function).

References

• [Gin12]

inductive Ginzburg2012.Category : Type

The syntactic categories of the examples' utterances and sub-utterances.

• s : Category
• np : Category

@[instance_reducible]

instance Ginzburg2012.instDecidableEqCategory : DecidableEq Category

Equations

• Ginzburg2012.instDecidableEqCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ginzburg2012.instReprCategory.repr : Category → ℕ → Std.Format

Equations

• Ginzburg2012.instReprCategory.repr Ginzburg2012.Category.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.Category.s")).group prec✝
• Ginzburg2012.instReprCategory.repr Ginzburg2012.Category.np prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.Category.np")).group prec✝

@[instance_reducible]

instance Ginzburg2012.instReprCategory : Repr Category

Equations

• Ginzburg2012.instReprCategory = { reprPrec := Ginzburg2012.instReprCategory.repr }

inductive Ginzburg2012.Parameter : Type

The contextual parameters of the examples are the referents of "George" and "Bo".

• george : Parameter
• bo : Parameter

@[instance_reducible]

instance Ginzburg2012.instDecidableEqParameter : DecidableEq Parameter

Equations

• Ginzburg2012.instDecidableEqParameter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ginzburg2012.instReprParameter.repr : Parameter → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Ginzburg2012.instReprParameter : Repr Parameter

Equations

• Ginzburg2012.instReprParameter = { reprPrec := Ginzburg2012.instReprParameter.repr }

@[reducible, inline]

abbrev Ginzburg2012.grammar : Discourse.GrammaticalDomain

The grammatical domain of the examples has orthographic forms, their categories, and the parameters, which are also the denotations of the names contributing them.

Equations

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

class Ginzburg2012.Content (Fact Q : Type) : Type

What a gameboard's content types supply: the polar question p?, the aboutness and influence relations of q-specificity, and resolution, with p resolving p?.

• polar : Fact → Q
• About : Fact → Q → Prop
• Influences : Q → Q → Prop
• Resolves : Fact → Q → Prop
• decAbout : DecidableRel About
• decInfluences : DecidableRel (Influences Fact)
• decResolves : DecidableRel Resolves
• resolves_polar (p : Fact) : Resolves p (polar p)

class Ginzburg2012.Clarifiable (P Fact Q : Type) : Type

The questions clarification accommodates: λx.Mean(A, u, x), what A meant by the sub-utterance u (Parameter Identification), and λx.v(u ↦ x), the content v with u's contextual parameter abstracted (Parameter Focussing).

• mean : P → Discourse.SubUtterance grammar → Q
• focus : Discourse.IllocutionaryAct Fact Q → Discourse.SubUtterance grammar → Q

@[reducible, inline]

abbrev Ginzburg2012.domain (P Fact Q : Type) [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] : Discourse.Gameboard.Domain

The domain of a gameboard whose utterances carry illocutionary content.

Equations

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

@[reducible, inline]

abbrev Ginzburg2012.Board (P Fact Q : Type) [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] : Type

A gameboard whose utterances, in MOVES and PENDING, carry illocutionary content.

Equations

• Ginzburg2012.Board P Fact Q = Discourse.Gameboard (Ginzburg2012.domain P Fact Q)

@[reducible, inline]

abbrev Ginzburg2012.Utterance (Fact Q : Type) : Type

An utterance with illocutionary content.

Equations

• Ginzburg2012.Utterance Fact Q = Discourse.LocutionaryProposition Ginzburg2012.grammar (Discourse.IllocutionaryAct Fact Q)

inductive Ginzburg2012.Agent : Type

The two participants of a duologue.

• A : Agent
• B : Agent

@[instance_reducible]

instance Ginzburg2012.instDecidableEqAgent : DecidableEq Agent

Equations

• Ginzburg2012.instDecidableEqAgent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Ginzburg2012.instReprAgent : Repr Agent

Equations

• Ginzburg2012.instReprAgent = { reprPrec := Ginzburg2012.instReprAgent.repr }

def Ginzburg2012.instReprAgent.repr : Agent → ℕ → Std.Format

Equations

• Ginzburg2012.instReprAgent.repr Ginzburg2012.Agent.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.Agent.A")).group prec✝
• Ginzburg2012.instReprAgent.repr Ginzburg2012.Agent.B prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.Agent.B")).group prec✝

def Ginzburg2012.ofMove {Fact Q : Type} (m : Discourse.IllocutionaryAct Fact Q) : Utterance Fact Q

The utterance of a bare move, a clause with no recorded form, when only its content matters (Ch. 4).

Equations

• Ginzburg2012.ofMove m = { form := "", category := Ginzburg2012.Category.s, content := m }

def Ginzburg2012.qudContrib {Fact Q : Type} [Content Fact Q] : Discourse.IllocutionaryAct Fact Q → Option Q

The question a move contributes to QUD: q for Ask(q), p? for Assert(p).

Equations

• Ginzburg2012.qudContrib (Discourse.IllocutionaryAct.ask q) = some q
• Ginzburg2012.qudContrib (Discourse.IllocutionaryAct.assert p) = some (Ginzburg2012.Content.polar p)
• Ginzburg2012.qudContrib x✝ = none

def Ginzburg2012.QSpecific {Fact Q : Type} [Content Fact Q] : Discourse.IllocutionaryAct Fact Q → Q → Prop

r is specific to q: About q for an assertion, Influencing q for a question.

Equations

• Ginzburg2012.QSpecific (Discourse.IllocutionaryAct.assert p) x✝ = Ginzburg2012.Content.About p x✝
• Ginzburg2012.QSpecific (Discourse.IllocutionaryAct.ask q') x✝ = Ginzburg2012.Content.Influences Fact q' x✝
• Ginzburg2012.QSpecific x✝¹ x✝ = False

inductive Ginzburg2012.Turn : Type

Who speaks next: the turn is kept (No-Turn-Change) or changes; a rule whose turn is underspecified takes either.

• keep : Turn
• change : Turn

@[instance_reducible]

instance Ginzburg2012.instDecidableEqTurn : DecidableEq Turn

Equations

• Ginzburg2012.instDecidableEqTurn x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ginzburg2012.instReprTurn.repr : Turn → ℕ → Std.Format

Equations

• Ginzburg2012.instReprTurn.repr Ginzburg2012.Turn.keep prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.Turn.keep")).group prec✝
• Ginzburg2012.instReprTurn.repr Ginzburg2012.Turn.change prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.Turn.change")).group prec✝

@[instance_reducible]

instance Ginzburg2012.instReprTurn : Repr Turn

Equations

• Ginzburg2012.instReprTurn = { reprPrec := Ginzburg2012.instReprTurn.repr }

def Ginzburg2012.Turn.act {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] : Turn → Board P Fact Q → Board P Fact Q

Effect the turn on a gameboard.

Equations

• Ginzburg2012.Turn.keep.act x✝ = x✝
• Ginzburg2012.Turn.change.act x✝ = Discourse.Gameboard.swapTurn x✝

inductive Ginzburg2012.Rule (P Fact Q : Type) : Type

The conversational rules of [Gin12] (Appendix B), with the utterance, question or turn a nondeterministic rule chooses made an argument. Ch. 4: greeting and counter-greeting, Free Speech, QSPEC, Ask and Assert QUD-incrementation, Assertion checking, Accept and Confirm, Fact update/QUD- downdate, QCoord. Ch. 6: Pending Update, Contextual Instantiation, pendification of a move-update rule (the move originates in PENDING), the two CCURs — Parameter Identification and Parameter Focussing, each merged with Utterance Interpolation — and CR Accommodation. §8.2: Backwards-looking appropriateness repair.

• greeting {P Fact Q : Type} : Rule P Fact Q
• counterGreeting {P Fact Q : Type} : Rule P Fact Q
• freeSpeech {P Fact Q : Type} (u : Utterance Fact Q) (t : Turn) : Rule P Fact Q
• qspec {P Fact Q : Type} (u : Utterance Fact Q) (t : Turn) : Rule P Fact Q
• askQud {P Fact Q : Type} : Rule P Fact Q
• assertQud {P Fact Q : Type} : Rule P Fact Q
• check {P Fact Q : Type} (u : Utterance Fact Q) (t : Turn) : Rule P Fact Q
• accept {P Fact Q : Type} (u : Utterance Fact Q) : Rule P Fact Q
• confirm {P Fact Q : Type} (u : Utterance Fact Q) : Rule P Fact Q
• factUpdate {P Fact Q : Type} : Rule P Fact Q
• qcoord {P Fact Q : Type} (u : Utterance Fact Q) : Rule P Fact Q
• pendingUpdate {P Fact Q : Type} (u : Utterance Fact Q) (speaker addressee : P) : Rule P Fact Q
• contextualInstantiation {P Fact Q : Type} (s : Finset Parameter) : Rule P Fact Q
• pendified {P Fact Q : Type} (r : Rule P Fact Q) : Rule P Fact Q
• parameterIdentification {P Fact Q : Type} (u : Discourse.SubUtterance grammar) (cr : Utterance Fact Q) : Rule P Fact Q
• parameterFocussing {P Fact Q : Type} (u : Discourse.SubUtterance grammar) (cr : Utterance Fact Q) : Rule P Fact Q
• crAccommodation {P Fact Q : Type} (u : Discourse.SubUtterance grammar) : Rule P Fact Q
• repair {P Fact Q : Type} (u : Discourse.SubUtterance grammar) (cr : Utterance Fact Q) : Rule P Fact Q

def Ginzburg2012.Rule.apply {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] : Rule P Fact Q → Board P Fact Q → Option (Board P Fact Q)

A rule as a partial map: none when the gameboard fails its preconditions. Accept, Confirm and the CCURs change the turn; Free Speech, QSPEC and checking leave it underspecified; the rest keep it. Contextual Instantiation witnesses the parameters s of MaxPending, as an agent does who believes their witnesses are the ones the speaker intended; CR Accommodation integrates the other party's clarification request, so the clarified speaker is the current addressee.

Equations

• One or more equations did not get rendered due to their size.
• Ginzburg2012.Rule.greeting.apply x✝ = match x✝.moves, x✝.qud with | [], [] => some (Discourse.Gameboard.recordMove x✝ (Ginzburg2012.ofMove Discourse.IllocutionaryAct.greet)) | x, x_1 => none
• (Ginzburg2012.Rule.freeSpeech u t).apply x✝ = match x✝.qud with | [] => some (Discourse.Gameboard.recordMove (t.act x✝) u) | x => none

def Ginzburg2012.run {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] (trace : List (Rule P Fact Q)) (d : Board P Fact Q) : Option (Board P Fact Q)

Apply a trace of rules in sequence (the composition of conversational rules).

Equations

• Ginzburg2012.run trace d = List.foldlM (fun (d : Ginzburg2012.Board P Fact Q) (r : Ginzburg2012.Rule P Fact Q) => r.apply d) d trace

def Ginzburg2012.Coherent {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] (d : Board P Fact Q) (u : Utterance Fact Q) : Prop

An utterance is coherent relative to a gameboard when some rule makes it the latest move (Ch. 4 M-Coherence; Appendix B Utterance Coherence).

Equations

• Ginzburg2012.Coherent d u = ∃ (r : Ginzburg2012.Rule P Fact Q) (d' : Ginzburg2012.Board P Fact Q), r.apply d = some d' ∧ Discourse.Gameboard.latestMove d' = some u

def Ginzburg2012.Reachable {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] (d d' : Board P Fact Q) : Prop

d' is a possible development of d.

Equations

• Ginzburg2012.Reachable d d' = ∃ (trace : List (Ginzburg2012.Rule P Fact Q)), Ginzburg2012.run trace d = some d'

QUD well-formedness

The Question Introduction Appropriateness Condition (52) p. 89 lets a question enter QUD only if no fact resolves it; (53) builds it into the gameboard type as non-resolve-cond, here the predicate Gameboard.NonResolveCond.

theorem Ginzburg2012.askQud_nonResolveCond_iff {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {d d' : Board P Fact Q} {q : Q} (hm : Discourse.Gameboard.latestContent d = some (Discourse.IllocutionaryAct.ask q)) (h : Rule.askQud.apply d = some d') : Discourse.Gameboard.NonResolveCond d' Content.Resolves ↔ (¬∃ f ∈ d.facts, Content.Resolves f q) ∧ Discourse.Gameboard.NonResolveCond d Content.Resolves

Ask QUD-incrementation keeps non-resolve-cond exactly when no fact resolves the question asked.

theorem Ginzburg2012.factUpdate_nonResolveCond {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {d d' : Board P Fact Q} (h : Rule.factUpdate.apply d = some d') : Discourse.Gameboard.NonResolveCond d' Content.Resolves

Fact update/QUD-downdate restores non-resolve-cond.

theorem Ginzburg2012.factUpdate_polar {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {d d' : Board P Fact Q} {p : Fact} (hm : Discourse.Gameboard.latestContent d = some (Discourse.IllocutionaryAct.accept p)) (h : Rule.factUpdate.apply d = some d') (i : Discourse.InformationStructure (domain P Fact Q).toGrammaticalDomain (domain P Fact Q).Question) : i ∈ d'.qud → i.question ≠ Content.polar p

Accepting p downdates p?.

Conversational genres (§4.6)

A genre is a type of the gameboards that end conversations of that kind (ex. 88 pp. 104–105), here a set of gameboards; the three genres of (88) differ only in the issues they require among the questions no longer under discussion. A move is relevant to a genre when some development of the gameboard after it is of that type, outcome(dgb, G) fulfilled (exx. 89–90 p. 105). Initiating Move (ex. 94 p. 108) is Free Speech restricted to moves the speaker takes to be relevant to the genre, which the private part of their information state records (ex. 93 p. 107); here the genre is an argument.

def Ginzburg2012.GenreRelevant {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] (G : Set (Board P Fact Q)) (d : Board P Fact Q) (u : Utterance Fact Q) : Prop

u is relevant to G in d when some development of d extended by u is of type G.

Equations

• Ginzburg2012.GenreRelevant G d u = ∃ (d' : Ginzburg2012.Board P Fact Q), Ginzburg2012.Reachable (Discourse.Gameboard.recordMove d u) d' ∧ d' ∈ G

def Ginzburg2012.IsInitiating {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] (G : Set (Board P Fact Q)) (d : Board P Fact Q) (u : Utterance Fact Q) : Prop

Initiating Move: with QUD empty, a move relevant to the assumed genre.

Equations

• Ginzburg2012.IsInitiating G d u = (d.qud = [] ∧ Ginzburg2012.GenreRelevant G d u)

theorem Ginzburg2012.coherent_of_isInitiating {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {G : Set (Board P Fact Q)} {d : Board P Fact Q} {u : Utterance Fact Q} (h : IsInitiating G d u) : Coherent d u

Every initiating move is coherent by Free Speech.

Self- and other-correction (§8.2)

Backwards-looking appropriateness repair (ex. 31 p. 287) is Parameter Identification (ex. 70 p. 192) without the turn change: the speaker of a pending utterance accommodates the issue of what they meant by one of its constituents and continues co-propositionally with it.

theorem Ginzburg2012.parameterIdentification_eq_repair_swapTurn {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] (u : Discourse.SubUtterance grammar) (cr : Utterance Fact Q) (d : Board P Fact Q) : (Rule.parameterIdentification u cr).apply d = Option.map Discourse.Gameboard.swapTurn ((Rule.repair u cr).apply d)

Parameter Identification is repair followed by a turn change.

The clarified constituent as focus-establishing constituent

In the final versions of the clarification rules (Appendix B (26e) p. 374, and (31) p. 287 for repair), MaxQUD is paired with the clarified sub-utterance, a constituent of the maximal pending utterance, as its focus-establishing constituent, which a reprise fragment must then match in category (p. 254).

theorem Ginzburg2012.focusEstablishing_parameterIdentification {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {u : Discourse.SubUtterance grammar} {cr : Utterance Fact Q} {d d' : Board P Fact Q} (h : (Rule.parameterIdentification u cr).apply d = some d') : (∃ v ∈ d.pending.head?, u ∈ v.constituents) ∧ Option.map (fun (x : Discourse.InformationStructure (domain P Fact Q).toGrammaticalDomain (domain P Fact Q).Question) => x.focusEstablishing) d'.qud.head? = some {u}

theorem Ginzburg2012.focusEstablishing_parameterFocussing {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {u : Discourse.SubUtterance grammar} {cr : Utterance Fact Q} {d d' : Board P Fact Q} (h : (Rule.parameterFocussing u cr).apply d = some d') : (∃ v ∈ d.pending.head?, u ∈ v.constituents) ∧ Option.map (fun (x : Discourse.InformationStructure (domain P Fact Q).toGrammaticalDomain (domain P Fact Q).Question) => x.focusEstablishing) d'.qud.head? = some {u}

theorem Ginzburg2012.focusEstablishing_repair {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {u : Discourse.SubUtterance grammar} {cr : Utterance Fact Q} {d d' : Board P Fact Q} (h : (Rule.repair u cr).apply d = some d') : (∃ v ∈ d.pending.head?, u ∈ v.constituents) ∧ Option.map (fun (x : Discourse.InformationStructure (domain P Fact Q).toGrammaticalDomain (domain P Fact Q).Question) => x.focusEstablishing) d'.qud.head? = some {u}

Worked traces (Ch. 4)

The book abbreviates contents as qᵢ and pᵢ and tabulates each trace as the sequence of rules applied with the gameboard they produce. The schematic content types below fix exactly the relations each trace's side conditions require.

def Ginzburg2012.initial {Fact Q : Type} [DecidableEq Fact] [DecidableEq Q] (facts : Finset Fact := ∅) : Board Agent Fact Q

The initial gameboard: A addressing B, with no moves.

Equations

• Ginzburg2012.initial facts = { speaker := Ginzburg2012.Agent.A, addressee := Ginzburg2012.Agent.B, facts := facts }

def Ginzburg2012.table {Fact Q : Type} [DecidableEq Fact] [DecidableEq Q] (d : Board Agent Fact Q) : Finset Fact × List Q × List (Discourse.IllocutionaryAct Fact Q)

The columns of a trace table: FACTS, QUD and the contents of MOVES.

Equations

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

Trace (66) p. 95 of dialogue (65): q₀ who to invite, q₁ who will agree to come (influencing q₀), p₁ an answer resolving q₁, p₂ About q₀; and trace (68) p. 95 of dialogue (67): A asserts p₁, checks it, B confirms.

inductive Ginzburg2012.Ex66.Fact : Type

• p₁ : Fact
• p₂ : Fact

@[instance_reducible]

instance Ginzburg2012.Ex66.instDecidableEqFact : DecidableEq Fact

Equations

• Ginzburg2012.Ex66.instDecidableEqFact x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Ginzburg2012.Ex66.instReprFact : Repr Fact

Equations

• Ginzburg2012.Ex66.instReprFact = { reprPrec := Ginzburg2012.Ex66.instReprFact.repr }

def Ginzburg2012.Ex66.instReprFact.repr : Fact → ℕ → Std.Format

Equations

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

inductive Ginzburg2012.Ex66.Q : Type

• q₀ : Q
• q₁ : Q
• polar (p : Fact) : Q

@[instance_reducible]

instance Ginzburg2012.Ex66.instDecidableEqQ : DecidableEq Q

Equations

• Ginzburg2012.Ex66.instDecidableEqQ = Ginzburg2012.Ex66.instDecidableEqQ.decEq

def Ginzburg2012.Ex66.instDecidableEqQ.decEq (x✝ x✝¹ : Q) : Decidable (x✝ = x✝¹)

Equations

• Ginzburg2012.Ex66.instDecidableEqQ.decEq Ginzburg2012.Ex66.Q.q₀ Ginzburg2012.Ex66.Q.q₀ = isTrue ⋯
• Ginzburg2012.Ex66.instDecidableEqQ.decEq Ginzburg2012.Ex66.Q.q₀ Ginzburg2012.Ex66.Q.q₁ = isFalse Ginzburg2012.Ex66.instDecidableEqQ.decEq._proof_3
• Ginzburg2012.Ex66.instDecidableEqQ.decEq Ginzburg2012.Ex66.Q.q₀ (Ginzburg2012.Ex66.Q.polar p) = isFalse ⋯
• Ginzburg2012.Ex66.instDecidableEqQ.decEq Ginzburg2012.Ex66.Q.q₁ Ginzburg2012.Ex66.Q.q₀ = isFalse Ginzburg2012.Ex66.instDecidableEqQ.decEq._proof_5
• Ginzburg2012.Ex66.instDecidableEqQ.decEq Ginzburg2012.Ex66.Q.q₁ Ginzburg2012.Ex66.Q.q₁ = isTrue ⋯
• Ginzburg2012.Ex66.instDecidableEqQ.decEq Ginzburg2012.Ex66.Q.q₁ (Ginzburg2012.Ex66.Q.polar p) = isFalse ⋯
• Ginzburg2012.Ex66.instDecidableEqQ.decEq (Ginzburg2012.Ex66.Q.polar p) Ginzburg2012.Ex66.Q.q₀ = isFalse ⋯
• Ginzburg2012.Ex66.instDecidableEqQ.decEq (Ginzburg2012.Ex66.Q.polar p) Ginzburg2012.Ex66.Q.q₁ = isFalse ⋯
• Ginzburg2012.Ex66.instDecidableEqQ.decEq (Ginzburg2012.Ex66.Q.polar a) (Ginzburg2012.Ex66.Q.polar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Ginzburg2012.Ex66.instReprQ : Repr Q

Equations

• Ginzburg2012.Ex66.instReprQ = { reprPrec := Ginzburg2012.Ex66.instReprQ.repr }

def Ginzburg2012.Ex66.instReprQ.repr : Q → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Ginzburg2012.Ex66.instReprQ.repr Ginzburg2012.Ex66.Q.q₀ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.Ex66.Q.q₀")).group prec✝
• Ginzburg2012.Ex66.instReprQ.repr Ginzburg2012.Ex66.Q.q₁ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.Ex66.Q.q₁")).group prec✝

@[instance_reducible]

instance Ginzburg2012.Ex66.instContentFactQ : Content Fact Q

Equations

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

@[instance_reducible]

instance Ginzburg2012.Ex66.instClarifiableAgentFactQ : Clarifiable Agent Fact Q

Equations

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

def Ginzburg2012.Ex66.trace66 : List (Rule Agent Fact Q)

A asks q₀; B asks q₁; A asserts p₁; B accepts; B asserts p₂; A accepts.

Equations

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

theorem Ginzburg2012.Ex66.trace : Option.map table (run trace66 initial) = some ({Fact.p₁, Fact.p₂}, [Q.q₀], [Discourse.IllocutionaryAct.ask Q.q₀, Discourse.IllocutionaryAct.ask Q.q₁, Discourse.IllocutionaryAct.assert Fact.p₁, Discourse.IllocutionaryAct.accept Fact.p₁, Discourse.IllocutionaryAct.assert Fact.p₂, Discourse.IllocutionaryAct.accept Fact.p₂])

After (65): FACTS {p₁, p₂}, QUD ⟨q₀⟩, the six moves recorded.

def Ginzburg2012.Ex66.trace68 : List (Rule Agent Fact Q)

A asserts p₁, checks it, B confirms.

Equations

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

theorem Ginzburg2012.Ex66.trace68_table : Option.map table (run trace68 initial) = some ({Fact.p₁}, [], [Discourse.IllocutionaryAct.assert Fact.p₁, Discourse.IllocutionaryAct.check Fact.p₁, Discourse.IllocutionaryAct.confirm Fact.p₁])

After (67): FACTS {p₁} and QUD empty.

Trace (79) p. 99 of dialogue (78): q₀ whom Max invites, q₁ when the guests arrive, not influencing q₀; p₀ resolves q₀, p₁ is About q₁.

inductive Ginzburg2012.Ex79.Fact : Type

• p₀ : Fact
• p₁ : Fact

@[instance_reducible]

instance Ginzburg2012.Ex79.instDecidableEqFact : DecidableEq Fact

Equations

• Ginzburg2012.Ex79.instDecidableEqFact x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ginzburg2012.Ex79.instReprFact.repr : Fact → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Ginzburg2012.Ex79.instReprFact : Repr Fact

Equations

• Ginzburg2012.Ex79.instReprFact = { reprPrec := Ginzburg2012.Ex79.instReprFact.repr }

inductive Ginzburg2012.Ex79.Q : Type

• q₀ : Q
• q₁ : Q
• polar (p : Fact) : Q

def Ginzburg2012.Ex79.instDecidableEqQ.decEq (x✝ x✝¹ : Q) : Decidable (x✝ = x✝¹)

Equations

• Ginzburg2012.Ex79.instDecidableEqQ.decEq Ginzburg2012.Ex79.Q.q₀ Ginzburg2012.Ex79.Q.q₀ = isTrue ⋯
• Ginzburg2012.Ex79.instDecidableEqQ.decEq Ginzburg2012.Ex79.Q.q₀ Ginzburg2012.Ex79.Q.q₁ = isFalse Ginzburg2012.Ex79.instDecidableEqQ.decEq._proof_3
• Ginzburg2012.Ex79.instDecidableEqQ.decEq Ginzburg2012.Ex79.Q.q₀ (Ginzburg2012.Ex79.Q.polar p) = isFalse ⋯
• Ginzburg2012.Ex79.instDecidableEqQ.decEq Ginzburg2012.Ex79.Q.q₁ Ginzburg2012.Ex79.Q.q₀ = isFalse Ginzburg2012.Ex79.instDecidableEqQ.decEq._proof_5
• Ginzburg2012.Ex79.instDecidableEqQ.decEq Ginzburg2012.Ex79.Q.q₁ Ginzburg2012.Ex79.Q.q₁ = isTrue ⋯
• Ginzburg2012.Ex79.instDecidableEqQ.decEq Ginzburg2012.Ex79.Q.q₁ (Ginzburg2012.Ex79.Q.polar p) = isFalse ⋯
• Ginzburg2012.Ex79.instDecidableEqQ.decEq (Ginzburg2012.Ex79.Q.polar p) Ginzburg2012.Ex79.Q.q₀ = isFalse ⋯
• Ginzburg2012.Ex79.instDecidableEqQ.decEq (Ginzburg2012.Ex79.Q.polar p) Ginzburg2012.Ex79.Q.q₁ = isFalse ⋯
• Ginzburg2012.Ex79.instDecidableEqQ.decEq (Ginzburg2012.Ex79.Q.polar a) (Ginzburg2012.Ex79.Q.polar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Ginzburg2012.Ex79.instDecidableEqQ : DecidableEq Q

Equations

• Ginzburg2012.Ex79.instDecidableEqQ = Ginzburg2012.Ex79.instDecidableEqQ.decEq

@[instance_reducible]

instance Ginzburg2012.Ex79.instReprQ : Repr Q

Equations

• Ginzburg2012.Ex79.instReprQ = { reprPrec := Ginzburg2012.Ex79.instReprQ.repr }

def Ginzburg2012.Ex79.instReprQ.repr : Q → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Ginzburg2012.Ex79.instReprQ.repr Ginzburg2012.Ex79.Q.q₀ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.Ex79.Q.q₀")).group prec✝
• Ginzburg2012.Ex79.instReprQ.repr Ginzburg2012.Ex79.Q.q₁ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.Ex79.Q.q₁")).group prec✝

@[instance_reducible]

instance Ginzburg2012.Ex79.instContentFactQ : Content Fact Q

Equations

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

@[instance_reducible]

instance Ginzburg2012.Ex79.instClarifiableAgentFactQ : Clarifiable Agent Fact Q

Equations

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

def Ginzburg2012.Ex79.trace79 : List (Rule Agent Fact Q)

A asks q₀ then q₁ (QCoord); B answers q₀; A accepts; B answers q₁.

Equations

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

theorem Ginzburg2012.Ex79.trace : Option.map table (run trace79 initial) = some ({Fact.p₀}, [Q.polar Fact.p₁, Q.q₁], [Discourse.IllocutionaryAct.ask Q.q₀, Discourse.IllocutionaryAct.ask Q.q₁, Discourse.IllocutionaryAct.assert Fact.p₀, Discourse.IllocutionaryAct.accept Fact.p₀, Discourse.IllocutionaryAct.assert Fact.p₁])

After (78): FACTS {p₀}, QUD ⟨p₁?, q₁⟩.

Activity relevance: dialogue (95) p. 108

B takes the genre to be CasualChat (ex. 88a), whose anticipated issues are how A is and how B is. "I'm off" is About the latter and, once accepted, resolves it; that A is present already resolves the former.

inductive Ginzburg2012.Ex95.Fact : Type

• here : Fact
• off : Fact

@[instance_reducible]

instance Ginzburg2012.Ex95.instDecidableEqFact : DecidableEq Fact

Equations

• Ginzburg2012.Ex95.instDecidableEqFact x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Ginzburg2012.Ex95.instReprFact : Repr Fact

Equations

• Ginzburg2012.Ex95.instReprFact = { reprPrec := Ginzburg2012.Ex95.instReprFact.repr }

def Ginzburg2012.Ex95.instReprFact.repr : Fact → ℕ → Std.Format

Equations

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

inductive Ginzburg2012.Ex95.Q : Type

• howA : Q
• howB : Q
• polar (p : Fact) : Q

@[instance_reducible]

instance Ginzburg2012.Ex95.instDecidableEqQ : DecidableEq Q

Equations

• Ginzburg2012.Ex95.instDecidableEqQ = Ginzburg2012.Ex95.instDecidableEqQ.decEq

def Ginzburg2012.Ex95.instDecidableEqQ.decEq (x✝ x✝¹ : Q) : Decidable (x✝ = x✝¹)

Equations

• Ginzburg2012.Ex95.instDecidableEqQ.decEq Ginzburg2012.Ex95.Q.howA Ginzburg2012.Ex95.Q.howA = isTrue ⋯
• Ginzburg2012.Ex95.instDecidableEqQ.decEq Ginzburg2012.Ex95.Q.howA Ginzburg2012.Ex95.Q.howB = isFalse Ginzburg2012.Ex95.instDecidableEqQ.decEq._proof_3
• Ginzburg2012.Ex95.instDecidableEqQ.decEq Ginzburg2012.Ex95.Q.howA (Ginzburg2012.Ex95.Q.polar p) = isFalse ⋯
• Ginzburg2012.Ex95.instDecidableEqQ.decEq Ginzburg2012.Ex95.Q.howB Ginzburg2012.Ex95.Q.howA = isFalse Ginzburg2012.Ex95.instDecidableEqQ.decEq._proof_5
• Ginzburg2012.Ex95.instDecidableEqQ.decEq Ginzburg2012.Ex95.Q.howB Ginzburg2012.Ex95.Q.howB = isTrue ⋯
• Ginzburg2012.Ex95.instDecidableEqQ.decEq Ginzburg2012.Ex95.Q.howB (Ginzburg2012.Ex95.Q.polar p) = isFalse ⋯
• Ginzburg2012.Ex95.instDecidableEqQ.decEq (Ginzburg2012.Ex95.Q.polar p) Ginzburg2012.Ex95.Q.howA = isFalse ⋯
• Ginzburg2012.Ex95.instDecidableEqQ.decEq (Ginzburg2012.Ex95.Q.polar p) Ginzburg2012.Ex95.Q.howB = isFalse ⋯
• Ginzburg2012.Ex95.instDecidableEqQ.decEq (Ginzburg2012.Ex95.Q.polar a) (Ginzburg2012.Ex95.Q.polar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Ginzburg2012.Ex95.instReprQ.repr : Q → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Ginzburg2012.Ex95.instReprQ.repr Ginzburg2012.Ex95.Q.howA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.Ex95.Q.howA")).group prec✝
• Ginzburg2012.Ex95.instReprQ.repr Ginzburg2012.Ex95.Q.howB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.Ex95.Q.howB")).group prec✝

@[instance_reducible]

instance Ginzburg2012.Ex95.instReprQ : Repr Q

Equations

• Ginzburg2012.Ex95.instReprQ = { reprPrec := Ginzburg2012.Ex95.instReprQ.repr }

@[instance_reducible]

instance Ginzburg2012.Ex95.instContentFactQ : Content Fact Q

Equations

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

@[instance_reducible]

instance Ginzburg2012.Ex95.instClarifiableAgentFactQ : Clarifiable Agent Fact Q

Equations

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

def Ginzburg2012.Ex95.casualChat : Set (Board Agent Fact Q)

CasualChat (88a) is the type of the gameboards that end a conversation in which the issues λP.P(A) and λP.P(B) have been resolved, with nothing left under discussion.

Equations

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

@[instance_reducible]

instance Ginzburg2012.Ex95.instDecidablePredBoardAgentFactQMemSetCasualChat : DecidablePred fun (x : Board Agent Fact Q) => x ∈ casualChat

Equations

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

theorem Ginzburg2012.Ex95.initiating_off : IsInitiating casualChat (Discourse.Gameboard.recordMove (initial {Fact.here}) (ofMove Discourse.IllocutionaryAct.greet)) (ofMove (Discourse.IllocutionaryAct.assert Fact.off))

After A's greeting, "I'm off" is an initiating move relative to CasualChat: B's assertion, accepted by A, resolves how B is.

Grounding and clarification: dialogue (90) of Ch. 6, p. 201

A asks whether George is here. A, omniscient about her own utterance, instantiates its contextual parameter and integrates it; B cannot, and initiates clarification by Parameter Focussing with "Is WHO here?". After that utterance the two gameboards are those of Ch. 6 (91) p. 202: A has p? under discussion and B's clarification request pending; B has the question who A is asking about under discussion and A's utterance pending.

inductive Ginzburg2012.George.Fact : Type

• georgeHere : Fact

@[instance_reducible]

instance Ginzburg2012.George.instDecidableEqFact : DecidableEq Fact

Equations

• Ginzburg2012.George.instDecidableEqFact x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ginzburg2012.George.instReprFact.repr : Fact → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Ginzburg2012.George.instReprFact : Repr Fact

Equations

• Ginzburg2012.George.instReprFact = { reprPrec := Ginzburg2012.George.instReprFact.repr }

inductive Ginzburg2012.George.Q : Type

p?; λx.Ask(A, B, ?In(l, x)), the focussed question; and λx.Mean(A, u, x).

• polar (p : Fact) : Q
• whoAsked : Q
• meant (u : Discourse.SubUtterance grammar) : Q

@[instance_reducible]

instance Ginzburg2012.George.instDecidableEqQ : DecidableEq Q

Equations

• Ginzburg2012.George.instDecidableEqQ = Ginzburg2012.George.instDecidableEqQ.decEq

def Ginzburg2012.George.instDecidableEqQ.decEq (x✝ x✝¹ : Q) : Decidable (x✝ = x✝¹)

Equations

• Ginzburg2012.George.instDecidableEqQ.decEq (Ginzburg2012.George.Q.polar a) (Ginzburg2012.George.Q.polar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Ginzburg2012.George.instDecidableEqQ.decEq (Ginzburg2012.George.Q.polar p) Ginzburg2012.George.Q.whoAsked = isFalse ⋯
• Ginzburg2012.George.instDecidableEqQ.decEq (Ginzburg2012.George.Q.polar p) (Ginzburg2012.George.Q.meant u) = isFalse ⋯
• Ginzburg2012.George.instDecidableEqQ.decEq Ginzburg2012.George.Q.whoAsked (Ginzburg2012.George.Q.polar p) = isFalse ⋯
• Ginzburg2012.George.instDecidableEqQ.decEq Ginzburg2012.George.Q.whoAsked Ginzburg2012.George.Q.whoAsked = isTrue ⋯
• Ginzburg2012.George.instDecidableEqQ.decEq Ginzburg2012.George.Q.whoAsked (Ginzburg2012.George.Q.meant u) = isFalse ⋯
• Ginzburg2012.George.instDecidableEqQ.decEq (Ginzburg2012.George.Q.meant u) (Ginzburg2012.George.Q.polar p) = isFalse ⋯
• Ginzburg2012.George.instDecidableEqQ.decEq (Ginzburg2012.George.Q.meant u) Ginzburg2012.George.Q.whoAsked = isFalse ⋯
• Ginzburg2012.George.instDecidableEqQ.decEq (Ginzburg2012.George.Q.meant a) (Ginzburg2012.George.Q.meant b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Ginzburg2012.George.instContentFactQ : Content Fact Q

Equations

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

@[instance_reducible]

instance Ginzburg2012.George.instClarifiableAgentFactQ : Clarifiable Agent Fact Q

Equations

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

def Ginzburg2012.George.george : Discourse.SubUtterance grammar

The sub-utterance "George".

Equations

• Ginzburg2012.George.george = { form := "George", category := Ginzburg2012.Category.np, denotation := Ginzburg2012.Parameter.george }

def Ginzburg2012.George.u₀ : Utterance Fact Q

A's utterance, with the referent of "George" a contextual parameter.

Equations

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

def Ginzburg2012.George.w₀ : Utterance Fact Q

A's utterance with its parameter witnessed.

Equations

• Ginzburg2012.George.w₀ = Discourse.LocutionaryProposition.instantiate Ginzburg2012.George.u₀ {Ginzburg2012.Parameter.george}

def Ginzburg2012.George.u₁ : Utterance Fact Q

B's clarification request.

Equations

• Ginzburg2012.George.u₁ = { form := "Is WHO here?", category := Ginzburg2012.Category.s, content := Discourse.IllocutionaryAct.ask Ginzburg2012.George.Q.whoAsked }

def Ginzburg2012.George.traceA : List (Rule Agent Fact Q)

A: utter u₀, instantiate it, integrate it by Free Speech, hear u₁.

Equations

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

def Ginzburg2012.George.traceB : List (Rule Agent Fact Q)

B: hear u₀, clarify by Parameter Focussing with u₁.

Equations

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

theorem Ginzburg2012.George.dgb_A : run traceA initial = some { speaker := Agent.B, addressee := Agent.A, moves := [w₀], pending := [u₁], qud := [{ question := Q.polar Fact.georgeHere }] }

(91b): A's gameboard.

theorem Ginzburg2012.George.dgb_B : run traceB initial = some { speaker := Agent.B, addressee := Agent.A, moves := [u₁], pending := [u₀], qud := [{ question := Q.whoAsked, focusEstablishing := {george} }] }

(91c): B's gameboard.

theorem Ginzburg2012.George.differ (dA : Board Agent Fact Q) : dA ∈ run traceA initial → ∀ dB ∈ run traceB initial, dA.qud ≠ dB.qud ∧ dA.pending ≠ dB.pending

The two participants have processed the same utterances and disagree on QUD and on PENDING.

theorem Ginzburg2012.George.accommodate : Option.map (fun (d : Board Agent Fact Q) => (List.map (fun (x : Discourse.InformationStructure (domain Agent Fact Q).toGrammaticalDomain (domain Agent Fact Q).Question) => x.question) d.qud, d.pending)) (run (traceA ++ [Rule.crAccommodation george]) initial) = some ([Q.whoAsked, Q.polar Fact.georgeHere], [])

A integrates B's request by CR Accommodation: the focussed question becomes MaxQUD and the request is no longer pending.

Who holds the turn (Chs. 1 and 8)

Only the addressee has the two clarification-request readings of "Bo?" and only the original speaker its self-correction reading (ex. 22); bare "Why?" is resolved differently by whoever holds the turn, the Turn-Taking Puzzle (ex. 23); and mid-utterance self-repair is the within-utterance analogue of a clarification request (ex. 24). Each turns on the turn a rule leaves, a general property of the inventory.

theorem Ginzburg2012.speaker_parameterIdentification {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {d d' : Board P Fact Q} {u : Discourse.SubUtterance grammar} {cr : Utterance Fact Q} (h : (Rule.parameterIdentification u cr).apply d = some d') : d'.speaker = d.addressee

Parameter Identification passes the turn to the clarifier.

theorem Ginzburg2012.speaker_parameterFocussing {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {d d' : Board P Fact Q} {u : Discourse.SubUtterance grammar} {cr : Utterance Fact Q} (h : (Rule.parameterFocussing u cr).apply d = some d') : d'.speaker = d.addressee

Parameter Focussing passes the turn to the clarifier.

theorem Ginzburg2012.speaker_repair {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {d d' : Board P Fact Q} {u : Discourse.SubUtterance grammar} {cr : Utterance Fact Q} (h : (Rule.repair u cr).apply d = some d') : d'.speaker = d.speaker

Repair keeps the turn.

theorem Ginzburg2012.speaker_qspec {P Fact Q : Type} [DecidableEq P] [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {d d' : Board P Fact Q} {u : Utterance Fact Q} {t : Turn} (h : (Rule.qspec u t).apply d = some d') : d'.speaker = (t.act d).speaker

QSPEC leaves the turn to its argument.

The rows of exx. 22–24: A asks about Bo, or which members of the audience own a parakeet, and either A or B follows with "Bo?" or "Why?".

inductive Ginzburg2012.Ex22.Fact : Type

• p₀ : Fact

@[instance_reducible]

instance Ginzburg2012.Ex22.instDecidableEqFact : DecidableEq Fact

Equations

• Ginzburg2012.Ex22.instDecidableEqFact x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ginzburg2012.Ex22.instReprFact.repr : Fact → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Ginzburg2012.Ex22.instReprFact : Repr Fact

Equations

• Ginzburg2012.Ex22.instReprFact = { reprPrec := Ginzburg2012.Ex22.instReprFact.repr }

inductive Ginzburg2012.Ex22.Q : Type

A's question, the follow-up why influencing it, p?, and λx.Mean(A, u, x).

• q₀ : Q
• why : Q
• polar (p : Fact) : Q
• meant (u : Discourse.SubUtterance grammar) : Q

def Ginzburg2012.Ex22.instDecidableEqQ.decEq (x✝ x✝¹ : Q) : Decidable (x✝ = x✝¹)

Equations

• Ginzburg2012.Ex22.instDecidableEqQ.decEq Ginzburg2012.Ex22.Q.q₀ Ginzburg2012.Ex22.Q.q₀ = isTrue ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq Ginzburg2012.Ex22.Q.q₀ Ginzburg2012.Ex22.Q.why = isFalse Ginzburg2012.Ex22.instDecidableEqQ.decEq._proof_3
• Ginzburg2012.Ex22.instDecidableEqQ.decEq Ginzburg2012.Ex22.Q.q₀ (Ginzburg2012.Ex22.Q.polar p) = isFalse ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq Ginzburg2012.Ex22.Q.q₀ (Ginzburg2012.Ex22.Q.meant u) = isFalse ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq Ginzburg2012.Ex22.Q.why Ginzburg2012.Ex22.Q.q₀ = isFalse Ginzburg2012.Ex22.instDecidableEqQ.decEq._proof_6
• Ginzburg2012.Ex22.instDecidableEqQ.decEq Ginzburg2012.Ex22.Q.why Ginzburg2012.Ex22.Q.why = isTrue ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq Ginzburg2012.Ex22.Q.why (Ginzburg2012.Ex22.Q.polar p) = isFalse ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq Ginzburg2012.Ex22.Q.why (Ginzburg2012.Ex22.Q.meant u) = isFalse ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq (Ginzburg2012.Ex22.Q.polar p) Ginzburg2012.Ex22.Q.q₀ = isFalse ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq (Ginzburg2012.Ex22.Q.polar p) Ginzburg2012.Ex22.Q.why = isFalse ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq (Ginzburg2012.Ex22.Q.polar a) (Ginzburg2012.Ex22.Q.polar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq (Ginzburg2012.Ex22.Q.polar p) (Ginzburg2012.Ex22.Q.meant u) = isFalse ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq (Ginzburg2012.Ex22.Q.meant u) Ginzburg2012.Ex22.Q.q₀ = isFalse ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq (Ginzburg2012.Ex22.Q.meant u) Ginzburg2012.Ex22.Q.why = isFalse ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq (Ginzburg2012.Ex22.Q.meant u) (Ginzburg2012.Ex22.Q.polar p) = isFalse ⋯
• Ginzburg2012.Ex22.instDecidableEqQ.decEq (Ginzburg2012.Ex22.Q.meant a) (Ginzburg2012.Ex22.Q.meant b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Ginzburg2012.Ex22.instDecidableEqQ : DecidableEq Q

Equations

• Ginzburg2012.Ex22.instDecidableEqQ = Ginzburg2012.Ex22.instDecidableEqQ.decEq

@[instance_reducible]

instance Ginzburg2012.Ex22.instContentFactQ : Content Fact Q

Equations

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

@[instance_reducible]

instance Ginzburg2012.Ex22.instClarifiableAgentFactQ : Clarifiable Agent Fact Q

Equations

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

def Ginzburg2012.Ex22.bo : Discourse.SubUtterance grammar

The sub-utterance "Bo".

Equations

• Ginzburg2012.Ex22.bo = { form := "Bo", category := Ginzburg2012.Category.np, denotation := Ginzburg2012.Parameter.bo }

def Ginzburg2012.Ex22.u₀ : Utterance Fact Q

A's question, with the referent of "Bo" a contextual parameter.

Equations

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

inductive Ginzburg2012.Ex22.Construction : Type

The construction of a row: a clarification request by the addressee, a self-repair by the original speaker, or a bare follow-up question.

• clarification : Construction
• selfRepair : Construction
• followUp : Construction

@[instance_reducible]

instance Ginzburg2012.Ex22.instDecidableEqConstruction : DecidableEq Construction

Equations

• Ginzburg2012.Ex22.instDecidableEqConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Ginzburg2012.Ex22.instReprConstruction : Repr Construction

Equations

• Ginzburg2012.Ex22.instReprConstruction = { reprPrec := Ginzburg2012.Ex22.instReprConstruction.repr }

def Ginzburg2012.Ex22.instReprConstruction.repr : Construction → ℕ → Std.Format

Equations

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

structure Ginzburg2012.Ex22.Row : Type

A row: its construction and the turn the book records after it.

• construction : Construction
• turn : Turn

def Ginzburg2012.Ex22.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Ginzburg2012.Ex22.instDecidableEqRow : DecidableEq Row

Equations

• Ginzburg2012.Ex22.instDecidableEqRow = Ginzburg2012.Ex22.instDecidableEqRow.decEq

def Ginzburg2012.Ex22.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def Ginzburg2012.Ex22.Row.board (r : Row) : Board Agent Fact Q

The gameboard the row's second utterance meets: A's question pending, for a clarification request or a repair addressing its constituent "Bo", or under discussion, for a follow-up.

Equations

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

def Ginzburg2012.Ex22.Row.rule (r : Row) : Rule Agent Fact Q

The rule the construction instantiates: Parameter Identification or repair over "Bo", or QSPEC with the influencing why, taking whichever turn the row records.

Equations

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

def Ginzburg2012.Ex22.rows : List Row

The seven rows of exx. 22–24.

Equations

• Ginzburg2012.Ex22.rows = List.filterMap Ginzburg2012.Ex22.Row.ofDatum Ginzburg2012.Examples.all

theorem Ginzburg2012.Ex22.rows_turn (r : Row) : r ∈ rows → Option.map (fun (x : Board Agent Fact Q) => x.speaker) (r.rule.apply r.board) = some (r.turn.act r.board).speaker

Each row's rule applies to its gameboard and leaves the turn where the book records it.

Taxonomies

The clarification-request forms of the BNC study reported in §6.2.1 (Table 6.1 p. 153), and the non-sentential-utterance classes of Table 7.3 p. 221 with their functional grouping in Table 7.4 p. 222, Sluice split into its reprise and direct uses. Readings of clarification requests are RFReading.

inductive Ginzburg2012.CRForm : Type

The eight clarification-request forms (§6.2.1).

• wot : CRForm

  "Eh? / What? / Pardon?"

• explicit : CRForm

  A context-independent request, "What did you say?"

• literalReprise : CRForm

  Verbatim repetition of the troubled utterance

• whSubstitutedReprise : CRForm

  Repetition with a constituent replaced by a wh-phrase

• repriseSluice : CRForm

  A bare wh-phrase

• repriseFragment : CRForm

  A bare phrase

• gap : CRForm

  The sentence with the targeted constituent omitted

• filler : CRForm

  A guess completing an unfinished sentence

@[instance_reducible]

instance Ginzburg2012.instDecidableEqCRForm : DecidableEq CRForm

Equations

• Ginzburg2012.instDecidableEqCRForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ginzburg2012.instReprCRForm.repr : CRForm → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Ginzburg2012.instReprCRForm.repr Ginzburg2012.CRForm.wot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.CRForm.wot")).group prec✝
• Ginzburg2012.instReprCRForm.repr Ginzburg2012.CRForm.gap prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.CRForm.gap")).group prec✝
• Ginzburg2012.instReprCRForm.repr Ginzburg2012.CRForm.filler prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ginzburg2012.CRForm.filler")).group prec✝

@[instance_reducible]

instance Ginzburg2012.instReprCRForm : Repr CRForm

Equations

• Ginzburg2012.instReprCRForm = { reprPrec := Ginzburg2012.instReprCRForm.repr }

inductive Ginzburg2012.NSUFunction : Type

The functional grouping of Table 7.4.

• positiveFeedback : NSUFunction
• answer : NSUFunction
• metacommunicativeQuery : NSUFunction
• extensionMove : NSUFunction

@[instance_reducible]

instance Ginzburg2012.instDecidableEqNSUFunction : DecidableEq NSUFunction

Equations

• Ginzburg2012.instDecidableEqNSUFunction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ginzburg2012.instReprNSUFunction.repr : NSUFunction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Ginzburg2012.instReprNSUFunction : Repr NSUFunction

Equations

• Ginzburg2012.instReprNSUFunction = { reprPrec := Ginzburg2012.instReprNSUFunction.repr }

inductive Ginzburg2012.NSUClass : Type

The NSU classes of Table 7.3, with Sluice split as in Table 7.4.

• plainAcknowledgement : NSUClass

  "mmh"

• repeatedAcknowledgement : NSUClass

  "Bo, hmm."

• clarificationEllipsis : NSUClass

  "Bo?"

• checkQuestion : NSUClass

  "Okay?"

• repriseSluice : NSUClass

  "Who?" reprising the antecedent

• filler : NSUClass

  completing "Did Bo …" with "leave?"

• shortAnswer : NSUClass

  "Bo"

• affirmativeAnswer : NSUClass

  "Yes"

• rejection : NSUClass

  "No"

• repeatedAffirmativeAnswer : NSUClass

  "Bo, yes."

• helpfulRejection : NSUClass

  "No, Max."

• propositionalModifier : NSUClass

  "Maybe"

• factiveModifier : NSUClass

  "Great!"

• bareModifierPhrase : NSUClass

  "Yesterday"

• directSluice : NSUClass

  "Who?" requesting new information

• conjunctionFragment : NSUClass

  "And Max."

@[instance_reducible]

instance Ginzburg2012.instDecidableEqNSUClass : DecidableEq NSUClass

Equations

• Ginzburg2012.instDecidableEqNSUClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ginzburg2012.instReprNSUClass.repr : NSUClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Ginzburg2012.instReprNSUClass : Repr NSUClass

Equations

• Ginzburg2012.instReprNSUClass = { reprPrec := Ginzburg2012.instReprNSUClass.repr }

def Ginzburg2012.NSUClass.function : NSUClass → NSUFunction

The function of each class (Table 7.4).

Equations

• Ginzburg2012.NSUClass.plainAcknowledgement.function = Ginzburg2012.NSUFunction.positiveFeedback
• Ginzburg2012.NSUClass.repeatedAcknowledgement.function = Ginzburg2012.NSUFunction.positiveFeedback
• Ginzburg2012.NSUClass.clarificationEllipsis.function = Ginzburg2012.NSUFunction.metacommunicativeQuery
• Ginzburg2012.NSUClass.checkQuestion.function = Ginzburg2012.NSUFunction.metacommunicativeQuery
• Ginzburg2012.NSUClass.repriseSluice.function = Ginzburg2012.NSUFunction.metacommunicativeQuery
• Ginzburg2012.NSUClass.filler.function = Ginzburg2012.NSUFunction.metacommunicativeQuery
• Ginzburg2012.NSUClass.shortAnswer.function = Ginzburg2012.NSUFunction.answer
• Ginzburg2012.NSUClass.affirmativeAnswer.function = Ginzburg2012.NSUFunction.answer
• Ginzburg2012.NSUClass.rejection.function = Ginzburg2012.NSUFunction.answer
• Ginzburg2012.NSUClass.repeatedAffirmativeAnswer.function = Ginzburg2012.NSUFunction.answer
• Ginzburg2012.NSUClass.helpfulRejection.function = Ginzburg2012.NSUFunction.answer
• Ginzburg2012.NSUClass.propositionalModifier.function = Ginzburg2012.NSUFunction.answer
• Ginzburg2012.NSUClass.factiveModifier.function = Ginzburg2012.NSUFunction.extensionMove
• Ginzburg2012.NSUClass.bareModifierPhrase.function = Ginzburg2012.NSUFunction.extensionMove
• Ginzburg2012.NSUClass.directSluice.function = Ginzburg2012.NSUFunction.extensionMove
• Ginzburg2012.NSUClass.conjunctionFragment.function = Ginzburg2012.NSUFunction.extensionMove