Documentation

Linglib.Discourse.Coherence

Coherence relations #

This file defines the coherence relations of [Keh02], the ways two adjacent discourse segments are understood to connect, and their classification into the three kinds of connection between ideas Hume distinguished: resemblance, cause–effect, and contiguity. The classes differ in the inference that establishes the relation. A resemblance relation aligns the predicates and arguments of the two segments and compares them; a cause–effect relation infers a proposition from each segment and connects the two by an implication; a contiguity relation reads the second segment's eventuality as continuing from the end state of the first. A cause–effect relation is oriented by which segment supplies the cause, and the orientation is defined on exactly that class (Relation.causalDirection_isSome_iff), so Explanation is Result with the segments exchanged, and Denial of Preventer is Violated Expectation with the segments exchanged.

Main definitions #

References #

source
inductive Discourse.Coherence.Class :
Type

The three kinds of connection between ideas, which classify coherence relations by the inference that establishes them.

  • resemblance : Class

    The predicates and arguments of the segments are aligned and compared.

  • causeEffect : Class

    A proposition inferred from each segment, the two connected by an implication.

  • contiguity : Class

    The second segment's eventuality continues from the end state of the first.

Instances For
    source
    @[instance_reducible]
    instance Discourse.Coherence.instDecidableEqClass :
    DecidableEq Class
    Equations
    source
    def Discourse.Coherence.instReprClass.repr :
    Class → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Discourse.Coherence.instReprClass :
      Repr Class
      Equations
      source
      @[instance_reducible]
      instance Discourse.Coherence.instFintypeClass :
      Fintype Class
      Equations
      • One or more equations did not get rendered due to their size.
      source
      inductive Discourse.Coherence.Relation :
      Type

      The coherence relations of [Keh02], each holding between a first segment and the second that continues it.

      • parallel : Relation

        A common predicate over pairwise similar arguments.

      • contrast : Relation

        A common predicate over pairwise similar arguments, one negated or the arguments contrasted.

      • exemplification : Relation

        A generalization, then an instance of it.

      • generalization : Relation

        An instance, then the generalization it instantiates.

      • exception : Relation

        A generalization and an instance that runs against it, in either order.

      • elaboration : Relation

        A second description of the first segment's eventuality.

      • result : Relation

        The first segment's proposition brings about the second's (and so).

      • explanation : Relation

        The second segment's proposition brings about the first's (because).

      • violatedExpectation : Relation

        The first segment's proposition would normally rule out the second's (but).

      • denialOfPreventer : Relation

        The second segment's proposition would normally rule out the first's (even though).

      • occasion : Relation

        The second segment's eventuality follows on the end state of the first's.

      Instances For
        source
        @[instance_reducible]
        instance Discourse.Coherence.instDecidableEqRelation :
        DecidableEq Relation
        Equations
        source
        def Discourse.Coherence.instReprRelation.repr :
        Relation → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[instance_reducible]
          instance Discourse.Coherence.instReprRelation :
          Repr Relation
          Equations
          source
          @[instance_reducible]
          instance Discourse.Coherence.instFintypeRelation :
          Fintype Relation
          Equations
          • One or more equations did not get rendered due to their size.
          source
          inductive Discourse.Coherence.Direction :
          Type

          Which segment a cause–effect relation takes as the cause: the first, so that the cause precedes its effect, or the second, so that the effect precedes its cause.

          Instances For
            source
            @[instance_reducible]
            instance Discourse.Coherence.instDecidableEqDirection :
            DecidableEq Direction
            Equations
            source
            @[instance_reducible]
            instance Discourse.Coherence.instReprDirection :
            Repr Direction
            Equations
            source
            def Discourse.Coherence.instReprDirection.repr :
            Direction → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance Discourse.Coherence.instFintypeDirection :
              Fintype Direction
              Equations
              • One or more equations did not get rendered due to their size.
              source
              def Discourse.Coherence.Relation.toClass :
              Relation → Class

              The class of a relation.

              Equations
              Instances For
                source
                def Discourse.Coherence.Relation.causalDirection :
                Relation → Option Direction

                The direction of a cause–effect relation: Result and Violated Expectation take the first segment as the cause, Explanation and Denial of Preventer the second.

                Equations
                Instances For
                  source
                  theorem Discourse.Coherence.Relation.causalDirection_isSome_iff (r : Relation) :
                  r.causalDirection.isSome = true ↔ r.toClass = Class.causeEffect

                  A relation has a direction exactly when it is a cause–effect relation.