Diatheses

A diathesis of a verb is the correspondence between its participants and the syntactic positions expressing them: here, an argument frame together with the slot each participant occupies, or none for a participant the construction leaves out. A verb's valency is its participants and its diatheses, the basic diathesis first, so one participant can be followed across the verb's constructions: the thing broken is the object of transitive break and the subject of intransitive break. Which diatheses a verb has, and which participant fills which slot, are lexical data; theories of argument linking are predicates on them. An alternation relates two diatheses of a verb, and a voice is an alternation the verb's form marks.

Main definitions

• Diathesis n: an argument frame and the slot of each of n participants.
• Diathesis.ofSlots: the diathesis whose slots, in order, hold the listed participants.
• Verb.Valency: a verb's participants, with their entailment profiles, and its diatheses, the basic diathesis first.

Implementation notes

• A link runs from a participant to its slot, so two participants can share a slot, as the agent and the patient of a reflexive do; an implied participant occupies an implicit position of the frame.
• Participants are numbered, and a diathesis is entered as the participants of its slots in slot order, the external argument first: ofSlots .np [0, 1] puts participant 0 in subject position and participant 1 in object position.
• A diathesis may leave out a participant another diathesis of the verb expresses, as the intransitive of break leaves out the breaker, so a causative or anticausative pair is two diatheses of one verb. Mel'čuk's narrower diathesis keeps the semantic actants fixed and treats such a pair as two lexical units.

References

• [Mel93]
• [ZK19]

structure Diathesis (n : ℕ) extends ArgumentFrame : Type

A diathesis of n participants is an argument frame together with the slot each participant occupies in it, none for a participant the construction leaves out.

• external : Option Position
• complements : List Position
• links : Vector (Option ArgumentFrame.Slot) n

  The slot each participant occupies.

@[instance_reducible]

instance instDecidableEqDiathesis {n✝ : ℕ} : DecidableEq (Diathesis n✝)

Equations

• instDecidableEqDiathesis = instDecidableEqDiathesis.decEq

def instDecidableEqDiathesis.decEq {n✝ : ℕ} (x✝ x✝¹ : Diathesis n✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqDiathesis.decEq { toArgumentFrame := a, links := a_1 } { toArgumentFrame := b, links := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance instReprDiathesis {n✝ : ℕ} : Repr (Diathesis n✝)

Equations

• instReprDiathesis = { reprPrec := instReprDiathesis.repr }

def instReprDiathesis.repr {n✝ : ℕ} : Diathesis n✝ → ℕ → Std.Format

Equations

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

def Diathesis.ofSlots {n : ℕ} (fr : ArgumentFrame) (ps : List ℕ) : Diathesis n

ofSlots fr ps is the diathesis of fr whose slots, in the order of ArgumentFrame.slots, hold the participants ps; a participant ps does not list is left out.

Equations

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

def Diathesis.participantAt {n : ℕ} (d : Diathesis n) (s : ArgumentFrame.Slot) : Option (Fin n)

The participant occupying a slot, the first if several share it.

Equations

• d.participantAt s = List.find? (fun (i : Fin n) => decide (d.links.get i = some s)) (List.finRange n)

def Diathesis.participantRole {n : ℕ} (d : Diathesis n) (i : Fin n) : Option ArgumentRole

The argument role of a participant, that of its slot.

Equations

• d.participantRole i = (d.links.get i).bind d.argumentRole

structure Verb.Valency : Type

A verb's valency is its participants, each with the proto-role entailment profile the entry records for it, and its diatheses, the basic diathesis first.

• arity : ℕ

  The number of participants.

• profiles : Vector (Option ArgumentStructure.EntailmentProfile) self.arity

  The entailment profile of each participant, where the entry records one.

• diatheses : List (Diathesis self.arity)

  The diatheses, the basic diathesis first.

def Verb.instDecidableEqValency.decEq (x✝ x✝¹ : Valency) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Verb.instDecidableEqValency : DecidableEq Valency

Equations

• Verb.instDecidableEqValency = Verb.instDecidableEqValency.decEq

def Verb.instReprValency.repr : Valency → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Verb.instReprValency : Repr Valency

Equations

• Verb.instReprValency = { reprPrec := Verb.instReprValency.repr }

def Verb.Valency.of (frs : List (ArgumentFrame × List ℕ)) (profiles : List (Option ArgumentStructure.EntailmentProfile) := []) : Valency

The valency whose diatheses are given as frames with the participants of their slots in slot order, and whose participants have the listed profiles; the participants are numbered from 0.

Equations

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

def Verb.Valency.ofFrame (fr : ArgumentFrame) (profiles : List (Option ArgumentStructure.EntailmentProfile) := []) : Valency

The valency of a verb with one diathesis, each slot of its frame holding its own participant in slot order.

Equations

• Verb.Valency.ofFrame fr profiles = Verb.Valency.of [(fr, List.range fr.slots.length)] profiles

def Verb.Valency.basic? (V : Valency) : Option (Diathesis V.arity)

The basic diathesis, the first.

Equations

• V.basic? = V.diatheses.head?

def Verb.Valency.frames (V : Valency) : List ArgumentFrame

The argument frames of the diatheses.

Equations

• V.frames = List.map (fun (x : Diathesis V.arity) => x.toArgumentFrame) V.diatheses

def Verb.Valency.profileAt (V : Valency) (d : Diathesis V.arity) (s : ArgumentFrame.Slot) : Option ArgumentStructure.EntailmentProfile

The entailment profile of the participant in a slot of one of the diatheses.

Equations

• V.profileAt d s = (d.participantAt s).bind V.profiles.get

@[simp]

theorem Verb.Valency.frames_of (frs : List (ArgumentFrame × List ℕ)) (ps : List (Option ArgumentStructure.EntailmentProfile)) : (of frs ps).frames = List.map (fun (x : ArgumentFrame × List ℕ) => x.1) frs