Catenal Construction: CxG ↔ DG Bridge Type @cite{osborne-gross-2012}

Defines the CatenalCx type — the fundamental bridge between Construction Grammar and Dependency Grammar. A catenal construction pairs a CxG Construction (form–meaning description) with a DG catena witness (dependency tree + connected node set).

Osborne & Groß (2012) argue that every construction corresponds to a catena. This type makes that claim checkable: to instantiate CatenalCx, one must provide a Construction, a DepTree, the relevant node indices, and a proof that those nodes form a catena.

Key Definitions

• CatenalCx: the bridge structure itself
• CatenalCx.singleton: every single word is a trivial catenal construction
• CatenalCx.isConstituent: whether the catena is also a constituent
• CatenalCx.isNonConstituentCatena: the constructions that require catena theory — things that constituency cannot capture
• CatenalCx.isContiguous: whether the yield is contiguous (non-risen)

Key Results

• CatenalCx.nodes_nonempty: a CatenalCx always has ≥ 1 node
• CatenalCx.singleton_isSingleWord: the singleton constructor yields a single-word construction
• constituent_implies_catena: every constituent is a catena (general statement; per-tree instances verified via native_decide in the bridge)

Concrete instances and verified claims are in Phenomena/Constructions/Studies/OsborneGross2012/Data.lean.

structure DepGrammar.CatenalConstruction.CatenalCx : Type

A catenal construction (Osborne & Groß 2012): a construction whose form-side corresponds to a catena in a dependency tree. This is the fundamental bridge type connecting CxG and DG — every construction can be witnessed as a catena over some dependency tree.

The construction field carries the CxG description. The tree, nodes, and catena fields provide the DG verification: the construction's words form a connected subgraph.

• construction : ConstructionGrammar.Construction

  CxG description of the construction

• tree : DepTree

  A dependency tree instantiating the construction

• nodes : List ℕ

  Node indices that carry the construction

• catena : Catena.isCatena self.tree.deps self.nodes = true

  The construction nodes form a catena

def DepGrammar.CatenalConstruction.CatenalCx.nodeCount (cx : CatenalCx) : ℕ

Number of nodes in the catenal construction.

Equations

• cx.nodeCount = cx.nodes.length

def DepGrammar.CatenalConstruction.CatenalCx.isSingleWord (cx : CatenalCx) : Bool

Whether the catenal construction is a single word. Single-word constructions are always catenae (trivially connected).

Equations

• cx.isSingleWord = (cx.nodes.length == 1)

def DepGrammar.CatenalConstruction.CatenalCx.isConstituent (cx : CatenalCx) : Bool

Whether the catena also forms a constituent (complete subtree rooted at some node). When true, the construction can be captured by constituent structure; when false, the catena concept is essential.

Equations

• cx.isConstituent = DepGrammar.Catena.isConstituent cx.tree.deps cx.tree.words.length cx.nodes

def DepGrammar.CatenalConstruction.CatenalCx.isNonConstituentCatena (cx : CatenalCx) : Bool

Whether the catenal construction is a non-constituent catena — the case that motivates the entire CxG ↔ DG bridge. These constructions cannot be captured by any constituent-based framework: their form-side is connected in dependency structure but does not correspond to any subtree. Idioms ("spill the beans"), LVCs ("take a bath"), and displacement ("beans she spilled") are typical examples.

Equations

• cx.isNonConstituentCatena = !cx.isConstituent

def DepGrammar.CatenalConstruction.CatenalCx.isContiguous (cx : CatenalCx) : Bool

Whether the catena's yield is contiguous in linear order. A catena with contiguous yield occupies a consecutive span of positions; a non-contiguous catena is a risen catena (@cite{osborne-2019}, Ch 7) — connected in the tree but separated by intervening material in the string.

Equations

• cx.isContiguous = DepGrammar.isInterval (cx.nodes.mergeSort fun (x1 x2 : ℕ) => decide (x1 ≤ x2))

def DepGrammar.CatenalConstruction.CatenalCx.singleton (cx : ConstructionGrammar.Construction) (tree : DepTree) (v : ℕ) : CatenalCx

Smart constructor: any single word in a tree trivially forms a CatenalCx. Uses singleton_isCatena — a single node is always connected.

Equations

• DepGrammar.CatenalConstruction.CatenalCx.singleton cx tree v = { construction := cx, tree := tree, nodes := [v], catena := ⋯ }

theorem DepGrammar.CatenalConstruction.CatenalCx.nodes_nonempty (cx : CatenalCx) : cx.nodes ≠ []

The node set of a CatenalCx is always non-empty. Follows directly from the catena requirement (isCatena checks !nodes.isEmpty).

theorem DepGrammar.CatenalConstruction.CatenalCx.singleton_isSingleWord (cx : ConstructionGrammar.Construction) (tree : DepTree) (v : ℕ) : (singleton cx tree v).isSingleWord = true

A singleton CatenalCx is always a single word.

theorem DepGrammar.CatenalConstruction.CatenalCx.singleton_nodeCount (cx : ConstructionGrammar.Construction) (tree : DepTree) (v : ℕ) : (singleton cx tree v).nodeCount = 1

A singleton CatenalCx always has node count 1.

theorem DepGrammar.CatenalConstruction.CatenalCx.singleton_isContiguous (cx : ConstructionGrammar.Construction) (tree : DepTree) (v : ℕ) : (singleton cx tree v).isContiguous = true

A singleton CatenalCx always has contiguous yield (trivially).

theorem DepGrammar.CatenalConstruction.constituent_implies_catena (deps : List Dependency) (n : ℕ) (nodes : List ℕ) (h : Catena.isConstituent deps n nodes = true) : Catena.isCatena deps nodes = true

Constituent → Catena: every constituent is a catena. Constituents are complete subtrees (projections rooted at some node), and complete subtrees are connected in the dependency tree.

This is the fundamental containment result establishing that catenae strictly generalize constituents: {constituents} ⊂ {catenae} ⊂ {subsets}.

Proof: a constituent nodes equals projection deps r for some root r. Every node in the projection is dominated by r, giving downward paths. The catena BFS traverses edges bidirectionally, so any start node can walk up to r (reversed dominance edges) then down to any target.