Shieber (1985): Evidence Against the Context-Freeness of Natural Language

This file proves Shieber's theorem that a language meeting his four claims about Swiss German subordinate clauses is not context-free. The homomorphism f sends the words of the clauses to letters, and the image of the language intersected with the regular language r = w a* b* x c* d* y is w aᵐ bⁿ x cᵐ dⁿ y. Erasing w, x and y leaves aᵐ bⁿ cᵐ dⁿ, which is not context-free, and the context-free languages are closed under homomorphisms and under intersection with regular languages.

Main definitions

• Letter: the letters of the image of f
• caseSorted: the regular language r
• Claims f L: the four claims about a language L whose words f sends to letters

Main results

• Claims.map_inf_caseSorted: the image of the language intersected with r
• Claims.not_isContextFree: a language meeting the claims is not context-free
• not_isContextFree_of_count_le: the same with optional objects, under a one-sided Claim 3
• acceptable_iff_perm: Claim 3 against the paper's clauses (1)–(22)

Implementation notes

The letters put the accusative d'chind and laa before the dative em Hans and hälfe, as the schema of Claim 2 and f do; the prose of Claim 2 puts the datives first. In the data, a verb requires the case of its entry in German.Zurich.Verbs, and a noun phrase bears the case its gloss marks.

TODO

Note 4 restricts Claim 3 to clauses with as many noun phrases as verbs, which does not suffice: the image, with the frame erased, can then be {aᵖ bᵠ cʳ dᵘ | p + q ≠ r + u} ∪ {aᵐ bⁿ cᵐ dⁿ}, the union of the context-free {aᵖ bᵠ cʳ dᵘ | p + q ≠ r + u} and {aᵏ bʲ cᵏ dˡ}. Stating the counterexample needs the closure of the context-free languages under union.

References

• [Shi85]
• [HU79]
• [BHPS61]

The letters and the regular language r

inductive Shieber1985.Letter : Type

Letter is the alphabet of the image of f, its letters declared in the order of r = w a* b* x c* d* y.

• w : Letter

  w is the image of Jan säit das mer 'Jan says that we'.

• a : Letter

  a is the image of the accusative d'chind 'the children'.

• b : Letter

  b is the image of the dative em Hans 'Hans'.

• x : Letter

  x is the image of es huus haend wele 'the house have wanted'.

• c : Letter

  c is the image of laa 'let', which requires an accusative.

• d : Letter

  d is the image of hälfe 'help', which requires a dative.

• y : Letter

  y is the image of aastriiche 'paint'.

• z : Letter

  z is the image of any other word.

@[instance_reducible]

instance Shieber1985.instDecidableEqLetter : DecidableEq Letter

Equations

• Shieber1985.instDecidableEqLetter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Shieber1985.instFintypeLetter : Fintype Letter

Equations

• Shieber1985.instFintypeLetter = { elems := { val := ↑Shieber1985.Letter.enumList, nodup := Shieber1985.Letter.enumList_nodup }, complete := Shieber1985.instFintypeLetter._proof_1 }

def Shieber1985.instReprLetter.repr : Letter → ℕ → Std.Format

Equations

• Shieber1985.instReprLetter.repr Shieber1985.Letter.w prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Shieber1985.Letter.w")).group prec✝
• Shieber1985.instReprLetter.repr Shieber1985.Letter.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Shieber1985.Letter.a")).group prec✝
• Shieber1985.instReprLetter.repr Shieber1985.Letter.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Shieber1985.Letter.b")).group prec✝
• Shieber1985.instReprLetter.repr Shieber1985.Letter.x prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Shieber1985.Letter.x")).group prec✝
• Shieber1985.instReprLetter.repr Shieber1985.Letter.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Shieber1985.Letter.c")).group prec✝
• Shieber1985.instReprLetter.repr Shieber1985.Letter.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Shieber1985.Letter.d")).group prec✝
• Shieber1985.instReprLetter.repr Shieber1985.Letter.y prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Shieber1985.Letter.y")).group prec✝
• Shieber1985.instReprLetter.repr Shieber1985.Letter.z prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Shieber1985.Letter.z")).group prec✝

@[instance_reducible]

instance Shieber1985.instReprLetter : Repr Letter

Equations

• Shieber1985.instReprLetter = { reprPrec := Shieber1985.instReprLetter.repr }

@[instance_reducible]

instance Shieber1985.instLinearOrderLetter : LinearOrder Letter

Equations

• Shieber1985.instLinearOrderLetter = LinearOrder.lift' Shieber1985.Letter.ctorIdx Shieber1985.instLinearOrderLetter._proof_1

def Shieber1985.clause (p q r u : ℕ) : List Letter

clause p q r u is w aᵖ bᵠ x cʳ dᵘ y, the image of the clause with p d'chind, q em Hans, r laa and u hälfe.

Equations

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

def Shieber1985.schema : Language Letter

schema is w (a|b)* x (c|d)* y, the images of the clauses of the schema of Claim 1.

Equations

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

def Shieber1985.caseSorted : Language Letter

caseSorted is the regular language r = w a* b* x c* d* y, the images of the clauses of the schema of Claim 2.

Equations

• Shieber1985.caseSorted = {l : List Shieber1985.Letter | ∃ (p : ℕ) (q : ℕ) (r : ℕ) (u : ℕ), l = Shieber1985.clause p q r u}

def Shieber1985.crossSerial : Language Letter

crossSerial is the language w aᵐ bⁿ x cᵐ dⁿ y.

Equations

• Shieber1985.crossSerial = {l : List Shieber1985.Letter | ∃ (m : ℕ) (n : ℕ), l = Shieber1985.clause m n m n}

theorem Shieber1985.sortedLE_clause (p q r u : ℕ) : (clause p q r u).SortedLE

theorem Shieber1985.count_clause (p q r u : ℕ) (ℓ : Letter) : List.count ℓ (clause p q r u) = match ℓ with | Letter.w => 1 | Letter.x => 1 | Letter.y => 1 | Letter.a => p | Letter.b => q | Letter.c => r | Letter.d => u | Letter.z => 0

theorem Shieber1985.clause_mem_schema (p q r u : ℕ) : clause p q r u ∈ schema

theorem Shieber1985.mem_caseSorted_iff {l : List Letter} : l ∈ caseSorted ↔ l.SortedLE ∧ List.count Letter.w l = 1 ∧ List.count Letter.x l = 1 ∧ List.count Letter.y l = 1 ∧ List.count Letter.z l = 0

A word is in r iff it is sorted with one w, one x, one y and no z, since a sorted word is determined by its letter counts.

theorem Shieber1985.isRegular_caseSorted : caseSorted.IsRegular

The image of note 5

def Shieber1985.eraseFrame : Letter → List Letter

eraseFrame is the homomorphism of note 5, which erases w, x and y; it also erases z, which does not occur in r.

Equations

• Shieber1985.eraseFrame Shieber1985.Letter.a = [Shieber1985.Letter.a]
• Shieber1985.eraseFrame Shieber1985.Letter.b = [Shieber1985.Letter.b]
• Shieber1985.eraseFrame Shieber1985.Letter.c = [Shieber1985.Letter.c]
• Shieber1985.eraseFrame Shieber1985.Letter.d = [Shieber1985.Letter.d]
• Shieber1985.eraseFrame x✝ = []

theorem Shieber1985.flatMap_eraseFrame_clause (p q r u : ℕ) : List.flatMap eraseFrame (clause p q r u) = List.replicate p Letter.a ++ List.replicate q Letter.b ++ List.replicate r Letter.c ++ List.replicate u Letter.d

theorem Shieber1985.stringMap_eraseFrame_crossSerial : (Language.stringMap eraseFrame) crossSerial = Language.ambncmdn Letter.a Letter.b Letter.c Letter.d

theorem Shieber1985.not_isContextFree_crossSerial : ¬crossSerial.IsContextFree

w aᵐ bⁿ x cᵐ dⁿ y is not context-free, since erasing the frame leaves aᵐ bⁿ cᵐ dⁿ.

The claims and the argument

structure Shieber1985.Claims {W : Type u_1} (f : W → Letter) (L : Language W) : Prop

Claims f L states the four claims of §3 about a language L over a vocabulary W whose words f sends to letters.

• exists_mem (m n : ℕ) : ∃ s ∈ L, List.map f s = clause m n m n

  By Claims 1, 2 and 4, some clause w aᵐ bⁿ x cᵐ dⁿ y is grammatical for all m, n.

• count_eq (s : List W) : s ∈ L → List.map f s ∈ schema → List.count Letter.a (List.map f s) = List.count Letter.c (List.map f s) ∧ List.count Letter.b (List.map f s) = List.count Letter.d (List.map f s)

  By Claim 3, a clause of the schema has as many c (laa) as a (d'chind) and as many d (hälfe) as b (em Hans).

theorem Shieber1985.Claims.map_inf_caseSorted {W : Type u_1} {f : W → Letter} {L : Language W} (h : Claims f L) : (Language.map f) L ⊓ caseSorted = crossSerial

The image of a language meeting the claims, intersected with r, is w aᵐ bⁿ x cᵐ dⁿ y.

theorem Shieber1985.Claims.not_isContextFree {W : Type u_1} {f : W → Letter} {L : Language W} (h : Claims f L) : ¬L.IsContextFree

A language meeting the four claims is not context-free.

theorem Shieber1985.not_isContextFree_of_count_le {W : Type u_1} {f : W → Letter} {L : Language W} (hmem : ∀ (n : ℕ), ∃ s ∈ L, List.map f s = clause n n n n) (hle : ∀ s ∈ L, List.map f s ∈ schema → List.count Letter.a (List.map f s) ≤ List.count Letter.c (List.map f s) ∧ List.count Letter.b (List.map f s) ≤ List.count Letter.d (List.map f s)) : ¬L.IsContextFree

A language is not context-free if every clause w aⁿ bⁿ x cⁿ dⁿ y is grammatical and every object noun phrase of a clause of the schema has a verb requiring its case, objects being optional.

The claims are consistent and not idle

def Shieber1985.countMatched : Language Letter

countMatched is the language of the words that meet Claim 3 if they are in the schema.

Equations

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

theorem Shieber1985.claims_countMatched : Claims id countMatched

The claims are consistent, since countMatched meets them.

theorem Shieber1985.not_claims_top : ¬Claims id ⊤

Claim 3 excludes the full language, which is context-free.

The paper's clauses (1)–(22)

def Shieber1985.npCase? (np : String) : Option German.Zurich.Case

npCase? np is the case the article of the noun phrase np marks: a word article followed by its noun, or a clitic article, written with a final apostrophe, attached to it.

Equations

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

def Shieber1985.objectCases (e : Datum) : List German.Zurich.Case

objectCases e lists the cases the articles of the clause e mark on its noun phrases.

Equations

• Shieber1985.objectCases e = List.filterMap (fun (x : String × String) => Shieber1985.npCase? x.1) e.glossedTokens

def Shieber1985.requiredCases (e : Datum) : List German.Zurich.Case

requiredCases e lists the cases the verbs of the clause e require of their objects.

Equations

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

theorem Shieber1985.length_objectCases_eq (e : Datum) : e ∈ Examples.all → (objectCases e).length = (requiredCases e).length

As note 4 observes, every clause of the paper has as many objects as its verbs require.

theorem Shieber1985.acceptable_iff_perm (e : Datum) : e ∈ Examples.all → (e.judgment = Judgment.acceptable ↔ (objectCases e).Perm (requiredCases e))

Among clauses (1)–(22), cross-serial or not, the acceptable ones are exactly those whose objects bear the cases their verbs require, as many of each.