Case Feature Decomposition @cite{anderson-jm-2006}

@cite{anderson-jm-2006} "Modern Grammars of Case" (Ch. 6) develops a localist case grammar (LCG) in which all semantic relations decompose into combinations of three first-order case features:

• abs (absolutive): holistic participant — the entity that participates as a whole in the predication. Semantically the least specific relation; every predication is assumed to have an absolutive.
• src (source/ergative): first-order source — the origin of action or force. Anderson's "ergative". In spatial contexts, the source of motion.
• loc (locative): place/location — the spatial or abstract location.

These features combine freely, yielding up to 8 possible argument roles. The four SIMPLE case relations are (eq. 11):

Features	Relation	Typical role
∅	abs	patient/theme
{src}	source/erg	agent
{loc}	locative	location
{loc,src²}	ablative	spatial source

where src² denotes second-order source subordinated to loc, distinct from first-order src. Second-order features are not separately represented in this flat model — ablative appears as just loc.

Complex roles (argument-level combinations)

Arguments can bear COMBINATIONS of first-order features (§6.2–6.3):

• Agent: src — first-order source alone (eq. 39a: "Bill read the book")
• Experiencer: src + loc — locative source (eq. 39h: "Bill knew the answer")
• Contactive/patient: abs + loc — located affected entity (eq. 22)
• Self-mover: abs + src — affected source (eq. 39c: "Bill flew to China")

Subject selection hierarchy (eq. 38')

Anderson directly states the hierarchy — it is NOT derived from feature cardinality:

erg > abs

First-order source (src) outranks absolutive. The argument with src becomes subject; if no argument has src, the absolutive becomes subject.

Subject formation (eq. 40): absolutive ⇒ absolutive{erg}. When an absolutive is selected as subject, it acquires the ergative feature — assimilatory neutralization.

Relation to Blake and Caha

• Blake's typological hierarchy (Core.Case.Hierarchy) and Anderson's hierarchy are concordant on core cases.
• Caha's containment hierarchy (Core.Case.Containment) operates at a different level (morphosyntactic form, not semantic features).

inductive Core.CaseFeature : Type

Anderson's three first-order case features (@cite{anderson-jm-2006}, Ch. 6).

The three features are the primitives from which all semantic relations are composed. Their names reflect Anderson's localist tradition.

• abs : CaseFeature

  Absolutive: holistic participant, the affected/located entity.

• src : CaseFeature

  Source/ergative: the origin of action or force (first-order).

• loc : CaseFeature

  Locative: place or spatial/abstract location.

instance Core.instDecidableEqCaseFeature : DecidableEq CaseFeature

Equations

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

instance Core.instBEqCaseFeature : BEq CaseFeature

Equations

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

def Core.instBEqCaseFeature.beq : CaseFeature → CaseFeature → Bool

Equations

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

def Core.instReprCaseFeature.repr : CaseFeature → Nat → Std.Format

Equations

• Core.instReprCaseFeature.repr Core.CaseFeature.abs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.CaseFeature.abs")).group prec✝
• Core.instReprCaseFeature.repr Core.CaseFeature.src prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.CaseFeature.src")).group prec✝
• Core.instReprCaseFeature.repr Core.CaseFeature.loc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.CaseFeature.loc")).group prec✝

instance Core.instReprCaseFeature : Repr CaseFeature

Equations

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

structure Core.CaseRelation : Type

An argument's case specification: a bundle of first-order features (@cite{anderson-jm-2006}, Ch. 6).

Represented as three Bools for computational tractability. The 8 possible bundles include both simple case relations (abs, erg, loc) and complex argument roles (abs+src, src+loc, abs+loc, abs+src+loc).

Second-order features ({goal}, {source} subordinated to loc/abs) are not separately represented. In particular, ablative (loc{source}) and plain locative (loc) are both ⟨false, false, true⟩. This is an acknowledged simplification: second-order source does not participate in subject selection, so the flat representation suffices for linking.

• abs : Bool

  Does this argument bear the absolutive feature?

• src : Bool

  Does this argument bear the source/ergative feature (first-order)?

• loc : Bool

  Does this argument bear the locative feature?

instance Core.instDecidableEqCaseRelation : DecidableEq CaseRelation

Equations

• Core.instDecidableEqCaseRelation = Core.instDecidableEqCaseRelation.decEq

def Core.instDecidableEqCaseRelation.decEq (x✝ x✝¹ : CaseRelation) : Decidable (x✝ = x✝¹)

Equations

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

instance Core.instBEqCaseRelation : BEq CaseRelation

Equations

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

def Core.instBEqCaseRelation.beq : CaseRelation → CaseRelation → Bool

Equations

• Core.instBEqCaseRelation.beq { abs := a, src := a_1, loc := a_2 } { abs := b, src := b_1, loc := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Core.instBEqCaseRelation.beq x✝¹ x✝ = false

def Core.instReprCaseRelation.repr : CaseRelation → Nat → Std.Format

Equations

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

instance Core.instReprCaseRelation : Repr CaseRelation

Equations

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

def Core.instInhabitedCaseRelation.default : CaseRelation

Equations

• Core.instInhabitedCaseRelation.default = { abs := default, src := default, loc := default }

instance Core.instInhabitedCaseRelation : Inhabited CaseRelation

Equations

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

def Core.CaseRelation.neutral : CaseRelation

∅: no features. The semantically empty base.

Equations

• Core.CaseRelation.neutral = { abs := false, src := false, loc := false }

def Core.CaseRelation.absolutive : CaseRelation

{abs}: absolutive alone. Patient/theme — affected entity.

Equations

• Core.CaseRelation.absolutive = { abs := true, src := false, loc := false }

def Core.CaseRelation.ergative : CaseRelation

{src}: source/ergative. Agent — source of action.

Equations

• Core.CaseRelation.ergative = { abs := false, src := true, loc := false }

def Core.CaseRelation.locative : CaseRelation

{loc}: locative. Place/location (also covers ablative = loc{source} in this flat representation, since second-order source is not tracked).

Equations

• Core.CaseRelation.locative = { abs := false, src := false, loc := true }

def Core.CaseRelation.srcAbs : CaseRelation

{abs, src}: absolutive + source. Self-moving agent — both the source of action AND the affected/moving entity. "Bill flew to China" (eq. 39c).

Equations

• Core.CaseRelation.srcAbs = { abs := true, src := true, loc := false }

def Core.CaseRelation.srcLoc : CaseRelation

{src, loc}: source + locative. Experiencer — locative source. "Bill knew the answer" (eq. 39h). The experience is "located at" the experiencer, who is also the source of the knowing. Anderson's notation: E (= erg,loc).

Equations

• Core.CaseRelation.srcLoc = { abs := false, src := true, loc := true }

def Core.CaseRelation.absLoc : CaseRelation

{abs, loc}: absolutive + locative. Contactive — the entity that is simultaneously located and holistically affected. "The ferry reached Patra" (20a); Contactive = abs,loc (eq. 22).

Equations

• Core.CaseRelation.absLoc = { abs := true, src := false, loc := true }

def Core.CaseRelation.absSrcLoc : CaseRelation

{abs, src, loc}: all three features. Complex experiencer/sufferer. "Phil suffered from asthma" (eq. 34).

Equations

• Core.CaseRelation.absSrcLoc = { abs := true, src := true, loc := true }

def Core.CaseRelation.subjectRank (cr : CaseRelation) : Nat

The subject selection rank of a case relation on Anderson's hierarchy (eq. 38', Ch. 6).

Anderson DIRECTLY STATES this hierarchy — it is NOT derived from feature cardinality. The rule: first-order source (src/erg) outranks absolutive. If an argument has src, it becomes subject. If no argument has src, the absolutive becomes subject.

• rank 2: any relation containing src (agent, experiencer, etc.)
• rank 1: any relation containing abs but not src (patient, theme)
• rank 0: locative without abs or src (pure spatial, not a subject)

Equations

• cr.subjectRank = if cr.src = true then 2 else if cr.abs = true then 1 else 0

theorem Core.ergative_rank : CaseRelation.ergative.subjectRank = 2

Source/ergative (agent) has rank 2 — highest.

theorem Core.absolutive_rank : CaseRelation.absolutive.subjectRank = 1

Absolutive (patient) has rank 1.

theorem Core.locative_rank : CaseRelation.locative.subjectRank = 0

Pure locative has rank 0 — not a subject candidate.

theorem Core.neutral_rank : CaseRelation.neutral.subjectRank = 0

Neutral has rank 0.

theorem Core.erg_above_abs : CaseRelation.ergative.subjectRank > CaseRelation.absolutive.subjectRank

Agent outranks patient: erg > abs. This IS Anderson's hierarchy.

theorem Core.abs_above_loc : CaseRelation.absolutive.subjectRank > CaseRelation.locative.subjectRank

Patient outranks pure locative: abs > loc.

theorem Core.experiencer_agent_same_rank : CaseRelation.srcLoc.subjectRank = CaseRelation.ergative.subjectRank

Experiencer (src+loc) has same rank as agent (src): both rank 2. Anderson DISTINGUISHES them (different feature bundles) but they are at the SAME tier for subject selection (both contain src).

theorem Core.selfMover_agent_same_rank : CaseRelation.srcAbs.subjectRank = CaseRelation.ergative.subjectRank

Self-moving agent (abs+src) has rank 2, same as simple agent.

theorem Core.contactive_abs_same_rank : CaseRelation.absLoc.subjectRank = CaseRelation.absolutive.subjectRank

Contactive (abs+loc) has rank 1, same as simple absolutive.

theorem Core.src_determines_subject_rank (cr : CaseRelation) (h : cr.src = true) : cr.subjectRank = 2

Anderson's hierarchy (eq. 38') entails that subject selection depends ONLY on the src feature — loc has no effect on subjectRank. This captures his direct statement: "erg > abs".

theorem Core.abs_without_src_rank (cr : CaseRelation) (h1 : cr.src = false) (h2 : cr.abs = true) : cr.subjectRank = 1

Absence of src with abs yields rank 1.

def Core.CaseRelation.isSubsetOf (inner outer : CaseRelation) : Bool

Does inner have a subset of outer's features?

Equations

• inner.isSubsetOf outer = ((!inner.abs || outer.abs) && (!inner.src || outer.src) && (!inner.loc || outer.loc))

theorem Core.absSrcLoc_is_top (cr : CaseRelation) : cr.isSubsetOf CaseRelation.absSrcLoc = true

{abs, src, loc} contains every case relation.

theorem Core.neutral_is_bottom (cr : CaseRelation) : CaseRelation.neutral.isSubsetOf cr = true

∅ is contained in every case relation.

def Core.CaseRelation.all : List CaseRelation

All 8 case relations, ordered by subject rank (highest first).

Equations

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

theorem Core.CaseRelation.all_length : all.length = 8

def Core.CaseRelation.inAll (cr : CaseRelation) : Bool

Membership check for decidable enumeration.

Equations

• cr.inAll = Core.CaseRelation.all.any fun (x : Core.CaseRelation) => x == cr

theorem Core.CaseRelation.all_complete (cr : CaseRelation) : cr.inAll = true

Every case relation is in the enumeration.

structure Core.Scenario : Type

A predicate's scenario (@cite{anderson-jm-2006}, Ch. 6): the case relations assigned to its arguments, listed with the subject first (highest subjectRank), then the object.

Eq. 39 shows Anderson's derivations for six English verb types:

• "Bill read the book": [erg, abs] — agent + patient
• "Bill fell to the ground": [abs, loc] — theme + locative goal
• "Bill flew to China": [srcAbs, loc] — self-mover + goal
• "Bill knew the answer": [srcLoc, abs] — experiencer + stimulus
• "Bill ran": [erg] — unergative agent

• relations : List CaseRelation

def Core.instReprScenario.repr : Scenario → Nat → Std.Format

Equations

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

instance Core.instReprScenario : Repr Scenario

Equations

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

def Core.Scenario.arity (s : Scenario) : Nat

Number of arguments in the scenario.

Equations

• s.arity = s.relations.length

def Core.Scenario.subjectRelation (s : Scenario) : Option CaseRelation

Case relation of the subject (highest-ranked argument).

Equations

• s.subjectRelation = s.relations.head?

def Core.Scenario.objectRelation (s : Scenario) : Option CaseRelation

Case relation of the direct object (second argument).

Equations

• s.objectRelation = match s.relations with | head :: cr :: tail => some cr | x => none

def Core.Scenario.transitive : Scenario

"Bill read the book" (eq. 39a): erg + abs. Agent (src) acts on patient (abs). Agent is subject: src > abs.

Equations

• Core.Scenario.transitive = { relations := [Core.CaseRelation.ergative, Core.CaseRelation.absolutive] }

def Core.Scenario.unergative : Scenario

"Bill ran" (unergative): erg alone. Agent only, no patient.

Equations

• Core.Scenario.unergative = { relations := [Core.CaseRelation.ergative] }

def Core.Scenario.unaccusative : Scenario

"Bill fell to the ground" (eq. 39b): abs + loc{goal}. Theme (abs) moves to locative goal. No src, so abs is subject.

Equations

• Core.Scenario.unaccusative = { relations := [Core.CaseRelation.absolutive, Core.CaseRelation.locative] }

def Core.Scenario.selfMoving : Scenario

"Bill flew to China" (eq. 39c): abs,erg + loc{goal}. Self-moving agent (abs+src) travels to goal. Has src → subject.

Equations

• Core.Scenario.selfMoving = { relations := [Core.CaseRelation.srcAbs, Core.CaseRelation.locative] }

def Core.Scenario.experiencer : Scenario

"Bill knew the answer" (eq. 39h): E + abs = erg,loc + abs. Experiencer (src+loc) knows stimulus (abs). Has src → subject.

Equations

• Core.Scenario.experiencer = { relations := [Core.CaseRelation.srcLoc, Core.CaseRelation.absolutive] }

theorem Core.transitive_subject_object : Scenario.transitive.subjectRelation = some CaseRelation.ergative ∧ Scenario.transitive.objectRelation = some CaseRelation.absolutive

Transitive: subject is erg (agent), object is abs (patient).

theorem Core.unergative_subject_only : Scenario.unergative.subjectRelation = some CaseRelation.ergative ∧ Scenario.unergative.objectRelation = none

Unergative: subject is erg, no object.

theorem Core.unaccusative_subject_loc : Scenario.unaccusative.subjectRelation = some CaseRelation.absolutive ∧ Scenario.unaccusative.objectRelation = some CaseRelation.locative

Unaccusative: subject is abs, second argument is loc.

theorem Core.selfMoving_subject : Scenario.selfMoving.subjectRelation = some CaseRelation.srcAbs ∧ Scenario.selfMoving.objectRelation = some CaseRelation.locative

Self-moving: subject is abs+src, second argument is loc.

theorem Core.experiencer_subject_object : Scenario.experiencer.subjectRelation = some CaseRelation.srcLoc ∧ Scenario.experiencer.objectRelation = some CaseRelation.absolutive

Experiencer: subject is src+loc, object is abs.

theorem Core.transitive_subject_outranks_object : CaseRelation.ergative.subjectRank > CaseRelation.absolutive.subjectRank

In a transitive, the subject (erg) outranks the object (abs).

theorem Core.unergative_unaccusative_differ : Scenario.unergative.subjectRelation ≠ Scenario.unaccusative.subjectRelation

Unergative and unaccusative have different subject case relations: unergative = src (agentive), unaccusative = abs (patient-like).

def Core.Case.toCaseRelation : Case → Option CaseRelation

Canonical mapping from Blake's morphological case inventory to Anderson's case-feature bundles (@cite{anderson-jm-2006}, Ch. 6).

NOM and ERG both map to abs+src: subject formation (eq. 40) means all subjects acquire the src feature, so nominative = abs{erg}. ACC and ABS map to abs (goal-absolutive for ACC, plain abs for ABS).

Peripheral spatial cases: ABL → loc (second-order source not tracked), LOC → loc, INST → src (source of force).

Equations

• Core.Case.nom.toCaseRelation = some Core.CaseRelation.srcAbs
• Core.Case.acc.toCaseRelation = some Core.CaseRelation.absolutive
• Core.Case.erg.toCaseRelation = some Core.CaseRelation.srcAbs
• Core.Case.abs.toCaseRelation = some Core.CaseRelation.absolutive
• Core.Case.abl.toCaseRelation = some Core.CaseRelation.locative
• Core.Case.loc.toCaseRelation = some Core.CaseRelation.locative
• Core.Case.inst.toCaseRelation = some Core.CaseRelation.ergative
• x✝.toCaseRelation = none

theorem Core.Case.nom_erg_same_relation : nom.toCaseRelation = erg.toCaseRelation

NOM and ERG map to the same case relation: abs+src.

theorem Core.Case.acc_abs_same_relation : acc.toCaseRelation = abs.toCaseRelation

ACC and ABS map to the same case relation: abs.