Documentation

Linglib.Discourse.Coherence

Discourse Coherence Relations #

[Hob79] [Keh02] [Umb04] Coherence relations classifying how adjacent discourse segments connect (resemblance / cause–effect / contiguity), with directionality and projections to coherence class. Kehler 2002's tripartition, extended with SDRT additions (background, consequence, alternation); CONTRAST / CORRECTION distinguished per [Umb04].

Coherence Classes ([Keh02]) #

source
inductive Discourse.Coherence.CoherenceClass :
Type

Kehler's three coherence classes, corresponding to Hume's three associative connections between ideas.

Instances For
    source
    @[implicit_reducible]
    instance Discourse.Coherence.instDecidableEqCoherenceClass :
    DecidableEq CoherenceClass
    Equations
    source
    @[implicit_reducible]
    instance Discourse.Coherence.instReprCoherenceClass :
    Repr CoherenceClass
    Equations
    source
    def Discourse.Coherence.instReprCoherenceClass.repr :
    CoherenceClass → Nat → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Coherence Relations #

      source
      inductive Discourse.Coherence.CoherenceRelation :
      Type

      Discourse coherence relations: Kehler's tripartition plus SDRT additions. CONTRAST and CORRECTION are distinguished per [Umb04] (additional vs substitutive exclusion).

      Instances For
        source
        @[implicit_reducible]
        instance Discourse.Coherence.instDecidableEqCoherenceRelation :
        DecidableEq CoherenceRelation
        Equations
        source
        def Discourse.Coherence.instReprCoherenceRelation.repr :
        CoherenceRelation → Nat → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance Discourse.Coherence.instReprCoherenceRelation :
          Repr CoherenceRelation
          Equations

          Properties #

          source
          def Discourse.Coherence.CoherenceRelation.toClass :
          CoherenceRelation → CoherenceClass

          Classify each relation into its coherence class.

          Equations
          Instances For
            source
            inductive Discourse.Coherence.CausalDirection :
            Type

            Causal direction: does the relation seek a cause in the prior segment?

            Instances For
              source
              @[implicit_reducible]
              instance Discourse.Coherence.instDecidableEqCausalDirection :
              DecidableEq CausalDirection
              Equations
              source
              @[implicit_reducible]
              instance Discourse.Coherence.instReprCausalDirection :
              Repr CausalDirection
              Equations
              source
              def Discourse.Coherence.instReprCausalDirection.repr :
              CausalDirection → Nat → Std.Format
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Discourse.Coherence.CoherenceRelation.causalDirection :
                CoherenceRelation → CausalDirection

                The causal direction of each relation.

                Equations
                Instances For
                  source
                  def Discourse.Coherence.CoherenceRelation.selectsCause (r : CoherenceRelation) :
                  Prop

                  Does this relation trigger a search for a cause?

                  Equations
                  Instances For
                    source
                    @[implicit_reducible]
                    instance Discourse.Coherence.instDecidableSelectsCause (r : CoherenceRelation) :
                    Decidable r.selectsCause
                    Equations
                    source
                    def Discourse.Coherence.CoherenceRelation.selectsEffect (r : CoherenceRelation) :
                    Prop

                    Does this relation trigger a search for an effect?

                    Equations
                    Instances For
                      source
                      @[implicit_reducible]
                      instance Discourse.Coherence.instDecidableSelectsEffect (r : CoherenceRelation) :
                      Decidable r.selectsEffect
                      Equations

                      Enumeration #

                      source
                      def Discourse.Coherence.CoherenceRelation.all :
                      List CoherenceRelation

                      Every coherence relation, for marginalizing over the full set (e.g. the next-mention mixture Σ_CR P(CR) · f(CR)).

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem Discourse.Coherence.CoherenceRelation.mem_all (r : CoherenceRelation) :
                        r ∈ all

                        all is exhaustive. Adding a constructor breaks this proof, forcing every marginalization over all to be revisited rather than silently dropping a relation.

                        Connective–Relation Mapping #

                        source
                        inductive Discourse.Coherence.Connective :
                        Type

                        German/English connective forms used as experimental stimuli ([SB22], Exps 1–4).

                        Instances For
                          source
                          @[implicit_reducible]
                          instance Discourse.Coherence.instDecidableEqConnective :
                          DecidableEq Connective
                          Equations
                          source
                          def Discourse.Coherence.instReprConnective.repr :
                          Connective → Nat → Std.Format
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[implicit_reducible]
                            instance Discourse.Coherence.instReprConnective :
                            Repr Connective
                            Equations
                            source
                            def Discourse.Coherence.Connective.toRelation :
                            Connective → CoherenceRelation

                            Map connectives to the coherence relation they signal.

                            Equations
                            Instances For

                              Theorems #

                              source
                              theorem Discourse.Coherence.because_selects_cause :
                              Connective.because.toRelation.selectsCause

                              "because" selects for causes (backward causal).

                              source
                              theorem Discourse.Coherence.andSo_selects_effect :
                              Connective.andSo.toRelation.selectsEffect

                              "and so" selects for effects (forward causal / I-Cons).

                              source
                              theorem Discourse.Coherence.although_not_causal :
                              ¬Connective.although.toRelation.selectsCause

                              "although" does not select for causes.

                              source
                              theorem Discourse.Coherence.andThen_not_causal :
                              ¬Connective.andThen.toRelation.selectsCause

                              "and then" does not select for causes.

                              source
                              theorem Discourse.Coherence.because_andSo_opposite_directions :
                              Connective.because.toRelation.causalDirection = CausalDirection.backward ∧ Connective.andSo.toRelation.causalDirection = CausalDirection.forward

                              "because" and "and so" are both causal but in opposite directions: I-Caus is backward, I-Cons is forward.

                              source
                              theorem Discourse.Coherence.causal_relations_same_class :
                              CoherenceRelation.explanation.toClass = CoherenceRelation.result.toClass

                              Both causal relations (explanation, result) belong to causeEffect class.

                              source
                              theorem Discourse.Coherence.contiguity_relations_same_class :
                              CoherenceRelation.occasion.toClass = CoherenceRelation.elaboration.toClass

                              Occasion and elaboration belong to contiguity class.

                              source
                              theorem Discourse.Coherence.contrast_correction_same_class :
                              CoherenceRelation.contrast.toClass = CoherenceRelation.correction.toClass

                              CONTRAST and CORRECTION are both resemblance relations ([Umb04], [Keh02]).

                              source
                              theorem Discourse.Coherence.contrast_ne_correction :
                              CoherenceRelation.contrast ≠ CoherenceRelation.correction

                              CONTRAST and CORRECTION are distinct despite sharing a class ([Umb04]).