Spatial Trace Function σ #

@cite{gawron-2009} @cite{krifka-1998} @cite{talmy-2000} @cite{zwarts-2005} @cite{zwarts-winter-2000}

The spatial dimension of event structure: σ maps events to their spatial trajectories (paths). This parallels τ (temporal trace, EventCEM.τ_hom) and θ (thematic role, RoleHom) as the third Krifka/Zwarts dimension.

Three-Dimension Picture #

Temporal: Events →τ Intervals →dur ℚ (temporal dimension)
Spatial: Events →σ Paths →dist ℚ (spatial dimension)
Object: Events →θ Entities →μ ℚ (object dimension)

All three use the same QUA/CUM pullback mechanism via MereoDim.

Key Results #

Bounded path → telic VP (§4): QUA path predicates pull back through σ to yield QUA (telic) VP predicates. "Walk to the store" is telic because "to the store" denotes a QUA set of paths (no proper subpath of a to-the-store path is also to-the-store).
Unbounded path → atelic VP (§4): CUM path predicates pull back through σ to yield CUM (atelic) VP predicates. "Walk towards the store" is atelic because "towards the store" denotes a CUM set of paths.

Sections #

SpatialTrace Class
IsSumHom Instance for σ
MereoDim for σ
Telicity Transfer Through σ
PathShape → Telicity Bridge
Motion Verb Path Annotations

source

class Semantics.Events.SpatialTrace (Loc : Type u_1) (Time : Type u_2) [LinearOrder Time] [cem : Mereology.EventCEM Time] [SemilatticeSup (Core.Path.Path Loc)] :

Type (max u_1 u_2)

Spatial trace: maps events to their spatial trajectories. @cite{zwarts-2005}, @cite{gawron-2009}: σ(e) is the path traversed in event e. Parallels τ (temporal trace) from EventCEM.

σ is required to be a sum homomorphism: σ(e₁ ⊕ e₂) = σ(e₁) ⊕ σ(e₂). This ensures CUM pulls back through σ (atelic paths → atelic VPs). For QUA pullback, injectivity must be assumed separately (via σ_mereoDim), just as for τ.

σ : Ev Time → Core.Path.Path Loc
Extract the spatial path of an event.
σ_map_sup (e₁ e₂ : Ev Time) : σ (SemilatticeSup.sup e₁ e₂) = σ e₁ ⊔ σ e₂
σ preserves sums: σ(e₁ ⊕ e₂) = σ(e₁) ⊕ σ(e₂).

Instances

source

instance Semantics.Events.SpatialTrace.instIsSumHomσ (Loc : Type u_1) (Time : Type u_2) [LinearOrder Time] [cem : Mereology.EventCEM Time] [SemilatticeSup (Core.Path.Path Loc)] [st : SpatialTrace Loc Time] :

Mereology.IsSumHom σ

σ as an IsSumHom instance, derived from SpatialTrace.σ_map_sup. Enables cum_pullback to work automatically for σ. Parallels instIsSumHomRuntime for τ.

source

def Semantics.Events.SpatialTrace.σ_mereoDim {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [cem : Mereology.EventCEM Time] [SemilatticeSup (Core.Path.Path Loc)] [st : SpatialTrace Loc Time] (hinj : Function.Injective σ) :

Mereology.MereoDim σ

σ with injectivity is a MereoDim: the spatial dimension is a mereological morphism, enabling QUA pullback through spatial paths. Parallels the pattern for τ (injective τ → MereoDim).

Equations

⋯ = ⋯

Instances For

source

theorem Semantics.Events.SpatialTrace.bounded_path_telic {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [cem : Mereology.EventCEM Time] [SemilatticeSup (Core.Path.Path Loc)] [st : SpatialTrace Loc Time] (hinj : Function.Injective σ) {P : Core.Path.Path Loc → Prop} (hP : Mereology.QUA P) :

Mereology.QUA (P ∘ σ)

Bounded path predicate → telic VP. "Walk to the store" is telic because "to the store" is QUA (no proper subpath of a to-the-store path is also to-the-store) and QUA pulls back through σ. @cite{zwarts-2005}: bounded PPs yield telic VPs.

source

theorem Semantics.Events.SpatialTrace.unbounded_path_atelic {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [cem : Mereology.EventCEM Time] [SemilatticeSup (Core.Path.Path Loc)] [st : SpatialTrace Loc Time] {P : Core.Path.Path Loc → Prop} (hP : Mereology.CUM P) :

Mereology.CUM (P ∘ σ)

Unbounded path predicate → atelic VP. "Walk towards the store" is atelic because "towards the store" is CUM and CUM pulls back through the σ sum homomorphism. @cite{zwarts-2005}: unbounded PPs yield atelic VPs.

source

def Semantics.Events.SpatialTrace.pathShapeToTelicity :

Core.Path.PathShape → Tense.Aspect.LexicalAspect.Telicity

Map PathShape to Telicity: bounded/source → telic, unbounded → atelic. @cite{zwarts-2005}: the boundedness of a directional PP determines whether the VP it creates is telic or atelic.

This is the spatial analog of the QUA/CUM ↔ telic/atelic correspondence from vendlerClass_telic_implies_qua_intent / vendlerClass_atelic_implies_cum_intent in Events/Mereology.lean.

Equations

Instances For

source

theorem Semantics.Events.SpatialTrace.bounded_telic :

pathShapeToTelicity Core.Path.PathShape.bounded = Tense.Aspect.LexicalAspect.Telicity.telic

Bounded paths are telic.

source

theorem Semantics.Events.SpatialTrace.source_telic :

pathShapeToTelicity Core.Path.PathShape.source = Tense.Aspect.LexicalAspect.Telicity.telic

Source paths are telic.

source

theorem Semantics.Events.SpatialTrace.unbounded_atelic :

pathShapeToTelicity Core.Path.PathShape.unbounded = Tense.Aspect.LexicalAspect.Telicity.atelic

Unbounded paths are atelic.

source

theorem Semantics.Events.SpatialTrace.telicity_boundedness_agree (s : Core.Path.PathShape) :

pathShapeToTelicity s = Tense.Aspect.LexicalAspect.Telicity.telic ↔ s.toBoundedness.isLicensed = true

PathShape telicity agrees with PathShape boundedness licensing: telic ↔ licensed (closed scale), atelic ↔ blocked (open scale). This connects the spatial classification to the scale-theoretic one.

source

def LevinClass.pathSpec :

LevinClass → Option Core.Path.PathShape

Whether a verb class inherently specifies a path shape. Inherently directed motion verbs (Levin 51.1: arrive, come, go) lexicalize a bounded path. Manner-of-motion verbs (51.3: run, walk) are path-neutral — the path comes from a PP complement. @cite{talmy-2000}: verb-framed vs. satellite-framed distinction.

Equations