Documentation

Linglib.Core.Discourse.DiscourseRole

Discourse Roles #

@cite{kaplan-1989} @cite{lakoff-1970} @cite{speas-tenny-2003}

Framework-agnostic discourse participant roles (speaker, addressee) and their connection to illocutionary mood. @cite{lakoff-1970} observes that tense selection depends on which participant holds epistemic authority -- declaratives attribute knowledge to the speaker, interrogatives to the addressee. This module provides the infrastructure; Tense/Perspective.lean builds Lakoff's constraints on top.

Existing framework-specific types (PRole in Minimalism/SpeechActs, Participant in Semantics.Dynamic/State) encode configurational or update-theoretic commitments. DiscourseRole is the agnostic version: just speaker vs addressee, resolved against a Kaplanian context via ContextTower (from the origin, since discourse roles reflect the actual speech-act participants).

source
inductive Core.Discourse.DiscourseRole :
Type

The two fundamental discourse participants. .addressee matches KContext.addressee (not .listener as in Semantics.Dynamic).

Instances For
    source
    instance Core.Discourse.instDecidableEqDiscourseRole :
    DecidableEq DiscourseRole
    Equations
    source
    instance Core.Discourse.instReprDiscourseRole :
    Repr DiscourseRole
    Equations
    source
    def Core.Discourse.instReprDiscourseRole.repr :
    DiscourseRole → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Core.Discourse.instBEqDiscourseRole.beq :
      DiscourseRole → DiscourseRole → Bool
      Equations
      Instances For
        source
        instance Core.Discourse.instBEqDiscourseRole :
        BEq DiscourseRole
        Equations
        source
        def Core.Discourse.instInhabitedDiscourseRole.default :
        DiscourseRole
        Equations
        Instances For
          source
          instance Core.Discourse.instInhabitedDiscourseRole :
          Inhabited DiscourseRole
          Equations
          source
          inductive Core.Discourse.IllocutionaryMood :
          Type

          Illocutionary mood -- the speech-act force of an utterance.

          Distinct from GramMood (indicative/subjunctive morphology) and the Minimalist SAPMood (configurational). This classifies the pragmatic act performed.

          Instances For
            source
            instance Core.Discourse.instDecidableEqIllocutionaryMood :
            DecidableEq IllocutionaryMood
            Equations
            source
            instance Core.Discourse.instReprIllocutionaryMood :
            Repr IllocutionaryMood
            Equations
            source
            def Core.Discourse.instReprIllocutionaryMood.repr :
            IllocutionaryMood → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance Core.Discourse.instBEqIllocutionaryMood :
              BEq IllocutionaryMood
              Equations
              source
              def Core.Discourse.instBEqIllocutionaryMood.beq :
              IllocutionaryMood → IllocutionaryMood → Bool
              Equations
              Instances For
                source
                instance Core.Discourse.instInhabitedIllocutionaryMood :
                Inhabited IllocutionaryMood
                Equations
                source
                def Core.Discourse.instInhabitedIllocutionaryMood.default :
                IllocutionaryMood
                Equations
                Instances For
                  source
                  def Core.Discourse.epistemicAuthority :
                  IllocutionaryMood → DiscourseRole

                  Which participant holds epistemic authority for a given illocutionary mood.

                  @cite{lakoff-1970}: in declaratives, imperatives, and promissives the speaker is the seat of knowledge; in interrogatives the addressee is.

                  Equations
                  Instances For
                    source
                    def Core.Discourse.resolveRole {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Context.ContextTower (Context.KContext W E P T)) :
                    DiscourseRole → E

                    Resolve a discourse role to a concrete entity via a ContextTower, reading from the origin (speech-act context). .speaker -> tower.origin.agent, .addressee -> tower.origin.addressee.

                    Equations
                    Instances For
                      source
                      theorem Core.Discourse.epistemic_authority_declarative :
                      epistemicAuthority IllocutionaryMood.declarative = DiscourseRole.speaker
                      source
                      theorem Core.Discourse.epistemic_authority_interrogative :
                      epistemicAuthority IllocutionaryMood.interrogative = DiscourseRole.addressee
                      source
                      theorem Core.Discourse.resolve_speaker_is_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Context.ContextTower (Context.KContext W E P T)) :
                      resolveRole tower DiscourseRole.speaker = tower.origin.agent
                      source
                      theorem Core.Discourse.resolve_addressee_is_addressee {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Context.ContextTower (Context.KContext W E P T)) :
                      resolveRole tower DiscourseRole.addressee = tower.origin.addressee
                      source
                      theorem Core.Discourse.resolveRole_shift_invariant {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Context.ContextTower (Context.KContext W E P T)) (σ : Context.ContextShift (Context.KContext W E P T)) (r : DiscourseRole) :
                      resolveRole (tower.push σ) r = resolveRole tower r

                      Discourse role resolution is invariant under tower push: discourse roles reflect speech-act participants (from origin), not embedded ones.