Catenae

This file defines a catena: a word or combination of words connected in the undirected presentation of a dependency tree.

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: exactly 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 = DependencyGrammar.instDecidableIsCatena._aux_1 g s

@[instance_reducible]

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

Equations

• DependencyGrammar.instDecidableIsConstituent g s = DependencyGrammar.instDecidableIsConstituent._aux_1 g s

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: 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: a constituent is the dominance cone of some position, and cones induce connected subgraphs.

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

The whole sentence is a constituent: the root's dominance cone.

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

The whole sentence is a catena.