Tanti Dargwa agreement

This file defines the gender and person agreement of Tanti Dargwa as Sumbatova describes it. Dargwa is among the few Nakh-Dagestanian languages with both. There are three genders, masculine for men, feminine for women and neuter for animals and things, and the gender marker a target shows distinguishes them only in the singular. In the plural it distinguishes humans from non-humans, and humans again by whether they include the speaker or the addressee, which is why Sumbatova counts three different plural genders. Gender agreement is controlled by the absolutive argument, by the predicate in a copular clause with two absolutives, and in Tanti a copula or essive in a transitive clause may agree with the ergative or dative instead.

Person agreement has three sets of markers and leaves the third person unmarked. In the clitic and optative sets the second person singular stands against the first person and the second person plural, the configuration Sumbatova calls the Dargic type after the literary Dargi paradigm in Cysouw's typology. A transitive verb agrees in person with the speech-act participant when only one of its arguments is one, and otherwise with the absolutive P. The thematic suffix of a transitive verb is -i when A outranks P on the person hierarchy 1, 2 > 3 and -u otherwise, so it marks exactly the clauses in which the verb agrees with A.

Main declarations

• Dargwa.Gender.Value: the three controller genders, with the singular and plural markers Value.sgMarker and Value.plMarker.
• Dargwa.PersonSet: the clitic, irrealis and optative sets of person markers.
• Dargwa.personController, Dargwa.thematic: the person agreement controller and the thematic suffix of a transitive clause.

Main results

• Dargwa.Gender.Value.sgMarker_injective, Dargwa.Gender.Value.plMarker_masc_eq_fem: the singular markers distinguish the three genders; the plural ones do not.
• Dargwa.PersonSet.realize_eq_nil_iff: in every set, a cell is unmarked exactly when it is not a speech-act participant's.
• Dargwa.isDargic_clitic, Dargwa.isDargic_optative, Dargwa.not_isDargic_irrealis: the clitic and optative sets have the Dargic configuration, the irrealis set does not.
• Dargwa.thematic_eq_i_iff: the thematic suffix is -i exactly when A controls person agreement.

Implementation notes

• A transitive clause is a Clause.Scenario of the persons of A and P. The thematic suffix is read off its kind on the binary scale Person.Class, as Sumbatova states it; the controller is the two-hierarchy rule as she states it.
• The masculine marker ‹w› is dropped or realized -j in some positions. Some nouns for liquids and granular substances take plural agreement, and a few nouns contain a gender marker of their own, which follows the referent's or the possessor's gender.
• Tanti has no clusivity, so the paradigms range over Agreement.Bundle.personNumberCells.

References

• N. Sumbatova, Dargwa (2021)
• M. Cysouw, The Paradigmatic Structure of Person Marking (2003)

Gender

inductive Dargwa.Gender.Value : Type

A controller gender is one of the three classes into which the nouns fall.

• masc : Value

  Men.

• fem : Value

  Women.

• neut : Value

  Animals and inanimates.

@[instance_reducible]

instance Dargwa.Gender.instDecidableEqValue : DecidableEq Value

Equations

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

@[instance_reducible]

instance Dargwa.Gender.instReprValue : Repr Value

Equations

• Dargwa.Gender.instReprValue = { reprPrec := Dargwa.Gender.instReprValue.repr }

def Dargwa.Gender.instReprValue.repr : Value → ℕ → Std.Format

Equations

• Dargwa.Gender.instReprValue.repr Dargwa.Gender.Value.masc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Gender.Value.masc")).group prec✝
• Dargwa.Gender.instReprValue.repr Dargwa.Gender.Value.fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Gender.Value.fem")).group prec✝
• Dargwa.Gender.instReprValue.repr Dargwa.Gender.Value.neut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Gender.Value.neut")).group prec✝

@[instance_reducible]

instance Dargwa.Gender.instFintypeValue : Fintype Value

Equations

• Dargwa.Gender.instFintypeValue = { elems := { val := ↑Dargwa.Gender.Value.enumList, nodup := Dargwa.Gender.Value.enumList_nodup }, complete := Dargwa.Gender.instFintypeValue._proof_1 }

def Dargwa.Gender.Value.toLabel : Value → Gender

Each gender bears the comparative label of the referents it is assigned to.

Equations

• Dargwa.Gender.Value.masc.toLabel = Gender.masculine
• Dargwa.Gender.Value.fem.toLabel = Gender.feminine
• Dargwa.Gender.Value.neut.toLabel = Gender.neuter

inductive Dargwa.Gender.Marker : Type

A gender marker is cited without its position, since a target takes it as a prefix, a suffix or an infix.

• w : Marker
• r : Marker
• b : Marker
• d : Marker

@[instance_reducible]

instance Dargwa.Gender.instDecidableEqMarker : DecidableEq Marker

Equations

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

@[instance_reducible]

instance Dargwa.Gender.instReprMarker : Repr Marker

Equations

• Dargwa.Gender.instReprMarker = { reprPrec := Dargwa.Gender.instReprMarker.repr }

def Dargwa.Gender.instReprMarker.repr : Marker → ℕ → Std.Format

Equations

• Dargwa.Gender.instReprMarker.repr Dargwa.Gender.Marker.w prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Gender.Marker.w")).group prec✝
• Dargwa.Gender.instReprMarker.repr Dargwa.Gender.Marker.r prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Gender.Marker.r")).group prec✝
• Dargwa.Gender.instReprMarker.repr Dargwa.Gender.Marker.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Gender.Marker.b")).group prec✝
• Dargwa.Gender.instReprMarker.repr Dargwa.Gender.Marker.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Gender.Marker.d")).group prec✝

@[instance_reducible]

instance Dargwa.Gender.instFintypeMarker : Fintype Marker

Equations

• Dargwa.Gender.instFintypeMarker = { elems := { val := ↑Dargwa.Gender.Marker.enumList, nodup := Dargwa.Gender.Marker.enumList_nodup }, complete := Dargwa.Gender.instFintypeMarker._proof_1 }

def Dargwa.Gender.Marker.form : Marker → String

The segment of a marker.

Equations

• Dargwa.Gender.Marker.w.form = "w"
• Dargwa.Gender.Marker.r.form = "r"
• Dargwa.Gender.Marker.b.form = "b"
• Dargwa.Gender.Marker.d.form = "d"

def Dargwa.Gender.Value.sgMarker : Value → Marker

A singular controller of each gender takes its own marker.

Equations

• Dargwa.Gender.Value.masc.sgMarker = Dargwa.Gender.Marker.w
• Dargwa.Gender.Value.fem.sgMarker = Dargwa.Gender.Marker.r
• Dargwa.Gender.Value.neut.sgMarker = Dargwa.Gender.Marker.b

def Dargwa.Gender.Value.plMarker : Value → Person.Class → Marker

A plural controller takes ‹d› when it is non-human or includes the speaker or the addressee, and ‹b› when it is human and does not.

Equations

• Dargwa.Gender.Value.neut.plMarker x✝ = Dargwa.Gender.Marker.d
• x✝.plMarker Person.Class.participant = Dargwa.Gender.Marker.d
• x✝.plMarker Person.Class.nonParticipant = Dargwa.Gender.Marker.b

theorem Dargwa.Gender.Value.sgMarker_injective : Function.Injective sgMarker

The singular markers distinguish the three genders.

theorem Dargwa.Gender.Value.plMarker_masc_eq_fem : masc.plMarker = fem.plMarker

The plural markers do not distinguish men from women.

theorem Dargwa.Gender.Value.plMarker_eq_d_iff {g : Value} {c : Person.Class} : g.plMarker c = Marker.d ↔ g = neut ∨ c = Person.Class.participant

Person markers

inductive Dargwa.PersonSet : Type

The person markers fall into three sets. The clitic set appears in the present, preterite, perfect, present resultative and propositive, the irrealis set in the past habitual, future and conditional, and the optative set in the optative.

• clitic : PersonSet
• irrealis : PersonSet
• optative : PersonSet

@[instance_reducible]

instance Dargwa.instDecidableEqPersonSet : DecidableEq PersonSet

Equations

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

def Dargwa.instReprPersonSet.repr : PersonSet → ℕ → Std.Format

Equations

• Dargwa.instReprPersonSet.repr Dargwa.PersonSet.clitic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.PersonSet.clitic")).group prec✝
• Dargwa.instReprPersonSet.repr Dargwa.PersonSet.irrealis prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.PersonSet.irrealis")).group prec✝
• Dargwa.instReprPersonSet.repr Dargwa.PersonSet.optative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.PersonSet.optative")).group prec✝

@[instance_reducible]

instance Dargwa.instReprPersonSet : Repr PersonSet

Equations

• Dargwa.instReprPersonSet = { reprPrec := Dargwa.instReprPersonSet.repr }

@[instance_reducible]

instance Dargwa.instFintypePersonSet : Fintype PersonSet

Equations

• Dargwa.instFintypePersonSet = { elems := { val := ↑Dargwa.PersonSet.enumList, nodup := Dargwa.PersonSet.enumList_nodup }, complete := Dargwa.instFintypePersonSet._proof_1 }

def Dargwa.PersonSet.paradigm : PersonSet → Agreement.Paradigm (List Morphology.Morph)

Each set is a paradigm over the person–number cells. The irrealis first person plural -ʜaˁ reduces to -ʜe, the second person -t: to -t, and the optative second person plural -a also appears as -a-ja.

Equations

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

theorem Dargwa.PersonSet.realize_eq_nil_iff (s : PersonSet) (c : Agreement.Bundle) : c ∈ Agreement.Bundle.personNumberCells → (s.paradigm.realize c = some [] ↔ ¬c.IsSAP)

In every set, a cell is unmarked exactly when it is not a speech-act participant's.

def Dargwa.pastClitic : Morphology.Morph

The past tense clitic bears no person.

Equations

• Dargwa.pastClitic = Morphology.Morph.encl "de"

theorem Dargwa.clitic_second_singular : PersonSet.clitic.paradigm.realize (Agreement.Bundle.personNumber Person.second Number.singular) = some [pastClitic]

The second person singular clitic is the past tense clitic.

def Dargwa.IsDargic (p : Agreement.Paradigm (List Morphology.Morph)) : Prop

A paradigm has the Dargic configuration when two speech-act participant cells share a marker exactly when both or neither is the second person singular.

Equations

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

@[instance_reducible]

instance Dargwa.instDecidableIsDargic (p : Agreement.Paradigm (List Morphology.Morph)) : Decidable (IsDargic p)

Equations

• Dargwa.instDecidableIsDargic p = id inferInstance

theorem Dargwa.isDargic_clitic : IsDargic PersonSet.clitic.paradigm

theorem Dargwa.isDargic_optative : IsDargic PersonSet.optative.paradigm

theorem Dargwa.not_isDargic_irrealis : ¬IsDargic PersonSet.irrealis.paradigm

The irrealis set has a first person plural marker of its own.

Transitive clauses

def Dargwa.personController (s : Clause.Scenario Person) : ArgumentRole

The argument a transitive verb agrees with in person, by the hierarchies 1, 2 > 3 and absolutive > ergative. It is A when A alone is a speech-act participant and the absolutive P otherwise.

Equations

• Dargwa.personController s = if s.high.IsSAP ∧ ¬s.low.IsSAP then ArgumentRole.A else ArgumentRole.P

def Dargwa.thematic (s : Clause.Scenario Person) : Morphology.Morph

The thematic suffix of a transitive verb is -i when A is higher than P on the person hierarchy 1, 2 > 3, and -u when the two are equal or P is higher.

Equations

• Dargwa.thematic s = if (Clause.Scenario.map Person.toClass s).kind = Clause.Scenario.Kind.downstream then Morphology.Morph.suff "i" else Morphology.Morph.suff "u"

def Dargwa.intransitiveThematic (p : Person) : List Morphology.Morph

An intransitive verb takes the thematic suffix -u with a speech-act participant, and -ar or -an otherwise.

Equations

• Dargwa.intransitiveThematic p = if p.IsSAP then [Morphology.Morph.suff "u"] else [Morphology.Morph.suff "ar", Morphology.Morph.suff "an"]

theorem Dargwa.thematic_eq_i_iff (s : Clause.Scenario Person) : thematic s = Morphology.Morph.suff "i" ↔ personController s = ArgumentRole.A

The thematic suffix is -i exactly when A controls person agreement.

def Dargwa.transitiveClitic (a p : Person × Number) : Option (List Morphology.Morph)

A transitive verb whose A and P are the given person–number cells takes the clitic of the cell that controls it.

Equations

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

theorem Dargwa.transitiveClitic_caught : transitiveClitic (Person.first, Number.singular) (Person.second, Number.singular) = some [Morphology.Morph.encl "de"] ∧ transitiveClitic (Person.second, Number.singular) (Person.first, Number.singular) = some [Morphology.Morph.encl "da"] ∧ transitiveClitic (Person.first, Number.singular) (Person.third, Number.singular) = some [Morphology.Morph.encl "da"] ∧ transitiveClitic (Person.second, Number.singular) (Person.third, Number.singular) = some [Morphology.Morph.encl "de"] ∧ transitiveClitic (Person.third, Number.singular) (Person.second, Number.singular) = some [Morphology.Morph.encl "de"]

'I caught you' takes =de, 'you caught me' =da, 'I caught him' =da, 'you caught him' =de and 'Rasul caught you' =de, since the verb agrees with the absolutive when both arguments are speech-act participants and with the participant when one is.