Dependency-grammar coreference (binding)

Binding via d-command and locality ([Hud90], [Gib25]). The c-command analogue in dependency grammar is d-command: x d-commands y iff both are dependents of the same head and x bears the subject relation. Locality is the dependency subgraph rooted at the matrix verb.

As with the other frameworks, the binding principles are not restated here: this file supplies dependency grammar's command relation as a Binding.CommandRelation instance, and the framework-neutral engine (Syntax/Binding/Basic.lean) derives Principles A/B/C over it. The file is language-neutral — it imports no Fragment.

Main definitions

• toDepTree, dCommands, subjectDCommandsObject, sameLocalDomain — the d-command relation and its locality restriction, over a Binding.SimpleClause.
• instance : CommandRelation — the dependency-grammar instance of the abstract command relation (d-command); the engine supplies Principles A/B/C over it.

D-command from the dependency tree

def DepGrammar.Coreference.toDepTree (clause : Binding.SimpleClause) : DepTree

Build a dependency tree from a clause. Indices: 0 = subject, 1 = verb (root), 2 = object (if present); subject ←nsubj— verb, object ←obj— verb.

Equations

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

def DepGrammar.Coreference.dCommands (tree : DepTree) (i j : ℕ) : Bool

D-command: the word at i d-commands the word at j if both are dependents of the same head and i bears the subject relation (nsubj).

Equations

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

def DepGrammar.Coreference.subjectDCommandsObject (clause : Binding.SimpleClause) : Bool

Subject d-commands object: both dependents of the verb, subject bears nsubj.

Equations

• DepGrammar.Coreference.subjectDCommandsObject clause = match clause.object with | none => false | some val => DepGrammar.Coreference.dCommands (DepGrammar.Coreference.toDepTree clause) 0 2

def DepGrammar.Coreference.sameLocalDomain (clause : Binding.SimpleClause) : Bool

Both positions are dependents of the same head (the verb) — one domain.

Equations

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

Dependency grammar as a command relation

def DepGrammar.Coreference.commands (c : Binding.SimpleClause) : Binding.Pos → Binding.Pos → Prop

The dependency-grammar command relation: d-command. Object→subject never holds (only the subject bears nsubj).

Equations

• DepGrammar.Coreference.commands c Binding.Pos.subject Binding.Pos.object = (DepGrammar.Coreference.subjectDCommandsObject c = true)
• DepGrammar.Coreference.commands c x✝¹ x✝ = False

def DepGrammar.Coreference.sameDomain (c : Binding.SimpleClause) : Binding.Pos → Binding.Pos → Prop

Locality: in a simple clause all positions share the one binding domain.

Equations

• DepGrammar.Coreference.sameDomain c x✝¹ x✝ = (DepGrammar.Coreference.sameLocalDomain c = true)

@[implicit_reducible]

instance DepGrammar.Coreference.instDecidableSameDomain (c : Binding.SimpleClause) (i j : Binding.Pos) : Decidable (sameDomain c i j)

Equations

• DepGrammar.Coreference.instDecidableSameDomain c i j = DepGrammar.Coreference.instDecidableSameDomain._aux_1 c i j

@[implicit_reducible]

instance DepGrammar.Coreference.instCommandRelation : Binding.CommandRelation

The dependency-grammar instance of the abstract command relation ([BP90]): d-command. The engine supplies Principles A/B/C; a study applies them with this instance and a language classifier.

Equations

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