KOS: Genre Relevance & Outcome Fulfillment

@cite{ginzburg-2012} §4.6 (pp. 101–110)

The genreRelevant predicate (eq. 90 p. 105) constraining which initiating moves are felicitous given a conversational genre, plus the outcome-fulfillability machinery (ex. 89 p. 105) that ex. 90 reduces to.

Relevance per ex. 90 p. 105

Ginzburg: "m0 is relevant to G0 in dgb0 for A iff A believes that outcome(dgb0 ⊕moves m0, G0) will be fulfilled."

We model this as: simulate adding the move's question content to QUD, then check whether the resulting QUD is consistent with the genre's anticipated questions (qnud) or its explicit qudConstraint.

Two genre-relevance predicates

This file provides two relevance computations:

• genreRelevant — the thin variant: uses the genre's qudConstraint predicate (no DecidableEq requirement). Suitable for genres that encode their constraints procedurally (e.g., bakery accepts only bread-related questions).
• genreRelevantViaQnud — the qnud-based variant: requires [DecidableEq QContent]. Suitable for genres that enumerate their anticipated questions explicitly. Models the eq. 88 qnud field directly.

Both project through the InfoStruc layer that QUD now stores (per Ch. 6 final shape, with QUD-as-InfoStruc treatment per §7.6 FEC discussion).

Outcome predicate

GenreType.outcomeFulfilled formalizes ex. 89's outcome relation: a DGB fulfills the genre's outcome when its QUD-projected questions are all in the anticipated qnud set. This is the substrate ex. 90 reduces to ("outcome will be fulfilled").

Deferred

Ginzburg's full TTR record (ex. 88) also includes agent fields, utt-time, facts subset, and a co-propositionality constraint relating MaxQUD to the move's content. These need richer machinery (TTR types for agents, co-propositionality predicates) that downstream consumers can add when they exercise these claims.

def Dialogue.KOS.GenreType.outcomeFulfilled {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [DecidableEq QContent] (genre : GenreType Fact QContent) (dgb : DGB P Fact QContent Cont) : Prop

A DGB fulfills the genre's outcome when its QUD's projected questions are all anticipated (i.e., in genre.qnud).

@cite{ginzburg-2012} ex. 89 (p. 105): the outcome of a dialogue is fulfilled when its trajectory is consistent with the genre's anticipated question stack. The full version also requires move sequence to be consistent with anticipatedMoves; we model the QUD half here.

Equations

• genre.outcomeFulfilled dgb = ∀ is ∈ dgb.qud, is.q ∈ genre.qnud

@[implicit_reducible]

instance Dialogue.KOS.instDecidableOutcomeFulfilled {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [DecidableEq QContent] (genre : GenreType Fact QContent) (dgb : DGB P Fact QContent Cont) : Decidable (genre.outcomeFulfilled dgb)

Equations

• Dialogue.KOS.instDecidableOutcomeFulfilled genre dgb = Dialogue.KOS.instDecidableOutcomeFulfilled._aux_1 genre dgb

def Dialogue.KOS.genreRelevant {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (genre : GenreType Fact QContent) (dgb : DGB P Fact QContent Cont) (m : IllocMove Fact QContent) : Prop

A move is genre-relevant via the explicit qudConstraint predicate.

@cite{ginzburg-2012} ex. 90 (p. 105): "m0 is relevant to G0 in dgb0 for A iff A believes that outcome(dgb0 ⊕moves m0, G0) will be fulfilled."

This thin variant uses the genre's qudConstraint field (a procedural predicate on the projected QUD content). For a qnud-list-based variant, see genreRelevantViaQnud.

Equations

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

@[implicit_reducible]

instance Dialogue.KOS.instDecidableGenreRelevant {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (genre : GenreType Fact QContent) (dgb : DGB P Fact QContent Cont) (m : IllocMove Fact QContent) : Decidable (genreRelevant genre dgb m)

Equations

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

def Dialogue.KOS.genreRelevantViaQnud {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [DecidableEq QContent] (genre : GenreType Fact QContent) (dgb : DGB P Fact QContent Cont) (m : IllocMove Fact QContent) : Prop

A move is genre-relevant via the qnud (anticipated questions) field.

Ex. 90 reduced to the operational form: simulating the move's QUD-incrementation, the resulting QUD must consist entirely of anticipated questions.

Equations

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

@[implicit_reducible]

instance Dialogue.KOS.instDecidableGenreRelevantViaQnud {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [DecidableEq QContent] (genre : GenreType Fact QContent) (dgb : DGB P Fact QContent Cont) (m : IllocMove Fact QContent) : Decidable (genreRelevantViaQnud genre dgb m)

Equations

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

theorem Dialogue.KOS.genreRelevantViaQnud_preserves_outcomeFulfilled {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} [DecidableEq QContent] (genre : GenreType Fact QContent) (dgb : DGB P Fact QContent Cont) (_h : genre.outcomeFulfilled dgb) (m : IllocMove Fact QContent) (hm : genreRelevantViaQnud genre dgb m) : match m.questionContent with | none => True | some q => q ∈ genre.qnud

Genre-relevance and outcome-fulfillment connect: if every move added to a DGB is genreRelevantViaQnud, then after the moves the outcome is fulfilled (qud entries are all anticipated). This is a structural witness that the qnud-based predicate genuinely tracks ex. 91's outcome relation.