Dependency grammar substrate

Core data types for dependency grammar: words connected by typed directed edges (Dependency), trees built over them (DepTree), and enhanced graphs allowing multiple incoming arcs (DepGraph). Argument structures (ArgStr) record direction and selectional category for each slot.

Dependency relations use UD.DepRel from Core/UD.lean (Universal Dependencies v2). [Hud10], [Gib25].

Main declarations

• Dependency, DepTree, DepGraph — the basic graph-shaped data.
• ArgStr, argStrV0/VN/VNN/VPassive — argument-structure schemas for the standard intransitive / transitive / ditransitive / passive valences.
• hasUniqueHeads, isAcyclic, isWellFormed — structural well-formedness predicates (Bool-valued; see Implementation notes).
• mkSVTree, mkSVOTree, mkDetNVTree, mkDitransTree — small fixture builders used by Studies and Formal/ test data.

Implementation notes

• Predicate-shape definitions return Bool rather than Prop + [Decidable]; this is a substrate-wide convention that downstream files inherit, and migrating it is a separate refactor.

inductive DepGrammar.Dir : Type

Direction of a dependent relative to head.

• left : Dir
• right : Dir

def DepGrammar.instReprDir.repr : Dir → ℕ → Std.Format

Equations

• DepGrammar.instReprDir.repr DepGrammar.Dir.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DepGrammar.Dir.left")).group prec✝
• DepGrammar.instReprDir.repr DepGrammar.Dir.right prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DepGrammar.Dir.right")).group prec✝

@[implicit_reducible]

instance DepGrammar.instReprDir : Repr Dir

Equations

• DepGrammar.instReprDir = { reprPrec := DepGrammar.instReprDir.repr }

@[implicit_reducible]

instance DepGrammar.instDecidableEqDir : DecidableEq Dir

Equations

• DepGrammar.instDecidableEqDir x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance DepGrammar.instInhabitedDir : Inhabited Dir

Equations

• DepGrammar.instInhabitedDir = { default := DepGrammar.instInhabitedDir.default }

structure DepGrammar.ArgSlot : Type

A single argument slot in an argument structure.

• depType : UD.DepRel
• dir : Dir
• required : Bool
• cat : Option UD.UPOS

def DepGrammar.instReprArgSlot.repr : ArgSlot → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DepGrammar.instReprArgSlot : Repr ArgSlot

Equations

• DepGrammar.instReprArgSlot = { reprPrec := DepGrammar.instReprArgSlot.repr }

@[implicit_reducible]

instance DepGrammar.instDecidableEqArgSlot : DecidableEq ArgSlot

Equations

• DepGrammar.instDecidableEqArgSlot = DepGrammar.instDecidableEqArgSlot.decEq

def DepGrammar.instDecidableEqArgSlot.decEq (x✝ x✝¹ : ArgSlot) : Decidable (x✝ = x✝¹)

Equations

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

structure DepGrammar.ArgStr : Type

Argument structure: what dependents a word requires/allows.

• slots : List ArgSlot

@[implicit_reducible]

instance DepGrammar.instReprArgStr : Repr ArgStr

Equations

• DepGrammar.instReprArgStr = { reprPrec := DepGrammar.instReprArgStr.repr }

def DepGrammar.instReprArgStr.repr : ArgStr → ℕ → Std.Format

Equations

• DepGrammar.instReprArgStr.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "slots" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.slots)).group) " }"

@[implicit_reducible]

instance DepGrammar.instDecidableEqArgStr : DecidableEq ArgStr

Equations

• DepGrammar.instDecidableEqArgStr = DepGrammar.instDecidableEqArgStr.decEq

def DepGrammar.instDecidableEqArgStr.decEq (x✝ x✝¹ : ArgStr) : Decidable (x✝ = x✝¹)

Equations

• DepGrammar.instDecidableEqArgStr.decEq { slots := a } { slots := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Dependencies and trees

structure DepGrammar.Dependency : Type

A dependency: directed edge from head to dependent. Uses UD.DepRel for the relation label.

• headIdx : ℕ
• depIdx : ℕ
• depType : UD.DepRel

def DepGrammar.instReprDependency.repr : Dependency → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DepGrammar.instReprDependency : Repr Dependency

Equations

• DepGrammar.instReprDependency = { reprPrec := DepGrammar.instReprDependency.repr }

def DepGrammar.instDecidableEqDependency.decEq (x✝ x✝¹ : Dependency) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance DepGrammar.instDecidableEqDependency : DecidableEq Dependency

Equations

• DepGrammar.instDecidableEqDependency = DepGrammar.instDecidableEqDependency.decEq

structure DepGrammar.DepTree : Type

A dependency tree for a sentence. frames carries the DG-specific lexical argument-structure premises, aligned with words (missing/short = no frame): the frame is framework apparatus (like HPSG's ARG-ST), so it lives on DG's tree, not on the shared Word token. Frames come from the lexical carrier at tree construction (complementToArgStr applied to a verb's complementType).

• words : List Word
• deps : List Dependency
• rootIdx : ℕ
• frames : List (Option ArgStr)

@[implicit_reducible]

instance DepGrammar.instReprDepTree : Repr DepTree

Equations

• DepGrammar.instReprDepTree = { reprPrec := DepGrammar.instReprDepTree.repr }

def DepGrammar.instReprDepTree.repr : DepTree → ℕ → Std.Format

Equations

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

def DepGrammar.DepTree.frame (t : DepTree) (i : ℕ) : Option ArgStr

The argument-structure frame at position i, if one was supplied.

Equations

• t.frame i = t.frames[i]?.getD none

structure DepGrammar.DepGraph : Type

An enhanced dependency graph: like DepTree but allows multiple heads per word. Relaxes the unique-heads constraint.

• words : List Word
• deps : List Dependency
• rootIdx : ℕ

@[implicit_reducible]

instance DepGrammar.instReprDepGraph : Repr DepGraph

Equations

• DepGrammar.instReprDepGraph = { reprPrec := DepGrammar.instReprDepGraph.repr }

def DepGrammar.instReprDepGraph.repr : DepGraph → ℕ → Std.Format

Equations

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

def DepGrammar.DepTree.toGraph (t : DepTree) : DepGraph

Every DepTree is trivially a DepGraph.

Equations

• t.toGraph = { words := t.words, deps := t.deps, rootIdx := t.rootIdx }

def DepGrammar.argStr_V0 : ArgStr

Intransitive verb: subject to the left

Equations

• DepGrammar.argStr_V0 = { slots := [{ depType := UD.DepRel.nsubj, dir := DepGrammar.Dir.left, cat := some UD.UPOS.DET }] }

def DepGrammar.argStr_VN : ArgStr

Transitive verb: subject left, object right

Equations

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

def DepGrammar.argStr_VNN : ArgStr

Ditransitive verb: subject left, indirect object right, object right

Equations

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

def DepGrammar.argStr_VPassive : ArgStr

Passive transitive: subject left (was patient), optional by-phrase right

Equations

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

def DepGrammar.complementToArgStr : ComplementType → Option ArgStr

Map a complement type to the corresponding standard DG argument structure. Returns none for frames without a standard schema: clause-embedding types take xcomp/ccomp, not obj, and .np_pp has no fixture here.

Equations

• DepGrammar.complementToArgStr ComplementType.none = some DepGrammar.argStr_V0
• DepGrammar.complementToArgStr ComplementType.np = some DepGrammar.argStr_VN
• DepGrammar.complementToArgStr ComplementType.np_np = some DepGrammar.argStr_VNN
• DepGrammar.complementToArgStr x✝ = none

def DepGrammar.hasUniqueHeads (t : DepTree) : Bool

Check if every word except root has exactly one head.

Equations

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

def DepGrammar.isAcyclic (t : DepTree) : Bool

Check for cycles: no word is its own ancestor.

Equations

• DepGrammar.isAcyclic t = (List.range t.words.length).all fun (start : ℕ) => DepGrammar.isAcyclic.follow t start [] (t.words.length + 1)

def DepGrammar.isAcyclic.follow (t : DepTree) (current : ℕ) (visited : List ℕ) (fuel : ℕ) : Bool

Equations

• One or more equations did not get rendered due to their size.
• DepGrammar.isAcyclic.follow t current visited 0 = true

structure DepGrammar.DepTree.WF (t : DepTree) : Prop

Bundled well-formedness: unique heads + valid index bounds. Collects the three hypotheses that most dominance/planarity theorems need.

• uniqueHeads : hasUniqueHeads t = true
• depIdx_lt (d : Dependency) : d ∈ t.deps → d.depIdx < t.words.length
• headIdx_lt (d : Dependency) : d ∈ t.deps → d.headIdx < t.words.length

def DepGrammar.checkSubjVerbAgr (t : DepTree) : Bool

Check subject-verb number agreement.

Equations

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

def DepGrammar.checkDetNounAgr (t : DepTree) : Bool

Check determiner-noun number agreement.

Equations

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

def DepGrammar.satisfiesArgStr (t : DepTree) (headIdx : ℕ) (argStr : ArgStr) : Bool

Check if a dependency tree satisfies an argument structure

Equations

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

def DepGrammar.coreArgRels : List UD.DepRel

Core argument relations governed by lexical frames.

Equations

• DepGrammar.coreArgRels = [UD.DepRel.nsubj, UD.DepRel.obj, UD.DepRel.iobj]

def DepGrammar.coreArgsLicensed (t : DepTree) (headIdx : ℕ) (argStr : ArgStr) : Bool

Every core-argument dependent of headIdx is licensed by a slot of argStr — the closed-world half of frame checking (satisfiesArgStr only checks that required slots are filled).

Equations

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

def DepGrammar.checkVerbSubcat (t : DepTree) : Bool

Check each verb's dependents against its lexical frame: required slots filled in the right direction (satisfiesArgStr) and no unlicensed core arguments (coreArgsLicensed). Verbs without a frame are skipped.

Equations

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

def DepGrammar.mkSVTree (subj verb : Word) (frame : Option ArgStr := none) : DepTree

Create a simple SV tree: subject -> verb.

Equations

• DepGrammar.mkSVTree subj verb frame = { words := [subj, verb], deps := [{ headIdx := 1, depIdx := 0, depType := UD.DepRel.nsubj }], rootIdx := 1, frames := [none, frame] }

def DepGrammar.mkSVOTree (subj verb obj : Word) (frame : Option ArgStr := none) : DepTree

Create a simple SVO tree: subject -> verb <- object.

Equations

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

def DepGrammar.mkDetNVTree (det noun verb : Word) (frame : Option ArgStr := none) : DepTree

Create Det-N-V tree: det -> noun -> verb.

Equations

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

def DepGrammar.mkDitransTree (subj verb iobj obj : Word) (frame : Option ArgStr := none) : DepTree

Create a ditransitive tree: subj -> verb <- iobj <- obj.

Equations

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