Hausa focus and the stabilizer nē/cē

Hausa focuses a constituent by fronting it (ex-situ) or leaving it in place (in-situ). Ex-situ focus shifts the clause's TAM to the Relative form where one exists; the agreeing polar-tone particle nē/cē — Newman's stabilizer ([New00] §66) — may surface after the focus in either strategy, and in-situ focus is otherwise unmarked, prosody included ([HZ07] §2, §5).

Main definitions

• Strategy: in-situ vs ex-situ focus.
• Stabilizer, stabilizerFor: the particle's two allomorphs and their selection by gender and number.
• FocusConfig: a focused clause's PAC, strategy, focus agreement features, and stabilizer.
• FocusConfig.Licensed: ex-situ focus with a Relative-capable TAM must surface Relative mode ([JG03] analyse this as movement to a single CP-internal position; only the licensing condition is recorded here).

Main results

• stabilizerFor_eq_cee_iff: cē appears exactly with feminine-singular focus.
• stabilizer_tone_is_polar: the stabilizer's surface tone is Hausa.polarOf of the host's final tone — the same autosegmental operation as the genitive linker -n.

Implementation notes

Licensed is propositional, not a Subtype invariant: FocusConfig is unrestricted, and exSitu_with_genCmp is an explicit ill-licensed configuration showing the predicate has bite. mkInSitu/mkExSitu are ergonomic constructors; the ex-situ one takes the licensing obligation as an argument.

Strategy and stabilizer

inductive Hausa.Strategy : Type

The two focus strategies of Hausa. Pragmatic-type distinctions cut across both strategies and live in study files.

• inSitu : Strategy
• exSitu : Strategy

@[implicit_reducible]

instance Hausa.instDecidableEqStrategy : DecidableEq Strategy

Equations

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

@[implicit_reducible]

instance Hausa.instReprStrategy : Repr Strategy

Equations

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

def Hausa.instReprStrategy.repr : Strategy → ℕ → Std.Format

Equations

• Hausa.instReprStrategy.repr Hausa.Strategy.inSitu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Strategy.inSitu")).group prec✝
• Hausa.instReprStrategy.repr Hausa.Strategy.exSitu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Strategy.exSitu")).group prec✝

@[implicit_reducible]

instance Hausa.instInhabitedStrategy : Inhabited Strategy

Equations

• Hausa.instInhabitedStrategy = { default := Hausa.instInhabitedStrategy.default }

inductive Hausa.Stabilizer : Type

The stabilizer's allomorphs: cē with feminine-singular focus, nē elsewhere ([New00] §66.1).

• nee : Stabilizer
• cee : Stabilizer

@[implicit_reducible]

instance Hausa.instDecidableEqStabilizer : DecidableEq Stabilizer

Equations

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

def Hausa.instReprStabilizer.repr : Stabilizer → ℕ → Std.Format

Equations

• Hausa.instReprStabilizer.repr Hausa.Stabilizer.nee prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Stabilizer.nee")).group prec✝
• Hausa.instReprStabilizer.repr Hausa.Stabilizer.cee prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Stabilizer.cee")).group prec✝

@[implicit_reducible]

instance Hausa.instReprStabilizer : Repr Stabilizer

Equations

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

@[implicit_reducible]

instance Hausa.instInhabitedStabilizer : Inhabited Stabilizer

Equations

• Hausa.instInhabitedStabilizer = { default := Hausa.instInhabitedStabilizer.default }

def Hausa.Stabilizer.form : Stabilizer → String

Surface form of the stabilizer.

Equations

• Hausa.Stabilizer.nee.form = "nē"
• Hausa.Stabilizer.cee.form = "cē"

def Hausa.stabilizerFor (g : Gender) (singular : Bool) : Stabilizer

The stabilizer agreeing with a focus of the given gender and number: cē iff feminine singular; plurals of either gender take nē ([New00] §66.1).

Equations

• Hausa.stabilizerFor Gender.feminine true = Hausa.Stabilizer.cee
• Hausa.stabilizerFor g singular = Hausa.Stabilizer.nee

Focus configurations

structure Hausa.FocusConfig : Type

A focused clause: its PAC, focus strategy, the focused constituent's agreement features, and whether a stabilizer surfaces.

• pac : PAC

  The clause's person-aspect complex.

• strategy : Strategy

  The focus strategy.

• focusG : Gender

  Gender of the focused constituent (selects nē vs cē).

• focusSG : Bool

  Whether the focused constituent is singular.

• hasStab : Bool

  Whether a stabilizer surfaces (optional ex-situ, sporadic sentence-final in-situ, [HZ07] §2.2).

def Hausa.instReprFocusConfig.repr : FocusConfig → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Hausa.instReprFocusConfig : Repr FocusConfig

Equations

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

def Hausa.FocusConfig.stab? (c : FocusConfig) : Option Stabilizer

The stabilizer realised by a configuration, if any.

Equations

• c.stab? = if c.hasStab = true then some (Hausa.stabilizerFor c.focusG c.focusSG) else none

def Hausa.FocusConfig.Licensed (c : FocusConfig) : Prop

Ex-situ focus must surface the Relative mode whenever the TAM has a Relative form; in-situ focus is unconstrained ([New00] §65–§66).

Equations

• c.Licensed = (c.strategy = Hausa.Strategy.exSitu → c.pac.tam.HasRelativeForm → c.pac.mode = Hausa.Mode.relative)

@[implicit_reducible]

instance Hausa.instDecidableLicensed (c : FocusConfig) : Decidable c.Licensed

Equations

• Hausa.instDecidableLicensed c = Hausa.instDecidableLicensed._aux_1 c

Constructors

def Hausa.mkInSitu (pac : PAC) (focusG : Gender) (focusSG : Bool) (hasStab : Bool := false) : FocusConfig

An in-situ focus configuration; always licensed. The stabilizer defaults to absent but may sporadically surface sentence-finally ([HZ07] §2.2).

Equations

• Hausa.mkInSitu pac focusG focusSG hasStab = { pac := pac, strategy := Hausa.Strategy.inSitu, focusG := focusG, focusSG := focusSG, hasStab := hasStab }

def Hausa.mkExSitu (pac : PAC) (focusG : Gender) (focusSG : Bool) : (pac.tam.HasRelativeForm → pac.mode = Mode.relative) → (hasStab : optParam Bool true) → FocusConfig

An ex-situ focus configuration; the anonymous argument is the licensing obligation it threads (see mkExSitu_licensed).

Equations

• Hausa.mkExSitu pac focusG focusSG x✝ hasStab = { pac := pac, strategy := Hausa.Strategy.exSitu, focusG := focusG, focusSG := focusSG, hasStab := hasStab }

theorem Hausa.mkInSitu_licensed (p : PAC) (g : Gender) (sg hs : Bool) : (mkInSitu p g sg hs).Licensed

theorem Hausa.mkExSitu_licensed (p : PAC) (g : Gender) (sg : Bool) (h : p.tam.HasRelativeForm → p.mode = Mode.relative) (hs : Bool) : (mkExSitu p g sg h hs).Licensed

Examples

def Hausa.exSitu_fem_relCmp : FocusConfig

Ex-situ feminine-singular focus with the Relative completive; licensed, surfaces cē.

Equations

• Hausa.exSitu_fem_relCmp = Hausa.mkExSitu Hausa.cmp_3sm_R Gender.feminine true Hausa.exSitu_fem_relCmp._proof_1

def Hausa.inSitu_any : FocusConfig

In-situ focus with a General-mode PAC; licensed unconditionally.

Equations

• Hausa.inSitu_any = Hausa.mkInSitu Hausa.cmp_3sm_G Gender.masculine true

def Hausa.exSitu_with_genCmp : FocusConfig

An ill-licensed ex-situ configuration with the General completive, built directly to show Licensed has bite.

Equations

• Hausa.exSitu_with_genCmp = { pac := Hausa.cmp_3sm_G, strategy := Hausa.Strategy.exSitu, focusG := Gender.masculine, focusSG := true, hasStab := false }

def Hausa.focusConfigs : List FocusConfig

The licensed focus-configuration registry used downstream; exSitu_with_genCmp is deliberately excluded.

Equations

• Hausa.focusConfigs = [Hausa.exSitu_fem_relCmp, Hausa.inSitu_any]

Licensing and agreement

theorem Hausa.stabilizerFor_eq_cee_iff (g : Gender) (sg : Bool) : stabilizerFor g sg = Stabilizer.cee ↔ g = Gender.feminine ∧ sg = true

cē appears exactly with feminine-singular focus.

theorem Hausa.all_focusConfigs_licensed (c : FocusConfig) : c ∈ focusConfigs → c.Licensed

theorem Hausa.exSitu_with_genCmp_not_licensed : ¬exSitu_with_genCmp.Licensed

theorem Hausa.exSitu_fem_picks_cee : exSitu_fem_relCmp.stab? = some Stabilizer.cee

The feminine-singular ex-situ example surfaces cē.

Stabilizer tone

def Hausa.Stabilizer.toneAfter : Stabilizer → (host : Tone.TRN) → Tone.TRN

Surface tone of the stabilizer after a host whose final TBU carries the given tone: polar, i.e. the opposite of the host ([New00] §66.1).

Equations

• x✝.toneAfter host = Hausa.polarOf host

theorem Hausa.stabilizer_tone_is_polar (s : Stabilizer) (host : Tone.TRN) : s.toneAfter host = polarOf host

The stabilizer's surface tone is Hausa.polarOf of the host tone — the same autosegmental operation as the genitive linker -n, not a separate stipulation.

theorem Hausa.stabilizer_toneAfter_involutive (s : Stabilizer) (h : Tone.TRN) (hh : h ∈ [Tone.TRN.H, Tone.TRN.L]) : polarOf (s.toneAfter h) = h

Two applications of the stabilizer-tone map restore the host tone on the H/L sublattice. Direct corollary of polarOf_involutive_on_HL.