Anderson (2006): Modern Grammars of Case: A Retrospective

In the localist case grammar of the book's sixth chapter, a semantic relation combines three first-order features, the absolutive, the source and the locative, with second-order features that make its absolutive or its locative a source or a goal. Each feature occupies a cell of a grid of two places, each with a plain member, a source and a goal: the absolutive is the plain nonspatial member, the ergative the nonspatial source, and the locative the plain spatial member. A case form that expresses several relations neutralizes them, leaving as residue the cells they share.

Goal specification makes a place of an argument a goal when a co-argument bears that place's source. Subject formation gives an absolutive that is not a goal a second-order source, and the subject is the argument a hierarchy ranks highest. The book's subjects share no cell, but once formed they share the nonspatial source: unlike French à, subjecthood is a neutralization whose residue a rule supplies.

Main statements

• Relation.IsSubjectOf.hasSourceAt_formSubject: every subject, once formed, bears the nonspatial source.
• residue_subjects_fell, residue_formedSubjects: the book's subjects share no cell, and once formed they share the nonspatial source.
• residue_a: à leaves in common a locative that is not a source.
• rows_subject: the hierarchy selects the subject the book records for each of its examples.

Implementation notes

• The comma of the hierarchy reads "combined with some other relation". The optional comma on the absolutive is left out: the with-phrase of The tank flooded with sewage is a circumstantial.
• The rows record second-order features as the book prints them. The rules and the hierarchy read only the cells, so to them a derived source and an inherent one look alike.
• A subject is any argument of maximal rank, since the hierarchy leaves equatives open.

TODO

• The book prints the objects of Bill read the book, knew and acquired as plain absolutives, though goal specification makes them goals, and it prints the locative goals of fell, flew and acquired without the source that makes them goals, which directional verbs leave unexpressed. Recording those sources needs the verbs' valencies.

References

• [And06b]

inductive Anderson2006b.Feature : Type

The three first-order case features.

• abs : Feature
• src : Feature
• loc : Feature

@[instance_reducible]

instance Anderson2006b.instDecidableEqFeature : DecidableEq Feature

Equations

• Anderson2006b.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Anderson2006b.Place : Type

The two places of the localist analysis.

• nonspatial : Place
• spatial : Place

@[instance_reducible]

instance Anderson2006b.instDecidableEqPlace : DecidableEq Place

Equations

• Anderson2006b.instDecidableEqPlace x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Anderson2006b.instFintypePlace : Fintype Place

Equations

• Anderson2006b.instFintypePlace = { elems := { val := ↑Anderson2006b.Place.enumList, nodup := Anderson2006b.Place.enumList_nodup }, complete := Anderson2006b.instFintypePlace._proof_1 }

inductive Anderson2006b.Direction : Type

The two directions a second-order feature gives a place.

• src : Direction
• goal : Direction

@[instance_reducible]

instance Anderson2006b.instDecidableEqDirection : DecidableEq Direction

Equations

• Anderson2006b.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Anderson2006b.instFintypeDirection : Fintype Direction

Equations

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

@[reducible, inline]

abbrev Anderson2006b.Cell : Type

A cell of the localist grid is a place with a direction, or with none for its plain member.

Equations

• Anderson2006b.Cell = (Anderson2006b.Place × Option Anderson2006b.Direction)

def Anderson2006b.Feature.cell : Feature → Cell

The absolutive is the plain nonspatial member, the ergative the nonspatial source, and the locative the plain spatial member.

Equations

• Anderson2006b.Feature.abs.cell = (Anderson2006b.Place.nonspatial, none)
• Anderson2006b.Feature.src.cell = (Anderson2006b.Place.nonspatial, some Anderson2006b.Direction.src)
• Anderson2006b.Feature.loc.cell = (Anderson2006b.Place.spatial, none)

structure Anderson2006b.Relation : Type

A semantic relation is a combination of first-order features with second-order ones, each a direction at a place.

• features : Finset Feature

  The first-order features.

• second : Finset (Place × Direction)

  The second-order features.

@[instance_reducible]

instance Anderson2006b.instDecidableEqRelation : DecidableEq Relation

Equations

• Anderson2006b.instDecidableEqRelation = Anderson2006b.instDecidableEqRelation.decEq

def Anderson2006b.instDecidableEqRelation.decEq (x✝ x✝¹ : Relation) : Decidable (x✝ = x✝¹)

Equations

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

@[reducible, inline]

abbrev Anderson2006b.Predication : Type

A predication lists the relations its predicator's arguments bear.

Equations

• Anderson2006b.Predication = List Anderson2006b.Relation

@[instance_reducible]

instance Anderson2006b.Relation.instMembershipFeature : Membership Feature Relation

Equations

• Anderson2006b.Relation.instMembershipFeature = { mem := fun (r : Anderson2006b.Relation) (f : Anderson2006b.Feature) => f ∈ r.features }

@[instance_reducible]

instance Anderson2006b.Relation.instDecidableMemFeature (f : Feature) (r : Relation) : Decidable (f ∈ r)

Equations

• Anderson2006b.Relation.instDecidableMemFeature f r = Finset.decidableMem f r.features

@[simp]

theorem Anderson2006b.Relation.mem_features {r : Relation} {f : Feature} : f ∈ r.features ↔ f ∈ r

def Anderson2006b.Relation.cells (r : Relation) : Finset Cell

The cells a relation occupies, first-order and second-order features alike.

Equations

• r.cells = Finset.image Anderson2006b.Feature.cell r.features ∪ Finset.image (Prod.map id some) r.second

def Anderson2006b.Relation.HasSourceAt (r : Relation) (x : Place) : Prop

A relation bears the source of a place.

Equations

• r.HasSourceAt x = ((x, some Anderson2006b.Direction.src) ∈ r.cells)

@[instance_reducible]

instance Anderson2006b.Relation.instDecidableHasSourceAt {r : Relation} (x : Place) : Decidable (r.HasSourceAt x)

Equations

• Anderson2006b.Relation.instDecidableHasSourceAt x = Anderson2006b.Relation.instDecidableHasSourceAt._aux_1 x

@[simp]

theorem Anderson2006b.Relation.nonspatial_none_mem_cells {r : Relation} : (Place.nonspatial, none) ∈ r.cells ↔ Feature.abs ∈ r

Named relations

@[reducible, inline]

abbrev Anderson2006b.Relation.absolutive : Relation

The absolutive, the semantically empty relation.

Equations

• Anderson2006b.Relation.absolutive = { features := {Anderson2006b.Feature.abs} }

@[reducible, inline]

abbrev Anderson2006b.Relation.ergative : Relation

The ergative, a source that is not locative.

Equations

• Anderson2006b.Relation.ergative = { features := {Anderson2006b.Feature.src} }

@[reducible, inline]

abbrev Anderson2006b.Relation.locative : Relation

The simple locative.

Equations

• Anderson2006b.Relation.locative = { features := {Anderson2006b.Feature.loc} }

@[reducible, inline]

abbrev Anderson2006b.Relation.experiencer : Relation

The experiencer, a locative source.

Equations

• Anderson2006b.Relation.experiencer = { features := {Anderson2006b.Feature.src, Anderson2006b.Feature.loc} }

@[reducible, inline]

abbrev Anderson2006b.Relation.contactive : Relation

The contactive, an absolutive locative.

Equations

• Anderson2006b.Relation.contactive = { features := {Anderson2006b.Feature.abs, Anderson2006b.Feature.loc} }

def Anderson2006b.Relation.IsPatient (r : Relation) : Prop

A relation is a patient when it combines the locative with the absolutive or the source.

Equations

• r.IsPatient = (Anderson2006b.Feature.loc ∈ r ∧ (Anderson2006b.Feature.abs ∈ r ∨ Anderson2006b.Feature.src ∈ r))

@[instance_reducible]

instance Anderson2006b.Relation.instDecidablePredIsPatient : DecidablePred IsPatient

Equations

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

theorem Anderson2006b.Relation.isPatient_experiencer : experiencer.IsPatient

theorem Anderson2006b.Relation.isPatient_contactive : contactive.IsPatient

Goals and derived sources

def Anderson2006b.Relation.IsGoalAt (r : Relation) (x : Place) (p : Predication) : Prop

Goal specification makes a place of an argument a goal when the argument bears that place's plain member but not its source, and a co-argument bears its source.

Equations

• r.IsGoalAt x p = ((x, none) ∈ r.cells ∧ ¬r.HasSourceAt x ∧ ∃ s ∈ p, s.HasSourceAt x)

@[instance_reducible]

instance Anderson2006b.Relation.instDecidableIsGoalAt {r : Relation} {p : Predication} (x : Place) : Decidable (r.IsGoalAt x p)

Equations

• Anderson2006b.Relation.instDecidableIsGoalAt x = { decide := decide ((x, none) ∈ r.cells) && decide (¬r.HasSourceAt x ∧ ∃ s ∈ p, s.HasSourceAt x), reflects_decide := ⋯ }

def Anderson2006b.Relation.IsDerivedSourceOf (r : Relation) (p : Predication) : Prop

Subject formation makes an absolutive a source when it bears no nonspatial source and is not a nonspatial goal.

Equations

• r.IsDerivedSourceOf p = (Anderson2006b.Feature.abs ∈ r ∧ ¬r.HasSourceAt Anderson2006b.Place.nonspatial ∧ ¬r.IsGoalAt Anderson2006b.Place.nonspatial p)

@[instance_reducible]

instance Anderson2006b.Relation.instDecidableIsDerivedSourceOf {r : Relation} {p : Predication} : Decidable (r.IsDerivedSourceOf p)

Equations

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

theorem Anderson2006b.Relation.isDerivedSourceOf_iff {r : Relation} {p : Predication} : r.IsDerivedSourceOf p ↔ Feature.abs ∈ r ∧ ¬r.HasSourceAt Place.nonspatial ∧ ∀ s ∈ p, ¬s.HasSourceAt Place.nonspatial

def Anderson2006b.Relation.formSubject (p : Predication) (r : Relation) : Relation

Subject formation gives a derived source a second-order source on its absolutive.

Equations

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

theorem Anderson2006b.Relation.hasSourceAt_formSubject_iff {r : Relation} {p : Predication} : (formSubject p r).HasSourceAt Place.nonspatial ↔ r.HasSourceAt Place.nonspatial ∨ r.IsDerivedSourceOf p

Subject selection

def Anderson2006b.Relation.subjectRank (r : Relation) : ℕ

The rank of a relation on the subject selection hierarchy. A simple ergative outranks a combined one, which outranks any absolutive, and a relation with neither is off the hierarchy.

Equations

• r.subjectRank = if r.HasSourceAt Anderson2006b.Place.nonspatial then if r.cells = Anderson2006b.Relation.ergative.cells then 3 else 2 else if Anderson2006b.Feature.abs ∈ r then 1 else 0

theorem Anderson2006b.Relation.subjectRank_pos_iff {r : Relation} : 0 < r.subjectRank ↔ r.HasSourceAt Place.nonspatial ∨ Feature.abs ∈ r

theorem Anderson2006b.Relation.two_le_subjectRank_iff {r : Relation} : 2 ≤ r.subjectRank ↔ r.HasSourceAt Place.nonspatial

theorem Anderson2006b.Relation.subjectRank_lt_ergative {r : Relation} (h : r.cells ≠ ergative.cells) : r.subjectRank < ergative.subjectRank

def Anderson2006b.Relation.IsSubjectOf (r : Relation) (p : Predication) : Prop

A subject of a predication is an argument of maximal rank on the hierarchy.

Equations

• r.IsSubjectOf p = MaximalFor (fun (s : Anderson2006b.Relation) => s ∈ p ∧ 0 < s.subjectRank) Anderson2006b.Relation.subjectRank r

theorem Anderson2006b.Relation.isSubjectOf_iff {r : Relation} {p : Predication} : r.IsSubjectOf p ↔ r ∈ p ∧ 0 < r.subjectRank ∧ ∀ s ∈ p, s.subjectRank ≤ r.subjectRank

@[instance_reducible]

instance Anderson2006b.Relation.instDecidableIsSubjectOf {r : Relation} {p : Predication} : Decidable (r.IsSubjectOf p)

Equations

• Anderson2006b.Relation.instDecidableIsSubjectOf = decidable_of_iff' (r ∈ p ∧ 0 < r.subjectRank ∧ ∀ s ∈ p, s.subjectRank ≤ r.subjectRank) ⋯

theorem Anderson2006b.Relation.isSubjectOf_iff_isDerivedSourceOf {r : Relation} {p : Predication} (hr : r ∈ p) (hsrc : ¬r.HasSourceAt Place.nonspatial) : r.IsSubjectOf p ↔ r.IsDerivedSourceOf p

An argument with no nonspatial source is the subject exactly when subject formation makes it a source.

theorem Anderson2006b.Relation.IsSubjectOf.hasSourceAt_or_isDerivedSourceOf {r : Relation} {p : Predication} (h : r.IsSubjectOf p) : r.HasSourceAt Place.nonspatial ∨ r.IsDerivedSourceOf p

theorem Anderson2006b.Relation.IsSubjectOf.hasSourceAt_formSubject {r : Relation} {p : Predication} (h : r.IsSubjectOf p) : (formSubject p r).HasSourceAt Place.nonspatial

Every subject, once formed, bears the nonspatial source, inherent or derived.

theorem Anderson2006b.Relation.IsSubjectOf.not_isGoalAt {r : Relation} {p : Predication} (h : r.IsSubjectOf p) : ¬r.IsGoalAt Place.nonspatial p

A subject is never a nonspatial goal.

The book's examples

def Anderson2006b.Relation.labels : List (String × Relation)

The labels the example rows give the relations.

Equations

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

Neutralization

def Anderson2006b.residue (E : Finset Relation) : Finset Cell

The residue of a neutralization is the cells every neutralized relation occupies.

Equations

• Anderson2006b.residue E = E.inf Anderson2006b.Relation.cells

def Anderson2006b.relationsOf? (e : Datum) (key : String) : Option (List Relation)

The relations a row records under a key, if every label names one.

Equations

• Anderson2006b.relationsOf? e key = List.mapM (fun (x : String) => List.lookup x Anderson2006b.Relation.labels) (e.features key)

@[reducible, inline]

abbrev Anderson2006b.Predication.ofRow? (e : Datum) : Option Predication

The predication a row records. Adjuncts are not arguments.

Equations

• Anderson2006b.Predication.ofRow? e = Anderson2006b.relationsOf? e "arg"

def Anderson2006b.subject? (e : Datum) : Option Relation

The subject a row records.

Equations

• Anderson2006b.subject? e = e.parse? "subject" Anderson2006b.Relation.labels

def Anderson2006b.formedSubject? (e : Datum) : Option Relation

The subject a row records, once formed.

Equations

• Anderson2006b.formedSubject? e = do let __do_lift ← Anderson2006b.Predication.ofRow? e let __do_lift_1 ← Anderson2006b.subject? e some (Anderson2006b.Relation.formSubject __do_lift __do_lift_1)

theorem Anderson2006b.rows_subject (e : Datum) : e ∈ Examples.all → e.feature? "subject" ≠ none → ∃ p ∈ Predication.ofRow? e, ∃ r ∈ subject? e, r.IsSubjectOf p ∧ ∀ s ∈ p, s.IsSubjectOf p → s = r

The hierarchy selects the subject the book records for each of its examples, and only that argument.

theorem Anderson2006b.read_object_goal : ∃ p ∈ Predication.ofRow? Examples.ex_39a, ∃ r ∈ p, r.IsGoalAt Place.nonspatial p

The object of Bill read the book is a nonspatial goal, so the accusative signals it.

theorem Anderson2006b.suffered_subject : ∃ p ∈ Predication.ofRow? Examples.ex_34, ∃ r ∈ p, r.IsSubjectOf p ∧ Relation.experiencer.features ⊆ r.features ∧ Relation.contactive.features ⊆ r.features ∧ r.IsGoalAt Place.spatial p

The subject of Phil suffered (from asthma) is at once an experiencer and a contactive, and its locative is a goal because the ablative is a source.

theorem Anderson2006b.residue_a : ∃ E ∈ relationsOf? Examples.ex_3 "neutralized", residue E.toFinset = Relation.locative.cells ∧ ∀ r ∈ E, ¬r.HasSourceAt Place.spatial

À neutralizes spatial goal and simple location, leaving in common a locative that is not a source.

theorem Anderson2006b.residue_subjects : ∃ E ∈ List.mapM subject? [Examples.ex_39a, Examples.ex_39c, Examples.ex_39h, Examples.ex_39i, Examples.ex_39j], residue E.toFinset = Relation.ergative.cells

The subjects of Bill read the book, flew to China, knew the answer, acquired a new shirt and suffered from asthma leave the ergative in common.

theorem Anderson2006b.residue_subjects_fell : ∃ E ∈ List.mapM subject? [Examples.ex_39a, Examples.ex_39b, Examples.ex_39c, Examples.ex_39h, Examples.ex_39i, Examples.ex_39j], residue E.toFinset = ∅

With the subject of Bill fell to the ground, the book's subjects share no cell.

theorem Anderson2006b.residue_formedSubjects : ∃ E ∈ List.mapM formedSubject? [Examples.ex_39a, Examples.ex_39b, Examples.ex_39c, Examples.ex_39h, Examples.ex_39i, Examples.ex_39j], residue E.toFinset = Relation.ergative.cells

Once formed, the book's subjects share the nonspatial source.

theorem Anderson2006b.fell_flew_neutralized : ∃ r ∈ formedSubject? Examples.ex_39b, ∃ s ∈ subject? Examples.ex_39c, r.cells = s.cells ∧ r ≠ s

Subject formation neutralizes agency, since the formed subject of Bill fell to the ground occupies the cells of the subject of Bill flew to China though the two relations differ.