Documentation

Linglib.Semantics.Spatial.Trace

Spatial Trace Function σ #

[Gaw09] [Kri98] [Tal00] [Zwa05] [ZW00]

The spatial dimension of event structure: σ maps events to their spatial trajectories (paths). This parallels τ (the temporal trace, Event.runtime) and the thematic-role dimension θ as Krifka/Zwarts trace functions — each a Mereology.IsSumHom into a different domain (intervals, paths, entities).

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] [Event.Mereology Time] [Mereology.ClassicalMereology (Event Time)] [SemilatticeSup (Path.Path Loc)] :
Type (max u_1 u_2)

Spatial trace: maps events to their spatial trajectories. [Zwa05], [Gaw09]: σ(e) is the path traversed in event e. Parallels the temporal trace τ (Event.runtime).

σ 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 τ.

  • σ : Event Time → Path.Path Loc

    Extract the spatial path of an event.

  • σ_map_sup (e₁ e₂ : Event Time) : σ (e₁ ⊔ e₂) = σ e₁ ⊔ σ e₂

    σ preserves sums: σ(e₁ ⊕ e₂) = σ(e₁) ⊕ σ(e₂).

Instances

    IsSumHom Instance for σ #

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

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

    MereoDim for σ #

    source
    def Semantics.Spatial.Trace.σ_mereoDim {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [Event.Mereology Time] [Mereology.ClassicalMereology (Event 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.

    Equations
    • ⋯ = ⋯
    Instances For

      Telicity Transfer Through σ #

      source
      theorem Semantics.Spatial.Trace.bounded_path_telic {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [Event.Mereology Time] [Mereology.ClassicalMereology (Event 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 σ. [Zwa05]: bounded PPs yield telic VPs.

      source
      theorem Semantics.Spatial.Trace.unbounded_path_atelic {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [Event.Mereology Time] [Mereology.ClassicalMereology (Event 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. [Zwa05]: 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. [Zwa05]: 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 over Features.VendlerClass.telicity (see Features.telic_classes).

      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

        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.Order.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.