Documentation

Linglib.Discourse.Response

Responses and their polarity features #

A responding move reacts to a sentence on the Table, put there by an assertion or a polar question. [FB10] classify it by two polarity features: its relative polarity, [same] when it confirms that sentence and [reverse] when it reverses it, and its absolute polarity, [+] or [−], the polarity of the sentence it asserts. A Discourse.Response records what fixes both: the move it reacts to, the polarity of the sentence on the Table, and its own polarity. Its relative polarity is the quotient of the two polarities in the group of polarities (Response.relative), positive for [same] and negative for [reverse].

A polarity particle is used in some responses and not others, so what a theory says about a particle is a set of responses. Each framework interpreting the particles of a language assigns them such sets, which form a Boolean algebra: rival interpretations of one particle are compared by inclusion, and an interpretation is tested against the acceptable responses of the data. Properties of a particle are properties of its set: the typology of answering negative questions asks which particle confirms the negative alternative (Response.ConfirmsNegativeQuestion).

Main definitions #

References #

source
inductive Discourse.InitiatingMove :
Type

A move that puts a sentence on the Table for a response to react to.

  • assertion : InitiatingMove

    An assertion: a [reverse] response to it is a denial.

  • polarQuestion : InitiatingMove

    A polar question: a [reverse] response to it is a reverse answer.

Instances For
    source
    @[instance_reducible]
    instance Discourse.instDecidableEqInitiatingMove :
    DecidableEq InitiatingMove
    Equations
    source
    @[instance_reducible]
    instance Discourse.instReprInitiatingMove :
    Repr InitiatingMove
    Equations
    source
    def Discourse.instReprInitiatingMove.repr :
    InitiatingMove → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Discourse.instFintypeInitiatingMove :
      Fintype InitiatingMove
      Equations
      • One or more equations did not get rendered due to their size.
      source
      structure Discourse.Response :
      Type

      A responding move: the move it reacts to, the polarity of the sentence radical on the Table, and the polarity of the sentence it asserts.

      • reactsTo : InitiatingMove

        The move responded to.

      • antecedent : Polarity

        The polarity of the sentence on the Table.

      • polarity : Polarity

        The polarity of the response, its absolute polarity.

      Instances For
        source
        def Discourse.instDecidableEqResponse.decEq (x✝ x✝¹ : Response) :
        Decidable (x✝ = x✝¹)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[instance_reducible]
          instance Discourse.instDecidableEqResponse :
          DecidableEq Response
          Equations
          source
          @[instance_reducible]
          instance Discourse.instReprResponse :
          Repr Response
          Equations
          source
          def Discourse.instReprResponse.repr :
          Response → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[instance_reducible]
            instance Discourse.instFintypeResponse :
            Fintype Response
            Equations
            source
            def Discourse.Response.relative (x : Response) :
            Polarity

            The relative polarity of a response: positive, [same], when it shares the polarity of the sentence on the Table, negative, [reverse], when it reverses it.

            Equations
            Instances For
              source
              @[simp]
              theorem Discourse.Response.relative_mk (m : InitiatingMove) (a p : Polarity) :
              { reactsTo := m, antecedent := a, polarity := p }.relative = p / a
              source
              theorem Discourse.Response.relative_eq_positive_iff {x : Response} :
              x.relative = Polarity.positive ↔ x.polarity = x.antecedent

              A response is [same] iff it shares the polarity of the sentence on the Table.

              source
              def Discourse.Response.ConfirmsNegativeQuestion (S : Set Response) :
              Prop

              The responses S include the answer confirming the negative alternative of a negative polar question, [same, −]. Which particle of a language does so tells its system of answering negative questions: the affirmative one in a system of relative polarity particles, agree/disagree or truth-based; the negative one in a system of absolute polarity particles, yes/no or polarity-based ([FB10], [SZ85], [Hol16]).

              Equations
              Instances For
                source
                @[instance_reducible]
                instance Discourse.Response.instDecidableConfirmsNegativeQuestionOfMemSet (S : Set Response) [h : Decidable ({ reactsTo := InitiatingMove.polarQuestion, antecedent := Polarity.negative, polarity := Polarity.negative } ∈ S)] :
                Decidable (ConfirmsNegativeQuestion S)
                Equations