Documentation

Linglib.Phenomena.Dialogue.Studies.Ginzburg2012

Ginzburg (2012): The Interactive Stance #

@cite{ginzburg-2012}

Key empirical claims from @cite{ginzburg-2012} formalized against the KOS framework and verified with the existing DGB/TIS/conversational-rule machinery.

Claims Formalized #

Non-sentential utterances (Ch. 5): bare fragments ("Paris.") are resolved via QUD — the question on QUD determines the fragment's propositional content.
Assertion–QUD coupling (Ch. 4): asserting p pushes About(p) onto QUD; the addressee's acceptance resolves it.
Grounding asymmetry (Ch. 4): the speaker's DGB and addressee's DGB evolve differently — only acceptance synchronizes them.
Self-repair (Ch. 7): disfluencies are modeled via TurnUnderConstr in the private state.
Genre relevance (Ch. 4): initiating moves must be relevant to the conversational genre.
NSU taxonomy (Ch. 7, Tables 7.3–7.4): 15 empirical NSU classes from BNC corpus + 4 functional groupings.
Grounding protocol (Ch. 6): LocProp integration branches on cparam resolution — grounding vs CRification.
End-to-end chain (§10): DialogueSign → LocProp → integration → DGB update, with non-resolve-cond verification.

Non-Sentential Utterances #

@cite{ginzburg-2012} Ch. 1 (p. 2) cites estimates that ~30% of utterances are non-sentential (de Waijer 2001); the BNC corpus study in Ch. 7 (§7.2.2) finds 1,299 NSUs in 14,315 sentences (~9%). Their interpretation depends on the QUD — the same fragment "Paris" means different things depending on what question is under discussion:

QUD: "Where's Bo?" → "Paris" = "Bo is in Paris" QUD: "What's the capital of France?" → "Paris" = "Paris is the capital"

The key mechanism: the QUD's question structure determines which argument slot the fragment fills. This connects Phenomena/Ellipsis/FragmentAnswers.lean to the KOS framework.

structure Phenomena.Dialogue.Studies.Ginzburg2012.NSUDatum :

An NSU resolution datum: a fragment interpreted relative to a QUD.

qud : String
The question under discussion
fragment : String
The non-sentential utterance
resolution : String
The full propositional content derived from QUD + fragment
source : String
Source (chapter/page in Ginzburg 2012)

Instances For

instance Phenomena.Dialogue.Studies.Ginzburg2012.instReprNSUDatum :

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instReprNSUDatum = { reprPrec := Phenomena.Dialogue.Studies.Ginzburg2012.instReprNSUDatum.repr }

def Phenomena.Dialogue.Studies.Ginzburg2012.instReprNSUDatum.repr :

NSUDatum → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Dialogue.Studies.Ginzburg2012.nsuLocation :

"Where's Bo?" / "Paris" → "Bo is in Paris".

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.nsuLocation = { qud := "Where is Bo?", fragment := "Paris", resolution := "Bo is in Paris", source := "Ch. 5" }

Instances For

def Phenomena.Dialogue.Studies.Ginzburg2012.nsuSubject :

"Who called?" / "Bo" → "Bo called".

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.nsuSubject = { qud := "Who called?", fragment := "Bo", resolution := "Bo called", source := "Ch. 5" }

Instances For

def Phenomena.Dialogue.Studies.Ginzburg2012.nsuObject :

"What did Bo eat?" / "A sandwich" → "Bo ate a sandwich".

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.nsuObject = { qud := "What did Bo eat?", fragment := "A sandwich", resolution := "Bo ate a sandwich", source := "Ch. 5" }

Instances For

def Phenomena.Dialogue.Studies.Ginzburg2012.nsuPolar :

Bare "yes"/"no" as polar answer.

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.nsuPolar = { qud := "Did Bo leave?", fragment := "Yes", resolution := "Bo left", source := "Ch. 5" }

Instances For

def Phenomena.Dialogue.Studies.Ginzburg2012.nsuExamples :

Equations

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

Instances For

theorem Phenomena.Dialogue.Studies.Ginzburg2012.all_nsu_resolved :

(nsuExamples.all fun (d : NSUDatum) => !d.resolution.isEmpty) = true

All NSU examples have non-empty resolutions.

The Full Inquiry Cycle #

@cite{ginzburg-2012} Ch. 4 (p. 95, ex. 66): the canonical dialogue pattern.

A(1): "Is Bo here?" — Ask: pushes q onto QUD B(1): "Bo is here." — Assert: adds p to FACTS, pushes About(p), downdates A(2): accepts — Accept: adds p to own FACTS

We verify that:

After Ask, QUD is non-empty
After Assert (with QUD push), the original question is resolved
After Accept, the fact appears in both participants' views

instance Phenomena.Dialogue.Studies.Ginzburg2012.instAnswerhoodString :

Theories.Pragmatics.Dialogue.KOS.Answerhood String String

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instAnswerhoodString = { resolves := fun (fact question : String) => fact == question }

theorem Phenomena.Dialogue.Studies.Ginzburg2012.cycle_ask_qud_nonempty :

Phenomena.Dialogue.Studies.Ginzburg2012.cycle₁✝.dgb.qud ≠ []

QUD is non-empty after Ask.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.cycle_assert_resolves :

Phenomena.Dialogue.Studies.Ginzburg2012.cycle₂✝.dgb.qud = []

After Assert, the original question is resolved and QUD is empty.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.cycle_assert_has_fact :

"Bo is here" ∈ Phenomena.Dialogue.Studies.Ginzburg2012.cycle₂✝.dgb.facts

The fact is in FACTS.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.cycle_accept_duplicates :

Phenomena.Dialogue.Studies.Ginzburg2012.cycle₃✝.dgb.facts = ["Bo is here", "Bo is here"]

After Accept, the fact appears twice (speaker's assert + addressee's accept).

theorem Phenomena.Dialogue.Studies.Ginzburg2012.cycle_full_moves :

Phenomena.Dialogue.Studies.Ginzburg2012.cycle₃✝.dgb.moves = [Theories.Pragmatics.Dialogue.KOS.IllocMove.ask "Bo is here", Theories.Pragmatics.Dialogue.KOS.IllocMove.assert "Bo is here", Theories.Pragmatics.Dialogue.KOS.IllocMove.accept "Bo is here"]

The full move history is recorded.

Speaker vs Addressee DGBs #

@cite{ginzburg-2012} Ch. 4: each participant maintains their own DGB. After A asserts p, A's DGB has p in FACTS. B's DGB does NOT have p in FACTS until B explicitly accepts. This models the difference between assertion and mutual acceptance.

instance Phenomena.Dialogue.Studies.Ginzburg2012.instAnswerhoodString_1 :

Theories.Pragmatics.Dialogue.KOS.Answerhood String String

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instAnswerhoodString_1 = { resolves := fun (fact question : String) => fact == question }

theorem Phenomena.Dialogue.Studies.Ginzburg2012.grounding_asymmetry :

"It's raining" ∈ Phenomena.Dialogue.Studies.Ginzburg2012.speakerDGB✝.dgb.facts ∧ "It's raining" ∉ Phenomena.Dialogue.Studies.Ginzburg2012.addresseeDGBBefore✝.dgb.facts

Speaker has the fact; addressee does not.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.grounding_resolved :

"It's raining" ∈ Phenomena.Dialogue.Studies.Ginzburg2012.addresseeDGBAfter✝.dgb.facts

Disfluencies and Self-Repair #

@cite{ginzburg-2012} Ch. 7: self-repairs ("I went to the — to the store") are modeled via TurnUnderConstr. The speaker interrupts the current turn, revises it, and continues. The TuC tracks the partial content so that the repair can target the right constituent.

We model a simple self-repair: "I saw the, uh, the manager."

def Phenomena.Dialogue.Studies.Ginzburg2012.tucMidRepair :

Theories.Pragmatics.Dialogue.KOS.TurnUnderConstr

A TuC mid-repair: speaker has said "I saw the" and is about to correct.

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.tucMidRepair = { phonSoFar := "I saw the", cat := some "S", partialContent := some "see(spkr, ?)" }

Instances For

def Phenomena.Dialogue.Studies.Ginzburg2012.tucAfterRepair :

Option Theories.Pragmatics.Dialogue.KOS.TurnUnderConstr

After repair: "I saw the manager" — TuC is cleared, content goes to DGB.

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.tucAfterRepair = none

Instances For

theorem Phenomena.Dialogue.Studies.Ginzburg2012.repair_clears_tuc :

tucAfterRepair = none

Self-repair clears the TuC.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.tuc_has_partial :

tucMidRepair.partialContent = some "see(spkr, ?)"

The TuC tracks partial content before repair.

Genre Constraints on Moves #

@cite{ginzburg-2012} §4.6 (pp. 101–110): genres constrain which moves are felicitous. In a bakery transaction, asking about the weather is infelicitous (though not ungrammatical); in casual chat, it's fine.

We verify that genre constraints correctly filter moves.

def Phenomena.Dialogue.Studies.Ginzburg2012.bakeryGenre :

Theories.Pragmatics.Dialogue.KOS.GenreType String

A bakery genre: only questions about baked goods are relevant.

Equations

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

Instances For

def Phenomena.Dialogue.Studies.Ginzburg2012.casualChat :

Theories.Pragmatics.Dialogue.KOS.GenreType String

An unrestricted casual chat genre.

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.casualChat = { name := "casual" }

Instances For

theorem Phenomena.Dialogue.Studies.Ginzburg2012.bakery_bread_relevant :

Theories.Pragmatics.Dialogue.KOS.genreRelevant bakeryGenre Phenomena.Dialogue.Studies.Ginzburg2012.emptyDGB✝ (Theories.Pragmatics.Dialogue.KOS.IllocMove.ask "What would you like?") = true

"What would you like?" is relevant in a bakery.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.bakery_weather_irrelevant :

Theories.Pragmatics.Dialogue.KOS.genreRelevant bakeryGenre Phenomena.Dialogue.Studies.Ginzburg2012.emptyDGB✝ (Theories.Pragmatics.Dialogue.KOS.IllocMove.ask "What's the weather?") = false

"What's the weather?" is NOT relevant in a bakery.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.casual_weather_relevant :

Theories.Pragmatics.Dialogue.KOS.genreRelevant casualChat Phenomena.Dialogue.Studies.Ginzburg2012.emptyDGB✝ (Theories.Pragmatics.Dialogue.KOS.IllocMove.ask "What's the weather?") = true

"What's the weather?" IS relevant in casual chat.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.genre_discrimination :

Theories.Pragmatics.Dialogue.KOS.genreRelevant bakeryGenre Phenomena.Dialogue.Studies.Ginzburg2012.emptyDGB✝ (Theories.Pragmatics.Dialogue.KOS.IllocMove.ask "What's the weather?") ≠ Theories.Pragmatics.Dialogue.KOS.genreRelevant casualChat Phenomena.Dialogue.Studies.Ginzburg2012.emptyDGB✝¹ (Theories.Pragmatics.Dialogue.KOS.IllocMove.ask "What's the weather?")

Genre relevance distinguishes the bakery from casual chat.

Bridge to Fragment Answer Data #

@cite{ginzburg-2012} Ch. 5 subsumes the fragment answer phenomenon: bare fragments are NSUs resolved via QUD. The FragmentDatum data from Phenomena/Ellipsis/FragmentAnswers.lean are instances of NSU resolution where the QUD is an explicit wh-question.

def Phenomena.Dialogue.Studies.Ginzburg2012.fragmentToNSU (fd : Ellipsis.FragmentAnswers.FragmentDatum) :

Fragment answers are NSUs: the question context provides the QUD, and the fragment is the non-sentential utterance.

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.fragmentToNSU fd = { qud := fd.question, fragment := fd.fragment, resolution := fd.interpretation, source := "Fragment answer, " ++ fd.source }

Instances For

theorem Phenomena.Dialogue.Studies.Ginzburg2012.subject_fragment_is_nsu :

(fragmentToNSU Ellipsis.FragmentAnswers.fragmentSubject).resolution = "Bob went to the movies"

The subject fragment answer maps to an NSU datum.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.all_fragments_are_nsus :

((List.map fragmentToNSU Ellipsis.FragmentAnswers.basicFragments).all fun (d : NSUDatum) => !d.resolution.isEmpty) = true

All basic fragments map to NSU data with non-empty resolutions.

NSU Classification #

@cite{ginzburg-2012} Ch. 7 (§7.2, Tables 7.3–7.4): empirical taxonomy of non-sentential utterances based on a BNC corpus study (Fernández 2006). 200 speaker-turns from 54 BNC files; 14,315 sentences; 1,299 NSUs found, of which 1,283 (98.9%) were classified.

Table 7.3 gives 15 empirical classes ordered by frequency. Table 7.4 groups them into 4 functional categories: positive feedback, answers, metacommunicative queries, extension moves.

inductive Phenomena.Dialogue.Studies.Ginzburg2012.NSUClass :

The 15 NSU classes from @cite{ginzburg-2012} Table 7.3 (p. 221). Ordered by frequency in the BNC sub-corpus.

plainAcknowledgement : NSUClass
"mmh", "uh-huh" — acknowledges preceding utterance (599)
shortAnswer : NSUClass
"Bo" — fills argument slot in MaxQUD (188)
affirmativeAnswer : NSUClass
"Yes" — positive answer to polar query (105)
repeatedAcknowledgement : NSUClass
"Bo, hmm" — acknowledgement with repetition (86)
clarificationEllipsis : NSUClass
"Bo?" — clarification ellipsis (79)
rejection : NSUClass
"No" — negative answer to polar query / assertion (49)
factiveModifier : NSUClass
"Great!" — factive modifier (27)
repeatedAffirmativeAnswer : NSUClass
"Bo, yes" — affirmative with repetition (26)
helpfulRejection : NSUClass
"No, Max" — rejection with helpful alternative (24)
sluice : NSUClass
"Who?" — bare wh-phrase requesting elaboration (24)
checkQuestion : NSUClass
"Okay?" — rising intonation check (22)
filler : NSUClass
"uh", "well" — hesitation / floor-holding (18)
bareModifierPhrase : NSUClass
"Yesterday" — bare modifier phrase (15)
propositionalModifier : NSUClass
"Maybe" — propositional modifier (11)
conjunctionFragment : NSUClass
"And Max" — conjunction + fragment (10)

Instances For

instance Phenomena.Dialogue.Studies.Ginzburg2012.instReprNSUClass :

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instReprNSUClass = { reprPrec := Phenomena.Dialogue.Studies.Ginzburg2012.instReprNSUClass.repr }

def Phenomena.Dialogue.Studies.Ginzburg2012.instReprNSUClass.repr :

NSUClass → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Dialogue.Studies.Ginzburg2012.instDecidableEqNSUClass :

DecidableEq NSUClass

Equations

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

instance Phenomena.Dialogue.Studies.Ginzburg2012.instBEqNSUClass :

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instBEqNSUClass = { beq := Phenomena.Dialogue.Studies.Ginzburg2012.instBEqNSUClass.beq }

def Phenomena.Dialogue.Studies.Ginzburg2012.instBEqNSUClass.beq :

NSUClass → NSUClass → Bool

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instBEqNSUClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.Dialogue.Studies.Ginzburg2012.NSUClass.frequency :

NSUClass → ℕ

BNC frequency count for each NSU class (Table 7.3).

Equations

Instances For

inductive Phenomena.Dialogue.Studies.Ginzburg2012.NSUFunction :

Functional grouping from @cite{ginzburg-2012} Tables 7.1–7.2 (pp. 219–220). The per-group counts are computed from the per-class frequencies in Table 7.3.

positiveFeedback : NSUFunction
Positive feedback: plain + repeated acknowledgement (599 + 86 = 685)
answer : NSUFunction
Answers: short, affirmative, rejection, repeated aff., helpful rej., prop. modifier (403)
metacommunicativeQuery : NSUFunction
Metacommunicative queries: CE, sluice, check question, filler (79 + 24 + 22 + 18 = 143). Note: the Sluice class is ambiguous between a metacommunicative "reprise sluice" reading (the more common one per §7.2.1) and a "direct sluice" reading that functions as an information query. The BNC data (Table 7.3) does not split the 24 sluice instances; we follow the primary classification (Tables 7.1–7.2) in placing sluice here. Direct sluice receives separate grammatical treatment in §7.8 and the Ch. 9 summary.
extensionMove : NSUFunction
Extension moves: factive modifier, bare modifier, conj+frag (27 + 15 + 10 = 52)

Instances For

def Phenomena.Dialogue.Studies.Ginzburg2012.instReprNSUFunction.repr :

NSUFunction → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Dialogue.Studies.Ginzburg2012.instReprNSUFunction :

Repr NSUFunction

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instReprNSUFunction = { reprPrec := Phenomena.Dialogue.Studies.Ginzburg2012.instReprNSUFunction.repr }

instance Phenomena.Dialogue.Studies.Ginzburg2012.instDecidableEqNSUFunction :

DecidableEq NSUFunction

Equations

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

def Phenomena.Dialogue.Studies.Ginzburg2012.instBEqNSUFunction.beq :

NSUFunction → NSUFunction → Bool

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instBEqNSUFunction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Dialogue.Studies.Ginzburg2012.instBEqNSUFunction :

BEq NSUFunction

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instBEqNSUFunction = { beq := Phenomena.Dialogue.Studies.Ginzburg2012.instBEqNSUFunction.beq }

def Phenomena.Dialogue.Studies.Ginzburg2012.NSUClass.toFunction :

NSUClass → NSUFunction

Classify an NSU class into its functional group (Tables 7.1–7.2).

Equations

Instances For

def Phenomena.Dialogue.Studies.Ginzburg2012.allNSUClasses :

All 15 NSU classes (Table 7.3).

Equations

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

Instances For

theorem Phenomena.Dialogue.Studies.Ginzburg2012.nsu_total_1283 :

(List.map NSUClass.frequency allNSUClasses).sum = 1283

Total classified NSUs: 1283 (Table 7.3).

theorem Phenomena.Dialogue.Studies.Ginzburg2012.functional_groups_sum_to_total :

have groups := List.map (fun (c : NSUClass) => (c.toFunction, c.frequency)) allNSUClasses; have pf := (List.map (fun (x : NSUFunction × ℕ) => x.2) (List.filter (fun (x : NSUFunction × ℕ) => x.1 == NSUFunction.positiveFeedback) groups)).sum; have ans := (List.map (fun (x : NSUFunction × ℕ) => x.2) (List.filter (fun (x : NSUFunction × ℕ) => x.1 == NSUFunction.answer) groups)).sum; have mcq := (List.map (fun (x : NSUFunction × ℕ) => x.2) (List.filter (fun (x : NSUFunction × ℕ) => x.1 == NSUFunction.metacommunicativeQuery) groups)).sum; have ext := (List.map (fun (x : NSUFunction × ℕ) => x.2) (List.filter (fun (x : NSUFunction × ℕ) => x.1 == NSUFunction.extensionMove) groups)).sum; pf = 685 ∧ ans = 403 ∧ mcq = 143 ∧ ext = 52 ∧ pf + ans + mcq + ext = 1283

Functional group frequencies sum to the total (1283).

Clarification Request Taxonomy #

@cite{ginzburg-2012} Ch. 6 (§6.2.1): 8 forms of clarification request, each compatible with up to 4 reading types.

inductive Phenomena.Dialogue.Studies.Ginzburg2012.CRForm :

The 8 CR forms from @cite{ginzburg-2012} Ch. 6 §6.2.1.

wot : CRForm
"Wot?" / "What?" — most general CR
literalReprise : CRForm
Literal reprise: exact echo with rising intonation ("Bo?")
whSubstituted : CRForm
Wh-substituted reprise: echo with wh-word ("Bo did WHAT?")
repriseSluice : CRForm
Reprise sluice: bare wh-word after antecedent ("Who?")
repriseFragment : CRForm
Reprise fragment: bare constituent echo ("Bo?")
gap : CRForm
Gap: reprise with a gap ("Did __ leave?")
fillerCR : CRForm
Filler: "Huh?"
explicit : CRForm
Explicit: metalinguistic ("What do you mean 'finagle'?")

Instances For

instance Phenomena.Dialogue.Studies.Ginzburg2012.instReprCRForm :

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instReprCRForm = { reprPrec := Phenomena.Dialogue.Studies.Ginzburg2012.instReprCRForm.repr }

def Phenomena.Dialogue.Studies.Ginzburg2012.instReprCRForm.repr :

CRForm → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Dialogue.Studies.Ginzburg2012.instDecidableEqCRForm :

DecidableEq CRForm

Equations

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

instance Phenomena.Dialogue.Studies.Ginzburg2012.instBEqCRForm :

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instBEqCRForm = { beq := Phenomena.Dialogue.Studies.Ginzburg2012.instBEqCRForm.beq }

def Phenomena.Dialogue.Studies.Ginzburg2012.instBEqCRForm.beq :

CRForm → CRForm → Bool

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instBEqCRForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

inductive Phenomena.Dialogue.Studies.Ginzburg2012.CRReading :

The 4 CR reading types from @cite{ginzburg-2012} Ch. 6 §6.2.1.

clausalConfirmation : CRReading
"Are you asking/saying that p?" — confirms propositional content
intendedContent : CRReading
"What do you mean by X?" — requests intended referent/predicate
repetition : CRReading
"Can you repeat X?" — requests phonological repetition
correction : CRReading
"Did you say X or Y?" — corrective alternative

Instances For

def Phenomena.Dialogue.Studies.Ginzburg2012.instReprCRReading.repr :

CRReading → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Dialogue.Studies.Ginzburg2012.instReprCRReading :

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instReprCRReading = { reprPrec := Phenomena.Dialogue.Studies.Ginzburg2012.instReprCRReading.repr }

instance Phenomena.Dialogue.Studies.Ginzburg2012.instDecidableEqCRReading :

DecidableEq CRReading

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instDecidableEqCRReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Dialogue.Studies.Ginzburg2012.instBEqCRReading.beq :

CRReading → CRReading → Bool

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instBEqCRReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Dialogue.Studies.Ginzburg2012.instBEqCRReading :

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instBEqCRReading = { beq := Phenomena.Dialogue.Studies.Ginzburg2012.instBEqCRReading.beq }

Grounding vs CRification #

@cite{ginzburg-2012} Ch. 6: when "Did Bo leave?" enters Pending, the addressee either grounds it (if they know who "Bo" is) or CRifies it (if "Bo" is unresolved → "Who's Bo?").

We show the branching behavior using integrateLocProp.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.unresolved_bo_crifies :

(Theories.Pragmatics.Dialogue.KOS.integrateLocProp Phenomena.Dialogue.Studies.Ginzburg2012.didBoLeave✝ Phenomena.Dialogue.Studies.Ginzburg2012.toCR✝).isGrounded = false

Unresolved "Bo" triggers CRification.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.resolved_bo_grounds :

(Theories.Pragmatics.Dialogue.KOS.integrateLocProp Phenomena.Dialogue.Studies.Ginzburg2012.didBoLeaveResolved✝ Phenomena.Dialogue.Studies.Ginzburg2012.toCR✝).isGrounded = true

Resolved version grounds successfully.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.cr_targets_bo :

Theories.Pragmatics.Dialogue.KOS.integrateLocProp Phenomena.Dialogue.Studies.Ginzburg2012.didBoLeave✝ Phenomena.Dialogue.Studies.Ginzburg2012.toCR✝ = Theories.Pragmatics.Dialogue.KOS.IntegrationResult.crification "Who do you mean by 'bo_ref'?" { index := "bo_ref", restriction := "individual" }

The CR question targets the unresolved parameter.

End-to-End: DialogueSign → LocProp → Integration → DGB #

@cite{ginzburg-2012}'s architecture connects grammar to dialogue via:

A DialogueSign (Ch. 5) with dgb-params, q-params, quest-dom
Conversion to a LocProp (Ch. 6) with cparams
Integration: grounding (cparams resolved → FACTS) or CRification (cparams unresolved → CR question on QUD)
DGB update via conversational rules (Ch. 4)

This section proves the full pipeline for the worked example "Did Jo leave?" — from DialogueSign to final DGB state.

instance Phenomena.Dialogue.Studies.Ginzburg2012.instAnswerhoodString_2 :

Theories.Pragmatics.Dialogue.KOS.Answerhood String String

Equations

Phenomena.Dialogue.Studies.Ginzburg2012.instAnswerhoodString_2 = { resolves := fun (fact question : String) => fact == question }

theorem Phenomena.Dialogue.Studies.Ginzburg2012.e2e_phon_preserved :

Phenomena.Dialogue.Studies.Ginzburg2012.joLocProp✝.phon = "Jo"

Conversion preserves the phonological form.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.e2e_cparams_from_dgb :

Phenomena.Dialogue.Studies.Ginzburg2012.joLocProp✝.cparams = Phenomena.Dialogue.Studies.Ginzburg2012.joSign✝.dgbParams

Conversion transfers dgb-params to cparams.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.e2e_jo_crifies :

(Theories.Pragmatics.Dialogue.KOS.integrateLocProp Phenomena.Dialogue.Studies.Ginzburg2012.joLocProp✝ Phenomena.Dialogue.Studies.Ginzburg2012.crQuestion✝).isGrounded = false

"Jo" has unresolved cparams → CRification (not grounding).

theorem Phenomena.Dialogue.Studies.Ginzburg2012.e2e_cr_question :

Theories.Pragmatics.Dialogue.KOS.integrateLocProp Phenomena.Dialogue.Studies.Ginzburg2012.joLocProp✝ Phenomena.Dialogue.Studies.Ginzburg2012.crQuestion✝ = Theories.Pragmatics.Dialogue.KOS.IntegrationResult.crification "Who do you mean by 'jo_ref'?" { index := "jo_ref", restriction := "individual" }

The CR question is derived from the unresolved parameter.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.e2e_cr_on_qud :

Phenomena.Dialogue.Studies.Ginzburg2012.tis₁_cr✝.dgb.qud.head? = some "Who do you mean by 'jo_ref'?"

After CRification, QUD has the CR question at the top.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.e2e_original_still_on_qud :

"leave(jo)" ∈ Phenomena.Dialogue.Studies.Ginzburg2012.tis₁_cr✝.dgb.qud

The original question is still on QUD (below the CR).

theorem Phenomena.Dialogue.Studies.Ginzburg2012.e2e_resolved_grounds :

(Theories.Pragmatics.Dialogue.KOS.integrateLocProp Phenomena.Dialogue.Studies.Ginzburg2012.joResolved✝ Phenomena.Dialogue.Studies.Ginzburg2012.crQuestion✝).isGrounded = true

Resolved "Jo" grounds successfully.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.e2e_ground_resolves_qud :

Phenomena.Dialogue.Studies.Ginzburg2012.tis₁_ground✝.dgb.qud = []

theorem Phenomena.Dialogue.Studies.Ginzburg2012.e2e_ground_adds_fact :

"leave(jo)" ∈ Phenomena.Dialogue.Studies.Ginzburg2012.tis₁_ground✝.dgb.facts

theorem Phenomena.Dialogue.Studies.Ginzburg2012.e2e_exhaustive (lp : Theories.Pragmatics.Dialogue.KOS.LocProp String) (toCR : Theories.Pragmatics.Dialogue.KOS.CParam → String) :

(Theories.Pragmatics.Dialogue.KOS.integrateLocProp lp toCR).isGrounded = true ∨ (Theories.Pragmatics.Dialogue.KOS.integrateLocProp lp toCR).isGrounded = false

The full chain is consistent: CRification and grounding are exhaustive. Every LocProp either grounds or CRifies — there is no third option.

theorem Phenomena.Dialogue.Studies.Ginzburg2012.e2e_nonResolveCond_after_ground :

Phenomena.Dialogue.Studies.Ginzburg2012.tis₁_ground✝.dgb.nonResolveCond = true

Non-resolve-cond holds after QUD-downdate in the grounding path.