Argument Realization and Suppression

General types for describing how arguments are suppressed and realized in voice alternations. These capture two independent dimensions:

1. Suppressed variable interpretation: whether a suppressed argument is interpreted as coreferent with the surface subject (reflexive) or disjoint (dispositional/passive).

2. Object realization: whether the internal argument is realized as a full DP (functional application) or an incorporated NP (head-adjunction to V).

The cross-product of these two dimensions yields a 2×2 typology of middle constructions, first articulated for Indonesian ber- by @cite{beavers-udayana-2022} but applicable cross-linguistically.

inductive Semantics.Events.ArgumentRealization.SuppressedVarReading : Type

How a suppressed argument variable is interpreted vis-à-vis the surface subject.

• coreferent : SuppressedVarReading

  The suppressed variable is interpreted as coreferent with the surface subject, yielding a reflexive reading.

• disjoint : SuppressedVarReading

  The suppressed variable is interpreted as disjoint from the surface subject, yielding a dispositional/passive reading.

instance Semantics.Events.ArgumentRealization.instDecidableEqSuppressedVarReading : DecidableEq SuppressedVarReading

Equations

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

instance Semantics.Events.ArgumentRealization.instBEqSuppressedVarReading : BEq SuppressedVarReading

Equations

• Semantics.Events.ArgumentRealization.instBEqSuppressedVarReading = { beq := Semantics.Events.ArgumentRealization.instBEqSuppressedVarReading.beq }

def Semantics.Events.ArgumentRealization.instBEqSuppressedVarReading.beq : SuppressedVarReading → SuppressedVarReading → Bool

Equations

• Semantics.Events.ArgumentRealization.instBEqSuppressedVarReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Events.ArgumentRealization.instReprSuppressedVarReading.repr : SuppressedVarReading → Nat → Std.Format

Equations

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

instance Semantics.Events.ArgumentRealization.instReprSuppressedVarReading : Repr SuppressedVarReading

Equations

• Semantics.Events.ArgumentRealization.instReprSuppressedVarReading = { reprPrec := Semantics.Events.ArgumentRealization.instReprSuppressedVarReading.repr }

inductive Semantics.Events.ArgumentRealization.ObjectRealization : Type

How the base object is syntactically realized.

• incorporation : ObjectRealization

  Object = incorporated NP (head-adjoined to V).

• noIncorporation : ObjectRealization

  Object = full DP (functional application).

instance Semantics.Events.ArgumentRealization.instDecidableEqObjectRealization : DecidableEq ObjectRealization

Equations

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

def Semantics.Events.ArgumentRealization.instBEqObjectRealization.beq : ObjectRealization → ObjectRealization → Bool

Equations

• Semantics.Events.ArgumentRealization.instBEqObjectRealization.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Events.ArgumentRealization.instBEqObjectRealization : BEq ObjectRealization

Equations

• Semantics.Events.ArgumentRealization.instBEqObjectRealization = { beq := Semantics.Events.ArgumentRealization.instBEqObjectRealization.beq }

def Semantics.Events.ArgumentRealization.instReprObjectRealization.repr : ObjectRealization → Nat → Std.Format

Equations

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

instance Semantics.Events.ArgumentRealization.instReprObjectRealization : Repr ObjectRealization

Equations

• Semantics.Events.ArgumentRealization.instReprObjectRealization = { reprPrec := Semantics.Events.ArgumentRealization.instReprObjectRealization.repr }

structure Semantics.Events.ArgumentRealization.MiddleType : Type

A middle type classified by two independent dimensions: how the suppressed variable is interpreted and how the object is realized.

• objRealization : ObjectRealization
• suppressedVar : SuppressedVarReading

instance Semantics.Events.ArgumentRealization.instDecidableEqMiddleType : DecidableEq MiddleType

Equations

• Semantics.Events.ArgumentRealization.instDecidableEqMiddleType = Semantics.Events.ArgumentRealization.instDecidableEqMiddleType.decEq

def Semantics.Events.ArgumentRealization.instDecidableEqMiddleType.decEq (x✝ x✝¹ : MiddleType) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Events.ArgumentRealization.instBEqMiddleType : BEq MiddleType

Equations

• Semantics.Events.ArgumentRealization.instBEqMiddleType = { beq := Semantics.Events.ArgumentRealization.instBEqMiddleType.beq }

def Semantics.Events.ArgumentRealization.instBEqMiddleType.beq : MiddleType → MiddleType → Bool

Equations

• Semantics.Events.ArgumentRealization.instBEqMiddleType.beq { objRealization := a, suppressedVar := a_1 } { objRealization := b, suppressedVar := b_1 } = (a == b && a_1 == b_1)
• Semantics.Events.ArgumentRealization.instBEqMiddleType.beq x✝¹ x✝ = false

def Semantics.Events.ArgumentRealization.instReprMiddleType.repr : MiddleType → Nat → Std.Format

Equations

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

instance Semantics.Events.ArgumentRealization.instReprMiddleType : Repr MiddleType

Equations

• Semantics.Events.ArgumentRealization.instReprMiddleType = { reprPrec := Semantics.Events.ArgumentRealization.instReprMiddleType.repr }

def Semantics.Events.ArgumentRealization.MiddleType.agentSurfaces (m : MiddleType) : Bool

Which argument surfaces as subject in a middle construction depends on object realization, not on the suppression operation itself.

• Incorporation: agent surfaces (patient is incorporated)
• No incorporation: patient surfaces (agent is suppressed)

This connects the MiddleType typology to the voice system's PivotTarget (@cite{beavers-udayana-2022}, (32d)).

Equations

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