Yoruba focus

Yorùbá focuses a constituent either in place, with no marking of any kind, or by fronting it to the beginning of the clause, where a focus particle accompanies it: asked what did Adé buy?, a speaker answers Adé ra bàtà as it stands or Bàtà ni Adé rà 'Adé bought A SHOE'. A focused subject must front, and the vacated subject position is then filled by the high-tone ó: Adé ni ó rà bàtà 'ADÉ bought a shoe', never Adé rà bàtà as an answer to who bought a shoe?. A fronted object or adjunct leaves its position empty, as under relativization. The dialects differ in where the particle stands. Standard (Ọ̀yọ́) Yorùbá places ni immediately after the fronted constituent, as in Awobuluyi's Omi mímu ni mo lọ pọn 'It was drinking water that I went to fetch'; the south-eastern dialect Ìkálẹ̀ places rín at the end of the clause whatever has been fronted, Adé ó jẹ ejíjẹ nẹ̀ rín 'ADÉ ate the food' and Tolú Adé rí rín 'Adé saw TOLÚ', against in-place Adé rí Tolú with no particle. Aremu describes the standard dialect in the dissertation and Ìkálẹ̀ in the chapter.

Main declarations

• Yoruba.Dialect, Yoruba.Dialect.focusParticle: the two dialects and each one's particle, a Particle positioned after its host or clause-finally.
• Yoruba.Focused: the focusable constituents; WithTop Focused hosts the reflexes, the clause on top of them.
• Yoruba.FocusConfig, Yoruba.FocusConfig.Licensed, Yoruba.FocusConfig.reflexes: a dialect, a focused constituent and a strategy; subject focus is only ex situ; the overt reflexes of a configuration in the Reflex vocabulary.
• Yoruba.piedPipes_iff: the particle is hosted above its focus exactly when it is clause-final, so Ìkálẹ̀ marks focus in the pied-piping configuration and the standard dialect on the focus itself.
• Yoruba.refutes_perceptibility: in-place focus has no reflex, the Yorùbá side of the Tangale and Hausa counterexamples to universal overt focus marking.
• Yoruba.npRel_eq_relative: a fronted focus vacates its position as relativization does.

References

• [Are25a]
• [Are25b]
• [Awo78]

Dialects and their particles

inductive Yoruba.Dialect : Type

The two dialects whose focus marking is recorded here, the standard (Ọ̀yọ́) dialect and the south-eastern dialect Ìkálẹ̀.

• standard : Dialect
• ikale : Dialect

@[instance_reducible]

instance Yoruba.instDecidableEqDialect : DecidableEq Dialect

Equations

• Yoruba.instDecidableEqDialect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Yoruba.instReprDialect.repr : Dialect → ℕ → Std.Format

Equations

• Yoruba.instReprDialect.repr Yoruba.Dialect.standard prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yoruba.Dialect.standard")).group prec✝
• Yoruba.instReprDialect.repr Yoruba.Dialect.ikale prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yoruba.Dialect.ikale")).group prec✝

@[instance_reducible]

instance Yoruba.instReprDialect : Repr Dialect

Equations

• Yoruba.instReprDialect = { reprPrec := Yoruba.instReprDialect.repr }

@[instance_reducible]

instance Yoruba.instFintypeDialect : Fintype Dialect

Equations

• Yoruba.instFintypeDialect = { elems := { val := ↑Yoruba.Dialect.enumList, nodup := Yoruba.Dialect.enumList_nodup }, complete := Yoruba.instFintypeDialect._proof_1 }

def Yoruba.ni : Particle

Standard Yorùbá ni, immediately after the fronted constituent.

Equations

• Yoruba.ni = { form := "ni", position := some Particle.Position.postHost }

def Yoruba.rin : Particle

Ìkálẹ̀ rín, at the end of the clause.

Equations

• Yoruba.rin = { form := "rín", position := some Particle.Position.clauseFinal }

def Yoruba.Dialect.focusParticle : Dialect → Particle

Each dialect's focus particle.

Equations

• Yoruba.Dialect.standard.focusParticle = Yoruba.ni
• Yoruba.Dialect.ikale.focusParticle = Yoruba.rin

def Yoruba.o : Morphology.Morph

The high-tone ó filling the subject position of a clause whose subject has been fronted.

Equations

• Yoruba.o = Morphology.Morph.free "ó"

Focusable constituents and hosts

inductive Yoruba.Focused : Type

A focus construction fronts the subject, the object, or an adjunct.

• subject : Focused
• object : Focused
• adjunct : Focused

@[instance_reducible]

instance Yoruba.instDecidableEqFocused : DecidableEq Focused

Equations

• Yoruba.instDecidableEqFocused x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Yoruba.instReprFocused : Repr Focused

Equations

• Yoruba.instReprFocused = { reprPrec := Yoruba.instReprFocused.repr }

def Yoruba.instReprFocused.repr : Focused → ℕ → Std.Format

Equations

• Yoruba.instReprFocused.repr Yoruba.Focused.subject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yoruba.Focused.subject")).group prec✝
• Yoruba.instReprFocused.repr Yoruba.Focused.object prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yoruba.Focused.object")).group prec✝
• Yoruba.instReprFocused.repr Yoruba.Focused.adjunct prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yoruba.Focused.adjunct")).group prec✝

@[instance_reducible]

instance Yoruba.instFintypeFocused : Fintype Focused

Equations

• Yoruba.instFintypeFocused = { elems := { val := ↑Yoruba.Focused.enumList, nodup := Yoruba.Focused.enumList_nodup }, complete := Yoruba.instFintypeFocused._proof_1 }

@[instance_reducible]

instance Yoruba.instPartialOrderFocused : PartialOrder Focused

Distinct focusable constituents contain neither one the other, so the reflex hosts WithTop Focused are the focusable constituents with the clause containing all of them.

Equations

• Yoruba.instPartialOrderFocused = { le := fun (x1 x2 : Yoruba.Focused) => x1 = x2, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := Yoruba.instPartialOrderFocused._proof_1, le_antisymm := ⋯ }

@[instance_reducible]

instance Yoruba.instDecidableLEFocused : DecidableLE Focused

Equations

• Yoruba.instDecidableLEFocused a b = Yoruba.instDecidableEqFocused a b

@[instance_reducible]

instance Yoruba.instDecidableLTFocused : DecidableLT Focused

Equations

• Yoruba.instDecidableLTFocused a b = { decide := decide (a = b) && decide ¬b = a, reflects_decide := ⋯ }

def Yoruba.Focused.relativePosition : Focused → Option Relativization.Position

The relativizable position a focused constituent occupies.

Equations

• Yoruba.Focused.subject.relativePosition = some Relativization.Position.subject
• Yoruba.Focused.object.relativePosition = some Relativization.Position.directObject
• Yoruba.Focused.adjunct.relativePosition = none

def Yoruba.Focused.npRel : Focused → Relativization.NPRel

A fronted subject leaves the high-tone ó in its position; a fronted object or adjunct leaves it empty.

Equations

• Yoruba.Focused.subject.npRel = Relativization.NPRel.resumptive
• Yoruba.Focused.object.npRel = Relativization.NPRel.gap
• Yoruba.Focused.adjunct.npRel = Relativization.NPRel.gap

def Yoruba.particleHost (p : Particle) (f : Focused) : WithTop Focused

A clause-final particle is hosted by the clause, any other particle by the fronted constituent it accompanies.

Equations

• Yoruba.particleHost p f = if p.position = some Particle.Position.clauseFinal then ⊤ else ↑f

Configurations and their reflexes

structure Yoruba.FocusConfig : Type

A focus configuration pairs a dialect and a focused constituent with whether it stays in place or fronts.

• dialect : Dialect
• focused : Focused
• strategy : Focus.Strategy

@[instance_reducible]

instance Yoruba.instDecidableEqFocusConfig : DecidableEq FocusConfig

Equations

• Yoruba.instDecidableEqFocusConfig = Yoruba.instDecidableEqFocusConfig.decEq

def Yoruba.instDecidableEqFocusConfig.decEq (x✝ x✝¹ : FocusConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Yoruba.instReprFocusConfig : Repr FocusConfig

Equations

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

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

Equations

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

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

A focused subject fronts; in place it is no answer to who bought a shoe?.

Equations

• c.Licensed = (c.focused = Yoruba.Focused.subject → c.strategy = Focus.Strategy.exSitu)

@[instance_reducible]

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

Equations

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

def Yoruba.FocusConfig.reflexes (c : FocusConfig) : Finset (Reflex (WithTop Focused))

The overt reflexes of a configuration. In place there are none; fronted, they are the displaced constituent, the dialect's particle at its host, and ó in a vacated subject position.

Equations

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

theorem Yoruba.reflexes_inSitu (d : Dialect) (f : Focused) : { dialect := d, focused := f, strategy := Focus.Strategy.inSitu }.reflexes = ∅

In place, a focus has no reflex in any channel, so Adé ra bàtà answers what did Adé buy? with neither particle nor prominence.

theorem Yoruba.not_licensed_inSitu_subject (d : Dialect) : ¬{ dialect := d, focused := Focused.subject, strategy := Focus.Strategy.inSitu }.Licensed

A subject in place is not focused, so Adé rà bàtà does not answer who bought a shoe?.

theorem Yoruba.reflexes_standard_subject : { dialect := Dialect.standard, focused := Focused.subject, strategy := Focus.Strategy.exSitu }.reflexes = {Reflex.displacement ↑Focused.subject, Reflex.morpheme ↑Focused.subject [Morphology.Morph.free ni.form], Reflex.morpheme ↑Focused.subject [o]}

In Adé ni ó rà bàtà 'ADÉ bought a shoe' the subject fronts, ni follows it and ó fills its position.

theorem Yoruba.reflexes_ikale_subject : { dialect := Dialect.ikale, focused := Focused.subject, strategy := Focus.Strategy.exSitu }.reflexes = {Reflex.displacement ↑Focused.subject, Reflex.morpheme ⊤ [Morphology.Morph.free rin.form], Reflex.morpheme ↑Focused.subject [o]}

In Adé ó jẹ ejíjẹ nẹ̀ rín 'ADÉ ate the food' the subject fronts, ó fills its position and rín closes the clause.

theorem Yoruba.reflexes_ikale_object : { dialect := Dialect.ikale, focused := Focused.object, strategy := Focus.Strategy.exSitu }.reflexes = {Reflex.displacement ↑Focused.object, Reflex.morpheme ⊤ [Morphology.Morph.free rin.form]}

In Tolú Adé rí rín 'Adé saw TOLÚ' the fronted object leaves its position empty.

theorem Yoruba.refutes_perceptibility : ¬∀ (c : FocusConfig), c.Licensed → c.reflexes.Nonempty

Yorùbá joins Tangale and Hausa against the claim that every focus receives an overt reflex: object focus in place, licensed, has none.

Where the particle sits

theorem Yoruba.piedPipes_iff (c : FocusConfig) : Reflex.PiedPipes c.reflexes ↑c.focused ↔ c.strategy = Focus.Strategy.exSitu ∧ c.dialect.focusParticle.position = some Particle.Position.clauseFinal

The particle is hosted by a constituent properly containing the focus exactly when the focus is fronted and the dialect's particle is clause-final: Ìkálẹ̀ marks focus in the pied-piping configuration, the standard dialect on the focus itself.

theorem Yoruba.ikale_piedPipes (f : Focused) : Reflex.PiedPipes { dialect := Dialect.ikale, focused := f, strategy := Focus.Strategy.exSitu }.reflexes ↑f

Whatever Ìkálẹ̀ fronts, rín is hosted by the clause above it.

theorem Yoruba.standard_exactlyTargets (f : Focused) : Reflex.ExactlyTargets { dialect := Dialect.standard, focused := f, strategy := Focus.Strategy.exSitu }.reflexes ↑f

Every reflex of a standard-dialect focus sits on the fronted constituent itself.

theorem Yoruba.npRel_eq_relative (f : Focused) (p : Relativization.Position) : f.relativePosition = some p → relTi.realize p = {f.npRel}

A fronted focus vacates its position as relativization does, the subject resumed by ó and the object left empty under both constructions.