Projectivity and its relaxations

A dependency graph is projective when the positions each position dominates form a contiguous stretch of the sentence. Natural language is not always projective, so the literature weakens the constraint in several directions: planarity bans crossing arcs, well-nestedness bans interleaved subtrees, and gap degree counts the discontinuities a single position may show.

This file defines those constraints and proves the inclusions among them that hold on forests. The witnesses separating the constraints are the source papers' own figures, and live in their study files.

Main definitions

• Graph.IsProjective: every yield is an interval. Graph.IsArcProjective is its arc form, every arc spanning only positions its head dominates.
• Graph.IsPlanar: no two links cross.
• Graph.Interleave and Graph.IsWellNested: subtrees that interleave, and the ban on interleaving subtrees neither of whose roots dominates the other.
• Graph.gapDegree: the greatest number of discontinuities in the projection of a position.
• Graph.crossings: the number of crossing pairs of links.

Main statements

• Graph.isProjective_iff_gapDegree_eq_zero and Graph.isPlanar_iff_crossings_eq_zero: each binary constraint is the least value of a count.
• Graph.IsProjective.isPlanar and Graph.IsPlanar.isWellNested: on forests, projective graphs are planar and planar graphs are well-nested.
• Graph.IsPlanar.root_mem_gap and Graph.IsPlanar.isProjective_of_isBot: every gap of a planar tree contains the root, so a planar tree rooted at a sentence boundary is projective.

References

• [KN06]
• [Kuh13]
• [Mel88]
• [dMN19]

The binary constraints: projectivity, planarity, well-nestedness

def DependencyGrammar.Graph.IsProjective {n : ℕ} (g : Graph n) : Prop

A dependency graph is projective if the positions dominated by any one position are order-convex ([KN06], Definition 3).

Equations

• g.IsProjective = ∀ (v : Fin n), (g.yield v).OrdConnected

@[reducible, inline]

abbrev DependencyGrammar.Alternate {n : ℕ} (a b c d : Fin n) : Prop

Positions a b c d alternate if a < c < b < d, so that the pairs {a, b} and {c, d} strictly interleave.

Equations

• DependencyGrammar.Alternate a b c d = (a < c ∧ c < b ∧ b < d)

def DependencyGrammar.Graph.IsPlanar {n : ℕ} (g : Graph n) : Prop

A dependency graph is planar if no two links alternate, so that its arcs can be drawn above the sentence without crossing ([KN06], Definition 4).

Equations

• g.IsPlanar = ∀ ⦃a b c d : Fin n⦄, g.Linked a b → g.Linked c d → ¬DependencyGrammar.Alternate a b c d

def DependencyGrammar.Graph.Interleave {n : ℕ} (g : Graph n) (v w : Fin n) : Prop

The subtrees at v and w interleave if each contributes two positions and the two pairs alternate.

Equations

• g.Interleave v w = ∃ a ∈ g.yield v, ∃ b ∈ g.yield v, ∃ c ∈ g.yield w, ∃ d ∈ g.yield w, DependencyGrammar.Alternate a b c d

def DependencyGrammar.Graph.IsWellNested {n : ℕ} (g : Graph n) : Prop

A dependency graph is well-nested if interleaved subtrees are never disjoint, one of the two roots always dominating the other ([KN06], Definition 8).

Equations

• g.IsWellNested = ∀ (v w : Fin n), g.Interleave v w → DependencyGrammar.Dominates g v w ∨ DependencyGrammar.Dominates g w v

theorem DependencyGrammar.Graph.isProjective_iff {n : ℕ} (g : Graph n) : g.IsProjective ↔ ∀ (v x : Fin n), Dominates g v x → ∀ (y : Fin n), Dominates g v y → ∀ (z : Fin n), x ≤ z → z ≤ y → Dominates g v z

Projectivity, unfolded: nothing between two dominated positions escapes.

@[instance_reducible]

instance DependencyGrammar.instDecidableIsProjective {n : ℕ} (g : Graph n) : Decidable g.IsProjective

Equations

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

def DependencyGrammar.Graph.IsArcProjective {n : ℕ} (g : Graph n) : Prop

The arc form of projectivity ([dMN19] §2.4, after Lecerf, Hays, Gaifman and Marcus): every position between the endpoints of an arc is dominated by its head.

Equations

• g.IsArcProjective = ∀ ⦃h d : Fin n⦄, g.Adj h d → ∀ w ∈ Set.uIcc h d, DependencyGrammar.Dominates g h w

theorem DependencyGrammar.Graph.IsArcProjective.dominates_of_mem_uIcc {n : ℕ} {g : Graph n} (hA : g.IsArcProjective) {v x : Fin n} (hx : Dominates g v x) {w : Fin n} (hw : w ∈ Set.uIcc v x) : Dominates g v w

Under the arc form, everything between a position and one it dominates is dominated by it.

theorem DependencyGrammar.Graph.isProjective_iff_isArcProjective {n : ℕ} (g : Graph n) : g.IsProjective ↔ g.IsArcProjective

The two formulations of projectivity agree: every yield is an interval iff every arc spans only positions dominated by its head.

@[instance_reducible]

instance DependencyGrammar.instDecidableIsArcProjective {n : ℕ} (g : Graph n) : Decidable g.IsArcProjective

Equations

• DependencyGrammar.instDecidableIsArcProjective g = decidable_of_iff g.IsProjective ⋯

@[instance_reducible]

instance DependencyGrammar.instDecidableIsPlanar {n : ℕ} (g : Graph n) : Decidable g.IsPlanar

Equations

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

@[instance_reducible]

instance DependencyGrammar.instDecidableInterleave {n : ℕ} (g : Graph n) (v w : Fin n) : Decidable (g.Interleave v w)

Equations

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

@[instance_reducible]

instance DependencyGrammar.instDecidableIsWellNested {n : ℕ} (g : Graph n) : Decidable g.IsWellNested

Equations

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

Gap degree

theorem DependencyGrammar.Graph.projection_pairwise_lt {n : ℕ} (g : Graph n) (v : Fin n) : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) (g.projection v)

The projection is strictly increasing.

def DependencyGrammar.Graph.gapDegreeAt {n : ℕ} (g : Graph n) (v : Fin n) : ℕ

The gap degree of a position counts the discontinuities in its projection, the adjacent members more than one position apart ([KN06], Definition 6).

Equations

• g.gapDegreeAt v = List.countP (fun (p : Fin n × Fin n) => decide (1 < ↑p.2 - ↑p.1)) ((g.projection v).zip (g.projection v).tail)

def DependencyGrammar.Graph.gapDegree {n : ℕ} (g : Graph n) : ℕ

The gap degree of a graph is the maximum over its positions.

Equations

• g.gapDegree = Finset.univ.sup g.gapDegreeAt

Crossings

def DependencyGrammar.Graph.crossings {n : ℕ} (g : Graph n) : ℕ

The number of crossing link pairs, counted as quadruples a < c < b < d carrying links {a, b} and {c, d}. Each crossing pair contributes once, since of the two ways to order the pairs only one alternates.

Equations

• g.crossings = {x : Fin n × Fin n × Fin n × Fin n | g.Linked x.1 x.2.1 ∧ g.Linked x.2.2.1 x.2.2.2 ∧ DependencyGrammar.Alternate x.1 x.2.1 x.2.2.1 x.2.2.2}.card

Projectivity as gap degree zero

theorem DependencyGrammar.Graph.isPlanar_iff_crossings_eq_zero {n : ℕ} {g : Graph n} : g.IsPlanar ↔ g.crossings = 0

Planarity is having no crossings — the binary constraint as the least value of the count.

theorem DependencyGrammar.Graph.gapDegreeAt_eq_zero_iff {n : ℕ} {g : Graph n} {v : Fin n} : g.gapDegreeAt v = 0 ↔ (g.yield v).OrdConnected

A position has gap degree zero exactly when what it dominates is order-convex.

theorem DependencyGrammar.Graph.isProjective_iff_gapDegree_eq_zero {n : ℕ} {g : Graph n} : g.IsProjective ↔ g.gapDegree = 0

Projectivity is gap degree zero: the parametric constraint at its least value is the binary one.

The hierarchy on forests

theorem DependencyGrammar.Graph.IsProjective.dominates_of_mem_uIcc {n : ℕ} {g : Graph n} (hP : g.IsProjective) {p t x : Fin n} (h : g.Adj p t) (hx : x ∈ Set.uIcc p t) : Dominates g p x

In a projective graph the head of an arc dominates every position the arc spans, since the head dominates both endpoints and is order-convex.

theorem DependencyGrammar.Graph.IsProjective.isPlanar {n : ℕ} {g : Graph n} (hF : g.IsForest) (hP : g.IsProjective) : g.IsPlanar

Every projective forest is planar.

theorem DependencyGrammar.Graph.IsPlanar.mem_uIcc_of_linked {n : ℕ} {g : Graph n} (hPl : g.IsPlanar) {lo hi p q : Fin n} (hL : g.Linked lo hi) (hL' : g.Linked p q) (hlp : lo < p) (hph : p < hi) : q ∈ Set.uIcc lo hi

In a planar graph, a link with one endpoint strictly inside the span of another link has its other endpoint inside that span too.

theorem DependencyGrammar.Graph.IsPlanar.no_strict_straddle {n : ℕ} {g : Graph n} (hPl : g.IsPlanar) {p q p' q' : Fin n} (hL : g.Linked p q) (hL' : g.Linked p' q') (hin : p' ∈ Set.uIcc p q) (hne1 : p' ≠ p) (hne2 : p' ≠ q) (hout : q' ∉ Set.uIcc p q) : False

Planarity forbids a link with one endpoint strictly inside another link's span and the other endpoint outside it.

theorem DependencyGrammar.Graph.IsPlanar.isWellNested {n : ℕ} {g : Graph n} (hF : g.IsForest) (hPl : g.IsPlanar) : g.IsWellNested

Every planar forest is well-nested: interleaved subtrees would force a link below one of them to straddle a link below the other.

theorem DependencyGrammar.Graph.IsPlanar.root_mem_gap {n : ℕ} {g : Graph n} (hT : g.IsTree) (hPl : g.IsPlanar) {v i j k : Fin n} (hi : Dominates g v i) (hj : Dominates g v j) (hik : i < k) (hkj : k < j) (hk : ¬Dominates g v k) : i < g.root ∧ g.root < j

In a planar tree every gap contains the root: if v dominates i and j but skips a position between them, the root lies strictly between i and j. So a planar tree rooted at a sentence boundary is projective, which is why planarity buys nothing once the root is given a boundary position.

theorem DependencyGrammar.Graph.IsPlanar.isProjective_of_isBot {n : ℕ} {g : Graph n} (hT : g.IsTree) (hPl : g.IsPlanar) (hr : IsBot g.root) : g.IsProjective

A planar tree whose root precedes every position is projective: a gap would have to contain the root, and nothing lies to its left.

theorem DependencyGrammar.Graph.IsProjective.isWellNested {n : ℕ} {g : Graph n} (hF : g.IsForest) (hP : g.IsProjective) : g.IsWellNested

Every projective forest is well-nested, via planarity.