Documentation

Linglib.Fragments.Indonesian.Predicates

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 :

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.

Instances For

@[implicit_reducible]

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.instReprRootClass.repr :

RootClass → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Fragments.Indonesian.Predicates.instReprRootClass :

Equations

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

def Fragments.Indonesian.Predicates.RootClass.defaultReading :

RootClass → Typology.Voice.SuppressedVarReading

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

Equations

Instances For

inductive Fragments.Indonesian.Predicates.TerClass :

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.

Instances For

@[implicit_reducible]

instance Fragments.Indonesian.Predicates.instDecidableEqTerClass :

DecidableEq TerClass

Equations

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

@[implicit_reducible]

instance Fragments.Indonesian.Predicates.instReprTerClass :

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.

Instances For

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

Instances For

def Fragments.Indonesian.Predicates.TerClass.volitionality :

TerClass → Semantics.Lexical.Roots.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

Instances For

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

Instances For

structure Fragments.Indonesian.Predicates.IndonesianVerbEntryextends Semantics.Lexical.VerbCore :

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 ArgumentStructure.EntailmentProfile.EntailmentProfile
objectEntailments : Option ArgumentStructure.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 Features.VendlerClass
degreeAchievementScale : Option Features.DegreeAchievement.DegreeAchievementScale
verbIncClass : Option Aspect.Incremental.VerbIncClass
presupType : Option PresupTriggerType
postsupType : Option PostsupType
projectionBehavior : Option ProjectionBehavior
selectsDimension : Option Features.Dimension.Dimension
cosType : Option Features.ChangeOfState.CoSType
implicative : Option Features.Implicative
causative : Option Features.Causative
causalSource : Option Causation.Psych.CausalSource
opaqueContext : Bool
attitude : Option Features.Attitude
takesQuestionBase : Bool
complementSig : Option Core.NaturalLogic.EntailmentSig
senseTag : SenseTag
levinClass : Option LevinClass
rootProfile : Option Roots.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.

Instances For

def Fragments.Indonesian.Predicates.instReprIndonesianVerbEntry.repr :

IndonesianVerbEntry → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Fragments.Indonesian.Predicates.instReprIndonesianVerbEntry :

Repr IndonesianVerbEntry

Equations

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

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

Instances For

@[implicit_reducible]

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

theorem Fragments.Indonesian.Predicates.reflexive_root_coreferent :

RootClass.reflexive.defaultReading = Typology.Voice.SuppressedVarReading.coreferent

Reflexive roots predict coreferent default reading.

theorem Fragments.Indonesian.Predicates.obviative_root_disjoint :

RootClass.obviative.defaultReading = Typology.Voice.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 = Typology.Voice.SuppressedVarReading.disjoint

Obviative verbs predict dispositional/passive middles (disjoint).

theorem Fragments.Indonesian.Predicates.masak_predicted_reading :

masak.rootClass.defaultReading = Typology.Voice.SuppressedVarReading.disjoint

theorem Fragments.Indonesian.Predicates.dandan_predicted_reading :

dandan.rootClass.defaultReading = Typology.Voice.SuppressedVarReading.coreferent

Reflexive verbs predict inherent reflexive middles (coreferent).

theorem Fragments.Indonesian.Predicates.cukur_predicted_reading :

cukur.rootClass.defaultReading = Typology.Voice.SuppressedVarReading.coreferent

theorem Fragments.Indonesian.Predicates.pecah_levin_class :

pecah.levinClass = some Semantics.Lexical.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 = Semantics.Lexical.Roots.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 :

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.

Instances For

@[implicit_reducible]

instance Fragments.Indonesian.Predicates.instDecidableEqDenominalNounClass :

DecidableEq DenominalNounClass

Equations

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

@[implicit_reducible]

instance Fragments.Indonesian.Predicates.instReprDenominalNounClass :

Repr DenominalNounClass

Equations

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

def Fragments.Indonesian.Predicates.instReprDenominalNounClass.repr :

DenominalNounClass → ℕ → Std.Format

Equations

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

Instances For

structure Fragments.Indonesian.Predicates.DenominalBerEntry :

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.

Instances For

@[implicit_reducible]

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.

Instances For

@[implicit_reducible]

instance Fragments.Indonesian.Predicates.instBEqDenominalBerEntry :

BEq DenominalBerEntry

Equations

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

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

Instances For

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" }

Instances For

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" }

Instances For

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" }

Instances For

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" }

Instances For

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" }

Instances For

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" }

Instances For

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" }

Instances For

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" }

Instances For

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" }

Instances For

def Fragments.Indonesian.Predicates.denominalEntries :

List DenominalBerEntry

All denominal ber- entries.

Equations

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

Instances For

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.

Instances For

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

Instances For

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.