Documentation

Linglib.Studies.AndersonJM2006

Anderson (2006): Modern Grammars of Case [And06b] #

[And06b] "Modern Grammars of Case: A Retrospective" (OUP) develops localist case grammar (LCG), where all semantic relations decompose into combinations of three first-order case features: absolutive (abs), source/ergative (src), and locative (loc).

Anderson's system (Ch. 6, eq. 11) #

The four simple case relations are:

abs (∅): the semantically empty base — holistic participant
source/erg ({src}): first-order source — agent, causer
loc ({loc}): place/location
abl ({loc, src²}): second-order source subordinated to loc

Arguments bear COMBINATIONS of first-order features to define complex roles (§6.2–6.3):

Agent = src alone ("Bill read the book", eq. 39a)
Experiencer = src + loc ("Bill knew the answer", eq. 39h)
Contactive/patient = abs + loc (eq. 22)
Self-mover = abs + src ("Bill flew to China", eq. 39c)

Subject selection (eq. 38') #

Anderson directly states: erg > abs. The argument with first-order source becomes subject. If no argument has source, the absolutive becomes subject. The hierarchy is NOT derived from feature cardinality.

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

Improvement over the two-feature model #

Our earlier formalization incorrectly used only two features (abs, erg) and collapsed experiencer with agent as {abs, erg}. Anderson's actual system DISTINGUISHES them: agent = {src}, experiencer = {src, loc}. Both have src (so both can be subjects), but they differ in the loc feature. The third feature (loc) is essential to Anderson's theory.

Costs #

The three-feature system collapses some Fragment distinctions:

{src} collapses agent, source, instrument, stimulus
{abs} collapses patient and theme But it correctly distinguishes experiencer from agent (unlike the two-feature simplification).

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. Originally landed as standalone substrate in Features/Case/Basic.lean; inlined here because only this study consumes it.

inductive AndersonJM2006.CaseFeature :

Anderson's three first-order case features (Ch. 6).

Instances For

@[implicit_reducible]

instance AndersonJM2006.instDecidableEqCaseFeature :

DecidableEq CaseFeature

Equations

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

def AndersonJM2006.instReprCaseFeature.repr :

CaseFeature → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance AndersonJM2006.instReprCaseFeature :

Repr CaseFeature

Equations

AndersonJM2006.instReprCaseFeature = { reprPrec := AndersonJM2006.instReprCaseFeature.repr }

@[implicit_reducible]

instance AndersonJM2006.instFintypeCaseFeature :

Fintype CaseFeature

Equations

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

@[reducible, inline]

abbrev AndersonJM2006.CaseRelation :

An argument's case specification: a bundle of first-order features (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

AndersonJM2006.CaseRelation = Finset AndersonJM2006.CaseFeature

Instances For

@[reducible]

def AndersonJM2006.CaseRelation.neutral :

Equations

AndersonJM2006.CaseRelation.neutral = ∅

Instances For

@[reducible]

def AndersonJM2006.CaseRelation.absolutive :

Equations

AndersonJM2006.CaseRelation.absolutive = {AndersonJM2006.CaseFeature.abs}

Instances For

@[reducible]

def AndersonJM2006.CaseRelation.ergative :

Equations

AndersonJM2006.CaseRelation.ergative = {AndersonJM2006.CaseFeature.src}

Instances For

@[reducible]

def AndersonJM2006.CaseRelation.locative :

Equations

AndersonJM2006.CaseRelation.locative = {AndersonJM2006.CaseFeature.loc}

Instances For

@[reducible]

def AndersonJM2006.CaseRelation.srcAbs :

Equations

AndersonJM2006.CaseRelation.srcAbs = {AndersonJM2006.CaseFeature.abs, AndersonJM2006.CaseFeature.src}

Instances For

@[reducible]

def AndersonJM2006.CaseRelation.srcLoc :

Equations

AndersonJM2006.CaseRelation.srcLoc = {AndersonJM2006.CaseFeature.src, AndersonJM2006.CaseFeature.loc}

Instances For

@[reducible]

def AndersonJM2006.CaseRelation.absLoc :

Equations

AndersonJM2006.CaseRelation.absLoc = {AndersonJM2006.CaseFeature.abs, AndersonJM2006.CaseFeature.loc}

Instances For

@[reducible]

def AndersonJM2006.CaseRelation.absSrcLoc :

Equations

AndersonJM2006.CaseRelation.absSrcLoc = {AndersonJM2006.CaseFeature.abs, AndersonJM2006.CaseFeature.src, AndersonJM2006.CaseFeature.loc}

Instances For

theorem AndersonJM2006.CaseRelation.absSrcLoc_eq_univ :

absSrcLoc = Finset.univ

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

@[reducible]

def AndersonJM2006.CaseRelation.abs (cr : CaseRelation) :

Convenience accessors for the three features.

Equations

cr.abs = (AndersonJM2006.CaseFeature.abs ∈ cr)

Instances For

@[reducible]

def AndersonJM2006.CaseRelation.src (cr : CaseRelation) :

Equations

cr.src = (AndersonJM2006.CaseFeature.src ∈ cr)

Instances For

@[reducible]

def AndersonJM2006.CaseRelation.loc (cr : CaseRelation) :

Equations

cr.loc = (AndersonJM2006.CaseFeature.loc ∈ cr)

Instances For

def AndersonJM2006.CaseRelation.subjectRank (cr : CaseRelation) :

Fin 3

The subject selection rank (eq. 38'). src (agent) outranks abs (patient) outranks loc (spatial).

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

Equations

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

Instances For

theorem AndersonJM2006.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 AndersonJM2006.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 AndersonJM2006.absSrcLoc_is_top (cr : CaseRelation) :

cr ⊆ CaseRelation.absSrcLoc

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

theorem AndersonJM2006.neutral_is_bottom (cr : CaseRelation) :

CaseRelation.neutral ⊆ cr

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

theorem AndersonJM2006.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 AndersonJM2006.Scenario :

A predicate's scenario (Ch. 6): the case relations assigned to its arguments.

relations : List CaseRelation

Instances For

def AndersonJM2006.Scenario.arity (s : Scenario) :

ℕ

Equations

s.arity = s.relations.length

Instances For

def AndersonJM2006.Scenario.subjectRelation (s : Scenario) :

Option CaseRelation

Equations

s.subjectRelation = s.relations.head?

Instances For

def AndersonJM2006.Scenario.objectRelation (s : Scenario) :

Option CaseRelation

Equations

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

Instances For

def AndersonJM2006.Scenario.transitive :

Equations

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

Instances For

def AndersonJM2006.Scenario.unergative :

Equations

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

Instances For

def AndersonJM2006.Scenario.unaccusative :

Equations

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

Instances For

def AndersonJM2006.Scenario.selfMoving :

Equations

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

Instances For

def AndersonJM2006.Scenario.experiencer :

Equations

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

Instances For

theorem AndersonJM2006.transitive_subject_object :

Scenario.transitive.subjectRelation = some CaseRelation.ergative ∧ Scenario.transitive.objectRelation = some CaseRelation.absolutive

theorem AndersonJM2006.unergative_subject_only :

Scenario.unergative.subjectRelation = some CaseRelation.ergative ∧ Scenario.unergative.objectRelation = none

theorem AndersonJM2006.unaccusative_subject_loc :

Scenario.unaccusative.subjectRelation = some CaseRelation.absolutive ∧ Scenario.unaccusative.objectRelation = some CaseRelation.locative

theorem AndersonJM2006.selfMoving_subject :

Scenario.selfMoving.subjectRelation = some CaseRelation.srcAbs ∧ Scenario.selfMoving.objectRelation = some CaseRelation.locative

theorem AndersonJM2006.experiencer_subject_object :

Scenario.experiencer.subjectRelation = some CaseRelation.srcLoc ∧ Scenario.experiencer.objectRelation = some CaseRelation.absolutive

theorem AndersonJM2006.transitive_subject_outranks_object :

CaseRelation.ergative.subjectRank > CaseRelation.absolutive.subjectRank

theorem AndersonJM2006.unergative_unaccusative_differ :

Scenario.unergative.subjectRelation ≠ Scenario.unaccusative.subjectRelation

Anderson's Case → CaseRelation map lives under namespace Syntax so it can be invoked via dot-notation on c : Case (mirroring how Case.hierarchyRank and the Caha containment defs project onto the type).

def Case.toCaseRelation :

Case → Option AndersonJM2006.CaseRelation

Canonical mapping from Blake's morphological cases to Anderson's case-feature bundles (Ch. 6).

Equations

Instances For

theorem Case.nom_erg_same_relation :

nom.toCaseRelation = erg.toCaseRelation

theorem Case.acc_abs_same_relation :

acc.toCaseRelation = abs.toCaseRelation

def AndersonJM2006.CaseRelation.canonicalTheta (cr : CaseRelation) :

Option ThetaRole

Anderson's canonical mapping from case-feature bundles to theta roles.

The three-feature system makes finer distinctions than the old two-feature version: experiencer ({src, loc}) is now SEPARATE from agent ({src}).

Equations

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

Instances For

def AndersonJM2006.thetaToCaseRelation :

ThetaRole → CaseRelation

Reverse mapping: from the Fragment's 8-role inventory to Anderson's case relations.

Key differences from the old two-feature mapping:

experiencer → srcLoc (was absErg, same as agent)
agent → ergative (was absErg, conflated with experiencer)
goal → locative (spatial goal = loc{goal})

The many-to-one collapses that remain:

agent, source, instrument, stimulus → ergative {src}
patient, theme → absolutive {abs}

Equations

Instances For

Anderson's derivations from Chapter 6 (eq. 39) show how the three-feature system assigns case relations to English verb arguments. For each verb, the subject is the argument with the highest subjectRank.

theorem AndersonJM2006.read_derivation :

have agent := CaseRelation.ergative; have patient := CaseRelation.absolutive; agent.subjectRank > patient.subjectRank

Eq. 39a: "Bill read the book" — erg + abs. Agent (src, rank 2) + patient (abs, rank 1). Agent is subject.

theorem AndersonJM2006.fell_derivation :

have theme := CaseRelation.absolutive; have goal := CaseRelation.locative; theme.subjectRank > goal.subjectRank

Eq. 39b: "Bill fell to the ground" — abs + loc{goal}. Theme (abs, rank 1) + locative goal (loc, rank 0). Theme is subject.

theorem AndersonJM2006.flew_derivation :

have selfMover := CaseRelation.srcAbs; have goal := CaseRelation.locative; selfMover.subjectRank > goal.subjectRank

Eq. 39c: "Bill flew to China" — abs,erg + loc{goal}. Self-mover (abs+src, rank 2) + goal (loc, rank 0). Self-mover is subject.

theorem AndersonJM2006.knew_derivation :

have experiencer := CaseRelation.srcLoc; have stimulus := CaseRelation.absolutive; experiencer.subjectRank > stimulus.subjectRank

Eq. 39h: "Bill knew the answer" — E + abs = erg,loc + abs. Experiencer (src+loc, rank 2) + stimulus (abs, rank 1). Experiencer is subject because it has src.

theorem AndersonJM2006.experiencer_agent_distinct_same_rank :

CaseRelation.srcLoc ≠ CaseRelation.ergative ∧ CaseRelation.srcLoc.subjectRank = CaseRelation.ergative.subjectRank

Anderson's key distinction: experiencer ≠ agent in feature content, but BOTH outrank absolutive. Agent = {src}, experiencer = {src, loc}. The loc feature distinguishes them without affecting subject selection.

def AndersonJM2006.toScenario (v : Verb) :

Derive Anderson's Scenario from a Fragment verb entry's derived roles (Verb.subjectRole/objectRole, the canonical theta-grid).

Equations

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

Instances For

def AndersonJM2006.andersonLinking :

ArgumentStructure.Linking.LinkingTheory Scenario Unit

Anderson's case grammar as a LinkingTheory ([And06b]). The verb type is Scenario, the context is Unit (lexicalist: linking is derived entirely from case-relation rank, no structural input).

Equations

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

Instances For

def AndersonJM2006.andersonPredictedSubjectTheta (v : Verb) :

Option ThetaRole

Anderson's predicted subject theta role for a verb entry.

Equations

AndersonJM2006.andersonPredictedSubjectTheta v = AndersonJM2006.andersonLinking.predict (AndersonJM2006.toScenario v) () ArgumentStructure.Linking.ArgPosition.subject

Instances For

theorem AndersonJM2006.anderson_canonical_linking :

Anderson correctly predicts argument linking for the canonical verb types, including experiencer (which the old two-feature model collapsed with agent).

theorem AndersonJM2006.experiencer_correctly_predicted :

andersonLinking.predict Scenario.experiencer () ArgumentStructure.Linking.ArgPosition.subject = some ThetaRole.experiencer

The three-feature system correctly predicts experiencer as subject, which the old two-feature system collapsed into agent.

theorem AndersonJM2006.anderson_linking_accuracy :

(List.filter (fun (v : English.Predicates.Verbal.VerbEntry) => (andersonPredictedSubjectTheta v.toVerb).isSome == (v.subjectRole.isSome && v.subjectRole != some ThetaRole.goal)) English.Predicates.Verbal.allVerbs).length = English.Predicates.Verbal.allVerbs.length

Anderson's prediction is defined iff the verb's derived subject role maps to a src/abs-bearing case relation. Want-class subjects fall outside that coverage: their [Dow91]-honest profile is bare independent existence ((29e), the desire class template), whose role label goal maps to locative {loc} — a case relation canonicalTheta cannot link to subject. For every other verb, prediction definedness tracks role definedness exactly.

theorem AndersonJM2006.want_outside_anderson_coverage :

English.Predicates.Verbal.want.subjectRole = some ThetaRole.goal ∧ andersonPredictedSubjectTheta English.Predicates.Verbal.want.toVerb = none

The coverage gap is non-vacuous: want has a derived subject role (goal, from the desire-class IE-only profile) but no Anderson subject prediction.

The three-feature system collapses fewer roles than the old two-feature model. Experiencer is now correctly distinguished from agent. The remaining collapses are:

{src} collapses agent with source, instrument, and stimulus
{abs} collapses patient with theme

theorem AndersonJM2006.patient_theme_collapse :

thetaToCaseRelation ThetaRole.patient = thetaToCaseRelation ThetaRole.theme ∧ ThetaRole.patient.canonicalProfile.pPatientScore = 3 ∧ ThetaRole.theme.canonicalProfile.pPatientScore = 1

Patient and theme both map to {abs}, but [Dow91] distinguishes them: patient has 3 P-Patient entailments, theme has only 1.

theorem AndersonJM2006.src_collapses :

thetaToCaseRelation ThetaRole.agent = thetaToCaseRelation ThetaRole.source ∧ thetaToCaseRelation ThetaRole.agent = thetaToCaseRelation ThetaRole.instrument ∧ thetaToCaseRelation ThetaRole.agent = thetaToCaseRelation ThetaRole.stimulus

Agent, source, instrument, and stimulus all map to {src}.

theorem AndersonJM2006.experiencer_distinguished :

thetaToCaseRelation ThetaRole.agent ≠ thetaToCaseRelation ThetaRole.experiencer

The three-feature system correctly separates experiencer from agent. This is the key improvement over the old two-feature formalization.

theorem AndersonJM2006.experiencer_verbs_correct :

(List.filter (fun (v : English.Predicates.Verbal.VerbEntry) => decide ((v.subjectRole == some ThetaRole.experiencer) = true ∧ (andersonPredictedSubjectTheta v.toVerb == some ThetaRole.experiencer) = true)) English.Predicates.Verbal.allVerbs).length = (List.filter (fun (v : English.Predicates.Verbal.VerbEntry) => v.subjectRole == some ThetaRole.experiencer) English.Predicates.Verbal.allVerbs).length

Experiencer subject verbs are now correctly predicted as experiencer, not collapsed into agent (for verbs with entailment profiles).

theorem AndersonJM2006.anderson_blake_concordant :

Case.nom.hierarchyRank ≥ Case.acc.hierarchyRank ∧ CaseRelation.srcAbs.subjectRank > CaseRelation.absolutive.subjectRank ∧ Case.nom.hierarchyRank = Case.acc.hierarchyRank ∧ CaseRelation.srcAbs.subjectRank ≠ CaseRelation.absolutive.subjectRank

Anderson and Blake are concordant on the core case ordering. Blake: NOM(6) ≥ ACC(6). Anderson: NOM/src+abs outranks ACC/abs (subjectRank 2 > 1). Both are inverse to Caha's containment hierarchy.

def AndersonJM2006.HasSpatialLoc :

Does a morphological case carry the spatial locative feature? ABL, LOC both map to {loc} — they share the locative feature because they involve spatial location.

Equations

AndersonJM2006.HasSpatialLoc Case.abl = True
AndersonJM2006.HasSpatialLoc Case.loc = True
AndersonJM2006.HasSpatialLoc x✝ = False

Instances For

@[implicit_reducible]

instance AndersonJM2006.instDecidablePredCaseHasSpatialLoc :

DecidablePred HasSpatialLoc

Equations

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

theorem AndersonJM2006.spatial_cases_are_locative :

Case.abl.toCaseRelation = some CaseRelation.locative ∧ Case.loc.toCaseRelation = some CaseRelation.locative

ABL and LOC both map to Anderson's locative case relation.

theorem AndersonJM2006.inst_is_ergative :

Case.inst.toCaseRelation = some CaseRelation.ergative

INST maps to {src} (source of force), not {loc}. Anderson argues that instrumental is the same semantic relation as agent: both are sources of action.

theorem AndersonJM2006.abl_loc_share_feature :

Case.abl.toCaseRelation = Case.loc.toCaseRelation

ABL and LOC share a case relation AND have an extension path between them. Anderson's explanation: a case marker conditioned on {loc} is polysemous across spatial functions.

theorem AndersonJM2006.alignment_is_labeling :

Case.nom.toCaseRelation = Case.erg.toCaseRelation ∧ Case.acc.toCaseRelation = Case.abs.toCaseRelation ∧ Case.nom.toCaseRelation ≠ Case.acc.toCaseRelation

Accusative and ergative alignment are different morphological labels for the same two case relations: NOM = ERG = src+abs, ACC = ABS = abs. The case relations are identical; alignment is labeling.

theorem AndersonJM2006.anderson_dowty_transitive_agree :

CaseRelation.ergative.canonicalTheta = some ThetaRole.agent ∧ CaseRelation.absolutive.canonicalTheta = some ThetaRole.patient ∧ ThetaRole.agent.canonicalProfile.OutranksForSubject ThetaRole.patient.canonicalProfile

Anderson and Dowty agree on transitive linking despite completely different primitives (features vs entailment profiles).

theorem AndersonJM2006.anderson_dowty_experiencer_agree :

thetaToCaseRelation ThetaRole.agent ≠ thetaToCaseRelation ThetaRole.experiencer ∧ ThetaRole.agent.canonicalProfile.pAgentScore > ThetaRole.experiencer.canonicalProfile.pAgentScore

The three-feature system improves on the old two-feature version for the experiencer case: Anderson distinguishes experiencer from agent (via loc), as does Dowty (different P-Agent entailment count).