Schlenker, Lamberton & Lamberton (2026): Traveling Shots in Language

This file formalizes the paper's extension of Iconological Semantics to dynamic viewpoints. In [SL24] a classifier predicate has an iconic component evaluated by projecting its argument onto signing space from the viewpoint a variable denotes, and a dynamic classifier, one that moves in signing space, is projected moment by moment along its movement (the paper's (27)). The paper's problem is relative motion: in ASL a classifier for a static object, a tree or a pole, can move past the signer to show the object passing a moving character, the traveling shot of film. With projection from static viewpoints a still object projects to a still classifier, so such readings are unavailable (DynProj.eq_of_isStatic); once a viewpoint is a function from times and worlds to static viewpoints (29), the movement of the classifier is information about the movement of the viewpoint (DynProj.viewpoint_ne), the character's path in the elicited paradigms of Data/Examples/SchlenkerEtAl2026.

The paper leaves two analyses open. On Analysis I any viewpoint variable may denote a dynamic viewpoint. On Analysis II only the context-bound variable π*, which denotes the dynamic viewpoint of the context's agent (33), may, and Role Shift, analyzed as overt context shift (34), abstracts over the agent, time and world of the context (roleShift), so that a role-shifted classifier is projected from the character's moving viewpoint (roleShift_classifierIcon_iff). Under the restrictive theory that free variables are static, a traveling shot therefore needs Role Shift (Restrictive.eq_of_free), and under Role Shift the classifier's movement is the character's (roleShift_viewpoint_ne). How dynamic viewpoints enter [Dav15]'s demonstrational analysis of Role Shift, which has no viewpoints, is left open by the paper.

Implementation notes

• A viewpoint is any type: the paper's viewpoints carry a Cartesian frame of reference and scaling factors, and projection is any function from an object, a static viewpoint, a time and a world to a position in signing space, so the geometry of projection is not modeled. The scaling of classifier time to evaluation time in (27) is an arbitrary clock from the moments of the movement to times, started at the time of evaluation. An object is still when its projection from any fixed viewpoint does not change over time.
• Role Shift (34) is composed from the substrate's attitude and temporal shifts of the context, which the paper's context triple identifies with the agent, world and time coordinates.
• The elicited paradigms are recorded as rows with the mean judgment on the seven-point scale; the paper's inferences about the character's path from the side on which the classifier passes are not modeled, since they require the geometry.

References

• [SLL26]
• [SL24]
• [Dav15]

Projection from dynamic viewpoints (§7)

def SchlenkerEtAl2026.IsStatic {W : Type u_1} {T : Type u_4} {V : Type u_5} (vp : T → W → V) : Prop

(29): a dynamic viewpoint is a function from times and worlds to the static viewpoints of [SL24]; the standard viewpoints are the constant ones.

Equations

• SchlenkerEtAl2026.IsStatic vp = ∃ (v : V), vp = fun (x : T) (x_1 : W) => v

def SchlenkerEtAl2026.projAt {W : Type u_1} {E : Type u_2} {T : Type u_4} {V : Type u_5} {S : Type u_6} (proj : E → V → T → W → S) (d : E) (vp : T → W → V) (t : T) (w : W) : S

(29): projection from a viewpoint that may move. proj d v t w is the position in signing space to which the object d projects from the static viewpoint v at t in w; from a dynamic viewpoint, d projects at t in w from the viewpoint's value there.

Equations

• SchlenkerEtAl2026.projAt proj d vp t w = proj d (vp t w) t w

def SchlenkerEtAl2026.DynProj {W : Type u_1} {E : Type u_2} {T : Type u_4} {V : Type u_5} {S : Type u_6} {ι : Type u_7} (proj : E → V → T → W → S) (d : E) (vp : T → W → V) (w : W) (clock : ι → T) (cl : ι → S) : Prop

(27), (32): an object projects to a dynamic classifier, a function cl from the moments of its movement to positions in signing space, when at each moment, sent to a time of evaluation by the classifier's clock, the object projects to the classifier's position there.

Equations

• SchlenkerEtAl2026.DynProj proj d vp w clock cl = ∀ (i : ι), SchlenkerEtAl2026.projAt proj d vp (clock i) w = cl i

def SchlenkerEtAl2026.IsStill {W : Type u_1} {E : Type u_2} {T : Type u_4} {V : Type u_5} {S : Type u_6} (proj : E → V → T → W → S) (d : E) (w : W) : Prop

An object is still in w when its projection from any fixed viewpoint does not change over time.

Equations

• SchlenkerEtAl2026.IsStill proj d w = ∀ (v : V) (t t' : T), proj d v t w = proj d v t' w

theorem SchlenkerEtAl2026.DynProj.eq_of_isStill {W : Type u_1} {E : Type u_2} {T : Type u_4} {V : Type u_5} {S : Type u_6} {ι : Type u_7} {proj : E → V → T → W → S} {d : E} {w : W} {clock : ι → T} {cl : ι → S} {vp : T → W → V} (h : DynProj proj d vp w clock cl) (hd : IsStill proj d w) {i j : ι} (hv : vp (clock i) w = vp (clock j) w) : cl i = cl j

A still object projects to the same position at two moments seen from the same static viewpoint.

theorem SchlenkerEtAl2026.DynProj.viewpoint_ne {W : Type u_1} {E : Type u_2} {T : Type u_4} {V : Type u_5} {S : Type u_6} {ι : Type u_7} {proj : E → V → T → W → S} {d : E} {w : W} {clock : ι → T} {cl : ι → S} {vp : T → W → V} (h : DynProj proj d vp w clock cl) (hd : IsStill proj d w) {i j : ι} (hij : cl i ≠ cl j) : vp (clock i) w ≠ vp (clock j) w

The traveling shot: when a still object projects to a classifier that moves, the viewpoint has moved between the two moments.

theorem SchlenkerEtAl2026.DynProj.eq_of_isStatic {W : Type u_1} {E : Type u_2} {T : Type u_4} {V : Type u_5} {S : Type u_6} {ι : Type u_7} {proj : E → V → T → W → S} {d : E} {w : W} {clock : ι → T} {cl : ι → S} {vp : T → W → V} (h : DynProj proj d vp w clock cl) (hd : IsStill proj d w) (hs : IsStatic vp) (i j : ι) : cl i = cl j

From a static viewpoint a still object projects to a classifier that does not move: the traveling shot is unavailable in [SL24].

Viewpoint variables and Role Shift (§8)

inductive SchlenkerEtAl2026.ViewpointVar : Type

A viewpoint variable: the free variables π_i, whose values come from the assignment, and the context-bound variable π*, introduced by Role Shift.

• free (i : ℕ) : ViewpointVar
• contextBound : ViewpointVar

def SchlenkerEtAl2026.instDecidableEqViewpointVar.decEq (x✝ x✝¹ : ViewpointVar) : Decidable (x✝ = x✝¹)

Equations

• SchlenkerEtAl2026.instDecidableEqViewpointVar.decEq (SchlenkerEtAl2026.ViewpointVar.free a) (SchlenkerEtAl2026.ViewpointVar.free b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• SchlenkerEtAl2026.instDecidableEqViewpointVar.decEq (SchlenkerEtAl2026.ViewpointVar.free i) SchlenkerEtAl2026.ViewpointVar.contextBound = isFalse ⋯
• SchlenkerEtAl2026.instDecidableEqViewpointVar.decEq SchlenkerEtAl2026.ViewpointVar.contextBound (SchlenkerEtAl2026.ViewpointVar.free i) = isFalse ⋯
• SchlenkerEtAl2026.instDecidableEqViewpointVar.decEq SchlenkerEtAl2026.ViewpointVar.contextBound SchlenkerEtAl2026.ViewpointVar.contextBound = isTrue ⋯

@[instance_reducible]

instance SchlenkerEtAl2026.instDecidableEqViewpointVar : DecidableEq ViewpointVar

Equations

• SchlenkerEtAl2026.instDecidableEqViewpointVar = SchlenkerEtAl2026.instDecidableEqViewpointVar.decEq

def SchlenkerEtAl2026.ViewpointVar.denote {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : Type u_5} (s : ℕ → T → W → V) (agentVP : E → T → W → V) (c : Reference.Context W E P T) : ViewpointVar → T → W → V

(33): a free viewpoint variable denotes its value under the assignment s; the context-bound variable π* denotes the dynamic viewpoint of the context's agent.

Equations

• SchlenkerEtAl2026.ViewpointVar.denote s agentVP c (SchlenkerEtAl2026.ViewpointVar.free i) = s i
• SchlenkerEtAl2026.ViewpointVar.denote s agentVP c SchlenkerEtAl2026.ViewpointVar.contextBound = agentVP c.agent

def SchlenkerEtAl2026.Restrictive {W : Type u_1} {T : Type u_4} {V : Type u_5} (s : ℕ → T → W → V) : Prop

The restrictive theory of §8: every free viewpoint variable denotes a static viewpoint.

Equations

• SchlenkerEtAl2026.Restrictive s = ∀ (i : ℕ), SchlenkerEtAl2026.IsStatic (s i)

def SchlenkerEtAl2026.roleShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (IP : Reference.Context W E P T → T → W → Prop) (c : Reference.Context W E P T) (x : E) (t : T) (w : W) : Prop

(34): Role Shift abstracts over the agent, time and world of the context, evaluating its clause at the shifted context and at that time and world.

Equations

• SchlenkerEtAl2026.roleShift IP c x t w = IP (Reference.temporalShift t (Reference.attitudeShift x w c)) t w

def SchlenkerEtAl2026.classifierIcon {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : Type u_5} {S : Type u_6} {ι : Type u_7} (s : ℕ → T → W → V) (agentVP : E → T → W → V) (π : ViewpointVar) (proj : E → V → T → W → S) (d : E) (clock : T → ι → T) (cl : ι → S) (c : Reference.Context W E P T) (t : T) (w : W) : Prop

(31), (36): the iconic component of a dynamic classifier with viewpoint variable π: its argument projects to the classifier from the viewpoint π denotes, along the clock started at the time of evaluation.

Equations

• SchlenkerEtAl2026.classifierIcon s agentVP π proj d clock cl c t w = SchlenkerEtAl2026.DynProj proj d (SchlenkerEtAl2026.ViewpointVar.denote s agentVP c π) w (clock t) cl

theorem SchlenkerEtAl2026.roleShift_classifierIcon_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : Type u_5} {S : Type u_6} {ι : Type u_7} {proj : E → V → T → W → S} {d : E} {cl : ι → S} {s : ℕ → T → W → V} {agentVP : E → T → W → V} {clock' : T → ι → T} (c : Reference.Context W E P T) (x : E) (t : T) (w : W) : roleShift (classifierIcon s agentVP ViewpointVar.contextBound proj d clock' cl) c x t w ↔ DynProj proj d (agentVP x) w (clock' t) cl

(37c): under Role Shift a classifier with the context-bound variable is projected from the character's dynamic viewpoint at the shifted time and world.

theorem SchlenkerEtAl2026.Restrictive.eq_of_free {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : Type u_5} {S : Type u_6} {ι : Type u_7} {proj : E → V → T → W → S} {d : E} {w : W} {clock : ι → T} {cl : ι → S} {s : ℕ → T → W → V} {agentVP : E → T → W → V} (hs : Restrictive s) (hd : IsStill proj d w) (c : Reference.Context W E P T) {i : ℕ} (h : DynProj proj d (ViewpointVar.denote s agentVP c (ViewpointVar.free i)) w clock cl) (j k : ι) : cl j = cl k

Under the restrictive theory a classifier with a free viewpoint variable cannot show a still object moving: a traveling shot needs Role Shift.

theorem SchlenkerEtAl2026.roleShift_viewpoint_ne {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : Type u_5} {S : Type u_6} {ι : Type u_7} {proj : E → V → T → W → S} {d : E} {w : W} {cl : ι → S} {s : ℕ → T → W → V} {agentVP : E → T → W → V} {clock' : T → ι → T} (c : Reference.Context W E P T) (x : E) (t : T) (hd : IsStill proj d w) (h : roleShift (classifierIcon s agentVP ViewpointVar.contextBound proj d clock' cl) c x t w) {i j : ι} (hij : cl i ≠ cl j) : agentVP x (clock' t i) w ≠ agentVP x (clock' t j) w

Under Role Shift the movement of a classifier for a still object is the character's own movement between the two moments.