Floating autosegmental form (Goldsmith)

Goldsmith-style autosegmental representation: tier elements (tones, floating segments, features) sit on a tier above the segmental backbone, connected by association lines (links). Multiple tier elements can associate to one backbone position (forming contours); a tier element with no associations is floating. Generic over both backbone type S (the lower tier) and tier-value type T (the upper tier); tonal use instantiates T := TRN, while non-tonal autosegmental work ([LK26]'s floating consonants, [Lie83]'s floating features, [Zim17]'s floating moras and prosodic nodes) chooses other T values.

Main definitions

• Link — an autosegmental link (tier-index, backbone-index).
• TierSpec T, SegSpec S — tier and backbone elements carrying morpheme membership via Morphology.WordStructure.Morpheme (re-exported into this namespace).
• FloatingForm S T — autosegmental form with underlying/surface split.
• FloatingForm.IsAlive, IsLinked, IsFloating, IsTautomorphemic, Crosses — decidable predicates on tier elements and links.
• FloatingForm.deleteTierElem, insertLink, deleteLink — atomic GEN operations (paper subset).
• FloatingForm.gen — one-step GEN as a Finset of candidate forms.
• FloatingForm.floatIndicator, linksTo, tierValues — indicator vectors for constraint evaluation.

Main results

• FloatingForm.gen_preserves_isPlanar — GEN is closed on the no-crossing WFC ([Gol76] / [Pul86]): every one-step candidate of a planar surface graph is itself planar.

Implementation notes

A FloatingForm carries an immutable underlying state (the inherited Graph: lower, upper, links) and a mutable surface state (deletedTier, surfaceLinks); GEN modifies only the surface. A tier element is floating iff it is alive (not deleted) and no surface link references it. This multi-element-per-position encoding (vs. the prior tonalOverwrite) is what [McPL26]'s *CROWD / *FALL constraints require.

gen is a paper-subset (delete tier element, insert/delete link; no insert-and-associate or shift), filtered for no-crossing ([Gol76]). A link is tautomorphemic when its tier element and backbone share a morpheme (*TAUTDOCK, after [Wol07]).

Tier and link primitives

@[reducible, inline]

abbrev Autosegmental.TierIdx : Type

Index into the upper tier.

Equations

• Autosegmental.TierIdx = ℕ

@[reducible, inline]

abbrev Autosegmental.SegIdx : Type

Index into the lower tier.

Equations

• Autosegmental.SegIdx = ℕ

@[reducible, inline]

abbrev Autosegmental.Link : Type

An autosegmental link: tier element fst is associated to backbone-position snd.

Equations

• Autosegmental.Link = (Autosegmental.TierIdx × Autosegmental.SegIdx)

structure Autosegmental.TierSpec (T : Type u_1) : Type u_1

An autosegmental tier element: a value of type T plus morpheme membership. Generalises [Gol76]'s tonal-tier element to arbitrary tier-value types (tones, segments, features).

• value : T

  The tier value (tone, segment, feature, ...).

• morpheme : Morpheme

def Autosegmental.instDecidableEqTierSpec.decEq {T✝ : Type u_1} [DecidableEq T✝] (x✝ x✝¹ : TierSpec T✝) : Decidable (x✝ = x✝¹)

Equations

• Autosegmental.instDecidableEqTierSpec.decEq { value := a, morpheme := a_1 } { value := b, morpheme := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Autosegmental.instDecidableEqTierSpec {T✝ : Type u_1} [DecidableEq T✝] : DecidableEq (TierSpec T✝)

Equations

• Autosegmental.instDecidableEqTierSpec = Autosegmental.instDecidableEqTierSpec.decEq

@[implicit_reducible]

instance Autosegmental.instReprTierSpec {T✝ : Type u_1} [Repr T✝] : Repr (TierSpec T✝)

Equations

• Autosegmental.instReprTierSpec = { reprPrec := Autosegmental.instReprTierSpec.repr }

def Autosegmental.instReprTierSpec.repr {T✝ : Type u_1} [Repr T✝] : TierSpec T✝ → ℕ → Std.Format

Equations

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

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

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

• seg : S
• morpheme : Morpheme

def Autosegmental.instDecidableEqSegSpec.decEq {S✝ : Type u_1} [DecidableEq S✝] (x✝ x✝¹ : SegSpec S✝) : Decidable (x✝ = x✝¹)

Equations

• Autosegmental.instDecidableEqSegSpec.decEq { seg := a, morpheme := a_1 } { seg := b, morpheme := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

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

Equations

• Autosegmental.instDecidableEqSegSpec = Autosegmental.instDecidableEqSegSpec.decEq

@[implicit_reducible]

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

Equations

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

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

Equations

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

FloatingForm

FloatingForm S T is an autosegmental form with segmental backbone of type S and tier-value type T. Tonal use chooses T := TRN; non-tonal autosegmental work chooses other T values ([LK26], [Lie83]). The OT-style bookkeeping (deletedTier, surfaceLinks vs underlying links) is language-independent.

structure Autosegmental.FloatingForm (S : Type u_1) (T : Type u_2) extends Autosegmental.Graph (Autosegmental.TierSpec T) (Autosegmental.SegSpec S) : Type (max u_1 u_2)

An autosegmental form: extends Graph (TierSpec T) (SegSpec S) with OT-style surface bookkeeping. The inherited Graph is the underlying representation; deletedTier and surfaceLinks track the surface state separately.

• upper : LabeledTuple (TierSpec T)
• lower : LabeledTuple (SegSpec S)
• links : Finset (ℕ × ℕ)
• deletedTier : Finset TierIdx

  SURFACE deletion set on the upper tier (current state).

• surfaceLinks : Finset Link

  SURFACE association lines (current state). May differ from the inherited links (the underlying associations).

@[implicit_reducible]

instance Autosegmental.instDecidableEqFloatingForm {S✝ : Type u_1} {T✝ : Type u_2} [DecidableEq S✝] [DecidableEq T✝] : DecidableEq (FloatingForm S✝ T✝)

Equations

• Autosegmental.instDecidableEqFloatingForm = Autosegmental.instDecidableEqFloatingForm.decEq

def Autosegmental.instDecidableEqFloatingForm.decEq {S✝ : Type u_1} {T✝ : Type u_2} [DecidableEq S✝] [DecidableEq T✝] (x✝ x✝¹ : FloatingForm S✝ T✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Autosegmental.instReprFloatingForm {S : Type u_1} {T : Type u_2} [Repr S] [Repr T] : Repr (FloatingForm S T)

Hides the Finset fields (mathlib's Finset.Repr is unsafe) and prints only segments and underlying tier elements; debug-only.

Equations

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

Surface graph (derived view)

@[reducible]

def Autosegmental.FloatingForm.surfaceGraph {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) : Graph (TierSpec T) (SegSpec S)

The surface graph: same tiers as the underlying graph but with surfaceLinks in place of links. Makes the underlying/surface duality explicit — both states are Graphs sharing tier data.

Equations

• f.surfaceGraph = { upper := f.upper, lower := f.lower, links := f.surfaceLinks }

Construction

def Autosegmental.FloatingForm.mkInput {S : Type u_1} {T : Type u_2} (lower : List (SegSpec S)) (upper : List (TierSpec T)) (links : Finset Link) : FloatingForm S T

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

Equations

• Autosegmental.FloatingForm.mkInput lower upper links = { upper := LabeledTuple.ofList upper, lower := LabeledTuple.ofList lower, links := links, deletedTier := ∅, surfaceLinks := links }

Morphemic structure

def Autosegmental.FloatingForm.upperMorpheme? {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (k : TierIdx) : Option Morpheme

The morpheme of the k-th upper-tier element, or none if out of range.

Equations

• f.upperMorpheme? k = Option.map Autosegmental.TierSpec.morpheme (f.upper.get? k)

def Autosegmental.FloatingForm.lowerMorpheme? {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (i : SegIdx) : Option Morpheme

The morpheme of the i-th lower-tier element, or none if out of range.

Equations

• f.lowerMorpheme? i = Option.map Autosegmental.SegSpec.morpheme (f.lower.get? i)

def Autosegmental.FloatingForm.morphemes {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) : Finset Morpheme

Every morpheme occurring on either tier.

Equations

• f.morphemes = (List.map Autosegmental.SegSpec.morpheme f.lower.toList).toFinset ∪ (List.map Autosegmental.TierSpec.morpheme f.upper.toList).toFinset

Predicates on tier elements and links

@[reducible, inline]

abbrev Autosegmental.FloatingForm.IsAlive {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (k : TierIdx) : Prop

The upper-tier element at index k is alive (not deleted). The structural primitive; IsDeleted is its negation.

Equations

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

@[reducible, inline]

abbrev Autosegmental.FloatingForm.IsDeleted {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (k : TierIdx) : Prop

The upper-tier element at index k is deleted. Sugar for ¬ IsAlive.

Equations

• f.IsDeleted k = ¬f.IsAlive k

@[reducible, inline]

abbrev Autosegmental.FloatingForm.IsLinked {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (k : TierIdx) : Prop

The upper-tier element at index k is linked to a backbone position on the surface.

Equations

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

@[reducible, inline]

abbrev Autosegmental.FloatingForm.IsFloating {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (k : TierIdx) : Prop

The upper-tier element at index k is floating: in-bounds, alive (not deleted), and unlinked. The in-bounds guard mirrors the substrate's Graph.IsFloatingUpper, so out-of-range indices are not spuriously floating.

Equations

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

@[reducible, inline]

abbrev Autosegmental.FloatingForm.IsTautomorphemic {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (l : Link) : Prop

A surface link (k, i) is tautomorphemic iff its upper- and lower-tier endpoints share a morpheme. Out-of-range indices on either side make this false.

Equations

• f.IsTautomorphemic l = (f.upperMorpheme? l.1 = f.lowerMorpheme? l.2 ∧ (f.upper.get? l.1).isSome = true)

Faithfulness: surface vs underlying

@[reducible, inline]

abbrev Autosegmental.FloatingForm.IsInsertedLink {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (l : Link) : Prop

A surface link absent underlyingly — inserted by GEN (DEP / *TAUTDOCK source).

Equations

• f.IsInsertedLink l = (l ∈ f.surfaceLinks ∧ l ∉ f.links)

@[reducible, inline]

abbrev Autosegmental.FloatingForm.IsDeletedLink {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (l : Link) : Prop

An underlying link absent on the surface — deleted by GEN (MAX source).

Equations

• f.IsDeletedLink l = (l ∈ f.links ∧ l ∉ f.surfaceLinks)

Atomic GEN operations

def Autosegmental.FloatingForm.deleteTierElem {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (k : TierIdx) : FloatingForm S T

Delete the underlying upper-tier element at index k. Cascades to remove any surface link referencing it.

Equations

• f.deleteTierElem k = { toGraph := f.toGraph, deletedTier := insert k f.deletedTier, surfaceLinks := {l ∈ f.surfaceLinks | l.1 ≠ k} }

def Autosegmental.FloatingForm.insertLink {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (k : TierIdx) (i : SegIdx) : FloatingForm S T

Insert a surface link (k, i).

Equations

• f.insertLink k i = { toGraph := f.toGraph, deletedTier := f.deletedTier, surfaceLinks := insert (k, i) f.surfaceLinks }

def Autosegmental.FloatingForm.deleteLink {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (k : TierIdx) (i : SegIdx) : FloatingForm S T

Delete the surface link (k, i).

Equations

• f.deleteLink k i = { toGraph := f.toGraph, deletedTier := f.deletedTier, surfaceLinks := f.surfaceLinks.erase (k, i) }

Well-formedness: no crossing lines

@[reducible, inline]

abbrev Autosegmental.FloatingForm.Crosses {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (k : TierIdx) (i : SegIdx) : Prop

A candidate link (k, i) would cross an existing surface link. Wraps the substrate IndexCrosses on the candidate link (k, i); IsNonCrossing (via mathlib's MonovaryOn) provides the set-level NCC and inherits mathlib's lemma library.

Equations

• f.Crosses k i = Autosegmental.IndexCrosses f.surfaceLinks (k, i)

GEN: one-step candidate generation

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

One-step GEN: the faithful candidate, deleting each alive tone, and (for each FLOATING tone) inserting a link to each TBU that doesn't cross an existing link. One operation per step, after [McCMS12]; a subset of [McPL26]'s operation set (omits insert-and-associate and shift). The no-crossing filter ([Gol76]) enforces well-formedness: without it a floating tone could dock across an intervening linked tone.

Equations

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

theorem Autosegmental.FloatingForm.gen_preserves_isPlanar {S : Type u_1} {T : Type u_2} [DecidableEq S] [DecidableEq T] (f : FloatingForm S T) (h : f.surfaceGraph.IsPlanar) (g : FloatingForm S T) : g ∈ f.gen → g.surfaceGraph.IsPlanar

GEN preserves the no-crossing WFC ([Gol76] / [Pul86]). If the surface graph is planar, every one-step GEN candidate is too: deletes shrink the surface link set (IsNonCrossing.subset), and each inserted link passed the ¬ Crosses filter (IsNonCrossing.insert_of_not_indexCrosses). So gen is closed on the structural well-formedness condition.

Indicator vectors for constraint evaluation

def Autosegmental.FloatingForm.floatIndicator {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) : List ℕ

Indicator vector of floating upper-tier elements, in tier order: entry k is 1 iff upper[k] is currently floating, else 0. Drives directional floating constraints (e.g. *FLOAT).

Equations

• f.floatIndicator = List.map (fun (k : Autosegmental.TierIdx) => if f.IsFloating k then 1 else 0) (List.range f.upper.len)

def Autosegmental.FloatingForm.linksTo {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (i : SegIdx) : List TierIdx

Upper-tier elements surface-linked to backbone position i, in tier order (smallest index first). List.range-based so the result is naturally sorted and reduces under kernel decide (avoiding Finset.sort, which doesn't unfold structurally).

Equations

• f.linksTo i = List.filter (fun (k : Autosegmental.TierIdx) => decide ((k, i) ∈ f.surfaceLinks)) (List.range f.upper.len)

def Autosegmental.FloatingForm.tierValues {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (i : SegIdx) : List T

Sequence of tier values linked to backbone position i, in tier order.

Equations

• f.tierValues i = List.filterMap (fun (k : ℕ) => Option.map Autosegmental.TierSpec.value (f.upper.get? k)) (f.linksTo i)

Tier and morpheme subsequences

def Autosegmental.FloatingForm.aliveTierIdxs {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) : List TierIdx

Indices of alive (non-deleted) underlying upper-tier elements, in tier order; List.range-based so it reduces under kernel decide.

Equations

• f.aliveTierIdxs = List.filter (fun (k : Autosegmental.TierIdx) => decide (f.IsAlive k)) (List.range f.upper.len)

def Autosegmental.FloatingForm.segsOfMorpheme {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (m : Morpheme) : List SegIdx

Lower-tier (backbone) indices belonging to morpheme m, in order. Out-of-range indices are excluded by construction.

Equations

• f.segsOfMorpheme m = List.filter (fun (i : Autosegmental.SegIdx) => decide (f.lowerMorpheme? i = some m)) (List.range f.lower.len)

Position counts

def Autosegmental.FloatingForm.countUpper {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (p : TierIdx → Prop) [DecidablePred p] : ℕ

Count upper-tier positions satisfying decidable p. List.range-based so it reduces under kernel decide (avoiding Finset pipelines).

Equations

• f.countUpper p = List.countP (fun (k : Autosegmental.TierIdx) => decide (p k)) (List.range f.upper.len)

def Autosegmental.FloatingForm.countLower {S : Type u_1} {T : Type u_2} (f : FloatingForm S T) (p : SegIdx → Prop) [DecidablePred p] : ℕ

Count lower-tier (backbone) positions satisfying decidable p.

Equations

• f.countLower p = List.countP (fun (i : Autosegmental.SegIdx) => decide (p i)) (List.range f.lower.len)