Documentation

Linglib.Theories.Semantics.Spatial.Trace

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 #

Trace Class #

source
class Semantics.Spatial.Trace (Loc : Type u_1) (Time : Type u_2) [LinearOrder Time] [cem : Events.CEM.EventCEM Time] [SemilatticeSup (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 τ.

Instances

    IsSumHom Instance for σ #

    source
    instance Semantics.Spatial.Trace.instIsSumHomσ (Loc : Type u_1) (Time : Type u_2) [LinearOrder Time] [cem : Events.CEM.EventCEM Time] [SemilatticeSup (Path.Path Loc)] [st : Trace Loc Time] :
    Mereology.IsSumHom σ

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

    MereoDim for σ #

    source
    def Semantics.Spatial.Trace.σ_mereoDim {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [cem : Events.CEM.EventCEM Time] [SemilatticeSup (Path.Path Loc)] [st : Trace 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

      Telicity Transfer Through σ #

      source
      theorem Semantics.Spatial.Trace.bounded_path_telic {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [cem : Events.CEM.EventCEM Time] [SemilatticeSup (Path.Path Loc)] [st : Trace Loc Time] (hinj : Function.Injective σ) {P : 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.Spatial.Trace.unbounded_path_atelic {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [cem : Events.CEM.EventCEM Time] [SemilatticeSup (Path.Path Loc)] [st : Trace Loc Time] {P : 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.

      PathShape → Telicity Bridge #

      source
      def Semantics.Spatial.Trace.pathShapeToTelicity :
      Path.PathShape → Features.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_cases / vendlerClass_atelic_cases in Events/CEM.lean.

      Equations
      Instances For
        source
        theorem Semantics.Spatial.Trace.bounded_telic :
        pathShapeToTelicity Path.PathShape.bounded = Features.Telicity.telic

        Bounded paths are telic.

        source
        theorem Semantics.Spatial.Trace.source_telic :
        pathShapeToTelicity Path.PathShape.source = Features.Telicity.telic

        Source paths are telic.

        source
        theorem Semantics.Spatial.Trace.unbounded_atelic :
        pathShapeToTelicity Path.PathShape.unbounded = Features.Telicity.atelic

        Unbounded paths are atelic.

        source
        theorem Semantics.Spatial.Trace.telicity_boundedness_agree (s : Path.PathShape) :
        pathShapeToTelicity s = Features.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
        @[implicit_reducible]
        instance Semantics.Spatial.Trace.instLicensingPipelinePathShape :
        Core.Scale.LicensingPipeline Path.PathShape

        LicensingPipeline instance for PathShape via the pathShapeToTelicity bridge. Co-located with the bridge per the convention noted in Core/Scales/Defs.lean (instances live with their type).

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