Japanese Passive Types

@cite{jo-seo-2023} @cite{ozaki-2026}

Japanese has two structurally distinct passive constructions that look superficially similar (both use -(r)are-):

• Direct passive (-niyotte agent): valency-reducing, requires thematic Voice. Only available for verbs that project an external argument.
• Indirect (adversative) passive (-ni agent): introduces a malefactive argument. Available for ALL verbs, including unaccusatives and intransitives.

The niyotte substitution test distinguishes them: direct passives allow the dative agent marker ni to be replaced with niyotte; indirect passives do not (@cite{jo-seo-2023}).

inductive Fragments.Japanese.Passive.PassiveType : Type

Types of passive in Japanese.

• direct : PassiveType
• indirect : PassiveType

@[implicit_reducible]

instance Fragments.Japanese.Passive.instDecidableEqPassiveType : DecidableEq PassiveType

Equations

• Fragments.Japanese.Passive.instDecidableEqPassiveType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Japanese.Passive.instReprPassiveType : Repr PassiveType

Equations

• Fragments.Japanese.Passive.instReprPassiveType = { reprPrec := Fragments.Japanese.Passive.instReprPassiveType.repr }

def Fragments.Japanese.Passive.instReprPassiveType.repr : PassiveType → Nat → Std.Format

Equations

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

def Fragments.Japanese.Passive.PassiveType.requiresThematicVoice : PassiveType → Bool

Direct passive requires thematic Voice (an agentive external argument).

Equations

• Fragments.Japanese.Passive.PassiveType.direct.requiresThematicVoice = true
• Fragments.Japanese.Passive.PassiveType.indirect.requiresThematicVoice = false