Documentation

Linglib.Theories.Dialogue.KOS.NSUTaxonomy

KOS: NSU Classification (Table 7.3 + Table 7.4) #

@cite{ginzburg-2012} Ch. 7 §7.2 (pp. 219–222) @cite{fernandez-2006}

The empirical taxonomy of non-sentential utterances from @cite{ginzburg-2012} Tables 7.3 and 7.4, derived from the BNC subcorpus study by @cite{fernandez-2006} (200 speaker-turns from 54 BNC files; 14,315 sentences; 1,299 NSUs found, of which 1,283 = 98.9% classified).

Class enumeration (Table 7.3, p. 221) #

Sixteen classes — the original Table 7.3 lists 15 because Sluice (24) is undivided there, but Table 7.4 (p. 222) splits Sluice into Reprise Sluice (13, a metacommunicative query) and Direct Sluice (11, an extension move). To match Table 7.4 functional grouping arithmetic, we adopt the split here.

Functional grouping (Table 7.4, p. 222) #

Four functional categories with cell-summed totals:

GroupCell sumMembers
Positive Feedback685plainAck (599), repeatedAck (86)
Answers403shortAnswer (188), affirmAnswer (105), rejection (49), repeatedAffirm (26),
helpfulRejection (24), propositionalModifier (11)
Metacommunicative Q's132clarificationEllipsis (79), repriseSluice (13), checkQuestion (22), filler (18)
Extension Moves63factiveModifier (27), bareModifier (15), conjFrag (10), directSluice (11)

Cell-sum total: 685 + 403 + 132 + 63 = 1283 ✓ (matches Table 7.3 total).

(Ginzburg's Table 7.4 header totals show 685/413/132/63 = 1293, off by 10 from the cell sums — the 10-utterance discrepancy is internal to the book.)

Anti-pattern avoided: aggregate count theorems #

Earlier formaliser versions had theorem nsu_total_1283 : ... = 1283 and theorem functional_groups_sum_to_total : pf + ans + mcq + ext = 1283. Per MEMORY.md feedback_no_aggregate_count_theorems, these go stale on any data revision and prove nothing about Ginzburg's framework — only that the formaliser's transcription is internally consistent.

The pattern this file uses instead: a single freqTable source of truth with a structural coherence theorem (frequency_coherent) that enforces both NSUClass.frequency and NSUClass.toFunction to agree with the table per class. If any cell changes, the coherence theorem fails until both functions are updated — automatic drift detection without numeric assertions.

source
inductive Dialogue.KOS.NSUClass :
Type

The 16 NSU classes from @cite{ginzburg-2012} Table 7.3 + Table 7.4.

Sluice is split into Reprise Sluice (metacommunicative) and Direct Sluice (extension move) per Table 7.4 — the original Table 7.3 had a single Sluice (24) entry but Table 7.4 partitions it 13 + 11.

  • plainAcknowledgement : NSUClass

    "mmh", "uh-huh" — acknowledges preceding utterance (599).

  • shortAnswer : NSUClass

    "Bo" — fills argument slot in MaxQUD (188).

  • affirmativeAnswer : NSUClass

    "Yes" — positive answer to polar query (105).

  • repeatedAcknowledgement : NSUClass

    "Bo, hmm" — acknowledgement with repetition (86).

  • clarificationEllipsis : NSUClass

    "Bo?" — clarification ellipsis (79).

  • rejection : NSUClass

    "No" — negative answer to polar query / assertion (49).

  • factiveModifier : NSUClass

    "Great!" — factive modifier (27).

  • repeatedAffirmativeAnswer : NSUClass

    "Bo, yes" — affirmative with repetition (26).

  • helpfulRejection : NSUClass

    "No, Max" — rejection with helpful alternative (24).

  • repriseSluice : NSUClass

    "Who?" — bare wh-phrase reprising the antecedent (13).

  • directSluice : NSUClass

    "Who?" — bare wh-phrase requesting new information (11).

  • checkQuestion : NSUClass

    "Okay?" — rising-intonation check (22).

  • filler : NSUClass

    "uh", "well" — hesitation / floor-holding (18).

  • bareModifierPhrase : NSUClass

    "Yesterday" — bare modifier phrase (15).

  • propositionalModifier : NSUClass

    "Maybe" — propositional modifier (11).

  • conjunctionFragment : NSUClass

    "And Max" — conjunction + fragment (10).

Instances For
    source
    def Dialogue.KOS.instReprNSUClass.repr :
    NSUClass → Nat → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Dialogue.KOS.instReprNSUClass :
      Repr NSUClass
      Equations
      source
      @[implicit_reducible]
      instance Dialogue.KOS.instDecidableEqNSUClass :
      DecidableEq NSUClass
      Equations
      source
      inductive Dialogue.KOS.NSUFunction :
      Type

      Functional grouping from @cite{ginzburg-2012} Table 7.4 (p. 222).

      • positiveFeedback : NSUFunction

        Positive feedback (685): plain + repeated acknowledgement.

      • answer : NSUFunction

        Answers (403): short, affirmative, rejection, repeated affirmative, helpful rejection, propositional modifier.

      • metacommunicativeQuery : NSUFunction

        Metacommunicative queries (132): CE + reprise sluice + check + filler.

      • extensionMove : NSUFunction

        Extension moves (63): factive modifier + bare modifier + conj+frag

        • direct sluice.
      Instances For
        source
        @[implicit_reducible]
        instance Dialogue.KOS.instReprNSUFunction :
        Repr NSUFunction
        Equations
        source
        def Dialogue.KOS.instReprNSUFunction.repr :
        NSUFunction → Nat → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance Dialogue.KOS.instDecidableEqNSUFunction :
          DecidableEq NSUFunction
          Equations
          source
          def Dialogue.KOS.freqTable :
          List (NSUClass × NSUFunction × Nat)

          Single source of truth for Tables 7.3 + 7.4: each row pairs an NSU class with its functional group and BNC frequency. Every entry below is verifiable against the published tables.

          Updating Table 7.3 or Table 7.4 means editing exactly one row here; the coherence theorem frequency_coherent ensures NSUClass.frequency and NSUClass.toFunction stay in sync.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Dialogue.KOS.allNSUClasses :
            List NSUClass

            All 16 NSU classes, ordered to match freqTable.

            Equations
            Instances For
              source
              def Dialogue.KOS.NSUClass.frequency :
              NSUClass → Nat

              BNC frequency for each NSU class (Table 7.3 cell + Table 7.4 sluice split).

              Equations
              Instances For
                source
                def Dialogue.KOS.NSUClass.toFunction :
                NSUClass → NSUFunction

                Functional group for each NSU class (Table 7.4 partitioning).

                Equations
                Instances For
                  source
                  theorem Dialogue.KOS.frequency_coherent :
                  (allNSUClasses.all fun (c : NSUClass) => decide ((c, c.toFunction, c.frequency) ∈ freqTable)) = true

                  Coherence: every class has a row in freqTable whose function-tag and frequency match the per-class projections. Updating the table without updating the projections (or vice versa) breaks this theorem.

                  This is the structural drift sentry that replaces the previous aggregate nsu_total_1283 and functional_groups_sum_to_total count theorems.

                  source
                  theorem Dialogue.KOS.allNSUClasses_complete :
                  allNSUClasses.length = 16

                  All 16 classes are present in the freqTable (in order).