Documentation

Linglib.Discourse.Gameboard.Defs

KOS: Type Definitions #

[Gin12]

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

TTR-residence #

KOS is built on TTR ([Coo23]). 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 Coe 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 (Cooper's "type-is-a-type" semantics requires Type 0 for the carrier). Same pinning applies in Gameboard/Austinian.lean (where BCheckableAustinian and TTRQuestionB similarly require 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
structure Discourse.Gameboard.TTRSign (Phon Cont : Type) :
Type

A sign: phonology paired with content ([Coo23] §2.5 ex 70). LocProp below is its structural refinement; the forgetful projection LocProp.toTTRSign and Coe instance discharge the TTR-residence commitment.

  • phon : Phon
  • cont : Cont
Instances For
    source
    @[instance_reducible]
    instance Discourse.Gameboard.instReprTTRSign {Phon✝ Cont✝ : Type} [Repr Phon✝] [Repr Cont✝] :
    Repr (TTRSign Phon✝ Cont✝)
    Equations
    source
    def Discourse.Gameboard.instReprTTRSign.repr {Phon✝ Cont✝ : Type} [Repr Phon✝] [Repr Cont✝] :
    TTRSign Phon✝ Cont✝ → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Discourse.Gameboard.instDecidableEqTTRSign {Phon✝ Cont✝ : Type} [DecidableEq Phon✝] [DecidableEq Cont✝] :
      DecidableEq (TTRSign Phon✝ Cont✝)
      Equations
      source
      def Discourse.Gameboard.instDecidableEqTTRSign.decEq {Phon✝ Cont✝ : Type} [DecidableEq Phon✝] [DecidableEq Cont✝] (x✝ x✝¹ : TTRSign Phon✝ Cont✝) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        inductive Discourse.Gameboard.IllocMove (Fact : Type u_1) (QContent : Type u_2) :
        Type (max u_1 u_2)

        An illocutionary move in dialogue.

        [Gin12] 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 Discourse.Gameboard.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
            @[instance_reducible]
            instance Discourse.Gameboard.instReprIllocMove {Fact✝ : Type u_1} {QContent✝ : Type u_2} [Repr Fact✝] [Repr QContent✝] :
            Repr (IllocMove Fact✝ QContent✝)
            Equations
            source
            def Discourse.Gameboard.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
              @[instance_reducible]
              instance Discourse.Gameboard.instDecidableEqIllocMove {Fact✝ : Type u_1} {QContent✝ : Type u_2} [DecidableEq Fact✝] [DecidableEq QContent✝] :
              DecidableEq (IllocMove Fact✝ QContent✝)
              Equations
              source
              def Discourse.Gameboard.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 Discourse.Gameboard.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)"). [GC04] ex. 28; surviving in [Gin12] 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 Discourse.Gameboard.instReprCParam.repr :
                  CParam → ℕ → Std.Format
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[instance_reducible]
                    instance Discourse.Gameboard.instReprCParam :
                    Repr CParam
                    Equations
                    source
                    @[instance_reducible]
                    instance Discourse.Gameboard.instDecidableEqCParam :
                    DecidableEq CParam
                    Equations
                    source
                    def Discourse.Gameboard.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 Discourse.Gameboard.CParamSet :
                      Type

                      A set of contextual parameters, analogous to the RSRL GAP set (Syntax/HPSG/Construction).

                      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 Discourse.Gameboard.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. [GC04] §2; surviving in [Gin12] Ch. 6 as the constits field on LocProps.

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

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

                              [Gin12] 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 [Gin12]'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 ([PG04], [Gin12] §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 ([Gin12] §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. [Gin12] Ch. 6: any sub-utterance can be targeted by a CR.

                              Instances For
                                source
                                def Discourse.Gameboard.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
                                  @[instance_reducible]
                                  instance Discourse.Gameboard.instReprLocProp {Cont✝ : Type} [Repr Cont✝] :
                                  Repr (LocProp Cont✝)
                                  Equations
                                  source
                                  def Discourse.Gameboard.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
                                    @[instance_reducible]
                                    instance Discourse.Gameboard.instDecidableEqLocProp {Cont✝ : Type} [DecidableEq Cont✝] :
                                    DecidableEq (LocProp Cont✝)
                                    Equations
                                    source
                                    def Discourse.Gameboard.LocProp.toTTRSign {Cont : Type} (lp : LocProp Cont) :
                                    TTRSign String Cont

                                    Forgetful projection LocProp Cont → TTRSign String Cont: keep phon

                                    • cont, drop dialogue-grade fields.
                                    Equations
                                    Instances For
                                      source
                                      @[instance_reducible]
                                      instance Discourse.Gameboard.instCoeLocPropTTRSignString {Cont : Type} :
                                      Coe (LocProp Cont) (TTRSign String Cont)

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

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

                                      The projection preserves phon.

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

                                      The projection preserves cont.

                                      source
                                      structure Discourse.Gameboard.InfoStruc (QContent : Type u_1) (Cont : Type) :
                                      Type u_1

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

                                      [Gin12] Ch. 7 (p. 239): 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
                                        @[instance_reducible]
                                        instance Discourse.Gameboard.instReprInfoStruc {QContent✝ : Type u_1} {Cont✝ : Type} [Repr QContent✝] [Repr Cont✝] :
                                        Repr (InfoStruc QContent✝ Cont✝)
                                        Equations
                                        source
                                        def Discourse.Gameboard.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
                                          @[instance_reducible]
                                          instance Discourse.Gameboard.instDecidableEqInfoStruc {QContent✝ : Type u_1} {Cont✝ : Type} [DecidableEq QContent✝] [DecidableEq Cont✝] :
                                          DecidableEq (InfoStruc QContent✝ Cont✝)
                                          Equations
                                          source
                                          def Discourse.Gameboard.instDecidableEqInfoStruc.decEq {QContent✝ : Type u_1} {Cont✝ : Type} [DecidableEq QContent✝] [DecidableEq Cont✝] (x✝ x✝¹ : InfoStruc QContent✝ Cont✝) :
                                          Decidable (x✝ = x✝¹)
                                          Equations
                                          Instances For
                                            source
                                            def Discourse.Gameboard.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
                                              structure Discourse.Gameboard.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.

                                              [Gin12] 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 CommonGround 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), where pending/moves store LocProps and qud is a poset of questions:

                                              • pending stores LocProp (with cparams, enabling CRification on form)
                                              • qud stores InfoStruc (questions paired with FECs) — the InfoStruc-as-QUD refinement is the Ch. 7 development (p. 239), not ex. 43 itself
                                              • 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 ([Gin12] ex. 100)

                                              • addr : Option Participant

                                                Current addressee ([Gin12] ex. 100)

                                              • facts : List Fact

                                                Shared commitments. [Gin12]: "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 Gameboard/Grounding.lean) checks for resolution.

                                              • qud : List (InfoStruc QContent Cont)

                                                Partially ordered set of questions under discussion. [Gin12] §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 Discourse.Gameboard.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 Discourse.Gameboard.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 Discourse.Gameboard.GenreType (Fact : Type u_1) (QContent : Type u_2) :
                                                    Type (max u_1 u_2)

                                                    A conversational genre type.

                                                    [Gin12] §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 Gameboard/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 Gameboard/Genre.lean.

                                                    Instances For

                                                      MaxPending = head of Pending (no separate field) #

                                                      Per [Gin12] §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 Gameboard/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 Discourse.Gameboard.PrivateState (Fact : Type u_1) (QContent : Type u_2) :
                                                      Type (max u_1 u_2)

                                                      The private component of an information state.

                                                      [Gin12] 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 Discourse.Gameboard.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).

                                                        [Gin12] 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 Discourse.Gameboard.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