Sande, Clem and Dąbkowski (2026): Discontinuous vowel harmony in Guébie: Cyclic interleaving of syntax and phonology

This file formalizes Sande, Clem and Dąbkowski's account of discontinuous harmony. In Guébie verb focus the particle of a particle verb fronts, yet it agrees in [ATR] with the clause-final verb across the subject, the auxiliary and the object. The paper derives this from local harmony followed by movement. The vP is spelled out when C merges, and it then holds the particle and, exactly when an auxiliary keeps the verb from raising to T, the verb; harmony applies there, and the particle keeps its value when the remnant VP that contains it fronts, as in Koopman's analysis of predicate clefts.

Both Spell-outs are computed from the two parameters of the analysis, whether T holds an auxiliary and whether the remnant VP fronts, and each clause's Minimalist derivation spells out the same two snapshots. Harmony then coincides with the verb's position in v, and under Fox and Pesetsky's cyclic linearization, which the paper adopts, nothing that ends up between the fronted particle and the verb shares in it. The Wolof relative clauses described by Sy and by Martinović show the same profile, the trigger moving instead of the target.

Main statements

• SandeClemDabkowski2026.Clause.harmony_iff_hasAux: harmony applies exactly when an auxiliary keeps the verb in v (44).
• SandeClemDabkowski2026.Clause.notMem_vP_of_between: what stands between the particle and the verb on the surface was not spelled out with them (41).
• SandeClemDabkowski2026.Clause.spellouts_eq_phases: the derivations spell out the vP and CP snapshots.
• SandeClemDabkowski2026.Clause.vPTableau_optimal: the vP tableau gives the particle the value harmony assigns.

Implementation notes

• The vP Spell-out is the vP's head and complement, the stage before the subject merges; the object shifts to the edge of the whole vP, standing for the VP-external position of footnote 7. The rows omit the tone numerals.
• The tableau ranks Sande's two constraints, ATRHARM being Agreement by Projection in Hansson's sense, and holds the root fixed as root control requires; with the root free the two constraints alone would change the root (optimal_rootFree).
• The verb adjoins to the head-final v by Internal Merge on the right, which merges it with the whole vP rather than forming a complex head.

TODO

• The verb-doubling orders of plain verb focus, the island and successive-cyclicity diagnostics of §3, and the Atchan nasal harmony the paper leaves open.

References

• [SCD26]
• [Koo97]
• [FP05]
• [San19]
• [Han14]
• [Sy05]
• [Mar19]

Predicate fronting and its two Spell-outs

inductive SandeClemDabkowski2026.Terminal : Type

A terminal is an overt word of a particle-verb clause.

• particle : Terminal
• subject : Terminal
• aux : Terminal
• verb : Terminal
• object : Terminal

@[instance_reducible]

instance SandeClemDabkowski2026.instDecidableEqTerminal : DecidableEq Terminal

Equations

• SandeClemDabkowski2026.instDecidableEqTerminal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SandeClemDabkowski2026.instReprTerminal : Repr Terminal

Equations

• SandeClemDabkowski2026.instReprTerminal = { reprPrec := SandeClemDabkowski2026.instReprTerminal.repr }

def SandeClemDabkowski2026.instReprTerminal.repr : Terminal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SandeClemDabkowski2026.instFintypeTerminal : Fintype Terminal

Equations

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

structure SandeClemDabkowski2026.Clause : Type

A clause is fixed by the two parameters of predicate fronting, whether an auxiliary in T stops the verb in v and whether focus fronts the remnant VP to Spec,CP.

• hasAux : Bool
• fronted : Bool

@[instance_reducible]

instance SandeClemDabkowski2026.instDecidableEqClause : DecidableEq Clause

Equations

• SandeClemDabkowski2026.instDecidableEqClause = SandeClemDabkowski2026.instDecidableEqClause.decEq

def SandeClemDabkowski2026.instDecidableEqClause.decEq (x✝ x✝¹ : Clause) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance SandeClemDabkowski2026.instReprClause : Repr Clause

Equations

• SandeClemDabkowski2026.instReprClause = { reprPrec := SandeClemDabkowski2026.instReprClause.repr }

def SandeClemDabkowski2026.instReprClause.repr : Clause → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SandeClemDabkowski2026.instFintypeClause : Fintype Clause

Equations

• SandeClemDabkowski2026.instFintypeClause = Fintype.ofEquiv ((_ : Bool) × Bool) SandeClemDabkowski2026.Clause.proxyTypeEquiv

def SandeClemDabkowski2026.remnantVP : List Terminal

The remnant VP holds only the particle, the object having shifted out and the verb having raised to v.

Equations

• SandeClemDabkowski2026.remnantVP = [SandeClemDabkowski2026.Terminal.particle]

def SandeClemDabkowski2026.Clause.verbInV (c : Clause) : List Terminal

The verb sits head-finally in v when an auxiliary in T stops it there.

Equations

• c.verbInV = if c.hasAux = true then [SandeClemDabkowski2026.Terminal.verb] else []

def SandeClemDabkowski2026.Clause.vP (c : Clause) : List Terminal

The vP Spell-out (45), (48) holds the phase head v and its complement when C merges.

Equations

• c.vP = SandeClemDabkowski2026.remnantVP ++ c.verbInV

def SandeClemDabkowski2026.Clause.middle (c : Clause) : List Terminal

The subject in Spec,TP precedes the auxiliary or raised verb in T and the shifted object.

Equations

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

def SandeClemDabkowski2026.Clause.cP (c : Clause) : List Terminal

In the CP Spell-out the remnant VP stays between the object and v, or fronts to Spec,CP.

Equations

• c.cP = if c.fronted = true then SandeClemDabkowski2026.remnantVP ++ c.middle ++ c.verbInV else c.middle ++ SandeClemDabkowski2026.remnantVP ++ c.verbInV

def SandeClemDabkowski2026.Clause.phases (c : Clause) : List (List Terminal)

A clause is spelled out at vP and at CP.

Equations

• c.phases = [c.vP, c.cP]

theorem SandeClemDabkowski2026.Clause.vP_sublist_cP (c : Clause) : c.vP.Sublist c.cP

theorem SandeClemDabkowski2026.Clause.cP_nodup (c : Clause) : c.cP.Nodup

theorem SandeClemDabkowski2026.Clause.consistent (c : Clause) : Minimalist.Linearization.Consistent c.phases

Every clause linearizes, since the particle is the left edge of the vP Spell-out and its fronting reverses no ordering statement (§6.2).

def SandeClemDabkowski2026.Clause.Harmony (c : Clause) : Prop

Harmony applies when the verb is spelled out with the particle (§6.1).

Equations

• c.Harmony = (SandeClemDabkowski2026.Terminal.verb ∈ c.vP)

@[instance_reducible]

instance SandeClemDabkowski2026.Clause.instDecidableHarmony (c : Clause) : Decidable c.Harmony

Equations

• c.instDecidableHarmony = { decide := decide (List.elem SandeClemDabkowski2026.Terminal.verb c.vP = true), reflects_decide := ⋯ }

theorem SandeClemDabkowski2026.Clause.harmony_iff_hasAux (c : Clause) : c.Harmony ↔ c.hasAux = true

Harmony applies exactly when an auxiliary keeps the verb in v, fronted or not (44).

theorem SandeClemDabkowski2026.Clause.isInfix_vP (c : Clause) (h : c.Harmony) : [Terminal.particle, Terminal.verb] <:+: c.vP

Under harmony the particle and the verb are adjacent in the vP Spell-out.

theorem SandeClemDabkowski2026.Clause.notMem_vP_of_between (c : Clause) (h : c.Harmony) {x : Terminal} (h₁ : [Terminal.particle, x].Sublist c.cP) (h₂ : [x, Terminal.verb].Sublist c.cP) : x ∉ c.vP

What stands between the particle and the verb on the surface was not spelled out with them, so the harmony of the vP does not reach it (41).

Discontinuous harmony (§7)

structure SandeClemDabkowski2026.Discontinuous {α : Type u_1} (phases : List (List α)) (a b : α) : Prop

Harmony is discontinuous when its trigger and target are adjacent at one Spell-out and separated at another, in a derivation that linearizes.

• consistent : Minimalist.Linearization.Consistent phases
• adjacent : ∃ p ∈ phases, [a, b] <:+: p
• separated : ∃ q ∈ phases, ∃ (x : α), [a, x].Sublist q ∧ [x, b].Sublist q

theorem SandeClemDabkowski2026.Discontinuous.exists_notMem {α : Type u_1} {phases : List (List α)} {a b : α} (h : Discontinuous phases a b) : ∃ p ∈ phases, [a, b] <:+: p ∧ ∃ q ∈ phases, ∃ x ∈ q, x ∉ p

Under discontinuous harmony some Spell-out puts between the two terminals material that the Spell-out where they were adjacent did not hold, so they did not stay together (§7).

theorem SandeClemDabkowski2026.discontinuous_partSAuxOV : Discontinuous { hasAux := true, fronted := true }.phases Terminal.particle Terminal.verb

The fronted clause with an auxiliary is discontinuous harmony, the target moving.

Harmony within the vP Spell-out

def SandeClemDabkowski2026.atrPattern : Phonology.Harmony.Pattern Phonology.Segment Bool

Every vowel takes part in [ATR] harmony (§5.1).

Equations

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

def SandeClemDabkowski2026.atrHarm : OptimalityTheory.Constraint (List Phonology.Segment)

ATRHARM (47) is an Agreement by Projection constraint, violated once by an output in which a vowel precedes a vowel of the other [ATR] value on the tier of vowels.

Equations

• SandeClemDabkowski2026.atrHarm = OptimalityTheory.Constraint.binary fun (out : List Phonology.Segment) => ¬SandeClemDabkowski2026.atrPattern.Harmonic out

def SandeClemDabkowski2026.identIO (input : List Phonology.Segment) : OptimalityTheory.Constraint (List Phonology.Segment)

IDENT-IO(ATR) (46) is violated once by each vowel whose [ATR] value departs from its input.

Equations

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

def SandeClemDabkowski2026.revaluations (l : List Phonology.Segment) : List (List Phonology.Segment)

A revaluation of a string of vowels gives each vowel either [ATR] value.

Equations

• SandeClemDabkowski2026.revaluations l = (List.map (fun (v : Phonology.Segment) => [Guebie.withATR v true, Guebie.withATR v false]) l).sections

theorem SandeClemDabkowski2026.revaluations_ne_nil (l : List Phonology.Segment) : revaluations l ≠ []

def SandeClemDabkowski2026.vPTableau (part : Guebie.Morpheme) (root : List Phonology.Segment) : OptimalityTheory.Tableau (List Phonology.Segment) 2

The vP tableau ranks ATRHARM above IDENT-IO(ATR) over every revaluation of the particle, followed by the root vowels the vP Spell-out holds.

Equations

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

theorem SandeClemDabkowski2026.vPTableau_optimal (pv : Guebie.ParticleVerb) : pv ∈ Guebie.particleVerbs → (vPTableau pv.particle pv.verb.vowels).optimal = {List.map (fun (x : Phonology.Segment) => Guebie.withATR x pv.verb.atr) pv.particle.vowels ++ pv.verb.vowels} ∧ (vPTableau pv.particle []).optimal = {pv.particle.vowels}

Over the particle verbs of (10)–(12), the vP tableau's unique winner gives the particle the root's value when the root is in the vP Spell-out, and keeps it faithful when it is not.

def SandeClemDabkowski2026.Clause.rootVowels (c : Clause) (verb : Guebie.Morpheme) : List Phonology.Segment

The vP Spell-out holds the verb's vowels under harmony and no root vowels otherwise.

Equations

• c.rootVowels verb = if c.Harmony then verb.vowels else []

def SandeClemDabkowski2026.Clause.particleATR (c : Clause) (part verb : Guebie.Morpheme) : Bool

The particle surfaces with the root's [ATR] value under harmony and with its own otherwise ((12), (13)).

Equations

• c.particleATR part verb = if c.Harmony then verb.atr else part.atr

theorem SandeClemDabkowski2026.Clause.vPTableau_optimal (c : Clause) {pv : Guebie.ParticleVerb} (hpv : pv ∈ Guebie.particleVerbs) : (vPTableau pv.particle (c.rootVowels pv.verb)).optimal = {List.map (fun (x : Phonology.Segment) => Guebie.withATR x (c.particleATR pv.particle pv.verb)) pv.particle.vowels ++ c.rootVowels pv.verb}

In every clause the vP tableau gives each particle vowel the value harmony assigns.

def SandeClemDabkowski2026.rootFreeTableau (input : List Phonology.Segment) : OptimalityTheory.Tableau (List Phonology.Segment) 2

This tableau ranks ATRHARM above IDENT-IO(ATR) over every revaluation of an input, the root's vowels included.

Equations

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

theorem SandeClemDabkowski2026.optimal_rootFree : (rootFreeTableau (Guebie.jOkU.vowels ++ Guebie.ni.vowels)).optimal = {[Guebie.openO, Guebie.upsilon, Guebie.smallCapitalI]} ∧ (rootFreeTableau (Guebie.mE.vowels ++ Guebie.nu.vowels)).optimal = {[Guebie.e, Guebie.u], [Guebie.epsilon, Guebie.upsilon]}

With the root free, the two constraints alone repair /jɔkʊ-ni/ at the root, against (12a), since one changed vowel beats two, and they leave /mɛ-nu/ undecided, against (10e).

The derivations

def SandeClemDabkowski2026.Terminal.token : Terminal → Minimalist.LexicalItem.Token

Each terminal spells out its own lexical item.

Equations

• SandeClemDabkowski2026.Terminal.particle.token = { item := Minimalist.LexicalItem.of Minimalist.Cat.P [], id := 1 }
• SandeClemDabkowski2026.Terminal.subject.token = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [], id := 2 }
• SandeClemDabkowski2026.Terminal.aux.token = { item := Minimalist.LexicalItem.of Minimalist.Cat.T [], id := 3 }
• SandeClemDabkowski2026.Terminal.verb.token = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [], id := 4 }
• SandeClemDabkowski2026.Terminal.object.token = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [], id := 5 }

def SandeClemDabkowski2026.Terminal.ofToken? (tok : Minimalist.LexicalItem.Token) : Option Terminal

A lexical item spells out at most one terminal.

Equations

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

def SandeClemDabkowski2026.v₀ : Minimalist.LexicalItem.Token

The light verb v is silent.

Equations

• SandeClemDabkowski2026.v₀ = { item := Minimalist.LexicalItem.of Minimalist.Cat.v [], id := 6 }

def SandeClemDabkowski2026.T₀ : Minimalist.LexicalItem.Token

The T a raised verb adjoins to is silent.

Equations

• SandeClemDabkowski2026.T₀ = { item := Minimalist.LexicalItem.of Minimalist.Cat.T [], id := 7 }

def SandeClemDabkowski2026.C₀ : Minimalist.LexicalItem.Token

The complementizer C is silent.

Equations

• SandeClemDabkowski2026.C₀ = { item := Minimalist.LexicalItem.of Minimalist.Cat.C [], id := 8 }

def SandeClemDabkowski2026.remnant : Minimalist.PlanarSyntacticObject

The remnant VP that fronts holds the particle between the traces of the object and the verb.

Equations

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

def SandeClemDabkowski2026.vSteps : List Minimalist.Step

The head and complement of the vP are built as in (31)–(34). The particle and the object merge with the verb in a head-final VP, v merges on its right, and the verb adjoins to v on the right.

Equations

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

def SandeClemDabkowski2026.edgeSteps : List Minimalist.Step

The subject merges in Spec,vP and the object shifts above the vP.

Equations

• SandeClemDabkowski2026.edgeSteps = [Minimalist.Step.em Edge.left ↑SandeClemDabkowski2026.Terminal.subject.token, Minimalist.Step.im ↑SandeClemDabkowski2026.Terminal.object.token]

def SandeClemDabkowski2026.cSteps : List Minimalist.Step

The subject raises to Spec,TP and C merges.

Equations

• SandeClemDabkowski2026.cSteps = [Minimalist.Step.im ↑SandeClemDabkowski2026.Terminal.subject.token, Minimalist.Step.em Edge.left ↑SandeClemDabkowski2026.C₀]

def SandeClemDabkowski2026.vPSchedule (d : Minimalist.Derivation) : List (ℕ × ℕ)

A clause is spelled out twice: the head and complement of its vP when C merges (l.1255–1260), and its CP at the end of the derivation.

Equations

• SandeClemDabkowski2026.vPSchedule d = [(SandeClemDabkowski2026.vSteps.length, (d.mergeStage? ↑SandeClemDabkowski2026.C₀).getD d.length), (d.length, d.length)]

def SandeClemDabkowski2026.Clause.tSteps (c : Clause) : List Minimalist.Step

Either the auxiliary merges in T, or T merges and the verb raises to it.

Equations

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

def SandeClemDabkowski2026.Clause.focusSteps (c : Clause) : List Minimalist.Step

Focus fronts the remnant VP to Spec,CP.

Equations

• c.focusSteps = if c.fronted = true then [Minimalist.Step.im ↑SandeClemDabkowski2026.remnant] else []

def SandeClemDabkowski2026.Clause.derivation (c : Clause) : Minimalist.Derivation

A clause's derivation starts from the verb.

Equations

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

theorem SandeClemDabkowski2026.Clause.spellouts_eq_phases (c : Clause) : List.map (fun (p : ℕ × ℕ) => List.filterMap Terminal.ofToken? (c.derivation.spellout p.1 p.2)) (vPSchedule c.derivation) = c.phases

The derivation's Spell-outs are the vP and CP snapshots.

theorem SandeClemDabkowski2026.Clause.linearizes (c : Clause) : c.derivation.Linearizes (vPSchedule c.derivation)

Every clause's derivation linearizes.

theorem SandeClemDabkowski2026.Clause.isRemnantStep_derivation (c : Clause) (h : c.fronted = true) : c.derivation.IsRemnantStep (c.derivation.length - 1)

Focus fronting is remnant movement, the fronted VP holding the trace of the verb (§4.1).

def SandeClemDabkowski2026.lateShift : Minimalist.Derivation

In this variant of the fronted clause with an auxiliary, the object shifts only after C merges.

Equations

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

theorem SandeClemDabkowski2026.not_linearizes_lateShift : ¬lateShift.Linearizes (vPSchedule lateShift)

Object shift lets the particle front (§6.2). If the object shifted only after C merged, the vP would be spelled out with the object before the particle, and fronting the particle past it would not linearize.

The Guébie examples

def SandeClemDabkowski2026.rowsIn (lang : String) : List Datum

rowsIn lang lists the rows in the language lang.

Equations

• SandeClemDabkowski2026.rowsIn lang = List.filter (fun (x : Datum) => x.language == lang) SandeClemDabkowski2026.Examples.all

def SandeClemDabkowski2026.patterns : List (String × List Terminal)

Equations

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

def SandeClemDabkowski2026.verbs : List (String × Guebie.Morpheme)

Equations

• SandeClemDabkowski2026.verbs = [("ni", Guebie.ni), ("ngwOsa", Guebie.ngwOsa)]

def SandeClemDabkowski2026.atrs : List (String × Bool)

Equations

• SandeClemDabkowski2026.atrs = [("plus", true), ("minus", false)]

theorem SandeClemDabkowski2026.order_rows (x : Datum) : x ∈ rowsIn "gabo1234" → ∀ p ∈ x.parse? "pattern" patterns, x.judgment = Judgment.acceptable ↔ ∃ (c : Clause), c.cP = p

A Guébie row's word order is acceptable exactly when some clause spells it out.

theorem SandeClemDabkowski2026.harmony_rows (x : Datum) : x ∈ rowsIn "gabo1234" → ∀ p ∈ x.parse? "pattern" patterns, ∀ v ∈ x.parse? "verb" verbs, ∀ (c : Clause), c.cP = p → (∀ a ∈ x.parse? "particleATR" atrs, a = c.particleATR Guebie.jOkU v) ∧ ∀ i ∈ x.parse? "interveningATR" atrs, i ≠ c.particleATR Guebie.jOkU v

In every Guébie row the particle /jɔkʊ/ bears the value of the clause that spells out the row's order, and the material the row records between the particle and the verb does not.

Wolof relative clauses (§7)

inductive SandeClemDabkowski2026.Nominal : Type

A nominal is an overt word of a Wolof noun phrase.

• noun : Nominal
• rel : Nominal
• stative : Nominal
• dem : Nominal

@[instance_reducible]

instance SandeClemDabkowski2026.instDecidableEqNominal : DecidableEq Nominal

Equations

• SandeClemDabkowski2026.instDecidableEqNominal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SandeClemDabkowski2026.instReprNominal.repr : Nominal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SandeClemDabkowski2026.instReprNominal : Repr Nominal

Equations

• SandeClemDabkowski2026.instReprNominal = { reprPrec := SandeClemDabkowski2026.instReprNominal.repr }

def SandeClemDabkowski2026.dP : List Nominal

The DP Spell-out (49) holds the head noun and its distal demonstrative.

Equations

• SandeClemDabkowski2026.dP = [SandeClemDabkowski2026.Nominal.noun, SandeClemDabkowski2026.Nominal.dem]

def SandeClemDabkowski2026.relClause : List Nominal

A relative clause (50) has the head noun at its left edge, then the relativizer, the stative verb and the demonstrative.

Equations

• SandeClemDabkowski2026.relClause = [SandeClemDabkowski2026.Nominal.noun, SandeClemDabkowski2026.Nominal.rel, SandeClemDabkowski2026.Nominal.stative, SandeClemDabkowski2026.Nominal.dem]

def SandeClemDabkowski2026.shapes : List (String × List Nominal)

Equations

• SandeClemDabkowski2026.shapes = [("localDP", SandeClemDabkowski2026.dP), ("relClause", SandeClemDabkowski2026.relClause)]

theorem SandeClemDabkowski2026.discontinuous_relClause : Discontinuous [dP, relClause] Nominal.noun Nominal.dem

The relative clause is discontinuous harmony, the trigger moving.

theorem SandeClemDabkowski2026.wolof_rows (x : Datum) : x ∈ rowsIn "nucl1347" → (∀ s ∈ x.parse? "shape" shapes, Minimalist.Linearization.Consistent [dP, s]) ∧ ∀ h ∈ x.parse? "headATR" atrs, ∀ d ∈ x.parse? "demATR" atrs, d = h

Every Wolof row's shape linearizes with the DP Spell-out, and its demonstrative bears the head noun's value whatever the stative verb between them bears.