Bresnan, Kaplan, Peters and Zaenen 1982: cross-serial dependencies in Dutch

This file formalizes the argument of [BKPZ82] that Dutch is not strongly context-free. In subordinate clauses like dat Jan Piet Marie zag helpen zwemmen the object NPs and the verbs form two parallel right-branching structures — a VP spine holding the arguments and a V′ cluster holding the verbs — whose depths must match: a verb with no argument at its level violates Completeness, an argument with no verb violates Coherence. The string set of these clauses is weakly context-free (the argument of [Huy76] fails), but no context-free grammar generates exactly the well-formed trees, under any relabelling of its nonterminals: a tall enough derivation tree repeats a nonterminal along the verb cluster, and pumping the cluster yields a licensed tree with more verbs than arguments. The lexical-functional grammar of [KB82] generates the trees through a context-free c-structure grammar filtered by the well-formedness conditions on f-structures, and functional control derives the cross-serial association itself.

Main definitions

• tree k m — the c-structure with k + 1 object NPs and m + 1 verbs; dutch n the matched ones, cStructure the context-free c-structure grammar, weakGrammar the string grammar
• Spine, Spine.Complete, Spine.Coherent — the f-structure spine and LFG's two conditions

Main results

• tree_licensed_cStructure — the c-structure grammar generates every tree k m
• Spine.complete_and_coherent_iff — Completeness and Coherence hold exactly when the objects match the non-final verbs
• yield_dutch_mem_weakGrammar — the matched strings are weakly context-free
• not_strongly_contextFree — no context-free grammar's derivation trees relabel onto the matched trees
• subjOfVerb_eq — the i-th NP is the subject of the i-th verb

References

• [BKPZ82]
• [KB82]
• [Huy76]
• [Eve75]
• [PG82]

inductive BresnanEtAl1982.Word : Type

A leaf is a noun phrase or a verb.

• np : Word
• v : Word

@[instance_reducible]

instance BresnanEtAl1982.instDecidableEqWord : DecidableEq Word

Equations

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

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

Equations

• BresnanEtAl1982.instReprWord.repr BresnanEtAl1982.Word.np prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BresnanEtAl1982.Word.np")).group prec✝
• BresnanEtAl1982.instReprWord.repr BresnanEtAl1982.Word.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BresnanEtAl1982.Word.v")).group prec✝

@[instance_reducible]

instance BresnanEtAl1982.instReprWord : Repr Word

Equations

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

inductive BresnanEtAl1982.Cat : Type

The phrasal categories of the c-structure rules (25).

• S : Cat
• VP : Cat
• vBar : Cat

@[instance_reducible]

instance BresnanEtAl1982.instDecidableEqCat : DecidableEq Cat

Equations

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

@[instance_reducible]

instance BresnanEtAl1982.instReprCat : Repr Cat

Equations

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

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

Equations

• BresnanEtAl1982.instReprCat.repr BresnanEtAl1982.Cat.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BresnanEtAl1982.Cat.S")).group prec✝
• BresnanEtAl1982.instReprCat.repr BresnanEtAl1982.Cat.VP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BresnanEtAl1982.Cat.VP")).group prec✝
• BresnanEtAl1982.instReprCat.repr BresnanEtAl1982.Cat.vBar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BresnanEtAl1982.Cat.vBar")).group prec✝

The trees

def BresnanEtAl1982.cluster : ℕ → RoseTree (Symbol Word Cat)

The verb cluster of m + 1 verbs is the right-branching V′ of (22), by V′ → V (V′).

Equations

• BresnanEtAl1982.cluster 0 = RoseTree.node (Symbol.nonterminal BresnanEtAl1982.Cat.vBar) [RoseTree.leaf (Symbol.terminal BresnanEtAl1982.Word.v)]
• BresnanEtAl1982.cluster m.succ = RoseTree.node (Symbol.nonterminal BresnanEtAl1982.Cat.vBar) [RoseTree.leaf (Symbol.terminal BresnanEtAl1982.Word.v), BresnanEtAl1982.cluster m]

def BresnanEtAl1982.spine : ℕ → RoseTree (Symbol Word Cat)

The embedded VP spine of k + 1 object NPs, by VP → (NP)(VP).

Equations

• BresnanEtAl1982.spine 0 = RoseTree.node (Symbol.nonterminal BresnanEtAl1982.Cat.VP) [RoseTree.leaf (Symbol.terminal BresnanEtAl1982.Word.np)]
• BresnanEtAl1982.spine m.succ = RoseTree.node (Symbol.nonterminal BresnanEtAl1982.Cat.VP) [RoseTree.leaf (Symbol.terminal BresnanEtAl1982.Word.np), BresnanEtAl1982.spine m]

def BresnanEtAl1982.topVP : ℕ → ℕ → RoseTree (Symbol Word Cat)

The VP of (22) has the first object, the spine of the remaining k objects, and the cluster.

Equations

• One or more equations did not get rendered due to their size.
• BresnanEtAl1982.topVP 0 x✝ = RoseTree.node (Symbol.nonterminal BresnanEtAl1982.Cat.VP) [RoseTree.leaf (Symbol.terminal BresnanEtAl1982.Word.np), BresnanEtAl1982.cluster x✝]

def BresnanEtAl1982.tree (k m : ℕ) : RoseTree (Symbol Word Cat)

The c-structure (22) of a clause with a subject, k + 1 object NPs and m + 1 verbs.

Equations

• BresnanEtAl1982.tree k m = RoseTree.node (Symbol.nonterminal BresnanEtAl1982.Cat.S) [RoseTree.leaf (Symbol.terminal BresnanEtAl1982.Word.np), BresnanEtAl1982.topVP k m]

def BresnanEtAl1982.dutch (n : ℕ) : RoseTree (Symbol Word Cat)

The well-formed trees have n + 1 objects and n + 2 verbs, each non-final verb with its object. (1) is dutch 0, (26) is dutch 1, (3) is dutch 2.

Equations

• BresnanEtAl1982.dutch n = BresnanEtAl1982.tree n (n + 1)

@[simp]

theorem BresnanEtAl1982.yield_cluster (m : ℕ) : (cluster m).yield = List.replicate (m + 1) Word.v

@[simp]

theorem BresnanEtAl1982.yield_spine (k : ℕ) : (spine k).yield = List.replicate (k + 1) Word.np

@[simp]

theorem BresnanEtAl1982.yield_topVP (k m : ℕ) : (topVP k m).yield = List.replicate (k + 1) Word.np ++ List.replicate (m + 1) Word.v

@[simp]

theorem BresnanEtAl1982.yield_tree (k m : ℕ) : (tree k m).yield = List.replicate (k + 2) Word.np ++ List.replicate (m + 1) Word.v

theorem BresnanEtAl1982.yield_dutch (n : ℕ) : (dutch n).yield = List.replicate (n + 2) Word.np ++ List.replicate (n + 2) Word.v

@[simp]

theorem BresnanEtAl1982.value_cluster (m : ℕ) : (cluster m).value = Symbol.nonterminal Cat.vBar

@[simp]

theorem BresnanEtAl1982.value_spine (k : ℕ) : (spine k).value = Symbol.nonterminal Cat.VP

@[simp]

theorem BresnanEtAl1982.value_topVP (k m : ℕ) : (topVP k m).value = Symbol.nonterminal Cat.VP

theorem BresnanEtAl1982.one_lt_height_cluster (m : ℕ) : 1 < (cluster m).height

The c-structure grammar

def BresnanEtAl1982.cStructure : ContextFreeGrammar Word

The c-structure grammar (25) has S → NP VP, VP → (NP)(VP)(V′) and V′ → V (V′), with the optional expansions the trees use. It generates every tree k m, matched or not; the f-structure conditions below do the filtering.

Equations

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

theorem BresnanEtAl1982.cluster_licensed (m : ℕ) : RoseTree.Licensed cStructure.Licenses (cluster m)

theorem BresnanEtAl1982.spine_licensed (k : ℕ) : RoseTree.Licensed cStructure.Licenses (spine k)

theorem BresnanEtAl1982.topVP_licensed (k m : ℕ) : RoseTree.Licensed cStructure.Licenses (topVP k m)

theorem BresnanEtAl1982.tree_licensed_cStructure (k m : ℕ) : RoseTree.Licensed cStructure.Licenses (tree k m)

The c-structure grammar generates every tree, whatever its counts of objects and verbs.

The f-structure and its well-formedness

structure BresnanEtAl1982.Spine : Type

In the f-structure spine a c-structure induces under (32) and (35)–(36), the VP branch supplies an OBJ at each depth below objects and the V′ branch a PRED at each depth below verbs, every non-final PRED subcategorizing SUBJ, OBJ and VCOMP and the final one SUBJ alone.

• objects : ℕ
• verbs : ℕ

def BresnanEtAl1982.Spine.ofTree (t : RoseTree (Symbol Word Cat)) : Spine

The spine of a tree records its object NPs (all but the subject) and its verbs.

Equations

• BresnanEtAl1982.Spine.ofTree t = { objects := List.count BresnanEtAl1982.Word.np t.yield - 1, verbs := List.count BresnanEtAl1982.Word.v t.yield }

@[simp]

theorem BresnanEtAl1982.Spine.ofTree_tree (k m : ℕ) : ofTree (tree k m) = { objects := k + 1, verbs := m + 1 }

def BresnanEtAl1982.Spine.HasObj (s : Spine) (i : ℕ) : Prop

The OBJ at depth i has a value.

Equations

• s.HasObj i = (i < s.objects)

def BresnanEtAl1982.Spine.GovernsObj (s : Spine) (i : ℕ) : Prop

The PRED at depth i subcategorizes an OBJ when it exists and is not the final verb.

Equations

• s.GovernsObj i = (i + 1 < s.verbs)

def BresnanEtAl1982.Spine.Complete (s : Spine) : Prop

Completeness requires every subcategorized OBJ to have a value.

Equations

• s.Complete = ∀ (i : ℕ), s.GovernsObj i → s.HasObj i

def BresnanEtAl1982.Spine.Coherent (s : Spine) : Prop

Coherence requires every OBJ present to be subcategorized by the PRED at its depth.

Equations

• s.Coherent = ∀ (i : ℕ), s.HasObj i → s.GovernsObj i

theorem BresnanEtAl1982.Spine.complete_and_coherent_iff (s : Spine) (hv : 1 ≤ s.verbs) : s.Complete ∧ s.Coherent ↔ s.objects + 1 = s.verbs

Completeness and Coherence hold together exactly when the objects match the non-final verbs.

theorem BresnanEtAl1982.dutch_wellFormed (n : ℕ) : (Spine.ofTree (dutch n)).Complete ∧ (Spine.ofTree (dutch n)).Coherent

Every matched tree is well formed; (26) is dutch 1.

theorem BresnanEtAl1982.extra_verb_incomplete : ¬(Spine.ofTree (tree 1 3)).Complete

In (43) dat Jan Piet Marie zag helpen laten zwemmen the extra verb's OBJ has no value.

theorem BresnanEtAl1982.extra_np_incoherent : ¬(Spine.ofTree (tree 2 2)).Coherent

In (46) dat Jan Piet Marie Hans zag helpen zwemmen the extra NP is an OBJ the final verb does not subcategorize.

def BresnanEtAl1982.npOfObj (i : ℕ) : ℕ

The OBJ at depth i is the i + 1-th NP, since the VP spine places one object per level below the subject.

Equations

• BresnanEtAl1982.npOfObj i = i + 1

def BresnanEtAl1982.subjOfVerb : ℕ → ℕ

Under functional control (36), (↑ VCOMP SUBJ) = (↑ OBJ), the subject of the verb at depth i + 1 is the OBJ at depth i, and the clause subject is the subject of the first verb.

Equations

• BresnanEtAl1982.subjOfVerb 0 = 0
• BresnanEtAl1982.subjOfVerb m.succ = BresnanEtAl1982.npOfObj m

theorem BresnanEtAl1982.subjOfVerb_eq (i : ℕ) : subjOfVerb i = i

In the cross-serial association of (1)–(3), the i-th NP is the subject of the i-th verb.

Weak context-freeness

def BresnanEtAl1982.weakGrammar : ContextFreeGrammar Word

This grammar for the strings of the matched trees, in the spirit of (8), has S → NP S V and S → NP V.

Equations

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

theorem BresnanEtAl1982.weakGrammar_derives_center (k : ℕ) : weakGrammar.Derives [Symbol.nonterminal ()] (List.replicate k (Symbol.terminal Word.np) ++ [Symbol.nonterminal ()] ++ List.replicate k (Symbol.terminal Word.v))

theorem BresnanEtAl1982.yield_dutch_mem_weakGrammar (n : ℕ) : (dutch n).yield ∈ weakGrammar.language

The matched strings are weakly context-free, since dutch n yields np^(n+2) v^(n+2).

Strong non-context-freeness

def BresnanEtAl1982.trees (g : ContextFreeGrammar Word) : Set (RoseTree (Symbol Word g.NT))

The derivation trees of g from its start symbol.

Equations

• BresnanEtAl1982.trees g = {t : RoseTree (Symbol BresnanEtAl1982.Word g.NT) | RoseTree.Licensed g.Licenses t ∧ t.value = Symbol.nonterminal g.initial}

def BresnanEtAl1982.path (L : ℕ) : List ℕ

The path from the root down the verb cluster goes into the VP, into the V′, then L steps along the cluster.

Equations

• BresnanEtAl1982.path L = 1 :: 2 :: List.replicate L 1

theorem BresnanEtAl1982.cluster_subtreeAt_replicate (m r : ℕ) : (cluster (m + r)).subtreeAt (List.replicate r 1) = some (cluster m)

theorem BresnanEtAl1982.dutch_subtreeAt_take (n L r : ℕ) (hr : r ≤ L) (hL : L ≤ n + 2) : (dutch (n + 1)).subtreeAt (List.take (r + 2) (path L)) = some (cluster (n + 2 - r))

def BresnanEtAl1982.catAt : ℕ → Cat

The category at depth k along path is S, then VP, then V′ all the way down.

Equations

• BresnanEtAl1982.catAt 0 = BresnanEtAl1982.Cat.S
• BresnanEtAl1982.catAt 1 = BresnanEtAl1982.Cat.VP
• BresnanEtAl1982.catAt n.succ.succ = BresnanEtAl1982.Cat.vBar

theorem BresnanEtAl1982.not_strongly_contextFree (g : ContextFreeGrammar Word) (ℓ : g.NT → Cat) : RoseTree.map (Symbol.mapNonterminal ℓ) '' trees g ≠ Set.range dutch

No context-free grammar generates exactly the well-formed trees, under any relabelling of its nonterminals to the categories S, VP, V′ — so no finite feature decoration helps. A grammar with L rules that generates dutch (L + 1) repeats a nonterminal along the verb cluster, and replacing the lower repeat by the upper one gives a licensed tree of the same root with more verbs than noun phrases, which no dutch n has.