Shieber (1985) @cite{shieber-1985}

Evidence against the Context-Freeness of Natural Language. Linguistics and Philosophy, 8(3), 333–343.

Core Argument

@cite{shieber-1985} proves that Swiss German is not weakly context-free, using a purely string-based argument that makes no assumptions about constituent structure or semantics. The proof rests on four empirical claims about Swiss German subordinate clauses, plus the closure of context-free languages under homomorphism and intersection with regular languages.

The Four Claims

1. Swiss German subordinate clauses have structures where all Vs follow all NPs.
2. Among such sentences, those with all DAT-NPs before all ACC-NPs, and all DAT-Vs before all ACC-Vs, are grammatical.
3. The number of DAT-Vs must equal the number of DAT-NPs (and similarly for ACC).
4. An arbitrary number of Vs can occur (subject to performance).

The Proof

Define a homomorphism f mapping Swiss German words to an abstract alphabet:

• DAT-NPs (e.g., em Hans) → a
• ACC-NPs (e.g., d'chind, de Hans) → b
• DAT-Vs (e.g., hälfe) → c
• ACC-Vs (e.g., lönd, aastriiche) → d
• Framing material → w, x, y

Intersect f(L) with the regular language r = w a* b* x c* d* y. By Claims 1–4, f(L) ∩ r = {w aᵐ bⁿ x cᵐ dⁿ y}.

A further homomorphism removing w, x, y yields {aᵐ bⁿ cᵐ dⁿ}, which contains {aⁿ bⁿ cⁿ dⁿ} (setting m = n). Since {aⁿ bⁿ cⁿ dⁿ} is not context-free (anbncndn_not_pumpable), and CFLs are closed under homomorphism and intersection with regular languages, Swiss German is not context-free.

Contrast with @cite{bresnan-etal-1982}

@cite{bresnan-etal-1982}'s earlier argument for Dutch non-context-freeness relied on linguistic assumptions about constituent structure, which @cite{gazdar-pullum-1982} contested. @cite{shieber-1985}'s argument is purely formal — it rests entirely on the string set of Swiss German and the case-marking facts, making no claims about phrase structure.

inductive Phenomena.WordOrder.Studies.Shieber1985.Token : Type

A Swiss German subordinate clause token, abstracting over specific lexical items to their role in the cross-serial construction.

@cite{shieber-1985}'s proof only needs to distinguish NPs and Vs by case.

• datNP : Token

  Dative NP (e.g., em Hans)

• accNP : Token

  Accusative NP (e.g., d'chind, de Hans)

• datV : Token

  Dative-subcategorizing verb (e.g., hälfe "help")

• accV : Token

  Accusative-subcategorizing verb (e.g., lönd "let", aastriiche "paint")

instance Phenomena.WordOrder.Studies.Shieber1985.instDecidableEqToken : DecidableEq Token

Equations

• Phenomena.WordOrder.Studies.Shieber1985.instDecidableEqToken x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.WordOrder.Studies.Shieber1985.instBEqToken.beq : Token → Token → Bool

Equations

• Phenomena.WordOrder.Studies.Shieber1985.instBEqToken.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.WordOrder.Studies.Shieber1985.instBEqToken : BEq Token

Equations

• Phenomena.WordOrder.Studies.Shieber1985.instBEqToken = { beq := Phenomena.WordOrder.Studies.Shieber1985.instBEqToken.beq }

def Phenomena.WordOrder.Studies.Shieber1985.instReprToken.repr : Token → ℕ → Std.Format

Equations

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

instance Phenomena.WordOrder.Studies.Shieber1985.instReprToken : Repr Token

Equations

• Phenomena.WordOrder.Studies.Shieber1985.instReprToken = { reprPrec := Phenomena.WordOrder.Studies.Shieber1985.instReprToken.repr }

def Phenomena.WordOrder.Studies.Shieber1985.Token.caseValue : Token → Core.Case

The case that a token bears or requires.

Equations

• Phenomena.WordOrder.Studies.Shieber1985.Token.datNP.caseValue = Core.Case.dat
• Phenomena.WordOrder.Studies.Shieber1985.Token.accNP.caseValue = Core.Case.acc
• Phenomena.WordOrder.Studies.Shieber1985.Token.datV.caseValue = Core.Case.dat
• Phenomena.WordOrder.Studies.Shieber1985.Token.accV.caseValue = Core.Case.acc

def Phenomena.WordOrder.Studies.Shieber1985.Token.isNP : Token → Bool

Whether a token is an NP (vs a verb).

Equations

• Phenomena.WordOrder.Studies.Shieber1985.Token.datNP.isNP = true
• Phenomena.WordOrder.Studies.Shieber1985.Token.accNP.isNP = true
• Phenomena.WordOrder.Studies.Shieber1985.Token.datV.isNP = false
• Phenomena.WordOrder.Studies.Shieber1985.Token.accV.isNP = false

structure Phenomena.WordOrder.Studies.Shieber1985.CrossSerialClause : Type

A cross-serial clause: a sequence of NPs followed by a sequence of Vs. This encodes Claims 1 and 2.

• datNPs : ℕ
• accNPs : ℕ
• datVs : ℕ
• accVs : ℕ

def Phenomena.WordOrder.Studies.Shieber1985.instDecidableEqCrossSerialClause.decEq (x✝ x✝¹ : CrossSerialClause) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.WordOrder.Studies.Shieber1985.instDecidableEqCrossSerialClause : DecidableEq CrossSerialClause

Equations

• Phenomena.WordOrder.Studies.Shieber1985.instDecidableEqCrossSerialClause = Phenomena.WordOrder.Studies.Shieber1985.instDecidableEqCrossSerialClause.decEq

instance Phenomena.WordOrder.Studies.Shieber1985.instBEqCrossSerialClause : BEq CrossSerialClause

Equations

• Phenomena.WordOrder.Studies.Shieber1985.instBEqCrossSerialClause = { beq := Phenomena.WordOrder.Studies.Shieber1985.instBEqCrossSerialClause.beq }

def Phenomena.WordOrder.Studies.Shieber1985.instBEqCrossSerialClause.beq : CrossSerialClause → CrossSerialClause → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.WordOrder.Studies.Shieber1985.instBEqCrossSerialClause.beq x✝¹ x✝ = false

def Phenomena.WordOrder.Studies.Shieber1985.instReprCrossSerialClause.repr : CrossSerialClause → ℕ → Std.Format

Equations

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

instance Phenomena.WordOrder.Studies.Shieber1985.instReprCrossSerialClause : Repr CrossSerialClause

Equations

• Phenomena.WordOrder.Studies.Shieber1985.instReprCrossSerialClause = { reprPrec := Phenomena.WordOrder.Studies.Shieber1985.instReprCrossSerialClause.repr }

def Phenomena.WordOrder.Studies.Shieber1985.CrossSerialClause.caseMatches (c : CrossSerialClause) : Prop

Claim 3: case matching — the number of dative verbs equals the number of dative NPs, and similarly for accusative.

Equations

• c.caseMatches = (c.datNPs = c.datVs ∧ c.accNPs = c.accVs)

structure Phenomena.WordOrder.Studies.Shieber1985.GrammaticalClauseextends Phenomena.WordOrder.Studies.Shieber1985.CrossSerialClause : Type

A grammatical cross-serial clause satisfies case matching.

• datNPs : ℕ
• accNPs : ℕ
• datVs : ℕ
• accVs : ℕ
• matching : self.caseMatches

def Phenomena.WordOrder.Studies.Shieber1985.arbitraryDepth (m n : ℕ) : GrammaticalClause

Claim 4: any combination of dative and accusative verb counts can occur (we can produce a GrammaticalClause for any m, n).

Equations

• Phenomena.WordOrder.Studies.Shieber1985.arbitraryDepth m n = { datNPs := m, accNPs := n, datVs := m, accVs := n, matching := ⋯ }

def Phenomena.WordOrder.Studies.Shieber1985.tokenToSymbol : Token → FourSymbol

Shieber's homomorphism f: maps Swiss German cross-serial clause tokens to the abstract alphabet {a, b, c, d}.

• DAT-NPs → a
• ACC-NPs → b
• DAT-Vs → c
• ACC-Vs → d

The framing material (Jan säit das mer, es huus haend wele, etc.) maps to fixed delimiter symbols that are removed by regular intersection.

Equations

• Phenomena.WordOrder.Studies.Shieber1985.tokenToSymbol Phenomena.WordOrder.Studies.Shieber1985.Token.datNP = FourSymbol.a
• Phenomena.WordOrder.Studies.Shieber1985.tokenToSymbol Phenomena.WordOrder.Studies.Shieber1985.Token.accNP = FourSymbol.b
• Phenomena.WordOrder.Studies.Shieber1985.tokenToSymbol Phenomena.WordOrder.Studies.Shieber1985.Token.datV = FourSymbol.c
• Phenomena.WordOrder.Studies.Shieber1985.tokenToSymbol Phenomena.WordOrder.Studies.Shieber1985.Token.accV = FourSymbol.d

def Phenomena.WordOrder.Studies.Shieber1985.clauseImage (c : GrammaticalClause) : FourString

The string image of a grammatical clause under the homomorphism.

Equations

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

theorem Phenomena.WordOrder.Studies.Shieber1985.clauseImage_shape (m n : ℕ) : clauseImage (arbitraryDepth m n) = List.replicate m FourSymbol.a ++ List.replicate n FourSymbol.b ++ List.replicate m FourSymbol.c ++ List.replicate n FourSymbol.d

A grammatical clause with m DAT-pairs and n ACC-pairs maps to aᵐ bⁿ cᵐ dⁿ.

theorem Phenomena.WordOrder.Studies.Shieber1985.diagonal_is_anbncndn (n : ℕ) : clauseImage (arbitraryDepth n n) = makeString_anbncndn n

Setting m = n in the clause image gives aⁿbⁿcⁿdⁿ.

theorem Phenomena.WordOrder.Studies.Shieber1985.diagonal_in_language (n : ℕ) : isInLanguage_anbncndn (clauseImage (arbitraryDepth n n)) = true

The diagonal clause images are in {aⁿbⁿcⁿdⁿ}.

def Phenomena.WordOrder.Studies.Shieber1985.cfl_closure_contrapositive : Prop

CFL closure (contrapositive). If a language L can be mapped by a homomorphism f and intersected with a regular language r to produce a non-context-free language, then L is not context-free.

This is the contrapositive of the standard closure theorem for CFLs (Hopcroft & Ullman 1979, pp. 130–135): CFLs are closed under homomorphism and under intersection with regular languages.

We state this as a proposition rather than proving it from first principles, since linglib does not formalize the full theory of CFLs. The pumping lemma proof of the specific non-CFL witness ({aⁿbⁿcⁿdⁿ}) IS fully verified.

Equations

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

theorem Phenomena.WordOrder.Studies.Shieber1985.swiss_german_not_context_free : (∀ (n : ℕ), isInLanguage_anbncndn (clauseImage (arbitraryDepth n n)) = true) ∧ ¬HasPumpingProperty4 isInLanguage_anbncndn

Main result. The image of Swiss German cross-serial clauses under @cite{shieber-1985}'s homomorphism contains {aⁿbⁿcⁿdⁿ}, which is not context-free. Combined with CFL closure properties, this proves Swiss German is not context-free.

The conjunction packages the two independently verified facts:

1. The homomorphism maps Swiss German data to {aⁿbⁿcⁿdⁿ} (by construction)
2. {aⁿbⁿcⁿdⁿ} violates the CFL pumping property (by proof)

theorem Phenomena.WordOrder.Studies.Shieber1985.cross_serial_classification : CrossSerial.crossSerialRequires = Core.FormalLanguageType.mildlyContextSensitive

Cross-serial dependencies with case-marking require at least mildly context-sensitive power — the same classification used by Phenomena.WordOrder.CrossSerial.

theorem Phenomena.WordOrder.Studies.Shieber1985.not_strongly_context_free : CrossSerial.crossSerialRequires ≠ Core.FormalLanguageType.contextFree

Corollary: Swiss German is not strongly context-free either.

@cite{shieber-1985} §3: "As a trivial corollary, Swiss German is not strongly context-free either, regardless of one's view as to the appropriate structures for the language." Since strong context-freeness implies weak context-freeness, weak non-context-freeness implies strong non-context-freeness.

theorem Phenomena.WordOrder.Studies.Shieber1985.haelfe_is_dat : Fragments.SwissGerman.Case.verbObjectCase Fragments.SwissGerman.Case.CrossSerialVerb.haelfe = Token.datV.caseValue

hälfe is a dative verb — its case requirement matches the DAT token.

theorem Phenomena.WordOrder.Studies.Shieber1985.loend_is_acc : Fragments.SwissGerman.Case.verbObjectCase Fragments.SwissGerman.Case.CrossSerialVerb.loend = Token.accV.caseValue

lönd is an accusative verb — its case requirement matches the ACC token.

theorem Phenomena.WordOrder.Studies.Shieber1985.aastriiche_is_acc : Fragments.SwissGerman.Case.verbObjectCase Fragments.SwissGerman.Case.CrossSerialVerb.aastriiche = Token.accV.caseValue

aastriiche is an accusative verb.

theorem Phenomena.WordOrder.Studies.Shieber1985.formal_processing_dissociation : CrossSerial.crossSerialRequires = Core.FormalLanguageType.mildlyContextSensitive ∧ CrossSerial.nestedRequires = Core.FormalLanguageType.contextFree

The formal–processing dissociation: crossed dependencies are formally harder (not CF) but psycholinguistically easier.

@cite{shieber-1985} establishes the formal side; the processing side is in Phenomena.WordOrder.Studies.BachBrownMarslenWilson1986.

def Phenomena.WordOrder.Studies.Shieber1985.example1 : GrammaticalClause

Example (1): mer em Hans es huus hälfed aastriiche "we helped Hans paint the house"

em Hans (DAT) → hälfed (DAT-verb "helped") es huus (ACC) → aastriiche (ACC-verb "paint")

Equations

• Phenomena.WordOrder.Studies.Shieber1985.example1 = Phenomena.WordOrder.Studies.Shieber1985.arbitraryDepth 1 1

def Phenomena.WordOrder.Studies.Shieber1985.example5 : GrammaticalClause

Example (5): triply embedded cross-serial clause mer d'chind em Hans es huus lönd hälfe aastriiche "we let the children help Hans paint the house"

d'chind (ACC) → lönd (ACC-verb "let") em Hans (DAT) → hälfe (DAT-verb "help") es huus (ACC) → aastriiche (ACC-verb "paint")

With case sorting: 1 DAT-NP, 2 ACC-NPs, 1 DAT-V, 2 ACC-Vs

Equations

• Phenomena.WordOrder.Studies.Shieber1985.example5 = Phenomena.WordOrder.Studies.Shieber1985.arbitraryDepth 1 2

theorem Phenomena.WordOrder.Studies.Shieber1985.example5_image : clauseImage example5 = [FourSymbol.a, FourSymbol.b, FourSymbol.b, FourSymbol.c, FourSymbol.d, FourSymbol.d]

The homomorphic image of example (5) is abcdd = a¹b²c¹d².