Anderson's Case Features

@cite{anderson-jm-2006}

Three first-order case features [abs, src, loc], the 8 case relations that arise as their feature bundles, the subject-selection hierarchy over those bundles, predicate scenarios (argument-structure tuples of relations), and the morphological-case → relation map.

A CaseRelation is just a Finset CaseFeature — containment, the empty bundle, the full bundle, and meet/join all come from Finset's BooleanAlgebra instance.

inductive Core.CaseFeature : Type

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

• abs : CaseFeature
• src : CaseFeature
• loc : CaseFeature

@[implicit_reducible]

instance Core.instDecidableEqCaseFeature : DecidableEq CaseFeature

Equations

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

def Core.instReprCaseFeature.repr : CaseFeature → ℕ → 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✝

@[implicit_reducible]

instance Core.instReprCaseFeature : Repr CaseFeature

Equations

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

@[implicit_reducible]

instance Core.instFintypeCaseFeature : Fintype CaseFeature

Equations

• Core.instFintypeCaseFeature = { elems := { val := ↑Core.CaseFeature.enumList, nodup := Core.CaseFeature.enumList_nodup }, complete := Core.instFintypeCaseFeature._proof_1 }

@[reducible, inline]

abbrev Core.CaseRelation : Type

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

A CaseRelation is a Finset CaseFeature — the powerset of the three primitive features. The 8 possible bundles are exactly Finset.powerset of Finset.univ. Containment (⊆), the empty bundle (∅), the full bundle (Finset.univ), and meet/join are inherited from Finset's BooleanAlgebra instance.

Equations

• Core.CaseRelation = Finset Core.CaseFeature

@[reducible]

def Core.CaseRelation.neutral : CaseRelation

Equations

• Core.CaseRelation.neutral = ∅

@[reducible]

def Core.CaseRelation.absolutive : CaseRelation

Equations

• Core.CaseRelation.absolutive = {Core.CaseFeature.abs}

@[reducible]

def Core.CaseRelation.ergative : CaseRelation

Equations

• Core.CaseRelation.ergative = {Core.CaseFeature.src}

@[reducible]

def Core.CaseRelation.locative : CaseRelation

Equations

• Core.CaseRelation.locative = {Core.CaseFeature.loc}

@[reducible]

def Core.CaseRelation.srcAbs : CaseRelation

Equations

• Core.CaseRelation.srcAbs = {Core.CaseFeature.abs, Core.CaseFeature.src}

@[reducible]

def Core.CaseRelation.srcLoc : CaseRelation

Equations

• Core.CaseRelation.srcLoc = {Core.CaseFeature.src, Core.CaseFeature.loc}

@[reducible]

def Core.CaseRelation.absLoc : CaseRelation

Equations

• Core.CaseRelation.absLoc = {Core.CaseFeature.abs, Core.CaseFeature.loc}

@[reducible]

def Core.CaseRelation.absSrcLoc : CaseRelation

Equations

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

theorem Core.CaseRelation.absSrcLoc_eq_univ : absSrcLoc = Finset.univ

The full feature set is Finset.univ and equals the 3-feature top.

@[reducible]

def Core.CaseRelation.abs (cr : CaseRelation) : Prop

Convenience accessors for the three features.

Equations

• cr.abs = (Core.CaseFeature.abs ∈ cr)

@[reducible]

def Core.CaseRelation.src (cr : CaseRelation) : Prop

Equations

• cr.src = (Core.CaseFeature.src ∈ cr)

@[reducible]

def Core.CaseRelation.loc (cr : CaseRelation) : Prop

Equations

• cr.loc = (Core.CaseFeature.loc ∈ cr)

def Core.CaseRelation.subjectRank (cr : CaseRelation) : Fin 3

The subject selection rank (@cite{anderson-jm-2006}, eq. 38'). src (agent) outranks abs (patient) outranks loc (spatial).

Codomain Fin 3 — three tiers, type-level boundedness.

Equations

• cr.subjectRank = if Core.CaseFeature.src ∈ cr then 2 else if Core.CaseFeature.abs ∈ cr then 1 else 0

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

The src feature alone determines subject rank 2 — regardless of other features. This is why ergative, experiencer (srcLoc), and self-mover (srcAbs) all tie for highest subject rank.

theorem Core.abs_without_src_rank (cr : CaseRelation) (h1 : CaseFeature.src ∉ cr) (h2 : CaseFeature.abs ∈ cr) : cr.subjectRank = 1

Without src, the abs feature determines rank 1. This is why absolutive and contactive (absLoc) tie at the second tier.

theorem Core.absSrcLoc_is_top (cr : CaseRelation) : cr ⊆ CaseRelation.absSrcLoc

Anderson's absSrcLoc is the top of the feature lattice.

theorem Core.neutral_is_bottom (cr : CaseRelation) : CaseRelation.neutral ⊆ cr

Anderson's neutral (the empty bundle) is the bottom of the feature lattice.

theorem Core.CaseRelation.card_all : Finset.univ.powerset.card = 8

The 8 possible case relations are exactly (Finset.univ : Finset CaseFeature).powerset. Cardinality follows from Finset.card_powerset.

structure Core.Scenario : Type

A predicate's scenario (@cite{anderson-jm-2006}, Ch. 6): the case relations assigned to its arguments.

• relations : List CaseRelation

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

Equations

• s.arity = s.relations.length

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

Equations

• s.subjectRelation = s.relations.head?

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

Equations

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

def Core.Scenario.transitive : Scenario

Equations

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

def Core.Scenario.unergative : Scenario

Equations

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

def Core.Scenario.unaccusative : Scenario

Equations

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

def Core.Scenario.selfMoving : Scenario

Equations

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

def Core.Scenario.experiencer : Scenario

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

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

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

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

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

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

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

def Core.Case.toCaseRelation : Case → Option CaseRelation

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

Equations

• Core.Case.toCaseRelation UD.Case.Nom = some Core.CaseRelation.srcAbs
• Core.Case.toCaseRelation UD.Case.Acc = some Core.CaseRelation.absolutive
• Core.Case.toCaseRelation UD.Case.Erg = some Core.CaseRelation.srcAbs
• Core.Case.toCaseRelation UD.Case.Abs = some Core.CaseRelation.absolutive
• Core.Case.toCaseRelation UD.Case.Abl = some Core.CaseRelation.locative
• Core.Case.toCaseRelation UD.Case.Loc = some Core.CaseRelation.locative
• Core.Case.toCaseRelation UD.Case.Ins = some Core.CaseRelation.ergative
• x✝.toCaseRelation = none

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

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