Voice System Interface

@cite{erlewine-2018} @cite{foley-2008}

Theory-neutral interface 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

This interface captures the alignment dimension of voice systems: which argument roles can be promoted, and is the system symmetrical? It complements ExtractionMorphology (which captures how extraction is marked) and Minimalism.VoiceFlavor (which captures the semantic contribution of the voice head).

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

instance Interfaces.instDecidableEqPivotTarget : DecidableEq PivotTarget

Equations

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

instance Interfaces.instBEqPivotTarget : BEq PivotTarget

Equations

• Interfaces.instBEqPivotTarget = { beq := Interfaces.instBEqPivotTarget.beq }

def Interfaces.instBEqPivotTarget.beq : PivotTarget → PivotTarget → Bool

Equations

• Interfaces.instBEqPivotTarget.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Interfaces.instReprPivotTarget : Repr PivotTarget

Equations

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

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

Equations

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

def Interfaces.PivotTarget.toArgumentRole : PivotTarget → 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 = Interfaces.ArgumentRole.agent
• Interfaces.PivotTarget.patient.toArgumentRole = Interfaces.ArgumentRole.patient
• Interfaces.PivotTarget.locative.toArgumentRole = Interfaces.ArgumentRole.oblique
• Interfaces.PivotTarget.instrumental.toArgumentRole = Interfaces.ArgumentRole.oblique
• Interfaces.PivotTarget.benefactive.toArgumentRole = Interfaces.ArgumentRole.oblique
• Interfaces.PivotTarget.circumstantial.toArgumentRole = Interfaces.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

instance Interfaces.instDecidableEqVoiceEntry : DecidableEq VoiceEntry

Equations

• Interfaces.instDecidableEqVoiceEntry = Interfaces.instDecidableEqVoiceEntry.decEq

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 ⋯

instance Interfaces.instBEqVoiceEntry : BEq VoiceEntry

Equations

• Interfaces.instBEqVoiceEntry = { beq := Interfaces.instBEqVoiceEntry.beq }

def Interfaces.instBEqVoiceEntry.beq : VoiceEntry → VoiceEntry → Bool

Equations

• Interfaces.instBEqVoiceEntry.beq { name := a, promotes := a_1 } { name := b, promotes := b_1 } = (a == b && a_1 == b_1)
• Interfaces.instBEqVoiceEntry.beq x✝¹ x✝ = false

instance Interfaces.instReprVoiceEntry : Repr VoiceEntry

Equations

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

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

Equations

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

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

instance Interfaces.instDecidableEqVoiceSystemSymmetry : DecidableEq VoiceSystemSymmetry

Equations

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

def Interfaces.instBEqVoiceSystemSymmetry.beq : VoiceSystemSymmetry → VoiceSystemSymmetry → Bool

Equations

• Interfaces.instBEqVoiceSystemSymmetry.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Interfaces.instBEqVoiceSystemSymmetry : BEq VoiceSystemSymmetry

Equations

• Interfaces.instBEqVoiceSystemSymmetry = { beq := Interfaces.instBEqVoiceSystemSymmetry.beq }

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

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) : Bool

Does any voice in this system promote a given role?

Equations

• p.promotesRole r = p.voices.any fun (x : Interfaces.VoiceEntry) => x.promotes == r

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

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

Equations

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

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

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)

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