Propositional Lexemes

@cite{ginzburg-2012} Appendix C (exx. 10–12)

Propositional lexemes are words whose meaning is defined by reference to the DGB state — they cannot be interpreted without knowing what question is under discussion (MaxQUD) and what assertion is pending (MaxPending).

Examples: "yes", "no", "mmh", "uh-huh", "huh".

These are NOT ordinary content words — their denotation is a function from DGB state to propositional content. This distinguishes them from regular affirmatives/negatives in languages that use verbal echo (e.g., Mandarin, Finnish).

Key Properties

1. DGB-dependent meaning: content is determined by MaxQUD/MaxPending
2. Polarity: yes/mmh affirm; no negates
3. Register: mmh/uh-huh are informal variants of yes
4. CR function: huh requests clarification (constituent reading)

inductive Fragments.English.PropositionalLexemes.DGBRef : Type

Which DGB component a propositional lexeme references.

• maxQUD : DGBRef

  References MaxQUD — the topmost question under discussion

• maxPending : DGBRef

  References MaxPending — the most recent ungrounded assertion

• both : DGBRef

  References both (e.g., for CR-initiating lexemes)

def Fragments.English.PropositionalLexemes.instReprDGBRef.repr : DGBRef → ℕ → Std.Format

Equations

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

instance Fragments.English.PropositionalLexemes.instReprDGBRef : Repr DGBRef

Equations

• Fragments.English.PropositionalLexemes.instReprDGBRef = { reprPrec := Fragments.English.PropositionalLexemes.instReprDGBRef.repr }

instance Fragments.English.PropositionalLexemes.instDecidableEqDGBRef : DecidableEq DGBRef

Equations

• Fragments.English.PropositionalLexemes.instDecidableEqDGBRef x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.English.PropositionalLexemes.instBEqDGBRef.beq : DGBRef → DGBRef → Bool

Equations

• Fragments.English.PropositionalLexemes.instBEqDGBRef.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.English.PropositionalLexemes.instBEqDGBRef : BEq DGBRef

Equations

• Fragments.English.PropositionalLexemes.instBEqDGBRef = { beq := Fragments.English.PropositionalLexemes.instBEqDGBRef.beq }

inductive Fragments.English.PropositionalLexemes.Polarity : Type

Polarity of a propositional lexeme's contribution.

• positive : Polarity
• negative : Polarity
• cr : Polarity

instance Fragments.English.PropositionalLexemes.instReprPolarity : Repr Polarity

Equations

• Fragments.English.PropositionalLexemes.instReprPolarity = { reprPrec := Fragments.English.PropositionalLexemes.instReprPolarity.repr }

def Fragments.English.PropositionalLexemes.instReprPolarity.repr : Polarity → ℕ → Std.Format

Equations

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

instance Fragments.English.PropositionalLexemes.instDecidableEqPolarity : DecidableEq Polarity

Equations

• Fragments.English.PropositionalLexemes.instDecidableEqPolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.English.PropositionalLexemes.instBEqPolarity.beq : Polarity → Polarity → Bool

Equations

• Fragments.English.PropositionalLexemes.instBEqPolarity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.English.PropositionalLexemes.instBEqPolarity : BEq Polarity

Equations

• Fragments.English.PropositionalLexemes.instBEqPolarity = { beq := Fragments.English.PropositionalLexemes.instBEqPolarity.beq }

structure Fragments.English.PropositionalLexemes.PropLexeme : Type

A propositional lexeme: a word whose meaning depends on DGB state.

• phon : String

  Phonological form

• cat : String

  Syntactic category

• dgbRef : DGBRef

  Which DGB component this lexeme references

• polarity : Polarity

  Polarity of the response

• contentRule : String

  Informal description of the content rule

• source : String

  Source in @cite{ginzburg-2012}

instance Fragments.English.PropositionalLexemes.instReprPropLexeme : Repr PropLexeme

Equations

• Fragments.English.PropositionalLexemes.instReprPropLexeme = { reprPrec := Fragments.English.PropositionalLexemes.instReprPropLexeme.repr }

def Fragments.English.PropositionalLexemes.instReprPropLexeme.repr : PropLexeme → ℕ → Std.Format

Equations

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

def Fragments.English.PropositionalLexemes.instDecidableEqPropLexeme.decEq (x✝ x✝¹ : PropLexeme) : Decidable (x✝ = x✝¹)

Equations

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

instance Fragments.English.PropositionalLexemes.instDecidableEqPropLexeme : DecidableEq PropLexeme

Equations

• Fragments.English.PropositionalLexemes.instDecidableEqPropLexeme = Fragments.English.PropositionalLexemes.instDecidableEqPropLexeme.decEq

instance Fragments.English.PropositionalLexemes.instBEqPropLexeme : BEq PropLexeme

Equations

• Fragments.English.PropositionalLexemes.instBEqPropLexeme = { beq := Fragments.English.PropositionalLexemes.instBEqPropLexeme.beq }

def Fragments.English.PropositionalLexemes.instBEqPropLexeme.beq : PropLexeme → PropLexeme → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.PropositionalLexemes.instBEqPropLexeme.beq x✝¹ x✝ = false

def Fragments.English.PropositionalLexemes.yes : PropLexeme

"yes" — propositional abstract of MaxQUD. @cite{ginzburg-2012} §7.5, ex. 21 (p. 232): content = max-qud([ ]). When MaxQUD = ?p (a polar question), max-qud([ ]) = p. DGB-PARAMS references max-qud : PolQuestion.

Equations

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

def Fragments.English.PropositionalLexemes.no : PropLexeme

"no" — negation of MaxQUD's propositional abstract. @cite{ginzburg-2012} §7.5, ex. 25 (p. 233): content is a proposition such that NegProp(cont) ∧ SimpleAns(cont, max-qud). DGB-PARAMS references max-qud : PolQuestion.

Equations

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

def Fragments.English.PropositionalLexemes.mmh : PropLexeme

"mmh" / "uh-huh" — informal positive acknowledgment. @cite{ginzburg-2012} Appendix C.

Equations

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

def Fragments.English.PropositionalLexemes.huh : PropLexeme

"huh" — clarification request. @cite{ginzburg-2012} Appendix C.

Equations

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

def Fragments.English.PropositionalLexemes.propLexemes : List PropLexeme

Equations

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

theorem Fragments.English.PropositionalLexemes.all_have_content_rules : (propLexemes.all fun (l : PropLexeme) => !l.contentRule.isEmpty) = true

All propositional lexemes have non-empty content rules.

theorem Fragments.English.PropositionalLexemes.yes_no_reference_maxQUD : yes.dgbRef = DGBRef.maxQUD ∧ no.dgbRef = DGBRef.maxQUD

yes and no both reference MaxQUD (not MaxPending directly). @cite{ginzburg-2012} §7.5: both derive content from max-qud via dgb-params.

theorem Fragments.English.PropositionalLexemes.yes_no_opposite_polarity : yes.polarity ≠ no.polarity

yes and no have opposite polarity.

theorem Fragments.English.PropositionalLexemes.huh_unique_cr : List.filter (fun (x : PropLexeme) => x.polarity == Polarity.cr) propLexemes = [huh]

huh is the only CR lexeme.