Pullum and Gazdar (1982): Natural Languages and Context-Free Languages

This file formalizes [PG82]'s examination of the published arguments that some natural language is not a context-free stringset, each of which the paper finds formally or empirically invalid. The formal exhibits are grammars. The finite state grammar of §1 generates unbounded long-distance number concord (concordGrammar, concord_unbounded). Grammar (9) generates exactly the nonidentity language (8) that Chomsky's comparative argument took to be beyond context-free power (xyGrammar_language), so the language is context-free (isXY_isContextFree). Grammar (29) generates exactly the Dutch verb-raising verb phrases (24) with as many object names as transitive verbs, which Huybregts's cross-serial dependencies were held to put beyond context-free power (dutchGrammar_language, isVerbPhrase_isContextFree), and the Dutch examples (25) to (31) fall out as predicted (dutch_rows). The empirical refutations are rows: the respectively judgments (18) and (19) contradict the number-matching characterization of English that the argument assumes (respectively_converse), and Mohawk classificatory and possessed incorporation, (39), (40), and (43d), break the stem-matching premise of the Mohawk argument (stem_matching_fails).

Implementation notes

Grammars are mathlib's ContextFreeGrammar, and the language theorems go through derivation trees: soundness by induction on a licensed tree, with what each nonterminal generates spelled out (Generated), and completeness by building the derivation. The Dutch verb phrases are described as the paper does, with the categories of the lexicon (29b) as terminals; the row predictions decide membership by stripping the names and counting the transitive verbs (isVerbPhrase), which is proved equivalent to the description. Finite stateness is the right-linear form of the rules, since mathlib has no bridge from grammars to regular languages. The π argument of §3, the xx-language closure argument of §1, the ditransitive schema (32), and the Mohawk translation of Langendoen's finite state language are not formalized.

References

• [PG82]
• [Huy76]
• [BHS60]

§1: unbounded concord in a finite state language

inductive PullumGazdar1982.Word : Type

The words of the finite state grammar of §1.

• which : Word
• problem : Word
• problems : Word
• did : Word
• your : Word
• professor : Word
• say : Word
• she : Word
• you : Word
• thought : Word
• was : Word
• were : Word
• unsolvable : Word

@[instance_reducible]

instance PullumGazdar1982.instDecidableEqWord : DecidableEq Word

Equations

• PullumGazdar1982.instDecidableEqWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PullumGazdar1982.instReprWord : Repr Word

Equations

• PullumGazdar1982.instReprWord = { reprPrec := PullumGazdar1982.instReprWord.repr }

def PullumGazdar1982.instReprWord.repr : Word → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• PullumGazdar1982.instReprWord.repr PullumGazdar1982.Word.did prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Word.did")).group prec✝
• PullumGazdar1982.instReprWord.repr PullumGazdar1982.Word.say prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Word.say")).group prec✝
• PullumGazdar1982.instReprWord.repr PullumGazdar1982.Word.she prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Word.she")).group prec✝
• PullumGazdar1982.instReprWord.repr PullumGazdar1982.Word.you prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Word.you")).group prec✝
• PullumGazdar1982.instReprWord.repr PullumGazdar1982.Word.was prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Word.was")).group prec✝

inductive PullumGazdar1982.ConcordNT : Type

Its three nonterminals.

• S : ConcordNT
• T : ConcordNT
• U : ConcordNT

@[instance_reducible]

instance PullumGazdar1982.instDecidableEqConcordNT : DecidableEq ConcordNT

Equations

• PullumGazdar1982.instDecidableEqConcordNT x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PullumGazdar1982.instReprConcordNT : Repr ConcordNT

Equations

• PullumGazdar1982.instReprConcordNT = { reprPrec := PullumGazdar1982.instReprConcordNT.repr }

def PullumGazdar1982.instReprConcordNT.repr : ConcordNT → ℕ → Std.Format

Equations

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

def PullumGazdar1982.concordGrammar : ContextFreeGrammar Word

In the finite state grammar of §1 a singular or plural which-phrase selects the chain of she thought and you thought clauses ending in the agreeing verb.

Equations

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

def PullumGazdar1982.IsFiniteState {T : Type u_1} (g : ContextFreeGrammar T) : Prop

In a finite state grammar every rule rewrites to terminals followed by at most one nonterminal.

Equations

• PullumGazdar1982.IsFiniteState g = ∀ r ∈ g.rules, ∀ s ∈ r.output.dropLast, s.terminal?.isSome = true

theorem PullumGazdar1982.concordGrammar_isFiniteState : IsFiniteState concordGrammar

def PullumGazdar1982.chain (ps : List Bool) : List Word

A chain of she thought and you thought clauses.

Equations

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

theorem PullumGazdar1982.concord_unbounded (ps : List Bool) : [Word.which, Word.problems, Word.did, Word.your, Word.professor, Word.say] ++ chain ps ++ [Word.were, Word.unsolvable] ∈ concordGrammar.language ∧ [Word.which, Word.problem, Word.did, Word.your, Word.professor, Word.say] ++ chain ps ++ [Word.was, Word.unsolvable] ∈ concordGrammar.language

Concord holds over an unbounded domain in a finite state language, since for every chain of embedded clauses the plural which-phrase agrees with were and the singular with was.

§2: the nonidentity language (8) and grammar (9)

inductive PullumGazdar1982.Sym : Type

The terminal vocabulary of (8) has the two letters of the differing substrings and the three markers.

• a : Sym
• b : Sym
• alpha : Sym
• beta : Sym
• gamma : Sym

@[instance_reducible]

instance PullumGazdar1982.instDecidableEqSym : DecidableEq Sym

Equations

• PullumGazdar1982.instDecidableEqSym x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def PullumGazdar1982.instReprSym.repr : Sym → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• PullumGazdar1982.instReprSym.repr PullumGazdar1982.Sym.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Sym.a")).group prec✝
• PullumGazdar1982.instReprSym.repr PullumGazdar1982.Sym.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Sym.b")).group prec✝
• PullumGazdar1982.instReprSym.repr PullumGazdar1982.Sym.beta prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Sym.beta")).group prec✝

@[instance_reducible]

instance PullumGazdar1982.instReprSym : Repr Sym

Equations

• PullumGazdar1982.instReprSym = { reprPrec := PullumGazdar1982.instReprSym.repr }

inductive PullumGazdar1982.XYNT : Type

Among the nonterminals of grammar (9), S₁, S₂, A₁, B₁ are the paper's S', S'', A', B'.

• S : XYNT
• S₁ : XYNT
• S₂ : XYNT
• A : XYNT
• B : XYNT
• A₁ : XYNT
• B₁ : XYNT
• C : XYNT
• D : XYNT

@[instance_reducible]

instance PullumGazdar1982.instDecidableEqXYNT : DecidableEq XYNT

Equations

• PullumGazdar1982.instDecidableEqXYNT x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def PullumGazdar1982.instReprXYNT.repr : XYNT → ℕ → Std.Format

Equations

• PullumGazdar1982.instReprXYNT.repr PullumGazdar1982.XYNT.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.XYNT.S")).group prec✝
• PullumGazdar1982.instReprXYNT.repr PullumGazdar1982.XYNT.S₁ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.XYNT.S₁")).group prec✝
• PullumGazdar1982.instReprXYNT.repr PullumGazdar1982.XYNT.S₂ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.XYNT.S₂")).group prec✝
• PullumGazdar1982.instReprXYNT.repr PullumGazdar1982.XYNT.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.XYNT.A")).group prec✝
• PullumGazdar1982.instReprXYNT.repr PullumGazdar1982.XYNT.B prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.XYNT.B")).group prec✝
• PullumGazdar1982.instReprXYNT.repr PullumGazdar1982.XYNT.A₁ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.XYNT.A₁")).group prec✝
• PullumGazdar1982.instReprXYNT.repr PullumGazdar1982.XYNT.B₁ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.XYNT.B₁")).group prec✝
• PullumGazdar1982.instReprXYNT.repr PullumGazdar1982.XYNT.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.XYNT.C")).group prec✝
• PullumGazdar1982.instReprXYNT.repr PullumGazdar1982.XYNT.D prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.XYNT.D")).group prec✝

@[instance_reducible]

instance PullumGazdar1982.instReprXYNT : Repr XYNT

Equations

• PullumGazdar1982.instReprXYNT = { reprPrec := PullumGazdar1982.instReprXYNT.repr }

def PullumGazdar1982.xyGrammar : ContextFreeGrammar Sym

Grammar (9), rules (a) to (i) in order.

Equations

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

def PullumGazdar1982.AB (l : List Sym) : Prop

A string over a and b.

Equations

• PullumGazdar1982.AB l = ∀ c ∈ l, c = PullumGazdar1982.Sym.a ∨ c = PullumGazdar1982.Sym.b

def PullumGazdar1982.IsXY (w : List Sym) : Prop

The language (8) has a central marker between two strings over a and b that differ.

Equations

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

def PullumGazdar1982.Generated : XYNT → List Sym → Prop

Each nonterminal of grammar (9) generates its own strings. S₁ generates a marker between strings of different lengths, S₂ a marker between strings differing at some position, A and B a specified a or b flanked by equally many characters before it and after the marker, and A₁ and B₁ a specified a or b and a tail.

Equations

• One or more equations did not get rendered due to their size.
• PullumGazdar1982.Generated PullumGazdar1982.XYNT.C x✝ = (x✝ = [PullumGazdar1982.Sym.a] ∨ x✝ = [PullumGazdar1982.Sym.b])
• PullumGazdar1982.Generated PullumGazdar1982.XYNT.D x✝ = (x✝ ≠ [] ∧ PullumGazdar1982.AB x✝)
• PullumGazdar1982.Generated PullumGazdar1982.XYNT.A₁ x✝ = ∃ (d : List PullumGazdar1982.Sym), x✝ = PullumGazdar1982.Sym.a :: d ∧ PullumGazdar1982.AB d
• PullumGazdar1982.Generated PullumGazdar1982.XYNT.B₁ x✝ = ∃ (d : List PullumGazdar1982.Sym), x✝ = PullumGazdar1982.Sym.b :: d ∧ PullumGazdar1982.AB d
• PullumGazdar1982.Generated PullumGazdar1982.XYNT.S x✝ = PullumGazdar1982.IsXY x✝

theorem PullumGazdar1982.xy_sound {t : RoseTree (Symbol Sym xyGrammar.NT)} (ht : RoseTree.Licensed xyGrammar.Licenses t) (N : xyGrammar.NT) : t.value = Symbol.nonterminal N → Generated N t.yield

By soundness, a tree of grammar (9) rooted at a nonterminal yields what that nonterminal generates, which at S is a string of (8).

Completeness

theorem PullumGazdar1982.derives_xy {w : List Sym} (hw : IsXY w) : xyGrammar.Derives [Symbol.nonterminal XYNT.S] (List.map Symbol.terminal w)

By completeness, every string of (8) is derived.

theorem PullumGazdar1982.xyGrammar_language : xyGrammar.language = {w : List Sym | IsXY w}

Grammar (9) generates exactly the language (8).

theorem PullumGazdar1982.isXY_isContextFree : Language.IsContextFree {w : List Sym | IsXY w}

The nonidentity language (8) is context-free, against the formal premise of the comparative argument.

§4: respectively

def PullumGazdar1982.Langendoen (r : Datum) : Prop

Langendoen's characterization (17) of English respectively sentences has each verb agree in number with its subject.

Equations

• PullumGazdar1982.Langendoen r = (r.feature? "subjects" = r.feature? "verbs")

@[instance_reducible]

instance PullumGazdar1982.instDecidableLangendoen (r : Datum) : Decidable (Langendoen r)

Equations

• PullumGazdar1982.instDecidableLangendoen r = id inferInstance

theorem PullumGazdar1982.respectively_converse : (Langendoen Examples.ex19a ∧ Examples.ex19a.judgment = Judgment.ungrammatical) ∧ ¬Langendoen Examples.ex19b ∧ Examples.ex19b.judgment = Judgment.acceptable

The judgments in (19) are the exact converse of the characterization.

theorem PullumGazdar1982.respectively_18b : Langendoen Examples.ex18b ∧ Examples.ex18b.judgment = Judgment.ungrammatical

(18b), the one string of (18) the characterization admits, is rejected.

§5: Dutch verb raising and grammar (29)

inductive PullumGazdar1982.Cat : Type

The categories of the lexicon (29b) are names, transitive infinitives, intransitive verbs, transitive and intransitive VP-complement-taking infinitives, and finite transitive and intransitive VP-complement-taking verbs.

• B : Cat
• D : Cat
• E : Cat
• F : Cat
• G : Cat
• H : Cat
• I : Cat

@[instance_reducible]

instance PullumGazdar1982.instDecidableEqCat : DecidableEq Cat

Equations

• PullumGazdar1982.instDecidableEqCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PullumGazdar1982.instReprCat : Repr Cat

Equations

• PullumGazdar1982.instReprCat = { reprPrec := PullumGazdar1982.instReprCat.repr }

def PullumGazdar1982.instReprCat.repr : Cat → ℕ → Std.Format

Equations

• PullumGazdar1982.instReprCat.repr PullumGazdar1982.Cat.B prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Cat.B")).group prec✝
• PullumGazdar1982.instReprCat.repr PullumGazdar1982.Cat.D prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Cat.D")).group prec✝
• PullumGazdar1982.instReprCat.repr PullumGazdar1982.Cat.E prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Cat.E")).group prec✝
• PullumGazdar1982.instReprCat.repr PullumGazdar1982.Cat.F prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Cat.F")).group prec✝
• PullumGazdar1982.instReprCat.repr PullumGazdar1982.Cat.G prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Cat.G")).group prec✝
• PullumGazdar1982.instReprCat.repr PullumGazdar1982.Cat.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Cat.H")).group prec✝
• PullumGazdar1982.instReprCat.repr PullumGazdar1982.Cat.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PullumGazdar1982.Cat.I")).group prec✝

inductive PullumGazdar1982.DutchNT : Type

The nonterminals of grammar (29a) are the verb phrase and its VP complement.

• A : DutchNT
• C : DutchNT

@[instance_reducible]

instance PullumGazdar1982.instDecidableEqDutchNT : DecidableEq DutchNT

Equations

• PullumGazdar1982.instDecidableEqDutchNT x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PullumGazdar1982.instReprDutchNT : Repr DutchNT

Equations

• PullumGazdar1982.instReprDutchNT = { reprPrec := PullumGazdar1982.instReprDutchNT.repr }

def PullumGazdar1982.instReprDutchNT.repr : DutchNT → ℕ → Std.Format

Equations

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

def PullumGazdar1982.dutchGrammar : ContextFreeGrammar Cat

Grammar (29a) has the rules A → B C D | C E and C → B C F | C G | B H | I.

Equations

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

def PullumGazdar1982.Cat.transitive : Cat → Bool

Whether a verb is subcategorized for a direct object.

Equations

• PullumGazdar1982.Cat.D.transitive = true
• PullumGazdar1982.Cat.F.transitive = true
• PullumGazdar1982.Cat.H.transitive = true
• x✝.transitive = false

@[simp]

theorem PullumGazdar1982.Cat.transitive_D : D.transitive = true

@[simp]

theorem PullumGazdar1982.Cat.transitive_E : E.transitive = false

@[simp]

theorem PullumGazdar1982.Cat.transitive_F : F.transitive = true

@[simp]

theorem PullumGazdar1982.Cat.transitive_G : G.transitive = false

@[simp]

theorem PullumGazdar1982.Cat.transitive_H : H.transitive = true

@[simp]

theorem PullumGazdar1982.Cat.transitive_I : I.transitive = false

def PullumGazdar1982.objects (vs : List Cat) : ℕ

The number of direct objects a string of verbs requires.

Equations

• PullumGazdar1982.objects vs = List.countP PullumGazdar1982.Cat.transitive vs

@[simp]

theorem PullumGazdar1982.objects_nil : objects [] = 0

@[simp]

theorem PullumGazdar1982.objects_cons (c : Cat) (w : List Cat) : objects (c :: w) = (if c.transitive = true then 1 else 0) + objects w

@[simp]

theorem PullumGazdar1982.objects_append (v w : List Cat) : objects (v ++ w) = objects v + objects w

def PullumGazdar1982.IsComplement (w : List Cat) : Prop

A VP complement consists of names, a finite VP-complement-taking verb, then nonfinite VP-complement-taking verbs, with one name for each transitive verb.

Equations

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

def PullumGazdar1982.IsVerbPhrase (w : List Cat) : Prop

The verb phrases of (24), as the paper describes them, consist of n names, a finite VP-complement-taking verb, a string of nonfinite VP-complement-taking verbs, and a final transitive or intransitive verb, with one name for each transitive verb.

Equations

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

theorem PullumGazdar1982.dutch_sound {t : RoseTree (Symbol Cat dutchGrammar.NT)} (ht : RoseTree.Licensed dutchGrammar.Licenses t) : (t.value = Symbol.nonterminal DutchNT.C → IsComplement t.yield) ∧ (t.value = Symbol.nonterminal DutchNT.A → IsVerbPhrase t.yield)

By soundness, a tree of grammar (29) rooted at C yields a VP complement and one rooted at A a verb phrase.

theorem PullumGazdar1982.derives_complement (x : List Cat) {n : ℕ} {h : Cat} : h = Cat.H ∨ h = Cat.I → (∀ c ∈ x, c = Cat.F ∨ c = Cat.G) → n = objects (h :: x) → dutchGrammar.Derives [Symbol.nonterminal DutchNT.C] (List.map Symbol.terminal (List.replicate n Cat.B ++ h :: x))

By completeness for C, every VP complement is derived.

theorem PullumGazdar1982.derives_verbPhrase {w : List Cat} (hw : IsVerbPhrase w) : dutchGrammar.Derives [Symbol.nonterminal DutchNT.A] (List.map Symbol.terminal w)

By completeness, every verb phrase is derived.

theorem PullumGazdar1982.dutchGrammar_language : dutchGrammar.language = {w : List Cat | IsVerbPhrase w}

Grammar (29) generates exactly the verb phrases the paper describes.

theorem PullumGazdar1982.isVerbPhrase_isContextFree : Language.IsContextFree {w : List Cat | IsVerbPhrase w}

Cross-serial word order with the right number of names is a context-free stringset.

The examples (25) to (31)

def PullumGazdar1982.isVerbPhrase (w : List Cat) : Bool

IsVerbPhrase is decided by stripping the names, reading the first and last verb, and counting.

Equations

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

theorem PullumGazdar1982.isVerbPhrase_iff (w : List Cat) : isVerbPhrase w = true ↔ IsVerbPhrase w

def PullumGazdar1982.Cat.ofChar? : Char → Option Cat

The category of a letter of a row's categories feature.

Equations

• PullumGazdar1982.Cat.ofChar? 'B' = some PullumGazdar1982.Cat.B
• PullumGazdar1982.Cat.ofChar? 'D' = some PullumGazdar1982.Cat.D
• PullumGazdar1982.Cat.ofChar? 'E' = some PullumGazdar1982.Cat.E
• PullumGazdar1982.Cat.ofChar? 'F' = some PullumGazdar1982.Cat.F
• PullumGazdar1982.Cat.ofChar? 'G' = some PullumGazdar1982.Cat.G
• PullumGazdar1982.Cat.ofChar? 'H' = some PullumGazdar1982.Cat.H
• PullumGazdar1982.Cat.ofChar? 'I' = some PullumGazdar1982.Cat.I
• PullumGazdar1982.Cat.ofChar? x✝ = none

def PullumGazdar1982.categories (r : Datum) : Option (List Cat)

A row's category string.

Equations

• PullumGazdar1982.categories r = (r.feature? "categories").bind fun (s : String) => List.mapM PullumGazdar1982.Cat.ofChar? s.toList

def PullumGazdar1982.Predicted (r : Datum) : Prop

A row is predicted when its grammaticality agrees with whether its category string is a verb phrase of grammar (29).

Equations

• PullumGazdar1982.Predicted r = match PullumGazdar1982.categories r with | some w => r.judgment = Judgment.acceptable ↔ PullumGazdar1982.isVerbPhrase w = true | none => False

@[instance_reducible]

instance PullumGazdar1982.instDecidablePredicted (r : Datum) : Decidable (Predicted r)

Equations

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

theorem PullumGazdar1982.dutch_rows (r : Datum) : r ∈ Examples.all → r.language = "dutc1256" → Predicted r

On (25) to (31), grammar (29) accepts the grammatical clauses and rejects the ungrammatical.

§6: Mohawk noun incorporation

def PullumGazdar1982.StemMatched (r : Datum) : Prop

The stem-matching premise of the Mohawk argument says that the stem incorporated in the verb is the head noun stem of its external argument.

Equations

• PullumGazdar1982.StemMatched r = (r.feature? "incorporated" = r.feature? "external")

@[instance_reducible]

instance PullumGazdar1982.instDecidableStemMatched (r : Datum) : Decidable (StemMatched r)

Equations

• PullumGazdar1982.instDecidableStemMatched r = id inferInstance

theorem PullumGazdar1982.stem_matching_fails (r : Datum) : r ∈ [Examples.ex39, Examples.ex40, Examples.ex43d] → r.judgment = Judgment.acceptable ∧ ¬StemMatched r

Classificatory incorporation (39), (40) and possessed incorporation (43d) are grammatical with mismatched stems.