Verb Cluster Bindings

Framework-agnostic type for verb cluster NP-verb binding patterns.

A verb cluster binding σ : Equiv.Perm (Fin n) maps each NP position (0-indexed) to the surface position of the verb it binds to. The two canonical patterns:

• Cross-serial (Dutch): σ = identity — NP₁→V₁, NP₂→V₂, ...
• Nested (German): σ = reverse — NP₁→Vₙ, NP₂→Vₙ₋₁, ...

The key structural property: two arcs (i, n+σ(i)) and (j, n+σ(j)) with i < j cross iff σ(i) < σ(j). Cross-serial (identity) has all concordant pairs → maximally non-projective. Nested (reverse) has all discordant pairs → fully projective.

Using Equiv.Perm (Mathlib) gives bijectivity by construction, DecidableEq, and group structure. Projectivity is characterized as Antitone σ.

@[reducible, inline]

abbrev Features.VerbClusterBinding (n : ℕ) : Type

Verb cluster binding: a permutation on n verb positions. σ i gives the surface position (among verbs) of the verb that NP_i binds to.

Equations

• Features.VerbClusterBinding n = Equiv.Perm (Fin n)

@[reducible, inline]

abbrev Features.VerbClusterBinding.identity (n : ℕ) : VerbClusterBinding n

Cross-serial binding: NP_i → V_i (identity permutation, Dutch pattern).

Equations

• Features.VerbClusterBinding.identity n = Equiv.refl (Fin n)

def Features.VerbClusterBinding.reverse (n : ℕ) : VerbClusterBinding n

Nested binding: NP_i → V_{n−1−i} (reversal permutation, German pattern). Self-inverse: reversing twice is the identity.

Equations

• Features.VerbClusterBinding.reverse n = { toFun := fun (i : Fin n) => ⟨n - 1 - ↑i, ⋯⟩, invFun := fun (i : Fin n) => ⟨n - 1 - ↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def Features.VerbClusterBinding.toList {n : ℕ} (σ : VerbClusterBinding n) : List ℕ

Convert a binding to a list of verb positions for display.

Equations

• σ.toList = List.map (fun (i : ℕ) => if hi : i < n then ↑(σ ⟨i, hi⟩) else 0) (List.range n)

@[implicit_reducible]

instance Features.VerbClusterBinding.instRepr {n : ℕ} : Repr (VerbClusterBinding n)

Equations

• Features.VerbClusterBinding.instRepr = { reprPrec := fun (σ : Features.VerbClusterBinding n) (x : ℕ) => repr σ.toList }

def Features.VerbClusterBinding.isProjective {n : ℕ} (σ : VerbClusterBinding n) : Bool

A binding is projective iff no two arcs cross (no concordant pairs). Projective = nested (German), non-projective = cross-serial (Dutch).

Equations

• σ.isProjective = !Features.VerbClusterBinding.hasCrossing✝ σ

theorem Features.VerbClusterBinding.isProjective_iff_antitone {n : ℕ} {σ : VerbClusterBinding n} : σ.isProjective = true ↔ Antitone ⇑σ

def Features.VerbClusterBinding.integratedCount {n : ℕ} (σ : VerbClusterBinding n) (k : ℕ) : ℕ

Count of NPs matrix-integrated after k verbs heard.

NP_i is matrix-integrated iff all verbs in the control chain from V_{σ(i)} to the matrix verb V_{σ(0)} have been heard. Since verbs are heard in surface order (position 0 first), and the control chain passes through surface positions min(σ(0), σ(i))..max(σ(0), σ(i)), NP_i is integrated iff max(σ(0), σ(i)) < k.

• Identity (σ(0) = 0): max(0, i) < k → i < k → min(k, n)
• Reverse (σ(0) = n−1): max(n−1, ·) = n−1 < k → k ≥ n → if k ≥ n then n else 0

Equations

• σ_2.integratedCount k = 0
• σ_2.integratedCount k = List.countP (fun (i : ℕ) => if hi : i < m + 1 then decide ((↑(σ_2 ⟨0, ⋯⟩)).max ↑(σ_2 ⟨i, hi⟩) < k) else false) (List.range (m + 1))

def Features.VerbClusterBinding.unintegratedCount {n : ℕ} (σ : VerbClusterBinding n) (k : ℕ) : ℕ

NPs awaiting matrix-connected integration after k verbs.

Equations

• σ.unintegratedCount k = n - σ.integratedCount k

def Features.VerbClusterBinding.npVerbDist (n : ℕ) (σ : VerbClusterBinding n) (i : Fin n) : ℕ

Absolute NP-verb distance. NP_i is at position i, V_{σ(i)} is at position n + σ(i). Distance = n + σ(i) − i.

Equations

• Features.VerbClusterBinding.npVerbDist n σ i = n + ↑(σ i) - ↑i

theorem Features.VerbClusterBinding.identity_not_projective {n : ℕ} (hn : n ≥ 2) : (identity n).isProjective = false

Cross-serial (identity) binding is non-projective for n ≥ 2.

theorem Features.VerbClusterBinding.reverse_is_projective {n : ℕ} : (reverse n).isProjective = true

Nested (reverse) binding is projective: no concordant pairs. For all i < j, σ(i) = n−1−i > n−1−j = σ(j), so all pairs are discordant. Equivalently, reverse is antitone.

theorem Features.VerbClusterBinding.identity_integratedCount {n : ℕ} (k : ℕ) : (identity n).integratedCount k = min k n

Identity integration count: min(k, n) NPs integrated after k verbs.

theorem Features.VerbClusterBinding.reverse_integratedCount {n : ℕ} (k : ℕ) : (reverse n).integratedCount k = if k ≥ n then n else 0

Reverse integration count: 0 until all verbs heard, then n.

theorem Features.VerbClusterBinding.identity_unintegratedCount {n : ℕ} (k : ℕ) : (identity n).unintegratedCount k = n - min k n

theorem Features.VerbClusterBinding.reverse_unintegratedCount {n : ℕ} (k : ℕ) : (reverse n).unintegratedCount k = if k ≥ n then 0 else n

inductive Features.BindingPattern : Type

Classification of binding patterns, derived from the binding. Replaces the old DependencyPattern enum — now computed, not stored.

• crossSerial : BindingPattern
• nested : BindingPattern
• other : BindingPattern

@[implicit_reducible]

instance Features.instDecidableEqBindingPattern : DecidableEq BindingPattern

Equations

• Features.instDecidableEqBindingPattern x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprBindingPattern.repr : BindingPattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprBindingPattern : Repr BindingPattern

Equations

• Features.instReprBindingPattern = { reprPrec := Features.instReprBindingPattern.repr }

def Features.VerbClusterBinding.pattern {n : ℕ} (σ : VerbClusterBinding n) : BindingPattern

Classify a binding as cross-serial, nested, or other. Uses DecidableEq (Equiv.Perm (Fin n)) for direct equality checks.

Equations

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