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 Discourse/SpeechAct.lean to break a would-be cycle between Semantics/Mood/IllocutionaryMood.lean (which needs DiscourseRole for moodAuthority) and the act-side material in SpeechAct.lean (which extends IllocutionaryMood with Searle classes and direction of fit).

inductive Discourse.DiscourseRole : Type

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

• speaker : DiscourseRole
• addressee : DiscourseRole

@[implicit_reducible]

instance Discourse.instDecidableEqDiscourseRole : DecidableEq DiscourseRole

Equations

• Discourse.instDecidableEqDiscourseRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Discourse.instReprDiscourseRole.repr : DiscourseRole → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Discourse.instReprDiscourseRole : Repr DiscourseRole

Equations

• Discourse.instReprDiscourseRole = { reprPrec := Discourse.instReprDiscourseRole.repr }

@[implicit_reducible]

instance Discourse.instInhabitedDiscourseRole : Inhabited DiscourseRole

Equations

• Discourse.instInhabitedDiscourseRole = { default := Discourse.instInhabitedDiscourseRole.default }

def Discourse.resolveRole {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Semantics.Context.ContextTower (Semantics.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

• Discourse.resolveRole tower Discourse.DiscourseRole.speaker = tower.origin.agent
• Discourse.resolveRole tower Discourse.DiscourseRole.addressee = tower.origin.addressee

theorem Discourse.resolve_speaker_is_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) : resolveRole tower DiscourseRole.speaker = tower.origin.agent

theorem Discourse.resolve_addressee_is_addressee {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) : resolveRole tower DiscourseRole.addressee = tower.origin.addressee

theorem Discourse.resolveRole_shift_invariant {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (σ : Semantics.Context.ContextShift (Semantics.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.