Toba Batak Fragment @cite{erlewine-2018}

Morphosyntactic data for Toba Batak (Austronesian, Sumatra) relevant to the extraction restriction and pivot system.

Toba Batak has predicate-initial word order (derived by predicate fronting) and an extraction restriction: only the "pivot" — the voice-determined, clause-peripheral argument — can undergo Ā-movement.

Voice System

Unlike Philippine-type Austronesian languages (Tagalog, Seediq), Toba Batak does not have a full voice/Case system with multiple voices. Two voice morphemes determine which argument is the pivot (= subject):

• Actor Voice (AV): agent is the pivot
• Object Voice (OV): patient/theme is the pivot

The restriction on extraction follows from nominal licensing: only the pivot (Case-licensed by T's [PROBE:D] in Spec,TP) can undergo Ā-movement; a non-pivot DP fronted to Spec,CP would lack a Case licensor. This is NOT a voice-as-Case system in the Philippine sense; it is a structural consequence of how probing and Case assignment interact with predicate fronting.

inductive Fragments.TobaBatak.Voice : Type

Toba Batak voice: determines which argument is the pivot.

• av : Voice

  Actor voice: the agent is the pivot (clause-final)

• ov : Voice

  Object voice: the patient/theme is the pivot

def Fragments.TobaBatak.instReprVoice.repr : Voice → Nat → Std.Format

Equations

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

instance Fragments.TobaBatak.instReprVoice : Repr Voice

Equations

• Fragments.TobaBatak.instReprVoice = { reprPrec := Fragments.TobaBatak.instReprVoice.repr }

instance Fragments.TobaBatak.instDecidableEqVoice : DecidableEq Voice

Equations

• Fragments.TobaBatak.instDecidableEqVoice x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.TobaBatak.instBEqVoice : BEq Voice

Equations

• Fragments.TobaBatak.instBEqVoice = { beq := Fragments.TobaBatak.instBEqVoice.beq }

def Fragments.TobaBatak.instBEqVoice.beq : Voice → Voice → Bool

Equations

• Fragments.TobaBatak.instBEqVoice.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.TobaBatak.Voice.pivotRole : Voice → Interfaces.ArgumentRole

Which argument role is the pivot for a given voice?

Equations

• Fragments.TobaBatak.Voice.av.pivotRole = Interfaces.ArgumentRole.agent
• Fragments.TobaBatak.Voice.ov.pivotRole = Interfaces.ArgumentRole.patient

inductive Fragments.TobaBatak.ExtractionJudgment : Type

Whether extraction of a given argument is grammatical.

• grammatical : ExtractionJudgment
• ungrammatical : ExtractionJudgment

instance Fragments.TobaBatak.instReprExtractionJudgment : Repr ExtractionJudgment

Equations

• Fragments.TobaBatak.instReprExtractionJudgment = { reprPrec := Fragments.TobaBatak.instReprExtractionJudgment.repr }

def Fragments.TobaBatak.instReprExtractionJudgment.repr : ExtractionJudgment → Nat → Std.Format

Equations

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

instance Fragments.TobaBatak.instDecidableEqExtractionJudgment : DecidableEq ExtractionJudgment

Equations

• Fragments.TobaBatak.instDecidableEqExtractionJudgment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.TobaBatak.instBEqExtractionJudgment.beq : ExtractionJudgment → ExtractionJudgment → Bool

Equations

• Fragments.TobaBatak.instBEqExtractionJudgment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.TobaBatak.instBEqExtractionJudgment : BEq ExtractionJudgment

Equations

• Fragments.TobaBatak.instBEqExtractionJudgment = { beq := Fragments.TobaBatak.instBEqExtractionJudgment.beq }

structure Fragments.TobaBatak.ExtractionDatum : Type

A Toba Batak extraction datum: voice choice + extracted element + judgment.

• voice : Voice

  Which voice the clause is in

• extracted : Interfaces.Extractee

  What is being extracted (DP argument or adjunct)

• judgment : ExtractionJudgment

  Whether the extraction is grammatical

• description : String

  Description

def Fragments.TobaBatak.instReprExtractionDatum.repr : ExtractionDatum → Nat → Std.Format

Equations

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

instance Fragments.TobaBatak.instReprExtractionDatum : Repr ExtractionDatum

Equations

• Fragments.TobaBatak.instReprExtractionDatum = { reprPrec := Fragments.TobaBatak.instReprExtractionDatum.repr }

def Fragments.TobaBatak.ExtractionDatum.extractsPivot (d : ExtractionDatum) : Bool

Is the extracted element the pivot for the given voice? Adjuncts are never pivots (they don't participate in Case licensing).

Equations

• d.extractsPivot = match d.extracted with | Interfaces.Extractee.dpArg role => role == d.voice.pivotRole | Interfaces.Extractee.adjunct => false

def Fragments.TobaBatak.avAgentExtraction : ExtractionDatum

AV + agent extraction: grammatical (agent is pivot in AV).

Equations

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

def Fragments.TobaBatak.avPatientExtraction : ExtractionDatum

AV + patient extraction: ungrammatical (patient is not pivot in AV).

Equations

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

def Fragments.TobaBatak.avObliqueExtraction : ExtractionDatum

AV + oblique extraction: ungrammatical (oblique is never pivot).

Equations

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

def Fragments.TobaBatak.ovPatientExtraction : ExtractionDatum

OV + patient extraction: grammatical (patient is pivot in OV).

Equations

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

def Fragments.TobaBatak.ovAgentExtraction : ExtractionDatum

OV + agent extraction: ungrammatical (agent is not pivot in OV).

Equations

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

def Fragments.TobaBatak.ovObliqueExtraction : ExtractionDatum

OV + oblique extraction: ungrammatical (oblique is never pivot).

Equations

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

def Fragments.TobaBatak.avAdjunctExtraction : ExtractionDatum

AV + adjunct extraction: grammatical (adjuncts don't need Case).

Equations

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

def Fragments.TobaBatak.ovAdjunctExtraction : ExtractionDatum

OV + adjunct extraction: grammatical (adjuncts don't need Case).

Equations

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

def Fragments.TobaBatak.extractionData : List ExtractionDatum

All monoclausal extraction data.

Equations

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

def Fragments.TobaBatak.tbExtractionProfile : Interfaces.ExtractionProfile

Toba Batak extraction profile: structural restriction (pivot-only).

Equations

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

def Fragments.TobaBatak.tbVoiceSystem : Interfaces.VoiceSystemProfile

Toba Batak voice system: two-way symmetrical (AV/OV).

Unlike Philippine-type languages (Tagalog: 4+ voices including locative, instrumental), Toba Batak has only actor and object voice. The system is symmetrical — neither voice is morphologically basic.

Equations

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

theorem Fragments.TobaBatak.tb_voice_system_symmetrical : tbVoiceSystem.symmetry = Interfaces.VoiceSystemSymmetry.symmetrical

theorem Fragments.TobaBatak.tb_voice_count : tbVoiceSystem.voiceCount = 2

theorem Fragments.TobaBatak.tb_is_active_passive : tbVoiceSystem.isActivePassive = true

theorem Fragments.TobaBatak.tb_promotes_agent : tbVoiceSystem.promotesRole Interfaces.PivotTarget.agent = true