The Case Filter

[Bak15] [Cho01] [Mar91] [Woo06]

Every DP must receive Case. In Minimalist terms:

• Every DP has [uCase] (unvalued Case feature)
• [uCase] must be valued by Agree with a Case-assigning head
• Failure to value [uCase] causes the derivation to crash

Case assigners (Agree-based):

• T assigns nominative to its specifier (subject)
• v assigns accusative to its complement (object)
• P assigns oblique to its complement

For the competing dependent-case approach, see DependentCase.lean. For inherent/Voice-based case, see Voice.lean and Mam.Agreement.

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)]

structure Minimalist.DPFeatures : Type

A DP's features (with unvalued Case).

• phi : List PhiFeature
• caseFeature : GramFeature

@[implicit_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) }

@[implicit_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 = (caseOf dp).isSome

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.

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.