Valency frames

This file defines valency frames over dependency graphs: slot data, standard frame schemas for the basic valences, the valency of a verb's lexical ArgumentFrame, read off the argument roles of its core arguments, and satisfaction of a frame by a position's dependents.

Main definitions

• Valency is a word's valency as a list of slots, each a relation, a head direction and an optionality.
• Valency.ofFrame is the valency of an argument frame, a slot for each core argument by its argument role.
• 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 (Valency.ofFrame of a verb's basic frame).

References

• [Tes59]
• [Hud10]
• [Osb19]

Slot data

structure DependencyGrammar.Valency.Slot : Type

A single valency slot, recording which relation fills it, the direction of the head with respect to the filler, and whether it must be filled.

• depType : UD.DepRel

  The UD relation of the filler.

• direction : HeadDirection

  The direction of the head with respect to the filler.

• required : Bool

  Whether the slot must be filled.

@[instance_reducible]

instance DependencyGrammar.Valency.instReprSlot : Repr Slot

Equations

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

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

Equations

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

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

Equations

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

@[instance_reducible]

instance DependencyGrammar.Valency.instDecidableEqSlot : DecidableEq Slot

Equations

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

@[reducible, inline]

abbrev DependencyGrammar.Valency : Type

The valency of a word is the list of 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, in which 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

An intransitive verb takes its subject to the left.

Equations

• DependencyGrammar.Valency.intransitive = [{ depType := UD.DepRel.nsubj, direction := HeadDirection.headFinal }]

def DependencyGrammar.Valency.transitive : Valency

A transitive verb takes its subject to the left and its object to the right.

Equations

• DependencyGrammar.Valency.transitive = [{ depType := UD.DepRel.nsubj, direction := HeadDirection.headFinal }, { depType := UD.DepRel.obj, direction := HeadDirection.headInitial }]

def DependencyGrammar.Valency.ditransitive : Valency

A ditransitive verb takes its subject to the left and its indirect object and object to the right.

Equations

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

def DependencyGrammar.Valency.passiveTransitive : Valency

A passive transitive verb takes its subject, the patient, to the left and an optional by-phrase to the right.

Equations

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

Valency of an argument frame

def DependencyGrammar.Valency.Slot.ofRole : ArgumentRole → Slot

The required slot of a core argument by its argument role. S and A are the subject, to the left of the head; P and T the object and R the indirect object, to its right.

Equations

• DependencyGrammar.Valency.Slot.ofRole ArgumentRole.S = { depType := UD.DepRel.nsubj, direction := HeadDirection.headFinal }
• DependencyGrammar.Valency.Slot.ofRole ArgumentRole.A = { depType := UD.DepRel.nsubj, direction := HeadDirection.headFinal }
• DependencyGrammar.Valency.Slot.ofRole ArgumentRole.P = { depType := UD.DepRel.obj, direction := HeadDirection.headInitial }
• DependencyGrammar.Valency.Slot.ofRole ArgumentRole.T = { depType := UD.DepRel.obj, direction := HeadDirection.headInitial }
• DependencyGrammar.Valency.Slot.ofRole ArgumentRole.R = { depType := UD.DepRel.iobj, direction := HeadDirection.headInitial }

def DependencyGrammar.Valency.ofFrame (fr : ArgumentFrame) : Valency

The valency of an argument frame has a slot for each core argument, by its argument role. Clausal and adpositional complements have none, since UD's clausal relations and obliques are not core arguments and Graph.SatisfiesFrames leaves them unconstrained.

Equations

• DependencyGrammar.Valency.ofFrame fr = List.filterMap (fun (s : ArgumentFrame.Slot) => Option.map DependencyGrammar.Valency.Slot.ofRole (fr.argumentRole s)) fr.coreSlots

theorem DependencyGrammar.Valency.ofFrame_intransitive : ofFrame ArgumentFrame.intransitive = intransitive

theorem DependencyGrammar.Valency.ofFrame_np : ofFrame ArgumentFrame.np = transitive

theorem DependencyGrammar.Valency.ofFrame_np_np : ofFrame ArgumentFrame.np_np = ditransitive

Argument-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 when the head has the slot's direction with respect to every filler of every slot, and required slots are filled.

Equations

• DependencyGrammar.SatisfiesValency g v val = ∀ slot ∈ val, (∀ w ∈ g.fillersOf v slot.depType, slot.direction.Orders 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.coreArgRels : List UD.DepRel

Core argument relations governed by lexical frames. Deliberately the nominal core only — UD's clausal core relations (csubj, ccomp, xcomp) are licensed by clause-embedding frames, which Valency.ofFrame does not schematize.

Equations

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

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

Every core-argument dependent of v is licensed by a slot of val — the closed-world half of valency checking (SatisfiesValency only checks that required slots are filled).

Equations

• DependencyGrammar.CoreArgsLicensed g v val = ∀ w ∈ g.children v, ∀ r ∈ g.label v w, r ∈ DependencyGrammar.coreArgRels → ∃ slot ∈ val, slot.depType = r

@[instance_reducible]

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

Equations

• DependencyGrammar.instDecidableCoreArgsLicensed g v val = Finset.decidableDforallFinset

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

Each verb's dependents satisfy its frame, with 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

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