Split-Ergative Conditioning @cite{blake-1994}

@cite{dixon-1994}

@cite{blake-1994} documents that split-ergative systems condition the choice between ergative and accusative alignment on factors such as tense/aspect (Hindi: perfective → ERG), person/animacy (Dyirbal: 3rd → ERG), clause type, or NP type.

The SplitErgativity structure captures this: parameterized by a Factor type and a predicate ergCondition that determines which factor values trigger ergative alignment.

structure Core.SplitErgativity (Factor : Type) : Type

A split-ergative system: the alignment varies by some conditioning factor.

The ergCondition predicate returns true for factor values that trigger ergative alignment, false for those that trigger accusative.

• ergCondition : Factor → Bool

  Predicate: does this factor value trigger ergative alignment?

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

Alignment selected by a split-ergative system for a given factor value.

Equations

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

inductive Core.Aspect : Type

Simple tense/aspect factor for split-ergative conditioning.

• perfective : Aspect
• imperfective : Aspect

instance Core.instDecidableEqAspect : DecidableEq Aspect

Equations

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

instance Core.instBEqAspect : BEq Aspect

Equations

• Core.instBEqAspect = { beq := Core.instBEqAspect.beq }

def Core.instBEqAspect.beq : Aspect → Aspect → Bool

Equations

• Core.instBEqAspect.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.instReprAspect : Repr Aspect

Equations

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

def Core.instReprAspect.repr : Aspect → Nat → 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

Hindi-style split: perfective → ergative, imperfective → accusative.

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