Ginzburg (2012): The Interactive Stance

This file formalizes the conversational rules of [ginzburg-2012] over the dialogue gameboard DGB: 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). The Question Introduction Appropriateness Condition survives QUD-incrementation and is restored by FACTS update (askQud_nonResolveCond, factUpdate_nonResolveCond); a genre makes an initiating move a relevant Free Speech move (IsInitiating, coherent_of_isInitiating); and self-repair is Parameter Identification with the turn held (parameterIdentification_eq_repair_swapTurn).

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 (spkr_parameterIdentification, spkr_repair, spkr_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.
• 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.
• 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

• [ginzburg-2012]

class Ginzburg2012.Content (Fact Q : Type) extends Question.DecidableSupport Fact Q : 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?.

• supports : Fact → Q → Prop
• decSupports (s : Fact) (q : Q) : Decidable (Support.supports s q)
• polar : Fact → Q
• About : Fact → Q → Prop
• Influences : Q → Q → Prop
• decAbout : DecidableRel About
• decInfluences : DecidableRel (Influences Fact)
• supports_polar (p : Fact) : Question.Support.supports 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.Gameboard.SubUtterance → Q
• focus : Discourse.Gameboard.IllocMove Fact Q → Discourse.Gameboard.SubUtterance → Q

@[reducible, inline]

abbrev Ginzburg2012.Board (P Fact Q : Type) : Type

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

Equations

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

@[reducible, inline]

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

An utterance record.

Equations

• Ginzburg2012.Utt Fact Q = Discourse.Gameboard.LocProp (Discourse.Gameboard.IllocMove 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 ⋯

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✝

@[instance_reducible]

instance Ginzburg2012.instReprAgent : Repr Agent

Equations

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

def Ginzburg2012.ofMove {Fact Q : Type} (m : Discourse.Gameboard.IllocMove Fact Q) : Utt Fact Q

The utterance of a bare move, when only its content matters (Ch. 4).

Equations

• Ginzburg2012.ofMove m = { phon := "", cat := "", cont := m }

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

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

Equations

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

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

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

Equations

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

def Ginzburg2012.ContextuallyExtends {Fact Q : Type} (w u : Utt Fact Q) : Prop

w contextually extends u: the same utterance with some of its contextual parameters witnessed.

Equations

• Ginzburg2012.ContextuallyExtends w u = (w.phon = u.phon ∧ w.cat = u.cat ∧ w.cont = u.cont ∧ w.constits = u.constits ∧ ∀ c ∈ w.cparams, c ∈ u.cparams)

@[instance_reducible]

instance Ginzburg2012.instDecidableContextuallyExtends {Fact Q : Type} [DecidableEq Fact] [DecidableEq Q] (w u : Utt Fact Q) : Decidable (ContextuallyExtends w u)

Equations

• Ginzburg2012.instDecidableContextuallyExtends w u = Ginzburg2012.instDecidableContextuallyExtends._aux_1 w u

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} : 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.DGB.swapTurn x✝

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

The conversational rules of [ginzburg-2012] (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 : Utt Fact Q) (t : Turn) : Rule P Fact Q
• qspec {P Fact Q : Type} (u : Utt 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 : Utt Fact Q) (t : Turn) : Rule P Fact Q
• accept {P Fact Q : Type} (u : Utt Fact Q) : Rule P Fact Q
• confirm {P Fact Q : Type} (u : Utt Fact Q) : Rule P Fact Q
• factUpdate {P Fact Q : Type} : Rule P Fact Q
• qcoord {P Fact Q : Type} (u : Utt Fact Q) : Rule P Fact Q
• pendingUpdate {P Fact Q : Type} (u : Utt Fact Q) (spkr addr : P) : Rule P Fact Q
• contextualInstantiation {P Fact Q : Type} (w : Utt Fact Q) : 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.Gameboard.SubUtterance) (cr : Utt Fact Q) : Rule P Fact Q
• parameterFocussing {P Fact Q : Type} (u : Discourse.Gameboard.SubUtterance) (cr : Utt Fact Q) : Rule P Fact Q
• crAccommodation {P Fact Q : Type} (u : Discourse.Gameboard.SubUtterance) : Rule P Fact Q
• repair {P Fact Q : Type} (u : Discourse.Gameboard.SubUtterance) (cr : Utt Fact Q) : Rule P Fact Q

def Ginzburg2012.Rule.apply {P Fact Q : Type} [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 is applied by an agent who believes the witnessed record w is the one 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.freeSpeech u t).apply x✝ = match x✝.qud with | [] => some (Discourse.Gameboard.DGB.recordMove (t.act x✝) u) | x => none
• Ginzburg2012.Rule.askQud.apply x✝ = match Discourse.Gameboard.DGB.latestContent x✝ with | some (Discourse.Gameboard.IllocMove.ask q) => some (Discourse.Gameboard.DGB.pushQud x✝ q) | x => none

def Ginzburg2012.run {P Fact Q : Type} [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 Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] (d : Board P Fact Q) (u : Utt 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.DGB.latestMove d' = some u

def Ginzburg2012.Reachable {P Fact Q : Type} [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 — a question enters QUD only if no established fact resolves it — is built into the gameboard type as non-resolve-cond (DGB.nonResolveCond).

theorem Ginzburg2012.askQud_nonResolveCond {P Fact Q : Type} [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {d d' : Board P Fact Q} {q : Q} (hd : Discourse.Gameboard.DGB.nonResolveCond d) (hm : Discourse.Gameboard.DGB.latestContent d = some (Discourse.Gameboard.IllocMove.ask q)) (hq : ∀ f ∈ d.facts, ¬Question.Support.supports f q) (h : Rule.askQud.apply d = some d') : Discourse.Gameboard.DGB.nonResolveCond d'

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

theorem Ginzburg2012.factUpdate_nonResolveCond {P Fact Q : Type} [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.DGB.nonResolveCond d'

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

theorem Ginzburg2012.factUpdate_polar {P Fact Q : Type} [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {d d' : Board P Fact Q} {p : Fact} (hm : Discourse.Gameboard.DGB.latestContent d = some (Discourse.Gameboard.IllocMove.accept p)) (h : Rule.factUpdate.apply d = some d') (i : Discourse.Gameboard.InfoStruc Q (Discourse.Gameboard.IllocMove Fact Q)) : i ∈ d'.qud → i.q ≠ Content.polar p

Accepting p downdates p?.

Conversational genres (§4.6)

A genre is the type of a participant's information state at the end of a conversation of that kind (ex. 88 pp. 104–105); the qnud field lists the issues such a conversation raises and resolves. A gameboard fulfils the outcome outcome(dgb, G) (ex. 89 p. 105) when its QUD is empty and FACTS resolve every anticipated issue, and a move is relevant to a genre when some continuation after it fulfils the outcome (ex. 90 p. 105). Initiating Move (ex. 94 p. 108) is Free Speech restricted to moves the speaker takes to be relevant to the genre in the private part of their information state (TIS.priv.genre, ex. 93 p. 107).

def Ginzburg2012.Fulfilled {P Fact Q : Type} [Content Fact Q] (G : Discourse.Gameboard.GenreType Fact Q) (d : Board P Fact Q) : Prop

The outcome of d relative to G is fulfilled.

Equations

• Ginzburg2012.Fulfilled G d = (d.qud = [] ∧ ∀ q ∈ G.qnud, ∃ f ∈ d.facts, Question.Support.supports f q)

@[instance_reducible]

instance Ginzburg2012.instDecidableFulfilled {P Fact Q : Type} [Content Fact Q] (G : Discourse.Gameboard.GenreType Fact Q) (d : Board P Fact Q) : Decidable (Fulfilled G d)

Equations

• Ginzburg2012.instDecidableFulfilled G d = Ginzburg2012.instDecidableFulfilled._aux_1 G d

def Ginzburg2012.GenreRelevant {P Fact Q : Type} [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] (G : Discourse.Gameboard.GenreType Fact Q) (d : Board P Fact Q) (u : Utt Fact Q) : Prop

u is relevant to G in d: some development of d extended by u fulfils the outcome.

Equations

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

def Ginzburg2012.IsInitiating {P Fact Q : Type} [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] (G : Discourse.Gameboard.GenreType Fact Q) (d : Board P Fact Q) (u : Utt 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 Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {G : Discourse.Gameboard.GenreType Fact Q} {d : Board P Fact Q} {u : Utt 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 Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] (u : Discourse.Gameboard.SubUtterance) (cr : Utt Fact Q) (d : Board P Fact Q) : (Rule.parameterIdentification u cr).apply d = Option.map Discourse.Gameboard.DGB.swapTurn ((Rule.repair u cr).apply d)

Parameter Identification is repair followed by a turn change.

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} (facts : List Fact := []) : Board Agent Fact Q

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

Equations

• Ginzburg2012.initial facts = { spkr := some Ginzburg2012.Agent.A, addr := some Ginzburg2012.Agent.B, facts := facts }

def Ginzburg2012.table {Fact Q : Type} (d : Board Agent Fact Q) : List Fact × List Q × List (Discourse.Gameboard.IllocMove 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 ⋯

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

Equations

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

@[instance_reducible]

instance Ginzburg2012.Ex66.instReprFact : Repr Fact

Equations

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

inductive Ginzburg2012.Ex66.Q : Type

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

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_1
• 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_3
• 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.instDecidableEqQ : DecidableEq Q

Equations

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

@[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.Gameboard.IllocMove.ask Q.q₀, Discourse.Gameboard.IllocMove.ask Q.q₁, Discourse.Gameboard.IllocMove.assert Fact.p₁, Discourse.Gameboard.IllocMove.accept Fact.p₁, Discourse.Gameboard.IllocMove.assert Fact.p₂, Discourse.Gameboard.IllocMove.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.Gameboard.IllocMove.assert Fact.p₁, Discourse.Gameboard.IllocMove.check Fact.p₁, Discourse.Gameboard.IllocMove.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

@[instance_reducible]

instance Ginzburg2012.Ex79.instDecidableEqQ : DecidableEq Q

Equations

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

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_1
• 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_3
• 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.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.Gameboard.IllocMove.ask Q.q₀, Discourse.Gameboard.IllocMove.ask Q.q₁, Discourse.Gameboard.IllocMove.assert Fact.p₀, Discourse.Gameboard.IllocMove.accept Fact.p₀, Discourse.Gameboard.IllocMove.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 ⋯

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

Equations

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

@[instance_reducible]

instance Ginzburg2012.Ex95.instReprFact : Repr Fact

Equations

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

inductive Ginzburg2012.Ex95.Q : Type

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

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_1
• 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_3
• 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 ⋯

@[instance_reducible]

instance Ginzburg2012.Ex95.instDecidableEqQ : DecidableEq Q

Equations

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

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 : Discourse.Gameboard.GenreType Fact Q

CasualChat: the issues λP.P(A), λP.P(B) are to be discussed.

Equations

• Ginzburg2012.Ex95.casualChat = { name := "CasualChat", qnud := [Ginzburg2012.Ex95.Q.howA, Ginzburg2012.Ex95.Q.howB] }

theorem Ginzburg2012.Ex95.initiating_off : IsInitiating casualChat (Discourse.Gameboard.DGB.recordMove (initial [Fact.here]) (ofMove Discourse.Gameboard.IllocMove.greet)) (ofMove (Discourse.Gameboard.IllocMove.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 ⋯

@[instance_reducible]

instance Ginzburg2012.George.instReprFact : Repr Fact

Equations

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

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

Equations

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

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.Gameboard.SubUtterance) : 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 ⋯

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

Equations

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

@[instance_reducible]

instance Ginzburg2012.George.instReprQ : Repr Q

Equations

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

@[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.Gameboard.SubUtterance

The sub-utterance "George".

Equations

• Ginzburg2012.George.george = { phon := "George", cat := "NP", cont := "g" }

def Ginzburg2012.George.u₀ : Utt 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₀ : Utt Fact Q

A's utterance with its parameter witnessed.

Equations

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

def Ginzburg2012.George.u₁ : Utt Fact Q

B's clarification request.

Equations

• Ginzburg2012.George.u₁ = { phon := "Is WHO here?", cat := "S", cont := Discourse.Gameboard.IllocMove.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 { spkr := some Agent.B, addr := some Agent.A, moves := [w₀], pending := [u₁], qud := [Discourse.Gameboard.InfoStruc.fromQuestion (Q.polar Fact.georgeHere)] }

(91b): A's gameboard.

theorem Ginzburg2012.George.dgb_B : run traceB initial = some { spkr := some Agent.B, addr := some Agent.A, moves := [u₁], pending := [u₀], qud := [Discourse.Gameboard.InfoStruc.fromQuestion Q.whoAsked] }

(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.Gameboard.InfoStruc Q (Discourse.Gameboard.IllocMove Fact Q)) => x.q) 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.spkr_parameterIdentification {P Fact Q : Type} [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {d d' : Board P Fact Q} {u : Discourse.Gameboard.SubUtterance} {cr : Utt Fact Q} (h : (Rule.parameterIdentification u cr).apply d = some d') : d'.spkr = d.addr

Parameter Identification passes the turn to the clarifier.

theorem Ginzburg2012.spkr_parameterFocussing {P Fact Q : Type} [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {d d' : Board P Fact Q} {u : Discourse.Gameboard.SubUtterance} {cr : Utt Fact Q} (h : (Rule.parameterFocussing u cr).apply d = some d') : d'.spkr = d.addr

Parameter Focussing passes the turn to the clarifier.

theorem Ginzburg2012.spkr_repair {P Fact Q : Type} [DecidableEq Fact] [DecidableEq Q] [Content Fact Q] [Clarifiable P Fact Q] {d d' : Board P Fact Q} {u : Discourse.Gameboard.SubUtterance} {cr : Utt Fact Q} (h : (Rule.repair u cr).apply d = some d') : d'.spkr = d.spkr

Repair keeps the turn.

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

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.Gameboard.SubUtterance) : 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_1
• 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_4
• 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.instReprQ : Repr Q

Equations

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

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

Equations

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

@[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.Gameboard.SubUtterance

The sub-utterance "Bo".

Equations

• Ginzburg2012.Ex22.bo = { phon := "Bo", cat := "NP", cont := "b" }

def Ginzburg2012.Ex22.u₀ : Utt 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

@[instance_reducible]

instance Ginzburg2012.Ex22.instDecidableEqRow : DecidableEq Row

Equations

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

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

Equations

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

def Ginzburg2012.Ex22.Row.ofExample (ex : Data.Examples.LinguisticExample) : 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.ofExample Ginzburg2012.Examples.all

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

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