Case: Theory-Neutral Inventory @cite{blake-1994}

@cite{comrie-1978}

A framework-agnostic case inventory drawn from @cite{blake-1994}'s cross-linguistic survey. These 19 values cover the cases attested across Blake's typological sample (Chs. 2, 5). Every syntactic framework (Minimalism, HPSG, DG, CCG) can import this type without committing to a particular theory of case assignment.

The inventory is ordered by Blake's case hierarchy (§5.8): if a language has a case lower on the hierarchy, it usually has all cases above it. The formal hierarchy itself lives in Core.Case.Hierarchy.

Core vs. Peripheral

Blake's most basic distinction (p. 32): core cases (NOM/ACC in accusative systems, ERG/ABS in ergative systems) mark grammatical relations determined by argument structure. Peripheral cases mark semantic roles (source, goal, instrument, etc.).

inductive Core.AlignmentFamily : Type

The two major morphosyntactic alignment families.

Used by SplitErgativity to parameterize which alignment a split-ergative system selects. The full five-way typology (neutral, accusative, ergative, tripartite, active) lives in Phenomena.Alignment.Typology.AlignmentType; this Core type restricts to the two families relevant to case splits.

• accusative : AlignmentFamily

  Accusative alignment: S = A (NOM) vs P (ACC)

• ergative : AlignmentFamily

  Ergative alignment: S = P (ABS) vs A (ERG)

instance Core.instDecidableEqAlignmentFamily : DecidableEq AlignmentFamily

Equations

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

def Core.instBEqAlignmentFamily.beq : AlignmentFamily → AlignmentFamily → Bool

Equations

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

instance Core.instBEqAlignmentFamily : BEq AlignmentFamily

Equations

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

instance Core.instReprAlignmentFamily : Repr AlignmentFamily

Equations

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

def Core.instReprAlignmentFamily.repr : AlignmentFamily → Nat → Std.Format

Equations

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

inductive Core.Case : Type

Cross-linguistic case inventory (@cite{blake-1994}, Chs. 2, 5).

The 19 values cover the morphological cases attested across Blake's typological sample. Ordered roughly by the Blake hierarchy (formalized in Hierarchy.lean), from core grammatical cases to peripheral semantic cases.

• nom : Case

  Nominative: unmarked subject in accusative systems

• acc : Case

  Accusative: transitive patient in accusative systems

• erg : Case

  Ergative: transitive agent in ergative systems

• abs : Case

  Absolutive: unmarked S/P in ergative systems

• gen : Case

  Genitive: possessor, partitive source

• dat : Case

  Dative: recipient, goal, experiencer

• loc : Case

  Locative: spatial location

• abl : Case

  Ablative: spatial source, origin

• all : Case

  Allative: spatial goal, direction toward

• inst : Case

  Instrumental: means, instrument

• com : Case

  Comitative: accompaniment ('with X')

• voc : Case

  Vocative: direct address

• part : Case

  Partitive: partial affectedness, existential

• perl : Case

  Perlative: path, motion through

• ben : Case

  Benefactive: beneficiary

• caus : Case

  Causal: reason, cause

• ess : Case

  Essive: state or role ('as X') — Finnish -nA

• transl : Case

  Translative: change of state ('becoming X') — Finnish -ksi

• abess : Case

  Abessive: privative ('without X') — Finnish -ttA

instance Core.instDecidableEqCase : DecidableEq Case

Equations

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

def Core.instBEqCase.beq : Case → Case → Bool

Equations

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

instance Core.instBEqCase : BEq Case

Equations

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

instance Core.instReprCase : Repr Case

Equations

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

def Core.instReprCase.repr : Case → Nat → Std.Format

Equations

• Core.instReprCase.repr Core.Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.nom")).group prec✝
• Core.instReprCase.repr Core.Case.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.acc")).group prec✝
• Core.instReprCase.repr Core.Case.erg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.erg")).group prec✝
• Core.instReprCase.repr Core.Case.abs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.abs")).group prec✝
• Core.instReprCase.repr Core.Case.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.gen")).group prec✝
• Core.instReprCase.repr Core.Case.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.dat")).group prec✝
• Core.instReprCase.repr Core.Case.loc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.loc")).group prec✝
• Core.instReprCase.repr Core.Case.abl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.abl")).group prec✝
• Core.instReprCase.repr Core.Case.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.all")).group prec✝
• Core.instReprCase.repr Core.Case.inst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.inst")).group prec✝
• Core.instReprCase.repr Core.Case.com prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.com")).group prec✝
• Core.instReprCase.repr Core.Case.voc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.voc")).group prec✝
• Core.instReprCase.repr Core.Case.part prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.part")).group prec✝
• Core.instReprCase.repr Core.Case.perl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.perl")).group prec✝
• Core.instReprCase.repr Core.Case.ben prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.ben")).group prec✝
• Core.instReprCase.repr Core.Case.caus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.caus")).group prec✝
• Core.instReprCase.repr Core.Case.ess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.ess")).group prec✝
• Core.instReprCase.repr Core.Case.transl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.transl")).group prec✝
• Core.instReprCase.repr Core.Case.abess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.abess")).group prec✝

def Core.instInhabitedCase.default : Case

Equations

• Core.instInhabitedCase.default = Core.Case.nom

instance Core.instInhabitedCase : Inhabited Case

Equations

• Core.instInhabitedCase = { default := Core.instInhabitedCase.default }

def Core.Case.allCases : List Case

All 19 case values (for finite verification).

Equations

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

theorem Core.Case.allCases_length : allCases.length = 19

def Core.Case.inAllCases (c : Case) : Bool

Check that a case is in the exhaustive list (Bool version for native_decide).

Equations

• c.inAllCases = Core.Case.allCases.any fun (x : Core.Case) => x == c

theorem Core.Case.allCases_complete (c : Case) : c.inAllCases = true

Every case is in the exhaustive list.

inductive Core.CaseAssignment : Type

How case is assigned to an NP in a given construction.

This parameter originates from @cite{stassen-1985} §2.2.1 on comparative constructions, but applies generally to any multi-NP construction: is the case of one NP determined by the case of another (derived), or does it receive a fixed case form regardless of context (fixed)?

• derived : CaseAssignment

  Derived case: NP's case parallels another NP's case. The two NPs show structural parallelism.

• fixed : CaseAssignment

  Fixed case: NP receives a specific oblique case form independent of other NPs' grammatical functions.

instance Core.instDecidableEqCaseAssignment : DecidableEq CaseAssignment

Equations

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

def Core.instBEqCaseAssignment.beq : CaseAssignment → CaseAssignment → Bool

Equations

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

instance Core.instBEqCaseAssignment : BEq CaseAssignment

Equations

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

def Core.instReprCaseAssignment.repr : CaseAssignment → Nat → Std.Format

Equations

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

instance Core.instReprCaseAssignment : Repr CaseAssignment

Equations

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

inductive Core.FixedCaseEncoding : Type

For fixed-case NPs, what syntactic role the NP occupies.

This distinguishes direct-object encoding (NP is governed by a verb) from adverbial encoding (NP is part of an adverbial/PP phrase).

• directObject : FixedCaseEncoding

  NP is direct object of a transitive verb.

• adverbial : FixedCaseEncoding

  NP is constituent of an adverbial phrase.

instance Core.instDecidableEqFixedCaseEncoding : DecidableEq FixedCaseEncoding

Equations

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

instance Core.instBEqFixedCaseEncoding : BEq FixedCaseEncoding

Equations

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

def Core.instBEqFixedCaseEncoding.beq : FixedCaseEncoding → FixedCaseEncoding → Bool

Equations

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

instance Core.instReprFixedCaseEncoding : Repr FixedCaseEncoding

Equations

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

def Core.instReprFixedCaseEncoding.repr : FixedCaseEncoding → Nat → Std.Format

Equations

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

def Core.Case.spatialTriad : List Case

The three spatial cases that serve as adverbial markers cross-linguistically.

These are a subset of the full Case inventory. Many constructions (comparison, possession, benefaction) borrow their markers from spatial case forms — the localistic hypothesis (@cite{stassen-1985} §2.2.3).

Equations

• Core.Case.spatialTriad = [Core.Case.abl, Core.Case.all, Core.Case.loc]

theorem Core.Case.spatialTriad_length : spatialTriad.length = 3