Documentation

Linglib.Theories.Dialogue.KOS.Defs

KOS: Type Definitions #

@cite{ginzburg-2012}

Pure type definitions for the KOS framework. No operations beyond the trivial constructors / accessors required for type families to compose. Operations live in sibling files (Basic, InquiryCycle, Grounding, Genre, Move).

TTR-residence #

KOS is built on TTR (@cite{cooper-2023}). LocProp is a structural refinement of TTRSign String Cont (Cooper §2.5 ex 70): same phon : String + cont : Cont fields, plus dialogue-grade additions (cat, cparams, qcparams, constits). The SubtypeOf instance and the forgetful projection LocProp.toTTRSign live with the type definition itself — LocProp ⊐ TTRSign is part of the substrate, not a downstream bridge file.

(Lean's deriving machinery doesn't compose smoothly with extends-based inheritance when parent fields involve free type parameters, so we keep LocProp as a flat structure and provide the forgetful map by hand. The structural commitment is unchanged: every LocProp projects to a TTRSign, dischargeable via the typeclass.)

Universe pinning #

Participant, Fact, QContent are universe-polymorphic (Type*). Cont is pinned to Type (= Type 0) because it flows into the TTRSign String Cont projection (LocProp.toTTRSign), and TTRSign is itself Type-pinned in Theories/Semantics/TypeTheoretic/Core.lean (Cooper's "type-is-a-type" semantics requires Type 0 for the carrier). Same pinning applies in KOS/Austinian.lean (where BCheckableAustinian and TTRQuestionB similarly require Type) and in KOS/CooperInfoState.lean (where InfoState from TypeTheoretic requires all type parameters at Type).

Migrating Cont to Type* requires lifting the entire TTR substrate to universe polymorphism — out of scope for this layer's cleanup. Document, don't migrate.

Architecture #

This file collects the load-bearing KOS types in dependency order:

Ginzburg fidelity #

The DGB and TIS types take a Cont parameter for utterance content, enabling the Ch. 6 final shape (ex. 43 p. 175) where Pending stores LocProp Cont (utterances with form + cparams + content) and QUD stores InfoStruc QContent Cont (questions paired with their focus-establishing constituents, §6.3 (Pending added to DGB; QUD-as-InfoStruc treatment in §7.6 FEC discussion)). Moves still use IllocMove Fact QContent for case-analysis convenience; in the book's final version they are also LocProps, but the IllocMove constructor tags carry information our consumers find useful.

source
inductive Dialogue.KOS.IllocMove (Fact : Type u_1) (QContent : Type u_2) :
Type (max u_1 u_2)

An illocutionary move in dialogue.

@cite{ginzburg-2012} Ch. 4: moves are illocutionary propositions — speech events classified by their illocutionary force. We abstract over the content: assertions carry propositional content, queries carry question content.

The Fact and QContent parameters match the DGB's content types.

Note: in the Ch. 6 final version (p. 215), MOVES stores LocProps (situated speech events). Here we keep IllocMove for case-analysis convenience — every constructor tag is a proper inductive case, which downstream pattern-matching consumers depend on.

  • assert {Fact : Type u_1} {QContent : Type u_2} : Fact → IllocMove Fact QContent

    An assertion: speaker commits to propositional content.

  • ask {Fact : Type u_1} {QContent : Type u_2} : QContent → IllocMove Fact QContent

    A query: speaker raises a question.

  • accept {Fact : Type u_1} {QContent : Type u_2} : Fact → IllocMove Fact QContent

    Accept: addressee grounds an assertion.

  • check {Fact : Type u_1} {QContent : Type u_2} : Fact → IllocMove Fact QContent

    Check: addressee requests confirmation of an assertion.

  • confirm {Fact : Type u_1} {QContent : Type u_2} : Fact → IllocMove Fact QContent

    Confirm: speaker confirms in response to check.

  • greet {Fact : Type u_1} {QContent : Type u_2} : IllocMove Fact QContent

    Greeting.

  • counterGreet {Fact : Type u_1} {QContent : Type u_2} : IllocMove Fact QContent

    Counter-greeting.

Instances For
    source
    def Dialogue.KOS.instReprIllocMove.repr {Fact✝ : Type u_1} {QContent✝ : Type u_2} [Repr Fact✝] [Repr QContent✝] :
    IllocMove Fact✝ QContent✝ → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Dialogue.KOS.instReprIllocMove {Fact✝ : Type u_1} {QContent✝ : Type u_2} [Repr Fact✝] [Repr QContent✝] :
      Repr (IllocMove Fact✝ QContent✝)
      Equations
      source
      @[implicit_reducible]
      instance Dialogue.KOS.instDecidableEqIllocMove {Fact✝ : Type u_1} {QContent✝ : Type u_2} [DecidableEq Fact✝] [DecidableEq QContent✝] :
      DecidableEq (IllocMove Fact✝ QContent✝)
      Equations
      source
      def Dialogue.KOS.instDecidableEqIllocMove.decEq {Fact✝ : Type u_1} {QContent✝ : Type u_2} [DecidableEq Fact✝] [DecidableEq QContent✝] (x✝ x✝¹ : IllocMove Fact✝ QContent✝) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        def Dialogue.KOS.IllocMove.factContent {Fact : Type u_1} {QContent : Type u_2} :
        IllocMove Fact QContent → Option Fact

        Extract the propositional content from a move, if any.

        Equations
        Instances For
          source
          def Dialogue.KOS.IllocMove.questionContent {Fact : Type u_1} {QContent : Type u_2} :
          IllocMove Fact QContent → Option QContent

          Extract the question content from a move, if any.

          Equations
          Instances For
            source
            structure Dialogue.KOS.CParam :
            Type

            A contextual parameter with INDEX and RESTR(ICTION).

            Each C-PARAM has an index variable (e.g., "b" for the referent of "Bo") and a restriction characterizing what values are acceptable (e.g., "named(Bo)(b)"). @cite{ginzburg-cooper-2004} ex. 28; surviving in @cite{ginzburg-2012} as the dgb-params primitive.

            This type is shared between 2004-paper-anchored studies (resolves/coercion operations live in the 2004 study file) and 2012-paper-anchored substrate (LocProp.cparams uses this as the dgb-params apparatus).

            • index : String
            • restriction : String
            Instances For
              source
              def Dialogue.KOS.instReprCParam.repr :
              CParam → ℕ → Std.Format
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[implicit_reducible]
                instance Dialogue.KOS.instReprCParam :
                Repr CParam
                Equations
                source
                @[implicit_reducible]
                instance Dialogue.KOS.instDecidableEqCParam :
                DecidableEq CParam
                Equations
                source
                def Dialogue.KOS.instDecidableEqCParam.decEq (x✝ x✝¹ : CParam) :
                Decidable (x✝ = x✝¹)
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[reducible, inline]
                  abbrev Dialogue.KOS.CParamSet :
                  Type

                  A set of contextual parameters, analogous to HPSG.SlashValue.

                  Both are non-local features (sets of outstanding dependencies):

                  • SLASH tracks syntactic gaps (filler-gap dependencies)
                  • C-PARAMS tracks contextual dependencies (referent resolution)

                  Both propagate via the same amalgamation mechanism (ex. 29 ≈ Nonlocal Feature Principle) and get discharged at specific sites.

                  Equations
                  Instances For
                    source
                    structure Dialogue.KOS.SubUtterance :
                    Type

                    A sub-utterance: the minimal addressable unit for clarification.

                    Every sub-utterance encodes PHON, CAT, and CONT — this fractal heterogeneity is what makes clarification of any constituent possible. @cite{ginzburg-cooper-2004} §2; surviving in @cite{ginzburg-2012} Ch. 6 as the constits field on LocProps.

                    • phon : String
                    • cat : String
                    • cont : String
                    Instances For
                      source
                      def Dialogue.KOS.instReprSubUtterance.repr :
                      SubUtterance → ℕ → Std.Format
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[implicit_reducible]
                        instance Dialogue.KOS.instReprSubUtterance :
                        Repr SubUtterance
                        Equations
                        source
                        def Dialogue.KOS.instDecidableEqSubUtterance.decEq (x✝ x✝¹ : SubUtterance) :
                        Decidable (x✝ = x✝¹)
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[implicit_reducible]
                          instance Dialogue.KOS.instDecidableEqSubUtterance :
                          DecidableEq SubUtterance
                          Equations
                          source
                          structure Dialogue.KOS.LocProp (Cont : Type) :
                          Type

                          A locutionary proposition: a speech event with both form and content.

                          @cite{ginzburg-2012} Ch. 6, Appendix A (ex. 8d): LocProp replaces IllocProp in MOVES and Pending. A LocProp records the phonological form, syntactic category, and contextual parameters of the utterance — not just its illocutionary content. This is crucial for CRification: clarification requests target the form of the utterance, not just its content.

                          Parameterized over the content type Cont for grammar-neutrality. When Cont = String, this subsumes the 2004 UttSkeleton representation.

                          The two parameter fields reflect @cite{ginzburg-2012}'s sign architecture: cparams carries dgb-params (referential, requiring contextual anchoring); qcparams carries q-params (existentially closed at proposition level). The asymmetry: only cparams triggers CRification under integrateLocProp; q-params travel with the sign but do not block grounding. This is the structural prerequisite for the Reprise Content Hypothesis (@cite{purver-ginzburg-2004}, @cite{ginzburg-2012} §8.5.1): fragment reprises query the q-params record, not the dgb-params one.

                          • phon : String

                            Phonological form of the utterance — same field name as TTRSign.phon.

                          • cat : String

                            Syntactic category

                          • cont : Cont

                            Semantic content — same field name as TTRSign.cont.

                          • cparams : CParamSet

                            DGB-PARAMS: referential parameters requiring contextual resolution. Empty = fully grounded; non-empty = CRification may be needed.

                          • qcparams : CParamSet

                            Q-PARAMS: parameters whose index is existentially closed at the sentential level (@cite{ginzburg-2012} §8.5.1, ex. 101–103, p. 325–326). Travel with the sign but do not trigger CRification — they contribute the descriptive content of non-referential NPs.

                          • constits : List SubUtterance

                            Sub-constituents accessible for clarification. @cite{ginzburg-2012} Ch. 6: any sub-utterance can be targeted by a CR.

                          Instances For
                            source
                            @[implicit_reducible]
                            instance Dialogue.KOS.instReprLocProp {Cont✝ : Type} [Repr Cont✝] :
                            Repr (LocProp Cont✝)
                            Equations
                            source
                            def Dialogue.KOS.instReprLocProp.repr {Cont✝ : Type} [Repr Cont✝] :
                            LocProp Cont✝ → ℕ → Std.Format
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[implicit_reducible]
                              instance Dialogue.KOS.instDecidableEqLocProp {Cont✝ : Type} [DecidableEq Cont✝] :
                              DecidableEq (LocProp Cont✝)
                              Equations
                              source
                              def Dialogue.KOS.instDecidableEqLocProp.decEq {Cont✝ : Type} [DecidableEq Cont✝] (x✝ x✝¹ : LocProp Cont✝) :
                              Decidable (x✝ = x✝¹)
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def Dialogue.KOS.LocProp.toTTRSign {Cont : Type} (lp : LocProp Cont) :
                                Semantics.TypeTheoretic.TTRSign String Cont

                                Forgetful projection LocProp Cont → TTRSign String Cont: keep phon

                                • cont, drop dialogue-grade fields.
                                Equations
                                Instances For
                                  source
                                  @[implicit_reducible]
                                  instance Dialogue.KOS.instSubtypeOfLocPropTTRSignString {Cont : Type} :
                                  LocProp Cont ⊑ Semantics.TypeTheoretic.TTRSign String Cont

                                  LocProp Cont ⊐ TTRSign String Cont is structural: every LocProp projects to a TTRSign via LocProp.toTTRSign.

                                  Equations
                                  source
                                  @[simp]
                                  theorem Dialogue.KOS.LocProp.toTTRSign_phon {Cont : Type} (lp : LocProp Cont) :
                                  lp.toTTRSign.phon = lp.phon

                                  The projection preserves phon.

                                  source
                                  @[simp]
                                  theorem Dialogue.KOS.LocProp.toTTRSign_cont {Cont : Type} (lp : LocProp Cont) :
                                  lp.toTTRSign.cont = lp.cont

                                  The projection preserves cont.

                                  source
                                  structure Dialogue.KOS.InfoStruc (QContent : Type u_1) (Cont : Type) :
                                  Type u_1

                                  An information structure: a question paired with its focus-establishing constituents (FECs).

                                  @cite{ginzburg-2012} Ch. 7, Appendix B (ex. 2): QUD entries are not bare questions but InfoStructs. The FEC records which sub-utterance(s) established the question — this is what enables NSU resolution.

                                  Example: "Who left?" pushes an InfoStruc with:

                                  • q = "who left?"
                                  • fec = [the LocProp for "who"] A subsequent fragment "Bo" resolves the question by filling the FEC slot.
                                  • q : QContent

                                    The question under discussion

                                  • fec : List (LocProp Cont)

                                    Focus-establishing constituents from the utterance that introduced q

                                  Instances For
                                    source
                                    @[implicit_reducible]
                                    instance Dialogue.KOS.instReprInfoStruc {QContent✝ : Type u_1} {Cont✝ : Type} [Repr QContent✝] [Repr Cont✝] :
                                    Repr (InfoStruc QContent✝ Cont✝)
                                    Equations
                                    source
                                    def Dialogue.KOS.instReprInfoStruc.repr {QContent✝ : Type u_1} {Cont✝ : Type} [Repr QContent✝] [Repr Cont✝] :
                                    InfoStruc QContent✝ Cont✝ → ℕ → Std.Format
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      def Dialogue.KOS.instDecidableEqInfoStruc.decEq {QContent✝ : Type u_1} {Cont✝ : Type} [DecidableEq QContent✝] [DecidableEq Cont✝] (x✝ x✝¹ : InfoStruc QContent✝ Cont✝) :
                                      Decidable (x✝ = x✝¹)
                                      Equations
                                      Instances For
                                        source
                                        @[implicit_reducible]
                                        instance Dialogue.KOS.instDecidableEqInfoStruc {QContent✝ : Type u_1} {Cont✝ : Type} [DecidableEq QContent✝] [DecidableEq Cont✝] :
                                        DecidableEq (InfoStruc QContent✝ Cont✝)
                                        Equations
                                        source
                                        def Dialogue.KOS.InfoStruc.fromQuestion {QContent : Type u_1} {Cont : Type} (q : QContent) :
                                        InfoStruc QContent Cont

                                        Create an InfoStruc from a bare question (no FECs).

                                        Equations
                                        Instances For
                                          source
                                          def Dialogue.KOS.InfoStruc.withFEC {QContent : Type u_1} {Cont : Type} (q : QContent) (fec : LocProp Cont) :
                                          InfoStruc QContent Cont

                                          Create an InfoStruc from a question and a wh-word sub-utterance.

                                          Equations
                                          Instances For
                                            source
                                            structure Dialogue.KOS.DGB (Participant : Type u_1) (Fact : Type u_2) (QContent : Type u_3) (Cont : Type) :
                                            Type (max (max u_1 u_2) u_3)

                                            The Dialogue Gameboard.

                                            @cite{ginzburg-2012} ex. 100 (p. 111) and final version ex. 43 (p. 175).

                                            Each conversational participant maintains their own DGB — distinct but coupled gameboards, NOT a single shared context. The DGB tracks the public component of a participant's conversational state.

                                            The type parameters make content types explicit:

                                            • Participant: type of participant identifiers (e.g., String, Fin 2)
                                            • Fact: type of accumulated facts (e.g., Set W for typed CG access)
                                            • QContent: type of QUD questions (e.g., partition-based QUD W)
                                            • Cont: type of locutionary content (e.g., String for surface form or BCheckableAustinian S for TTR-typed propositions)

                                            This shape matches Ginzburg's Ch. 6 final DGB (ex. 43 p. 175):

                                            • pending stores LocProp (with cparams, enabling CRification on form)
                                            • qud stores InfoStruc (questions paired with FECs, enabling NSU resolution)
                                            • moves keeps IllocMove for case-analysis convenience (the book's final form uses LocProps; converting incurs no fidelity cost since IllocMove constructors carry information LocProps would have to recover)
                                            • spkr : Option Participant

                                              Current speaker (@cite{ginzburg-2012} ex. 100)

                                            • addr : Option Participant

                                              Current addressee (@cite{ginzburg-2012} ex. 100)

                                            • facts : List Fact

                                              Shared commitments. @cite{ginzburg-2012}: "Facts : Set(Prop)"

                                            • moves : List (IllocMove Fact QContent)

                                              History of illocutionary moves (Ch. 4 ex. 100; cf. Ch. 6 ex. 43 LocProp form)

                                            • pending : List (LocProp Cont)

                                              Ungrounded locutionary propositions: Ch. 6 ex. 43 (p. 175) final shape. Each LocProp carries cparams (dgb-params) that the integration protocol (integrateLocProp in KOS/Grounding.lean) checks for resolution.

                                            • qud : List (InfoStruc QContent Cont)

                                              Partially ordered set of questions under discussion. @cite{ginzburg-2012} §6.3 / §7.6 (location verified against Ch. 6/7 narrative; specific ex. number not directly cited) final shape: QUD entries are InfoStrucs (questions with focus-establishing constituents), not bare questions. We use a list (most recent = front) following QUD-maximality.

                                            Instances For
                                              source
                                              def Dialogue.KOS.DGB.latestMove {Participant : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (dgb : DGB Participant Fact QContent Cont) :
                                              Option (IllocMove Fact QContent)

                                              The latest move is the last element of the moves list.

                                              Equations
                                              Instances For
                                                source
                                                def Dialogue.KOS.DGB.initial {Participant : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} :
                                                DGB Participant Fact QContent Cont

                                                An empty DGB.

                                                Equations
                                                Instances For
                                                  source
                                                  structure Dialogue.KOS.GenreType (Fact : Type u_1) (QContent : Type u_2) :
                                                  Type (max u_1 u_2)

                                                  A conversational genre type.

                                                  @cite{ginzburg-2012} §4.6 (pp. 101–110, ex. 88 p. 104): genres are TTR record types that classify conversations by their characteristic conversational structures. Example genres from the book: CasualChat (ex. 88a), PetrolMarket (ex. 88b), BakeryChat (ex. 88c).

                                                  This schema captures the load-bearing fields from ex. 88:

                                                  • qnud (anticipated questions) — the question types that conversations of this genre are expected to raise
                                                  • anticipatedMoves — illocutionary moves the genre licenses
                                                  • qudConstraint — an optional explicit predicate on QUD content, subsuming qnud when set (used for thin worked examples)

                                                  The full TTR record per ex. 88 also includes agent fields (A, B : Ind), utt-time, facts subset, and a co-propositionality constraint (eq. 91 p. 106) between MaxQUD and what each move can add. These need additional type parameters (Participant, Fact, Cont) and richer co-propositionality machinery that we defer to consumer-driven enrichment.

                                                  The relevance check (ex. 90 p. 105) and outcome predicate live in KOS/Genre.lean.

                                                  • name : String

                                                    Genre name for identification

                                                  • qnud : List QContent

                                                    Anticipated questions in this genre (Ginzburg eq. 88 qnud field). Empty list = no anticipation (unrestricted on questions).

                                                  • anticipatedMoves : List (IllocMove Fact QContent)

                                                    Anticipated illocutionary moves the genre licenses (Ginzburg eq. 88 moves field). Used for outcome-fulfillability checks.

                                                  • qudConstraint : Option (List QContent → Bool)

                                                    Optional explicit constraint on QUD content; supersedes qnud when set. none = unrestricted (like CasualChat). The qudConstraint-based genreRelevant predicate (Ginzburg eq. 90) lives in KOS/Genre.lean.

                                                  Instances For
                                                    source
                                                    def Dialogue.KOS.GenreType.generic {Fact : Type u_1} {QContent : Type u_2} :
                                                    GenreType Fact QContent

                                                    The generic DGBType — the supertype of all genre types. @cite{ginzburg-2012} ex. 86 (p. 103): DGBTypefin GenreType.

                                                    Equations
                                                    Instances For

                                                      MaxPending = head of Pending (no separate field) #

                                                      Per @cite{ginzburg-2012} §6.3 (footnote 31 p. 168) and §8.2: MaxPending is the maximal element of the dgb.pending field, not a separately- stored struct. Pending stores LocProp Conts in last-in-first-out order; MaxPending is pending.head?. The previous formaliser struct (MaxPending with phonSoFar/cat/partialContent) bore no resemblance to Ginzburg's notion and is now deleted. The accessor lives on TIS (see KOS/SelfRepair.lean).

                                                      For incremental construction (§8.2.3 word-by-word), substrate operates on the head of Pending directly — the LocProp's phon field gets extended, no separate "phonSoFar" field needed.

                                                      source
                                                      structure Dialogue.KOS.PrivateState (Fact : Type u_1) (QContent : Type u_2) :
                                                      Type (max u_1 u_2)

                                                      The private component of an information state.

                                                      @cite{ginzburg-2012} ex. 93 (p. 107): PRType has genre, beliefs, and agenda. Agenda is a list of illocutionary propositions that the participant plans to realize. Beliefs are private (non-public) propositional attitudes.

                                                      • genre : Option (GenreType Fact QContent)

                                                        The conversational genre the participant takes the interaction to be.

                                                      • agenda : List (IllocMove Fact QContent)

                                                        The participant's agenda: planned illocutionary moves.

                                                      Instances For
                                                        source
                                                        structure Dialogue.KOS.TIS (Participant : Type u_1) (Fact : Type u_2) (QContent : Type u_3) (Cont : Type) :
                                                        Type (max (max u_1 u_2) u_3)

                                                        Total Information State (TIS).

                                                        @cite{ginzburg-2012} ex. 93 (p. 107): the TIS consists of the public DGB and a private component (genre, beliefs, agenda). The Cont parameter threads through to the DGB's pending and qud fields.

                                                        • dgb : DGB Participant Fact QContent Cont

                                                          The public dialogue gameboard

                                                        • priv : PrivateState Fact QContent

                                                          Private state: genre, agenda

                                                        Instances For
                                                          source
                                                          def Dialogue.KOS.TIS.initial {Participant : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} :
                                                          TIS Participant Fact QContent Cont

                                                          An empty TIS.

                                                          Equations
                                                          Instances For