Split Ergativity

@cite{blake-1994} @cite{dixon-1994}

A SplitErgativity Factor is parameterised by the conditioning factor (aspect, person, animacy, …); alignment projects to either the ergative or accusative family. The Hindi aspect-conditioned split (perfective ⇒ ergative; imperfective ⇒ accusative) is the canonical worked example.

structure Core.SplitErgativity (Factor : Type) : Type

A split-ergative system (@cite{blake-1994}, @cite{dixon-1994}): alignment varies by some conditioning factor.

• ergCondition : Factor → Bool

def Core.SplitErgativity.alignment {Factor : Type} (split : SplitErgativity Factor) (f : Factor) : AlignmentFamily

Equations

• split.alignment f = if split.ergCondition f = true then Core.AlignmentFamily.ergative else Core.AlignmentFamily.accusative

inductive Core.Aspect : Type

• perfective : Aspect
• imperfective : Aspect

@[implicit_reducible]

instance Core.instDecidableEqAspect : DecidableEq Aspect

Equations

• Core.instDecidableEqAspect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.instReprAspect : Repr Aspect

Equations

• Core.instReprAspect = { reprPrec := Core.instReprAspect.repr }

def Core.instReprAspect.repr : Aspect → ℕ → Std.Format

Equations

• Core.instReprAspect.repr Core.Aspect.perfective prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Aspect.perfective")).group prec✝
• Core.instReprAspect.repr Core.Aspect.imperfective prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Aspect.imperfective")).group prec✝

def Core.hindiSplit : SplitErgativity Aspect

Equations

• Core.hindiSplit = { ergCondition := fun (a : Core.Aspect) => a == Core.Aspect.perfective }

theorem Core.hindi_perfective_erg : hindiSplit.alignment Aspect.perfective = AlignmentFamily.ergative

theorem Core.hindi_imperfective_acc : hindiSplit.alignment Aspect.imperfective = AlignmentFamily.accusative