Indonesian verbs

This file defines the Indonesian verbs of Beavers and Udayana's study of the middle voice and three verbs that show the readings of the prefix ter- in Sneddon's grammar.

An entry records the segments of the root, whether the root has a middle in ber-, and the reading of its ter- form if it has one. The prefixed forms are derived, the active by the nasal alternation of Indonesian.Phonology.meN.

Main definitions

• TerClass: the stative, accidental and abilitative readings of ter-.
• Indonesian.Verb: a verb entry, with the forms Verb.meN, Verb.di, Verb.ber? and Verb.ter?.
• verbs: the entries of this file.

References

• [Sne96]
• [BU22]

Readings of ter-

inductive Indonesian.TerClass : Type

The three readings of a verb in ter- in Sneddon's grammar. Some verbs have more than one, as terbuka 'open', which can also be accidental or abilitative.

• stative : TerClass

  The state that follows an action, as in tertulis 'written'.

• accidental : TerClass

  An action that was not intended, as in terbawa 'taken by mistake'.

• abilitative : TerClass

  The ability to carry out the action, as in tidak terbeli 'cannot be afforded'.

@[instance_reducible]

instance Indonesian.instDecidableEqTerClass : DecidableEq TerClass

Equations

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

@[instance_reducible]

instance Indonesian.instReprTerClass : Repr TerClass

Equations

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

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

Equations

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

def Indonesian.TerClass.HasAgent (c : TerClass) : Prop

A stative ter- verb involves no action and so has no actor, and an accidental or abilitative one can take an agent phrase with oleh.

Equations

• c.HasAgent = (c ≠ Indonesian.TerClass.stative)

@[instance_reducible]

instance Indonesian.TerClass.instDecidablePredHasAgent : DecidablePred HasAgent

Equations

• x✝.instDecidablePredHasAgent = { decide := !decide (x✝ = Indonesian.TerClass.stative), reflects_decide := ⋯ }

def Indonesian.TerClass.IsNonvolitional (c : TerClass) : Prop

An accidental ter- verb marks the action as not intended; the other two readings leave volition open.

Equations

• c.IsNonvolitional = (c = Indonesian.TerClass.accidental)

@[instance_reducible]

instance Indonesian.TerClass.instDecidablePredIsNonvolitional : DecidablePred IsNonvolitional

Equations

• x✝.instDecidablePredIsNonvolitional = Indonesian.TerClass.instDecidablePredIsNonvolitional._aux_1 x✝

def Indonesian.TerClass.RetainsSuffix (c : TerClass) : Prop

An abilitative ter- verb keeps the suffix -kan or -i of its base, as in terpecahkan 'can be solved', which the other two readings drop.

Equations

• c.RetainsSuffix = (c = Indonesian.TerClass.abilitative)

@[instance_reducible]

instance Indonesian.TerClass.instDecidablePredRetainsSuffix : DecidablePred RetainsSuffix

Equations

• x✝.instDecidablePredRetainsSuffix = Indonesian.TerClass.instDecidablePredRetainsSuffix._aux_1 x✝

Entries

structure Indonesian.Verbextends Verb : Type

An Indonesian verb is the root entry, whose form is the spelled root, together with the segments of the root and its prefixation.

• valency : Valency
• voiceType : Option VoiceType
• passivizable : Bool
• perfectAuxiliaries : Finset PerfectAuxiliary
• vendlerClass : Option Aspect.VendlerClass
• scaleDimension : Option Degree.ScalarDimension
• scalePolarity : Polarity
• direction : Option Spatial.Path.Direction
• incrementality : Option Aspect.Incrementality
• phasal : Option Aspect.Phasal
• factivity : Option Presupposition.Factivity
• implicative : NaturalLogic.ImplicationSignature
• opaqueContext : Bool
• attitude : Option _root_.Attitude
• readings : List Reading
• complementSig : Option NaturalLogic.Signature
• levinClasses : Finset ArgumentStructure.LevinClass
• levinExcluded : Finset ArgumentStructure.LevinClass
• root : Semantics.Root
• morphs : List Morphology.Morph
• speechActVerb : Bool
• senseTag : SenseTag
• rootSegments : List Phonology.Segment

  The segments of the root.

• ber : Bool

  Whether the root has a middle in ber-.

• terClass : Option TerClass

  The reading of the ter- form, for a root that has one.

• incorporatedNPs : List String

  The nouns that the ber- form incorporates.

def Indonesian.instBEqVerb.beq : Verb → Verb → Bool

Equations

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

@[instance_reducible]

instance Indonesian.instBEqVerb : BEq Verb

Equations

• Indonesian.instBEqVerb = { beq := Indonesian.instBEqVerb.beq }

def Indonesian.Verb.meN (v : Verb) : List Phonology.Segment

The active form in meN-.

Equations

• v.meN = Indonesian.Phonology.meN v.rootSegments

def Indonesian.Verb.di (v : Verb) : List Phonology.Segment

The passive form in di-.

Equations

• v.di = [Indonesian.Phonology.d, Indonesian.Phonology.i] ++ v.rootSegments

def Indonesian.Verb.ber? (v : Verb) : Option (List Phonology.Segment)

The middle in ber-, for a root that has one.

Equations

• v.ber? = if v.ber = true then some ([Indonesian.Phonology.b, Indonesian.Phonology.e, Indonesian.Phonology.r] ++ v.rootSegments) else none

def Indonesian.Verb.ter? (v : Verb) : Option (List Phonology.Segment)

The form in ter-, for a root that has one.

Equations

• v.ter? = Option.map (fun (x : Indonesian.TerClass) => [Indonesian.Phonology.t, Indonesian.Phonology.e, Indonesian.Phonology.r] ++ v.rootSegments) v.terClass

def Indonesian.Verb.IncorporatesDiri (v : Verb) : Prop

The ber- form of the verb can incorporate diri 'self', which gives it a reflexive reading.

Equations

• v.IncorporatesDiri = ("diri" ∈ v.incorporatedNPs)

@[instance_reducible]

instance Indonesian.Verb.instDecidablePredIncorporatesDiri : DecidablePred IncorporatesDiri

Equations

• x✝.instDecidablePredIncorporatesDiri = { decide := decide (List.elem "diri" x✝.incorporatedNPs = true), reflects_decide := ⋯ }

Roots with a middle in ber-

def Indonesian.jual : Verb

jual 'sell', as in Mobil itu berjual dengan mudah 'The car sells easily'. Its middle incorporates a noun, as in berjual baju and berjual diri.

Equations

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

def Indonesian.masak : Verb

masak 'cook'.

Equations

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

def Indonesian.cuci : Verb

cuci 'wash', whose middle incorporates body-part nouns and others, as in bercuci mata 'wash one's eyes'.

Equations

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

def Indonesian.tambat : Verb

tambat 'tie, moor', as in Kapal itu bertambat dengan mudah 'The boat moors easily'.

Equations

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

def Indonesian.dandan : Verb

dandan 'dress', as in Ali berdandan 'Ali dressed'.

Equations

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

def Indonesian.cukur : Verb

cukur 'shave'.

Equations

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

def Indonesian.jemur : Verb

jemur 'dry in the sun', whose middle berjemur (diri) is 'sunbathe'.

Equations

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

def Indonesian.sisir : Verb

sisir 'comb'.

Equations

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

Roots with a form in ter-

def Indonesian.buka : Verb

buka 'open', as in Pintu itu terbuka 'The door opened'.

Equations

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

def Indonesian.pecah : Verb

pecah 'break', as in Jendela itu terpecah 'The window broke'.

Equations

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

def Indonesian.tulis : Verb

tulis 'write', whose stative is Surat itu tertulis dalam bahasa Inggris 'That letter is written in English', beside the passive ditulis 'was written'.

Equations

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

def Indonesian.bawa : Verb

bawa 'carry, take', whose accidental is Koran saudara terbawa oleh saya 'I took your newspaper by mistake'.

Equations

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

def Indonesian.dengar : Verb

dengar 'hear', whose abilitative is tidak terdengar dari sini 'cannot be heard from here'.

Equations

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

def Indonesian.verbs : List Verb

The entries of this file.

Equations

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

Derived forms

theorem Indonesian.pecah_forms : pecah.meN = [Phonology.m, Phonology.e, Phonology.m, Phonology.e, Phonology.c, Phonology.a, Phonology.h] ∧ pecah.ter? = some [Phonology.t, Phonology.e, Phonology.r, Phonology.p, Phonology.e, Phonology.c, Phonology.a, Phonology.h]

memecah and terpecah. The root-initial p is substituted in the active alone.

theorem Indonesian.tambat_forms : tambat.meN = [Phonology.m, Phonology.e, Phonology.n, Phonology.a, Phonology.m, Phonology.b, Phonology.a, Phonology.t] ∧ tambat.ber? = some [Phonology.b, Phonology.e, Phonology.r, Phonology.t, Phonology.a, Phonology.m, Phonology.b, Phonology.a, Phonology.t]

menambat and bertambat. Substitution takes the root-initial t and leaves the cluster inside the root.

theorem Indonesian.sisir_meN : sisir.meN = [Phonology.m, Phonology.e, Phonology.ny, Phonology.i, Phonology.s, Phonology.i, Phonology.r]

menyisir, with the palatal nasal for the root-initial s and the second s kept.

theorem Indonesian.masak_meN : masak.meN = [Phonology.m, Phonology.e, Phonology.m, Phonology.a, Phonology.s, Phonology.a, Phonology.k]

memasak, with the prefix nasal lost before a nasal.

theorem Indonesian.dengar_forms : dengar.meN = [Phonology.m, Phonology.e, Phonology.n, Phonology.d, Phonology.e, Phonology.ng, Phonology.a, Phonology.r] ∧ dengar.di = [Phonology.d, Phonology.i, Phonology.d, Phonology.e, Phonology.ng, Phonology.a, Phonology.r]

mendengar and didengar, with assimilation alone before a voiced stop.

theorem Indonesian.meN_suffix (v : Verb) : v ∈ verbs → ∀ x ∈ v.rootSegments.head?, if x ∈ Phonology.substituting then v.rootSegments.tail <:+ v.meN ∧ ¬v.rootSegments <:+ v.meN else v.rootSegments <:+ v.meN

The active keeps the whole root after a root-initial segment that is not substituted, and loses exactly that segment otherwise.