Catenal Construction

The fundamental bridge type connecting Construction Grammar and Dependency Grammar ([OG12]): a CatenalCx pairs a CxG Construction (form–meaning description) with a DG catena witness (dependency tree plus a set of node indices proven to form a catena).

Main declarations

• CatenalCx — the bridge structure.
• constituent_implies_catena — every constituent is a catena, the containment establishing that catenae strictly generalise constituents.

Implementation notes

Per-instance witnesses (specific idioms, LVCs, displacement constructions) live in Studies/OsborneGross2012/Data.lean; their catena fields are discharged by decide over the concrete tree.

Core bridge type

def ConstructionGrammar.SlotFiller.matchesWord : SlotFiller String → Word → Bool

A tree word satisfies a slot filler — the lexicalized analogue of the licensing layer's SlotFiller.matches, with POS read off the word itself. A single word may realize a phrasal slot (it projects the phrase); semantic constraints are not checkable at this level.

Equations

• (ConstructionGrammar.SlotFiller.fixed lex).matchesWord x✝ = (lex == x✝.form)
• (ConstructionGrammar.SlotFiller.open_ cat).matchesWord x✝ = (x✝.cat == cat)
• (ConstructionGrammar.SlotFiller.headed lex a).matchesWord x✝ = (lex == x✝.form)
• (ConstructionGrammar.SlotFiller.semantic a).matchesWord x✝ = true
• ConstructionGrammar.SlotFiller.phrasal.matchesWord x✝ = true

structure DepGrammar.CatenalConstruction.CatenalCx : Type

A construction paired with a DG catena witness in some dependency tree. The realizes field keeps the pairing honest: each catena node's word must instantiate some slot of the construction's typed form, so a CatenalCx cannot pair a construction with an unrelated tree.

• 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.

• realizes : (self.nodes.all fun (n : ℕ) => Option.any (fun (w : Word) => List.any self.construction.form fun (x : ConstructionGrammar.Slot String) => x.filler.matchesWord w) self.tree.words[n]?) = true

  Every catena node's word instantiates some slot of the form.

Constituent–catena containment

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); the catena BFS traverses edges bidirectionally, so any pair of constituent nodes is reachable via the root. This is the containment behind {constituents} ⊂ {catenae} ⊂ {subsets}.