Documentation

Linglib.Theories.Semantics.Spatial.Path

Spatial Path Infrastructure #

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

Framework-agnostic types for spatial paths and their boundedness classification. Paths are the spatial analog of temporal intervals (Core.Time.Interval): directed stretches of space between locations.

The key linguistic insight: the boundedness of a directional PP determines whether the VP it creates is telic or atelic. Bounded PPs ("to the store") yield telic VPs; unbounded PPs ("towards the store") yield atelic VPs. This parallels the QUA/CUM mereological classification from Core/Mereology.lean.

Sections #

  1. Path Type
  2. Path Shape (Boundedness Classification)
  3. PathShape ↔ Scale Boundedness Bridge
source
structure Semantics.Spatial.Path.Path (Loc : Type u_1) :
Type u_1

Spatial path: a directed trajectory between locations. @cite{zwarts-2005}: paths are directed stretches of space with a source (starting point) and goal (endpoint).

Parallels Core.Time.Interval for the temporal domain. Unlike intervals, paths have no valid : source ≤ goal constraint because spatial locations lack a canonical linear ordering.

  • source : Loc

    Starting location of the path.

  • goal : Loc

    Ending location of the path.

Instances For
    source
    inductive Semantics.Spatial.Path.PathShape :
    Type

    Directional PP boundedness classification. @cite{zwarts-2005}: the boundedness of a directional PP determines whether the VP it creates is telic or atelic.

    • bounded: goal-oriented ("to the store", "into the room")
    • unbounded: direction-oriented ("towards the store", "along the road")
    • source: origin-oriented ("from the store", "out of the room")

    This classifies the set of paths denoted by a PP, not individual paths. "To X" denotes {p | p.goal = X} — a QUA set (no proper subpath of a to-X path is also to-X). "Towards X" denotes a CUM set (concatenating two towards-X paths gives another).

    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Spatial.Path.instDecidableEqPathShape :
      DecidableEq PathShape
      Equations
      source
      def Semantics.Spatial.Path.instReprPathShape.repr :
      PathShape → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[implicit_reducible]
        instance Semantics.Spatial.Path.instReprPathShape :
        Repr PathShape
        Equations
        source
        def Semantics.Spatial.Path.PathShape.toBoundedness :
        PathShape → Core.Scale.Boundedness

        Path shape to scale boundedness: bounded/source paths correspond to closed scales, unbounded paths to open scales. Parallel to quaBoundedness/cumBoundedness in Core/MereoDim.lean §1.

        Equations
        Instances For
          source
          theorem Semantics.Spatial.Path.bounded_path_licensed :
          PathShape.bounded.toBoundedness.isLicensed = true

          Bounded paths are licensed (closed scale → admits degree modification). @cite{zwarts-2005}: "to the store" creates a telic VP because the path set is bounded, corresponding to a closed scale.

          source
          theorem Semantics.Spatial.Path.source_path_licensed :
          PathShape.source.toBoundedness.isLicensed = true

          Source paths are licensed (closed scale at the origin end).

          source
          theorem Semantics.Spatial.Path.unbounded_path_blocked :
          PathShape.unbounded.toBoundedness.isLicensed = false

          Unbounded paths are blocked (open scale → no inherent endpoint). @cite{zwarts-2005}: "towards the store" creates an atelic VP because the path set is unbounded, corresponding to an open scale.

          source
          def Semantics.Spatial.Path.Path.adjacent {Loc : Type u_1} (p1 p2 : Path Loc) :
          Prop

          Two paths are spatially adjacent (∞_H in @cite{krifka-1998}'s notation) if they share an endpoint: one's goal is the other's source. The general adjacency primitive (@cite{krifka-1998} §2.3 eq. 14) is axiomatized abstractly on a part structure; for the concrete Path Loc the share-an-endpoint definition is the intended instance. Used by K98 §4 movement-relation definitions (inlined in Phenomena/TenseAspect/Studies/Krifka1998.lean Part II) to relate spatial adjacency on paths to temporal adjacency on events.

          Equations
          Instances For
            source
            theorem Semantics.Spatial.Path.Path.adjacent_symm {Loc : Type u_1} (p1 p2 : Path Loc) :
            p1.adjacent p2 ↔ p2.adjacent p1

            Path adjacency is symmetric.

            source
            theorem Semantics.Spatial.Path.Path.adjacent_trivial {Loc : Type u_1} (p : Path Loc) (h : p.source = p.goal) :
            p.adjacent p

            A path is adjacent to itself when its source equals its goal (degenerate single-point path). Trivial corner case used in the K98 §4.5 SOURCE/GOAL definitions.