Iconological Semantics

@cite{schlenker-lamberton-2024}

Core types for Iconological Semantics: a framework combining compositional logical semantics with pictorial semantics for sign language classifier predicates. Classifiers have both a logical component (predicate over entities) and an iconic component (projection from a viewpoint).

Viewpoints may be static (a fixed observation point) or dynamic (varying with time and world), following @cite{schlenker-lamberton-lamberton-2026}'s extension.

Key Types

• StaticViewpoint P — a fixed observation point in position space P
• DynamicViewpoint W T P — a viewpoint that varies with time and world
• ViewpointVar — a viewpoint variable: free (π_i) or context-bound (π*)
• ClassifierPred E P — a classifier predicate with logical + iconic content
• dynamicProjection — evaluate projection from a dynamic viewpoint at (w, t)

structure Semantics.Iconic.StaticViewpoint (P : Type u_1) : Type u_1

A static viewpoint: a fixed observation point in some position space. In Iconological Semantics, this is the point from which a classifier's iconic content is evaluated via geometric projection.

• position : P

def Semantics.Iconic.DynamicViewpoint (W : Type u_1) (T : Type u_2) (P : Type u_3) : Type (max (max u_1 u_2) u_3)

A dynamic viewpoint: a function from time-world pairs to static viewpoints. This is @cite{schlenker-lamberton-lamberton-2026}'s key generalization: viewpoints can move, modeling traveling camera shots in sign language narrative.

Equations

• Semantics.Iconic.DynamicViewpoint W T P = (W → T → Semantics.Iconic.StaticViewpoint P)

def Semantics.Iconic.DynamicViewpoint.static {W : Type u_1} {T : Type u_2} {P : Type u_3} (sv : StaticViewpoint P) : DynamicViewpoint W T P

Lift a static viewpoint to a dynamic one (constant function).

Equations

• Semantics.Iconic.DynamicViewpoint.static sv x✝¹ x✝ = sv

def Semantics.Iconic.DynamicViewpoint.isStatic {W : Type u_1} {T : Type u_2} {P : Type u_3} (vp : DynamicViewpoint W T P) : Prop

A dynamic viewpoint is static iff it is constant across all time-world pairs. Standard (non-traveling) viewpoints satisfy this.

Equations

• vp.isStatic = ∀ (w₁ w₂ : W) (t₁ t₂ : T), vp w₁ t₁ = vp w₂ t₂

theorem Semantics.Iconic.static_isStatic {W : Type u_1} {T : Type u_2} {P : Type u_3} (sv : StaticViewpoint P) : (DynamicViewpoint.static sv).isStatic

A static viewpoint lifted to dynamic is indeed static.

inductive Semantics.Iconic.ViewpointVar : Type

A viewpoint variable: determines how a classifier's viewpoint is resolved.

• .free i: the variable π_i, whose value comes from the assignment function. Different classifiers in the same sentence can have distinct free viewpoint variables.
• .contextBound: the variable π*, whose value is the dynamic viewpoint associated with the context's agent. Introduced by Role Shift.

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

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

Equations

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

instance Semantics.Iconic.instDecidableEqViewpointVar : DecidableEq ViewpointVar

Equations

• Semantics.Iconic.instDecidableEqViewpointVar = Semantics.Iconic.instDecidableEqViewpointVar.decEq

instance Semantics.Iconic.instReprViewpointVar : Repr ViewpointVar

Equations

• Semantics.Iconic.instReprViewpointVar = { reprPrec := Semantics.Iconic.instReprViewpointVar.repr }

def Semantics.Iconic.instReprViewpointVar.repr : ViewpointVar → ℕ → Std.Format

Equations

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

def Semantics.Iconic.instBEqViewpointVar.beq : ViewpointVar → ViewpointVar → Bool

Equations

• Semantics.Iconic.instBEqViewpointVar.beq (Semantics.Iconic.ViewpointVar.free a) (Semantics.Iconic.ViewpointVar.free b) = (a == b)
• Semantics.Iconic.instBEqViewpointVar.beq Semantics.Iconic.ViewpointVar.contextBound Semantics.Iconic.ViewpointVar.contextBound = true
• Semantics.Iconic.instBEqViewpointVar.beq x✝¹ x✝ = false

instance Semantics.Iconic.instBEqViewpointVar : BEq ViewpointVar

Equations

• Semantics.Iconic.instBEqViewpointVar = { beq := Semantics.Iconic.instBEqViewpointVar.beq }

def Semantics.Iconic.dynamicProjection {W : Type u_1} {T : Type u_2} {E : Type u_3} {P : Type u_4} (projects : E → StaticViewpoint P → Bool) (d : E) (vp : DynamicViewpoint W T P) (w : W) (t : T) : Bool

Dynamic projection: evaluate projection from a viewpoint that varies with time and world.

At time t in world w, the object is projected from the static viewpoint π(w, t). This captures the traveling shot: as the viewpoint moves, different spatial configurations are visible.

When the viewpoint is static (constructed via DynamicViewpoint.static), this reduces to plain function application at the fixed viewpoint.

Equations

• Semantics.Iconic.dynamicProjection projects d vp w t = projects d (vp w t)

theorem Semantics.Iconic.dynamicProjection_static {W : Type u_1} {T : Type u_2} {E : Type u_3} {P : Type u_4} (projects : E → StaticViewpoint P → Bool) (d : E) (sv : StaticViewpoint P) (w : W) (t₁ t₂ : T) : dynamicProjection projects d (DynamicViewpoint.static sv) w t₁ = dynamicProjection projects d (DynamicViewpoint.static sv) w t₂

Dynamic projection at a static viewpoint is time-invariant.

structure Semantics.Iconic.ClassifierPred (E : Type u_1) (P : Type u_2) : Type (max u_1 u_2)

A classifier predicate: the lexical entry for a sign language classifier, combining logical and iconic content.

The logical component is a standard predicate (e.g., "is a tree"). The iconic component specifies how entities project to the classifier form from a viewpoint. The viewpoint variable determines which viewpoint the iconic component is evaluated relative to.

This corresponds to the paper's (25): ⟦P^π⟧ = λx. ⟦P⟧(x) = 1 and proj(x, s(π), t, w) = P

• logical : E → Bool

  The logical predicate (e.g., tree', pole', person')

• projects : E → StaticViewpoint P → Bool

  The iconic projection function

• viewpointVar : ViewpointVar

  The viewpoint variable this classifier is evaluated relative to

• label : String

  The classifier label (for transcription)

def Semantics.Iconic.ClassifierPred.eval {E : Type u_1} {P : Type u_2} {W : Type u_3} {T : Type u_4} (cl : ClassifierPred E P) (d : E) (vp : DynamicViewpoint W T P) (w : W) (t : T) : Bool

Evaluate a classifier predicate at a dynamic viewpoint. Returns true iff the logical predicate holds AND the object projects to the classifier from the viewpoint at (w, t).

Equations

• cl.eval d vp w t = (cl.logical d && Semantics.Iconic.dynamicProjection cl.projects d vp w t)

theorem Semantics.Iconic.ClassifierPred.eval_static {E : Type u_1} {P : Type u_2} {W : Type u_3} {T : Type u_4} (cl : ClassifierPred E P) (d : E) (sv : StaticViewpoint P) (w : W) (t₁ t₂ : T) : cl.eval d (DynamicViewpoint.static sv) w t₁ = cl.eval d (DynamicViewpoint.static sv) w t₂

At a static viewpoint, classifier evaluation is time-invariant.