Spatial adpositions: the cartographic refinement

[Sve10] [svenonius-2006] [Pan11] [Zwa05]

The refinement a theory supplies for Adposition with relation = .spatial: the Cinque-Rizzi/Svenonius decomposition of the spatial relation into axial part × region × direction × boundedness. This is the spatial slice of the universal functional sequence ([Sve10]); a temporal or grammatical adposition has none of it, which is why it refines a relation rather than defining the category.

The decomposition reuses the Case spatial substrate: direction is Case.PathDir (Pantcheva's Place ⊂ Goal ⊂ Source ⊂ Route) and region is Case.Region — an adposition and a spatial case spell out the same content ([cinque, this volume]: spatial P, adverb, particle, and case all spell out portions of one configuration). The genuinely new piece is AxPart, the object-geometry axial parts ([svenonius-2006]) that case morphology lacks — and unlike PathDir/Region, the axial parts are a flat paradigm, not a ranked containment, so AxPart does not instantiate the partialOrderOfRank gadget.

Main declarations

• Adposition.AxPart — Svenonius axial parts (front/back/top/…), the differentia
• Adposition.SpatialReading — the cartographic decomposition (the plug-in type)
• Adposition.SpatialReading.toCase is left to per-language Studies

inductive Adposition.AxPart : Type

Axial parts ([svenonius-2006]): the object-geometry regions a spatial adposition projects onto the Ground's axes. behind = back, under = bottom, on top of = top, in front of = front, beside = side, inside = interior, outside = exterior. A flat paradigm (the axes are not nested), distinct from the ranked Case.PathDir/Case.Region.

• front : AxPart
• back : AxPart
• top : AxPart
• bottom : AxPart
• side : AxPart
• interior : AxPart
• exterior : AxPart

@[implicit_reducible]

instance Adposition.instDecidableEqAxPart : DecidableEq AxPart

Equations

• Adposition.instDecidableEqAxPart x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Adposition.instReprAxPart : Repr AxPart

Equations

• Adposition.instReprAxPart = { reprPrec := Adposition.instReprAxPart.repr }

def Adposition.instReprAxPart.repr : AxPart → ℕ → Std.Format

Equations

• Adposition.instReprAxPart.repr Adposition.AxPart.front prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adposition.AxPart.front")).group prec✝
• Adposition.instReprAxPart.repr Adposition.AxPart.back prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adposition.AxPart.back")).group prec✝
• Adposition.instReprAxPart.repr Adposition.AxPart.top prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adposition.AxPart.top")).group prec✝
• Adposition.instReprAxPart.repr Adposition.AxPart.bottom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adposition.AxPart.bottom")).group prec✝
• Adposition.instReprAxPart.repr Adposition.AxPart.side prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adposition.AxPart.side")).group prec✝
• Adposition.instReprAxPart.repr Adposition.AxPart.interior prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adposition.AxPart.interior")).group prec✝
• Adposition.instReprAxPart.repr Adposition.AxPart.exterior prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adposition.AxPart.exterior")).group prec✝

@[implicit_reducible]

instance Adposition.instFintypeAxPart : Fintype AxPart

Equations

• Adposition.instFintypeAxPart = { elems := { val := ↑Adposition.AxPart.enumList, nodup := Adposition.AxPart.enumList_nodup }, complete := Adposition.instFintypeAxPart._proof_1 }

structure Adposition.SpatialReading : Type

The cartographic decomposition of a spatial adposition's relation ([Sve10]): an axial part (Svenonius), a stative region (reused Case.Region), a direction (reused Case.PathDir, Pantcheva), and a boundedness ([Zwa05], the separate algebraic axis — to vs towards). Theories own the slices; this is the shared vocabulary that a relation = .spatial adposition is refined into.

• axPart : Option AxPart

  The axial part, if the P is axial/complex (behind); none for the simple directional/locative Ps (in/to/from).

• region : Option Case.Region

  The stative region (interior/surface/exterior), reused from Case.

• direction : Case.PathDir

  The direction (Place/Goal/Source/Route), reused from Case (Pantcheva).

• bounded : Bool

  Boundedness ([Zwa05]): bounded (telic to) vs unbounded (atelic towards) — orthogonal to direction.

def Adposition.instReprSpatialReading.repr : SpatialReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Adposition.instReprSpatialReading : Repr SpatialReading

Equations

• Adposition.instReprSpatialReading = { reprPrec := Adposition.instReprSpatialReading.repr }

def Adposition.instDecidableEqSpatialReading.decEq (x✝ x✝¹ : SpatialReading) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Adposition.instDecidableEqSpatialReading : DecidableEq SpatialReading

Equations

• Adposition.instDecidableEqSpatialReading = Adposition.instDecidableEqSpatialReading.decEq

def Adposition.SpatialReading.denote (r : SpatialReading) : Case.PathProfile

The directional denotation of a spatial reading is the reused Case.PathDir.denote — a spatial adposition and a spatial case with the same direction share one meaning, two exponences.

Equations

• r.denote = r.direction.denote

Smoke tests — the differentia and the reuse

def Adposition.behind : SpatialReading

behind: an axial preposition (back), stative, no direction change.

Equations

• Adposition.behind = { axPart := some Adposition.AxPart.back, direction := Case.PathDir.place }

def Adposition.under : SpatialReading

under: axial (bottom), stative.

Equations

• Adposition.under = { axPart := some Adposition.AxPart.bottom, direction := Case.PathDir.place }

def Adposition.into : SpatialReading

into: interior goal, bounded — no axial part (a simple directional P).

Equations

• Adposition.into = { region := some Case.Region.interior, direction := Case.PathDir.goal, bounded := true }