Tonal constraints

OT and harmonic-serialism constraints over the candidates Candidate u of an autosegmental form u : Form S TRN M, generic over the segment type S and the opaque sponsor type M. Each is an OptimalityTheory.Constraint, a violation count. Equation numbers are McPherson and Lamont's.

Main definitions

• starFloatBlock / starFloatBlockRev / starFloatCount — *FLOAT (eq. 16): directional block (L→R / R→L) vs. count variant
• starTautDock — *TAUTDOCK (eq. 15)
• 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)

Implementation notes

• Faithfulness (maxTone, maxLinkTone, depLinkTone) compares a candidate's surface state with its form, which the candidate carries as a parameter; without it the left-to-right versus right-to-left asymmetry of multi-step derivations collapses.
• Directionality is a property of EVAL, not a kind of constraint: *FLOAT is a position-indexed block of float flags (starFloatBlock), and splicing the block into a ranking under the lexicographic profile order recovers directional evaluation (List.ofFn_le_ofFn_iff). starFloatCount is its count collapse, which agrees with the block on at most one floating tone and cannot tell deleting the leftmost from deleting the rightmost.

References

• [McPL26]
• [Lam22d]
• [Wol07]

Tone-value predicate

Link faithfulness (Candidate.insertedLinks / deletedLinks) and the morphemes (Form.morphemes, Form.lowerOfMorpheme) are tone-agnostic and live on the substrate; only the TRN-reading predicate is here.

@[reducible, inline]

abbrev Tone.ToneHasValue {S : Type u_1} {M : Type u_2} {u : Autosegmental.Form S TRN M} (k : Fin u.upper.length) (t : TRN) : Prop

The tone at index k has value t.

Equations

• Tone.ToneHasValue k t = (u.upper[k].value = t)

*FLOAT (Directional)

def Tone.starFloatBlock {S : Type u_1} {M : Type u_2} {u : Autosegmental.Form S TRN M} : List (OptimalityTheory.Constraint (Autosegmental.Candidate u))

*FLOAT (paper, eq. 16) is a position-indexed block of scalar constraints, whose coordinate i flags whether underlying tone i is currently floating. Spliced forward it is *FLOAT^→, and the directional EVAL is recovered as the canonical lex order over the block ([Lam22d]).

Equations

• Tone.starFloatBlock = List.map (fun (i : Fin u.upper.length) (c : Autosegmental.Candidate u) => if c.IsFloating i then 1 else 0) (List.finRange u.upper.length)

def Tone.starFloatBlockRev {S : Type u_1} {M : Type u_2} {u : Autosegmental.Form S TRN M} : List (OptimalityTheory.Constraint (Autosegmental.Candidate u))

*FLOAT^← is starFloatBlock laid out in reverse position order, for right-to-left evaluation.

Equations

• Tone.starFloatBlockRev = Tone.starFloatBlock.reverse

def Tone.starFloatCount {S : Type u_1} {M : Type u_2} {u : Autosegmental.Form S TRN M} : OptimalityTheory.Constraint (Autosegmental.Candidate u)

The count variant of *FLOAT totals the floating tones as a single scalar constraint, the degree collapse of starFloatBlock.

Equations

• Tone.starFloatCount c = (Finset.filter c.IsFloating Finset.univ).card

*TAUTDOCK

def Tone.starTautDock {S : Type u_1} {M : Type u_2} [DecidableEq M] {u : Autosegmental.Form S TRN M} : OptimalityTheory.Constraint (Autosegmental.Candidate u)

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

Equations

• Tone.starTautDock c = (Finset.filter u.IsTautomorphemic c.insertedLinks).card

*CROWD (per-morpheme tone count)

def Tone.tonesForMorpheme {S : Type u_1} {M : Type u_2} [DecidableEq M] {u : Autosegmental.Form S TRN M} (c : Autosegmental.Candidate u) (m : M) : Finset (Fin u.upper.length)

The tones counting toward morpheme m's tonal mass are its surviving underlying tones and the tones surface-linked to its TBUs.

Equations

• Tone.tonesForMorpheme c m = {k : Fin u.upper.length | k ∉ c.deleted ∧ u.upper[k].morpheme = m} ∪ Finset.image Prod.fst ({l ∈ c.links | u.lower[l.2].morpheme = m})

def Tone.starCrowd {S : Type u_1} {M : Type u_2} [DecidableEq M] {u : Autosegmental.Form S TRN M} (threshold : ℕ := 2) : OptimalityTheory.Constraint (Autosegmental.Candidate u)

*CROWD (paper eq. 5) assigns 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 c = {m ∈ u.morphemes | threshold < (Tone.tonesForMorpheme c 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))

@[instance_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) = { decide := decide (Tone.IsFallingPair t1 t2) || decide (Tone.HasFall (t2 :: rest)), reflects_decide := ⋯ }

def Tone.starFall {S : Type u_1} {M : Type u_2} {u : Autosegmental.Form S TRN M} : OptimalityTheory.Constraint (Autosegmental.Candidate u)

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

Equations

• Tone.starFall c = {i : Fin u.lower.length | Tone.HasFall (c.tierValues i)}.card

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

def Tone.starMlessL {S : Type u_1} {M : Type u_2} {u : Autosegmental.Form S TRN M} : OptimalityTheory.Constraint (Autosegmental.Candidate u)

*M<L (paper eq. 29) assigns one violation per M tone immediately preceding an L on the tonal tier, with adjacency measured over the surviving tones in tier order, so deletions skip positions.

Equations

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

HAVETONE

def Tone.haveTone {S : Type u_1} {M : Type u_2} {u : Autosegmental.Form S TRN M} : OptimalityTheory.Constraint (Autosegmental.Candidate u)

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

Equations

• Tone.haveTone c = {i : Fin u.lower.length | c.linksTo i = []}.card

Faithfulness — Generic over Tone Value

def Tone.maxTone {S : Type u_1} {M : Type u_2} {u : Autosegmental.Form S TRN M} (t : TRN) : OptimalityTheory.Constraint (Autosegmental.Candidate u)

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

Equations

• Tone.maxTone t c = {k ∈ c.deleted | Tone.ToneHasValue k t}.card

def Tone.depLinkTone {S : Type u_1} {M : Type u_2} {u : Autosegmental.Form S TRN M} (t : TRN) : OptimalityTheory.Constraint (Autosegmental.Candidate u)

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

Equations

• Tone.depLinkTone t c = {l ∈ c.insertedLinks | Tone.ToneHasValue l.1 t}.card

def Tone.maxLinkTone {S : Type u_1} {M : Type u_2} {u : Autosegmental.Form S TRN M} (t : TRN) : OptimalityTheory.Constraint (Autosegmental.Candidate u)

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

Equations

• Tone.maxLinkTone t c = {l ∈ c.deletedLinks | Tone.ToneHasValue l.1 t}.card