Documentation

Linglib.Discourse.Gameboard.Defs

Dialogue gameboards #

This file defines the dialogue gameboard of Ginzburg's theory of dialogue, KoS, and the records it holds. A dialogue gameboard is one participant's view of the public state of a conversation: who holds the turn and whom they address, the facts accepted so far, the moves made, the utterances not yet grounded, and the questions under discussion. An utterance is recorded as a locutionary proposition, which keeps its phonological form, category, contextual parameters and sub-utterances beside its content, so that a clarification request can target any part of its form, as Ginzburg and Cooper argue. A question under discussion carries the sub-utterances that established it, which a fragment resolving the question must match.

The types a gameboard is built from form a domain: the grammatical domain of forms, categories, parameter labels and sub-utterance denotations, extended by participants, facts, questions and utterance contents. A question may mention sub-utterances, as the question of what a speaker meant by one does, so the grammatical domain comes first.

Main definitions #

Implementation notes #

References #

source
structure Discourse.GrammaticalDomain :
Type (u + 1)

The grammatical domain of a gameboard ([Gin12] Appendix C) supplies the phonological forms, syntactic categories and contextual-parameter labels of signs, and the denotations of sub-utterances, each with decidable equality.

  • Form : Type u

    Phonological forms.

  • Category : Type u

    Syntactic categories.

  • Label : Type u

    Labels of contextual parameters.

  • Denotation : Type u

    Denotations of sub-utterances.

  • decEqForm : DecidableEq self.Form
  • decEqCategory : DecidableEq self.Category
  • decEqLabel : DecidableEq self.Label
  • decEqDenotation : DecidableEq self.Denotation
Instances For
    source
    structure Discourse.Gameboard.Domainextends Discourse.GrammaticalDomain :
    Type (u + 1)

    The domain of a gameboard extends a grammatical domain with the participants, facts, questions and utterance contents of [Gin12] Appendix A, each with decidable equality.

    Instances For
      source
      inductive Discourse.IllocutionaryAct (Fact : Type u_1) (Question : Type u_2) :
      Type (max u_1 u_2)

      An illocutionary act is the illocutionary relation of an illocutionary proposition applied to its content ([Gin12] (8c) p. 361), without the speaker and addressee that the proposition also records. The inventory is that of the rules of Ch. 4 less parting and counter-parting.

      Instances For
        source
        @[instance_reducible]
        instance Discourse.instReprIllocutionaryAct {Fact✝ : Type u_1} {Question✝ : Type u_2} [Repr Fact✝] [Repr Question✝] :
        Repr (IllocutionaryAct Fact✝ Question✝)
        Equations
        source
        def Discourse.instReprIllocutionaryAct.repr {Fact✝ : Type u_1} {Question✝ : Type u_2} [Repr Fact✝] [Repr Question✝] :
        IllocutionaryAct Fact✝ Question✝ → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[instance_reducible]
          instance Discourse.instDecidableEqIllocutionaryAct {Fact✝ : Type u_1} {Question✝ : Type u_2} [DecidableEq Fact✝] [DecidableEq Question✝] :
          DecidableEq (IllocutionaryAct Fact✝ Question✝)
          Equations
          source
          def Discourse.instDecidableEqIllocutionaryAct.decEq {Fact✝ : Type u_1} {Question✝ : Type u_2} [DecidableEq Fact✝] [DecidableEq Question✝] (x✝ x✝¹ : IllocutionaryAct Fact✝ Question✝) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            structure Discourse.SubUtterance (G : GrammaticalDomain) :
            Type u

            A sub-utterance carries a phonological form, a category and a denotation, which make any constituent of an utterance clarifiable, the fractal heterogeneity of [GC04].

            • form : G.Form

              The phonological form.

            • category : G.Category

              The syntactic category.

            • denotation : G.Denotation

              The denotation, which for a sub-utterance contributing a contextual parameter is its label.

            Instances For
              source
              def Discourse.instDecidableEqSubUtterance.decEq {G✝ : GrammaticalDomain} (x✝ x✝¹ : SubUtterance G✝) :
              Decidable (x✝ = x✝¹)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[instance_reducible]
                instance Discourse.instDecidableEqSubUtterance {G✝ : GrammaticalDomain} :
                DecidableEq (SubUtterance G✝)
                Equations
                source
                structure Discourse.LocutionaryProposition (G : GrammaticalDomain) (Content : Type u) :
                Type u

                A locutionary proposition records an utterance with its phonological form, category, content, contextual parameters and constituents ([Gin12] pp. 172–174), so that a clarification request can target the form of the utterance and any of its constituents, not only its content. The fields are the single-type notation of (42) p. 174; the Austinian proposition [sit = u, sit-type = Tᵤ] of (41) p. 173 and Appendix A (8d) p. 362 is not represented.

                • form : G.Form

                  The phonological form.

                • category : G.Category

                  The syntactic category.

                • content : Content

                  The content.

                • parameters : Finset G.Label

                  The labels of the contextual parameters, which grounding must witness; like SLASH they are pooled from the words of the utterance ([GC04] (29)). The restrictions on their values, the RESTR of (28), are not represented.

                • constituents : Finset (SubUtterance G)

                  The sub-utterances, the utterance itself among them as in (42) p. 174, listed rather than computed from the daughters by the CONSTITS Amalgamation Constraint of [GC04] (30).

                Instances For
                  source
                  @[instance_reducible]
                  instance Discourse.instDecidableEqLocutionaryProposition {G✝ : GrammaticalDomain} {Content✝ : Type u_1} [DecidableEq Content✝] :
                  DecidableEq (LocutionaryProposition G✝ Content✝)
                  Equations
                  source
                  def Discourse.instDecidableEqLocutionaryProposition.decEq {G✝ : GrammaticalDomain} {Content✝ : Type u_1} [DecidableEq Content✝] (x✝ x✝¹ : LocutionaryProposition G✝ Content✝) :
                  Decidable (x✝ = x✝¹)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    structure Discourse.InformationStructure (G : GrammaticalDomain) (Question : Type u) :
                    Type u

                    An information structure pairs a question under discussion with its focus-establishing constituents, the sub-utterances a fragment resolving the question must match in category ([Gin12] p. 239 and (9) p. 362). The focus-establishing constituent of a wh-question is its wh-phrase, and that of a clarification request the sub-utterance it clarifies; it replaces the sal-utt of [GS00]. (9) types these constituents as locutionary propositions; they are sub-utterances here because the rules that set them pick a constituent of an utterance (p. 241, and Appendix B (26e) p. 374).

                    • question : Question

                      The question.

                    • focusEstablishing : Finset (SubUtterance G)

                      The focus-establishing constituents.

                    Instances For
                      source
                      @[instance_reducible]
                      instance Discourse.instDecidableEqInformationStructure {G✝ : GrammaticalDomain} {Question✝ : Type u_1} [DecidableEq Question✝] :
                      DecidableEq (InformationStructure G✝ Question✝)
                      Equations
                      source
                      def Discourse.instDecidableEqInformationStructure.decEq {G✝ : GrammaticalDomain} {Question✝ : Type u_1} [DecidableEq Question✝] (x✝ x✝¹ : InformationStructure G✝ Question✝) :
                      Decidable (x✝ = x✝¹)
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        structure Discourse.Gameboard (D : Gameboard.Domain) :
                        Type u

                        The dialogue gameboard of a participant is their public share of the conversational state ([Gin12] (43) p. 175); each participant has their own. Its moves and pending utterances are locutionary propositions whose contents are the domain's, and its questions under discussion are information structures (p. 239). With IllocutionaryAct contents it is the gameboard of Ch. 4 ((100) p. 111), whose moves are illocutionary propositions. QUD is a partial order in (43), here a list.

                        Instances For
                          source
                          def Discourse.instDecidableEqGameboard.decEq {D✝ : Gameboard.Domain} (x✝ x✝¹ : Gameboard D✝) :
                          Decidable (x✝ = x✝¹)
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[instance_reducible]
                            instance Discourse.instDecidableEqGameboard {D✝ : Gameboard.Domain} :
                            DecidableEq (Gameboard D✝)
                            Equations