Woolford (1997): Four-Way Case Systems: Ergative, Nominative, Objective and Accusative

This file formalizes [Woo97b]'s account of the Nez Perce case system, in which a transitive clause is nominative–accusative or ergative–objective and a ditransitive adds a second object case. The core inventory has three structural cases, nominative and objective checked in the specifiers of Agr-S and Agr-O and accusative assigned by the verb inside VP, and the lexical cases ergative and dative, assigned with a θ-role (WCase). Agreement is checked in the specifier of an Agr head, so nominative and ergative subjects both trigger subject agreement while only objective objects trigger object agreement (WCase.position). A verb assigns at most as many accusatives as it has arguments minus its lexical cases minus one, the Max. Acc. formula (Frame.maxAcc), which subsumes Burzio's generalization and the generalization that a lexically cased subject denies accusative to its highest object. An object denied accusative moves to Spec Agr-O for objective case; there is one such position, and economy sends the thematically highest caseless object there (Frame.pattern). The four attested ditransitive patterns and the eight prohibited ones follow (patterns_22A, patterns_22B); the strong reading of the generalization, on which a lexical subject denies accusative to every object, leaves the ergative double-object clause underivable (strong_underivable); and the differences between Nez Perce, Thangu and Kalkatungu reduce to whether ergative and dative are assigned optionally or obligatorily (Params.patterns).

Implementation notes

Accusative assignment is obligatory in Nez Perce, so a nominative subject never co-occurs with an objective object; the paper attributes nominative–objective patterns elsewhere to languages whose verbs assign accusative optionally or not at all, a parameter not modelled here. Dative is placed on goals only, as in the paper's ditransitive frames.

References

• [Woo97b]
• [Bur86]

The case inventory and agreement

inductive Woolford1997.WCase : Type

The core cases: structural nominative, objective and accusative, and lexical ergative and dative.

• nom : WCase
• obj : WCase
• acc : WCase
• erg : WCase
• dat : WCase

@[instance_reducible]

instance Woolford1997.instDecidableEqWCase : DecidableEq WCase

Equations

• Woolford1997.instDecidableEqWCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Woolford1997.instReprWCase : Repr WCase

Equations

• Woolford1997.instReprWCase = { reprPrec := Woolford1997.instReprWCase.repr }

def Woolford1997.instReprWCase.repr : WCase → ℕ → Std.Format

Equations

• Woolford1997.instReprWCase.repr Woolford1997.WCase.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Woolford1997.WCase.nom")).group prec✝
• Woolford1997.instReprWCase.repr Woolford1997.WCase.obj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Woolford1997.WCase.obj")).group prec✝
• Woolford1997.instReprWCase.repr Woolford1997.WCase.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Woolford1997.WCase.acc")).group prec✝
• Woolford1997.instReprWCase.repr Woolford1997.WCase.erg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Woolford1997.WCase.erg")).group prec✝
• Woolford1997.instReprWCase.repr Woolford1997.WCase.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Woolford1997.WCase.dat")).group prec✝

@[instance_reducible]

instance Woolford1997.instFintypeWCase : Fintype WCase

Equations

• Woolford1997.instFintypeWCase = { elems := { val := ↑Woolford1997.WCase.enumList, nodup := Woolford1997.WCase.enumList_nodup }, complete := Woolford1997.instFintypeWCase._proof_1 }

inductive Woolford1997.Lexical : Type

The lexical cases, assigned together with a θ-role.

• erg : Lexical
• dat : Lexical

@[instance_reducible]

instance Woolford1997.instDecidableEqLexical : DecidableEq Lexical

Equations

• Woolford1997.instDecidableEqLexical x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Woolford1997.instReprLexical.repr : Lexical → ℕ → Std.Format

Equations

• Woolford1997.instReprLexical.repr Woolford1997.Lexical.erg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Woolford1997.Lexical.erg")).group prec✝
• Woolford1997.instReprLexical.repr Woolford1997.Lexical.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Woolford1997.Lexical.dat")).group prec✝

@[instance_reducible]

instance Woolford1997.instReprLexical : Repr Lexical

Equations

• Woolford1997.instReprLexical = { reprPrec := Woolford1997.instReprLexical.repr }

@[instance_reducible]

instance Woolford1997.instFintypeLexical : Fintype Lexical

Equations

• Woolford1997.instFintypeLexical = { elems := { val := ↑Woolford1997.Lexical.enumList, nodup := Woolford1997.Lexical.enumList_nodup }, complete := Woolford1997.instFintypeLexical._proof_1 }

def Woolford1997.Lexical.toCase : Lexical → WCase

Equations

• Woolford1997.Lexical.erg.toCase = Woolford1997.WCase.erg
• Woolford1997.Lexical.dat.toCase = Woolford1997.WCase.dat

inductive Woolford1997.Position : Type

Where an argument sits at LF: the specifier of Agr-S, the specifier of Agr-O, or inside VP.

• specAgrS : Position
• specAgrO : Position
• inVP : Position

@[instance_reducible]

instance Woolford1997.instDecidableEqPosition : DecidableEq Position

Equations

• Woolford1997.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Woolford1997.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Woolford1997.instReprPosition : Repr Position

Equations

• Woolford1997.instReprPosition = { reprPrec := Woolford1997.instReprPosition.repr }

def Woolford1997.WCase.position : WCase → Position

Nominative and ergative subjects raise to Spec Agr-S, objective objects to Spec Agr-O, and accusative and dative objects stay inside VP.

Equations

• Woolford1997.WCase.nom.position = Woolford1997.Position.specAgrS
• Woolford1997.WCase.erg.position = Woolford1997.Position.specAgrS
• Woolford1997.WCase.obj.position = Woolford1997.Position.specAgrO
• Woolford1997.WCase.acc.position = Woolford1997.Position.inVP
• Woolford1997.WCase.dat.position = Woolford1997.Position.inVP

def Woolford1997.WCase.TriggersSubjectAgreement (c : WCase) : Prop

Subject agreement is checked in Spec Agr-S.

Equations

• c.TriggersSubjectAgreement = (c.position = Woolford1997.Position.specAgrS)

def Woolford1997.WCase.TriggersObjectAgreement (c : WCase) : Prop

Object agreement is checked in Spec Agr-O.

Equations

• c.TriggersObjectAgreement = (c.position = Woolford1997.Position.specAgrO)

@[instance_reducible]

instance Woolford1997.instDecidablePredWCaseTriggersSubjectAgreement : DecidablePred WCase.TriggersSubjectAgreement

Equations

• Woolford1997.instDecidablePredWCaseTriggersSubjectAgreement x✝ = Woolford1997.instDecidablePredWCaseTriggersSubjectAgreement._aux_1 x✝

@[instance_reducible]

instance Woolford1997.instDecidablePredWCaseTriggersObjectAgreement : DecidablePred WCase.TriggersObjectAgreement

Equations

• Woolford1997.instDecidablePredWCaseTriggersObjectAgreement x✝ = Woolford1997.instDecidablePredWCaseTriggersObjectAgreement._aux_1 x✝

theorem Woolford1997.agreement_pattern : WCase.erg.TriggersSubjectAgreement ∧ WCase.nom.TriggersSubjectAgreement ∧ WCase.obj.TriggersObjectAgreement ∧ ¬WCase.acc.TriggersObjectAgreement

The agreement system is nominative–accusative though the case system is ergative: both subject cases trigger subject agreement, and of the two structural object cases only objective triggers object agreement.

The Max. Acc. formula and structural case

structure Woolford1997.Frame : Type

A clause's arguments with their lexical cases: the subject, then the objects in order of thematic prominence.

• subject : Option Lexical
• objects : List (Option Lexical)

def Woolford1997.instDecidableEqFrame.decEq (x✝ x✝¹ : Frame) : Decidable (x✝ = x✝¹)

Equations

• Woolford1997.instDecidableEqFrame.decEq { subject := a, objects := a_1 } { subject := b, objects := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Woolford1997.instDecidableEqFrame : DecidableEq Frame

Equations

• Woolford1997.instDecidableEqFrame = Woolford1997.instDecidableEqFrame.decEq

@[instance_reducible]

instance Woolford1997.instReprFrame : Repr Frame

Equations

• Woolford1997.instReprFrame = { reprPrec := Woolford1997.instReprFrame.repr }

def Woolford1997.instReprFrame.repr : Frame → ℕ → Std.Format

Equations

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

def Woolford1997.Frame.lexicalCount (f : Frame) : ℕ

The number of arguments with lexical case.

Equations

• f.lexicalCount = List.countP Option.isSome (f.subject :: f.objects)

def Woolford1997.Frame.maxAcc (f : Frame) : ℕ

The Max. Acc. formula: the verb assigns at most as many structural accusatives as it has arguments minus its lexical cases minus one.

Equations

• f.maxAcc = f.objects.length + 1 - f.lexicalCount - 1

def Woolford1997.Frame.caseless (f : Frame) : ℕ

The objects without lexical case.

Equations

• f.caseless = List.countP Option.isNone f.objects

def Woolford1997.Frame.denied (f : Frame) : ℕ

The caseless objects denied accusative, which must find case in Spec Agr-O.

Equations

• f.denied = f.caseless - f.maxAcc

def Woolford1997.Frame.assignObjects : ℕ → List (Option Lexical) → List WCase

Structural case on the objects: k caseless objects, the thematically highest, get objective in Spec Agr-O, the rest accusative inside VP.

Equations

• Woolford1997.Frame.assignObjects x✝ [] = []
• Woolford1997.Frame.assignObjects x✝ (some l :: rest) = l.toCase :: Woolford1997.Frame.assignObjects x✝ rest
• Woolford1997.Frame.assignObjects 0 (none :: rest) = Woolford1997.WCase.acc :: Woolford1997.Frame.assignObjects 0 rest
• Woolford1997.Frame.assignObjects k.succ (none :: rest) = Woolford1997.WCase.obj :: Woolford1997.Frame.assignObjects k rest

def Woolford1997.Frame.pattern (f : Frame) : Option (List WCase)

The case pattern of a clause: a caseless subject is nominative, and the objects get structural case, provided at most one object is denied accusative, there being one Spec Agr-O.

Equations

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

def Woolford1997.Frame.deniedStrong (f : Frame) : ℕ

Under the strong reading of the generalization a lexical subject denies accusative to every object.

Equations

• f.deniedStrong = if f.subject.isSome = true then f.caseless else f.denied

def Woolford1997.Frame.patternStrong (f : Frame) : Option (List WCase)

The pattern under the strong reading.

Equations

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

theorem Woolford1997.Frame.maxAcc_eq (f : Frame) : f.maxAcc = f.objects.length - f.lexicalCount

The formula as a count over the objects: their number minus the lexical cases.

theorem Woolford1997.Frame.maxAcc_intransitive (s : Option Lexical) : { subject := s, objects := [] }.maxAcc = 0

A verb with one argument assigns no accusative, whether its argument is external or internal: Burzio's generalization.

theorem Woolford1997.Frame.maxAcc_lexical_subject (l : Lexical) (o : Option Lexical) : { subject := some l, objects := [o] }.maxAcc = 0

A transitive verb with a lexically cased subject assigns no accusative.

Nez Perce patterns

theorem Woolford1997.patterns_transitive : { subject := none, objects := [none] }.pattern = some [WCase.nom, WCase.acc] ∧ { subject := some Lexical.erg, objects := [none] }.pattern = some [WCase.erg, WCase.obj]

The transitive patterns: a nominative subject takes an accusative object, an ergative subject an objective one.

theorem Woolford1997.patterns_transitive_prohibited (s o : Option Lexical) : { subject := s, objects := [o] }.pattern ≠ some [WCase.nom, WCase.obj] ∧ { subject := s, objects := [o] }.pattern ≠ some [WCase.erg, WCase.acc]

Neither nominative–objective nor ergative–accusative is derivable.

theorem Woolford1997.patterns_22A : { subject := none, objects := [none, none] }.pattern = some [WCase.nom, WCase.acc, WCase.acc] ∧ { subject := none, objects := [some Lexical.dat, none] }.pattern = some [WCase.nom, WCase.dat, WCase.acc] ∧ { subject := some Lexical.erg, objects := [none, none] }.pattern = some [WCase.erg, WCase.obj, WCase.acc] ∧ { subject := some Lexical.erg, objects := [some Lexical.dat, none] }.pattern = some [WCase.erg, WCase.dat, WCase.obj]

The four attested ditransitive patterns, one per choice of lexical case on the subject and the goal.

theorem Woolford1997.patterns_22B (s g t : Option Lexical) : { subject := s, objects := [g, t] }.pattern ∉ List.map some [[WCase.nom, WCase.obj, WCase.obj], [WCase.nom, WCase.obj, WCase.acc], [WCase.nom, WCase.acc, WCase.obj], [WCase.nom, WCase.dat, WCase.obj], [WCase.erg, WCase.acc, WCase.acc], [WCase.erg, WCase.acc, WCase.obj], [WCase.erg, WCase.obj, WCase.obj], [WCase.erg, WCase.dat, WCase.acc]]

The eight prohibited ditransitive patterns are derivable from no frame.

theorem Woolford1997.strong_underivable : { subject := some Lexical.erg, objects := [none, none] }.patternStrong = none ∧ { subject := some Lexical.erg, objects := [none, none] }.pattern = some [WCase.erg, WCase.obj, WCase.acc]

Under the strong reading, the ergative double-object clause has two objects competing for the one Spec Agr-O and is underivable; the weak reading derives the attested ergative–objective–accusative.

Typological variation

inductive Woolford1997.Assignment : Type

Whether a verb assigns a lexical case obligatorily or optionally.

• obligatory : Assignment
• optional : Assignment

@[instance_reducible]

instance Woolford1997.instDecidableEqAssignment : DecidableEq Assignment

Equations

• Woolford1997.instDecidableEqAssignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Woolford1997.instReprAssignment : Repr Assignment

Equations

• Woolford1997.instReprAssignment = { reprPrec := Woolford1997.instReprAssignment.repr }

def Woolford1997.instReprAssignment.repr : Assignment → ℕ → Std.Format

Equations

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

def Woolford1997.Assignment.options (l : Lexical) : Assignment → List (Option Lexical)

The lexical markings a setting allows on a slot.

Equations

• Woolford1997.Assignment.options l Woolford1997.Assignment.obligatory = [some l]
• Woolford1997.Assignment.options l Woolford1997.Assignment.optional = [none, some l]

structure Woolford1997.Params : Type

A language's settings for ergative on transitive subjects and dative on goals.

• ergative : Assignment
• dative : Assignment

def Woolford1997.instDecidableEqParams.decEq (x✝ x✝¹ : Params) : Decidable (x✝ = x✝¹)

Equations

• Woolford1997.instDecidableEqParams.decEq { ergative := a, dative := a_1 } { ergative := b, dative := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Woolford1997.instDecidableEqParams : DecidableEq Params

Equations

• Woolford1997.instDecidableEqParams = Woolford1997.instDecidableEqParams.decEq

@[instance_reducible]

instance Woolford1997.instReprParams : Repr Params

Equations

• Woolford1997.instReprParams = { reprPrec := Woolford1997.instReprParams.repr }

def Woolford1997.instReprParams.repr : Params → ℕ → Std.Format

Equations

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

def Woolford1997.Params.frames (P : Params) : List Frame

The intransitive, transitive and ditransitive frames the settings allow.

Equations

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

def Woolford1997.Params.patterns (P : Params) : List (List WCase)

The derivable case patterns.

Equations

• P.patterns = List.filterMap Woolford1997.Frame.pattern P.frames

def Woolford1997.nezPerce : Params

Nez Perce assigns both lexical cases optionally.

Equations

• Woolford1997.nezPerce = { ergative := Woolford1997.Assignment.optional, dative := Woolford1997.Assignment.optional }

def Woolford1997.thangu : Params

Thangu assigns both obligatorily.

Equations

• Woolford1997.thangu = { ergative := Woolford1997.Assignment.obligatory, dative := Woolford1997.Assignment.obligatory }

def Woolford1997.kalkatungu : Params

Kalkatungu assigns ergative obligatorily and dative optionally.

Equations

• Woolford1997.kalkatungu = { ergative := Woolford1997.Assignment.obligatory, dative := Woolford1997.Assignment.optional }

theorem Woolford1997.nezPerce_patterns : nezPerce.patterns = [[WCase.nom], [WCase.nom, WCase.acc], [WCase.erg, WCase.obj], [WCase.nom, WCase.acc, WCase.acc], [WCase.nom, WCase.dat, WCase.acc], [WCase.erg, WCase.obj, WCase.acc], [WCase.erg, WCase.dat, WCase.obj]]

Nez Perce derives the two transitive and four ditransitive patterns.

theorem Woolford1997.thangu_no_accusative (p : List WCase) : p ∈ thangu.patterns → WCase.acc ∉ p

Thangu has a three-way system: with both lexical cases obligatory, no accusative is ever assigned.

theorem Woolford1997.kalkatungu_patterns : kalkatungu.patterns = [[WCase.nom], [WCase.erg, WCase.obj], [WCase.erg, WCase.obj, WCase.acc], [WCase.erg, WCase.dat, WCase.obj]]

Kalkatungu has no nominative–accusative pattern, but its double-object construction without a dative shows accusative.