Tanti Dargwa verbs

A Tanti Dargwa verb is simplex (a root with at most a gender prefix), a preverb verb, or complex (a lexical stem followed by a light verb, with any preverbs between them). Roots, some preverbs and some lexical stems agree in gender by a prefix, so each is given as its morphs under each gender marker, and the marker of the agreement controller fills every gender slot of a verb. The preverbs share the orientation markers and directions of the locative forms.

Main definitions

• Dargwa.Tanti.Localization.preverb?, Dargwa.Tanti.Direction.preverb: the preverbs of a localization with an orientation, and of a direction
• Dargwa.Tanti.localizationPreverbs, Dargwa.Tanti.directionPreverbs: the two groups of preverbs
• Dargwa.Tanti.preverbTemplate: the positions of the two groups, the first before the second
• Dargwa.Tanti.lightVerbs, Dargwa.Tanti.boundLightVerbs: the light verbs, and those found only in complex verbs
• Dargwa.Tanti.ComplexVerb, Dargwa.Tanti.ComplexVerb.morphs: a complex verb and its morphs

Main results

• Dargwa.Tanti.Localization.preverb?_super: če-, če-b- and če-r- are super with the lative, essive and elative markers
• Dargwa.Tanti.length_le_two_of_licensed: a verb whose preverbs the template licenses has at most two
• Dargwa.Tanti.morphs_startCrying: the stem and the light verb of w-isːe-w-ig- take the same marker

Implementation notes

• Sumbatova gives the orientations of the first group as the lative, essive and elative, and glosses če-tːi- and gu-tːi- 'above (motion)' and 'below (motion)'; they are super and sub with the translative marker. tːura- 'outside', ča- 'upward' and ča-r- 'from the top' are cited whole.
• Sumbatova lists aq- both as 'hang' and among the light verbs found only in complex verbs, so hang is in both inventories.
• Her list of light verbs omits b-ut'- 'cut', the light verb of č'u-b-ut'- 'divide by two'.

References

• N. Sumbatova, Dargwa (2021)

Preverbs

def Dargwa.Tanti.Localization.prefix? : Localization → Option Morphology.Morph

The prefix of a localization in a preverb of the first group: če- 'on' for super, gu- 'under' for sub, sa- 'in front of' for ante, and none for the others.

Equations

• Dargwa.Tanti.Localization.super.prefix? = some (Morphology.Morph.pref "če")
• Dargwa.Tanti.Localization.sub.prefix? = some (Morphology.Morph.pref "gu")
• Dargwa.Tanti.Localization.ante.prefix? = some (Morphology.Morph.pref "sa")
• x✝.prefix? = none

def Dargwa.Tanti.Localization.preverb? (l : Localization) (o : Orientation) : Option (Gender.Marker → List Morphology.Morph)

The preverb of the first group with the localization l and the orientation o, the prefix of l followed by the marker of o, and none for a localization without a prefix.

Equations

• l.preverb? o = Option.map (fun (p : Morphology.Morph) (g : Dargwa.Tanti.Gender.Marker) => p :: (Option.map Morphology.Morph.pref (o.marker? g)).toList) l.prefix?

def Dargwa.Tanti.outside : Gender.Marker → List Morphology.Morph

tːura- 'outside', a lative.

Equations

• Dargwa.Tanti.outside x✝ = [Morphology.Morph.pref "tːura"]

def Dargwa.Tanti.onUpward : Gender.Marker → List Morphology.Morph

ča- 'upward', from če- 'on' and ha- 'upward'.

Equations

• Dargwa.Tanti.onUpward x✝ = [Morphology.Morph.pref "ča"]

def Dargwa.Tanti.fromTop : Gender.Marker → List Morphology.Morph

ča-r- 'from the top'.

Equations

• Dargwa.Tanti.fromTop x✝ = [Morphology.Morph.pref "ča", Morphology.Morph.pref "r"]

def Dargwa.Tanti.localizationPreverbs : Finset (Gender.Marker → List Morphology.Morph)

The preverbs of the first group, which express a localization and an orientation: the lative, essive and elative of each localization with a prefix, če-tːi- 'above (motion)' and gu-tːi- 'below (motion)', and those cited whole.

Equations

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

def Dargwa.Tanti.Direction.preverb : Direction → Gender.Marker → List Morphology.Morph

The preverb of a direction: ha- 'upward', ka- 'downward', sa- 'hither (to the speaker)' and b-it- 'thither'.

Equations

• Dargwa.Tanti.Direction.up.preverb x✝ = [Morphology.Morph.pref "ha"]
• Dargwa.Tanti.Direction.down.preverb x✝ = [Morphology.Morph.pref "ka"]
• Dargwa.Tanti.Direction.hither.preverb x✝ = [Morphology.Morph.pref "sa"]
• Dargwa.Tanti.Direction.thither.preverb x✝ = [Morphology.Morph.pref x✝.form, Morphology.Morph.pref "it"]

def Dargwa.Tanti.toAddressee : Gender.Marker → List Morphology.Morph

le- 'hither (to the addressee)', a direction the locative forms lack.

Equations

• Dargwa.Tanti.toAddressee x✝ = [Morphology.Morph.pref "le"]

def Dargwa.Tanti.directionPreverbs : Finset (Gender.Marker → List Morphology.Morph)

The preverbs of the second group, which express a direction.

Equations

• Dargwa.Tanti.directionPreverbs = insert Dargwa.Tanti.toAddressee (Finset.image Dargwa.Tanti.Direction.preverb Finset.univ)

inductive Dargwa.Tanti.PreverbGroup : Type

The two groups of preverbs, the positions they fill.

• localization : PreverbGroup

  The first group, which expresses a localization and an orientation.

• direction : PreverbGroup

  The second group, which expresses a direction.

@[instance_reducible]

instance Dargwa.Tanti.instDecidableEqPreverbGroup : DecidableEq PreverbGroup

Equations

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

@[instance_reducible]

instance Dargwa.Tanti.instReprPreverbGroup : Repr PreverbGroup

Equations

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

def Dargwa.Tanti.instReprPreverbGroup.repr : PreverbGroup → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dargwa.Tanti.instFintypePreverbGroup : Fintype PreverbGroup

Equations

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

def Dargwa.Tanti.PreverbGroup.preverbs : PreverbGroup → Finset (Gender.Marker → List Morphology.Morph)

The preverbs of a group.

Equations

• Dargwa.Tanti.PreverbGroup.localization.preverbs = Dargwa.Tanti.localizationPreverbs
• Dargwa.Tanti.PreverbGroup.direction.preverbs = Dargwa.Tanti.directionPreverbs

def Dargwa.Tanti.preverbTemplate : Morphology.AffixTemplate PreverbGroup

As a rule a verb has at most two preverbs, one of the first group followed by one of the second.

Equations

• Dargwa.Tanti.preverbTemplate = { prefixSlots := [Dargwa.Tanti.PreverbGroup.localization, Dargwa.Tanti.PreverbGroup.direction] }

theorem Dargwa.Tanti.licensed_preverbTemplate_iff {E : PreverbGroup → Type u_1} {w : List ((σ : PreverbGroup) × E σ)} : preverbTemplate.Licensed w ↔ (List.map Sigma.fst w).Sublist [PreverbGroup.localization, PreverbGroup.direction]

theorem Dargwa.Tanti.length_le_two_of_licensed {E : PreverbGroup → Type u_1} {w : List ((σ : PreverbGroup) × E σ)} (h : preverbTemplate.Licensed w) : w.length ≤ 2

A string of preverbs the template licenses has at most two.

theorem Dargwa.Tanti.Localization.preverb?_super : (super.preverb? Orientation.lative = some fun (x : Gender.Marker) => [Morphology.Morph.pref "če"]) ∧ (super.preverb? Orientation.essive = some fun (g : Gender.Marker) => [Morphology.Morph.pref "če", Morphology.Morph.pref g.form]) ∧ super.preverb? Orientation.elative = some fun (x : Gender.Marker) => [Morphology.Morph.pref "če", Morphology.Morph.pref "r"]

če-, če-b- and če-r- are super with the lative, essive and elative markers.

Light verbs

def Dargwa.Tanti.make : Gender.Marker → List Morphology.Morph

b-arq'- 'do, make', the most common light verb.

Equations

• Dargwa.Tanti.make g = [Morphology.Morph.pref g.form, Morphology.Morph.root "arq'"]

def Dargwa.Tanti.become : Gender.Marker → List Morphology.Morph

b-iχ- 'become'.

Equations

• Dargwa.Tanti.become g = [Morphology.Morph.pref g.form, Morphology.Morph.root "iχ"]

def Dargwa.Tanti.speak : Gender.Marker → List Morphology.Morph

w-ik'- 'speak'.

Equations

• Dargwa.Tanti.speak g = [Morphology.Morph.pref g.form, Morphology.Morph.root "ik'"]

def Dargwa.Tanti.leave : Gender.Marker → List Morphology.Morph

b-at- 'leave'.

Equations

• Dargwa.Tanti.leave g = [Morphology.Morph.pref g.form, Morphology.Morph.root "at"]

def Dargwa.Tanti.fall : Gender.Marker → List Morphology.Morph

b-ič- 'fall'.

Equations

• Dargwa.Tanti.fall g = [Morphology.Morph.pref g.form, Morphology.Morph.root "ič"]

def Dargwa.Tanti.hit : Gender.Marker → List Morphology.Morph

b-aˁq- 'hit'.

Equations

• Dargwa.Tanti.hit g = [Morphology.Morph.pref g.form, Morphology.Morph.root "aˁq"]

def Dargwa.Tanti.standUp : Gender.Marker → List Morphology.Morph

b-icː- 'stand up'.

Equations

• Dargwa.Tanti.standUp g = [Morphology.Morph.pref g.form, Morphology.Morph.root "icː"]

def Dargwa.Tanti.sitDown : Gender.Marker → List Morphology.Morph

b-ig- 'sit down'.

Equations

• Dargwa.Tanti.sitDown g = [Morphology.Morph.pref g.form, Morphology.Morph.root "ig"]

def Dargwa.Tanti.hang : Gender.Marker → List Morphology.Morph

aq- 'hang'.

Equations

• Dargwa.Tanti.hang x✝ = [Morphology.Morph.root "aq"]

def Dargwa.Tanti.reach : Gender.Marker → List Morphology.Morph

aʁ- 'reach'.

Equations

• Dargwa.Tanti.reach x✝ = [Morphology.Morph.root "aʁ"]

def Dargwa.Tanti.come : Gender.Marker → List Morphology.Morph

b-ač'- 'come'.

Equations

• Dargwa.Tanti.come g = [Morphology.Morph.pref g.form, Morphology.Morph.root "ač'"]

def Dargwa.Tanti.comeHere : Gender.Marker → List Morphology.Morph

le-b-q'- 'come (here)', whose gender prefix follows the preverb le-.

Equations

• Dargwa.Tanti.comeHere g = Dargwa.Tanti.toAddressee g ++ [Morphology.Morph.pref g.form, Morphology.Morph.root "q'"]

def Dargwa.Tanti.collect : Gender.Marker → List Morphology.Morph

b-arʁ- 'collect'.

Equations

• Dargwa.Tanti.collect g = [Morphology.Morph.pref g.form, Morphology.Morph.root "arʁ"]

def Dargwa.Tanti.put : Gender.Marker → List Morphology.Morph

b-ixː- 'put'.

Equations

• Dargwa.Tanti.put g = [Morphology.Morph.pref g.form, Morphology.Morph.root "ixː"]

def Dargwa.Tanti.beat : Gender.Marker → List Morphology.Morph

it- 'beat'.

Equations

• Dargwa.Tanti.beat x✝ = [Morphology.Morph.root "it"]

def Dargwa.Tanti.goAway : Gender.Marker → List Morphology.Morph

ag- 'go away'.

Equations

• Dargwa.Tanti.goAway x✝ = [Morphology.Morph.root "ag"]

def Dargwa.Tanti.say : Gender.Marker → List Morphology.Morph

ʔ- 'say'.

Equations

• Dargwa.Tanti.say x✝ = [Morphology.Morph.root "ʔ"]

def Dargwa.Tanti.drive : Gender.Marker → List Morphology.Morph

b-erk'- 'drive'.

Equations

• Dargwa.Tanti.drive g = [Morphology.Morph.pref g.form, Morphology.Morph.root "erk'"]

def Dargwa.Tanti.sift : Gender.Marker → List Morphology.Morph

arg- 'sift'.

Equations

• Dargwa.Tanti.sift x✝ = [Morphology.Morph.root "arg"]

def Dargwa.Tanti.tear : Gender.Marker → List Morphology.Morph

b-ertː- 'tear'.

Equations

• Dargwa.Tanti.tear g = [Morphology.Morph.pref g.form, Morphology.Morph.root "ertː"]

def Dargwa.Tanti.struggle : Gender.Marker → List Morphology.Morph

b-aˁʜ- 'struggle'.

Equations

• Dargwa.Tanti.struggle g = [Morphology.Morph.pref g.form, Morphology.Morph.root "aˁʜ"]

def Dargwa.Tanti.cut : Gender.Marker → List Morphology.Morph

b-ut'- 'cut'.

Equations

• Dargwa.Tanti.cut g = [Morphology.Morph.pref g.form, Morphology.Morph.root "ut'"]

def Dargwa.Tanti.uq : Gender.Marker → List Morphology.Morph

b-uq-, found only in complex verbs.

Equations

• Dargwa.Tanti.uq g = [Morphology.Morph.pref g.form, Morphology.Morph.root "uq"]

def Dargwa.Tanti.ikk : Gender.Marker → List Morphology.Morph

b-ikː-, found only in complex verbs.

Equations

• Dargwa.Tanti.ikk g = [Morphology.Morph.pref g.form, Morphology.Morph.root "ikː"]

def Dargwa.Tanti.art : Gender.Marker → List Morphology.Morph

art-, found only in complex verbs.

Equations

• Dargwa.Tanti.art x✝ = [Morphology.Morph.root "art"]

def Dargwa.Tanti.lightVerbs : Finset (Gender.Marker → List Morphology.Morph)

The light verbs Sumbatova lists.

Equations

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

def Dargwa.Tanti.boundLightVerbs : Finset (Gender.Marker → List Morphology.Morph)

The light verbs Sumbatova lists as found only in complex verbs.

Equations

• Dargwa.Tanti.boundLightVerbs = {Dargwa.Tanti.uq, Dargwa.Tanti.hang, Dargwa.Tanti.ikk, Dargwa.Tanti.art}

Complex verbs

inductive Dargwa.Tanti.StemClass : Type

The word class of the lexical stem of a complex verb as an independent word.

• noun : StemClass
• adjective : StemClass
• numeral : StemClass
• verb : StemClass
• ideophone : StemClass

@[instance_reducible]

instance Dargwa.Tanti.instDecidableEqStemClass : DecidableEq StemClass

Equations

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

@[instance_reducible]

instance Dargwa.Tanti.instReprStemClass : Repr StemClass

Equations

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

def Dargwa.Tanti.instReprStemClass.repr : StemClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dargwa.Tanti.instFintypeStemClass : Fintype StemClass

Equations

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

structure Dargwa.Tanti.ComplexVerb : Type

A complex verb is a lexical stem followed by a light verb, with any preverbs between them.

• stem : Gender.Marker → List Morphology.Morph

  The lexical stem, which carries the core meaning of the complex.

• category : Option StemClass

  The word class of the stem, none for a stem restricted to the complex verb.

• preverbs : List ((σ : PreverbGroup) × ↥σ.preverbs)

  The preverbs between the stem and the light verb, each with its group.

• lightVerb : Gender.Marker → List Morphology.Morph

  The light verb.

• gloss : String

  The meaning of the complex verb.

def Dargwa.Tanti.ComplexVerb.morphs (c : ComplexVerb) (g : Gender.Marker) : List Morphology.Morph

The morphs of a complex verb whose agreement controller takes the marker g.

Equations

• c.morphs g = c.stem g ++ List.flatMap (fun (x : (σ : Dargwa.Tanti.PreverbGroup) × ↥σ.preverbs) => ↑x.snd g) c.preverbs ++ c.lightVerb g

def Dargwa.Tanti.finish : ComplexVerb

taman-b-arq'- 'finish' (transitive), from taman 'end'.

Equations

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

def Dargwa.Tanti.prepare : ComplexVerb

ʜaˁdur-d-arq'- 'prepare', from ʜaˁdur- 'ready'.

Equations

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

def Dargwa.Tanti.divideByTwo : ComplexVerb

č'u-b-ut'- 'divide by two', from č'u 'two'.

Equations

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

def Dargwa.Tanti.cough : ComplexVerb

qeʜ-w-ik'- 'cough' (imperfective), from the ideophone qeʜ-.

Equations

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

def Dargwa.Tanti.startCrying : ComplexVerb

w-isːe-w-ig- 'start crying', from w-isː- 'cry' (imperfective).

Equations

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

def Dargwa.Tanti.spin : ComplexVerb

tːurχ-b-arq'- 'spin', from a stem found nowhere else.

Equations

• Dargwa.Tanti.spin = { stem := fun (x : Dargwa.Tanti.Gender.Marker) => [Morphology.Morph.root "tːurχ"], category := none, lightVerb := Dargwa.Tanti.make, gloss := "spin" }

def Dargwa.Tanti.stop : ComplexVerb

t'aš-ka-b-icː- 'stop', from a stem found nowhere else, with the preverb ka- 'downward' between it and the light verb.

Equations

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

theorem Dargwa.Tanti.morphs_startCrying (g : Gender.Marker) : startCrying.morphs g = [Morphology.Morph.pref g.form, Morphology.Morph.root "isːe", Morphology.Morph.pref g.form, Morphology.Morph.root "ig"]

In w-isːe-w-ig- 'start crying' the stem and the light verb each take the marker of the agreement controller.