Documentation

Linglib.Core.Discourse.Roles

Discourse Roles #

The two fundamental discourse participants — speaker and addressee — and the function that resolves them through a ContextTower to concrete entities.

This file exists separately from Core/Discourse/IllocutionaryForce.lean to break a would-be cycle between Core/Mood/IllocutionaryMood.lean (which needs DiscourseRole for moodAuthority) and the act-side material in IllocutionaryForce.lean (which extends IllocutionaryMood with Searle classes and direction of fit).

source
inductive Core.Discourse.DiscourseRole :
Type

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

Instances For
    source
    @[implicit_reducible]
    instance Core.Discourse.instDecidableEqDiscourseRole :
    DecidableEq 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
      @[implicit_reducible]
      instance Core.Discourse.instReprDiscourseRole :
      Repr DiscourseRole
      Equations
      source
      @[implicit_reducible]
      instance Core.Discourse.instInhabitedDiscourseRole :
      Inhabited DiscourseRole
      Equations
      source
      def Core.Discourse.instInhabitedDiscourseRole.default :
      DiscourseRole
      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.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.