Projectivity and its relaxations

A dependency graph is projective when the positions each node 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 node may show.

In this file we define those constraints and prove the inclusions among them that hold on trees. The witnesses separating the constraints are the source papers' own figures, and live in their study files.

Main definitions

• Graph.IsProjective is projectivity: every Graph.dominated set is an interval (Definition 3).
• Graph.IsPlanar is planarity: no two links cross (Definition 4), the Link Grammar notion.
• Graph.Interleave and Graph.IsWellNested are interleaving and well-nestedness (Definition 8).
• Graph.gapDegree counts the discontinuities in a node's projection (Definitions 6–7).

Main results

• 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: the chain projective ⊆ planar ⊆ well-nested on trees.
• Graph.IsPlanar.isProjective_of_isBot: every gap of a planar tree contains the root (Graph.IsPlanar.root_mem_gap), so a planar tree rooted at a sentence boundary is already projective.

References

[KN06] — Mildly non-projective dependency structures, source of the Definition numbers cited above [Kuh13] — Mildly non-projective dependency grammar [Mel88] — Dependency syntax: theory and practice, source of the Link Grammar planarity notion

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.

Equations

• g.IsProjective = ∀ (v : Fin n), (g.dominated 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.

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.dominated v, ∃ b ∈ g.dominated v, ∃ c ∈ g.dominated w, ∃ d ∈ g.dominated 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.

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.

@[instance_reducible]

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

Equations

• DependencyGrammar.instDecidableIsPlanar g = DependencyGrammar.instDecidableIsPlanar._aux_1 g

@[instance_reducible]

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

Equations

• DependencyGrammar.instDecidableInterleave g v w = DependencyGrammar.instDecidableInterleave._aux_1 g v w

@[instance_reducible]

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

Equations

• DependencyGrammar.instDecidableIsWellNested g = DependencyGrammar.instDecidableIsWellNested._aux_1 g

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.

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.dominated 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 trees

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} (hT : g.IsTree) (hP : g.IsProjective) : g.IsPlanar

Every projective tree 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} (hT : g.IsTree) (hPl : g.IsPlanar) : g.IsWellNested

Every planar tree 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} (hT : g.IsTree) (hP : g.IsProjective) : g.IsWellNested

Every projective tree is well-nested, via planarity.