Hausa verbs

Hausa verbs fall into morphological classes called grades, each defined by a tone pattern and a termination, a final vowel or in a few grades a final -aC: dafā̀ 'cook' is grade 1, zā̀gā 'insult' grade 2, kōmō 'return here' grade 6. A verb base operates in several grades, as sàyā 'buy' (grade 2) appears as sayḕ 'buy up' (grade 4), sayar̃ 'sell' (grade 5), sayō 'buy and bring' (grade 6) and sàyu 'be well bought' (grade 7). Within its grade a verb has up to four forms by syntactic context: the A-form with no object after it, the B-form before a personal pronoun direct object, the C-form before any other direct object, and the D-form before an indirect object, where grades 2, 3 and 7 have no form of their own and add the pre-dative suffix instead. Grades 0 to 3 are primary; grade 3 is exclusively intransitive and grade 2 exclusively transitive. The secondary grades carry meanings: grade 4 action totally done, grade 5, the efferential, action directed away from the speaker, grade 6, the ventive, action toward the speaker, and grade 7, the sustentative, an agentless passive or middle ([New00]).

Main definitions

• Hausa.Grade, Hausa.Grade.terminations, Hausa.Grade.melody — the grades and their terminations and tones by form
• Hausa.Grade.HasObjectForms, Hausa.Grade.UsesPreDative — a grade has forms before a direct object; it adds the pre-dative suffix before an indirect object
• Hausa.Verb — a verb with its grade

Main results

• Hausa.Grade.usesPreDative_iff — the grades that add the pre-dative suffix are grade 2 and the grades with no form before a direct object
• Hausa.Grade.changing_iff — grade 2 is the one grade whose A-, B- and C-forms all differ
• Hausa.Verb.isIntransitive_of_not_hasObjectForms — the entries of a grade with no form before a direct object are intransitive

Implementation notes

The terminations and tones are those of [New00]'s table of the grade system, for finite verbs outside the imperative. A grade's melody is its tone pattern on a verb of two syllables, spreading from the right, so that a lone high covers every syllable; the tone of a third syllable, which differs between forms in grades 1, 2 and 4, is not recorded. The particle dà that follows some grade 5 forms is not part of the verb and is left out, and the grade 5 form with no termination is written -Ø.

References

• [New00]

inductive Hausa.Grade : Type

The grades.

• gr0 : Grade
• gr1 : Grade
• gr2 : Grade
• gr3 : Grade
• gr3a : Grade
• gr3b : Grade
• gr4 : Grade
• gr5 : Grade
• gr5d : Grade
• gr6 : Grade
• gr7 : Grade

@[instance_reducible]

instance Hausa.instDecidableEqGrade : DecidableEq Grade

Equations

• Hausa.instDecidableEqGrade x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hausa.instReprGrade.repr : Grade → ℕ → Std.Format

Equations

• Hausa.instReprGrade.repr Hausa.Grade.gr0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Grade.gr0")).group prec✝
• Hausa.instReprGrade.repr Hausa.Grade.gr1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Grade.gr1")).group prec✝
• Hausa.instReprGrade.repr Hausa.Grade.gr2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Grade.gr2")).group prec✝
• Hausa.instReprGrade.repr Hausa.Grade.gr3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Grade.gr3")).group prec✝
• Hausa.instReprGrade.repr Hausa.Grade.gr3a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Grade.gr3a")).group prec✝
• Hausa.instReprGrade.repr Hausa.Grade.gr3b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Grade.gr3b")).group prec✝
• Hausa.instReprGrade.repr Hausa.Grade.gr4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Grade.gr4")).group prec✝
• Hausa.instReprGrade.repr Hausa.Grade.gr5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Grade.gr5")).group prec✝
• Hausa.instReprGrade.repr Hausa.Grade.gr5d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Grade.gr5d")).group prec✝
• Hausa.instReprGrade.repr Hausa.Grade.gr6 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Grade.gr6")).group prec✝
• Hausa.instReprGrade.repr Hausa.Grade.gr7 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Grade.gr7")).group prec✝

@[instance_reducible]

instance Hausa.instReprGrade : Repr Grade

Equations

• Hausa.instReprGrade = { reprPrec := Hausa.instReprGrade.repr }

@[instance_reducible]

instance Hausa.instFintypeGrade : Fintype Grade

Equations

• Hausa.instFintypeGrade = { elems := { val := ↑Hausa.Grade.enumList, nodup := Hausa.Grade.enumList_nodup }, complete := Hausa.instFintypeGrade._proof_1 }

inductive Hausa.VerbForm : Type

The forms of a verb by syntactic context.

• A : VerbForm

  With no object after the verb.

• B : VerbForm

  Before a personal pronoun direct object.

• C : VerbForm

  Before any other direct object.

• D : VerbForm

  Before an indirect object.

@[instance_reducible]

instance Hausa.instDecidableEqVerbForm : DecidableEq VerbForm

Equations

• Hausa.instDecidableEqVerbForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hausa.instReprVerbForm.repr : VerbForm → ℕ → Std.Format

Equations

• Hausa.instReprVerbForm.repr Hausa.VerbForm.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.VerbForm.A")).group prec✝
• Hausa.instReprVerbForm.repr Hausa.VerbForm.B prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.VerbForm.B")).group prec✝
• Hausa.instReprVerbForm.repr Hausa.VerbForm.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.VerbForm.C")).group prec✝
• Hausa.instReprVerbForm.repr Hausa.VerbForm.D prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.VerbForm.D")).group prec✝

@[instance_reducible]

instance Hausa.instReprVerbForm : Repr VerbForm

Equations

• Hausa.instReprVerbForm = { reprPrec := Hausa.instReprVerbForm.repr }

@[instance_reducible]

instance Hausa.instFintypeVerbForm : Fintype VerbForm

Equations

• Hausa.instFintypeVerbForm = { elems := { val := ↑Hausa.VerbForm.enumList, nodup := Hausa.VerbForm.enumList_nodup }, complete := Hausa.instFintypeVerbForm._proof_1 }

def Hausa.Grade.terminations : Grade → VerbForm → Finset String

The terminations of a grade in a form; empty where the grade has no such form.

Equations

• Hausa.Grade.gr0.terminations Hausa.VerbForm.A = {"-i", "-ā", "-ō"}
• Hausa.Grade.gr0.terminations Hausa.VerbForm.C = {"-i", "-ā", "-ō"}
• Hausa.Grade.gr0.terminations Hausa.VerbForm.B = {"-ī", "-ā", "-ō"}
• Hausa.Grade.gr0.terminations Hausa.VerbForm.D = {"-i", "-ī", "-ā", "-ō"}
• Hausa.Grade.gr1.terminations Hausa.VerbForm.C = {"-a"}
• Hausa.Grade.gr1.terminations x✝ = {"-ā"}
• Hausa.Grade.gr2.terminations Hausa.VerbForm.A = {"-ā"}
• Hausa.Grade.gr2.terminations Hausa.VerbForm.B = {"-ē"}
• Hausa.Grade.gr2.terminations Hausa.VerbForm.C = {"-i"}
• Hausa.Grade.gr3.terminations Hausa.VerbForm.A = {"-a"}
• Hausa.Grade.gr3a.terminations Hausa.VerbForm.A = {"-a"}
• Hausa.Grade.gr3b.terminations Hausa.VerbForm.A = {"-i", "-u", "-a"}
• Hausa.Grade.gr4.terminations Hausa.VerbForm.C = {"-e", "-ē", "-nye", "-nyē"}
• Hausa.Grade.gr4.terminations x✝ = {"-ē", "-nyē"}
• Hausa.Grade.gr5.terminations Hausa.VerbForm.A = {"-ar̃"}
• Hausa.Grade.gr5.terminations Hausa.VerbForm.D = {"-ar̃"}
• Hausa.Grade.gr5.terminations Hausa.VerbForm.B = {"-ar̃", "-shē", "-Ø"}
• Hausa.Grade.gr5.terminations Hausa.VerbForm.C = {"-ar̃", "-Ø"}
• Hausa.Grade.gr5d.terminations Hausa.VerbForm.C = {"-dà"}
• Hausa.Grade.gr5d.terminations x✝ = {"-dā"}
• Hausa.Grade.gr6.terminations x✝ = {"-ō"}
• Hausa.Grade.gr7.terminations Hausa.VerbForm.A = {"-u"}
• x✝¹.terminations x✝ = ∅

def Hausa.Grade.melody : Grade → List Tone.TRN

The tone pattern of a grade on a verb of two syllables.

Equations

• Hausa.Grade.gr0.melody = [Tone.TRN.H]
• Hausa.Grade.gr3a.melody = [Tone.TRN.H]
• Hausa.Grade.gr5.melody = [Tone.TRN.H]
• Hausa.Grade.gr6.melody = [Tone.TRN.H]
• Hausa.Grade.gr1.melody = [Tone.TRN.H, Tone.TRN.L]
• Hausa.Grade.gr3b.melody = [Tone.TRN.H, Tone.TRN.L]
• Hausa.Grade.gr4.melody = [Tone.TRN.H, Tone.TRN.L]
• Hausa.Grade.gr5d.melody = [Tone.TRN.H, Tone.TRN.L]
• Hausa.Grade.gr2.melody = [Tone.TRN.L, Tone.TRN.H]
• Hausa.Grade.gr3.melody = [Tone.TRN.L, Tone.TRN.H]
• Hausa.Grade.gr7.melody = [Tone.TRN.L, Tone.TRN.H]

def Hausa.Grade.HasObjectForms (g : Grade) : Prop

The grade has forms before a direct object.

Equations

• g.HasObjectForms = ((g.terminations Hausa.VerbForm.B).Nonempty ∧ (g.terminations Hausa.VerbForm.C).Nonempty)

@[instance_reducible]

instance Hausa.Grade.instDecidableHasObjectForms (g : Grade) : Decidable g.HasObjectForms

Equations

• g.instDecidableHasObjectForms = { decide := decide (g.terminations Hausa.VerbForm.B).Nonempty && decide (g.terminations Hausa.VerbForm.C).Nonempty, reflects_decide := ⋯ }

def Hausa.Grade.UsesPreDative (g : Grade) : Prop

The grade has no D-form and adds the pre-dative suffix before an indirect object.

Equations

• g.UsesPreDative = (g.terminations Hausa.VerbForm.D = ∅)

@[instance_reducible]

instance Hausa.Grade.instDecidableUsesPreDative (g : Grade) : Decidable g.UsesPreDative

Equations

• g.instDecidableUsesPreDative = { decide := decide ((g.terminations Hausa.VerbForm.D).val = ∅.val), reflects_decide := ⋯ }

theorem Hausa.Grade.usesPreDative_iff (g : Grade) : g.UsesPreDative ↔ g = gr2 ∨ ¬g.HasObjectForms

The grades that add the pre-dative suffix are grade 2 and those with no form before a direct object, grades 3, 3a, 3b and 7.

theorem Hausa.Grade.changing_iff (g : Grade) : g.HasObjectForms ∧ Disjoint (g.terminations VerbForm.A) (g.terminations VerbForm.B) ∧ Disjoint (g.terminations VerbForm.B) (g.terminations VerbForm.C) ∧ Disjoint (g.terminations VerbForm.A) (g.terminations VerbForm.C) ↔ g = gr2

Grade 2 is the one grade whose A-, B- and C-forms all differ.

structure Hausa.Verbextends Verb : Type

A Hausa verb, cited in its A-form, with the grade it operates in.

• 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
• grade : Grade

def Hausa.ci : Verb

ci 'eat'.

Equations

• Hausa.ci = { valency := Verb.Valency.ofFrame ArgumentFrame.np, morphs := [Morphology.Morph.root "ci"], grade := Hausa.Grade.gr0 }

def Hausa.ja : Verb

jā 'pull'.

Equations

• Hausa.ja = { valency := Verb.Valency.ofFrame ArgumentFrame.np, morphs := [Morphology.Morph.root "jā"], grade := Hausa.Grade.gr0 }

def Hausa.dafa : Verb

dafā̀ 'cook'.

Equations

• Hausa.dafa = { valency := Verb.Valency.ofFrame ArgumentFrame.np, morphs := [Morphology.Morph.root "dafā̀"], grade := Hausa.Grade.gr1 }

def Hausa.zaga : Verb

zā̀gā 'insult'.

Equations

• Hausa.zaga = { valency := Verb.Valency.ofFrame ArgumentFrame.np, morphs := [Morphology.Morph.root "zā̀gā"], grade := Hausa.Grade.gr2 }

def Hausa.saya : Verb

sàyā 'buy', C-form sàyi.

Equations

• Hausa.saya = { valency := Verb.Valency.ofFrame ArgumentFrame.np, morphs := [Morphology.Morph.root "sàyā"], grade := Hausa.Grade.gr2 }

def Hausa.fita : Verb

fita 'go out'.

Equations

• Hausa.fita = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, morphs := [Morphology.Morph.root "fita"], grade := Hausa.Grade.gr3 }

def Hausa.kaura : Verb

ƙaura 'migrate'.

Equations

• Hausa.kaura = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, morphs := [Morphology.Morph.root "ƙaura"], grade := Hausa.Grade.gr3a }

def Hausa.gudu : Verb

guɗù 'run away'.

Equations

• Hausa.gudu = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, morphs := [Morphology.Morph.root "guɗù"], grade := Hausa.Grade.gr3b }

def Hausa.saye : Verb

sayḕ 'buy up'.

Equations

• Hausa.saye = { valency := Verb.Valency.ofFrame ArgumentFrame.np, morphs := [Morphology.Morph.root "sayḕ"], grade := Hausa.Grade.gr4 }

def Hausa.sayar : Verb

sayar̃ 'sell'.

Equations

• Hausa.sayar = { valency := Verb.Valency.ofFrame ArgumentFrame.np, morphs := [Morphology.Morph.root "sayar̃"], grade := Hausa.Grade.gr5 }

def Hausa.sayo : Verb

sayō 'buy and bring'.

Equations

• Hausa.sayo = { valency := Verb.Valency.ofFrame ArgumentFrame.np, morphs := [Morphology.Morph.root "sayō"], grade := Hausa.Grade.gr6 }

def Hausa.komo : Verb

kōmō 'return here'.

Equations

• Hausa.komo = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, morphs := [Morphology.Morph.root "kōmō"], grade := Hausa.Grade.gr6 }

def Hausa.sayu : Verb

sàyu 'be well bought'.

Equations

• Hausa.sayu = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, morphs := [Morphology.Morph.root "sàyu"], grade := Hausa.Grade.gr7 }

def Hausa.gyaru : Verb

gyā̀ru 'be well repaired'.

Equations

• Hausa.gyaru = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, morphs := [Morphology.Morph.root "gyā̀ru"], grade := Hausa.Grade.gr7 }

def Hausa.verbs : List Verb

The verbs.

Equations

• Hausa.verbs = [Hausa.ci, Hausa.ja, Hausa.dafa, Hausa.zaga, Hausa.saya, Hausa.fita, Hausa.kaura, Hausa.gudu, Hausa.saye, Hausa.sayar, Hausa.sayo, Hausa.komo, Hausa.sayu, Hausa.gyaru]

theorem Hausa.Verb.isIntransitive_of_not_hasObjectForms (v : Verb) : v ∈ verbs → ¬v.grade.HasObjectForms → v.IsIntransitive

The verbs of a grade with no form before a direct object are intransitive.