Tonal constraints

OT/HS constraint constructors over the FloatingForm S TRN autosegmental representation (Phonology/Autosegmental/Floating.lean), generic over the segment type S. Each is a canonical Constraints.Constraint — a scalar · → ℕ violation count. Equation numbers below are [McPL26]'s.

Main definitions

• starFloatBlock / starFloatBlockRev / starFloatCount — *FLOAT (eq. 16): directional block (L→R / R→L) vs. count variant
• starTautDock — *TAUTDOCK (eq. 15, after [Wol07])
• starCrowd — *CROWD (eq. 5): per-morpheme tone-count ceiling
• starFall — *FALL (eq. 23): falling-contour ban
• starMlessL — *M<L (eq. 29): M immediately before L on the tier
• maxTone / depLinkTone / maxLinkTone — MAX(T) / DEP(link)/T / MAX(link)/T (eq. 7)
• haveTone — HAVETONE (eq. 17)
• integrityTone — INTEGRITY ([AF26]; [McCP95])

Implementation notes

Faithfulness (maxTone, maxLinkTone, depLinkTone) compares surface state to the immutable underlying state stored in FloatingForm. Without that underlying-form tracking, faithfulness can't fire and the [McPL26] LR-vs-RL multi-step asymmetry collapses.

Directionality is not a separate kind of constraint. Following [Lam22d] (directionality is a property of EVAL), *FLOAT is a position-indexed block of scalar float-flag constraints (starFloatBlock): coordinate i is floatIndicator's i-th entry, so splicing the block into a ranking and comparing under the canonical lexicographic profile order recovers the directional EVAL exactly (Core.Optimization.Evaluation.lexLE_ofFn). The block is laid out left-to-right for *FLOAT^→ (starFloatBlock) or right-to-left for *FLOAT^← (starFloatBlockRev); starFloatCount is the count collapse (parallel *FLOAT). They agree on at most one floating tone but diverge as the set grows — a single count cannot tell "delete leftmost" from "delete rightmost" ([McPL26]'s eq. (62) divergent tie).

Tone-value predicate

Link faithfulness (FloatingForm.IsInsertedLink / IsDeletedLink) and the morpheme accessors (upperMorpheme? / lowerMorpheme? / morphemes) are tone-agnostic and live on FloatingForm; only the TRN-reading predicate is here.

@[reducible, inline]

abbrev Tone.ToneHasValue {S : Type u_1} (f : Autosegmental.FloatingForm S TRN) (k : Autosegmental.TierIdx) (t : TRN) : Prop

The tone at index k has value t.

Equations

• Tone.ToneHasValue f k t = (Option.map Autosegmental.TierSpec.value (f.upper.get? k) = some t)

*FLOAT (Directional)

def Tone.starFloatBlock {S : Type u_1} (k : ℕ) : List (Constraints.Constraint (Autosegmental.FloatingForm S TRN))

*FLOAT (paper, eq. 16) as a position-indexed block of scalar constraints: coordinate i flags whether underlying tone i is currently floating (= the i-th entry of floatIndicator). Splice forward for L→R (*FLOAT^→); the directional EVAL is recovered as the canonical lex order over this block ([Lam22d]). k is the underlying tone count f.upper.len, invariant under GEN, so it is a fixed literal per tableau.

Equations

• Tone.starFloatBlock k = List.map (fun (i : Autosegmental.TierIdx) (g : Autosegmental.FloatingForm S Tone.TRN) => if g.IsFloating i then 1 else 0) (List.range k)

def Tone.starFloatBlockRev {S : Type u_1} (k : ℕ) : List (Constraints.Constraint (Autosegmental.FloatingForm S TRN))

*FLOAT^← (right-to-left): starFloatBlock laid out in reverse position order.

Equations

• Tone.starFloatBlockRev k = (Tone.starFloatBlock k).reverse

def Tone.starFloatCount {S : Type u_1} : Constraints.Constraint (Autosegmental.FloatingForm S TRN)

*FLOAT (count): the parallel/count variant — the total floating-tone count as a single scalar constraint (the degree collapse of starFloatBlock).

Equations

• Tone.starFloatCount f = f.floatIndicator.sum

*TAUTDOCK

def Tone.starTautDock {S : Type u_1} : Constraints.Constraint (Autosegmental.FloatingForm S TRN)

*TAUTDOCK (paper, eq. 15, after [Wol07]): one violation per GEN-inserted tautomorphemic surface link.

Equations

• Tone.starTautDock f = {l ∈ f.surfaceLinks | f.IsInsertedLink l ∧ f.IsTautomorphemic l}.card

*CROWD (per-morpheme tone count)

def Tone.tonesForMorpheme {S : Type u_1} (f : Autosegmental.FloatingForm S TRN) (m : Morphology.WordStructure.Morpheme) : Finset Autosegmental.TierIdx

The tone indices counting toward morpheme m's tonal mass: surviving underlying tones of m, plus tones surface-linked to TBUs of m.

Equations

• Tone.tonesForMorpheme f m = {k ∈ Finset.range f.upper.len | f.IsAlive k ∧ f.upperMorpheme? k = some m} ∪ Finset.image Prod.fst ({l ∈ f.surfaceLinks | f.lowerMorpheme? l.2 = some m})

def Tone.starCrowd {S : Type u_1} (threshold : ℕ := 2) : Constraints.Constraint (Autosegmental.FloatingForm S TRN)

*CROWD (paper eq. 5): one violation per morpheme with more than threshold tones (default 2), counting its surviving underlying tones plus tones docked onto its TBUs from other morphemes.

Equations

• Tone.starCrowd threshold f = {m ∈ f.morphemes | threshold < (Tone.tonesForMorpheme f m).card}.card

*FALL (falling contours on multi-linked TBUs)

@[reducible, inline]

abbrev Tone.IsFallingPair (t1 t2 : TRN) : Prop

A tone pair (t1, t2) (in tier order) is falling iff it is HM, HL, or ML (paper eq. 23).

Equations

• Tone.IsFallingPair t1 t2 = (t1 = Tone.TRN.H ∧ t2 = Tone.TRN.M ∨ t1 = Tone.TRN.H ∧ t2 = Tone.TRN.L ∨ t1 = Tone.TRN.M ∧ t2 = Tone.TRN.L)

def Tone.HasFall : List TRN → Prop

A tone sequence contains a falling adjacent pair.

Equations

• Tone.HasFall [] = False
• Tone.HasFall [head] = False
• Tone.HasFall (t1 :: t2 :: rest) = (Tone.IsFallingPair t1 t2 ∨ Tone.HasFall (t2 :: rest))

@[implicit_reducible]

instance Tone.decidableHasFall (ts : List TRN) : Decidable (HasFall ts)

Equations

• Tone.decidableHasFall [] = isFalse not_false
• Tone.decidableHasFall [head] = isFalse not_false
• Tone.decidableHasFall (t1 :: t2 :: rest) = Tone.decidableHasFall._aux_1 t1 t2 rest (Tone.decidableHasFall (t2 :: rest))

def Tone.starFall {S : Type u_1} : Constraints.Constraint (Autosegmental.FloatingForm S TRN)

*FALL (paper eq. 23): one violation per syllable with a falling contour (HM, HL, ML).

Equations

• Tone.starFall f = f.countLower fun (i : Autosegmental.SegIdx) => Tone.HasFall (f.tierValues i)

*M<L (M-then-L adjacency on the tier)

def Tone.starMlessL {S : Type u_1} : Constraints.Constraint (Autosegmental.FloatingForm S TRN)

*M<L (paper eq. 29): one violation per M tone immediately preceding an L on the tonal tier — adjacency measured over the surviving (non-deleted) tones in ulTier order (deletions skip positions).

Equations

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

HAVETONE

def Tone.haveTone {S : Type u_1} : Constraints.Constraint (Autosegmental.FloatingForm S TRN)

HAVETONE (paper, eq. 17): one violation per syllable not associated to any tone.

Equations

• Tone.haveTone f = f.countLower fun (i : Autosegmental.SegIdx) => (f.linksTo i).isEmpty = true

Faithfulness — Generic over Tone Value

def Tone.maxTone {S : Type u_1} (t : TRN) : Constraints.Constraint (Autosegmental.FloatingForm S TRN)

MAX(T) (paper, eq. 7c): one violation per underlying tone of value t deleted by GEN.

Equations

• Tone.maxTone t f = f.countUpper fun (k : Autosegmental.TierIdx) => f.IsDeleted k ∧ Tone.ToneHasValue f k t

def Tone.depLinkTone {S : Type u_1} (t : TRN) : Constraints.Constraint (Autosegmental.FloatingForm S TRN)

DEP(link)/T (paper, eq. 7a): one violation per surface link inserted by GEN whose linked tone has value t.

Equations

• Tone.depLinkTone t f = {l ∈ f.surfaceLinks | f.IsInsertedLink l ∧ Tone.ToneHasValue f l.1 t}.card

def Tone.maxLinkTone {S : Type u_1} (t : TRN) : Constraints.Constraint (Autosegmental.FloatingForm S TRN)

MAX(link)/T (paper, eq. 7b): one violation per underlying link of value t deleted by GEN.

Equations

• Tone.maxLinkTone t f = {l ∈ f.links | f.IsDeletedLink l ∧ Tone.ToneHasValue f l.1 t}.card

def Tone.integrityTone {S : Type u_1} (m : Morphology.WordStructure.Morpheme) (t : TRN) : Constraints.Constraint (Autosegmental.FloatingForm S TRN)

INTEGRITY ([McCP95]; [AF26]): no input tone has multiple output correspondents — here, alive ulTier entries sharing tone value t and morpheme m. Spreading (one multi-linked entry) → 0; copying (n such entries) → n - 1 violations.

Equations

• Tone.integrityTone m t f = (f.countUpper fun (k : Autosegmental.TierIdx) => f.IsAlive k ∧ f.upperMorpheme? k = some m ∧ Tone.ToneHasValue f k t) - 1