Tanti Dargwa locative forms

This file defines the locative forms of Tanti Dargwa as Sumbatova describes them. A locative form is the oblique stem followed by three suffix slots: a localization, the domain in space with respect to the reference point, of which Tanti has eight; an orientation, whether the object is in that domain, moving towards it, from it or across it; and a direction of the motion with respect to the speaker, which the essive lacks, the elative requires and the lative admits. The translative combines only with the localizations sub, ante and post, and post with the translative alone. The orientations are the path heads of Pantcheva's decomposition and the localizations refine its regions, so the forms fill the region-by-path grid except for the route outside the exterior. An elative without the direction marker the spatial paradigm demands has a non-locative use, as the causee of a transitive causative and the standard of comparison.

Main definitions

• Dargwa.Tanti.Localization, Dargwa.Tanti.Orientation, Dargwa.Tanti.Direction: the three categories with their suffixes, and Localization.region and Orientation.pathDir their comparative labels
• Dargwa.Tanti.Orientation.marker?: the marker of an orientation, apart from the side it attaches on
• Dargwa.Tanti.LocativeForm: a form, with LocativeForm.morphs its suffixes and LocativeForm.IsSpatial the combinatorics of the spatial paradigm
• Dargwa.Tanti.comparisonStandard: the super-elative of the standard of comparison

Main results

• Dargwa.Tanti.LocativeForm.not_isSpatial_elative_none: no directionless elative is spatial
• Dargwa.Tanti.LocativeForm.isSpatial_post_iff: post takes the translative alone
• Dargwa.Tanti.LocativeForm.exists_isSpatial_iff: the region-by-path grid is filled except for the route outside the exterior

Implementation notes

• The essive is the localization followed by the gender marker, so morphs takes the marker.
• The direction suffixes are cited in their long forms; the short forms drop -le, and -sale and -dale vary with -sele and -dele. Whether the translative takes a direction marker is not stated, so IsSpatial leaves it open.
• The general-localization form of some nouns, kis-na-b 'in the pocket', is irregular and left out, as are the locative adverbs and postpositions, which inflect for orientation.

References

• N. Sumbatova, Dargwa (2021)
• M. Pantcheva, Decomposing Path: The Nanosyntax of Directional Expressions (2011)

Localization

inductive Dargwa.Tanti.Localization : Type

A localization is the domain in space a locative form specifies with respect to the reference point.

• super : Localization

  super -ja, on the surface of the object.

• sub : Localization

  sub -gu, under the object.

• ante : Localization

  ante -sa, in front of the object.

• in_ : Localization

  in -ʜe, -ʜaˁ for some nouns, inside a container.

• inter : Localization

  inter -cːe, in a solid substance.

• apud : Localization

  apud -hira, near the object.

• ad : Localization

  ad -šːu, in the place functionally associated with the object.

• post : Localization

  post -hi, behind the object.

@[instance_reducible]

instance Dargwa.Tanti.instDecidableEqLocalization : DecidableEq Localization

Equations

• Dargwa.Tanti.instDecidableEqLocalization x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Dargwa.Tanti.instReprLocalization : Repr Localization

Equations

• Dargwa.Tanti.instReprLocalization = { reprPrec := Dargwa.Tanti.instReprLocalization.repr }

def Dargwa.Tanti.instReprLocalization.repr : Localization → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dargwa.Tanti.instFintypeLocalization : Fintype Localization

Equations

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

def Dargwa.Tanti.Localization.suffix : Localization → Morphology.Morph

The localization suffix.

Equations

• Dargwa.Tanti.Localization.super.suffix = Morphology.Morph.suff "ja"
• Dargwa.Tanti.Localization.sub.suffix = Morphology.Morph.suff "gu"
• Dargwa.Tanti.Localization.ante.suffix = Morphology.Morph.suff "sa"
• Dargwa.Tanti.Localization.in_.suffix = Morphology.Morph.suff "ʜe"
• Dargwa.Tanti.Localization.inter.suffix = Morphology.Morph.suff "cːe"
• Dargwa.Tanti.Localization.apud.suffix = Morphology.Morph.suff "hira"
• Dargwa.Tanti.Localization.ad.suffix = Morphology.Morph.suff "šːu"
• Dargwa.Tanti.Localization.post.suffix = Morphology.Morph.suff "hi"

def Dargwa.Tanti.Localization.region : Localization → Spatial.Localization

The region of the comparative decomposition a localization falls in. super is the surface, in and inter are the interior and the rest are the exterior.

Equations

• Dargwa.Tanti.Localization.super.region = Spatial.Localization.surface
• Dargwa.Tanti.Localization.in_.region = Spatial.Localization.interior
• Dargwa.Tanti.Localization.inter.region = Spatial.Localization.interior
• Dargwa.Tanti.Localization.sub.region = Spatial.Localization.exterior
• Dargwa.Tanti.Localization.ante.region = Spatial.Localization.exterior
• Dargwa.Tanti.Localization.apud.region = Spatial.Localization.exterior
• Dargwa.Tanti.Localization.ad.region = Spatial.Localization.exterior
• Dargwa.Tanti.Localization.post.region = Spatial.Localization.exterior

def Dargwa.Tanti.Localization.TakesTranslative (l : Localization) : Prop

The localizations the translative combines with.

Equations

• l.TakesTranslative = (l = Dargwa.Tanti.Localization.sub ∨ l = Dargwa.Tanti.Localization.ante ∨ l = Dargwa.Tanti.Localization.post)

@[instance_reducible]

instance Dargwa.Tanti.instDecidablePredLocalizationTakesTranslative : DecidablePred Localization.TakesTranslative

Equations

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

Orientation

inductive Dargwa.Tanti.Orientation : Type

An orientation is the motion, or its absence, with respect to the reference point.

• lative : Orientation

  The lative, unmarked, motion towards the reference point.

• elative : Orientation

  The elative -r, motion from the reference point.

• essive : Orientation

  The essive, the gender marker after the localization, location in the reference point.

• translative : Orientation

  The translative -tːi, motion across the reference point.

@[instance_reducible]

instance Dargwa.Tanti.instDecidableEqOrientation : DecidableEq Orientation

Equations

• Dargwa.Tanti.instDecidableEqOrientation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Dargwa.Tanti.instReprOrientation.repr : Orientation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dargwa.Tanti.instReprOrientation : Repr Orientation

Equations

• Dargwa.Tanti.instReprOrientation = { reprPrec := Dargwa.Tanti.instReprOrientation.repr }

@[instance_reducible]

instance Dargwa.Tanti.instFintypeOrientation : Fintype Orientation

Equations

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

def Dargwa.Tanti.Orientation.marker? : Orientation → Gender.Marker → Option String

The marker of an orientation, the gender marker g for the essive and none for the lative.

Equations

• Dargwa.Tanti.Orientation.lative.marker? x✝ = none
• Dargwa.Tanti.Orientation.elative.marker? x✝ = some "r"
• Dargwa.Tanti.Orientation.essive.marker? x✝ = some x✝.form
• Dargwa.Tanti.Orientation.translative.marker? x✝ = some "tːi"

def Dargwa.Tanti.Orientation.morphs (o : Orientation) (g : Gender.Marker) : List Morphology.Morph

The orientation suffixes, with the gender marker g the essive takes.

Equations

• o.morphs g = (Option.map Morphology.Morph.suff (o.marker? g)).toList

def Dargwa.Tanti.Orientation.pathDir : Orientation → Spatial.Path.Direction

The path head of the comparative decomposition an orientation expresses.

Equations

• Dargwa.Tanti.Orientation.essive.pathDir = Spatial.Path.Direction.place
• Dargwa.Tanti.Orientation.lative.pathDir = Spatial.Path.Direction.goal
• Dargwa.Tanti.Orientation.elative.pathDir = Spatial.Path.Direction.source
• Dargwa.Tanti.Orientation.translative.pathDir = Spatial.Path.Direction.route

Direction

inductive Dargwa.Tanti.Direction : Type

A direction orients the motion with respect to the speaker or another point of reference.

• up : Direction

  -ha(le), upward.

• down : Direction

  -ka(le), downward.

• hither : Direction

  -se(le) or -sale, towards the speaker.

• thither : Direction

  -de(le) or -dale, away from the speaker.

@[instance_reducible]

instance Dargwa.Tanti.instDecidableEqDirection : DecidableEq Direction

Equations

• Dargwa.Tanti.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Dargwa.Tanti.instReprDirection : Repr Direction

Equations

• Dargwa.Tanti.instReprDirection = { reprPrec := Dargwa.Tanti.instReprDirection.repr }

def Dargwa.Tanti.instReprDirection.repr : Direction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dargwa.Tanti.instFintypeDirection : Fintype Direction

Equations

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

def Dargwa.Tanti.Direction.suffix : Direction → Morphology.Morph

The direction suffix, in its long form.

Equations

• Dargwa.Tanti.Direction.up.suffix = Morphology.Morph.suff "hale"
• Dargwa.Tanti.Direction.down.suffix = Morphology.Morph.suff "kale"
• Dargwa.Tanti.Direction.hither.suffix = Morphology.Morph.suff "sele"
• Dargwa.Tanti.Direction.thither.suffix = Morphology.Morph.suff "dele"

Locative forms

structure Dargwa.Tanti.LocativeForm : Type

A locative form is a localization, an orientation and, where the form has one, a direction.

• localization : Localization
• orientation : Orientation
• direction : Option Direction

@[instance_reducible]

instance Dargwa.Tanti.instDecidableEqLocativeForm : DecidableEq LocativeForm

Equations

• Dargwa.Tanti.instDecidableEqLocativeForm = Dargwa.Tanti.instDecidableEqLocativeForm.decEq

def Dargwa.Tanti.instDecidableEqLocativeForm.decEq (x✝ x✝¹ : LocativeForm) : Decidable (x✝ = x✝¹)

Equations

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

def Dargwa.Tanti.instReprLocativeForm.repr : LocativeForm → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dargwa.Tanti.instReprLocativeForm : Repr LocativeForm

Equations

• Dargwa.Tanti.instReprLocativeForm = { reprPrec := Dargwa.Tanti.instReprLocativeForm.repr }

@[instance_reducible]

instance Dargwa.Tanti.instFintypeLocativeForm : Fintype LocativeForm

Equations

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

def Dargwa.Tanti.LocativeForm.morphs (f : LocativeForm) (g : Gender.Marker) : List Morphology.Morph

The suffixes of a locative form after the oblique stem, with the gender marker g in the essive.

Equations

• f.morphs g = f.localization.suffix :: (f.orientation.morphs g ++ (Option.map Dargwa.Tanti.Direction.suffix f.direction).toList)

def Dargwa.Tanti.LocativeForm.IsSpatial (f : LocativeForm) : Prop

A form is spatial when its slots combine as the paradigm allows. The essive takes no direction marker, the elative requires one and the lative admits one; the translative combines only with the localizations that take it, and post only with the translative.

Equations

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

@[instance_reducible]

instance Dargwa.Tanti.LocativeForm.instDecidablePredIsSpatial : DecidablePred IsSpatial

Equations

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

theorem Dargwa.Tanti.LocativeForm.super_elative_hither : { localization := Localization.super, orientation := Orientation.elative, direction := some Direction.hither }.IsSpatial ∧ { localization := Localization.super, orientation := Orientation.elative, direction := some Direction.hither }.morphs Gender.Marker.b = [Morphology.Morph.suff "ja", Morphology.Morph.suff "r", Morphology.Morph.suff "sele"]

theorem Dargwa.Tanti.LocativeForm.not_isSpatial_elative_none (l : Localization) : ¬{ localization := l, orientation := Orientation.elative, direction := none }.IsSpatial

No elative without a direction marker is spatial.

theorem Dargwa.Tanti.LocativeForm.isSpatial_essive {l : Localization} (h : l ≠ Localization.post) : { localization := l, orientation := Orientation.essive, direction := none }.IsSpatial

theorem Dargwa.Tanti.LocativeForm.isSpatial_lative {l : Localization} (d : Option Direction) (h : l ≠ Localization.post) : { localization := l, orientation := Orientation.lative, direction := d }.IsSpatial

theorem Dargwa.Tanti.LocativeForm.isSpatial_elative_some {l : Localization} (d : Direction) (h : l ≠ Localization.post) : { localization := l, orientation := Orientation.elative, direction := some d }.IsSpatial

theorem Dargwa.Tanti.LocativeForm.isSpatial_translative_iff {l : Localization} {d : Option Direction} : { localization := l, orientation := Orientation.translative, direction := d }.IsSpatial ↔ l.TakesTranslative

theorem Dargwa.Tanti.LocativeForm.isSpatial_post_iff {o : Orientation} {d : Option Direction} : { localization := Localization.post, orientation := o, direction := d }.IsSpatial ↔ o = Orientation.translative

post takes the translative alone.

theorem Dargwa.Tanti.LocativeForm.exists_isSpatial_iff (r : Spatial.Localization) (d : Spatial.Path.Direction) : (∃ (f : LocativeForm), f.IsSpatial ∧ f.localization.region = r ∧ f.orientation.pathDir = d) ↔ d ≠ Spatial.Path.Direction.route ∨ r = Spatial.Localization.exterior

The forms fill the grid of regions and path heads except for the route, which the translative expresses, outside the exterior.

def Dargwa.Tanti.comparisonStandard : LocativeForm

The super-elative without a direction marker of the standard of comparison.

Equations

• Dargwa.Tanti.comparisonStandard = { localization := Dargwa.Tanti.Localization.super, orientation := Dargwa.Tanti.Orientation.elative, direction := none }

theorem Dargwa.Tanti.not_isSpatial_comparisonStandard : ¬comparisonStandard.IsSpatial