Catenae

[OG12]

Formalizes the catena (Osborne, Putnam & Groß 2012, Syntax 15:4, 354–396): a connected subgraph of a dependency tree — any word or combination of words that is continuous with respect to the dominance relation. Catenae strictly generalize constituents: every constituent is a catena, but not every catena is a constituent.

Main declarations

• bfsReachable — BFS within a restricted node set; the computable core of catena-membership checking.
• isConnected, isCatena, isConstituent — Bool-valued predicates over a node list and a dependency list.
• BidirReachable — Prop-level bidirectional reachability matching bfsReachable, with bidir_symm / bidir_trans.
• bfsReachable_complete — every BidirReachable node appears in the BFS output. Used by downstream files to convert structural reachability proofs into computable catena membership.
• singleton_isCatena — singletons are catenae.

Implementation notes

• Predicate-shape definitions return Bool to integrate with downstream decide-style theorems; a substrate-wide migration to Prop + [DecidablePred] is deferred.
• The original IsCatena mathlib-Prop bridge (via SimpleGraph.Preconnected on induced subgraphs) and the worked numerical examples (tree9, tree22, chain4, star4, counting / ratio API) were removed during the mathlib-quality pass; they had no external consumers.

Computable BFS over dependency edges

def DepGrammar.Catena.isConnected (deps : List Dependency) (nodes : List ℕ) : Bool

Check if a node set is connected within the dependency graph. BFS from the first node and check that all others are reached.

Equations

• DepGrammar.Catena.isConnected deps [] = true
• DepGrammar.Catena.isConnected deps (start :: tail) = (start :: tail).all (DepGrammar.Catena.bfsReachable✝ deps (start :: tail) start).contains

def DepGrammar.Catena.isCatena (deps : List Dependency) (nodes : List ℕ) : Bool

Computable catena check: non-empty and connected in the tree.

Equations

• DepGrammar.Catena.isCatena deps nodes = (!nodes.isEmpty && DepGrammar.Catena.isConnected deps nodes)

def DepGrammar.Catena.isConstituent (deps : List Dependency) (n : ℕ) (nodes : List ℕ) : Bool

Check if a node set equals the complete subtree (projection) rooted at some node.

Equations

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

BFS invariants

Bidirectional reachability (Prop level)

inductive DepGrammar.Catena.BidirReachable (deps : List Dependency) (allowed : List ℕ) : ℕ → ℕ → Prop

Bidirectional reachability within a restricted node set. BidirReachable deps allowed u v holds when there is a path from u to v using dependency edges (in either direction) where all nodes are in allowed.

• here {deps : List Dependency} {allowed : List ℕ} (v : ℕ) : v ∈ allowed → BidirReachable deps allowed v v
• step {deps : List Dependency} {allowed : List ℕ} (u v w : ℕ) : u ∈ allowed → v ∈ allowed → (∃ d ∈ deps, d.headIdx = u ∧ d.depIdx = v ∨ d.depIdx = u ∧ d.headIdx = v) → BidirReachable deps allowed v w → BidirReachable deps allowed u w

theorem DepGrammar.Catena.bidir_step_append {deps : List Dependency} {allowed : List ℕ} {u v w : ℕ} (h : BidirReachable deps allowed u v) (hv : v ∈ allowed) (hw : w ∈ allowed) (hedge : ∃ d ∈ deps, d.headIdx = v ∧ d.depIdx = w ∨ d.depIdx = v ∧ d.headIdx = w) : BidirReachable deps allowed u w

Append a step to the end of a bidirectional path.

theorem DepGrammar.Catena.bidir_symm {deps : List Dependency} {allowed : List ℕ} {u v : ℕ} (h : BidirReachable deps allowed u v) : BidirReachable deps allowed v u

Bidirectional reachability is symmetric.

theorem DepGrammar.Catena.bidir_trans {deps : List Dependency} {allowed : List ℕ} {u v w : ℕ} (h1 : BidirReachable deps allowed u v) (h2 : BidirReachable deps allowed v w) : BidirReachable deps allowed u w

Bidirectional reachability is transitive.

BFS completeness

theorem DepGrammar.Catena.bfsReachable_complete (deps : List Dependency) (allowed : List ℕ) (start target : ℕ) (h : BidirReachable deps allowed start target) : target ∈ DepGrammar.Catena.bfsReachable✝ deps allowed start

BFS completeness: every bidirectionally reachable node appears in the bfsReachable output.

theorem DepGrammar.Catena.singleton_isCatena (deps : List Dependency) (v : ℕ) : isCatena deps [v] = true

Any singleton is a catena: non-empty and trivially connected.