Manambu medial clauses

Manambu (Ndu, East Sepik Province, Papua New Guinea) chains medial clauses before a single main clause and marks the medial predicate with one of nine suffixes. Six are sensitive to switch-reference: the completive pair -ku (same subject) and -k (different subject) 'after', -ta:y 'while' and -taka 'as soon as' with same-subject forms only, and -kǝb (different subject) and -ta:y-kǝb (same subject) for a brief temporal overlap; -ga:y 'if' marks an unlikely condition with the same subject, and -lǝk 'because' and the versatile -n are neutral. The verb is bare before the same-subject markers and -n, carries subject cross-referencing before -k and -kǝb, and the tensed cross-referencing of a main clause before -lǝk. Medial clauses are negated with -ma:r-, except after -ga:y, and the same-subject completive and -n clauses occur on their own.

Implementation notes

• The clause-chaining typology over the markers is in Studies/SarvasyAikhenvald2025.lean.

References

• [Aik08]
• [Aik25]

inductive Manambu.MedialInflection : Type

The inflection a medial verb carries before its marker.

• uninflected : MedialInflection

  The bare stem.

• subject : MedialInflection

  The non-tensed subject cross-referencing markers of a dependent verb.

• tensedSubject : MedialInflection

  The tensed subject cross-referencing of a main-clause verb.

@[instance_reducible]

instance Manambu.instDecidableEqMedialInflection : DecidableEq MedialInflection

Equations

• Manambu.instDecidableEqMedialInflection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Manambu.instReprMedialInflection.repr : MedialInflection → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Manambu.instReprMedialInflection : Repr MedialInflection

Equations

• Manambu.instReprMedialInflection = { reprPrec := Manambu.instReprMedialInflection.repr }

@[instance_reducible]

instance Manambu.instFintypeMedialInflection : Fintype MedialInflection

Equations

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

inductive Manambu.MedialMarker : Type

The markers of medial clauses, suffixes on the medial predicate.

• ku : MedialMarker

  -ku, the same-subject completive 'after', also read as reason.

• k : MedialMarker

  -k, the different-subject completive 'after', also read as reason or real condition.

• tay : MedialMarker

  -ta:y 'while', cotemporaneous 'before, during and after', same subject only.

• taka : MedialMarker

  -taka 'as soon as', immediate sequence, same subject only; -tataka after a light root.

• keb : MedialMarker

  -kǝb 'as soon as', immediate sequence with a possible short overlap, different subject; -kǝkǝb after a light root.

• taykeb : MedialMarker

  -ta:y-kǝb, an action started before the following clause's and overlapping with it, same subject.

• lek : MedialMarker

  -lǝk 'because', not sensitive to switch-reference.

• gay : MedialMarker

  -ga:y 'if', an unlikely condition, same subject.

• n : MedialMarker

  -n, simultaneous, preceding or concomitant action or manner, not sensitive to switch-reference.

@[instance_reducible]

instance Manambu.instDecidableEqMedialMarker : DecidableEq MedialMarker

Equations

• Manambu.instDecidableEqMedialMarker x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Manambu.instReprMedialMarker.repr : MedialMarker → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Manambu.instReprMedialMarker.repr Manambu.MedialMarker.ku prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Manambu.MedialMarker.ku")).group prec✝
• Manambu.instReprMedialMarker.repr Manambu.MedialMarker.k prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Manambu.MedialMarker.k")).group prec✝
• Manambu.instReprMedialMarker.repr Manambu.MedialMarker.tay prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Manambu.MedialMarker.tay")).group prec✝
• Manambu.instReprMedialMarker.repr Manambu.MedialMarker.taka prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Manambu.MedialMarker.taka")).group prec✝
• Manambu.instReprMedialMarker.repr Manambu.MedialMarker.keb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Manambu.MedialMarker.keb")).group prec✝
• Manambu.instReprMedialMarker.repr Manambu.MedialMarker.lek prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Manambu.MedialMarker.lek")).group prec✝
• Manambu.instReprMedialMarker.repr Manambu.MedialMarker.gay prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Manambu.MedialMarker.gay")).group prec✝
• Manambu.instReprMedialMarker.repr Manambu.MedialMarker.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Manambu.MedialMarker.n")).group prec✝

@[instance_reducible]

instance Manambu.instReprMedialMarker : Repr MedialMarker

Equations

• Manambu.instReprMedialMarker = { reprPrec := Manambu.instReprMedialMarker.repr }

@[instance_reducible]

instance Manambu.instFintypeMedialMarker : Fintype MedialMarker

Equations

• Manambu.instFintypeMedialMarker = { elems := { val := ↑Manambu.MedialMarker.enumList, nodup := Manambu.MedialMarker.enumList_nodup }, complete := Manambu.instFintypeMedialMarker._proof_1 }

def Manambu.MedialMarker.morphs : MedialMarker → List Morphology.Morph

The morphs of a marker.

Equations

• Manambu.MedialMarker.ku.morphs = [Morphology.Morph.suff "ku"]
• Manambu.MedialMarker.k.morphs = [Morphology.Morph.suff "k"]
• Manambu.MedialMarker.tay.morphs = [Morphology.Morph.suff "ta:y"]
• Manambu.MedialMarker.taka.morphs = [Morphology.Morph.suff "taka"]
• Manambu.MedialMarker.keb.morphs = [Morphology.Morph.suff "kǝb"]
• Manambu.MedialMarker.taykeb.morphs = [Morphology.Morph.suff "ta:y", Morphology.Morph.suff "kǝb"]
• Manambu.MedialMarker.lek.morphs = [Morphology.Morph.suff "lǝk"]
• Manambu.MedialMarker.gay.morphs = [Morphology.Morph.suff "ga:y"]
• Manambu.MedialMarker.n.morphs = [Morphology.Morph.suff "n"]

def Manambu.MedialMarker.form (m : MedialMarker) : String

The form of a marker in boundary notation.

Equations

• m.form = Morphology.Morph.surface m.morphs

def Manambu.MedialMarker.sr : MedialMarker → Option Clause.Chaining.SwitchReference

The switch-reference value a marker carries; none for -lǝk and -n.

Equations

• Manambu.MedialMarker.ku.sr = some Clause.Chaining.SwitchReference.ss
• Manambu.MedialMarker.tay.sr = some Clause.Chaining.SwitchReference.ss
• Manambu.MedialMarker.taka.sr = some Clause.Chaining.SwitchReference.ss
• Manambu.MedialMarker.taykeb.sr = some Clause.Chaining.SwitchReference.ss
• Manambu.MedialMarker.gay.sr = some Clause.Chaining.SwitchReference.ss
• Manambu.MedialMarker.k.sr = some Clause.Chaining.SwitchReference.ds
• Manambu.MedialMarker.keb.sr = some Clause.Chaining.SwitchReference.ds
• Manambu.MedialMarker.lek.sr = none
• Manambu.MedialMarker.n.sr = none

def Manambu.MedialMarker.relations : MedialMarker → Finset Clause.Chaining.InterclauseRelation

The interclausal relations a marker encodes.

Equations

• Manambu.MedialMarker.ku.relations = {Clause.Chaining.InterclauseRelation.sequential, Clause.Chaining.InterclauseRelation.causal}
• Manambu.MedialMarker.k.relations = {Clause.Chaining.InterclauseRelation.sequential, Clause.Chaining.InterclauseRelation.causal, Clause.Chaining.InterclauseRelation.conditional}
• Manambu.MedialMarker.tay.relations = {Clause.Chaining.InterclauseRelation.simultaneous}
• Manambu.MedialMarker.taykeb.relations = {Clause.Chaining.InterclauseRelation.simultaneous}
• Manambu.MedialMarker.taka.relations = {Clause.Chaining.InterclauseRelation.sequential}
• Manambu.MedialMarker.keb.relations = {Clause.Chaining.InterclauseRelation.sequential, Clause.Chaining.InterclauseRelation.simultaneous}
• Manambu.MedialMarker.lek.relations = {Clause.Chaining.InterclauseRelation.causal}
• Manambu.MedialMarker.gay.relations = {Clause.Chaining.InterclauseRelation.conditional}
• Manambu.MedialMarker.n.relations = {Clause.Chaining.InterclauseRelation.sequential, Clause.Chaining.InterclauseRelation.simultaneous, Clause.Chaining.InterclauseRelation.manner}

def Manambu.MedialMarker.inflection : MedialMarker → MedialInflection

The inflection of the verb before the marker.

Equations

• Manambu.MedialMarker.ku.inflection = Manambu.MedialInflection.uninflected
• Manambu.MedialMarker.tay.inflection = Manambu.MedialInflection.uninflected
• Manambu.MedialMarker.taka.inflection = Manambu.MedialInflection.uninflected
• Manambu.MedialMarker.taykeb.inflection = Manambu.MedialInflection.uninflected
• Manambu.MedialMarker.gay.inflection = Manambu.MedialInflection.uninflected
• Manambu.MedialMarker.n.inflection = Manambu.MedialInflection.uninflected
• Manambu.MedialMarker.k.inflection = Manambu.MedialInflection.subject
• Manambu.MedialMarker.keb.inflection = Manambu.MedialInflection.subject
• Manambu.MedialMarker.lek.inflection = Manambu.MedialInflection.tensedSubject

def Manambu.MedialMarker.IndexesSubject (m : MedialMarker) : Prop

The verb before the marker cross-references its subject.

Equations

• m.IndexesSubject = (m.inflection ≠ Manambu.MedialInflection.uninflected)

@[instance_reducible]

instance Manambu.MedialMarker.instDecidablePredIndexesSubject : DecidablePred IndexesSubject

Equations

• x✝.instDecidablePredIndexesSubject = { decide := !decide (x✝.inflection = Manambu.MedialInflection.uninflected), reflects_decide := ⋯ }

def Manambu.MedialMarker.HeadsPredicate (m : MedialMarker) : Prop

The marked verb can head the predicate of a verbless clause.

Equations

• m.HeadsPredicate = (m = Manambu.MedialMarker.n ∨ m = Manambu.MedialMarker.tay ∨ m = Manambu.MedialMarker.keb)

@[instance_reducible]

instance Manambu.MedialMarker.instDecidablePredHeadsPredicate : DecidablePred HeadsPredicate

Equations

• x✝.instDecidablePredHeadsPredicate = { decide := decide (x✝ = Manambu.MedialMarker.n) || decide (x✝ = Manambu.MedialMarker.tay ∨ x✝ = Manambu.MedialMarker.keb), reflects_decide := ⋯ }

def Manambu.MedialMarker.Negatable (m : MedialMarker) : Prop

The medial clause can be negated.

Equations

• m.Negatable = (m ≠ Manambu.MedialMarker.gay)

@[instance_reducible]

instance Manambu.MedialMarker.instDecidablePredNegatable : DecidablePred Negatable

Equations

• x✝.instDecidablePredNegatable = { decide := !decide (x✝ = Manambu.MedialMarker.gay), reflects_decide := ⋯ }

def Manambu.MedialMarker.WithCompletive (m : MedialMarker) : Prop

The marker combines with the completive auxiliary napa-.

Equations

• m.WithCompletive = (m ≠ Manambu.MedialMarker.taykeb ∧ m ≠ Manambu.MedialMarker.lek ∧ m ≠ Manambu.MedialMarker.gay)

@[instance_reducible]

instance Manambu.MedialMarker.instDecidablePredWithCompletive : DecidablePred WithCompletive

Equations

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

def Manambu.MedialMarker.StandsAlone (m : MedialMarker) : Prop

A medial clause with the marker occurs on its own, as a command or with a resultative sense.

Equations

• m.StandsAlone = (m = Manambu.MedialMarker.ku ∨ m = Manambu.MedialMarker.n)

@[instance_reducible]

instance Manambu.MedialMarker.instDecidablePredStandsAlone : DecidablePred StandsAlone

Equations

• x✝.instDecidablePredStandsAlone = { decide := decide (x✝ = Manambu.MedialMarker.ku) || decide (x✝ = Manambu.MedialMarker.n), reflects_decide := ⋯ }

@[instance_reducible]

instance Manambu.MedialMarker.instMedialForm : Clause.Chaining.MedialForm MedialMarker

Equations

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

def Manambu.dependentNegator : Morphology.Morph

-ma:r-, the negator of dependent clauses.

Equations

• Manambu.dependentNegator = Morphology.Morph.suff "ma:r"

def Manambu.completive : Morphology.Morph

napa-, the completive auxiliary of medial clauses.

Equations

• Manambu.completive = Morphology.Morph.root "napa"