Case in the Minimalist feature system

This file gives the Agree-based account of structural case its feature-level form: T, v and P carry a valued Case feature they assign to the closest DP ([chomsky-2001]), a DP carries [uCase] until some head values it, and the Case Filter is the convergence condition that no DP reach the interfaces unvalued.

DPFeatures is the DP-side bundle — φ-features plus one Case feature, valued or not — and satisfiesCaseFilter is the predicate on it. The configural alternative, on which case is read off the arrangement of nominals rather than assigned by a head, is Syntax/Case/Dependent.lean ([marantz-1991], [baker-2015]).

Main definitions

• DPFeatures: a DP's φ-features together with its Case feature.
• satisfiesCaseFilter, caseFilterHolds: the Case Filter on one DP and on a derivation's DPs.
• tAssignsNominative, vAssignsAccusative, dpNeedsCase: the assigner and goal feature bundles.

References

• [chomsky-2001]
• [woolford-2006]

Assigner feature bundles

def Minimalist.tAssignsNominative : FeatureBundle

Nominative Case is assigned by T. T has [uCase:nom], assigns to closest DP in Spec-TP.

Equations

• Minimalist.tAssignsNominative = Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.case Case.nom)]

def Minimalist.vAssignsAccusative : FeatureBundle

Accusative Case is assigned by v (transitive light verb). v has [uCase:acc], assigns to closest DP (object).

Equations

• Minimalist.vAssignsAccusative = Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.case Case.acc)]

def Minimalist.dpNeedsCase : FeatureBundle

DP needs Case (Case Filter). All DPs have [uCase], must be valued by Agree. The .dat value here is a placeholder — featuresMatch ignores values for unvalued probes, so any Case would work; .dat is conventional.

Equations

• Minimalist.dpNeedsCase = Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.case Case.dat)]

DP feature structures

structure Minimalist.DPFeatures : Type

A DP's features (with unvalued Case).

• phi : List PhiFeature
• caseFeature : GramFeature

@[instance_reducible]

instance Minimalist.instReprDPFeatures : Repr DPFeatures

Equations

• Minimalist.instReprDPFeatures = { reprPrec := Minimalist.instReprDPFeatures.repr }

def Minimalist.instReprDPFeatures.repr : DPFeatures → ℕ → Std.Format

Equations

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

def Minimalist.DPFeatures.withUnvaluedCase (phi : List PhiFeature) : DPFeatures

Create DP features with unvalued Case. The .dat value is a placeholder — see dpNeedsCase for the rationale.

Equations

• Minimalist.DPFeatures.withUnvaluedCase phi = { phi := phi, caseFeature := Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.case Case.dat) }

def Minimalist.DPFeatures.withCase (phi : List PhiFeature) (c : Case) : DPFeatures

Create DP features with valued Case.

Equations

• Minimalist.DPFeatures.withCase phi c = { phi := phi, caseFeature := Minimalist.GramFeature.valued (Minimalist.FeatureVal.case c) }

@[instance_reducible]

instance Minimalist.instHasCaseDPFeatures : HasCase DPFeatures

A DP bears the case its valued Case feature carries; an unvalued Case feature (or a degenerate non-Case feature in the slot) is caseless.

Equations

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

def Minimalist.satisfiesCaseFilter (dp : DPFeatures) : Bool

Does a DP satisfy the Case Filter? — it bears a case (HasCase.caseOf is some).

Equations

• Minimalist.satisfiesCaseFilter dp = Option.isSome (caseOf dp)

def Minimalist.DPFeatures.toBundle (dp : DPFeatures) : FeatureBundle

Convert DPFeatures to a FeatureBundle.

Equations

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

The Case Filter

def Minimalist.caseFilterHolds (dps : List DPFeatures) : Bool

The Case Filter: a derivation converges only if all DPs have valued Case. This is stated as: for all DPs in the structure, their Case feature must be valued.

Equations

• Minimalist.caseFilterHolds dps = dps.all Minimalist.satisfiesCaseFilter

theorem Minimalist.case_filter_necessary (dps : List DPFeatures) : caseFilterHolds dps = false → ∃ dp ∈ dps, satisfiesCaseFilter dp = false

If Case Filter fails, there exists a DP without Case.

theorem Minimalist.case_filter_at_interfaces (dps : List DPFeatures) (hWF : caseFilterHolds dps = true) (dp : DPFeatures) : dp ∈ dps → satisfiesCaseFilter dp = true

A well-formed derivation satisfies the Case Filter.