Catenae

A catena is a word or a combination of words that is connected in the undirected view of a dependency graph. Every constituent, the dominance cone of a word, is a catena, and a head with one of several dependents is a catena that is not a constituent.

Main definitions

• DependencyGrammar.IsCatena: the words of s induce a connected subgraph.
• DependencyGrammar.IsConstituent: s is the dominance cone of a word.

Main statements

• DependencyGrammar.IsConstituent.isCatena: every constituent is a catena.
• DependencyGrammar.not_isConstituent_pair: in a forest, a head with one of two dependents is not a constituent.
• DependencyGrammar.Graph.IsTree.isTree_toSimpleGraph: the undirected view of a dependency tree is a tree.

References

• [Osb19]

def DependencyGrammar.IsCatena {n : ℕ} (g : Graph n) (s : Finset (Fin n)) : Prop

s is a catena if the subgraph induced on s is connected.

Equations

• DependencyGrammar.IsCatena g s = (SimpleGraph.induce (↑s) g.toSimpleGraph).Connected

def DependencyGrammar.IsConstituent {n : ℕ} (g : Graph n) (s : Finset (Fin n)) : Prop

s is a constituent if it is the dominance cone of some position.

Equations

• DependencyGrammar.IsConstituent g s = ∃ (v : Fin n), ∀ (w : Fin n), w ∈ s ↔ DependencyGrammar.Dominates g v w

@[instance_reducible]

instance DependencyGrammar.instDecidableIsCatena {n : ℕ} (g : Graph n) (s : Finset (Fin n)) : Decidable (IsCatena g s)

Equations

• DependencyGrammar.instDecidableIsCatena g s = { decide := decide ((SimpleGraph.induce (↑s) g.toSimpleGraph).Preconnected ∧ Finset.univ.Nonempty), reflects_decide := ⋯ }

@[instance_reducible]

instance DependencyGrammar.instDecidableIsConstituent {n : ℕ} (g : Graph n) (s : Finset (Fin n)) : Decidable (IsConstituent g s)

Equations

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

theorem DependencyGrammar.singleton_isCatena {n : ℕ} (g : Graph n) (v : Fin n) : IsCatena g {v}

Every single word is a catena.

theorem DependencyGrammar.connected_induce_cone {n : ℕ} (g : Graph n) (v : Fin n) : (SimpleGraph.induce {x : Fin n | Dominates g v x} g.toSimpleGraph).Connected

The dominance cone of a position induces a connected subgraph of the undirected view, since each dominated position is reached along its own dominance path, which never leaves the cone.

theorem DependencyGrammar.IsConstituent.isCatena {n : ℕ} {g : Graph n} {s : Finset (Fin n)} (h : IsConstituent g s) : IsCatena g s

Every constituent is a catena, since a constituent is the dominance cone of some position and cones induce connected subgraphs.

theorem DependencyGrammar.isCatena_pair {n : ℕ} (g : Graph n) {v w : Fin n} (h : g.Adj v w) (hne : v ≠ w) : IsCatena g {v, w}

A head with one of its dependents is a catena.

theorem DependencyGrammar.not_isConstituent_pair {n : ℕ} {g : Graph n} (hF : g.IsForest) {v w u : Fin n} (hw : g.Adj v w) (hu : g.Adj v u) (huw : u ≠ w) : ¬IsConstituent g {v, w}

In a forest, a head with one of its dependents is not a constituent when the head has another dependent, since the head's cone contains the other dependent and the dependent's cone does not contain the head.

theorem DependencyGrammar.isConstituent_univ {n : ℕ} {g : Graph n} (hT : g.IsTree) : IsConstituent g Finset.univ

The whole sentence is a constituent, the dominance cone of the root.

theorem DependencyGrammar.isCatena_univ {n : ℕ} {g : Graph n} (hT : g.IsTree) : IsCatena g Finset.univ

The whole sentence is a catena.

theorem DependencyGrammar.Graph.IsTree.isTree_toSimpleGraph {n : ℕ} {g : Graph n} (hT : g.IsTree) : g.toSimpleGraph.IsTree

The undirected view of a dependency tree is a tree: it is connected, the whole sentence being a catena, and its edges are the links from each position other than the root to its head.