KOS–Grammar Integration

@cite{ginzburg-2012} Ch. 5, @cite{ginzburg-sag-2000}

@cite{ginzburg-2012}'s central thesis: interaction is built into grammar. The Sign type has dgb-params and q-params — dialogue features living inside syntactic representations (Ch. 5, §5.2).

This module provides the integration point between HPSG signs and KOS dialogue gameboards. Neither HPSG/Core/Basic.lean nor KOS/Basic.lean knows about the other; this module imports both and defines:

1. DialogueSign — an HPSG sign extended with DGB-params and Q-params
2. Conversions to both HPSG.Synsem and KOS.LocProp
3. Example entries for wh-words and proper names

Design

This is opt-in integration: theories that don't need dialogue features continue to use plain HPSG signs. Theories that need the Ginzburg 2012 architecture import this module.

structure Dialogue.KOS.Grammar.DialogueSign (Cont : Type) : Type

An HPSG sign extended with dialogue features.

@cite{ginzburg-2012} Ch. 5 §5.2 (Sign schema, p. 122 ex. 12) introduces dgb-params and quest-dom as dialogue-relevant features on Sign:

• dgbParams: contextual parameters that must be resolved for grounding
• questDom: the question domain — what question the sign introduces

The third field, q-params (parameters contributed by interrogative elements like wh-words), is added in Ch. 8 §8.5.1 (ex. 101 p. 325, ex. 103 p. 326, ex. 104 p. 326) — Ginzburg's footnote on p. 122 explicitly notes "the field q-params introduced in section 8.5 of Chapter 8". We include it here in the canonical form for substrate convenience.

These correspond to DGB-PARAMS, Q-PARAMS, and QUEST-DOM in the book.

The Cont parameter is the content type — String for surface form, or richer typed values (BCheckableAustinian S, etc.) for TTR-typed grammars.

• phon : String

  Phonological form

• pos : UD.UPOS

  Part of speech (UD-based, matching HPSG.Synsem.cat)

• head : HPSG.HeadFeatures

  Head features from HPSG

• cont : Cont

  Semantic content

• dgbParams : CParamSet

  DGB-PARAMS: contextual parameters requiring grounding. Non-empty for referential NPs ("Bo"), demonstratives, etc.

• qParams : CParamSet

  Q-PARAMS: parameters contributed by interrogative elements. Non-empty for wh-words ("who", "what").

• questDom : Option String

  QUEST-DOM: the question this sign introduces (if interrogative).

def Dialogue.KOS.Grammar.DialogueSign.toSynsem {Cont : Type} (ds : DialogueSign Cont) : HPSG.Synsem

Project a DialogueSign to its HPSG Synsem (dropping dialogue features).

Equations

• ds.toSynsem = { cat := ds.pos, head := ds.head }

def Dialogue.KOS.Grammar.DialogueSign.toLocProp {Cont : Type} (ds : DialogueSign Cont) : LocProp Cont

Convert a DialogueSign to a LocProp for the KOS DGB. DGB-PARAMS become cparams (block grounding until resolved); Q-PARAMS become qcparams (travel with the sign, do not block grounding, but remain available for fragment-reprise queries per @cite{ginzburg-2012} §8.5.1, @cite{purver-ginzburg-2004}).

Equations

• ds.toLocProp = { phon := ds.phon, cat := toString ds.pos, cont := ds.cont, cparams := ds.dgbParams, qcparams := ds.qParams }

theorem Dialogue.KOS.Grammar.toLocProp_preserves_phon {Cont : Type} (ds : DialogueSign Cont) : ds.toLocProp.phon = ds.phon

Conversion preserves phonological form.

theorem Dialogue.KOS.Grammar.toLocProp_preserves_cont {Cont : Type} (ds : DialogueSign Cont) : ds.toLocProp.cont = ds.cont

Conversion preserves content.

theorem Dialogue.KOS.Grammar.toLocProp_dgb_to_cparams {Cont : Type} (ds : DialogueSign Cont) : ds.toLocProp.cparams = ds.dgbParams

Conversion routes DGB-PARAMS to cparams (the resolution channel).

theorem Dialogue.KOS.Grammar.toLocProp_q_to_qcparams {Cont : Type} (ds : DialogueSign Cont) : ds.toLocProp.qcparams = ds.qParams

Conversion routes Q-PARAMS to qcparams (the existential-witness channel) — the structural prerequisite for the Reprise Content Hypothesis.

def Dialogue.KOS.Grammar.who : DialogueSign String

"who" — a wh-word with Q-PARAMS. @cite{ginzburg-2012} Ch. 5: wh-words contribute Q-PARAMS that project to the QUEST-DOM of the clause.

Equations

• Dialogue.KOS.Grammar.who = { phon := "who", pos := UD.UPOS.PRON, cont := "who(x)", qParams := [{ index := "x", restriction := "individual" }], questDom := some "?x.P(x)" }

def Dialogue.KOS.Grammar.jo : DialogueSign String

"Jo" — a proper name with DGB-PARAMS. @cite{ginzburg-2012} Ch. 6: referential NPs introduce DGB-PARAMS that must be resolved (grounded) for the utterance to be integrated.

Equations

• Dialogue.KOS.Grammar.jo = { phon := "Jo", pos := UD.UPOS.PROPN, cont := "jo", dgbParams := [{ index := "jo_ref", restriction := "individual" }] }

def Dialogue.KOS.Grammar.left : DialogueSign String

"left" — an intransitive verb (no dialogue params).

Equations

• Dialogue.KOS.Grammar.left = { phon := "left", pos := UD.UPOS.VERB, cont := "leave(x)" }

theorem Dialogue.KOS.Grammar.jo_needs_grounding : ¬jo.toLocProp.isFullyResolved

"Jo" needs grounding: it has non-empty DGB-PARAMS.

theorem Dialogue.KOS.Grammar.who_has_qparams : who.qParams ≠ []

"who" has Q-PARAMS (it's interrogative).

theorem Dialogue.KOS.Grammar.who_no_grounding_needed : who.toLocProp.isFullyResolved

"who" doesn't need grounding (Q-PARAMS ≠ DGB-PARAMS).

theorem Dialogue.KOS.Grammar.left_plain : left.dgbParams = [] ∧ left.qParams = []

"left" has no dialogue features.

theorem Dialogue.KOS.Grammar.slash_cparams_both_decrease (sv : HPSG.SlashValue) (cat : UD.UPOS) (ps : CParamSet) (idx : String) : (sv.discharge cat).gaps.length ≤ sv.gaps.length ∧ (List.filter (fun (x : CParam) => x.index != idx) ps).length ≤ List.length ps

Structural analogy: discharging a SLASH gap and resolving a C-PARAM both reduce the count of outstanding dependencies.

Both SLASH (filler-gap) and C-PARAMS (grounding) are sets of outstanding dependencies discharged by similar mechanisms. This theorem makes the isomorphism explicit.