VP Divergence: DG vs PSG Constituency

@cite{osborne-2019} @cite{osborne-gross-2012}

Formalizes the central empirical disagreement between Dependency Grammar and Phrase Structure Grammar regarding the finite VP (@cite{osborne-2019}, Ch. 2–4; Osborne, Putnam & Groß 2012, Syntax 15:4).

The core claim: In DG, the finite VP (verb + complements, excluding subject) is a catena but not a constituent. In PSG, the finite VP is a constituent. Constituency tests (topicalization, clefting, pseudoclefting, proform substitution, answer fragments) systematically fail to identify the finite VP as a constituent — supporting DG's prediction.

Key Results

• strict_containment_*: For any non-trivial tree, constituents ⊊ catenae
• exists_catena_not_constituent: Universal witness — singleton of internal node
• vp_is_catena_* / vp_not_constituent_*: The finite VP divergence
• dg_predictions_match_observed: DG matches ≥4/5 constituency tests
• psg_predictions_mismatch: PSG matches ≤2/5 constituency tests

Bridges

• → Catena.lean: reuses isCatena, isConstituent, catenaeCount, constituentCount
• → Core/Basic.lean: uses DepTree, Dependency, Word
• → DependencyLength.lean: VP catena dep length

def DepGrammar.VPDivergence.isStrictSubset (n : ℕ) (deps : List Dependency) : Bool

Check that constituent count is strictly less than catena count.

Equations

• DepGrammar.VPDivergence.isStrictSubset n deps = decide (DepGrammar.Catena.constituentCount n deps < DepGrammar.Catena.catenaeCount n deps)

def DepGrammar.VPDivergence.nonConstituentCatenae (n : ℕ) (deps : List Dependency) : List (List ℕ)

Enumerate all catenae that are NOT constituents.

Equations

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

theorem DepGrammar.VPDivergence.strict_containment_tree9 : Catena.constituentCount 4 Catena.tree9 < Catena.catenaeCount 4 Catena.tree9

Strict containment for tree (9): constituents < catenae. (4 constituents < 10 catenae, @cite{osborne-gross-2012}, p. 359)

theorem DepGrammar.VPDivergence.strict_containment_chain4 : Catena.constituentCount 4 Catena.chain4 < Catena.catenaeCount 4 Catena.chain4

Strict containment for chain4: constituents < catenae. (4 constituents < 10 catenae)

theorem DepGrammar.VPDivergence.strict_containment_star4 : Catena.constituentCount 4 Catena.star4 < Catena.catenaeCount 4 Catena.star4

Strict containment for star4: constituents < catenae. (4 constituents < 11 catenae)

theorem DepGrammar.VPDivergence.tree9_non_constituent_catenae_count : (nonConstituentCatenae 4 Catena.tree9).length = 6

Tree (9) has exactly 6 non-constituent catenae.

theorem DepGrammar.VPDivergence.exists_catena_not_constituent (deps : List Dependency) (v w : ℕ) (hvw : v ≠ w) (hedge : ∃ d ∈ deps, d.headIdx = v ∧ d.depIdx = w) : Catena.isCatena deps [v] = true ∧ ¬projection deps v = [v]

Universal witness for strict containment:

For any tree with ≥2 nodes and an edge (v, w), the singleton {v} is a catena (trivially connected: any singleton is connected in the dep graph) but NOT a constituent ({v} ≠ projection(v) because projection(v) includes w as a descendant).

Uses the computable isCatena (from Catena.lean) rather than the Prop-level IsCatena which takes a SimpleGraph parameter unrelated to the dependency list. The two key facts:

1. isCatena deps [v] = true — any singleton is a catena
2. projection deps v ≠ [v] — v has a child w, so projection is strictly larger

inductive DepGrammar.VPDivergence.PSTree : Type

A minimal phrase structure tree for structural comparisons with DG. NOT intended to replace Minimalism's SyntacticObject/XBarPhrase (those carry theory-specific features). This is purely for the DG-vs-PSG constituency comparison.

• leaf (word : String) (cat : UD.UPOS) : PSTree
• node (label : String) (children : List PSTree) : PSTree

partial def DepGrammar.VPDivergence.instReprPSTree.repr : PSTree → ℕ → Std.Format

instance DepGrammar.VPDivergence.instReprPSTree : Repr PSTree

Equations

• DepGrammar.VPDivergence.instReprPSTree = { reprPrec := DepGrammar.VPDivergence.instReprPSTree.repr }

@[irreducible]

def DepGrammar.VPDivergence.PSTree.words : PSTree → List String

Yield of a PSTree: the leaf words in left-to-right order.

Equations

• (DepGrammar.VPDivergence.PSTree.leaf a a_1).words = [a]
• (DepGrammar.VPDivergence.PSTree.node a a_1).words = List.flatMap DepGrammar.VPDivergence.PSTree.words a_1

@[irreducible]

def DepGrammar.VPDivergence.PSTree.constituents : PSTree → List (List String)

All constituents of a PSTree: every subtree's yield is a constituent.

Equations

• (DepGrammar.VPDivergence.PSTree.leaf a a_1).constituents = [[a]]
• (DepGrammar.VPDivergence.PSTree.node a a_1).constituents = List.flatMap DepGrammar.VPDivergence.PSTree.words a_1 :: List.flatMap DepGrammar.VPDivergence.PSTree.constituents a_1

def DepGrammar.VPDivergence.PSTree.constituentCount (t : PSTree) : ℕ

Count of distinct constituents in a PSTree.

Equations

• t.constituentCount = t.constituents.length

def DepGrammar.VPDivergence.PSTree.hasConstituent (t : PSTree) (ws : List String) : Bool

Check whether a given word sequence is a constituent of this PSTree.

Equations

• t.hasConstituent ws = t.constituents.any fun (x : List String) => x == ws

"Bill plays chess" (@cite{osborne-2019}, p. 92, example 24)

DG analysis:

    plays(0)
   / \
Bill(1) chess(2)

• 3 DG constituents: {Bill}, {chess}, {Bill, plays, chess}
• 6 catenae: {Bill}, {plays}, {chess}, {Bill,plays}, {plays,chess}, {Bill,plays,chess}
• The finite VP {plays, chess} is a catena but not a constituent

PSG analysis:

       S
      / \
   Bill VP
         / \
      plays chess

• 5 PS constituents: {Bill}, {plays}, {chess}, {plays, chess}, {Bill, plays, chess}
• The finite VP {plays, chess} IS a constituent

def DepGrammar.VPDivergence.billPlaysChess_dg : DepTree

DG tree for "Bill plays chess": plays(0) → Bill(1), plays(0) → chess(2).

Equations

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

def DepGrammar.VPDivergence.billPlaysChess_psg : PSTree

PSG tree for "Bill plays chess".

Equations

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

"She reads everything" (@cite{osborne-2019}, p. 46, example 12)

DG: reads(0) → she(1), reads(0) → everything(2). {reads, everything} is catena not constituent.

PSG: [S she [VP reads everything]]. {reads, everything} IS a constituent.

def DepGrammar.VPDivergence.sheReadsEverything_dg : DepTree

DG tree for "She reads everything".

Equations

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

def DepGrammar.VPDivergence.sheReadsEverything_psg : PSTree

PSG tree for "She reads everything".

Equations

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

"They will get the teacher a present" (@cite{osborne-2019}, p. 95–97, ex. 30–34)

DG analysis — flat tree from will:

        will(0)
      / | \ \ \
They(1) get(2) teacher(3) present(4) the(5)
                                      |
                                      a(6)

Actually, following UD conventions more carefully:

• will(0) is AUX but heads in UD (aux relation goes dep→head)
• get(1) → will(0) via aux
• Let's use: get as root, will as aux dependent

Simplified DG (UD-style): get(0) → They(1), get(0) → will(2), get(0) → teacher(3), get(0) → present(4), teacher(3) → the(5), present(4) → a(6)

{get, teacher, present} is catena but not constituent.

PSG analysis — deeply layered:

         S
       / \
    They VP
           / \
         will VP
              / \
           get VP
                 / \
           the teacher NP
                       / \
                      a present

Multiple constituents DG doesn't recognize.

def DepGrammar.VPDivergence.theyWillGet_dg : DepTree

DG tree for "They will get the teacher a present" (UD-style).

Equations

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

def DepGrammar.VPDivergence.theyWillGet_psg : PSTree

PSG tree for "They will get the teacher a present".

Equations

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

theorem DepGrammar.VPDivergence.vp_is_catena_billPlaysChess : Catena.isCatena billPlaysChess_dg.deps [0, 2] = true

The finite VP {plays, chess} is a catena in DG.

theorem DepGrammar.VPDivergence.vp_not_constituent_billPlaysChess : Catena.isConstituent billPlaysChess_dg.deps 3 [0, 2] = false

The finite VP {plays, chess} is NOT a constituent in DG. (subtree of plays = {plays, Bill, chess} = whole sentence)

theorem DepGrammar.VPDivergence.vp_is_constituent_psg_billPlaysChess : billPlaysChess_psg.hasConstituent ["plays", "chess"] = true

The finite VP {plays, chess} IS a constituent in PSG.

theorem DepGrammar.VPDivergence.dg_fewer_constituents_billPlaysChess : Catena.constituentCount 3 billPlaysChess_dg.deps < billPlaysChess_psg.constituentCount

DG has 3 constituents, PSG has 5 — DG has fewer.

theorem DepGrammar.VPDivergence.billPlaysChess_dg_constituents : Catena.constituentCount 3 billPlaysChess_dg.deps = 3

"Bill plays chess": exactly 3 DG constituents.

theorem DepGrammar.VPDivergence.billPlaysChess_dg_catenae : Catena.catenaeCount 3 billPlaysChess_dg.deps = 6

"Bill plays chess": exactly 6 catenae.

theorem DepGrammar.VPDivergence.billPlaysChess_psg_constituents : billPlaysChess_psg.constituentCount = 5

"Bill plays chess": exactly 5 PSG constituents.

theorem DepGrammar.VPDivergence.vp_is_catena_sheReadsEverything : Catena.isCatena sheReadsEverything_dg.deps [0, 2] = true

The finite VP {reads, everything} is a catena in DG.

theorem DepGrammar.VPDivergence.vp_not_constituent_sheReadsEverything : Catena.isConstituent sheReadsEverything_dg.deps 3 [0, 2] = false

The finite VP {reads, everything} is NOT a constituent in DG.

theorem DepGrammar.VPDivergence.vp_is_constituent_psg_sheReadsEverything : sheReadsEverything_psg.hasConstituent ["reads", "everything"] = true

The finite VP {reads, everything} IS a constituent in PSG.

theorem DepGrammar.VPDivergence.vp_catena_theyWillGet : Catena.isCatena theyWillGet_dg.deps [0, 3, 4] = true

{get, teacher, present} is a catena in the DG tree.

theorem DepGrammar.VPDivergence.vp_not_constituent_theyWillGet : Catena.isConstituent theyWillGet_dg.deps 7 [0, 3, 4] = false

{get, teacher, present} is NOT a constituent in DG.

theorem DepGrammar.VPDivergence.full_vp_catena_theyWillGet : Catena.isCatena theyWillGet_dg.deps [0, 3, 4, 5, 6] = true

{get, the, teacher, a, present} is a catena in DG.

theorem DepGrammar.VPDivergence.full_vp_not_constituent_theyWillGet : Catena.isConstituent theyWillGet_dg.deps 7 [0, 3, 4, 5, 6] = false

{get, the, teacher, a, present} is NOT a constituent in DG (subtree of get = whole sentence).

inductive DepGrammar.VPDivergence.ConstituencyTest : Type

The five standard constituency tests (@cite{osborne-2019}, p. 92, ex. 25).

• topicalization : ConstituencyTest
• clefting : ConstituencyTest
• pseudoclefting : ConstituencyTest
• proformSub : ConstituencyTest
• answerFragment : ConstituencyTest

def DepGrammar.VPDivergence.instReprConstituencyTest.repr : ConstituencyTest → ℕ → Std.Format

Equations

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

instance DepGrammar.VPDivergence.instReprConstituencyTest : Repr ConstituencyTest

Equations

• DepGrammar.VPDivergence.instReprConstituencyTest = { reprPrec := DepGrammar.VPDivergence.instReprConstituencyTest.repr }

instance DepGrammar.VPDivergence.instDecidableEqConstituencyTest : DecidableEq ConstituencyTest

Equations

• DepGrammar.VPDivergence.instDecidableEqConstituencyTest x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DepGrammar.VPDivergence.instBEqConstituencyTest : BEq ConstituencyTest

Equations

• DepGrammar.VPDivergence.instBEqConstituencyTest = { beq := DepGrammar.VPDivergence.instBEqConstituencyTest.beq }

def DepGrammar.VPDivergence.instBEqConstituencyTest.beq : ConstituencyTest → ConstituencyTest → Bool

Equations

• DepGrammar.VPDivergence.instBEqConstituencyTest.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure DepGrammar.VPDivergence.TestResult : Type

A constituency test result recording DG vs PSG predictions vs observation.

• test : ConstituencyTest
• dgPredicts : Bool
• psgPredicts : Bool
• observed : Bool

def DepGrammar.VPDivergence.instReprTestResult.repr : TestResult → ℕ → Std.Format

Equations

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

instance DepGrammar.VPDivergence.instReprTestResult : Repr TestResult

Equations

• DepGrammar.VPDivergence.instReprTestResult = { reprPrec := DepGrammar.VPDivergence.instReprTestResult.repr }

instance DepGrammar.VPDivergence.instBEqTestResult : BEq TestResult

Equations

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

def DepGrammar.VPDivergence.finiteVPTests : List TestResult

Constituency test results for the finite VP "plays chess" (@cite{osborne-2019}, p. 92, example 25):

• Topicalization: *"...and plays chess Bill" → FAIL
• Clefting: *"It is plays chess that Bill does" → FAIL
• Pseudoclefting: ?"What Bill does is plays chess" → FAIL (infinitival preferred)
• Proform sub (do so): "Bill does so" → PASS (but do-so matches non-constituents too, §3.5)
• Answer fragment: *"?Plays chess" → FAIL (bare infinitive "Play chess" preferred)

DG predicts: FAIL on all 5 (finite VP is not a constituent) PSG predicts: PASS on all 5 (finite VP is a constituent)

Equations

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

theorem DepGrammar.VPDivergence.dg_predictions_match_observed : (List.filter (fun (t : TestResult) => t.dgPredicts == t.observed) finiteVPTests).length ≥ 4

DG predictions match observed results on 4 of 5 tests (only proform substitution is a mismatch — DG predicts fail, observed pass; but proform sub is known to be unreliable for finite VP, see §3.5).

theorem DepGrammar.VPDivergence.psg_predictions_mismatch : (List.filter (fun (t : TestResult) => t.psgPredicts == t.observed) finiteVPTests).length ≤ 2

PSG predictions match observed results on only 1 of 5 tests. PSG predicts all 5 pass (it's a constituent), but only proform sub passes.

theorem DepGrammar.VPDivergence.psg_matches_exactly_one : (List.filter (fun (t : TestResult) => t.psgPredicts == t.observed) finiteVPTests).length = 1

PSG matches exactly 1 out of 5 tests.

theorem DepGrammar.VPDivergence.dg_matches_exactly_four : (List.filter (fun (t : TestResult) => t.dgPredicts == t.observed) finiteVPTests).length = 4

DG matches exactly 4 out of 5 tests.

theorem DepGrammar.VPDivergence.dg_constituent_count_eq_words_billPlaysChess : Catena.constituentCount 3 billPlaysChess_dg.deps = 3

DG always has exactly n constituents for an n-word tree (one per node's complete subtree). Verified for "Bill plays chess" (3 words, 3 constituents).

theorem DepGrammar.VPDivergence.dg_constituent_count_eq_words_sheReads : Catena.constituentCount 3 sheReadsEverything_dg.deps = 3

"She reads everything": also 3 constituents for 3 words.

theorem DepGrammar.VPDivergence.billPlaysChess_dg_ratio : Catena.catenaRatio 3 billPlaysChess_dg.deps = (6, 1)

Constituent ratio comparison: DG 3:4 vs PSG 5:2 for "Bill plays chess" (out of 7 total non-empty subsets of 3 words).

theorem DepGrammar.VPDivergence.dg_fewer_constituents_sheReads : Catena.constituentCount 3 sheReadsEverything_dg.deps < sheReadsEverything_psg.constituentCount

DG produces strictly fewer constituents than PSG for every example sentence.

theorem DepGrammar.VPDivergence.vp_catena_dep_length_billPlaysChess : Catena.catenaTotalDepLength billPlaysChess_dg.deps [0, 2] = 2

The VP catena {plays, chess} has dependency length 2 (bridge to DependencyLength.lean).

theorem DepGrammar.VPDivergence.full_sentence_dep_length_billPlaysChess : Catena.catenaTotalDepLength billPlaysChess_dg.deps [0, 1, 2] = 3

The full sentence constituent has dependency length 3.

theorem DepGrammar.VPDivergence.constituent_is_catena_billPlaysChess : ((Catena.allNonEmptySubsets 3).all fun (nodes : List ℕ) => if Catena.isConstituent billPlaysChess_dg.deps 3 nodes = true then Catena.isCatena billPlaysChess_dg.deps nodes else true) = true

Every constituent is a catena — verified exhaustively for "Bill plays chess". (Bridge to Catena.lean's constituent_is_catena theorems)

theorem DepGrammar.VPDivergence.isomorphic_divergence : Catena.isCatena sheReadsEverything_dg.deps [0, 2] = true ∧ Catena.isConstituent sheReadsEverything_dg.deps 3 [0, 2] = false ∧ sheReadsEverything_psg.hasConstituent ["reads", "everything"] = true

The finite VP divergence is robust: it holds for the isomorphic "She reads everything" tree as well. Same structure → same divergence.