Valency frames

This file defines valency frames over dependency graphs: slot data, standard frame schemas for the basic valences, the map from a verb's lexical ComplementType into them, and satisfaction of a frame by a position's dependents.

Main definitions

• Valency is a word's valency as a list of slots: relation, side of the head, optionality.
• Frames n is the per-position valency table.
• Graph.SatisfiesFrames is frame satisfaction: every filler on its slot's side of the head, required slots filled, and no unlicensed core arguments.

Implementation notes

Frames are a side table (Frames n), not part of the graph carrier: the frame is framework apparatus (like HPSG's ARG-ST), supplied alongside the graph by the consumers that reason about valency and populated from the lexical carrier (a verb's complementType.valency).

References

[Tes59] — Éléments de syntaxe structurale, source of the valency notion [Hud10] — An introduction to Word Grammar [Osb19] — A dependency grammar of English

Slot data

inductive DependencyGrammar.Dir : Type

Direction of a dependent relative to its head.

• left : Dir

  The dependent precedes the head.

• right : Dir

  The dependent follows the head.

@[instance_reducible]

instance DependencyGrammar.instReprDir : Repr Dir

Equations

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

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

Equations

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

@[instance_reducible]

instance DependencyGrammar.instDecidableEqDir : DecidableEq Dir

Equations

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

def DependencyGrammar.Dir.Admits {n : ℕ} : Dir → Fin n → Fin n → Prop

A dependent at position dep sits on side dir of the head at position head.

Equations

• DependencyGrammar.Dir.left.Admits x✝¹ x✝ = (x✝ < x✝¹)
• DependencyGrammar.Dir.right.Admits x✝¹ x✝ = (x✝¹ < x✝)

@[instance_reducible]

instance DependencyGrammar.instDecidableAdmits {n : ℕ} (dir : Dir) (head dep : Fin n) : Decidable (dir.Admits head dep)

Equations

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

structure DependencyGrammar.Valency.Slot : Type

A single valency slot: which relation fills it, on which side of the head, and whether it must be filled.

• depType : UD.DepRel

  The UD relation of the filler.

• dir : Dir

  Which side of the head the filler sits.

• required : Bool

  Whether the slot must be filled.

def DependencyGrammar.Valency.instReprSlot.repr : Slot → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DependencyGrammar.Valency.instReprSlot : Repr Slot

Equations

• DependencyGrammar.Valency.instReprSlot = { reprPrec := DependencyGrammar.Valency.instReprSlot.repr }

@[instance_reducible]

instance DependencyGrammar.Valency.instDecidableEqSlot : DecidableEq Slot

Equations

• DependencyGrammar.Valency.instDecidableEqSlot = DependencyGrammar.Valency.instDecidableEqSlot.decEq

def DependencyGrammar.Valency.instDecidableEqSlot.decEq (x✝ x✝¹ : Slot) : Decidable (x✝ = x✝¹)

Equations

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

@[reducible, inline]

abbrev DependencyGrammar.Valency : Type

The valency of a word: the dependent slots it requires or allows.

Equations

• DependencyGrammar.Valency = List DependencyGrammar.Valency.Slot

@[reducible, inline]

abbrev DependencyGrammar.Frames (n : ℕ) : Type

The per-position frame table supplied alongside a Graph n.

Equations

• DependencyGrammar.Frames n = (Fin n → Option DependencyGrammar.Valency)

def DependencyGrammar.Frames.ofList {n : ℕ} (l : List (Fin n × Valency)) : Frames n

A sparse frame table: positions not listed carry no frame.

Equations

• DependencyGrammar.Frames.ofList l i = Option.map (fun (x : Fin n × DependencyGrammar.Valency) => x.2) (List.find? (fun (x : Fin n × DependencyGrammar.Valency) => x.1 == i) l)

Standard schemas

def DependencyGrammar.Valency.intransitive : Valency

Intransitive verb: subject to the left.

Equations

• DependencyGrammar.Valency.intransitive = [{ depType := UD.DepRel.nsubj, dir := DependencyGrammar.Dir.left }]

def DependencyGrammar.Valency.transitive : Valency

Transitive verb: subject left, object right.

Equations

• DependencyGrammar.Valency.transitive = [{ depType := UD.DepRel.nsubj, dir := DependencyGrammar.Dir.left }, { depType := UD.DepRel.obj, dir := DependencyGrammar.Dir.right }]

def DependencyGrammar.Valency.ditransitive : Valency

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

Equations

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

def DependencyGrammar.Valency.passiveTransitive : Valency

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

Equations

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

def ComplementType.valency : ComplementType → Option DependencyGrammar.Valency

A verb's lexical complement type as a standard valency. Returns none for frames without a standard schema: clause-embedding types take xcomp/ccomp, not obj, and .np_pp has no fixture here.

Equations

• ComplementType.none.valency = some DependencyGrammar.Valency.intransitive
• ComplementType.np.valency = some DependencyGrammar.Valency.transitive
• ComplementType.np_np.valency = some DependencyGrammar.Valency.ditransitive
• x✝.valency = none

Frame satisfaction

def DependencyGrammar.Graph.fillersOf {n : ℕ} (g : Graph n) (v : Fin n) (rel : UD.DepRel) : Finset (Fin n)

The dependents of v linked by relation rel.

Equations

• g.fillersOf v rel = {w ∈ g.children v | g.label v w = some rel}

def DependencyGrammar.SatisfiesValency {n : ℕ} (g : Graph n) (v : Fin n) (val : Valency) : Prop

The graph satisfies a valency at head v: every filler of every slot sits on the slot's side of the head, and required slots are filled.

Equations

• DependencyGrammar.SatisfiesValency g v val = ∀ slot ∈ val, (∀ w ∈ g.fillersOf v slot.depType, slot.dir.Admits v w) ∧ (slot.required = true → (g.fillersOf v slot.depType).Nonempty)

@[instance_reducible]

instance DependencyGrammar.instDecidableSatisfiesValency {n : ℕ} (g : Graph n) (v : Fin n) (val : Valency) : Decidable (SatisfiesValency g v val)

Equations

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

def DependencyGrammar.Graph.SatisfiesFrames {n : ℕ} (g : Graph n) (frames : Frames n) : Prop

Each verb's dependents satisfy its frame: required slots filled in the right direction (SatisfiesValency) and no unlicensed core arguments (CoreArgsLicensed). Verbs without a frame are unconstrained.

Equations

• g.SatisfiesFrames frames = ∀ (v : Fin n), (g.words v).cat = UD.UPOS.VERB → ∀ val ∈ frames v, DependencyGrammar.SatisfiesValency g v val ∧ DependencyGrammar.CoreArgsLicensed✝ g v val

@[instance_reducible]

instance DependencyGrammar.instDecidableSatisfiesFrames {n : ℕ} (g : Graph n) (frames : Frames n) : Decidable (g.SatisfiesFrames frames)

Equations

• DependencyGrammar.instDecidableSatisfiesFrames g frames = DependencyGrammar.instDecidableSatisfiesFrames._aux_1 g frames