Dargwa (Tanti) Locative System @cite{sumbatova-2021}

In addition to the 6 grammatical cases (see Dargwa/Case.lean), Dargwa has a rich spatial case system. Locative forms decompose into three morphological layers:

STEM — LOCALIZATION — ORIENTATION — DIRECTION

Eight localizations (SUPER, SUB, ANTE, IN, INTER, AD, APUD, POST) × four orientations (LATIVE, ELATIVE, ESSIVE, TRANSLATIVE) × four directions (UP, DOWN, HITHER, THITHER).

This yields a large paradigm, though not all cells are filled.

inductive Fragments.Dargwa.Locatives.Localization : Type

Localization values: spatial domain w.r.t. the reference point. Tanti has 8 localizations (@cite{sumbatova-2021} §4.4.3.3).

• super : Localization
• sub : Localization
• ante : Localization
• in_ : Localization
• inter : Localization
• ad : Localization
• apud : Localization
• post : Localization

@[implicit_reducible]

instance Fragments.Dargwa.Locatives.instDecidableEqLocalization : DecidableEq Localization

Equations

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

def Fragments.Dargwa.Locatives.instReprLocalization.repr : Localization → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Dargwa.Locatives.instReprLocalization : Repr Localization

Equations

• Fragments.Dargwa.Locatives.instReprLocalization = { reprPrec := Fragments.Dargwa.Locatives.instReprLocalization.repr }

inductive Fragments.Dargwa.Locatives.Orientation : Type

Orientation values: motion w.r.t. the reference point. Tanti has 4 orientations (@cite{sumbatova-2021} §4.4.3.3).

• lative : Orientation
• elative : Orientation
• essive : Orientation
• translative : Orientation

@[implicit_reducible]

instance Fragments.Dargwa.Locatives.instDecidableEqOrientation : DecidableEq Orientation

Equations

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

def Fragments.Dargwa.Locatives.instReprOrientation.repr : Orientation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Dargwa.Locatives.instReprOrientation : Repr Orientation

Equations

• Fragments.Dargwa.Locatives.instReprOrientation = { reprPrec := Fragments.Dargwa.Locatives.instReprOrientation.repr }

inductive Fragments.Dargwa.Locatives.Direction : Type

Direction values: motion w.r.t. the speaker. Tanti has 4 directions (@cite{sumbatova-2021} §4.4.3.3).

• up : Direction
• down : Direction
• hither : Direction
• thither : Direction

@[implicit_reducible]

instance Fragments.Dargwa.Locatives.instDecidableEqDirection : DecidableEq Direction

Equations

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

@[implicit_reducible]

instance Fragments.Dargwa.Locatives.instReprDirection : Repr Direction

Equations

• Fragments.Dargwa.Locatives.instReprDirection = { reprPrec := Fragments.Dargwa.Locatives.instReprDirection.repr }

def Fragments.Dargwa.Locatives.instReprDirection.repr : Direction → ℕ → Std.Format

Equations

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

structure Fragments.Dargwa.Locatives.LocativeForm : Type

A full locative form combines all three layers.

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

def Fragments.Dargwa.Locatives.instReprLocativeForm.repr : LocativeForm → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Dargwa.Locatives.instReprLocativeForm : Repr LocativeForm

Equations

• Fragments.Dargwa.Locatives.instReprLocativeForm = { reprPrec := Fragments.Dargwa.Locatives.instReprLocativeForm.repr }

def Fragments.Dargwa.Locatives.LocativeForm.wellFormed (lf : LocativeForm) : Bool

Well-formedness of a locative form, encoding all combinatorial constraints from @cite{sumbatova-2021} §4.4.3.3:

Direction: absent in essive and translative, obligatory in elative, optional in lative.

Localization × Orientation: translative combines only with SUB, ANTE, POST. POST combines only with translative.

Equations

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

def Fragments.Dargwa.Locatives.Orientation.translativeRestricted (loc : Localization) : Bool

Translative combines only with SUB, ANTE, and POST.

Equations

• Fragments.Dargwa.Locatives.Orientation.translativeRestricted Fragments.Dargwa.Locatives.Localization.sub = true
• Fragments.Dargwa.Locatives.Orientation.translativeRestricted Fragments.Dargwa.Locatives.Localization.ante = true
• Fragments.Dargwa.Locatives.Orientation.translativeRestricted Fragments.Dargwa.Locatives.Localization.post = true
• Fragments.Dargwa.Locatives.Orientation.translativeRestricted loc = false

theorem Fragments.Dargwa.Locatives.eight_localizations : [Localization.super, Localization.sub, Localization.ante, Localization.in_, Localization.inter, Localization.ad, Localization.apud, Localization.post].length = 8

All 8 localizations are distinct (no collapse).

theorem Fragments.Dargwa.Locatives.translative_restricted_sub : Orientation.translativeRestricted Localization.sub = true

Translative combines only with SUB, ANTE, and POST (@cite{sumbatova-2021} ex. 13).

theorem Fragments.Dargwa.Locatives.translative_restricted_ante : Orientation.translativeRestricted Localization.ante = true

theorem Fragments.Dargwa.Locatives.translative_restricted_post : Orientation.translativeRestricted Localization.post = true

theorem Fragments.Dargwa.Locatives.translative_blocked_super : Orientation.translativeRestricted Localization.super = false

theorem Fragments.Dargwa.Locatives.post_lative_illformed : { localization := Localization.post, orientation := Orientation.lative, direction := none }.wellFormed = false

POST + LATIVE is ill-formed (POST only combines with translative).

theorem Fragments.Dargwa.Locatives.post_translative_wellformed : { localization := Localization.post, orientation := Orientation.translative, direction := none }.wellFormed = true

POST + TRANSLATIVE is the only well-formed POST combination.

theorem Fragments.Dargwa.Locatives.elative_needs_direction : { localization := Localization.super, orientation := Orientation.elative, direction := none }.wellFormed = false

Elative requires a direction marker.

theorem Fragments.Dargwa.Locatives.essive_rejects_direction : { localization := Localization.super, orientation := Orientation.essive, direction := some Direction.hither }.wellFormed = false

Essive rejects direction markers.

theorem Fragments.Dargwa.Locatives.super_elative_hither : { localization := Localization.super, orientation := Orientation.elative, direction := some Direction.hither }.wellFormed = true

SUPER-ELATIVE-HITHER (ex. 16: 'from the bridge hither') is well-formed.

theorem Fragments.Dargwa.Locatives.super_essive : { localization := Localization.super, orientation := Orientation.essive, direction := none }.wellFormed = true

SUPER-ESSIVE (ex. 12: 'on the bridge, position') is well-formed.

theorem Fragments.Dargwa.Locatives.sub_translative : { localization := Localization.sub, orientation := Orientation.translative, direction := none }.wellFormed = true

SUB-TRANSLATIVE (ex. 13: 'under the bridge, motion') is well-formed.

theorem Fragments.Dargwa.Locatives.translative_super_illformed : { localization := Localization.super, orientation := Orientation.translative, direction := none }.wellFormed = false

Translative + SUPER is ill-formed.