Nungon Medial Verb Morphology @cite{sarvasy-2017}

@cite{sarvasy-2015} @cite{sarvasy-aikhenvald-2025}

Medial verb morphology in Nungon (Trans-New Guinea, Finisterre-Huon family; Morobe Province, Papua New Guinea). Nungon has the most extensively described clause chaining system in the recent literature.

Key properties

Nungon medial verbs are maximally reduced: they carry no tense, no aspect, and no independent mood marking. The single final verb in each chain supplies tense and mood for the entire chain. The only morphology on a medial verb is:

1. The verb stem
2. A switch-reference suffix encoding subject continuity (SS vs. DS) and temporal relation (sequential vs. simultaneous)

Switch-reference

The SR system is four-way, crossing two binary dimensions:

• Subject continuity: same subject (SS) vs. different subject (DS)
• Temporal relation: sequential (SEQ) vs. simultaneous (SIM)

SS forms are invariant (no person/number indexing). DS forms obligatorily index the person and number of the medial clause's subject argument — the participant whose identity differs from the following clause's subject.

DS person/number paradigm (@cite{sarvasy-aikhenvald-2025}: Table 2)

Person	Singular	Dual	Plural
1	-wa-ya	-ra-ya	-na-ya
2	-i-ya	-uny-a	-u-ya
3	-un-a	-uny-a	-u-ya

Note: 2du and 3du are syncretic (-uny-a); 2pl and 3pl are syncretic (-u-ya).

inductive Fragments.Nungon.MedialVerbs.SRCategory : Type

Switch-reference category combining subject continuity and temporal relation. Nungon has a four-way system: SS-SEQ, SS-SIM, DS-SEQ, DS-SIM.

• ssSEQ : SRCategory
• ssSIM : SRCategory
• dsSEQ : SRCategory
• dsSIM : SRCategory

instance Fragments.Nungon.MedialVerbs.instDecidableEqSRCategory : DecidableEq SRCategory

Equations

• Fragments.Nungon.MedialVerbs.instDecidableEqSRCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Nungon.MedialVerbs.instReprSRCategory.repr : SRCategory → Nat → Std.Format

Equations

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

instance Fragments.Nungon.MedialVerbs.instReprSRCategory : Repr SRCategory

Equations

• Fragments.Nungon.MedialVerbs.instReprSRCategory = { reprPrec := Fragments.Nungon.MedialVerbs.instReprSRCategory.repr }

def Fragments.Nungon.MedialVerbs.instBEqSRCategory.beq : SRCategory → SRCategory → Bool

Equations

• Fragments.Nungon.MedialVerbs.instBEqSRCategory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Nungon.MedialVerbs.instBEqSRCategory : BEq SRCategory

Equations

• Fragments.Nungon.MedialVerbs.instBEqSRCategory = { beq := Fragments.Nungon.MedialVerbs.instBEqSRCategory.beq }

instance Fragments.Nungon.MedialVerbs.instInhabitedSRCategory : Inhabited SRCategory

Equations

• Fragments.Nungon.MedialVerbs.instInhabitedSRCategory = { default := Fragments.Nungon.MedialVerbs.instInhabitedSRCategory.default }

def Fragments.Nungon.MedialVerbs.instInhabitedSRCategory.default : SRCategory

Equations

• Fragments.Nungon.MedialVerbs.instInhabitedSRCategory.default = Fragments.Nungon.MedialVerbs.SRCategory.ssSEQ

def Fragments.Nungon.MedialVerbs.SRCategory.isSS : SRCategory → Bool

Whether this SR category indicates same subject.

Equations

• Fragments.Nungon.MedialVerbs.SRCategory.ssSEQ.isSS = true
• Fragments.Nungon.MedialVerbs.SRCategory.ssSIM.isSS = true
• Fragments.Nungon.MedialVerbs.SRCategory.dsSEQ.isSS = false
• Fragments.Nungon.MedialVerbs.SRCategory.dsSIM.isSS = false

def Fragments.Nungon.MedialVerbs.SRCategory.isSequential : SRCategory → Bool

Whether this SR category indicates sequential temporal relation.

Equations

• Fragments.Nungon.MedialVerbs.SRCategory.ssSEQ.isSequential = true
• Fragments.Nungon.MedialVerbs.SRCategory.dsSEQ.isSequential = true
• Fragments.Nungon.MedialVerbs.SRCategory.ssSIM.isSequential = false
• Fragments.Nungon.MedialVerbs.SRCategory.dsSIM.isSequential = false

structure Fragments.Nungon.MedialVerbs.PersonNumber : Type

Person/number combination for DS medial verb agreement.

• person : UD.Person
• number : UD.Number

instance Fragments.Nungon.MedialVerbs.instDecidableEqPersonNumber : DecidableEq PersonNumber

Equations

• Fragments.Nungon.MedialVerbs.instDecidableEqPersonNumber = Fragments.Nungon.MedialVerbs.instDecidableEqPersonNumber.decEq

def Fragments.Nungon.MedialVerbs.instDecidableEqPersonNumber.decEq (x✝ x✝¹ : PersonNumber) : Decidable (x✝ = x✝¹)

Equations

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

instance Fragments.Nungon.MedialVerbs.instReprPersonNumber : Repr PersonNumber

Equations

• Fragments.Nungon.MedialVerbs.instReprPersonNumber = { reprPrec := Fragments.Nungon.MedialVerbs.instReprPersonNumber.repr }

def Fragments.Nungon.MedialVerbs.instReprPersonNumber.repr : PersonNumber → Nat → Std.Format

Equations

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

instance Fragments.Nungon.MedialVerbs.instBEqPersonNumber : BEq PersonNumber

Equations

• Fragments.Nungon.MedialVerbs.instBEqPersonNumber = { beq := Fragments.Nungon.MedialVerbs.instBEqPersonNumber.beq }

def Fragments.Nungon.MedialVerbs.instBEqPersonNumber.beq : PersonNumber → PersonNumber → Bool

Equations

• Fragments.Nungon.MedialVerbs.instBEqPersonNumber.beq { person := a, number := a_1 } { person := b, number := b_1 } = (a == b && a_1 == b_1)
• Fragments.Nungon.MedialVerbs.instBEqPersonNumber.beq x✝¹ x✝ = false

structure Fragments.Nungon.MedialVerbs.DSSuffix : Type

A DS suffix entry: form + person/number it indexes.

• form : String
• personNumber : PersonNumber

def Fragments.Nungon.MedialVerbs.instReprDSSuffix.repr : DSSuffix → Nat → Std.Format

Equations

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

instance Fragments.Nungon.MedialVerbs.instReprDSSuffix : Repr DSSuffix

Equations

• Fragments.Nungon.MedialVerbs.instReprDSSuffix = { reprPrec := Fragments.Nungon.MedialVerbs.instReprDSSuffix.repr }

instance Fragments.Nungon.MedialVerbs.instBEqDSSuffix : BEq DSSuffix

Equations

• Fragments.Nungon.MedialVerbs.instBEqDSSuffix = { beq := Fragments.Nungon.MedialVerbs.instBEqDSSuffix.beq }

def Fragments.Nungon.MedialVerbs.instBEqDSSuffix.beq : DSSuffix → DSSuffix → Bool

Equations

• Fragments.Nungon.MedialVerbs.instBEqDSSuffix.beq { form := a, personNumber := a_1 } { form := b, personNumber := b_1 } = (a == b && a_1 == b_1)
• Fragments.Nungon.MedialVerbs.instBEqDSSuffix.beq x✝¹ x✝ = false

def Fragments.Nungon.MedialVerbs.ds1sg : DSSuffix

1sg DS suffix.

Equations

• Fragments.Nungon.MedialVerbs.ds1sg = { form := "-wa-ya", personNumber := { person := UD.Person.first, number := UD.Number.Sing } }

def Fragments.Nungon.MedialVerbs.ds2sg : DSSuffix

2sg DS suffix.

Equations

• Fragments.Nungon.MedialVerbs.ds2sg = { form := "-i-ya", personNumber := { person := UD.Person.second, number := UD.Number.Sing } }

def Fragments.Nungon.MedialVerbs.ds3sg : DSSuffix

3sg DS suffix.

Equations

• Fragments.Nungon.MedialVerbs.ds3sg = { form := "-un-a", personNumber := { person := UD.Person.third, number := UD.Number.Sing } }

def Fragments.Nungon.MedialVerbs.ds1du : DSSuffix

1du DS suffix.

Equations

• Fragments.Nungon.MedialVerbs.ds1du = { form := "-ra-ya", personNumber := { person := UD.Person.first, number := UD.Number.Dual } }

def Fragments.Nungon.MedialVerbs.ds2du : DSSuffix

2du DS suffix (syncretic with 3du).

Equations

• Fragments.Nungon.MedialVerbs.ds2du = { form := "-uny-a", personNumber := { person := UD.Person.second, number := UD.Number.Dual } }

def Fragments.Nungon.MedialVerbs.ds3du : DSSuffix

3du DS suffix (syncretic with 2du).

Equations

• Fragments.Nungon.MedialVerbs.ds3du = { form := "-uny-a", personNumber := { person := UD.Person.third, number := UD.Number.Dual } }

def Fragments.Nungon.MedialVerbs.ds1pl : DSSuffix

1pl DS suffix.

Equations

• Fragments.Nungon.MedialVerbs.ds1pl = { form := "-na-ya", personNumber := { person := UD.Person.first, number := UD.Number.Plur } }

def Fragments.Nungon.MedialVerbs.ds2pl : DSSuffix

2pl DS suffix (syncretic with 3pl).

Equations

• Fragments.Nungon.MedialVerbs.ds2pl = { form := "-u-ya", personNumber := { person := UD.Person.second, number := UD.Number.Plur } }

def Fragments.Nungon.MedialVerbs.ds3pl : DSSuffix

3pl DS suffix (syncretic with 2pl).

Equations

• Fragments.Nungon.MedialVerbs.ds3pl = { form := "-u-ya", personNumber := { person := UD.Person.third, number := UD.Number.Plur } }

def Fragments.Nungon.MedialVerbs.dsParadigm : List DSSuffix

Full DS paradigm.

Equations

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

structure Fragments.Nungon.MedialVerbs.SSSuffix : Type

SS suffixes are invariant (no person/number indexing).

• form : String
• category : SRCategory

instance Fragments.Nungon.MedialVerbs.instReprSSSuffix : Repr SSSuffix

Equations

• Fragments.Nungon.MedialVerbs.instReprSSSuffix = { reprPrec := Fragments.Nungon.MedialVerbs.instReprSSSuffix.repr }

def Fragments.Nungon.MedialVerbs.instReprSSSuffix.repr : SSSuffix → Nat → Std.Format

Equations

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

def Fragments.Nungon.MedialVerbs.instBEqSSSuffix.beq : SSSuffix → SSSuffix → Bool

Equations

• Fragments.Nungon.MedialVerbs.instBEqSSSuffix.beq { form := a, category := a_1 } { form := b, category := b_1 } = (a == b && a_1 == b_1)
• Fragments.Nungon.MedialVerbs.instBEqSSSuffix.beq x✝¹ x✝ = false

instance Fragments.Nungon.MedialVerbs.instBEqSSSuffix : BEq SSSuffix

Equations

• Fragments.Nungon.MedialVerbs.instBEqSSSuffix = { beq := Fragments.Nungon.MedialVerbs.instBEqSSSuffix.beq }

def Fragments.Nungon.MedialVerbs.ssSEQ : SSSuffix

SS sequential suffix.

Equations

• Fragments.Nungon.MedialVerbs.ssSEQ = { form := "-se", category := Fragments.Nungon.MedialVerbs.SRCategory.ssSEQ }

def Fragments.Nungon.MedialVerbs.ssSIM : SSSuffix

SS simultaneous suffix.

Equations

• Fragments.Nungon.MedialVerbs.ssSIM = { form := "-ma", category := Fragments.Nungon.MedialVerbs.SRCategory.ssSIM }

def Fragments.Nungon.MedialVerbs.ssSuffixes : List SSSuffix

All SS suffixes.

Equations

• Fragments.Nungon.MedialVerbs.ssSuffixes = [Fragments.Nungon.MedialVerbs.ssSEQ, Fragments.Nungon.MedialVerbs.ssSIM]

theorem Fragments.Nungon.MedialVerbs.ds_paradigm_size : dsParadigm.length = 9

9 cells in the DS paradigm (3 persons x 3 numbers).

theorem Fragments.Nungon.MedialVerbs.ss_suffix_count : ssSuffixes.length = 2

2 SS suffixes (sequential and simultaneous).

theorem Fragments.Nungon.MedialVerbs.du_syncretism : ds2du.form = ds3du.form

2du and 3du are syncretic (same form).

theorem Fragments.Nungon.MedialVerbs.pl_syncretism : ds2pl.form = ds3pl.form

2pl and 3pl are syncretic (same form).

theorem Fragments.Nungon.MedialVerbs.ssSEQ_is_ss : SRCategory.ssSEQ.isSS = true

SS-SEQ is same-subject.

theorem Fragments.Nungon.MedialVerbs.dsSEQ_is_ds : SRCategory.dsSEQ.isSS = false

DS-SEQ is different-subject.

theorem Fragments.Nungon.MedialVerbs.ssSEQ_is_seq : SRCategory.ssSEQ.isSequential = true

SS-SEQ is sequential.

theorem Fragments.Nungon.MedialVerbs.ssSIM_not_seq : SRCategory.ssSIM.isSequential = false

SS-SIM is not sequential (it's simultaneous).