Dependent Case Theory

@cite{marantz-1991} @cite{baker-2015} @cite{deal-2010} @cite{ozaki-2026} @cite{scott-2023}

Originally proposed by @cite{marantz-1991} as an alternative to Agree-based case assignment; developed into a cross-linguistic algorithm by @cite{baker-2015}. Case is determined by the structural configuration of NPs within a Spell-Out domain:

1. Lexical case: Assigned by a particular head (P, V) — highest priority
2. Dependent case: Assigned to an NP that stands in a c-command relation with another caseless NP in the same domain
   • Accusative languages: lower NP gets ACC
   • Ergative languages: higher NP gets ERG
   • Tripartite languages: higher NP gets ERG and lower gets ACC
3. Unmarked case: Default for any NP still without case
   • Accusative languages: NOM
   • Ergative languages: ABS
   • Tripartite languages: ABS

Tripartite Alignment

In tripartite systems (e.g., Nez Perce; @cite{deal-2010}), intransitive subjects (S), transitive agents (A), and transitive patients (P) each receive distinct case. Under dependent case, this follows from applying both dependent ergative (to the higher NP) and dependent accusative (to the lower NP) in the same domain, with ABS as the unmarked default (surfacing only when no case competitor exists — i.e., intransitives).

Note: Not all tripartite systems use dependent case. SJA Mam achieves tripartite alignment via inherent case from Voice (ERG for agents, ACC for objects) plus structural case from Infl (ABS for intransitive S). See Fragments.Mayan.Mam.Agreement for the Agree-based analysis.

Key Application: @cite{ozaki-2026}

Japanese departure verbs (hanareru 'leave', deru 'exit') are dyadic unaccusatives with two internal arguments and no thematic Voice. Accusative -o on the source arises from dependent case (not from v/Voice), while ablative kara is lexical case from an optional P head that bleeds dependent accusative.

inductive Minimalism.CaseSource : Type

The source of case assignment, ordered by priority. Lexical case (assigned by P, V) takes priority over dependent case, which takes priority over unmarked (default) case.

• lexical : CaseSource
• dependent : CaseSource
• unmarked : CaseSource

instance Minimalism.instDecidableEqCaseSource : DecidableEq CaseSource

Equations

• Minimalism.instDecidableEqCaseSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.instBEqCaseSource : BEq CaseSource

Equations

• Minimalism.instBEqCaseSource = { beq := Minimalism.instBEqCaseSource.beq }

def Minimalism.instBEqCaseSource.beq : CaseSource → CaseSource → Bool

Equations

• Minimalism.instBEqCaseSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instReprCaseSource : Repr CaseSource

Equations

• Minimalism.instReprCaseSource = { reprPrec := Minimalism.instReprCaseSource.repr }

def Minimalism.instReprCaseSource.repr : CaseSource → ℕ → Std.Format

Equations

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

inductive Minimalism.CaseLanguageType : Type

Language type determines which dependent and unmarked cases are used.

• Accusative: dependent = ACC (on lower NP), unmarked = NOM
• Ergative: dependent = ERG (on higher NP), unmarked = ABS
• Tripartite: dependent = ERG (on higher) + ACC (on lower), unmarked = ABS (@cite{scott-2023}: SJA Mam; cf. Nez Perce)

• accusative : CaseLanguageType
• ergative : CaseLanguageType
• tripartite : CaseLanguageType

instance Minimalism.instDecidableEqCaseLanguageType : DecidableEq CaseLanguageType

Equations

• Minimalism.instDecidableEqCaseLanguageType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.instBEqCaseLanguageType : BEq CaseLanguageType

Equations

• Minimalism.instBEqCaseLanguageType = { beq := Minimalism.instBEqCaseLanguageType.beq }

def Minimalism.instBEqCaseLanguageType.beq : CaseLanguageType → CaseLanguageType → Bool

Equations

• Minimalism.instBEqCaseLanguageType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Minimalism.instReprCaseLanguageType.repr : CaseLanguageType → ℕ → Std.Format

Equations

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

instance Minimalism.instReprCaseLanguageType : Repr CaseLanguageType

Equations

• Minimalism.instReprCaseLanguageType = { reprPrec := Minimalism.instReprCaseLanguageType.repr }

structure Minimalism.NPInDomain : Type

An NP within a Spell-Out domain, before case assignment. List position encodes structural height: earlier = higher = c-commands later.

If a P head (e.g., Japanese kara) assigns lexical case to the NP, lexicalCase is some c; otherwise it is none.

• label : String

  Label identifying this NP

• lexicalCase : Option CaseVal

  Lexical case pre-assigned by a P or V head (e.g., ABL from kara)

instance Minimalism.instDecidableEqNPInDomain : DecidableEq NPInDomain

Equations

• Minimalism.instDecidableEqNPInDomain = Minimalism.instDecidableEqNPInDomain.decEq

def Minimalism.instDecidableEqNPInDomain.decEq (x✝ x✝¹ : NPInDomain) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalism.instBEqNPInDomain.beq : NPInDomain → NPInDomain → Bool

Equations

• Minimalism.instBEqNPInDomain.beq { label := a, lexicalCase := a_1 } { label := b, lexicalCase := b_1 } = (a == b && a_1 == b_1)
• Minimalism.instBEqNPInDomain.beq x✝¹ x✝ = false

instance Minimalism.instBEqNPInDomain : BEq NPInDomain

Equations

• Minimalism.instBEqNPInDomain = { beq := Minimalism.instBEqNPInDomain.beq }

instance Minimalism.instReprNPInDomain : Repr NPInDomain

Equations

• Minimalism.instReprNPInDomain = { reprPrec := Minimalism.instReprNPInDomain.repr }

def Minimalism.instReprNPInDomain.repr : NPInDomain → ℕ → Std.Format

Equations

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

structure Minimalism.CasedNP : Type

Result of case assignment: an NP with its case value and source.

• label : String
• case : CaseVal
• source : CaseSource

instance Minimalism.instDecidableEqCasedNP : DecidableEq CasedNP

Equations

• Minimalism.instDecidableEqCasedNP = Minimalism.instDecidableEqCasedNP.decEq

def Minimalism.instDecidableEqCasedNP.decEq (x✝ x✝¹ : CasedNP) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalism.instBEqCasedNP.beq : CasedNP → CasedNP → Bool

Equations

• Minimalism.instBEqCasedNP.beq { label := a, case := a_1, source := a_2 } { label := b, case := b_1, source := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Minimalism.instBEqCasedNP.beq x✝¹ x✝ = false

instance Minimalism.instBEqCasedNP : BEq CasedNP

Equations

• Minimalism.instBEqCasedNP = { beq := Minimalism.instBEqCasedNP.beq }

instance Minimalism.instReprCasedNP : Repr CasedNP

Equations

• Minimalism.instReprCasedNP = { reprPrec := Minimalism.instReprCasedNP.repr }

def Minimalism.instReprCasedNP.repr : CasedNP → ℕ → Std.Format

Equations

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

def Minimalism.getCaseOf (label : String) (results : List CasedNP) : Option CaseVal

Look up the assigned case for an NP by label.

Equations

• Minimalism.getCaseOf label results = Option.map (fun (x : Minimalism.CasedNP) => x.case) (List.find? (fun (x : Minimalism.CasedNP) => x.label == label) results)

def Minimalism.getSourceOf (label : String) (results : List CasedNP) : Option CaseSource

Look up the case source for an NP by label.

Equations

• Minimalism.getSourceOf label results = Option.map (fun (x : Minimalism.CasedNP) => x.source) (List.find? (fun (x : Minimalism.CasedNP) => x.label == label) results)

def Minimalism.anyLacksCaseIn (nps : List NPInDomain) : Bool

Does any NP in the list lack lexical case? Used to check whether a dependent case competitor exists.

Equations

• Minimalism.anyLacksCaseIn nps = nps.any fun (x : Minimalism.NPInDomain) => x.lexicalCase.isNone

def Minimalism.dependentAccusative (higherNPs : List NPInDomain) (np : NPInDomain) : Option CaseVal

Dependent accusative: assigned to an NP that is c-commanded by another caseless NP in the same domain.

In our list representation, NP at index i is c-commanded by all NPs at index j < i. So NP_i gets ACC if it has no lexical case and some NP before it also has no lexical case.

Equations

• Minimalism.dependentAccusative higherNPs np = if (np.lexicalCase.isNone && Minimalism.anyLacksCaseIn higherNPs) = true then some Minimalism.CaseVal.acc else none

def Minimalism.dependentErgative (np : NPInDomain) (lowerNPs : List NPInDomain) : Option CaseVal

Dependent ergative: assigned to an NP that c-commands another caseless NP. NP_i gets ERG if it has no lexical case and some NP after it also has no lexical case.

Equations

• Minimalism.dependentErgative np lowerNPs = if (np.lexicalCase.isNone && Minimalism.anyLacksCaseIn lowerNPs) = true then some Minimalism.CaseVal.erg else none

def Minimalism.unmarkedCaseFor (lang : CaseLanguageType) : CaseVal

Unmarked (default) case for a given language type.

• Accusative languages: NOM
• Ergative languages: ABS
• Tripartite languages: ABS (only intransitive S gets unmarked case)

Equations

• Minimalism.unmarkedCaseFor Minimalism.CaseLanguageType.accusative = Minimalism.CaseVal.nom
• Minimalism.unmarkedCaseFor Minimalism.CaseLanguageType.ergative = Minimalism.CaseVal.abs
• Minimalism.unmarkedCaseFor Minimalism.CaseLanguageType.tripartite = Minimalism.CaseVal.abs

def Minimalism.assignOneCase (lang : CaseLanguageType) (higherNPs lowerNPs : List NPInDomain) (np : NPInDomain) : CasedNP

Assign case to a single NP given the NPs structurally above and below it. Applies the three-step priority: lexical → dependent → unmarked.

Equations

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

def Minimalism.assignCasesAux (lang : CaseLanguageType) (higher remaining : List NPInDomain) : List CasedNP

Assign case to all NPs in a Spell-Out domain. Processes the list left-to-right, maintaining context of higher NPs and remaining lower NPs for each position.

Equations

• Minimalism.assignCasesAux lang higher [] = []
• Minimalism.assignCasesAux lang higher (np :: rest) = Minimalism.assignOneCase lang higher rest np :: Minimalism.assignCasesAux lang (higher ++ [np]) rest

def Minimalism.assignCases (lang : CaseLanguageType) (nps : List NPInDomain) : List CasedNP

Top-level case assignment for a list of NPs in a Spell-Out domain. List order encodes structural height: first = highest = c-commands all others.

Equations

• Minimalism.assignCases lang nps = Minimalism.assignCasesAux lang [] nps

ACC Variant

"Taro-ga mura-o hanare-ta" (Taro-NOM village-ACC leave-PAST)

Two bare NPs in the TP Spell-Out domain:

• Leaver NP (higher, raised to Spec-TP)
• Source NP (lower, complement of V)
• Source gets dependent ACC; Leaver gets unmarked NOM

def Minimalism.accVariantNPs : List NPInDomain

Equations

• Minimalism.accVariantNPs = [{ label := "leaver", lexicalCase := none }, { label := "source", lexicalCase := none }]

def Minimalism.accVariantResult : List CasedNP

Equations

• Minimalism.accVariantResult = Minimalism.assignCases Minimalism.CaseLanguageType.accusative Minimalism.accVariantNPs

ABL Variant

"Taro-ga mura-kara hanare-ta" (Taro-NOM village-from leave-PAST)

One bare NP + one PP (lexical ABL from kara):

• Leaver NP (higher, raised to Spec-TP)
• Source PP (lower, kara assigns lexical ABL)
• Source has lexical ABL (bleeds dependent case); Leaver gets unmarked NOM

def Minimalism.ablVariantNPs : List NPInDomain

Equations

• Minimalism.ablVariantNPs = [{ label := "leaver", lexicalCase := none }, { label := "source", lexicalCase := some Minimalism.CaseVal.abl }]

def Minimalism.ablVariantResult : List CasedNP

Equations

• Minimalism.ablVariantResult = Minimalism.assignCases Minimalism.CaseLanguageType.accusative Minimalism.ablVariantNPs

theorem Minimalism.lexical_bleeds_dependent (lang : CaseLanguageType) (c : CaseVal) (higherNPs lowerNPs : List NPInDomain) : (assignOneCase lang higherNPs lowerNPs { label := "x", lexicalCase := some c }).source = CaseSource.lexical

Lexical case bleeds dependent case: an NP with lexical case is never assigned dependent case, regardless of structural configuration.

theorem Minimalism.acc_variant_source_gets_acc : getCaseOf "source" accVariantResult = some CaseVal.acc

ACC variant: source (lower NP) gets dependent accusative.

theorem Minimalism.acc_variant_source_is_dependent : getSourceOf "source" accVariantResult = some CaseSource.dependent

ACC variant: source case is dependent (not lexical or unmarked).

theorem Minimalism.acc_variant_leaver_gets_nom : getCaseOf "leaver" accVariantResult = some CaseVal.nom

ACC variant: leaver (higher NP) gets unmarked nominative.

theorem Minimalism.acc_variant_leaver_is_unmarked : getSourceOf "leaver" accVariantResult = some CaseSource.unmarked

ACC variant: leaver case is unmarked.

theorem Minimalism.abl_variant_source_gets_abl : getCaseOf "source" ablVariantResult = some CaseVal.abl

ABL variant: source gets lexical ablative (from kara).

theorem Minimalism.abl_variant_source_is_lexical : getSourceOf "source" ablVariantResult = some CaseSource.lexical

ABL variant: source case is lexical (from P head kara).

theorem Minimalism.abl_variant_leaver_gets_nom : getCaseOf "leaver" ablVariantResult = some CaseVal.nom

ABL variant: leaver gets unmarked nominative.

theorem Minimalism.no_voice_needed_for_acc : have nps := [{ label := "subj", lexicalCase := none }, { label := "obj", lexicalCase := none }]; getCaseOf "obj" (assignCases CaseLanguageType.accusative nps) = some CaseVal.acc ∧ getSourceOf "obj" (assignCases CaseLanguageType.accusative nps) = some CaseSource.dependent

Dependent ACC does not require agentive Voice — it only requires two caseless NPs in the same Spell-Out domain. The Voice head's flavor is irrelevant to the case algorithm.

theorem Minimalism.acc_variant_all_cased : accVariantResult.length = 2

All NPs receive case in the ACC variant.

theorem Minimalism.abl_variant_all_cased : ablVariantResult.length = 2

All NPs receive case in the ABL variant.

Tripartite: Theory-Level Properties

In a tripartite system, both dependent ergative and dependent accusative are active simultaneously: the higher NP gets ERG, the lower gets ACC, and an NP with no case competitor gets unmarked ABS. These are properties of the algorithm, not of any particular language. Language-specific derivations (e.g., SJA Mam) belong in Phenomena/Case/Bridge/.

theorem Minimalism.tripartite_higher_gets_erg : have nps := [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]; getCaseOf "higher" (assignCases CaseLanguageType.tripartite nps) = some CaseVal.erg

Tripartite transitive: higher NP gets dependent ERG.

theorem Minimalism.tripartite_lower_gets_acc : have nps := [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]; getCaseOf "lower" (assignCases CaseLanguageType.tripartite nps) = some CaseVal.acc

Tripartite transitive: lower NP gets dependent ACC.

theorem Minimalism.tripartite_sole_gets_abs : have nps := [{ label := "sole", lexicalCase := none }]; getCaseOf "sole" (assignCases CaseLanguageType.tripartite nps) = some CaseVal.abs

Tripartite intransitive: sole NP gets unmarked ABS.

theorem Minimalism.tripartite_three_distinct : have tr := assignCases CaseLanguageType.tripartite [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]; have intr := assignCases CaseLanguageType.tripartite [{ label := "sole", lexicalCase := none }]; getCaseOf "higher" tr ≠ getCaseOf "lower" tr ∧ getCaseOf "higher" tr ≠ getCaseOf "sole" intr ∧ getCaseOf "lower" tr ≠ getCaseOf "sole" intr

All three cases are distinct — the defining property of tripartite. ERG ≠ ACC ≠ ABS, derived purely from the algorithm.

theorem Minimalism.tripartite_subsumes_both : have nps := [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]; getCaseOf "higher" (assignCases CaseLanguageType.tripartite nps) = getCaseOf "higher" (assignCases CaseLanguageType.ergative nps) ∧ getCaseOf "lower" (assignCases CaseLanguageType.tripartite nps) = getCaseOf "lower" (assignCases CaseLanguageType.accusative nps)

Tripartite subsumes both ergative and accusative dependent case: ERG on the higher NP matches pure ergative; ACC on the lower NP matches pure accusative.

theorem Minimalism.acc_abl_mutually_exclusive : getCaseOf "source" accVariantResult = some CaseVal.acc ∧ getCaseOf "source" ablVariantResult = some CaseVal.abl

ACC and ABL are mutually exclusive on the source: the same structural position receives exactly one of ACC (dependent) or ABL (lexical), never both. This follows from the priority ordering — lexical case preempts dependent case entirely.

theorem Minimalism.leaver_nom_invariant : getCaseOf "leaver" accVariantResult = some CaseVal.nom ∧ getCaseOf "leaver" ablVariantResult = some CaseVal.nom

The leaver gets NOM in both variants. The alternation affects only the source argument; the subject case is invariant.

theorem Minimalism.ergative_mirror : have nps := [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]; getCaseOf "higher" (assignCases CaseLanguageType.ergative nps) = some CaseVal.erg ∧ getCaseOf "lower" (assignCases CaseLanguageType.ergative nps) = some CaseVal.abs

Ergative mirror: in an ergative language with two caseless NPs, the higher NP gets dependent ERG and the lower gets unmarked ABS. This is the typological inverse of the accusative pattern.

theorem Minimalism.single_np_nom : have nps := [{ label := "sole", lexicalCase := none }]; getCaseOf "sole" (assignCases CaseLanguageType.accusative nps) = some CaseVal.nom ∧ getSourceOf "sole" (assignCases CaseLanguageType.accusative nps) = some CaseSource.unmarked

A single caseless NP in an accusative language gets NOM — the standard intransitive case. No dependent case arises because there is no case competitor.

theorem Minimalism.case_is_configural : getCaseOf "source" accVariantResult ≠ getCaseOf "source" ablVariantResult

Case is purely configural: two NPs with identical labels but different lexical case inputs produce different outputs. The algorithm is sensitive only to the NP inventory, not to verb type or Voice flavor.

def Minimalism.structuralCasesFor : CaseLanguageType → List CaseVal

The structural (non-lexical) cases that the dependent case algorithm can assign for each language type. These are exactly the cases that appear in the none (no lexical case) branch of assignOneCase.

Equations

• Minimalism.structuralCasesFor Minimalism.CaseLanguageType.accusative = [Minimalism.CaseVal.nom, Minimalism.CaseVal.acc]
• Minimalism.structuralCasesFor Minimalism.CaseLanguageType.ergative = [Minimalism.CaseVal.abs, Minimalism.CaseVal.erg]
• Minimalism.structuralCasesFor Minimalism.CaseLanguageType.tripartite = [Minimalism.CaseVal.abs, Minimalism.CaseVal.erg, Minimalism.CaseVal.acc]

theorem Minimalism.accusative_nonlexical_cases (higherNPs lowerNPs : List NPInDomain) (np : NPInDomain) (h : np.lexicalCase = none) : have result := assignOneCase CaseLanguageType.accusative higherNPs lowerNPs np; result.case = CaseVal.nom ∨ result.case = CaseVal.acc

In an accusative language, any NP without lexical case receives either NOM (unmarked) or ACC (dependent).

theorem Minimalism.ergative_nonlexical_cases (higherNPs lowerNPs : List NPInDomain) (np : NPInDomain) (h : np.lexicalCase = none) : have result := assignOneCase CaseLanguageType.ergative higherNPs lowerNPs np; result.case = CaseVal.abs ∨ result.case = CaseVal.erg

In an ergative language, any NP without lexical case receives either ABS (unmarked) or ERG (dependent).

theorem Minimalism.tripartite_nonlexical_cases (higherNPs lowerNPs : List NPInDomain) (np : NPInDomain) (h : np.lexicalCase = none) : have result := assignOneCase CaseLanguageType.tripartite higherNPs lowerNPs np; result.case = CaseVal.abs ∨ result.case = CaseVal.erg ∨ result.case = CaseVal.acc

In a tripartite language, any NP without lexical case receives ABS (unmarked), ERG (dependent on a lower NP), or ACC (dependent on a higher NP).