Documentation

Linglib.Theories.Dialogue.KOS.Move

IllocMove ↔ Searle Bridge #

@cite{ginzburg-2012} @cite{searle-1979}

Maps KOS's IllocMove constructors to @cite{searle-1979}'s five-class illocutionary taxonomy and to direction-of-fit. Surfaces as:

These are pure projections from move constructors to substrate-shared illocutionary primitives — they do not depend on the dialogue gameboard machinery.

source
def Dialogue.KOS.IllocMove.toSearleClass {Fact : Type u_1} {QContent : Type u_2} :
IllocMove Fact QContent → Core.Discourse.SearleClass

Map an illocutionary move to @cite{searle-1979}'s five-class taxonomy.

Assert/accept/confirm are assertives (mind-to-world fit). Ask is a directive (world-to-mind: the speaker tries to get the addressee to provide information). Check is a directive (requesting confirmation). Greet/counterGreet are expressives (null fit).

Equations
Instances For
    source
    def Dialogue.KOS.IllocMove.directionOfFit {Fact : Type u_1} {QContent : Type u_2} (m : IllocMove Fact QContent) :
    Core.Discourse.DirectionOfFit

    Direction of fit for an illocutionary move, derived via Searle class.

    Equations
    Instances For
      source
      theorem Dialogue.KOS.IllocMove.assert_mind_to_world {Fact : Type u_1} {QContent : Type u_2} (p : Fact) :
      (assert p).directionOfFit = Core.Discourse.DirectionOfFit.mindToWorld

      Assertions have mind-to-world fit: the speaker is responsible if p is false.

      source
      theorem Dialogue.KOS.IllocMove.ask_world_to_mind {Fact : Type u_1} {QContent : Type u_2} (q : QContent) :
      (ask q).directionOfFit = Core.Discourse.DirectionOfFit.worldToMind

      Queries have world-to-mind fit: the speaker wants the addressee to act.

      source
      theorem Dialogue.KOS.IllocMove.greet_null_fit {Fact : Type u_1} {QContent : Type u_2} :
      greet.directionOfFit = Core.Discourse.DirectionOfFit.null

      Greetings have null fit: they express social acknowledgement.

      source
      theorem Dialogue.KOS.assertive_moves_mind_to_world {Fact : Type u_1} {QContent : Type u_2} (p : Fact) :
      (IllocMove.assert p).directionOfFit = Core.Discourse.DirectionOfFit.mindToWorld ∧ (IllocMove.accept p).directionOfFit = Core.Discourse.DirectionOfFit.mindToWorld ∧ (IllocMove.confirm p).directionOfFit = Core.Discourse.DirectionOfFit.mindToWorld

      All assertive-class moves (assert, accept, confirm) share mind-to-world fit: the speaker takes responsibility for truth.

      source
      theorem Dialogue.KOS.directive_moves_world_to_mind {Fact : Type u_1} {QContent : Type u_2} (q : QContent) (p : Fact) :
      (IllocMove.ask q).directionOfFit = Core.Discourse.DirectionOfFit.worldToMind ∧ (IllocMove.check p).directionOfFit = Core.Discourse.DirectionOfFit.worldToMind

      Directive moves (ask, check) share world-to-mind fit: the speaker wants the addressee to act.