Tangale tense–aspect morphology

The six tense–aspect categories of Tangale (Kaltungo dialect) and their exponence, from [Kid85]'s summary diagram: the perfective and imperative are verb-final suffixes; the four imperfective non-imperatives share the suffix -é and are distinguished by a preposed particle (wa future, né continuous), the subject clitic -n (habitual), or nothing (subjunctive). Suffix alternants are conditioned by voicing of the preceding segment and tense–lax vowel harmony (§1.19–1.20).

The subjectVE field records the (23)–(24) generalization: the subject's final vowel elides unless wa, né, or -n intervenes — the morphological ground for the focus-marking asymmetry between perfective and progressive clauses in [HZ04]. [Jun91] is the lexical companion source.

inductive Tangale.TAM : Type

The six tense–aspect categories ([Kid85] §1.20).

• perfective : TAM
• imperative : TAM
• future : TAM
• continuous : TAM
• habitual : TAM
• subjunctive : TAM

@[implicit_reducible]

instance Tangale.instDecidableEqTAM : DecidableEq TAM

Equations

• Tangale.instDecidableEqTAM x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Tangale.instReprTAM : Repr TAM

Equations

• Tangale.instReprTAM = { reprPrec := Tangale.instReprTAM.repr }

def Tangale.instReprTAM.repr : TAM → Nat → Std.Format

Equations

• Tangale.instReprTAM.repr Tangale.TAM.perfective prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tangale.TAM.perfective")).group prec✝
• Tangale.instReprTAM.repr Tangale.TAM.imperative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tangale.TAM.imperative")).group prec✝
• Tangale.instReprTAM.repr Tangale.TAM.future prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tangale.TAM.future")).group prec✝
• Tangale.instReprTAM.repr Tangale.TAM.continuous prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tangale.TAM.continuous")).group prec✝
• Tangale.instReprTAM.repr Tangale.TAM.habitual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tangale.TAM.habitual")).group prec✝
• Tangale.instReprTAM.repr Tangale.TAM.subjunctive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tangale.TAM.subjunctive")).group prec✝

inductive Tangale.Marker : Type

The distinctive marker accompanying an aspect beyond the verb-final suffix ([Kid85] §1.20).

• none : Marker
• preposed (form : String) : Marker
• subjectClitic (form : String) : Marker

@[implicit_reducible]

instance Tangale.instDecidableEqMarker : DecidableEq Marker

Equations

• Tangale.instDecidableEqMarker = Tangale.instDecidableEqMarker.decEq

def Tangale.instDecidableEqMarker.decEq (x✝ x✝¹ : Marker) : Decidable (x✝ = x✝¹)

Equations

• Tangale.instDecidableEqMarker.decEq Tangale.Marker.none Tangale.Marker.none = isTrue ⋯
• Tangale.instDecidableEqMarker.decEq Tangale.Marker.none (Tangale.Marker.preposed form) = isFalse ⋯
• Tangale.instDecidableEqMarker.decEq Tangale.Marker.none (Tangale.Marker.subjectClitic form) = isFalse ⋯
• Tangale.instDecidableEqMarker.decEq (Tangale.Marker.preposed form) Tangale.Marker.none = isFalse ⋯
• Tangale.instDecidableEqMarker.decEq (Tangale.Marker.preposed a) (Tangale.Marker.preposed b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Tangale.instDecidableEqMarker.decEq (Tangale.Marker.preposed form) (Tangale.Marker.subjectClitic form_1) = isFalse ⋯
• Tangale.instDecidableEqMarker.decEq (Tangale.Marker.subjectClitic form) Tangale.Marker.none = isFalse ⋯
• Tangale.instDecidableEqMarker.decEq (Tangale.Marker.subjectClitic form) (Tangale.Marker.preposed form_1) = isFalse ⋯
• Tangale.instDecidableEqMarker.decEq (Tangale.Marker.subjectClitic a) (Tangale.Marker.subjectClitic b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Tangale.instReprMarker.repr : Marker → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Tangale.instReprMarker.repr Tangale.Marker.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tangale.Marker.none")).group prec✝

@[implicit_reducible]

instance Tangale.instReprMarker : Repr Marker

Equations

• Tangale.instReprMarker = { reprPrec := Tangale.instReprMarker.repr }

structure Tangale.TAMEntry : Type

One row of [Kid85]'s tense–aspect paradigm: the verb-final suffix alternants and the distinctive marker. subjectVE is the (23)–(24) generalization: the preceding subject's final vowel elides iff no marker intervenes.

• tam : TAM
• suffixAlternants : List String
• marker : Marker
• subjectVE : Bool

@[implicit_reducible]

instance Tangale.instDecidableEqTAMEntry : DecidableEq TAMEntry

Equations

• Tangale.instDecidableEqTAMEntry = Tangale.instDecidableEqTAMEntry.decEq

def Tangale.instDecidableEqTAMEntry.decEq (x✝ x✝¹ : TAMEntry) : Decidable (x✝ = x✝¹)

Equations

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

def Tangale.instReprTAMEntry.repr : TAMEntry → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Tangale.instReprTAMEntry : Repr TAMEntry

Equations

• Tangale.instReprTAMEntry = { reprPrec := Tangale.instReprTAMEntry.repr }

def Tangale.perfectiveSg : TAMEntry

Perfective, singular-object suffix set (voicing × harmony alternants).

Equations

• Tangale.perfectiveSg = { tam := Tangale.TAM.perfective, suffixAlternants := ["kó", "kọ́", "gó", "gọ́"], marker := Tangale.Marker.none, subjectVE := true }

def Tangale.perfectivePl : TAMEntry

Perfective, plural-object suffix set — the o → u raising variant of the singular.

Equations

• Tangale.perfectivePl = { tam := Tangale.TAM.perfective, suffixAlternants := ["kú", "kụ́", "gú", "gụ́"], marker := Tangale.Marker.none, subjectVE := true }

def Tangale.perfectiveDistal : TAMEntry

Perfective for action performed at a location different from the speaker's.

Equations

• Tangale.perfectiveDistal = { tam := Tangale.TAM.perfective, suffixAlternants := ["ná"], marker := Tangale.Marker.none, subjectVE := true }

def Tangale.imperative : TAMEntry

Imperfective imperative.

Equations

• Tangale.imperative = { tam := Tangale.TAM.imperative, suffixAlternants := ["u", "ụ"], marker := Tangale.Marker.none, subjectVE := true }

def Tangale.future : TAMEntry

Future: -é plus preposed wa.

Equations

• Tangale.future = { tam := Tangale.TAM.future, suffixAlternants := ["é", "ẹ́"], marker := Tangale.Marker.preposed "wa", subjectVE := false }

def Tangale.continuous : TAMEntry

Continuous: -é plus preposed né — the progressive of [HZ04]'s focus examples.

Equations

• Tangale.continuous = { tam := Tangale.TAM.continuous, suffixAlternants := ["é", "ẹ́"], marker := Tangale.Marker.preposed "né", subjectVE := false }

def Tangale.habitual : TAMEntry

Habitual: -é plus -n cliticized to the subject.

Equations

• Tangale.habitual = { tam := Tangale.TAM.habitual, suffixAlternants := ["é", "ẹ́"], marker := Tangale.Marker.subjectClitic "n", subjectVE := false }

def Tangale.subjunctive : TAMEntry

Subjunctive: -é with no distinctive marker.

Equations

• Tangale.subjunctive = { tam := Tangale.TAM.subjunctive, suffixAlternants := ["é", "ẹ́"], marker := Tangale.Marker.none, subjectVE := true }

def Tangale.tamEntries : List TAMEntry

The full tense–aspect paradigm.

Equations

• Tangale.tamEntries = [Tangale.perfectiveSg, Tangale.perfectivePl, Tangale.perfectiveDistal, Tangale.imperative, Tangale.future, Tangale.continuous, Tangale.habitual, Tangale.subjunctive]

theorem Tangale.imperfectives_share_suffix (e : TAMEntry) : e ∈ tamEntries → e.tam = TAM.future ∨ e.tam = TAM.continuous ∨ e.tam = TAM.habitual ∨ e.tam = TAM.subjunctive → e.suffixAlternants = ["é", "ẹ́"]

The four imperfective non-imperatives share the -é suffix and are distinguished by marker alone.

theorem Tangale.subjectVE_iff_no_marker (e : TAMEntry) : e ∈ tamEntries → (e.subjectVE = true ↔ e.marker = Marker.none)

Subject-final vowel elision is blocked exactly by an intervening marker ((23)–(24)): wa, né, and -n protect the subject's final vowel; bare-suffix aspects elide it.