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.

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.

instance DepGrammar.instDecidableEqDependency : DecidableEq Dependency

Equations

• DepGrammar.instDecidableEqDependency = DepGrammar.instDecidableEqDependency.decEq

structure DepGrammar.DepTree : Type

A dependency tree for a sentence.

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

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

Equations

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

instance DepGrammar.instReprDepTree : Repr DepTree

Equations

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

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 : ℕ

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 }

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✝

instance DepGrammar.instReprDir : Repr Dir

Equations

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

instance DepGrammar.instDecidableEqDir : DecidableEq Dir

Equations

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

instance DepGrammar.instInhabitedDir : Inhabited Dir

Equations

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

def DepGrammar.instInhabitedDir.default : Dir

Equations

• DepGrammar.instInhabitedDir.default = DepGrammar.Dir.left

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.

instance DepGrammar.instReprArgSlot : Repr ArgSlot

Equations

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

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

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) " }"

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.valenceToArgStr : Valence → Option ArgStr

Map Valence to the corresponding standard DG argument structure. Returns none for valences without a standard frame (clausal, copular, dative, locative).

Equations

• DepGrammar.valenceToArgStr Valence.intransitive = some DepGrammar.argStr_V0
• DepGrammar.valenceToArgStr Valence.transitive = some DepGrammar.argStr_VN
• DepGrammar.valenceToArgStr Valence.ditransitive = some DepGrammar.argStr_VNN
• DepGrammar.valenceToArgStr 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.countDepsOfType (t : DepTree) (headIdx : ℕ) (dtype : UD.DepRel) : ℕ

Count dependents of a given type for a head.

Equations

• DepGrammar.countDepsOfType t headIdx dtype = (List.filter (fun (d : DepGrammar.Dependency) => d.headIdx == headIdx && d.depType == dtype) t.deps).length

def DepGrammar.checkVerbSubcat (t : DepTree) : Bool

Check if verb has correct argument structure.

Equations

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

def DepGrammar.mkSVTree (subj verb : Word) : DepTree

Create a simple SV tree: subject -> verb.

Equations

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

def DepGrammar.mkSVOTree (subj verb obj : Word) : 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) : 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) : DepTree

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

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.