Voice System

@cite{erlewine-2018}

Theory-neutral types for cross-linguistic voice system typology --- how languages map argument roles to a privileged syntactic position (the "pivot") via voice alternation.

Languages vary in:

• How many voices they have (2 in Toba Batak, 4+ in Tagalog)
• Which roles can be promoted to pivot (agent/patient only, or also locative, instrumental, benefactive, circumstantial)
• Whether the system is symmetrical --- in symmetrical systems (Toba Batak, Tagalog), no voice is morphologically or syntactically basic; in asymmetrical systems (English active/passive), one voice is marked

inductive Interfaces.PivotTarget : Type

Which argument role can be promoted to pivot in a given voice.

Finer-grained than ArgumentRole: Philippine-type systems distinguish locative, instrumental, benefactive, and circumstantial pivots, all of which collapse to ArgumentRole.oblique.

• agent : PivotTarget
• patient : PivotTarget
• locative : PivotTarget
• instrumental : PivotTarget
• benefactive : PivotTarget
• circumstantial : PivotTarget

@[implicit_reducible]

instance Interfaces.instDecidableEqPivotTarget : DecidableEq PivotTarget

Equations

• Interfaces.instDecidableEqPivotTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Interfaces.instReprPivotTarget.repr : PivotTarget → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Interfaces.instReprPivotTarget : Repr PivotTarget

Equations

• Interfaces.instReprPivotTarget = { reprPrec := Interfaces.instReprPivotTarget.repr }

def Interfaces.PivotTarget.toArgumentRole : PivotTarget → Typology.ArgumentRole

Coercion from PivotTarget to ArgumentRole.

Locative, instrumental, benefactive, and circumstantial all collapse to oblique --- the distinction among obliques is a voice-system concern, not an extraction-morphology concern.

Equations

• Interfaces.PivotTarget.agent.toArgumentRole = Typology.ArgumentRole.agent
• Interfaces.PivotTarget.patient.toArgumentRole = Typology.ArgumentRole.patient
• Interfaces.PivotTarget.locative.toArgumentRole = Typology.ArgumentRole.oblique
• Interfaces.PivotTarget.instrumental.toArgumentRole = Typology.ArgumentRole.oblique
• Interfaces.PivotTarget.benefactive.toArgumentRole = Typology.ArgumentRole.oblique
• Interfaces.PivotTarget.circumstantial.toArgumentRole = Typology.ArgumentRole.oblique

structure Interfaces.VoiceEntry : Type

A single voice in a voice system: a name and the role it promotes.

• name : String

  Name of the voice (e.g., "Actor Voice", "Patient Voice")

• promotes : PivotTarget

  Which argument role this voice promotes to pivot

def Interfaces.instDecidableEqVoiceEntry.decEq (x✝ x✝¹ : VoiceEntry) : Decidable (x✝ = x✝¹)

Equations

• Interfaces.instDecidableEqVoiceEntry.decEq { name := a, promotes := a_1 } { name := b, promotes := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Interfaces.instDecidableEqVoiceEntry : DecidableEq VoiceEntry

Equations

• Interfaces.instDecidableEqVoiceEntry = Interfaces.instDecidableEqVoiceEntry.decEq

def Interfaces.instReprVoiceEntry.repr : VoiceEntry → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Interfaces.instReprVoiceEntry : Repr VoiceEntry

Equations

• Interfaces.instReprVoiceEntry = { reprPrec := Interfaces.instReprVoiceEntry.repr }

inductive Interfaces.VoiceSystemSymmetry : Type

Whether a voice system is symmetrical or asymmetrical.

• Symmetrical: no voice is morphologically or syntactically basic; all voices have equal status (e.g., Tagalog, Toba Batak)
• Asymmetrical: one voice (typically active) is basic/unmarked and the other(s) are derived (e.g., English active/passive)

• symmetrical : VoiceSystemSymmetry
• asymmetrical : VoiceSystemSymmetry

@[implicit_reducible]

instance Interfaces.instDecidableEqVoiceSystemSymmetry : DecidableEq VoiceSystemSymmetry

Equations

• Interfaces.instDecidableEqVoiceSystemSymmetry x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Interfaces.instReprVoiceSystemSymmetry : Repr VoiceSystemSymmetry

Equations

• Interfaces.instReprVoiceSystemSymmetry = { reprPrec := Interfaces.instReprVoiceSystemSymmetry.repr }

def Interfaces.instReprVoiceSystemSymmetry.repr : VoiceSystemSymmetry → Nat → Std.Format

Equations

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

structure Interfaces.VoiceSystemProfile : Type

A language's voice system profile: its inventory of voices, symmetry type, and descriptive notes.

• language : String

  Language name

• voices : List VoiceEntry

  The voices in the system

• symmetry : VoiceSystemSymmetry

  Symmetrical or asymmetrical

• notes : String

  Notes

@[implicit_reducible]

instance Interfaces.instReprVoiceSystemProfile : Repr VoiceSystemProfile

Equations

• Interfaces.instReprVoiceSystemProfile = { reprPrec := Interfaces.instReprVoiceSystemProfile.repr }

def Interfaces.instReprVoiceSystemProfile.repr : VoiceSystemProfile → Nat → Std.Format

Equations

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

def Interfaces.VoiceSystemProfile.voiceCount (p : VoiceSystemProfile) : Nat

How many voices does this system have?

Equations

• p.voiceCount = p.voices.length

def Interfaces.VoiceSystemProfile.promotesRole (p : VoiceSystemProfile) (r : PivotTarget) : Prop

Does any voice in this system promote a given role?

Equations

• p.promotesRole r = ∃ (v : Interfaces.VoiceEntry), v ∈ p.voices ∧ v.promotes = r

@[implicit_reducible]

instance Interfaces.instDecidablePromotesRole (p : VoiceSystemProfile) (r : PivotTarget) : Decidable (p.promotesRole r)

Equations

• Interfaces.instDecidablePromotesRole p r = Interfaces.instDecidablePromotesRole._aux_1 p r

def Interfaces.VoiceSystemProfile.distinguishesObliques (p : VoiceSystemProfile) : Prop

Does this system distinguish among oblique pivots (locative, instrumental, benefactive, circumstantial)?

Equations

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

@[implicit_reducible]

instance Interfaces.instDecidableDistinguishesObliques (p : VoiceSystemProfile) : Decidable p.distinguishesObliques

Equations

• Interfaces.instDecidableDistinguishesObliques p = Interfaces.instDecidableDistinguishesObliques._aux_1 p

def Interfaces.VoiceSystemProfile.isActivePassive (p : VoiceSystemProfile) : Prop

Is this a simple active/passive system (exactly agent + patient)?

Equations

• p.isActivePassive = (p.voiceCount = 2 ∧ p.promotesRole Interfaces.PivotTarget.agent ∧ p.promotesRole Interfaces.PivotTarget.patient)

@[implicit_reducible]

instance Interfaces.instDecidableIsActivePassive (p : VoiceSystemProfile) : Decidable p.isActivePassive

Equations

• Interfaces.instDecidableIsActivePassive p = Interfaces.instDecidableIsActivePassive._aux_1 p

def Interfaces.VoiceSystemProfile.promotableRoles (p : VoiceSystemProfile) : List PivotTarget

The set of roles promotable to pivot in this system.

Equations

• p.promotableRoles = (List.map (fun (x : Interfaces.VoiceEntry) => x.promotes) p.voices).eraseDups