Arka 2013: the typology and syntax of TAM in Indonesian

Indonesian has no grammatical TAM: there is no obligatory morphosyntactic opposition, a bare verb is anchored in time by context or by an optional adjunct, and the perfect auxiliary sudah/telah expresses only that the event precedes the reference time, which is free to sit at the moment of speech or in the past — so Klein's puzzle about the English present perfect, which pins the reference time to the present, does not arise. The language nonetheless shows finiteness: the TAM auxiliaries occupy I, a finite clause projects IP whether or not an auxiliary is present, and truncated or controlled complements, resultatives, and sambil adjuncts are bare VPs that admit none of them, while nominal predicates project no I at all. The clitic =nya nominalises verbs of saying and feeling, modals, and evidential roots; a nominalisation carries a default past temporal axis that an adjunct like nanti cancels, a nominalised modal reports a past or present state of affairs counterfactually where the bare modal points to a future one, and the copula adalah and the negator bukan show that these structures are equational.

Main definitions

• Annotation: the paper's E/R/S annotations, with Annotation.frame the Reichenbach frame they describe.
• Aux, Aux.frame: the auxiliaries the paper analyses and the frame relation each expresses; englishPresentPerfect the English contrast.
• projectsI: a clause projects I exactly when its complement coding is not reduced; the selecting verbs and subordinators are fragment entries.

References

• [arka-2013]
• [klein-1992] — the present perfect puzzle
• [kibort-2009] — languages grammaticalise different E, R, S configurations
• [sneddon-1996] — the marker inventory in the fragment

Tense theory and the status of Indonesian TAM (§2)

structure Arka2013.Annotation : Type

An E/R/S annotation as the paper prints it — E-R<S, S<E-R, E<S,R — read as the temporal group each primitive falls in, later groups later in time.

• e : ℕ
• r : ℕ
• s : ℕ

@[instance_reducible]

instance Arka2013.instDecidableEqAnnotation : DecidableEq Annotation

Equations

• Arka2013.instDecidableEqAnnotation = Arka2013.instDecidableEqAnnotation.decEq

def Arka2013.instDecidableEqAnnotation.decEq (x✝ x✝¹ : Annotation) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Arka2013.instReprAnnotation : Repr Annotation

Equations

• Arka2013.instReprAnnotation = { reprPrec := Arka2013.instReprAnnotation.repr }

def Arka2013.instReprAnnotation.repr : Annotation → ℕ → Std.Format

Equations

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

def Arka2013.Annotation.parse? (str : String) : Option Annotation

Read an annotation: < opens a later group, - and , keep the current one.

Equations

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

def Arka2013.Annotation.frame (a : Annotation) : Tense.ReichenbachFrame ℤ

The frame an annotation describes, with the perspective at speech time.

Equations

• a.frame = { speechTime := ↑a.s, perspectiveTime := ↑a.s, referenceTime := ↑a.r, eventTime := ↑a.e }

inductive Arka2013.Aux : Type

The auxiliaries the paper assigns a frame relation: akan future, sedang progressive, sudah/telah perfect.

• akan : Aux
• sedang : Aux
• sudah : Aux

@[instance_reducible]

instance Arka2013.instDecidableEqAux : DecidableEq Aux

Equations

• Arka2013.instDecidableEqAux x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Arka2013.instReprAux.repr : Aux → ℕ → Std.Format

Equations

• Arka2013.instReprAux.repr Arka2013.Aux.akan prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arka2013.Aux.akan")).group prec✝
• Arka2013.instReprAux.repr Arka2013.Aux.sedang prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arka2013.Aux.sedang")).group prec✝
• Arka2013.instReprAux.repr Arka2013.Aux.sudah prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arka2013.Aux.sudah")).group prec✝

@[instance_reducible]

instance Arka2013.instReprAux : Repr Aux

Equations

• Arka2013.instReprAux = { reprPrec := Arka2013.instReprAux.repr }

@[instance_reducible]

instance Arka2013.instFintypeAux : Fintype Aux

Equations

• Arka2013.instFintypeAux = { elems := { val := ↑Arka2013.Aux.enumList, nodup := Arka2013.Aux.enumList_nodup }, complete := Arka2013.instFintypeAux._proof_1 }

def Arka2013.Aux.ofMarker (m : Indonesian.TemporalMarker) : Option Aux

The auxiliary a fragment marker realises, by its meaning.

Equations

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

def Arka2013.Aux.ofForm (s : String) : Option Aux

The auxiliary written as a form, through the fragment's inventory.

Equations

• Arka2013.Aux.ofForm s = (List.find? (fun (x : Indonesian.TemporalMarker) => decide (x.form = s)) Indonesian.temporalMarkers).bind Arka2013.Aux.ofMarker

def Arka2013.Aux.frame {T : Type u_1} [LinearOrder T] : Aux → Tense.ReichenbachFrame T → Prop

The frame relation each auxiliary expresses: akan S < E-R, sedang E = R, sudah E < R with R free.

Equations

• Arka2013.Aux.akan.frame x✝ = (x✝.isFuture ∧ x✝.isPerfective)
• Arka2013.Aux.sedang.frame x✝ = x✝.isPerfective
• Arka2013.Aux.sudah.frame x✝ = x✝.isPerfect

@[instance_reducible]

instance Arka2013.instDecidableFrame {T : Type u_1} [LinearOrder T] (a : Aux) (f : Tense.ReichenbachFrame T) : Decidable (a.frame f)

Equations

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

theorem Arka2013.telah_sudah : Aux.ofMarker Indonesian.telah = Aux.ofMarker Indonesian.sudah

telah and sudah realise the same auxiliary.

theorem Arka2013.rows_annotations (r : Data.Examples.LinguisticExample) : r ∈ Examples.all → ∀ a ∈ (r.feature? "aux" >>= Aux.ofForm).toList, ∀ ann ∈ (r.feature? "frame" >>= Annotation.parse?).toList, a.frame ann.frame

Every annotated sentence with an auxiliary satisfies the auxiliary's frame relation.

def Arka2013.sudahAnnotations : List Annotation

The annotations of the sudah sentences (5).

Equations

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

theorem Arka2013.sudah_reference_free : (∃ a ∈ sudahAnnotations, a.r = a.s) ∧ (∃ a ∈ sudahAnnotations, a.r < a.s) ∧ ∀ a ∈ sudahAnnotations, a.e < a.r

R is free under sudah: it sits at speech time in one annotation and before it in another, the event preceding it in both.

def Arka2013.englishPresentPerfect {T : Type u_1} [LinearOrder T] (f : Tense.ReichenbachFrame T) : Prop

The English present perfect grammaticalises E < R together with R at the deictic centre.

Equations

• Arka2013.englishPresentPerfect f = (f.isPerfect ∧ f.isPresent)

@[instance_reducible]

instance Arka2013.instDecidableEnglishPresentPerfect {T : Type u_1} [LinearOrder T] (f : Tense.ReichenbachFrame T) : Decidable (englishPresentPerfect f)

Equations

• Arka2013.instDecidableEnglishPresentPerfect f = id inferInstance

theorem Arka2013.klein_puzzle_dissolved : (∀ (f : Tense.ReichenbachFrame ℤ), englishPresentPerfect f → f.isPast → False) ∧ ∃ (f : Tense.ReichenbachFrame ℤ), Aux.sudah.frame f ∧ f.isPast

Klein's puzzle and its Indonesian dissolution: with a past reference time the English present perfect is contradictory, while sudah under the same reference time is satisfiable — (5b) Dia sudah pergi kemarin.

theorem Arka2013.english_pp_strictly_stronger {T : Type u_1} [LinearOrder T] : (∀ (f : Tense.ReichenbachFrame T), englishPresentPerfect f → Aux.sudah.frame f) ∧ ∃ (f : Tense.ReichenbachFrame ℤ), Aux.sudah.frame f ∧ ¬englishPresentPerfect f

The English present perfect strictly strengthens sudah.

Finiteness (§3)

def Arka2013.matrixVerb : String → Option Verb

The verb selecting a row's complement clause, from the fragment.

Equations

• Arka2013.matrixVerb "ingin" = some Indonesian.Complementation.ingin
• Arka2013.matrixVerb "belajar" = some Indonesian.Complementation.belajar
• Arka2013.matrixVerb "menyuruh" = some Indonesian.Complementation.menyuruh
• Arka2013.matrixVerb "mendorong" = some Indonesian.Complementation.mendorong
• Arka2013.matrixVerb "tahu" = some Indonesian.Complementation.tahu
• Arka2013.matrixVerb x✝ = none

def Arka2013.subordinator : String → Option Complementizer

The subordinator typing a row's dependent clause, from the fragment.

Equations

• Arka2013.subordinator "bahwa" = some Indonesian.Complementation.bahwa
• Arka2013.subordinator "agar" = some Indonesian.Complementation.agar
• Arka2013.subordinator x✝ = none

def Arka2013.projectsI (c : Complement.Coding) : Bool

A clause projects I — the position of the TAM auxiliaries (16) — exactly when its coding is not reduced: a full clause anchors its own temporal axis, a reduced complement is a bare VP (17).

Equations

• Arka2013.projectsI c = !c.isReduced

def Arka2013.complementCoding (v : Verb) : Option Complement.Coding

The coding of the clause a verb's citation frame selects.

Equations

• Arka2013.complementCoding v = v.frames.head?.bind fun (fr : Frame) => fr.codings.head?

theorem Arka2013.rows_finiteness (r : Data.Examples.LinguisticExample) : r ∈ Examples.all → (∀ v ∈ (r.feature? "matrix" >>= matrixVerb).toList, ∀ c ∈ (complementCoding v).toList, projectsI c = true ↔ r.feature? "withAux" = some "acceptable") ∧ (∀ s ∈ (r.feature? "subordinator" >>= subordinator).toList, ∀ c ∈ s.coding.toList, projectsI c = true ↔ r.feature? "withAux" = some "acceptable") ∧ (r.feature? "clause" = some "root" → r.feature? "withAux" = some "acceptable") ∧ (r.feature? "predicate" = some "nominal" → ∀ j ∈ (r.feature? "withAux").toList, j ≠ "acceptable")

A TAM auxiliary is acceptable in a dependent clause exactly when the clause its selector takes projects I; root clauses do, and a nominal predicate projects no verbal structure.

Morphosemantic TAM: =nya nominalisation (§4)

theorem Arka2013.rows_nya_default_past (r : Data.Examples.LinguisticExample) : r ∈ Examples.all → r.feature? "nominalised" = some "true" → ∀ axis ∈ (r.feature? "axis").toList, axis = "future" ↔ r.feature? "adjunct" = some "nanti"

The default past axis of a nominalisation is cancelled exactly by a future adjunct (34)–(36).

theorem Arka2013.rows_modal_nominalisation (r : Data.Examples.LinguisticExample) : r ∈ Examples.all → ∀ soa ∈ (r.feature? "soa").toList, soa = "future" ↔ r.feature? "nominalised" = some "false"

A bare modal evaluates a future state of affairs; its nominalisation a past or present one (37)–(39).

theorem Arka2013.rows_equational (r : Data.Examples.LinguisticExample) : r ∈ Examples.all → ∀ key ∈ ["adalah", "bukan"], ∀ j ∈ (r.feature? key).toList, j = "acceptable" ↔ r.feature? "predicate" = some "nominal"

The copula adalah and the negator bukan take nominal predicates only, the nominalisations among them (44)–(48).