Documentation

Linglib.Core.Context.Shifts

Standard Context Shifts #

Shift constructors for KContext that correspond to specific linguistic operations: attitude embedding, temporal shift, full perspective shift, and the identity (no-op) shift. Each preserves or changes specific coordinates, with theorems documenting the preservation pattern.

These are the building blocks for tower-based composition. An attitude verb pushes attitudeShift, a sequence-of-tense embedding pushes temporalShift, FID pushes perspectiveShift, and Kaplan-compliant English attitude verbs push identityShift.

source
def Core.Context.attitudeShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (holder : E) (attWorld : W) :
ContextShift (KContext W E P T)

Attitude shift: changes agent (to the attitude holder) and world (to an attitude-accessible world). Addressee, time, and position are preserved.

@cite{schlenker-2003}: "John said that I am happy" — under the monster analysis, the attitude verb shifts agent to John. Under Kaplan's thesis, English uses identityShift instead.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Core.Context.temporalShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newTime : T) :
    ContextShift (KContext W E P T)

    Temporal shift: changes time only. Used for sequence of tense, where embedded tense is evaluated relative to the matrix event time.

    @cite{von-stechow-2009}: the attitude verb transmits its event time to the embedded clause's perspective time.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Core.Context.perspectiveShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newAgent : E) (newTime : T) (newWorld : W) :
      ContextShift (KContext W E P T)

      Perspective shift: changes agent, time, and world simultaneously. This is the shift for Free Indirect Discourse (FID), where the narrative adopts the character's perspective across all coordinates.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Core.Context.identityShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} :
        ContextShift (KContext W E P T)

        Identity shift: no change to the context. Kaplan's thesis for English says attitude verbs push identity shifts — embedding happens without shifting the context of utterance.

        Equations
        Instances For
          source
          @[simp]
          theorem Core.Context.attitudeShift_preserves_addressee {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (holder : E) (attWorld : W) (c : KContext W E P T) :
          ((attitudeShift holder attWorld).apply c).addressee = c.addressee
          source
          @[simp]
          theorem Core.Context.attitudeShift_preserves_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (holder : E) (attWorld : W) (c : KContext W E P T) :
          ((attitudeShift holder attWorld).apply c).time = c.time
          source
          @[simp]
          theorem Core.Context.attitudeShift_preserves_position {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (holder : E) (attWorld : W) (c : KContext W E P T) :
          ((attitudeShift holder attWorld).apply c).position = c.position
          source
          @[simp]
          theorem Core.Context.attitudeShift_changes_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (holder : E) (attWorld : W) (c : KContext W E P T) :
          ((attitudeShift holder attWorld).apply c).agent = holder
          source
          @[simp]
          theorem Core.Context.attitudeShift_changes_world {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (holder : E) (attWorld : W) (c : KContext W E P T) :
          ((attitudeShift holder attWorld).apply c).world = attWorld
          source
          @[simp]
          theorem Core.Context.temporalShift_preserves_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newTime : T) (c : KContext W E P T) :
          ((temporalShift newTime).apply c).agent = c.agent
          source
          @[simp]
          theorem Core.Context.temporalShift_preserves_world {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newTime : T) (c : KContext W E P T) :
          ((temporalShift newTime).apply c).world = c.world
          source
          @[simp]
          theorem Core.Context.temporalShift_preserves_addressee {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newTime : T) (c : KContext W E P T) :
          ((temporalShift newTime).apply c).addressee = c.addressee
          source
          @[simp]
          theorem Core.Context.temporalShift_preserves_position {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newTime : T) (c : KContext W E P T) :
          ((temporalShift newTime).apply c).position = c.position
          source
          @[simp]
          theorem Core.Context.temporalShift_changes_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newTime : T) (c : KContext W E P T) :
          ((temporalShift newTime).apply c).time = newTime
          source
          @[simp]
          theorem Core.Context.identityShift_apply {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) :
          identityShift.apply c = c
          source
          theorem Core.Context.push_identityShift_innermost {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : ContextTower (KContext W E P T)) :
          (t.push identityShift).innermost = t.innermost

          Pushing an identity shift doesn't change the innermost context.

          source
          @[simp]
          theorem Core.Context.perspectiveShift_changes_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (a : E) (t : T) (w : W) (c : KContext W E P T) :
          ((perspectiveShift a t w).apply c).agent = a
          source
          @[simp]
          theorem Core.Context.perspectiveShift_changes_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (a : E) (t : T) (w : W) (c : KContext W E P T) :
          ((perspectiveShift a t w).apply c).time = t
          source
          @[simp]
          theorem Core.Context.perspectiveShift_changes_world {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (a : E) (t : T) (w : W) (c : KContext W E P T) :
          ((perspectiveShift a t w).apply c).world = w
          source
          @[simp]
          theorem Core.Context.perspectiveShift_preserves_addressee {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (a : E) (t : T) (w : W) (c : KContext W E P T) :
          ((perspectiveShift a t w).apply c).addressee = c.addressee
          source
          @[simp]
          theorem Core.Context.perspectiveShift_preserves_position {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (a : E) (t : T) (w : W) (c : KContext W E P T) :
          ((perspectiveShift a t w).apply c).position = c.position