Voice: middle constructions

[BU22]

The middle/diathesis axis of the unified Voice substrate: the two orthogonal dimensions of [BU22]'s Indonesian middle typology — how a suppressed argument is interpreted, and how the base object is realized. The 2×2 of constructions is the literal product ObjectRealization × SuppressedVarReading (no bundling record). Which argument surfaces as pivot is derived from object realization via ObjectRealization.pivot.

inductive Voice.SuppressedVarReading : Type

How a suppressed argument variable is interpreted vis-à-vis the surface subject: coreferent (reflexive) or disjoint (dispositional/passive).

• coreferent : SuppressedVarReading
• disjoint : SuppressedVarReading

@[implicit_reducible]

instance Voice.instDecidableEqSuppressedVarReading : DecidableEq SuppressedVarReading

Equations

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

@[implicit_reducible]

instance Voice.instReprSuppressedVarReading : Repr SuppressedVarReading

Equations

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

def Voice.instReprSuppressedVarReading.repr : SuppressedVarReading → Nat → Std.Format

Equations

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

inductive Voice.ObjectRealization : Type

How the base object is realized: incorporated NP (head-adjoined to V) or full DP (functional application).

• incorporation : ObjectRealization
• noIncorporation : ObjectRealization

@[implicit_reducible]

instance Voice.instDecidableEqObjectRealization : DecidableEq ObjectRealization

Equations

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

def Voice.instReprObjectRealization.repr : ObjectRealization → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Voice.instReprObjectRealization : Repr ObjectRealization

Equations

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

def Voice.ObjectRealization.pivot : ObjectRealization → PivotTarget

The pivot a middle promotes, derived from object realization: incorporation leaves the agent surfacing, no-incorporation leaves the patient ([BU22]).

Equations

• Voice.ObjectRealization.incorporation.pivot = Voice.PivotTarget.agent
• Voice.ObjectRealization.noIncorporation.pivot = Voice.PivotTarget.patient

def Voice.ObjectRealization.agentSurfaces (o : ObjectRealization) : Prop

Does the agent surface as subject? (Equivalently, the object is incorporated.)

Equations

• o.agentSurfaces = (o = Voice.ObjectRealization.incorporation)

@[implicit_reducible]

instance Voice.instDecidablePredObjectRealizationAgentSurfaces : DecidablePred ObjectRealization.agentSurfaces

Equations

• Voice.instDecidablePredObjectRealizationAgentSurfaces o = decEq o Voice.ObjectRealization.incorporation