Swiss German Case and Verb Subcategorization @cite{shieber-1985}

Swiss German uses the same four-case inventory as Standard German (NOM, ACC, GEN, DAT). The critical fact for @cite{shieber-1985}'s argument is that different verbs in cross-serial constructions subcategorize for different cases on their NP objects:

• hälfe ("help") requires dative
• lönd ("let") requires accusative
• aastriiche ("paint") requires accusative

This case-verb pairing is what makes Swiss German cross-serial dependencies produce the pattern a^m b^n c^m d^n (DAT-NPs, ACC-NPs, DAT-Vs, ACC-Vs), which is not context-free.

def Fragments.SwissGerman.Case.caseInventory : List Core.Case

Swiss German uses the same 4-case inventory as Standard German.

Equations

• Fragments.SwissGerman.Case.caseInventory = [Core.Case.nom, Core.Case.acc, Core.Case.gen, Core.Case.dat]

inductive Fragments.SwissGerman.Case.CrossSerialVerb : Type

Verbs that participate in cross-serial subordinate clause constructions.

These are the verbs from @cite{shieber-1985}'s Swiss German data. Each subcategorizes for a specific case on its NP object.

• haelfe : CrossSerialVerb

  hälfe "help" — requires dative NP object

• loend : CrossSerialVerb

  lönd "let" — requires accusative NP object

• aastriiche : CrossSerialVerb

  aastriiche "paint" — requires accusative NP object

instance Fragments.SwissGerman.Case.instDecidableEqCrossSerialVerb : DecidableEq CrossSerialVerb

Equations

• Fragments.SwissGerman.Case.instDecidableEqCrossSerialVerb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.SwissGerman.Case.instBEqCrossSerialVerb : BEq CrossSerialVerb

Equations

• Fragments.SwissGerman.Case.instBEqCrossSerialVerb = { beq := Fragments.SwissGerman.Case.instBEqCrossSerialVerb.beq }

def Fragments.SwissGerman.Case.instBEqCrossSerialVerb.beq : CrossSerialVerb → CrossSerialVerb → Bool

Equations

• Fragments.SwissGerman.Case.instBEqCrossSerialVerb.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.SwissGerman.Case.instReprCrossSerialVerb : Repr CrossSerialVerb

Equations

• Fragments.SwissGerman.Case.instReprCrossSerialVerb = { reprPrec := Fragments.SwissGerman.Case.instReprCrossSerialVerb.repr }

def Fragments.SwissGerman.Case.instReprCrossSerialVerb.repr : CrossSerialVerb → Nat → Std.Format

Equations

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

def Fragments.SwissGerman.Case.verbObjectCase : CrossSerialVerb → Core.Case

Case required by each verb on its NP object.

This is the empirical fact that drives @cite{shieber-1985}'s proof: verbs sort into dative-subcategorizing and accusative-subcategorizing classes, and in the cross-serial construction the case on each NP must match the requirement of its corresponding verb.

Equations

• Fragments.SwissGerman.Case.verbObjectCase Fragments.SwissGerman.Case.CrossSerialVerb.haelfe = Core.Case.dat
• Fragments.SwissGerman.Case.verbObjectCase Fragments.SwissGerman.Case.CrossSerialVerb.loend = Core.Case.acc
• Fragments.SwissGerman.Case.verbObjectCase Fragments.SwissGerman.Case.CrossSerialVerb.aastriiche = Core.Case.acc

theorem Fragments.SwissGerman.Case.dat_acc_distinction : verbObjectCase CrossSerialVerb.haelfe ≠ verbObjectCase CrossSerialVerb.loend

The two case classes are genuinely distinct — hälfe requires dative while lönd requires accusative. This non-trivial case distinction is what produces the crossed agreement pattern a^m b^n c^m d^n.

theorem Fragments.SwissGerman.Case.loend_aastriiche_same_class : verbObjectCase CrossSerialVerb.loend = verbObjectCase CrossSerialVerb.aastriiche

lönd and aastriiche belong to the same case class (accusative).