Voice

A construction of a verb gives each of its participants a status: a nominal term with a transitivity-related role, a dative oblique, an implied participant, or none. A voice relates an initial and a derived diathesis of its participants, and so an initial and a derived construction, as two diatheses of a verb relate in an alternation. What a grammar says of a voice is read off that pair: the fate of each initial core term, whether a participant is nucleativized or denucleativized and so whether valency increases or decreases, and whether the voice only selects a pivot. A voice also records its pivot, the derived slot that is the syntactically privileged term, and the marker by which the verb codes it; a fragment states a voice with its marker, Voice.passive.marked [.suff "x"], and the bare constants are unmarked.

Main definitions

• Voice.Status, Voice.Construction: a participant's status, and a construction.
• Voice.Construction.Nucleativized, Denucleativized, fate: an initial construction compared with a derived one.
• Voice: an initial and a derived diathesis, the pivot and the marker.
• Voice.of: the voice whose initial participants are those of a frame's slots in order.
• Voice.Relates, Verb.Alternates: two diatheses of a verb related by a voice, and a verb with two such diatheses.
• Voice.passive, antipassive, anticausative, causative, reflexive, applicative, patientVoice, obliqueVoice: the voices.
• Voice.leaveImplicit: the voice leaving one complement of a frame unexpressed.

Main statements

• Voice.Construction.valency_eq_of_nucleativized_of_denucleativized: nucleativization is not valency increase.
• Voice.passive_anticausative_fate: the passive keeps the initial A in participant structure, the anticausative suppresses it.
• Voice.isSymmetrical_refl: the trivial voice neither nucleativizes nor denucleativizes.

Implementation notes

• A voice's participants are numbered as a verb's are: those of the initial frame's slots in order, then those the voice adds, which the initial diathesis leaves out; a participant the derived diathesis leaves out is suppressed.
• A frame without a subject codes its core objects as such, so an impersonal construction keeps its P; IsImpersonal reads impersonality off the pivot, which defaults to the first core slot and is none for an impersonal construction.
• The marker is the segmental material coding the voice, in surface order, and the coding type is read off it: synthetic when every morph is bound, analytic when a free morph, an auxiliary, is among them, uncoded when it is empty.
• The names of the alternations as processes, passivization and the rest, are predicates on pairs of constructions in Studies/Creissels2024.lean; the constants here are the voices.

References

• [Com89]
• [Cre24]
• [Dix94]
• [DA00]
• [Fil86]
• [Lev93]
• [Son96]

Transitivity-related roles

inductive Voice.TermRole : Type

The role of a nominal term in [Cre24]'s binary core-term system is one of the core roles S, A and P, or X for an oblique.

• S : TermRole

  The sole core term of an intransitive clause.

• A : TermRole

  The agent-like core term of a transitive clause.

• P : TermRole

  The patient-like core term of a transitive clause.

• X : TermRole

  An oblique.

@[instance_reducible]

instance Voice.instDecidableEqTermRole : DecidableEq TermRole

Equations

• Voice.instDecidableEqTermRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Voice.instReprTermRole.repr : TermRole → ℕ → Std.Format

Equations

• Voice.instReprTermRole.repr Voice.TermRole.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.TermRole.S")).group prec✝
• Voice.instReprTermRole.repr Voice.TermRole.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.TermRole.A")).group prec✝
• Voice.instReprTermRole.repr Voice.TermRole.P prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.TermRole.P")).group prec✝
• Voice.instReprTermRole.repr Voice.TermRole.X prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.TermRole.X")).group prec✝

@[instance_reducible]

instance Voice.instReprTermRole : Repr TermRole

Equations

• Voice.instReprTermRole = { reprPrec := Voice.instReprTermRole.repr }

def Voice.TermRole.ofArgumentRole : ArgumentRole → TermRole

The transitivity-related role of a comparative coding role, under which recipients and themes are P-like core terms.

Equations

• Voice.TermRole.ofArgumentRole ArgumentRole.S = Voice.TermRole.S
• Voice.TermRole.ofArgumentRole ArgumentRole.A = Voice.TermRole.A
• Voice.TermRole.ofArgumentRole ArgumentRole.P = Voice.TermRole.P
• Voice.TermRole.ofArgumentRole ArgumentRole.R = Voice.TermRole.P
• Voice.TermRole.ofArgumentRole ArgumentRole.T = Voice.TermRole.P

Participant fate

inductive Voice.ParticipantFate : Type

What a voice does to a core term of the initial construction.

• denucleativized : ParticipantFate

  Not a core term of the derived construction, but maintained in participant structure as an oblique or an implied participant.

• suppressed : ParticipantFate

  Removed from participant structure.

• maintained : ParticipantFate

  A core term of the derived construction.

• cumulated : ParticipantFate

  One core term of the derived construction with another initial core term.

• na : ParticipantFate

  Not a core term of the initial construction.

@[instance_reducible]

instance Voice.instDecidableEqParticipantFate : DecidableEq ParticipantFate

Equations

• Voice.instDecidableEqParticipantFate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Voice.instReprParticipantFate.repr : ParticipantFate → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Voice.instReprParticipantFate.repr Voice.ParticipantFate.na prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.ParticipantFate.na")).group prec✝

@[instance_reducible]

instance Voice.instReprParticipantFate : Repr ParticipantFate

Equations

• Voice.instReprParticipantFate = { reprPrec := Voice.instReprParticipantFate.repr }

def Voice.ParticipantFate.RemovesFromCoreStatus : ParticipantFate → Prop

The fate removes the participant from core-term status.

Equations

• Voice.ParticipantFate.denucleativized.RemovesFromCoreStatus = True
• Voice.ParticipantFate.suppressed.RemovesFromCoreStatus = True
• x✝.RemovesFromCoreStatus = False

@[instance_reducible]

instance Voice.instDecidablePredParticipantFateRemovesFromCoreStatus : DecidablePred ParticipantFate.RemovesFromCoreStatus

Equations

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

Constructions

inductive Voice.Status : Type

A construction expresses a potential participant of its verb as a nominal term with a transitivity-related role or as a dative oblique, leaves it implied but unexpressed, or has it outside participant structure.

• term (r : TermRole) : Status
• dative : Status
• implicit : Status
• absent : Status

@[instance_reducible]

instance Voice.instDecidableEqStatus : DecidableEq Status

Equations

• Voice.instDecidableEqStatus = Voice.instDecidableEqStatus.decEq

def Voice.instDecidableEqStatus.decEq (x✝ x✝¹ : Status) : Decidable (x✝ = x✝¹)

Equations

• Voice.instDecidableEqStatus.decEq (Voice.Status.term a) (Voice.Status.term b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Voice.instDecidableEqStatus.decEq (Voice.Status.term r) Voice.Status.dative = isFalse ⋯
• Voice.instDecidableEqStatus.decEq (Voice.Status.term r) Voice.Status.implicit = isFalse ⋯
• Voice.instDecidableEqStatus.decEq (Voice.Status.term r) Voice.Status.absent = isFalse ⋯
• Voice.instDecidableEqStatus.decEq Voice.Status.dative (Voice.Status.term r) = isFalse ⋯
• Voice.instDecidableEqStatus.decEq Voice.Status.dative Voice.Status.dative = isTrue ⋯
• Voice.instDecidableEqStatus.decEq Voice.Status.dative Voice.Status.implicit = isFalse Voice.instDecidableEqStatus.decEq._proof_8
• Voice.instDecidableEqStatus.decEq Voice.Status.dative Voice.Status.absent = isFalse Voice.instDecidableEqStatus.decEq._proof_9
• Voice.instDecidableEqStatus.decEq Voice.Status.implicit (Voice.Status.term r) = isFalse ⋯
• Voice.instDecidableEqStatus.decEq Voice.Status.implicit Voice.Status.dative = isFalse Voice.instDecidableEqStatus.decEq._proof_11
• Voice.instDecidableEqStatus.decEq Voice.Status.implicit Voice.Status.implicit = isTrue ⋯
• Voice.instDecidableEqStatus.decEq Voice.Status.implicit Voice.Status.absent = isFalse Voice.instDecidableEqStatus.decEq._proof_12
• Voice.instDecidableEqStatus.decEq Voice.Status.absent (Voice.Status.term r) = isFalse ⋯
• Voice.instDecidableEqStatus.decEq Voice.Status.absent Voice.Status.dative = isFalse Voice.instDecidableEqStatus.decEq._proof_14
• Voice.instDecidableEqStatus.decEq Voice.Status.absent Voice.Status.implicit = isFalse Voice.instDecidableEqStatus.decEq._proof_15
• Voice.instDecidableEqStatus.decEq Voice.Status.absent Voice.Status.absent = isTrue ⋯

@[instance_reducible]

instance Voice.instReprStatus : Repr Status

Equations

• Voice.instReprStatus = { reprPrec := Voice.instReprStatus.repr }

def Voice.instReprStatus.repr : Status → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Voice.instReprStatus.repr Voice.Status.dative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.Status.dative")).group prec✝
• Voice.instReprStatus.repr Voice.Status.implicit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.Status.implicit")).group prec✝
• Voice.instReprStatus.repr Voice.Status.absent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.Status.absent")).group prec✝

def Voice.Status.role : Status → Option TermRole

The role of the nominal term, datives counting as obliques.

Equations

• (Voice.Status.term r).role = some r
• Voice.Status.dative.role = some Voice.TermRole.X
• x✝.role = none

def Voice.Status.Nuclear : Status → Prop

A participant is nuclear when it is expressed as a core term.

Equations

• (Voice.Status.term r).Nuclear = (r ≠ Voice.TermRole.X)
• x✝.Nuclear = False

@[instance_reducible]

instance Voice.Status.instDecidablePredNuclear : DecidablePred Nuclear

Equations

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

@[reducible, inline]

abbrev Voice.Construction (ι : Type u_1) : Type u_1

A construction of a verb gives each of its potential participants a status.

Equations

• Voice.Construction ι = (ι → Voice.Status)

def Voice.Construction.Transitive {ι : Type u_1} (c : Construction ι) : Prop

A transitive construction has an A term and a P term.

Equations

• c.Transitive = ((∃ (i : ι), c i = Voice.Status.term Voice.TermRole.A) ∧ ∃ (i : ι), c i = Voice.Status.term Voice.TermRole.P)

def Voice.Construction.Impersonal {ι : Type u_1} (c : Construction ι) : Prop

An impersonal construction has neither an A term nor an S term.

Equations

• c.Impersonal = ∀ (i : ι), c i ≠ Voice.Status.term Voice.TermRole.A ∧ c i ≠ Voice.Status.term Voice.TermRole.S

def Voice.Construction.valency {ι : Type u_1} (c : Construction ι) [Fintype ι] : ℕ

The valency of a construction is its number of nuclear participants.

Equations

• c.valency = {i : ι | (c i).Nuclear}.card

Comparing an initial construction c with a derived construction d of the same verb.

def Voice.Construction.Nucleativized {ι : Type u_1} (c d : Construction ι) (i : ι) : Prop

A participant that is not a core term of the initial construction is one of the derived construction.

Equations

• c.Nucleativized d i = (¬(c i).Nuclear ∧ (d i).Nuclear)

def Voice.Construction.Denucleativized {ι : Type u_1} (c d : Construction ι) (i : ι) : Prop

A core term of the initial construction is not one of the derived construction.

Equations

• c.Denucleativized d i = ((c i).Nuclear ∧ ¬(d i).Nuclear)

def Voice.Construction.Suppressed {ι : Type u_1} (c d : Construction ι) (i : ι) : Prop

A core term of the initial construction is removed from participant structure.

Equations

• c.Suppressed d i = ((c i).Nuclear ∧ d i = Voice.Status.absent)

def Voice.Construction.Introduced {ι : Type u_1} (c d : Construction ι) (i : ι) : Prop

A participant the initial construction does not express as a core term is expressed, and differently, by the derived construction.

Equations

• c.Introduced d i = (¬(c i).Nuclear ∧ c i ≠ d i ∧ (d i).role.isSome = true)

def Voice.Construction.Cumulated {ι : Type u_1} (c d : Construction ι) (i : ι) : Prop

A core term of the initial construction shares its derived A or S term with another; a clause has one A and one S, so two participants with either share it.

Equations

• c.Cumulated d i = ((c i).Nuclear ∧ (d i = Voice.Status.term Voice.TermRole.A ∨ d i = Voice.Status.term Voice.TermRole.S) ∧ ∃ (j : ι), j ≠ i ∧ (c j).Nuclear ∧ d j = d i)

def Voice.Construction.Nucleativizes {ι : Type u_1} (c d : Construction ι) : Prop

Some participant is nucleativized.

Equations

• c.Nucleativizes d = ∃ (i : ι), c.Nucleativized d i

def Voice.Construction.Denucleativizes {ι : Type u_1} (c d : Construction ι) : Prop

Some participant is denucleativized.

Equations

• c.Denucleativizes d = ∃ (i : ι), c.Denucleativized d i

def Voice.Construction.IsValencyIncreasing {ι : Type u_1} (c d : Construction ι) : Prop

The alternation is valency-increasing when it nucleativizes without denucleativizing.

Equations

• c.IsValencyIncreasing d = (c.Nucleativizes d ∧ ¬c.Denucleativizes d)

def Voice.Construction.IsValencyDecreasing {ι : Type u_1} (c d : Construction ι) : Prop

The alternation is valency-decreasing when it denucleativizes without nucleativizing.

Equations

• c.IsValencyDecreasing d = (c.Denucleativizes d ∧ ¬c.Nucleativizes d)

def Voice.Construction.IsSymmetrical {ι : Type u_1} (c d : Construction ι) : Prop

The alternation is symmetrical when it neither nucleativizes nor denucleativizes, so that it does not affect the transitivity of the construction ([Cre24] §8.1.7).

Equations

• c.IsSymmetrical d = (¬c.Nucleativizes d ∧ ¬c.Denucleativizes d)

theorem Voice.Construction.isSymmetrical_self {ι : Type u_1} (c : Construction ι) : c.IsSymmetrical c

@[instance_reducible]

instance Voice.Construction.instDecidableTransitive {ι : Type u_1} (c : Construction ι) [Fintype ι] : Decidable c.Transitive

Equations

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

@[instance_reducible]

instance Voice.Construction.instDecidableImpersonal {ι : Type u_1} (c : Construction ι) [Fintype ι] : Decidable c.Impersonal

Equations

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

@[instance_reducible]

instance Voice.Construction.instDecidableNucleativized {ι : Type u_1} (c d : Construction ι) (i : ι) : Decidable (c.Nucleativized d i)

Equations

• c.instDecidableNucleativized d i = { decide := decide ¬(c i).Nuclear && decide (d i).Nuclear, reflects_decide := ⋯ }

@[instance_reducible]

instance Voice.Construction.instDecidableDenucleativized {ι : Type u_1} (c d : Construction ι) (i : ι) : Decidable (c.Denucleativized d i)

Equations

• c.instDecidableDenucleativized d i = { decide := decide (c i).Nuclear && decide ¬(d i).Nuclear, reflects_decide := ⋯ }

@[instance_reducible]

instance Voice.Construction.instDecidableSuppressed {ι : Type u_1} (c d : Construction ι) (i : ι) : Decidable (c.Suppressed d i)

Equations

• c.instDecidableSuppressed d i = { decide := decide (c i).Nuclear && decide (d i = Voice.Status.absent), reflects_decide := ⋯ }

@[instance_reducible]

instance Voice.Construction.instDecidableIntroduced {ι : Type u_1} (c d : Construction ι) (i : ι) : Decidable (c.Introduced d i)

Equations

• c.instDecidableIntroduced d i = { decide := decide ¬(c i).Nuclear && decide (c i ≠ d i ∧ (d i).role.isSome = true), reflects_decide := ⋯ }

@[instance_reducible]

instance Voice.Construction.instDecidableCumulated {ι : Type u_1} (c d : Construction ι) [Fintype ι] [DecidableEq ι] (i : ι) : Decidable (c.Cumulated d i)

Equations

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

@[instance_reducible]

instance Voice.Construction.instDecidableNucleativizes {ι : Type u_1} (c d : Construction ι) [Fintype ι] : Decidable (c.Nucleativizes d)

Equations

• c.instDecidableNucleativizes d = { decide := decide (∃ a ∈ Finset.univ, c.Nucleativized d a), reflects_decide := ⋯ }

@[instance_reducible]

instance Voice.Construction.instDecidableDenucleativizes {ι : Type u_1} (c d : Construction ι) [Fintype ι] : Decidable (c.Denucleativizes d)

Equations

• c.instDecidableDenucleativizes d = { decide := decide (∃ a ∈ Finset.univ, c.Denucleativized d a), reflects_decide := ⋯ }

@[instance_reducible]

instance Voice.Construction.instDecidableIsValencyIncreasing {ι : Type u_1} (c d : Construction ι) [Fintype ι] : Decidable (c.IsValencyIncreasing d)

Equations

• c.instDecidableIsValencyIncreasing d = { decide := decide (c.Nucleativizes d) && decide ¬c.Denucleativizes d, reflects_decide := ⋯ }

@[instance_reducible]

instance Voice.Construction.instDecidableIsValencyDecreasing {ι : Type u_1} (c d : Construction ι) [Fintype ι] : Decidable (c.IsValencyDecreasing d)

Equations

• c.instDecidableIsValencyDecreasing d = { decide := decide (c.Denucleativizes d) && decide ¬c.Nucleativizes d, reflects_decide := ⋯ }

@[instance_reducible]

instance Voice.Construction.instDecidableIsSymmetrical {ι : Type u_1} (c d : Construction ι) [Fintype ι] : Decidable (c.IsSymmetrical d)

Equations

• c.instDecidableIsSymmetrical d = { decide := decide ¬c.Nucleativizes d && decide ¬c.Denucleativizes d, reflects_decide := ⋯ }

def Voice.Construction.fate {ι : Type u_1} (c d : Construction ι) [Fintype ι] [DecidableEq ι] (i : ι) : ParticipantFate

An initial core term is suppressed when it leaves participant structure, cumulated when it shares its derived core term with another, maintained when it remains a core term, and denucleativized otherwise.

Equations

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

theorem Voice.Construction.valency_eq_of_nucleativized_of_denucleativized {ι : Type u_1} [Fintype ι] [DecidableEq ι] {c d : Construction ι} {i j : ι} (hi : c.Nucleativized d i) (hj : c.Denucleativized d j) (h : ∀ (k : ι), k ≠ i → k ≠ j → ((c k).Nuclear ↔ (d k).Nuclear)) : c.valency = d.valency

Nucleativization is not valency increase: an alternation may nucleativize one participant and denucleativize another, keeping the valency ([Cre24] §8.1.3).

def ArgumentFrame.status (fr : ArgumentFrame) (s : Slot) : Voice.Status

The status a frame gives the participant of a slot is the transitivity-related role of a core slot, X for an expressed oblique, implicit for an implicit position, and absent for an expletive or an unfilled slot.

Equations

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

def Diathesis.construction {n : ℕ} (d : Diathesis n) : Voice.Construction (Fin n)

The construction of a diathesis gives each participant the status of its slot, absent where the diathesis leaves it out.

Equations

• d.construction i = (d.links.get i).elim Voice.Status.absent d.status

Coding

inductive Voice.Coding : Type

A voice is coded on the verb by verbal morphology, by an analytic construction, or not at all, as the unmarked voice of a system and a flexivalent alternation are ([Cre24] §1.1.3). Equipollence is a property of a system, Voice.Equipollent.

• synthetic : Coding
• analytic : Coding
• uncoded : Coding

@[instance_reducible]

instance Voice.instDecidableEqCoding : DecidableEq Coding

Equations

• Voice.instDecidableEqCoding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Voice.instReprCoding : Repr Coding

Equations

• Voice.instReprCoding = { reprPrec := Voice.instReprCoding.repr }

def Voice.instReprCoding.repr : Coding → ℕ → Std.Format

Equations

• Voice.instReprCoding.repr Voice.Coding.synthetic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.Coding.synthetic")).group prec✝
• Voice.instReprCoding.repr Voice.Coding.analytic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.Coding.analytic")).group prec✝
• Voice.instReprCoding.repr Voice.Coding.uncoded prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.Coding.uncoded")).group prec✝

def Voice.Coding.ofMarker (ms : List Morphology.Morph) : Coding

A marker is uncoded when empty, synthetic when every morph is bound, and analytic otherwise.

Equations

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

structure Voice : Type

A voice relates an initial and a derived diathesis of its participants, privileges a slot of the derived diathesis as its pivot, and is coded by a marker on the verb.

• arity : ℕ

  The number of participants.

• initial : Diathesis self.arity

  The initial diathesis.

• derived : Diathesis self.arity

  The derived diathesis, which leaves out the participants the voice suppresses.

• pivot : Option ArgumentFrame.Slot

  The pivot is the syntactically privileged term of the derived construction, its first core slot, S or A, unless a symmetrical voice selects another; it is none for an impersonal construction ([Cre24] §8.1.7).

• marker : List Morphology.Morph

  The marker lists the morphs coding the voice on the verb in surface order, affixes or an auxiliary, and is empty for a zero-marked or an unmarked voice.

def instDecidableEqVoice.decEq (x✝ x✝¹ : Voice) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqVoice : DecidableEq Voice

Equations

• instDecidableEqVoice = instDecidableEqVoice.decEq

@[instance_reducible]

instance instReprVoice : Repr Voice

Equations

• instReprVoice = { reprPrec := instReprVoice.repr }

def instReprVoice.repr : Voice → ℕ → Std.Format

Equations

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

def Voice.of (fr gr : ArgumentFrame) (links : List (Option ArgumentFrame.Slot)) : Voice

The voice from fr to gr whose participants are those of the slots of fr in order and then those it adds, each in the slot of gr that links lists for it, none for a participant gr leaves out.

Equations

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

The participants of a voice

def Voice.image (v : Voice) (s : ArgumentFrame.Slot) : Option ArgumentFrame.Slot

The derived slot of the participant of an initial slot.

Equations

• v.image s = (v.initial.participantAt s).bind v.derived.links.get

def Voice.preimages (v : Voice) (t : ArgumentFrame.Slot) : List ArgumentFrame.Slot

The initial slots whose participant occupies a derived slot.

Equations

• v.preimages t = List.filter (fun (s : ArgumentFrame.Slot) => v.image s == some t) v.initial.slots

def Voice.newSlots (v : Voice) : List ArgumentFrame.Slot

The derived slots of the participants the voice adds.

Equations

• v.newSlots = List.filterMap (fun (i : Fin v.arity) => if v.initial.links.get i = none then v.derived.links.get i else none) (List.finRange v.arity)

def Voice.fate (v : Voice) (s : ArgumentFrame.Slot) : ParticipantFate

The fate of the participant of an initial slot.

Equations

• v.fate s = (v.initial.participantAt s).elim Voice.ParticipantFate.na (v.initial.construction.fate v.derived.construction)

def Voice.fateOfRole (v : Voice) (r : TermRole) : ParticipantFate

The fate of the initial core term with a transitivity-related role.

Equations

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

def Voice.newParticipant (v : Voice) : Option TermRole

The role of the first participant the voice introduces, if one.

Equations

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

def Voice.pivotRole (v : Voice) : Option TermRole

The transitivity-related role of the pivot is S, A or P for a core term and X for an oblique.

Equations

• v.pivotRole = v.pivot.bind fun (t : ArgumentFrame.Slot) => (v.derived.status t).role

Classification

def Voice.Nucleativizes (v : Voice) : Prop

Some participant becomes a core term.

Equations

• v.Nucleativizes = v.initial.construction.Nucleativizes v.derived.construction

def Voice.Denucleativizes (v : Voice) : Prop

Some initial core term ceases to be one.

Equations

• v.Denucleativizes = v.initial.construction.Denucleativizes v.derived.construction

def Voice.Cumulates (v : Voice) : Prop

Two initial core terms are cumulated.

Equations

• v.Cumulates = ∃ (i : Fin v.arity), v.initial.construction.Cumulated v.derived.construction i

def Voice.IsValencyIncreasing (v : Voice) : Prop

A voice is valency-increasing when it nucleativizes without denucleativizing.

Equations

• v.IsValencyIncreasing = v.initial.construction.IsValencyIncreasing v.derived.construction

def Voice.IsValencyDecreasing (v : Voice) : Prop

A voice is valency-decreasing when it denucleativizes without nucleativizing.

Equations

• v.IsValencyDecreasing = v.initial.construction.IsValencyDecreasing v.derived.construction

def Voice.IsSymmetrical (v : Voice) : Prop

A voice is symmetrical when it neither nucleativizes nor denucleativizes.

Equations

• v.IsSymmetrical = v.initial.construction.IsSymmetrical v.derived.construction

def Voice.SelectsOblique (v : Voice) : Prop

The pivot is an oblique, the selection a binary system does not allow ([Cre24] §8.5.2).

Equations

• v.SelectsOblique = (v.pivotRole = some Voice.TermRole.X)

def Voice.IsImpersonal (v : Voice) : Prop

A voice is impersonal when its derived construction privileges no term ([Cre24] §8.3.2.2).

Equations

• v.IsImpersonal = (v.pivot = none)

def Voice.coding (v : Voice) : Coding

The coding type of the voice, read off its marker ([Cre24] §1.1.3).

Equations

• v.coding = Voice.Coding.ofMarker v.marker

def Voice.IsCoded (v : Voice) : Prop

A voice is coded when it is marked on the verb, as against a flexivalent alternation ([Cre24] §1.1.3).

Equations

• v.IsCoded = (v.marker ≠ [])

@[instance_reducible]

instance Voice.instDecidableNucleativizes (v : Voice) : Decidable v.Nucleativizes

Equations

• v.instDecidableNucleativizes = { decide := decide (∃ a ∈ Finset.univ, v.initial.construction.Nucleativized v.derived.construction a), reflects_decide := ⋯ }

@[instance_reducible]

instance Voice.instDecidableDenucleativizes (v : Voice) : Decidable v.Denucleativizes

Equations

• v.instDecidableDenucleativizes = { decide := decide (∃ a ∈ Finset.univ, v.initial.construction.Denucleativized v.derived.construction a), reflects_decide := ⋯ }

@[instance_reducible]

instance Voice.instDecidableCumulates (v : Voice) : Decidable v.Cumulates

Equations

• v.instDecidableCumulates = { decide := decide (∃ k < v.arity, ∀ (h : k < v.arity), v.initial.construction.Cumulated v.derived.construction ⟨k, h⟩), reflects_decide := ⋯ }

@[instance_reducible]

instance Voice.instDecidableIsValencyIncreasing (v : Voice) : Decidable v.IsValencyIncreasing

Equations

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

@[instance_reducible]

instance Voice.instDecidableIsValencyDecreasing (v : Voice) : Decidable v.IsValencyDecreasing

Equations

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

@[instance_reducible]

instance Voice.instDecidableIsSymmetrical (v : Voice) : Decidable v.IsSymmetrical

Equations

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

@[instance_reducible]

instance Voice.instDecidableSelectsOblique (v : Voice) : Decidable v.SelectsOblique

Equations

• v.instDecidableSelectsOblique = Voice.instDecidableSelectsOblique._aux_1 v

@[instance_reducible]

instance Voice.instDecidableIsImpersonal (v : Voice) : Decidable v.IsImpersonal

Equations

• v.instDecidableIsImpersonal = Voice.instDecidableIsImpersonal._aux_1 v

@[instance_reducible]

instance Voice.instDecidableIsCoded (v : Voice) : Decidable v.IsCoded

Equations

• v.instDecidableIsCoded = { decide := !decide (v.marker = []), reflects_decide := ⋯ }

Marking

def Voice.marked (v : Voice) (ms : List Morphology.Morph) : Voice

The voice with the given marker.

Equations

• v.marked ms = { arity := v.arity, initial := v.initial, derived := v.derived, pivot := v.pivot, marker := ms }

@[simp]

theorem Voice.marker_marked (v : Voice) (ms : List Morphology.Morph) : (v.marked ms).marker = ms

theorem Voice.coding_eq_uncoded_iff (v : Voice) : v.coding = Coding.uncoded ↔ v.marker = []

theorem Voice.isCoded_iff (v : Voice) : v.IsCoded ↔ v.coding ≠ Coding.uncoded

theorem Voice.IsValencyIncreasing.not_isSymmetrical {v : Voice} (h : v.IsValencyIncreasing) : ¬v.IsSymmetrical

theorem Voice.IsValencyDecreasing.not_isSymmetrical {v : Voice} (h : v.IsValencyDecreasing) : ¬v.IsSymmetrical

The trivial voice

def Voice.refl (fr : ArgumentFrame) : Voice

The trivial voice of a frame with itself is the initial construction of a system.

Equations

• Voice.refl fr = Voice.of fr fr (List.map some fr.slots)

theorem Voice.derived_refl (fr : ArgumentFrame) : (refl fr).derived = (refl fr).initial

theorem Voice.isSymmetrical_refl (fr : ArgumentFrame) : (refl fr).IsSymmetrical

The trivial voice is symmetrical.

The voices

def Voice.active : Voice

The active is the initial transitive construction.

Equations

• Voice.active = Voice.refl ArgumentFrame.np

@[reducible, inline]

abbrev Voice.agentVoice : Voice

The agent voice of a symmetrical system, with the agent the pivot, is the active.

Equations

• Voice.agentVoice = Voice.active

def Voice.passive (fr : ArgumentFrame := ArgumentFrame.np) : Voice

The passive of a frame with a complement, the transitive one by default, makes the first complement the subject, the pivot, and denucleativizes the external argument but maintains it in participant structure, implied here and expressed as an oblique in a long passive ([Cre24] §8.3.2.1).

Equations

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

def Voice.impersonalPassive (fr : ArgumentFrame := ArgumentFrame.np) : Voice

The impersonal passive denucleativizes the external argument as the passive does and leaves the complements in place, with no subject, so the initial P keeps its coding and the derived construction has no pivot ([Cre24] §8.3.2.2); of an intransitive frame, it denucleativizes the S (§8.3.2.4).

Equations

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

def Voice.antipassive : Voice

The antipassive denucleativizes the initial P and makes the initial A the S of an intransitive construction ([Cre24] §8.3.2.3).

Equations

• Voice.antipassive = Voice.of ArgumentFrame.np ArgumentFrame.pp [some ArgumentFrame.Slot.external, some (ArgumentFrame.Slot.complement 0)]

def Voice.leaveImplicit (fr : ArgumentFrame) (i : ℕ) (a : Option ImplicitInterp := none) : Voice

The voice leaving the i-th complement of fr unexpressed, interpreted as a, every participant keeping its slot and the one of that complement implied there, as in Fillmore's null complements and Levin's unexpressed object alternations.

Equations

• Voice.leaveImplicit fr i a = Voice.of fr (fr.leaveImplicit i a) (List.map some fr.slots)

def Voice.anticausative : Voice

The anticausative suppresses the initial A from participant structure and makes the initial P the S of an intransitive construction, [Cre24]'s decausativization (§8.3.1.2).

Equations

• Voice.anticausative = Voice.of ArgumentFrame.np ArgumentFrame.intransitive [none, some ArgumentFrame.Slot.external]

def Voice.causative : Voice

The causative nucleativizes a causer as the A of a transitive construction whose P is the initial S ([Cre24] §8.3.1.1).

Equations

• Voice.causative = Voice.of ArgumentFrame.intransitive ArgumentFrame.np [some (ArgumentFrame.Slot.complement 0), some ArgumentFrame.Slot.external]

def Voice.reflexive : Voice

The reflexive cumulates the initial A and P in one S ([Cre24] §8.3.3).

Equations

• Voice.reflexive = Voice.of ArgumentFrame.np ArgumentFrame.intransitive [some ArgumentFrame.Slot.external, some ArgumentFrame.Slot.external]

@[reducible, inline]

abbrev Voice.reciprocal : Voice

The reciprocal is the reflexive with a group reading ([Cre24] §8.3.3).

Equations

• Voice.reciprocal = Voice.reflexive

def Voice.applicative : Voice

The applicative nucleativizes an applied participant as a second P beside the initial A and P ([Cre24] §8.3.5).

Equations

• Voice.applicative = Voice.of ArgumentFrame.np ArgumentFrame.np_np [some ArgumentFrame.Slot.external, some (ArgumentFrame.Slot.complement 0), some (ArgumentFrame.Slot.complement 1)]

def Voice.patientVoice : Voice

The patient voice of a symmetrical system leaves the transitive construction unchanged and makes the patient the pivot ([Cre24] §8.5.1).

Equations

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

def Voice.obliqueVoice (r : Case.Kind) : Voice

An oblique voice of a multiple symmetrical system leaves the transitive construction with an oblique marking a case of type r unchanged and makes the oblique the pivot ([Cre24] §8.5.2).

Equations

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

@[reducible, inline]

abbrev Voice.locativeVoice : Voice

The locative voice is the oblique voice of a spatial oblique.

Equations

• Voice.locativeVoice = Voice.obliqueVoice Case.Kind.spatial

Properties of the voices

theorem Voice.causative_isValencyIncreasing : causative.IsValencyIncreasing

theorem Voice.anticausative_isValencyDecreasing : anticausative.IsValencyDecreasing

theorem Voice.passive_isValencyDecreasing : passive.IsValencyDecreasing

theorem Voice.passive_anticausative_fate : passive.fateOfRole TermRole.A = ParticipantFate.denucleativized ∧ anticausative.fateOfRole TermRole.A = ParticipantFate.suppressed

The passive maintains the initial A in participant structure; the anticausative suppresses it ([Cre24] §8.3.2.1).

theorem Voice.impersonalPassive_isImpersonal (fr : ArgumentFrame) : (impersonalPassive fr).IsImpersonal

theorem Voice.passive_not_isImpersonal : ¬passive.IsImpersonal

theorem Voice.antipassive_isValencyDecreasing : antipassive.IsValencyDecreasing

theorem Voice.reflexive_cumulates : reflexive.Cumulates

theorem Voice.applicative_isValencyIncreasing : applicative.IsValencyIncreasing

theorem Voice.patientVoice_isSymmetrical : patientVoice.IsSymmetrical

theorem Voice.obliqueVoice_isSymmetrical (r : Case.Kind) : (obliqueVoice r).IsSymmetrical

theorem Voice.obliqueVoice_selectsOblique (r : Case.Kind) : (obliqueVoice r).SelectsOblique

Alternating verbs

def Voice.Relates {v : Voice} {n : ℕ} (c d : Diathesis n) : Prop

A voice relates two diatheses of a verb when their frames refine its initial and derived frames and each participant moves as the voice says: a participant of an initial slot to the derived slot the voice sends it to, out of the construction where it sends it nowhere, and a participant the first diathesis leaves out to a derived slot no initial slot reaches, if any.

Equations

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

@[instance_reducible]

instance Voice.instDecidableRelates {v : Voice} {n : ℕ} (c d : Diathesis n) : Decidable (Relates c d)

Equations

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

def Verb.Alternates (w : Verb) (v : Voice) : Prop

The verb alternates by v when the voice relates two of its diatheses.

Equations

• w.Alternates v = ∃ c ∈ w.valency.diatheses, ∃ d ∈ w.valency.diatheses, Voice.Relates c d

@[instance_reducible]

instance Voice.instDecidableAlternates (w : Verb) (v : Voice) : Decidable (w.Alternates v)

Deciding the alternation skips a diathesis whose frame does not refine the initial one before looking for a derived one.

Equations

• Voice.instDecidableAlternates w v = decidable_of_iff (∃ c ∈ w.valency.diatheses, v.initial.toArgumentFrame ≤ c.toArgumentFrame ∧ ∃ d ∈ w.valency.diatheses, Voice.Relates c d) ⋯

Alignment

inductive Voice.Alignment : Type

The alignment of the core terms of transitive and intransitive clauses codes S like A or like P ([Cre24] §1.3.4).

• A_alignment : Alignment

  S is coded like A, traditionally accusative.

• P_alignment : Alignment

  S is coded like P, traditionally ergative.

@[instance_reducible]

instance Voice.instDecidableEqAlignment : DecidableEq Alignment

Equations

• Voice.instDecidableEqAlignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Voice.instReprAlignment.repr : Alignment → ℕ → Std.Format

Equations

• Voice.instReprAlignment.repr Voice.Alignment.A_alignment prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.Alignment.A_alignment")).group prec✝
• Voice.instReprAlignment.repr Voice.Alignment.P_alignment prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Voice.Alignment.P_alignment")).group prec✝

@[instance_reducible]

instance Voice.instReprAlignment : Repr Alignment

Equations

• Voice.instReprAlignment = { reprPrec := Voice.instReprAlignment.repr }