Indonesian Verbal Predicates

@cite{sneddon-1996} @cite{beavers-udayana-2022}

Indonesian verb entries with voice paradigm forms (meN-, ber-, ter-, di-), root class annotations from @cite{beavers-udayana-2022}, and ter- semantic classification (stative, accidental, abilitative) from @cite{sneddon-1996} §1.265–1.275.

Root classes

The paper distinguishes three root classes that determine the default interpretation of the suppressed variable z in ber- middles:

• Reflexive roots (body care/grooming): the conventional expectation is self-action, so the default reading of z is coreferent with the surface subject. Examples: dandan 'dress', cukur 'shave'.
• Obviative roots (all others): the conventional expectation is disjoint reference, so the default reading is dispositional/passive. Examples: jual 'sell', masak 'cook'.
• Causer-unspecified roots (change-of-state without entailed external cause): the verb does not entail an external causer, and ber- surfaces as ter- with an anticausative reading. Examples: buka 'open', pecah 'break'.

ter- classification (@cite{sneddon-1996} §1.265–1.275)

The prefix ter- has three semantic categories:

• Stative (§1.266): result state, no agent (terbuka 'open', tertulis 'written')
• Accidental (§1.267–1.270): unintended action (terbawa 'accidentally carried')
• Abilitative (§1.272): ability (terdengar 'audible', tidak terbeli 'unaffordable')

These connect to linglib's semantic infrastructure: accidental ter- maps to Volitionality.nonvolitional, abilitative ter- expresses circumstantial modality, and stative ter- is agentless.

Incorporation

Some verbs additionally license noun incorporation (ber-V=NP), where the incorporated NP classifies the patient. Body-part nouns are the most productive class. When diri 'self' is incorporated, a reflexive reading arises even for obviative roots.

inductive Fragments.Indonesian.Predicates.RootClass : Type

Root class of Indonesian verbs, determining the default interpretation of the suppressed variable in ber- middles (@cite{beavers-udayana-2022}, §3.5, table (58)).

• reflexive : RootClass

  Body care/grooming verbs: default coreferent (z = surface subject).

• obviative : RootClass

  All other transitive verbs: default disjoint (z ≠ surface subject).

• causerUnspecified : RootClass

  Change-of-state verbs without entailed external cause: anticausative via ter-. The causer is left unspecified in the verb root.

instance Fragments.Indonesian.Predicates.instDecidableEqRootClass : DecidableEq RootClass

Equations

• Fragments.Indonesian.Predicates.instDecidableEqRootClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Indonesian.Predicates.instBEqRootClass.beq : RootClass → RootClass → Bool

Equations

• Fragments.Indonesian.Predicates.instBEqRootClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Indonesian.Predicates.instBEqRootClass : BEq RootClass

Equations

• Fragments.Indonesian.Predicates.instBEqRootClass = { beq := Fragments.Indonesian.Predicates.instBEqRootClass.beq }

instance Fragments.Indonesian.Predicates.instReprRootClass : Repr RootClass

Equations

• Fragments.Indonesian.Predicates.instReprRootClass = { reprPrec := Fragments.Indonesian.Predicates.instReprRootClass.repr }

def Fragments.Indonesian.Predicates.instReprRootClass.repr : RootClass → ℕ → Std.Format

Equations

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

def Fragments.Indonesian.Predicates.RootClass.defaultReading : RootClass → Semantics.Events.ArgumentRealization.SuppressedVarReading

The root class predicts the default reading of the suppressed variable in non-incorporation ber- forms.

Equations

• Fragments.Indonesian.Predicates.RootClass.reflexive.defaultReading = Semantics.Events.ArgumentRealization.SuppressedVarReading.coreferent
• Fragments.Indonesian.Predicates.RootClass.obviative.defaultReading = Semantics.Events.ArgumentRealization.SuppressedVarReading.disjoint
• Fragments.Indonesian.Predicates.RootClass.causerUnspecified.defaultReading = Semantics.Events.ArgumentRealization.SuppressedVarReading.disjoint

inductive Fragments.Indonesian.Predicates.TerClass : Type

The three semantic categories of ter- verbs, following @cite{sneddon-1996} §1.265–1.275.

• Stative (§1.266): refers to a resulting state, not an action. No agent is possible. Corresponds to di- passives but describes the state rather than the action: tertulis 'written (in a state)' vs ditulis 'written (by someone)'.
• Accidental (§1.267–1.270): unintended, involuntary action. Contrasts with deliberate di-: tertinggal 'left accidentally' vs ditinggalkan 'left deliberately'. Can be intransitive or transitive. Suffixes (-kan, -i) are usually dropped.
• Abilitative (§1.272): indicates ability to perform the action. Almost always negated: tidak terbeli 'can't afford'. Suffixes (-kan, -i) are regularly retained. Expresses circumstantial possibility (Kratzer's modal flavor).

Some verbs are ambiguous across categories (§1.273): terbuka is primarily stative ('open') but can be accidental ('opened by accident') or abilitative ('managed to open'). The terClass field records the primary/default reading.

• stative : TerClass

  Result state: no agent, no action — the state following an event.

• accidental : TerClass

  Unintended/involuntary action: the agent exists but did not intend the action. Suffixes usually dropped.

• abilitative : TerClass

  Ability: the agent can (or usually cannot) perform the action. Suffixes retained. Expresses circumstantial modality.

instance Fragments.Indonesian.Predicates.instDecidableEqTerClass : DecidableEq TerClass

Equations

• Fragments.Indonesian.Predicates.instDecidableEqTerClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Indonesian.Predicates.instBEqTerClass.beq : TerClass → TerClass → Bool

Equations

• Fragments.Indonesian.Predicates.instBEqTerClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Indonesian.Predicates.instBEqTerClass : BEq TerClass

Equations

• Fragments.Indonesian.Predicates.instBEqTerClass = { beq := Fragments.Indonesian.Predicates.instBEqTerClass.beq }

instance Fragments.Indonesian.Predicates.instReprTerClass : Repr TerClass

Equations

• Fragments.Indonesian.Predicates.instReprTerClass = { reprPrec := Fragments.Indonesian.Predicates.instReprTerClass.repr }

def Fragments.Indonesian.Predicates.instReprTerClass.repr : TerClass → ℕ → Std.Format

Equations

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

def Fragments.Indonesian.Predicates.TerClass.hasAgent : TerClass → Bool

Whether the ter- reading entails the existence of an agent. Stative ter- is agentless (no oleh 'by' phrase possible); accidental and abilitative ter- allow an (often pronoun) agent (@cite{sneddon-1996} §1.266 vs §1.269, §1.272).

Equations

• Fragments.Indonesian.Predicates.TerClass.stative.hasAgent = false
• Fragments.Indonesian.Predicates.TerClass.accidental.hasAgent = true
• Fragments.Indonesian.Predicates.TerClass.abilitative.hasAgent = true

def Fragments.Indonesian.Predicates.TerClass.volitionality : TerClass → Volitionality

The volitionality entailed by a ter- reading. Accidental ter- explicitly encodes nonvolitional action; stative and abilitative are neutral (stative has no agent, abilitative is about capacity not intention).

Equations

• Fragments.Indonesian.Predicates.TerClass.stative.volitionality = Volitionality.neutral
• Fragments.Indonesian.Predicates.TerClass.accidental.volitionality = Volitionality.nonvolitional
• Fragments.Indonesian.Predicates.TerClass.abilitative.volitionality = Volitionality.neutral

def Fragments.Indonesian.Predicates.TerClass.retainsSuffix : TerClass → Bool

Whether transitive suffixes (-kan, -i) are retained in the ter- form. Abilitative ter- regularly retains suffixes: terpecahkan 'can be solved', terhindarkan 'can be avoided' (§1.272, §1.274). Accidental ter- usually drops them: terpikir not terpikirkan for the accidental reading (§1.270, §1.274). Stative ter- has no suffix to retain (§1.266).

Equations

• Fragments.Indonesian.Predicates.TerClass.stative.retainsSuffix = false
• Fragments.Indonesian.Predicates.TerClass.accidental.retainsSuffix = false
• Fragments.Indonesian.Predicates.TerClass.abilitative.retainsSuffix = true

structure Fragments.Indonesian.Predicates.IndonesianVerbEntryextends Core.Verbs.VerbCore : Type

An Indonesian verb entry extending VerbCore with voice paradigm forms.

Voice prefixes follow @cite{sneddon-1996} (§1.167–177 for ber-, §1.265–275 for ter-, §3.26–40 for active/passive voice):

• meN-: agent voice / active (@cite{sneddon-1996} §3.26)
• di-: patient voice / passive (@cite{sneddon-1996} §3.27–28)
• ber-: middle voice — reflexive, dispositional, incorporation (@cite{beavers-udayana-2022})
• ter-: stative / accidental / abilitative (@cite{sneddon-1996} §1.265–275); analyzed as anticausative for causer-unspecified roots by @cite{beavers-udayana-2022}

• form : String
• complementType : ComplementType
• subjectEntailments : Option Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile
• objectEntailments : Option Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile
• controlType : ControlType
• altComplementType : Option ComplementType
• altControlType : ControlType
• unaccusative : Bool
• voiceType : Option VoiceType
• passivizable : Bool
• implicitObj : Option ImplicitInterp
• implicitGoal : Option ImplicitInterp
• speechActVerb : Bool
• vendlerClass : Option Semantics.Tense.Aspect.LexicalAspect.VendlerClass
• degreeAchievementScale : Option Semantics.Lexical.Verb.DegreeAchievement.DegreeAchievementScale
• verbIncClass : Option Semantics.Events.Krifka1998.VerbIncClass
• presupType : Option PresupTriggerType
• projectionBehavior : Option ProjectionBehavior
• selectsDimension : Option Semantics.Probabilistic.Measurement.Dimension
• cosType : Option Semantics.Lexical.Verb.ChangeOfState.CoSType
• implicativeBuilder : Option Nadathur2024.Implicative.ImplicativeBuilder
• causativeBuilder : Option NadathurLauer2020.CausativeBuilder
• causalSource : Option Semantics.Causation.PsychCausation.CausalSource
• opaqueContext : Bool
• attitudeBuilder : Option AttitudeBuilder
• takesQuestionBase : Bool
• complementSig : Option NaturalLogic.EntailmentSig
• senseTag : SenseTag
• levinClass : Option LevinClass
• rootProfile : Option RootProfile
• formMeN : Option String

  Active voice meN- form (with allomorph selection).

• formBer : Option String

  Middle voice ber- form.

• formTer : Option String

  Anticausative / stative / accidental / abilitative ter- form.

• terClass : Option TerClass

  Semantic class of the ter- form (@cite{sneddon-1996} §1.265–1.275).

• formDi : Option String

  Passive voice di- form.

• rootClass : RootClass

  Root class determining default middle reading.

• incorporatedNPs : List String

  Body-part or lexical NPs that can incorporate with ber-.

• incorporatesDiri : Bool

  Whether diri 'self' can incorporate to force reflexive reading.

instance Fragments.Indonesian.Predicates.instReprIndonesianVerbEntry : Repr IndonesianVerbEntry

Equations

• Fragments.Indonesian.Predicates.instReprIndonesianVerbEntry = { reprPrec := Fragments.Indonesian.Predicates.instReprIndonesianVerbEntry.repr }

def Fragments.Indonesian.Predicates.instReprIndonesianVerbEntry.repr : IndonesianVerbEntry → ℕ → Std.Format

Equations

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

def Fragments.Indonesian.Predicates.instBEqIndonesianVerbEntry.beq : IndonesianVerbEntry → IndonesianVerbEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Indonesian.Predicates.instBEqIndonesianVerbEntry.beq x✝¹ x✝ = false

instance Fragments.Indonesian.Predicates.instBEqIndonesianVerbEntry : BEq IndonesianVerbEntry

Equations

• Fragments.Indonesian.Predicates.instBEqIndonesianVerbEntry = { beq := Fragments.Indonesian.Predicates.instBEqIndonesianVerbEntry.beq }

def Fragments.Indonesian.Predicates.jual : IndonesianVerbEntry

jual 'sell': core example of dispositional/passive ber- middle. Active: Dia men-jual mobil itu. 'S/he sold the car.' (the paper's (6a)) Middle: Mobil itu ber-jual dengan mudah. 'The car sells easily.' ((2b)) Also licenses: incorporation (ber-jual=baju (18b)), reflexive incorporation (ber-jual=diri (26b)).

Equations

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

def Fragments.Indonesian.Predicates.masak : IndonesianVerbEntry

masak 'cook': dispositional middle. Active: Dia me-masak. Middle: ber-masak. (the paper's table (4)).

Equations

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

def Fragments.Indonesian.Predicates.cuci : IndonesianVerbEntry

cuci 'wash': both dispositional and reflexive readings. Active: Dia men-cuci. Middle: ber-cuci. Also licenses body-part incorporation: ber-cuci=mata (18a). (the paper's table (4) and (18)).

Equations

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

def Fragments.Indonesian.Predicates.tambat : IndonesianVerbEntry

tambat 'tie': dispositional middle. Active: Dia men-(t)ambat kapal itu. 'S/he moored the boat.' ((5a)) Middle: Kapal itu ber-tambat dengan mudah. 'The boat moors easily.' ((5b)) (the paper's table (4)).

Equations

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

def Fragments.Indonesian.Predicates.dandan : IndonesianVerbEntry

dandan 'dress': canonical natural reflexive. Active: Tono men-dandan Ali. 'Tono dressed Ali.' ((3a)) Middle: Ali ber-dandan. 'Ali dressed.' ((2a)) Body care verb — default coreferent reading. (the paper's table (15)).

Equations

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

def Fragments.Indonesian.Predicates.cukur : IndonesianVerbEntry

cukur 'shave': natural reflexive. Active: men-cukur. Middle: ber-cukur. (the paper's table (15)).

Equations

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

def Fragments.Indonesian.Predicates.jemur : IndonesianVerbEntry

jemur 'sunbathe': natural reflexive. Active: men-jemur. Middle: ber-jemur. Optionally takes diri 'self': ber-jemur (diri) (@cite{sneddon-1996} §1.168; the paper's table (15)).

Equations

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

def Fragments.Indonesian.Predicates.sisir : IndonesianVerbEntry

sisir 'comb': natural reflexive. Active: meny-(s)isir. Middle: ber-sisir. (the paper's table (15)).

Equations

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

def Fragments.Indonesian.Predicates.buka : IndonesianVerbEntry

buka 'open': anticausative via ter-. Active: Dia mem-buka pintu. 'S/he opened the door.' Anticausative: Pintu itu ter-buka. 'The door opened.' ((2d)) Change-of-state verb without entailed external cause.

Equations

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

def Fragments.Indonesian.Predicates.pecah : IndonesianVerbEntry

pecah 'break': anticausative via ter-. Active: Dia mem-(p)ecah jendela. 'S/he broke the window.' Anticausative: Jendela itu ter-pecah. 'The window broke.' ((68)) (the paper's §5, (67)–(68)).

Equations

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

def Fragments.Indonesian.Predicates.tulis : IndonesianVerbEntry

tulis 'write': stative ter-. Active: Surat itu di-tulis(nya) dalam bahasa Inggris. 'That letter was written (by him) in English.' Stative: Surat itu ter-tulis dalam bahasa Inggris. 'That letter is written in English.' The ter- form describes the resulting state; the di- form describes the action. No agent (oleh) possible with stative ter-. (@cite{sneddon-1996} §1.266).

Equations

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

def Fragments.Indonesian.Predicates.bawa : IndonesianVerbEntry

bawa 'carry, bring': accidental ter-. Active: Dia mem-bawa koran saudara. 'He carried your newspaper.' Accidental: Maaf, koran saudara ter-bawa oleh saya. 'Sorry, I took your newspaper by mistake.' The accidental ter- form explicitly marks the action as unintended. Contrasts with deliberate di-bawa. Agent expressed with oleh (§1.269). (@cite{sneddon-1996} §1.269, §1.273).

Equations

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

def Fragments.Indonesian.Predicates.dengar : IndonesianVerbEntry

dengar 'hear': abilitative ter-. Active: Dia men-dengar suara dosen. 'He heard the lecturer's voice.' Abilitative: Suara dosen tidak ter-dengar dari sini. 'The lecturer can't be heard from here.' Abilitative ter- is usually negated, expressing inability. The negated form tidak terdengar corresponds to English 'inaudible'. (@cite{sneddon-1996} §1.272).

Equations

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

theorem Fragments.Indonesian.Predicates.reflexive_root_coreferent : RootClass.reflexive.defaultReading = Semantics.Events.ArgumentRealization.SuppressedVarReading.coreferent

Reflexive roots predict coreferent default reading.

theorem Fragments.Indonesian.Predicates.obviative_root_disjoint : RootClass.obviative.defaultReading = Semantics.Events.ArgumentRealization.SuppressedVarReading.disjoint

Obviative roots predict disjoint default reading.

theorem Fragments.Indonesian.Predicates.jual_is_obviative : jual.rootClass = RootClass.obviative

theorem Fragments.Indonesian.Predicates.masak_is_obviative : masak.rootClass = RootClass.obviative

theorem Fragments.Indonesian.Predicates.cuci_is_obviative : cuci.rootClass = RootClass.obviative

theorem Fragments.Indonesian.Predicates.tambat_is_obviative : tambat.rootClass = RootClass.obviative

theorem Fragments.Indonesian.Predicates.dandan_is_reflexive : dandan.rootClass = RootClass.reflexive

theorem Fragments.Indonesian.Predicates.cukur_is_reflexive : cukur.rootClass = RootClass.reflexive

theorem Fragments.Indonesian.Predicates.jemur_is_reflexive : jemur.rootClass = RootClass.reflexive

theorem Fragments.Indonesian.Predicates.sisir_is_reflexive : sisir.rootClass = RootClass.reflexive

theorem Fragments.Indonesian.Predicates.buka_is_causerUnspecified : buka.rootClass = RootClass.causerUnspecified

theorem Fragments.Indonesian.Predicates.pecah_is_causerUnspecified : pecah.rootClass = RootClass.causerUnspecified

theorem Fragments.Indonesian.Predicates.tulis_is_obviative : tulis.rootClass = RootClass.obviative

theorem Fragments.Indonesian.Predicates.bawa_is_obviative : bawa.rootClass = RootClass.obviative

theorem Fragments.Indonesian.Predicates.dengar_is_obviative : dengar.rootClass = RootClass.obviative

theorem Fragments.Indonesian.Predicates.jual_has_ber : jual.formBer.isSome = true

All obviative verbs have ber- forms.

theorem Fragments.Indonesian.Predicates.masak_has_ber : masak.formBer.isSome = true

theorem Fragments.Indonesian.Predicates.cuci_has_ber : cuci.formBer.isSome = true

theorem Fragments.Indonesian.Predicates.tambat_has_ber : tambat.formBer.isSome = true

theorem Fragments.Indonesian.Predicates.dandan_has_ber : dandan.formBer.isSome = true

All reflexive verbs have ber- forms.

theorem Fragments.Indonesian.Predicates.cukur_has_ber : cukur.formBer.isSome = true

theorem Fragments.Indonesian.Predicates.buka_has_ter : buka.formTer.isSome = true

Causer-unspecified verbs have ter- forms, not ber- forms.

theorem Fragments.Indonesian.Predicates.buka_no_ber : buka.formBer.isNone = true

theorem Fragments.Indonesian.Predicates.pecah_has_ter : pecah.formTer.isSome = true

theorem Fragments.Indonesian.Predicates.pecah_no_ber : pecah.formBer.isNone = true

theorem Fragments.Indonesian.Predicates.tulis_has_ter : tulis.formTer.isSome = true

Sneddon ter- verbs also have ter- forms (without ber-).

theorem Fragments.Indonesian.Predicates.tulis_no_ber : tulis.formBer.isNone = true

theorem Fragments.Indonesian.Predicates.bawa_has_ter : bawa.formTer.isSome = true

theorem Fragments.Indonesian.Predicates.bawa_no_ber : bawa.formBer.isNone = true

theorem Fragments.Indonesian.Predicates.dengar_has_ter : dengar.formTer.isSome = true

theorem Fragments.Indonesian.Predicates.dengar_no_ber : dengar.formBer.isNone = true

theorem Fragments.Indonesian.Predicates.jual_incorporates_diri : jual.incorporatesDiri = true

jual licenses diri incorporation → reflexive incorporation middle.

theorem Fragments.Indonesian.Predicates.cuci_incorporates_diri : cuci.incorporatesDiri = true

cuci has the richest incorporation paradigm: body parts + diri.

theorem Fragments.Indonesian.Predicates.cuci_incorporation_count : cuci.incorporatedNPs.length = 9

theorem Fragments.Indonesian.Predicates.jemur_incorporates_diri : jemur.incorporatesDiri = true

jemur 'sunbathe' optionally incorporates diri 'self' (@cite{sneddon-1996} §1.168: berjemur (diri)).

theorem Fragments.Indonesian.Predicates.dandan_no_incorporation : dandan.incorporatedNPs.length = 0

Reflexive-root verbs (dandan, cukur) do not incorporate lexical NPs by default — their ber- forms are already reflexive.

theorem Fragments.Indonesian.Predicates.cukur_no_incorporation : cukur.incorporatedNPs.length = 0

theorem Fragments.Indonesian.Predicates.jual_predicted_reading : jual.rootClass.defaultReading = Semantics.Events.ArgumentRealization.SuppressedVarReading.disjoint

Obviative verbs predict dispositional/passive middles (disjoint).

theorem Fragments.Indonesian.Predicates.masak_predicted_reading : masak.rootClass.defaultReading = Semantics.Events.ArgumentRealization.SuppressedVarReading.disjoint

theorem Fragments.Indonesian.Predicates.dandan_predicted_reading : dandan.rootClass.defaultReading = Semantics.Events.ArgumentRealization.SuppressedVarReading.coreferent

Reflexive verbs predict inherent reflexive middles (coreferent).

theorem Fragments.Indonesian.Predicates.cukur_predicted_reading : cukur.rootClass.defaultReading = Semantics.Events.ArgumentRealization.SuppressedVarReading.coreferent

theorem Fragments.Indonesian.Predicates.pecah_levin_class : pecah.levinClass = some LevinClass.break_

pecah is a break-class verb → participates in middle alternation (change-of-state) and causative/inchoative alternation.

theorem Fragments.Indonesian.Predicates.buka_ter_stative : buka.terClass = some TerClass.stative

theorem Fragments.Indonesian.Predicates.pecah_ter_stative : pecah.terClass = some TerClass.stative

theorem Fragments.Indonesian.Predicates.tulis_ter_stative : tulis.terClass = some TerClass.stative

theorem Fragments.Indonesian.Predicates.bawa_ter_accidental : bawa.terClass = some TerClass.accidental

theorem Fragments.Indonesian.Predicates.dengar_ter_abilitative : dengar.terClass = some TerClass.abilitative

theorem Fragments.Indonesian.Predicates.stative_no_agent : TerClass.stative.hasAgent = false

Stative ter- has no agent — the oleh 'by' phrase is impossible (@cite{sneddon-1996} §1.266).

theorem Fragments.Indonesian.Predicates.accidental_nonvolitional : TerClass.accidental.volitionality = Volitionality.nonvolitional

Accidental ter- entails the agent acted nonvolitionally (@cite{sneddon-1996} §1.267: "unintended, unexpected, sudden").

theorem Fragments.Indonesian.Predicates.accidental_has_agent : TerClass.accidental.hasAgent = true

Accidental ter- has an agent (expressed or implied) — unlike stative, which is agentless. Maaf, koran saudara terbawa oleh saya. 'Sorry, I took your newspaper by mistake.' (§1.269).

theorem Fragments.Indonesian.Predicates.abilitative_retains_suffix : TerClass.abilitative.retainsSuffix = true

Abilitative ter- retains transitive suffixes (-kan, -i) from the base verb, unlike accidental ter-, which drops them (@cite{sneddon-1996} §1.272, §1.274).

theorem Fragments.Indonesian.Predicates.accidental_drops_suffix : TerClass.accidental.retainsSuffix = false

theorem Fragments.Indonesian.Predicates.causer_unspecified_have_stative_ter : ([buka, pecah].all fun (v : IndonesianVerbEntry) => v.rootClass == RootClass.causerUnspecified && v.terClass == some TerClass.stative) = true

The causer-unspecified roots from @cite{beavers-udayana-2022} have stative ter- — their ter- forms describe resulting states, not unintended actions or abilities. This connects B&U's root class analysis to Sneddon's ter- classification.

inductive Fragments.Indonesian.Predicates.DenominalNounClass : Type

Denominal root class: relational nouns (body parts, kin terms, clothing) that form ber- middles with stative possessional readings. The root names a relational noun, not a verbal action.

Examples: ber-topi 'have a hat on', ber-kaki 'have legs', ber-istri 'have a wife'.

These combine incorporation (the noun head-adjoins to ber-) with object promotion (the possessor surfaces as subject). The reading derives from the relational noun's possession relation π' (@cite{barker-1995}; @cite{beavers-udayana-2022} §4).

• bodyPart : DenominalNounClass

  Body part nouns: inalienable possession.

• kinTerm : DenominalNounClass

  Kin terms: social/familial relation.

• clothing : DenominalNounClass

  Clothing nouns: wearing relation.

instance Fragments.Indonesian.Predicates.instDecidableEqDenominalNounClass : DecidableEq DenominalNounClass

Equations

• Fragments.Indonesian.Predicates.instDecidableEqDenominalNounClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Indonesian.Predicates.instBEqDenominalNounClass.beq : DenominalNounClass → DenominalNounClass → Bool

Equations

• Fragments.Indonesian.Predicates.instBEqDenominalNounClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Indonesian.Predicates.instBEqDenominalNounClass : BEq DenominalNounClass

Equations

• Fragments.Indonesian.Predicates.instBEqDenominalNounClass = { beq := Fragments.Indonesian.Predicates.instBEqDenominalNounClass.beq }

def Fragments.Indonesian.Predicates.instReprDenominalNounClass.repr : DenominalNounClass → ℕ → Std.Format

Equations

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

instance Fragments.Indonesian.Predicates.instReprDenominalNounClass : Repr DenominalNounClass

Equations

• Fragments.Indonesian.Predicates.instReprDenominalNounClass = { reprPrec := Fragments.Indonesian.Predicates.instReprDenominalNounClass.repr }

structure Fragments.Indonesian.Predicates.DenominalBerEntry : Type

A denominal ber- entry: a relational noun that forms a stative possessional middle via ber- + incorporation.

• root : String

  The noun root.

• formBer : String

  The ber- form.

• nounClass : DenominalNounClass

  The noun class determining the possession relation.

• gloss : String

  English gloss.

instance Fragments.Indonesian.Predicates.instReprDenominalBerEntry : Repr DenominalBerEntry

Equations

• Fragments.Indonesian.Predicates.instReprDenominalBerEntry = { reprPrec := Fragments.Indonesian.Predicates.instReprDenominalBerEntry.repr }

def Fragments.Indonesian.Predicates.instReprDenominalBerEntry.repr : DenominalBerEntry → ℕ → Std.Format

Equations

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

def Fragments.Indonesian.Predicates.instBEqDenominalBerEntry.beq : DenominalBerEntry → DenominalBerEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Indonesian.Predicates.instBEqDenominalBerEntry.beq x✝¹ x✝ = false

instance Fragments.Indonesian.Predicates.instBEqDenominalBerEntry : BEq DenominalBerEntry

Equations

• Fragments.Indonesian.Predicates.instBEqDenominalBerEntry = { beq := Fragments.Indonesian.Predicates.instBEqDenominalBerEntry.beq }

def Fragments.Indonesian.Predicates.kaki : DenominalBerEntry

Equations

• Fragments.Indonesian.Predicates.kaki = { root := "kaki", formBer := "ber-kaki", nounClass := Fragments.Indonesian.Predicates.DenominalNounClass.bodyPart, gloss := "have legs" }

def Fragments.Indonesian.Predicates.mulut : DenominalBerEntry

Equations

• Fragments.Indonesian.Predicates.mulut = { root := "mulut", formBer := "ber-mulut", nounClass := Fragments.Indonesian.Predicates.DenominalNounClass.bodyPart, gloss := "have a mouth" }

def Fragments.Indonesian.Predicates.tangan : DenominalBerEntry

Equations

• Fragments.Indonesian.Predicates.tangan = { root := "tangan", formBer := "ber-tangan", nounClass := Fragments.Indonesian.Predicates.DenominalNounClass.bodyPart, gloss := "have hands" }

def Fragments.Indonesian.Predicates.istri : DenominalBerEntry

Equations

• Fragments.Indonesian.Predicates.istri = { root := "istri", formBer := "ber-istri", nounClass := Fragments.Indonesian.Predicates.DenominalNounClass.kinTerm, gloss := "have a wife" }

def Fragments.Indonesian.Predicates.suami : DenominalBerEntry

Equations

• Fragments.Indonesian.Predicates.suami = { root := "suami", formBer := "ber-suami", nounClass := Fragments.Indonesian.Predicates.DenominalNounClass.kinTerm, gloss := "have a husband" }

def Fragments.Indonesian.Predicates.adik : DenominalBerEntry

Equations

• Fragments.Indonesian.Predicates.adik = { root := "adik", formBer := "ber-adik", nounClass := Fragments.Indonesian.Predicates.DenominalNounClass.kinTerm, gloss := "have a younger sibling" }

def Fragments.Indonesian.Predicates.topi : DenominalBerEntry

Equations

• Fragments.Indonesian.Predicates.topi = { root := "topi", formBer := "ber-topi", nounClass := Fragments.Indonesian.Predicates.DenominalNounClass.clothing, gloss := "have a hat on" }

def Fragments.Indonesian.Predicates.sepatu : DenominalBerEntry

Equations

• Fragments.Indonesian.Predicates.sepatu = { root := "sepatu", formBer := "ber-sepatu", nounClass := Fragments.Indonesian.Predicates.DenominalNounClass.clothing, gloss := "have shoes on" }

def Fragments.Indonesian.Predicates.baju : DenominalBerEntry

Equations

• Fragments.Indonesian.Predicates.baju = { root := "baju", formBer := "ber-baju", nounClass := Fragments.Indonesian.Predicates.DenominalNounClass.clothing, gloss := "have a dress on" }

def Fragments.Indonesian.Predicates.denominalEntries : List DenominalBerEntry

All denominal ber- entries.

Equations

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

theorem Fragments.Indonesian.Predicates.denominal_classes_covered : ([DenominalNounClass.bodyPart, DenominalNounClass.kinTerm, DenominalNounClass.clothing].all fun (nc : DenominalNounClass) => denominalEntries.any fun (e : DenominalBerEntry) => e.nounClass == nc) = true

All three noun classes are covered in the fragment.

def Fragments.Indonesian.Predicates.allVerbs : List IndonesianVerbEntry

All 13 verbs in the fragment.

Equations

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

theorem Fragments.Indonesian.Predicates.all_have_men : (allVerbs.all fun (v : IndonesianVerbEntry) => v.formMeN.isSome) = true

Every verb has an active meN- form.

theorem Fragments.Indonesian.Predicates.all_have_di : (allVerbs.all fun (v : IndonesianVerbEntry) => v.formDi.isSome) = true

Every verb has a passive di- form.

theorem Fragments.Indonesian.Predicates.all_have_middle_or_anticausative : (allVerbs.all fun (v : IndonesianVerbEntry) => v.formBer.isSome || v.formTer.isSome) = true

Every verb has EITHER ber- OR ter- (middle or anticausative).

theorem Fragments.Indonesian.Predicates.ber_ter_complementary : (allVerbs.all fun (v : IndonesianVerbEntry) => !(v.formBer.isSome && v.formTer.isSome)) = true

No verb has BOTH ber- and ter-. For B&U verbs this follows from root class (ber- for reflexive/obviative, ter- for causer-unspecified). For Sneddon verbs, ter- serves stative/accidental/abilitative functions on roots that lack ber- forms.

def Fragments.Indonesian.Predicates.terVerbs : List IndonesianVerbEntry

The five ter- verbs in the fragment.

Equations

• Fragments.Indonesian.Predicates.terVerbs = List.filter (fun (v : Fragments.Indonesian.Predicates.IndonesianVerbEntry) => v.formTer.isSome) Fragments.Indonesian.Predicates.allVerbs

theorem Fragments.Indonesian.Predicates.all_ter_classified : (terVerbs.all fun (v : IndonesianVerbEntry) => v.terClass.isSome) = true

Every ter- verb has a ter- class assigned — no unclassified ter- forms.

theorem Fragments.Indonesian.Predicates.ter_classes_covered : ([TerClass.stative, TerClass.accidental, TerClass.abilitative].all fun (tc : TerClass) => terVerbs.any fun (v : IndonesianVerbEntry) => v.terClass == some tc) = true

The fragment covers all three ter- classes from @cite{sneddon-1996}.

theorem Fragments.Indonesian.Predicates.all_men_forms_derived : (allVerbs.all fun (v : IndonesianVerbEntry) => v.formMeN == Morphophonology.deriveMeN v.form) = true

Every verb's stored meN- form matches the phonologically derived form from @cite{sneddon-1996} §1.5. This proves the stipulated forms are not arbitrary — they follow the regular nasal assimilation rules. If a root or meN- form is changed incorrectly, this breaks.