KOS: Dialogue Gameboards #

This file formalizes the KOS framework for dialogue as presented in two distinct sources:

@cite{ginzburg-2012} Ch. 4 (§§4.1–4.7): The Dialogue Gameboard (DGB) and Total Information State (TIS), conversational rules, genres, and M-Coherence. This is the primary source.
@cite{ginzburg-cooper-2004}: Clarification Ellipsis machinery — C-PARAMS, coercion operations (parameter focussing, parameter identification, existential generalization), utterance skeletons, and the sign+assignment model of grounding. This is a supplementary source for the CE analysis.

@cite{ginzburg-2012} DGB (ex. 100, p. 111; final version ex. 113, p. 215) #

The DGB is a conversational participant's own version of the public context:

spkr, addr: current speaker and addressee
Facts: shared commitments (Set of propositions)
Moves: history of illocutionary moves (list of LocProp)
Pending: ungrounded locutionary propositions (added in Ch. 6)
QUD: partially ordered set of questions under discussion
non-resolve-cond: well-formedness constraint — no QUD question is resolved by FACTS (see DGB.nonResolveCond in Rules.lean)

Known simplifications #

Our DGB corresponds to the Ch. 4 intermediate version (ex. 100), not the final Ch. 6 version (ex. 113). Specific differences:

MOVES: stores IllocMove (Ch. 4) not LocProp (Ch. 6 final)
QUD: stores bare QContent not InfoStruc (question + FECs, ex. 39)
Pending: uses PendingLoc not LocProp (Ch. 6 final)
utt-time / c-utt: temporal fields from ex. 100 are not modeled

@cite{ginzburg-2012} TIS (ex. 93, p. 107) #

The Total Information State wraps the DGB and adds a private component:

DGB: the public dialogue gameboard
Private: genre, beliefs, agenda — non-public processing state

@cite{ginzburg-cooper-2004}: Clarification Ellipsis (§§3–6) #

C-PARAMS, coercion operations, utterance skeletons, and the MAX-QUD/SAL-UTT processing state for Clarification Ellipsis. These are preserved in a clearly separated section below.

source

inductive Theories.Pragmatics.Dialogue.KOS.IllocMove (Fact QContent : Type) :

Type

An illocutionary move in dialogue.

@cite{ginzburg-2012} Ch. 4: moves are illocutionary propositions — speech events classified by their illocutionary force. In the final version (p. 215), MOVES stores locutionary propositions (situated speech events). We abstract over the content: assertions carry propositional content, queries carry question content.

The Fact and QContent parameters match the DGB's content types.

assert {Fact QContent : Type} : Fact → IllocMove Fact QContent
An assertion: speaker commits to propositional content.
ask {Fact QContent : Type} : QContent → IllocMove Fact QContent
A query: speaker raises a question.
accept {Fact QContent : Type} : Fact → IllocMove Fact QContent
Accept: addressee grounds an assertion.
check {Fact QContent : Type} : Fact → IllocMove Fact QContent
Check: addressee requests confirmation of an assertion.
confirm {Fact QContent : Type} : Fact → IllocMove Fact QContent
Confirm: speaker confirms in response to check.
greet {Fact QContent : Type} : IllocMove Fact QContent
Greeting.
counterGreet {Fact QContent : Type} : IllocMove Fact QContent
Counter-greeting.

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instReprIllocMove {Fact✝ QContent✝ : Type} [Repr Fact✝] [Repr QContent✝] :

Repr (IllocMove Fact✝ QContent✝)

Equations

Theories.Pragmatics.Dialogue.KOS.instReprIllocMove = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprIllocMove.repr }

source

def Theories.Pragmatics.Dialogue.KOS.instReprIllocMove.repr {Fact✝ QContent✝ : Type} [Repr Fact✝] [Repr QContent✝] :

IllocMove Fact✝ QContent✝ → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instDecidableEqIllocMove {Fact✝ QContent✝ : Type} [DecidableEq Fact✝] [DecidableEq QContent✝] :

DecidableEq (IllocMove Fact✝ QContent✝)

Equations

Theories.Pragmatics.Dialogue.KOS.instDecidableEqIllocMove = Theories.Pragmatics.Dialogue.KOS.instDecidableEqIllocMove.decEq

source

def Theories.Pragmatics.Dialogue.KOS.instDecidableEqIllocMove.decEq {Fact✝ QContent✝ : Type} [DecidableEq Fact✝] [DecidableEq QContent✝] (x✝ x✝¹ : IllocMove Fact✝ QContent✝) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.instBEqIllocMove.beq {Fact✝ QContent✝ : Type} [BEq Fact✝] [BEq QContent✝] :

IllocMove Fact✝ QContent✝ → IllocMove Fact✝ QContent✝ → Bool

Equations

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instBEqIllocMove {Fact✝ QContent✝ : Type} [BEq Fact✝] [BEq QContent✝] :

BEq (IllocMove Fact✝ QContent✝)

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqIllocMove = { beq := Theories.Pragmatics.Dialogue.KOS.instBEqIllocMove.beq }

source

def Theories.Pragmatics.Dialogue.KOS.IllocMove.factContent {Fact QContent : Type} :

IllocMove Fact QContent → Option Fact

Extract the propositional content from a move, if any.

Equations

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.IllocMove.questionContent {Fact QContent : Type} :

IllocMove Fact QContent → Option QContent

Extract the question content from a move, if any.

Equations

(Theories.Pragmatics.Dialogue.KOS.IllocMove.ask q).questionContent = some q
x✝.questionContent = none

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.IllocMove.toSearleClass {Fact QContent : Type} :

IllocMove Fact QContent → Core.Discourse.SearleClass

Map an illocutionary move to @cite{searle-1979}'s five-class taxonomy.

Assert/accept/confirm are assertives (mind-to-world fit). Ask is a directive (world-to-mind: the speaker tries to get the addressee to provide information). Check is a directive (requesting confirmation). Greet/counterGreet are expressives (null fit).

Equations

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.IllocMove.directionOfFit {Fact QContent : Type} (m : IllocMove Fact QContent) :

Core.Discourse.DirectionOfFit

Direction of fit for an illocutionary move, derived via Searle class.

Equations

m.directionOfFit = m.toSearleClass.directionOfFit

Instances For

source

theorem Theories.Pragmatics.Dialogue.KOS.IllocMove.assert_mind_to_world {Fact QContent : Type} (p : Fact) :

(assert p).directionOfFit = Core.Discourse.DirectionOfFit.mindToWorld

Assertions have mind-to-world fit: the speaker is responsible if p is false.

source

theorem Theories.Pragmatics.Dialogue.KOS.IllocMove.ask_world_to_mind {Fact QContent : Type} (q : QContent) :

(ask q).directionOfFit = Core.Discourse.DirectionOfFit.worldToMind

Queries have world-to-mind fit: the speaker wants the addressee to act.

source

theorem Theories.Pragmatics.Dialogue.KOS.IllocMove.greet_null_fit {Fact QContent : Type} :

greet.directionOfFit = Core.Discourse.DirectionOfFit.null

Greetings have null fit: they express social acknowledgement.

source

structure Theories.Pragmatics.Dialogue.KOS.PendingLoc :

Type

A pending locutionary proposition: an ungrounded utterance.

@cite{ginzburg-2012} Ch. 6, ex. 113 (p. 215): in the final DGB version, Pending stores full LocProps (defined in §15 below). This PendingLoc is a simplified representation used in the DGB struct. For the full LocProp-based grounding protocol, see integrateLocProp in Rules.lean.

Known simplification: the final DGB (ex. 113) uses List(LocProp) for both MOVES and Pending. Our DGB uses IllocMove for MOVES and PendingLoc for Pending — this corresponds to the Ch. 4 intermediate version.

utt : String
The utterance event identifier
uttType : String
The classifying type (as string description)

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.instReprPendingLoc.repr :

PendingLoc → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instReprPendingLoc :

Repr PendingLoc

Equations

Theories.Pragmatics.Dialogue.KOS.instReprPendingLoc = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprPendingLoc.repr }

source

instance Theories.Pragmatics.Dialogue.KOS.instDecidableEqPendingLoc :

DecidableEq PendingLoc

Equations

Theories.Pragmatics.Dialogue.KOS.instDecidableEqPendingLoc = Theories.Pragmatics.Dialogue.KOS.instDecidableEqPendingLoc.decEq

source

def Theories.Pragmatics.Dialogue.KOS.instDecidableEqPendingLoc.decEq (x✝ x✝¹ : PendingLoc) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.instBEqPendingLoc.beq :

PendingLoc → PendingLoc → Bool

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqPendingLoc.beq { utt := a, uttType := a_1 } { utt := b, uttType := b_1 } = (a == b && a_1 == b_1)
Theories.Pragmatics.Dialogue.KOS.instBEqPendingLoc.beq x✝¹ x✝ = false

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instBEqPendingLoc :

BEq PendingLoc

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqPendingLoc = { beq := Theories.Pragmatics.Dialogue.KOS.instBEqPendingLoc.beq }

source

structure Theories.Pragmatics.Dialogue.KOS.DGB (Participant Fact QContent : Type) :

Type

The Dialogue Gameboard.

@cite{ginzburg-2012} ex. 100 (p. 111) and final version ex. 113 (p. 215).

Each conversational participant maintains their own DGB — distinct but coupled gameboards, NOT a single shared context. The DGB tracks the public component of a participant's conversational state.

The type parameters make content types explicit:

Participant: type of participant identifiers (e.g., String, Fin 2)
Fact: type of accumulated facts (e.g., BProp W for typed CG access)
QContent: type of QUD entries (e.g., partition-based QUD W)

spkr : Option Participant
Current speaker (@cite{ginzburg-2012} ex. 100)
addr : Option Participant
Current addressee (@cite{ginzburg-2012} ex. 100)
facts : List Fact
Shared commitments. @cite{ginzburg-2012}: "Facts : Set(Prop)"
moves : List (IllocMove Fact QContent)
History of illocutionary moves. @cite{ginzburg-2012}: "Moves : list(IllocProp)". The last element is the LatestMove.
Known simplification: the final DGB (ex. 113, p. 215) stores LocProps in MOVES, not illocutionary propositions. We use IllocMove here, matching the Ch. 4 version.
pending : List PendingLoc
Ungrounded locutionary propositions. @cite{ginzburg-2012} Ch. 6 (p. 215): added to the DGB in the final version.
qud : List QContent
Partially ordered set of questions under discussion. @cite{ginzburg-2012}: "QUD : poset(Question)". We use a list (most recent = front) following QUD-maximality.
Known simplification: the final version (ex. 39, p. 239) makes QUD entries InfoStruc (question + FECs) rather than bare questions. We use bare QContent here; the InfoStruc type is defined in §16 below.

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.DGB.latestMove {Participant Fact QContent : Type} (dgb : DGB Participant Fact QContent) :

Option (IllocMove Fact QContent)

The latest move is the last element of the moves list.

Equations

dgb.latestMove = dgb.moves.getLast?

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.DGB.initial {Participant Fact QContent : Type} :

DGB Participant Fact QContent

An empty DGB.

Equations

Theories.Pragmatics.Dialogue.KOS.DGB.initial = { }

Instances For

source

structure Theories.Pragmatics.Dialogue.KOS.GenreType (QContent : Type) :

Type

A conversational genre type.

@cite{ginzburg-2012} §4.6 (pp. 101–110): genres are TTR record types that classify conversations by their characteristic conversational structures. Example genres from the book: CasualChat (ex. 88a), PetrolMarket (ex. 88b), BakeryChat (ex. 88c).

We model genre types as records with optional constraints on the QUD content and move patterns. The qudConstraint field captures the genre- specific restrictions on what questions may be discussed.

name : String
Genre name for identification
qudConstraint : Option (List QContent → Bool)
Constraint on which questions may be in QUD. none means unrestricted (like CasualChat).

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.GenreType.generic {QContent : Type} :

GenreType QContent

The generic DGBType — the supertype of all genre types. @cite{ginzburg-2012} ex. 86 (p. 103): DGBTypefin GenreType.

Equations

Theories.Pragmatics.Dialogue.KOS.GenreType.generic = { name := "generic" }

Instances For

source

structure Theories.Pragmatics.Dialogue.KOS.TurnUnderConstr :

Type

A turn under construction: an incomplete utterance being built incrementally.

@cite{ginzburg-2012} Ch. 6–7: the TuC tracks the unfolding utterance as it is produced word-by-word. Participants can intervene mid-turn (completions, collaborative finishes, self-repairs). The TuC is part of the private state because each participant may have a different parse of the emerging turn.

The pending field on the DGB tracks ungrounded complete utterances; TuC tracks incomplete ones. When the turn is complete, its content moves from TuC to Pending (if unresolved) or Facts (if grounded).

phonSoFar : String
Phonological material produced so far
cat : Option String
Syntactic category of the emerging constituent
partialContent : Option String
Partial content accumulated

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instReprTurnUnderConstr :

Repr TurnUnderConstr

Equations

Theories.Pragmatics.Dialogue.KOS.instReprTurnUnderConstr = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprTurnUnderConstr.repr }

source

def Theories.Pragmatics.Dialogue.KOS.instReprTurnUnderConstr.repr :

TurnUnderConstr → ℕ → Std.Format

Equations

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

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.instDecidableEqTurnUnderConstr.decEq (x✝ x✝¹ : TurnUnderConstr) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instDecidableEqTurnUnderConstr :

DecidableEq TurnUnderConstr

Equations

Theories.Pragmatics.Dialogue.KOS.instDecidableEqTurnUnderConstr = Theories.Pragmatics.Dialogue.KOS.instDecidableEqTurnUnderConstr.decEq

source

def Theories.Pragmatics.Dialogue.KOS.instBEqTurnUnderConstr.beq :

TurnUnderConstr → TurnUnderConstr → Bool

Equations

One or more equations did not get rendered due to their size.
Theories.Pragmatics.Dialogue.KOS.instBEqTurnUnderConstr.beq x✝¹ x✝ = false

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instBEqTurnUnderConstr :

BEq TurnUnderConstr

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqTurnUnderConstr = { beq := Theories.Pragmatics.Dialogue.KOS.instBEqTurnUnderConstr.beq }

source

structure Theories.Pragmatics.Dialogue.KOS.PrivateState (Fact QContent : Type) :

Type

The private component of an information state.

@cite{ginzburg-2012} ex. 93 (p. 107): PRType has genre, beliefs, and agenda. Agenda is a list of illocutionary propositions that the participant plans to realize. Beliefs are private (non-public) propositional attitudes.

genre : Option (GenreType QContent)
The conversational genre the participant takes the interaction to be.
agenda : List (IllocMove Fact QContent)
The participant's agenda: planned illocutionary moves.
turnUnderConstr : Option TurnUnderConstr
The turn currently under construction (if any). @cite{ginzburg-2012} Ch. 7: enables self-repair and collaborative completion.

Instances For

source

structure Theories.Pragmatics.Dialogue.KOS.TIS (Participant Fact QContent : Type) :

Type

Total Information State (TIS).

@cite{ginzburg-2012} ex. 93 (p. 107): the TIS consists of the public DGB and a private component (genre, beliefs, agenda).

This replaces the earlier IS type which conflated @cite{ginzburg-cooper-2004} processing state (MAX-QUD, SAL-UTT) with the 2012 architecture. The 2004 clarification processing state is available separately via CEState.

dgb : DGB Participant Fact QContent
The public dialogue gameboard
private_ : PrivateState Fact QContent
Private state: genre, agenda

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.TIS.initial {Participant Fact QContent : Type} :

TIS Participant Fact QContent

An empty TIS.

Equations

Theories.Pragmatics.Dialogue.KOS.TIS.initial = { }

Instances For

Clarification Ellipsis Machinery #

The following definitions are from @cite{ginzburg-cooper-2004}, which develops a theory of Clarification Ellipsis (CE) using contextual parameters (C-PARAMS), utterance skeletons, and coercion operations. These concepts predate the TTR reformulation in @cite{ginzburg-2012} Ch. 5–6.

In the 2012 book, the corresponding machinery uses dgb-params (record types) rather than C-PARAMS (index-restriction pairs), and Clarification Context Update Rules (CCURs) rather than the three coercion operations. We preserve the 2004 formulation as it is more directly computational.

source

structure Theories.Pragmatics.Dialogue.KOS.CParam :

Type

A contextual parameter with INDEX and RESTR(ICTION).

Each C-PARAM has an index variable (e.g., "b" for the referent of "Bo") and a restriction characterizing what values are acceptable (e.g., "named(Bo)(b)"). @cite{ginzburg-cooper-2004} ex. 28.

index : String
restriction : String

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.instReprCParam.repr :

CParam → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instReprCParam :

Repr CParam

Equations

Theories.Pragmatics.Dialogue.KOS.instReprCParam = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprCParam.repr }

source

instance Theories.Pragmatics.Dialogue.KOS.instDecidableEqCParam :

DecidableEq CParam

Equations

Theories.Pragmatics.Dialogue.KOS.instDecidableEqCParam = Theories.Pragmatics.Dialogue.KOS.instDecidableEqCParam.decEq

source

def Theories.Pragmatics.Dialogue.KOS.instDecidableEqCParam.decEq (x✝ x✝¹ : CParam) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instBEqCParam :

BEq CParam

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqCParam = { beq := Theories.Pragmatics.Dialogue.KOS.instBEqCParam.beq }

source

def Theories.Pragmatics.Dialogue.KOS.instBEqCParam.beq :

CParam → CParam → Bool

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqCParam.beq { index := a, restriction := a_1 } { index := b, restriction := b_1 } = (a == b && a_1 == b_1)
Theories.Pragmatics.Dialogue.KOS.instBEqCParam.beq x✝¹ x✝ = false

Instances For

source

@[reducible, inline]

abbrev Theories.Pragmatics.Dialogue.KOS.CParamSet :

Type

A set of contextual parameters, analogous to HPSG.SlashValue.

Both are non-local features (sets of outstanding dependencies):

SLASH tracks syntactic gaps (filler-gap dependencies)
C-PARAMS tracks contextual dependencies (referent resolution)

Both propagate via the same amalgamation mechanism (ex. 29 ≈ Nonlocal Feature Principle) and get discharged at specific sites.

Equations

Theories.Pragmatics.Dialogue.KOS.CParamSet = List Theories.Pragmatics.Dialogue.KOS.CParam

Instances For

source

structure Theories.Pragmatics.Dialogue.KOS.CtxtAssignment :

Type

A contextual assignment maps parameter indices to values.

Grounding requires a total assignment (all C-PARAMS resolved). Clarification arises when the assignment is partial. @cite{ginzburg-cooper-2004} §6, ex. 81–82.

bindings : List (String × String)

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.instReprCtxtAssignment.repr :

CtxtAssignment → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instReprCtxtAssignment :

Repr CtxtAssignment

Equations

Theories.Pragmatics.Dialogue.KOS.instReprCtxtAssignment = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprCtxtAssignment.repr }

source

def Theories.Pragmatics.Dialogue.KOS.instDecidableEqCtxtAssignment.decEq (x✝ x✝¹ : CtxtAssignment) :

Decidable (x✝ = x✝¹)

Equations

Theories.Pragmatics.Dialogue.KOS.instDecidableEqCtxtAssignment.decEq { bindings := a } { bindings := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instDecidableEqCtxtAssignment :

DecidableEq CtxtAssignment

Equations

Theories.Pragmatics.Dialogue.KOS.instDecidableEqCtxtAssignment = Theories.Pragmatics.Dialogue.KOS.instDecidableEqCtxtAssignment.decEq

source

instance Theories.Pragmatics.Dialogue.KOS.instBEqCtxtAssignment :

BEq CtxtAssignment

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqCtxtAssignment = { beq := Theories.Pragmatics.Dialogue.KOS.instBEqCtxtAssignment.beq }

source

def Theories.Pragmatics.Dialogue.KOS.instBEqCtxtAssignment.beq :

CtxtAssignment → CtxtAssignment → Bool

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqCtxtAssignment.beq { bindings := a } { bindings := b } = (a == b)
Theories.Pragmatics.Dialogue.KOS.instBEqCtxtAssignment.beq x✝¹ x✝ = false

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.CtxtAssignment.resolves (f : CtxtAssignment) (cp : CParam) :

Bool

Does the assignment resolve a given parameter?

Equations

f.resolves cp = f.bindings.any fun (x : String × String) => x.1 == cp.index

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.CtxtAssignment.resolvesAll (f : CtxtAssignment) (ps : CParamSet) :

Bool

Does the assignment resolve all parameters in a set?

Equations

f.resolvesAll ps = List.all ps f.resolves

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.CtxtAssignment.unresolved (f : CtxtAssignment) (ps : CParamSet) :

CParamSet

Which parameters remain unresolved?

Equations

f.unresolved ps = List.filter (fun (x : Theories.Pragmatics.Dialogue.KOS.CParam) => !f.resolves x) ps

Instances For

source

structure Theories.Pragmatics.Dialogue.KOS.SubUtterance :

Type

A sub-utterance: the minimal addressable unit for clarification.

Every sub-utterance encodes PHON, CAT, and CONT — this fractal heterogeneity is what makes clarification of any constituent possible. @cite{ginzburg-cooper-2004} §2.

phon : String
cat : String
cont : String

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.instReprSubUtterance.repr :

SubUtterance → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instReprSubUtterance :

Repr SubUtterance

Equations

Theories.Pragmatics.Dialogue.KOS.instReprSubUtterance = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprSubUtterance.repr }

source

instance Theories.Pragmatics.Dialogue.KOS.instDecidableEqSubUtterance :

DecidableEq SubUtterance

Equations

Theories.Pragmatics.Dialogue.KOS.instDecidableEqSubUtterance = Theories.Pragmatics.Dialogue.KOS.instDecidableEqSubUtterance.decEq

source

def Theories.Pragmatics.Dialogue.KOS.instDecidableEqSubUtterance.decEq (x✝ x✝¹ : SubUtterance) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instBEqSubUtterance :

BEq SubUtterance

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqSubUtterance = { beq := Theories.Pragmatics.Dialogue.KOS.instBEqSubUtterance.beq }

source

def Theories.Pragmatics.Dialogue.KOS.instBEqSubUtterance.beq :

SubUtterance → SubUtterance → Bool

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqSubUtterance.beq { phon := a, cat := a_1, cont := a_2 } { phon := b, cat := b_1, cont := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
Theories.Pragmatics.Dialogue.KOS.instBEqSubUtterance.beq x✝¹ x✝ = false

Instances For

source

structure Theories.Pragmatics.Dialogue.KOS.UttSkeleton :

Type

An utterance skeleton: a sign with C-PARAMS and CONSTITS.

The CONSTITS feature (ex. 30) provides access to all sub-utterances. C-PARAMS (ex. 28–29) are the contextual dependencies introduced by the sign, amalgamated from daughters via the Non-local Amalgamation Constraint. @cite{ginzburg-cooper-2004} §3.

phon : String
cat : String
cont : String
cparams : CParamSet
constits : List SubUtterance

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.instReprUttSkeleton.repr :

UttSkeleton → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instReprUttSkeleton :

Repr UttSkeleton

Equations

Theories.Pragmatics.Dialogue.KOS.instReprUttSkeleton = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprUttSkeleton.repr }

source

instance Theories.Pragmatics.Dialogue.KOS.instDecidableEqUttSkeleton :

DecidableEq UttSkeleton

Equations

Theories.Pragmatics.Dialogue.KOS.instDecidableEqUttSkeleton = Theories.Pragmatics.Dialogue.KOS.instDecidableEqUttSkeleton.decEq

source

def Theories.Pragmatics.Dialogue.KOS.instDecidableEqUttSkeleton.decEq (x✝ x✝¹ : UttSkeleton) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.instBEqUttSkeleton.beq :

UttSkeleton → UttSkeleton → Bool

Equations

One or more equations did not get rendered due to their size.
Theories.Pragmatics.Dialogue.KOS.instBEqUttSkeleton.beq x✝¹ x✝ = false

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instBEqUttSkeleton :

BEq UttSkeleton

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqUttSkeleton = { beq := Theories.Pragmatics.Dialogue.KOS.instBEqUttSkeleton.beq }

source

def Theories.Pragmatics.Dialogue.KOS.UttSkeleton.constitForParam (u : UttSkeleton) (paramIdx : String) :

Option SubUtterance

Find the constituent whose CONT matches a parameter index.

Equations

u.constitForParam paramIdx = List.find? (fun (x : Theories.Pragmatics.Dialogue.KOS.SubUtterance) => x.cont == paramIdx) u.constits

Instances For

source

structure Theories.Pragmatics.Dialogue.KOS.SignAssignment :

Type

A sign paired with a contextual assignment.

@cite{ginzburg-cooper-2004} ex. 81, p.353. The assignment f records which C-PARAMS have been resolved. Grounding checks whether f is total.

sign : UttSkeleton
assignment : CtxtAssignment

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.instReprSignAssignment.repr :

SignAssignment → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instReprSignAssignment :

Repr SignAssignment

Equations

Theories.Pragmatics.Dialogue.KOS.instReprSignAssignment = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprSignAssignment.repr }

source

def Theories.Pragmatics.Dialogue.KOS.instDecidableEqSignAssignment.decEq (x✝ x✝¹ : SignAssignment) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instDecidableEqSignAssignment :

DecidableEq SignAssignment

Equations

Theories.Pragmatics.Dialogue.KOS.instDecidableEqSignAssignment = Theories.Pragmatics.Dialogue.KOS.instDecidableEqSignAssignment.decEq

source

def Theories.Pragmatics.Dialogue.KOS.instBEqSignAssignment.beq :

SignAssignment → SignAssignment → Bool

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqSignAssignment.beq { sign := a, assignment := a_1 } { sign := b, assignment := b_1 } = (a == b && a_1 == b_1)
Theories.Pragmatics.Dialogue.KOS.instBEqSignAssignment.beq x✝¹ x✝ = false

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instBEqSignAssignment :

BEq SignAssignment

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqSignAssignment = { beq := Theories.Pragmatics.Dialogue.KOS.instBEqSignAssignment.beq }

source

structure Theories.Pragmatics.Dialogue.KOS.CEState (QContent : Type) :

Type

Clarification Ellipsis processing state.

@cite{ginzburg-cooper-2004}: MAX-QUD and SAL-UTT are processing state for the CE analysis. These are NOT part of the @cite{ginzburg-2012} DGB or TIS (in 2012, MaxQUD is computed from the QUD poset's maximal element, not stored separately).

This state can be used alongside the 2012 TIS when CE processing is needed.

maxQud : Option QContent
The currently maximal question — for CE coercion operations
salUtt : Option SubUtterance
The salient sub-utterance — target of clarification
pendingUtts : List SignAssignment
Pending utterances awaiting C-PARAMS resolution

Instances For

source

inductive Theories.Pragmatics.Dialogue.KOS.CoercionOp :

Type

The three coercion operations on signs with unresolved C-PARAMS. @cite{ginzburg-cooper-2004} §5.

paramFocussing : CoercionOp
Clausal CE reading: polar question about content (ex. 53)
paramIdentification : CoercionOp
Constituent CE reading: wh-question about speaker meaning (ex. 59)
existentialGeneralization : CoercionOp
Ground without clarification: ∃-quantify a parameter (ex. 77)

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instReprCoercionOp :

Repr CoercionOp

Equations

Theories.Pragmatics.Dialogue.KOS.instReprCoercionOp = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprCoercionOp.repr }

source

def Theories.Pragmatics.Dialogue.KOS.instReprCoercionOp.repr :

CoercionOp → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instDecidableEqCoercionOp :

DecidableEq CoercionOp

Equations

Theories.Pragmatics.Dialogue.KOS.instDecidableEqCoercionOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Theories.Pragmatics.Dialogue.KOS.instBEqCoercionOp :

BEq CoercionOp

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqCoercionOp = { beq := Theories.Pragmatics.Dialogue.KOS.instBEqCoercionOp.beq }

source

def Theories.Pragmatics.Dialogue.KOS.instBEqCoercionOp.beq :

CoercionOp → CoercionOp → Bool

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqCoercionOp.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

structure Theories.Pragmatics.Dialogue.KOS.CoercionOutput :

Type

Output of a coercion operation: partial specification for the clarification context.

op : CoercionOp
salUtt : SubUtterance
SAL-UTT: the sub-utterance to be echoed
maxQud : String
MAX-QUD: the question raised (string representation)

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.instReprCoercionOutput.repr :

CoercionOutput → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instReprCoercionOutput :

Repr CoercionOutput

Equations

Theories.Pragmatics.Dialogue.KOS.instReprCoercionOutput = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprCoercionOutput.repr }

source

instance Theories.Pragmatics.Dialogue.KOS.instDecidableEqCoercionOutput :

DecidableEq CoercionOutput

Equations

Theories.Pragmatics.Dialogue.KOS.instDecidableEqCoercionOutput = Theories.Pragmatics.Dialogue.KOS.instDecidableEqCoercionOutput.decEq

source

def Theories.Pragmatics.Dialogue.KOS.instDecidableEqCoercionOutput.decEq (x✝ x✝¹ : CoercionOutput) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instBEqCoercionOutput :

BEq CoercionOutput

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqCoercionOutput = { beq := Theories.Pragmatics.Dialogue.KOS.instBEqCoercionOutput.beq }

source

def Theories.Pragmatics.Dialogue.KOS.instBEqCoercionOutput.beq :

CoercionOutput → CoercionOutput → Bool

Equations

Theories.Pragmatics.Dialogue.KOS.instBEqCoercionOutput.beq { op := a, salUtt := a_1, maxQud := a_2 } { op := b, salUtt := b_1, maxQud := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
Theories.Pragmatics.Dialogue.KOS.instBEqCoercionOutput.beq x✝¹ x✝ = false

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.parameterFocussing (antecedent : UttSkeleton) (paramIdx : String) :

Option CoercionOutput

Parameter focussing (@cite{ginzburg-cooper-2004} ex. 53): derive clausal CE reading.

Takes the antecedent sign and a problematic parameter index. Finds the constituent that introduced the parameter. Produces MAX-QUD = polar question about the antecedent content.

Equations

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

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.parameterIdentification (antecedent : UttSkeleton) (paramIdx : String) :

Option CoercionOutput

Parameter identification (@cite{ginzburg-cooper-2004} ex. 59): derive constituent CE reading.

Produces MAX-QUD = wh-question about speaker meaning.

Equations

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

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.existentialGeneralization (sk : UttSkeleton) (paramIdx : String) :

UttSkeleton

Contextual existential generalization (@cite{ginzburg-cooper-2004} ex. 77): ground without clarifying.

Removes a parameter from C-PARAMS by existentially quantifying it.

Equations

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

Instances For

source

structure Theories.Pragmatics.Dialogue.KOS.IS (Fact QContent : Type) :

Type

Information State for the @cite{ginzburg-cooper-2004} model.

Bundles a DGB with CE processing state (pending utterances). Uses String for both Fact and QContent, matching the string-based representations in the 2004 paper. The Participant type parameter is set to String.

This is NOT the @cite{ginzburg-2012} TIS — it predates the genre/agenda private state. It exists to support the CE running example.

dgb : DGB String Fact QContent
pending : List SignAssignment
Utterances awaiting full C-PARAMS resolution
ce : CEState QContent

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.IS.initial {Fact QContent : Type} :

IS Fact QContent

An empty IS.

Equations

Theories.Pragmatics.Dialogue.KOS.IS.initial = { }

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.IS.integrateUtterance {Fact QContent : Type} [BEq Fact] (is_ : IS Fact QContent) (skel : UttSkeleton) (assign : CtxtAssignment) (toFact : String → Fact) :

IS Fact QContent

Integrate an utterance into the IS.

If the assignment fully resolves all C-PARAMS, the utterance is grounded: its content goes to FACTS. Otherwise, it goes to PENDING. @cite{ginzburg-cooper-2004} §6, ex. 82.

Equations

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

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.IS.integrateUtteranceStr (is_ : IS String String) (skel : UttSkeleton) (assign : CtxtAssignment) :

IS String String

String-specialized integration (content IS the fact).

Equations

is_.integrateUtteranceStr skel assign = is_.integrateUtterance skel assign id

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.IS.applyCoercion {Fact QContent : Type} (is_ : IS Fact QContent) (co : CoercionOutput) (toQ : String → QContent) :

IS Fact QContent

Apply a coercion output to the IS: set MAX-QUD and SAL-UTT.

Equations

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

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.IS.applyCoercionStr (is_ : IS String String) (co : CoercionOutput) :

IS String String

String-specialized coercion application.

Equations

is_.applyCoercionStr co = is_.applyCoercion co id

Instances For

source

theorem Theories.Pragmatics.Dialogue.KOS.DGB.initial_no_moves {Participant Fact QContent : Type} :

initial.moves = []

An empty DGB has no moves.

source

theorem Theories.Pragmatics.Dialogue.KOS.DGB.initial_no_qud {Participant Fact QContent : Type} :

initial.qud = []

An empty DGB has empty QUD.

source

theorem Theories.Pragmatics.Dialogue.KOS.DGB.initial_no_latestMove {Participant Fact QContent : Type} :

initial.latestMove = none

An empty DGB has no latest move.

source

theorem Theories.Pragmatics.Dialogue.KOS.coercions_same_salUtt (ant : UttSkeleton) (idx : String) :

Option.map CoercionOutput.salUtt (parameterFocussing ant idx) = Option.map CoercionOutput.salUtt (parameterIdentification ant idx)

Both coercion operations target the same SAL-UTT.

source

theorem Theories.Pragmatics.Dialogue.KOS.coercions_different_op (ant : UttSkeleton) (idx : String) (r1 r2 : CoercionOutput) (h1 : parameterFocussing ant idx = some r1) (h2 : parameterIdentification ant idx = some r2) :

r1.op ≠ r2.op

The two coercion operations produce different operation types.

source

theorem Theories.Pragmatics.Dialogue.KOS.resolved_means_no_unresolved (f : CtxtAssignment) (ps : CParamSet) (h : f.resolvesAll ps = true) :

f.unresolved ps = []

A fully resolved assignment leaves no unresolved parameters.

source

theorem Theories.Pragmatics.Dialogue.KOS.existential_gen_weakens (sk : UttSkeleton) (idx : String) :

List.length (existentialGeneralization sk idx).cparams ≤ List.length sk.cparams

Existential generalization never increases the parameter count.

source

instance Theories.Pragmatics.Dialogue.KOS.instHasContextSetDGBBProp {W Participant QContent : Type} :

Core.CommonGround.HasContextSet (DGB Participant (BProp W) QContent) W

DGB with BProp W facts projects to a context set. @cite{ginzburg-2012} Ch. 4: the DGB's FACTS field IS the common ground.

Equations

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

source

instance Theories.Pragmatics.Dialogue.KOS.instHasContextSetTISBProp {W Participant QContent : Type} :

Core.CommonGround.HasContextSet (TIS Participant (BProp W) QContent) W

TIS with BProp W facts inherits the DGB's context set.

Equations

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

source

theorem Theories.Pragmatics.Dialogue.KOS.tis_contextSet_eq_dgb {W Participant QContent : Type} (tis : TIS Participant (BProp W) QContent) :

Core.CommonGround.HasContextSet.toContextSet tis = Core.CommonGround.HasContextSet.toContextSet tis.dgb

TIS context set is extracted from the DGB.

source

def Theories.Pragmatics.Dialogue.KOS.DGB.mapFacts {Participant Fact Fact' QContent : Type} (f : Fact → Fact') (dgb : DGB Participant Fact QContent) :

DGB Participant Fact' QContent

Map over a DGB's fact type, preserving structure.

Equations

Theories.Pragmatics.Dialogue.KOS.DGB.mapFacts f dgb = { spkr := dgb.spkr, addr := dgb.addr, facts := List.map f dgb.facts, pending := dgb.pending, qud := dgb.qud }

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.DGB.mapQud {Participant Fact QContent QContent' : Type} (f : QContent → QContent') (dgb : DGB Participant Fact QContent) :

DGB Participant Fact QContent'

Map over a DGB's question type, preserving structure.

Equations

Theories.Pragmatics.Dialogue.KOS.DGB.mapQud f dgb = { spkr := dgb.spkr, addr := dgb.addr, facts := dgb.facts, pending := dgb.pending, qud := List.map f dgb.qud }

Instances For

source

theorem Theories.Pragmatics.Dialogue.KOS.DGB.mapFacts_length {Participant Fact Fact' QContent : Type} (f : Fact → Fact') (dgb : DGB Participant Fact QContent) :

(mapFacts f dgb).facts.length = dgb.facts.length

Mapping facts preserves fact count.

source

structure Theories.Pragmatics.Dialogue.KOS.LocProp (Cont : Type) :

Type

A locutionary proposition: a speech event with both form and content.

@cite{ginzburg-2012} Ch. 6, Appendix A (ex. 8d): LocProp replaces IllocProp in MOVES and Pending. A LocProp records the phonological form, syntactic category, and contextual parameters of the utterance — not just its illocutionary content. This is crucial for CRification: clarification requests target the form of the utterance, not just its content.

Parameterized over the content type Cont for grammar-neutrality. When Cont = String, this subsumes both PendingLoc and UttSkeleton.

phon : String
Phonological form of the utterance
cat : String
Syntactic category
cont : Cont
Semantic content
cparams : CParamSet
Contextual parameters: unresolved dependencies. Empty = fully grounded; non-empty = CRification may be needed.
constits : List SubUtterance
Sub-constituents accessible for clarification. @cite{ginzburg-2012} Ch. 6: any sub-utterance can be targeted by a CR.

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.instReprLocProp.repr {Cont✝ : Type} [Repr Cont✝] :

LocProp Cont✝ → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instReprLocProp {Cont✝ : Type} [Repr Cont✝] :

Repr (LocProp Cont✝)

Equations

Theories.Pragmatics.Dialogue.KOS.instReprLocProp = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprLocProp.repr }

source

def Theories.Pragmatics.Dialogue.KOS.PendingLoc.toLocProp (pl : PendingLoc) :

LocProp String

Convert a PendingLoc to a string-content LocProp.

Equations

pl.toLocProp = { phon := pl.utt, cat := pl.uttType, cont := pl.utt }

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.LocProp.toPendingLoc (lp : LocProp String) :

PendingLoc

Convert a LocProp String to a PendingLoc.

Equations

lp.toPendingLoc = { utt := lp.phon, uttType := lp.cat }

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.UttSkeleton.toLocProp (sk : UttSkeleton) :

LocProp String

Convert an UttSkeleton to a string-content LocProp. Subsumes the @cite{ginzburg-cooper-2004} skeleton representation.

Equations

sk.toLocProp = { phon := sk.phon, cat := sk.cat, cont := sk.cont, cparams := sk.cparams, constits := sk.constits }

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.LocProp.toSkeleton (lp : LocProp String) :

UttSkeleton

Convert a LocProp String back to an UttSkeleton.

Equations

lp.toSkeleton = { phon := lp.phon, cat := lp.cat, cont := lp.cont, cparams := lp.cparams, constits := lp.constits }

Instances For

source

theorem Theories.Pragmatics.Dialogue.KOS.skeleton_locprop_roundtrip (sk : UttSkeleton) :

sk.toLocProp.toSkeleton = sk

Round-trip: UttSkeleton → LocProp → UttSkeleton is identity.

source

structure Theories.Pragmatics.Dialogue.KOS.InfoStruc (QContent Cont : Type) :

Type

An information structure: a question paired with its focus-establishing constituents (FECs).

@cite{ginzburg-2012} Ch. 7, Appendix B (ex. 2): QUD entries are not bare questions but InfoStructs. The FEC records which sub-utterance(s) established the question — this is what enables NSU resolution.

Example: "Who left?" pushes an InfoStruc with:

q = "who left?"
fec = [the LocProp for "who"] A subsequent fragment "Bo" resolves the question by filling the FEC slot.

q : QContent
The question under discussion
fec : List (LocProp Cont)
Focus-establishing constituents from the utterance that introduced q

Instances For

source

instance Theories.Pragmatics.Dialogue.KOS.instReprInfoStruc {QContent✝ Cont✝ : Type} [Repr QContent✝] [Repr Cont✝] :

Repr (InfoStruc QContent✝ Cont✝)

Equations

Theories.Pragmatics.Dialogue.KOS.instReprInfoStruc = { reprPrec := Theories.Pragmatics.Dialogue.KOS.instReprInfoStruc.repr }

source

def Theories.Pragmatics.Dialogue.KOS.instReprInfoStruc.repr {QContent✝ Cont✝ : Type} [Repr QContent✝] [Repr Cont✝] :

InfoStruc QContent✝ Cont✝ → ℕ → Std.Format

Equations

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

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.InfoStruc.fromQuestion {QContent Cont : Type} (q : QContent) :

InfoStruc QContent Cont

Create an InfoStruc from a bare question (no FECs).

Equations

Theories.Pragmatics.Dialogue.KOS.InfoStruc.fromQuestion q = { q := q }

Instances For

source

def Theories.Pragmatics.Dialogue.KOS.InfoStruc.withFEC {QContent Cont : Type} (q : QContent) (fec : LocProp Cont) :

InfoStruc QContent Cont

Create an InfoStruc from a question and a wh-word sub-utterance.

Equations

Theories.Pragmatics.Dialogue.KOS.InfoStruc.withFEC q fec = { q := q, fec := [fec] }

Instances For

Documentation

Linglib.Theories.Pragmatics.Dialogue.KOS.Basic

KOS: Dialogue Gameboards #

@cite{ginzburg-2012} DGB (ex. 100, p. 111; final version ex. 113, p. 215) #

Known simplifications #

@cite{ginzburg-2012} TIS (ex. 93, p. 107) #

@cite{ginzburg-cooper-2004}: Clarification Ellipsis (§§3–6) #

Clarification Ellipsis Machinery #