Floating Tones — Autosegmental Forms with Multi-Tone TBUs

@cite{goldsmith-1976} @cite{wolf-2007} @cite{mcpherson-lamont-2026}

Goldsmith-style autosegmental representation: tones live on a tier above the segmental backbone, connected by association lines (links). Multiple tones can associate to one TBU (forming contours); a tone with no associations is floating.

This refactor (over the prior overwrite-semantics encoding) is required by the @cite{mcpherson-lamont-2026} fig. 3 derivation: *CROWD penalises TBUs with too many associated tones, and *FALL penalises HM/HL/ML contours — both of which presuppose multi-tone-per-TBU representation.

Encoding

The form carries an immutable underlying state and a mutable surface state. GEN operations modify only the surface state.

Underlying (immutable):

• segs : List (SegSpec S) — segmental backbone with morpheme membership
• ulTones : List ToneSpec — tier elements with morpheme membership
• ulLinks : Finset Link — input association lines

Surface (mutable):

• deletedTones : Finset ToneIdx — set of GEN-deleted tone indices
• surfaceLinks : Finset Link — current association lines

A tone is floating iff it is not deleted AND no surface link references it.

Operations (paper, eq. 6 subset)

• deleteTone k — paper (6c): mark tone k deleted; cascades to remove any surface link referencing it
• insertLink k i — paper (6a): add link (k, i) to surfaceLinks
• deleteLink k i — paper (6b): remove link (k, i) from surfaceLinks

The paper's GEN also includes (6d) insert+associate a new tone and (6e) shift a tone (the latter credited to Gietz et al. 2023 in the paper); both omitted here as they don't appear in the fig. 3 derivation.

Tautomorphic vs heteromorphic links

A surface link (k, i) is tautomorphic iff ulTones[k].morpheme = segs[i].morpheme. The constraint *TAUTDOCK (paper, eq. 15, after @cite{wolf-2007}) penalises tautomorphic links inserted by GEN (i.e., in surfaceLinks but not in ulLinks).

@[reducible, inline]

abbrev Phonology.Autosegmental.ToneIdx : Type

Index into ulTones.

Equations

• Phonology.Autosegmental.ToneIdx = ℕ

@[reducible, inline]

abbrev Phonology.Autosegmental.SegIdx : Type

Index into segs.

Equations

• Phonology.Autosegmental.SegIdx = ℕ

def Phonology.Autosegmental.MorphemeId : Type

Identifier for a morpheme. Concrete IDs are fragment-specific. Opaque (def, not abbrev) so that arithmetic on Nat doesn't silently leak through — only the operations declared below (DecidableEq, Repr, OfNat literals) are exposed to consumers.

Equations

• Phonology.Autosegmental.MorphemeId = ℕ

@[implicit_reducible]

instance Phonology.Autosegmental.MorphemeId.instDecidableEq : DecidableEq MorphemeId

Equations

• Phonology.Autosegmental.MorphemeId.instDecidableEq = Phonology.Autosegmental.MorphemeId.instDecidableEq._aux_1

@[implicit_reducible]

instance Phonology.Autosegmental.MorphemeId.instRepr : Repr MorphemeId

Equations

• Phonology.Autosegmental.MorphemeId.instRepr = { reprPrec := Phonology.Autosegmental.MorphemeId.instRepr._aux_1 }

@[implicit_reducible]

instance Phonology.Autosegmental.MorphemeId.instToString : ToString MorphemeId

Equations

• Phonology.Autosegmental.MorphemeId.instToString = { toString := Phonology.Autosegmental.MorphemeId.instToString._aux_1 }

@[implicit_reducible]

instance Phonology.Autosegmental.MorphemeId.instOfNat (n : ℕ) : OfNat MorphemeId n

Equations

• Phonology.Autosegmental.MorphemeId.instOfNat n = { ofNat := Phonology.Autosegmental.MorphemeId.instOfNat._aux_1 n }

@[reducible, inline]

abbrev Phonology.Autosegmental.Link : Type

An autosegmental link: tone fst is associated to TBU snd.

Equations

• Phonology.Autosegmental.Link = (Phonology.Autosegmental.ToneIdx × Phonology.Autosegmental.SegIdx)

structure Phonology.Autosegmental.ToneSpec : Type

A tonal-tier element: tone value plus morpheme membership.

• tone : RegisterTier.TRN
• morpheme : MorphemeId

@[implicit_reducible]

instance Phonology.Autosegmental.instDecidableEqToneSpec : DecidableEq ToneSpec

Equations

• Phonology.Autosegmental.instDecidableEqToneSpec = Phonology.Autosegmental.instDecidableEqToneSpec.decEq

def Phonology.Autosegmental.instDecidableEqToneSpec.decEq (x✝ x✝¹ : ToneSpec) : Decidable (x✝ = x✝¹)

Equations

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

def Phonology.Autosegmental.instReprToneSpec.repr : ToneSpec → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.instReprToneSpec : Repr ToneSpec

Equations

• Phonology.Autosegmental.instReprToneSpec = { reprPrec := Phonology.Autosegmental.instReprToneSpec.repr }

structure Phonology.Autosegmental.SegSpec (S : Type) : Type

A segmental backbone element: segment plus morpheme membership. Generic over the segment type S.

• seg : S
• morpheme : MorphemeId

def Phonology.Autosegmental.instReprSegSpec.repr {S✝ : Type} [Repr S✝] : SegSpec S✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.instReprSegSpec {S✝ : Type} [Repr S✝] : Repr (SegSpec S✝)

Equations

• Phonology.Autosegmental.instReprSegSpec = { reprPrec := Phonology.Autosegmental.instReprSegSpec.repr }

@[implicit_reducible]

instance Phonology.Autosegmental.instDecidableEqSegSpec {S : Type} [DecidableEq S] : DecidableEq (SegSpec S)

Equations

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

structure Phonology.Autosegmental.FloatingForm (S : Type) : Type

An autosegmental tonal form. See module docstring for the underlying-vs-surface convention.

• segs : List (SegSpec S)

  Segmental backbone (tier order).

• ulTones : List ToneSpec

  UNDERLYING tonal tier (tier order; immutable).

• ulLinks : Finset Link

  UNDERLYING association lines (immutable).

• deletedTones : Finset ToneIdx

  SURFACE deletion set (current state).

• surfaceLinks : Finset Link

  SURFACE association lines (current state).

@[implicit_reducible]

instance Phonology.Autosegmental.instReprFloatingForm {S : Type} [Repr S] : Repr (FloatingForm S)

Repr drops Finset fields (mathlib's Finset.Repr is unsafe). Shows only segs and ulTones for debugging.

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.instDecidableEqFloatingForm {S : Type} [DecidableEq S] : DecidableEq (FloatingForm S)

Equations

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

def Phonology.Autosegmental.FloatingForm.mkInput {S : Type} (segs : List (SegSpec S)) (ulTones : List ToneSpec) (ulLinks : Finset Link) : FloatingForm S

Construct an input form: surface state mirrors underlying state, nothing deleted, all underlying links intact.

Equations

• Phonology.Autosegmental.FloatingForm.mkInput segs ulTones ulLinks = { segs := segs, ulTones := ulTones, ulLinks := ulLinks, deletedTones := ∅, surfaceLinks := ulLinks }

def Phonology.Autosegmental.FloatingForm.IsAlive {S : Type} (f : FloatingForm S) (k : ToneIdx) : Prop

The tone at index k is alive (not deleted). The structural primitive; IsDeleted is its negation.

Equations

• f.IsAlive k = (k ∉ f.deletedTones)

@[implicit_reducible]

instance Phonology.Autosegmental.FloatingForm.instDecidableIsAlive {S : Type} (f : FloatingForm S) (k : ToneIdx) : Decidable (f.IsAlive k)

Equations

• f.instDecidableIsAlive k = Phonology.Autosegmental.FloatingForm.instDecidableIsAlive._aux_1 f k

@[reducible, inline]

abbrev Phonology.Autosegmental.FloatingForm.IsDeleted {S : Type} (f : FloatingForm S) (k : ToneIdx) : Prop

The tone at index k is deleted. Sugar for ¬ IsAlive.

Equations

• f.IsDeleted k = ¬f.IsAlive k

def Phonology.Autosegmental.FloatingForm.IsLinked {S : Type} (f : FloatingForm S) (k : ToneIdx) : Prop

The tone at index k is linked to some TBU on the surface.

Equations

• f.IsLinked k = ∃ l ∈ f.surfaceLinks, l.1 = k

@[implicit_reducible]

instance Phonology.Autosegmental.FloatingForm.instDecidableIsLinked {S : Type} (f : FloatingForm S) (k : ToneIdx) : Decidable (f.IsLinked k)

Equations

• f.instDecidableIsLinked k = decidable_of_iff (∃ l ∈ f.surfaceLinks, l.1 = k) ⋯

def Phonology.Autosegmental.FloatingForm.IsFloating {S : Type} (f : FloatingForm S) (k : ToneIdx) : Prop

The tone at index k is floating (alive but unlinked).

Equations

• f.IsFloating k = (f.IsAlive k ∧ ¬f.IsLinked k)

@[implicit_reducible]

instance Phonology.Autosegmental.FloatingForm.instDecidableIsFloating {S : Type} (f : FloatingForm S) (k : ToneIdx) : Decidable (f.IsFloating k)

Equations

• f.instDecidableIsFloating k = Phonology.Autosegmental.FloatingForm.instDecidableIsFloating._aux_1 f k

def Phonology.Autosegmental.FloatingForm.IsTautomorphic {S : Type} (f : FloatingForm S) (l : Link) : Prop

A surface link (k, i) is tautomorphic iff its tone and TBU share a morpheme. Out-of-range indices on either side make this false. Used by *TAUTDOCK (paper, eq. 15) and the tautomorphic vs heteromorphic distinction discussed in the module docstring.

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.FloatingForm.instDecidableIsTautomorphic {S : Type} (f : FloatingForm S) (l : Link) : Decidable (f.IsTautomorphic l)

Equations

• f.instDecidableIsTautomorphic l = Phonology.Autosegmental.FloatingForm.instDecidableIsTautomorphic._aux_1 f l

def Phonology.Autosegmental.FloatingForm.deleteTone {S : Type} (f : FloatingForm S) (k : ToneIdx) : FloatingForm S

(6c) Delete the underlying tone at index k. Cascades to remove any surface link referencing it.

Equations

• f.deleteTone k = { segs := f.segs, ulTones := f.ulTones, ulLinks := f.ulLinks, deletedTones := insert k f.deletedTones, surfaceLinks := {l ∈ f.surfaceLinks | l.1 ≠ k} }

def Phonology.Autosegmental.FloatingForm.insertLink {S : Type} (f : FloatingForm S) (k : ToneIdx) (i : SegIdx) : FloatingForm S

(6a) Insert a surface link (k, i).

Equations

• f.insertLink k i = { segs := f.segs, ulTones := f.ulTones, ulLinks := f.ulLinks, deletedTones := f.deletedTones, surfaceLinks := insert (k, i) f.surfaceLinks }

def Phonology.Autosegmental.FloatingForm.deleteLink {S : Type} (f : FloatingForm S) (k : ToneIdx) (i : SegIdx) : FloatingForm S

(6b) Delete the surface link (k, i).

Equations

• f.deleteLink k i = { segs := f.segs, ulTones := f.ulTones, ulLinks := f.ulLinks, deletedTones := f.deletedTones, surfaceLinks := f.surfaceLinks.erase (k, i) }

def Phonology.Autosegmental.FloatingForm.Crosses {S : Type} (f : FloatingForm S) (k : ToneIdx) (i : SegIdx) : Prop

A candidate link (k, i) would cross an existing surface link (k', i') iff tier order disagrees with segmental order: (k < k' ∧ i > i') ∨ (k > k' ∧ i < i'). Crossing-association candidates violate the No-Crossing Constraint of @cite{goldsmith-1976} autosegmental phonology and are excluded from GEN.

Equations

• f.Crosses k i = ∃ l ∈ f.surfaceLinks, k < l.1 ∧ l.2 < i ∨ l.1 < k ∧ i < l.2

@[implicit_reducible]

instance Phonology.Autosegmental.FloatingForm.instDecidableCrosses {S : Type} (f : FloatingForm S) (k : ToneIdx) (i : SegIdx) : Decidable (f.Crosses k i)

Equations

• f.instDecidableCrosses k i = decidable_of_iff (∃ l ∈ f.surfaceLinks, k < l.1 ∧ l.2 < i ∨ l.1 < k ∧ i < l.2) ⋯

def Phonology.Autosegmental.FloatingForm.gen {S : Type} [DecidableEq S] (f : FloatingForm S) : Finset (FloatingForm S)

One-step GEN. Enumerates: (a) the faithful candidate, (b) deleting each alive tone, (c) for each FLOATING tone, inserting a link to each TBU that doesn't cross an existing link. Subset of paper eq. 6: omits (d) insert-and-associate and (e) shift, which fig. 3 doesn't use. The no-crossing filter (@cite{goldsmith-1976}) enforces autosegmental well-formedness — without it, a floating H could dock across an intervening linked tone, which the paper's GEN implicitly forbids.

Equations

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

def Phonology.Autosegmental.FloatingForm.floatIndicator {S : Type} (f : FloatingForm S) : List ℕ

Indicator vector for floating-tone presence at each underlying-tone position, in tier order. Entry k is 1 iff ulTones[k] is currently floating, else 0. Used by directional *FLOAT (paper, eq. 16).

Equations

• f.floatIndicator = List.map (fun (k : Phonology.Autosegmental.ToneIdx) => if f.IsFloating k then 1 else 0) (List.range f.ulTones.length)

def Phonology.Autosegmental.FloatingForm.linksTo {S : Type} (f : FloatingForm S) (i : SegIdx) : List ToneIdx

Surface tones linked to TBU i, returned in tier order (smallest tone index first). Used by *FALL and *CROWD. We iterate over List.range f.ulTones.length so the result is naturally sorted and reduces well via kernel decide (avoiding Finset.sort, which doesn't unfold structurally).

Equations

• f.linksTo i = List.filter (fun (k : Phonology.Autosegmental.ToneIdx) => decide ((k, i) ∈ f.surfaceLinks)) (List.range f.ulTones.length)

def Phonology.Autosegmental.FloatingForm.toneSequence {S : Type} (f : FloatingForm S) (i : SegIdx) : List RegisterTier.TRN

Sequence of tone values linked to TBU i, in tier order.

Equations

• f.toneSequence i = List.filterMap (fun (k : Phonology.Autosegmental.ToneIdx) => Option.map Phonology.Autosegmental.ToneSpec.tone f.ulTones[k]?) (f.linksTo i)

def Phonology.Autosegmental.FloatingForm.aliveTones {S : Type} (f : FloatingForm S) : List ToneIdx

Indices of alive (non-deleted) underlying tones, in tier order. Iterates List.range f.ulTones.length so the result is naturally sorted and reduces well via kernel decide.

Equations

• f.aliveTones = List.filter (fun (k : Phonology.Autosegmental.ToneIdx) => decide (f.IsAlive k)) (List.range f.ulTones.length)

def Phonology.Autosegmental.FloatingForm.segsOfMorpheme {S : Type} (f : FloatingForm S) (m : MorphemeId) : List SegIdx

Segment indices belonging to morpheme m, in segmental order. Out-of-range indices are excluded by construction.

Equations

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