Voice system typology

[Erl18]

Theory-neutral types for cross-linguistic voice-system typology — how languages map argument roles to a privileged syntactic position (the "pivot") via voice alternation. Per-language data are bare def voices : List VoiceEntry and def symmetry : VoiceSystemSymmetry in Fragments/<Lang>/…; the queries below operate on the voice list.

Main definitions

• PivotTarget : the role a voice promotes to pivot (finer than ArgumentRole).
• VoiceEntry, VoiceSystemSymmetry : one voice (name + promoted role); system symmetry.
• Voice.voiceCount / promotesRole / distinguishesObliques / isActivePassive / promotableRoles : queries over a language's List VoiceEntry.

Pivot target

inductive Voice.PivotTarget : Type

Which argument role a voice promotes to pivot. Finer-grained than Extraction.ArgumentRole: Philippine-type systems distinguish locative, instrumental, benefactive, and circumstantial pivots, all collapsing to oblique.

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

@[implicit_reducible]

instance Voice.instDecidableEqPivotTarget : DecidableEq PivotTarget

Equations

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

@[implicit_reducible]

instance Voice.instReprPivotTarget : Repr PivotTarget

Equations

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

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

Equations

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

def Voice.PivotTarget.toArgumentRole : PivotTarget → Extraction.ArgumentRole

Coarsen a PivotTarget to a Extraction.ArgumentRole (obliques collapse).

Equations

• Voice.PivotTarget.agent.toArgumentRole = Extraction.ArgumentRole.agent
• Voice.PivotTarget.patient.toArgumentRole = Extraction.ArgumentRole.patient
• Voice.PivotTarget.locative.toArgumentRole = Extraction.ArgumentRole.oblique
• Voice.PivotTarget.instrumental.toArgumentRole = Extraction.ArgumentRole.oblique
• Voice.PivotTarget.benefactive.toArgumentRole = Extraction.ArgumentRole.oblique
• Voice.PivotTarget.circumstantial.toArgumentRole = Extraction.ArgumentRole.oblique

Voice entry and symmetry

structure Voice.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.

@[implicit_reducible]

instance Voice.instDecidableEqVoiceEntry : DecidableEq VoiceEntry

Equations

• Voice.instDecidableEqVoiceEntry = Voice.instDecidableEqVoiceEntry.decEq

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

Equations

• Voice.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 ⋯

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

Equations

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

@[implicit_reducible]

instance Voice.instReprVoiceEntry : Repr VoiceEntry

Equations

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

inductive Voice.VoiceSystemSymmetry : Type

Whether a voice system is symmetrical (no basic voice, e.g. Tagalog) or asymmetrical (one basic voice, e.g. English active/passive).

• symmetrical : VoiceSystemSymmetry
• asymmetrical : VoiceSystemSymmetry

@[implicit_reducible]

instance Voice.instDecidableEqVoiceSystemSymmetry : DecidableEq VoiceSystemSymmetry

Equations

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

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

Equations

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

@[implicit_reducible]

instance Voice.instReprVoiceSystemSymmetry : Repr VoiceSystemSymmetry

Equations

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

Queries over a voice inventory

def Voice.voiceCount (voices : List VoiceEntry) : Nat

How many voices a system has.

Equations

• Voice.voiceCount voices = voices.length

def Voice.promotesRole (voices : List VoiceEntry) (r : PivotTarget) : Prop

Does any voice promote a given role?

Equations

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

@[implicit_reducible]

instance Voice.instDecidablePromotesRole (voices : List VoiceEntry) (r : PivotTarget) : Decidable (promotesRole voices r)

Equations

• Voice.instDecidablePromotesRole voices r = Voice.instDecidablePromotesRole._aux_1 voices r

def Voice.distinguishesObliques (voices : List VoiceEntry) : Prop

Does the 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 Voice.instDecidableDistinguishesObliques (voices : List VoiceEntry) : Decidable (distinguishesObliques voices)

Equations

• Voice.instDecidableDistinguishesObliques voices = Voice.instDecidableDistinguishesObliques._aux_1 voices

def Voice.isActivePassive (voices : List VoiceEntry) : Prop

A simple active/passive system: exactly agent + patient.

Equations

• Voice.isActivePassive voices = (Voice.voiceCount voices = 2 ∧ Voice.promotesRole voices Voice.PivotTarget.agent ∧ Voice.promotesRole voices Voice.PivotTarget.patient)

@[implicit_reducible]

instance Voice.instDecidableIsActivePassive (voices : List VoiceEntry) : Decidable (isActivePassive voices)

Equations

• Voice.instDecidableIsActivePassive voices = Voice.instDecidableIsActivePassive._aux_1 voices

def Voice.promotableRoles (voices : List VoiceEntry) : List PivotTarget

The roles promotable to pivot in a system.

Equations

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