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 Theories.Pragmatics.Dialogue.KOS.Grammar.DialogueSign : Type

An HPSG sign extended with dialogue features.

@cite{ginzburg-2012} Ch. 5, §5.2: the sign type has three dialogue-relevant features:

• dgbParams: contextual parameters that must be resolved for grounding
• qParams: parameters contributed by interrogative elements (wh-words)
• questDom: the question domain — what question the sign introduces

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

• phon : String

  Phonological form

• pos : UD.UPOS

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

• head : HPSG.HeadFeatures

  Head features from HPSG

• cont : String

  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).

instance Theories.Pragmatics.Dialogue.KOS.Grammar.instReprDialogueSign : Repr DialogueSign

Equations

• Theories.Pragmatics.Dialogue.KOS.Grammar.instReprDialogueSign = { reprPrec := Theories.Pragmatics.Dialogue.KOS.Grammar.instReprDialogueSign.repr }

def Theories.Pragmatics.Dialogue.KOS.Grammar.instReprDialogueSign.repr : DialogueSign → ℕ → Std.Format

Equations

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

def Theories.Pragmatics.Dialogue.KOS.Grammar.DialogueSign.toSynsem (ds : DialogueSign) : HPSG.Synsem

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

Equations

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

def Theories.Pragmatics.Dialogue.KOS.Grammar.DialogueSign.toLocProp (ds : DialogueSign) : LocProp String

Convert a DialogueSign to a LocProp for the KOS DGB. DGB-PARAMS become cparams; Q-PARAMS are not cparams (they are contributed, not requiring resolution).

Equations

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

theorem Theories.Pragmatics.Dialogue.KOS.Grammar.toLocProp_preserves_phon (ds : DialogueSign) : ds.toLocProp.phon = ds.phon

Conversion preserves phonological form.

theorem Theories.Pragmatics.Dialogue.KOS.Grammar.toLocProp_preserves_cont (ds : DialogueSign) : ds.toLocProp.cont = ds.cont

Conversion preserves content.

def Theories.Pragmatics.Dialogue.KOS.Grammar.who : DialogueSign

"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

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

def Theories.Pragmatics.Dialogue.KOS.Grammar.jo : DialogueSign

"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

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

def Theories.Pragmatics.Dialogue.KOS.Grammar.left : DialogueSign

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

Equations

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

theorem Theories.Pragmatics.Dialogue.KOS.Grammar.jo_needs_grounding : jo.toLocProp.isFullyResolved = false

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

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

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

theorem Theories.Pragmatics.Dialogue.KOS.Grammar.who_no_grounding_needed : who.toLocProp.isFullyResolved = true

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

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

"left" has no dialogue features.

theorem Theories.Pragmatics.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.