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 M, SegSpec S M — tier and backbone elements carrying membership in a sponsor of opaque type M — the morpheme identity, kept abstract so the phonology imports nothing from the morphology (Morphology instantiates M := Morpheme at its call sites).
• FloatingForm S T M — 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) (M : Type u_2) : Type (max u_1 u_2)

An autosegmental tier element: a value of type T plus its sponsoring morpheme identity M. Generalises [Gol76]'s tonal-tier element to arbitrary tier-value types (tones, segments, features) and an opaque sponsor.

• value : T

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

• morpheme : M

  The sponsoring morpheme identity (opaque).

@[instance_reducible]

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

Equations

• Autosegmental.instDecidableEqTierSpec = Autosegmental.instDecidableEqTierSpec.decEq

def Autosegmental.instDecidableEqTierSpec.decEq {T✝ : Type u_1} {M✝ : Type u_2} [DecidableEq T✝] [DecidableEq M✝] (x✝ x✝¹ : TierSpec T✝ M✝) : 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 ⋯

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

Equations

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

@[instance_reducible]

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

Equations

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

structure Autosegmental.SegSpec (S : Type u_1) (M : Type u_2) : Type (max u_1 u_2)

A segmental backbone element: segment plus its sponsoring morpheme identity. Generic over the segment type S and sponsor type M.

• seg : S
• morpheme : M

  The sponsoring morpheme identity (opaque).

def Autosegmental.instDecidableEqSegSpec.decEq {S✝ : Type u_1} {M✝ : Type u_2} [DecidableEq S✝] [DecidableEq M✝] (x✝ x✝¹ : SegSpec S✝ M✝) : 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 ⋯

@[instance_reducible]

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

Equations

• Autosegmental.instDecidableEqSegSpec = Autosegmental.instDecidableEqSegSpec.decEq

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

Equations

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

@[instance_reducible]

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

Equations

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

FloatingForm

FloatingForm S T M is an autosegmental form with segmental backbone of type S, tier-value type T, and sponsor type M. 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) (M : Type u_3) : Type (max (max u_1 u_2) u_3)

An autosegmental form: an underlying two-tier presentation (tones over segments, with association links) plus OT-style surface bookkeeping — deletedTier and surfaceLinks track the surface state separately.

• upper : LabeledTuple (TierSpec T M)

  The tonal tier (underlying).

• lower : LabeledTuple (SegSpec S M)

  The segmental backbone (underlying).

• links : Finset Link

  The underlying association links.

• 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).

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

Equations

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

@[instance_reducible]

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

Equations

• Autosegmental.instDecidableEqFloatingForm = Autosegmental.instDecidableEqFloatingForm.decEq

@[instance_reducible]

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

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, inline]

abbrev Autosegmental.FloatingForm.SurfaceIsPlanar {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : FloatingForm S T M) : Prop

The surface state is planar: the surface links satisfy the per-pair No-Crossing Constraint.

Equations

• f.SurfaceIsPlanar = Autosegmental.IsNonCrossing f.surfaceLinks

Construction

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

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} {M : Type u_3} (f : FloatingForm S T M) (k : TierIdx) : Option M

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} {M : Type u_3} (f : FloatingForm S T M) (i : SegIdx) : Option M

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} {M : Type u_3} [DecidableEq M] (f : FloatingForm S T M) : Finset M

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} {M : Type u_3} (f : FloatingForm S T M) (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} {M : Type u_3} (f : FloatingForm S T M) (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} {M : Type u_3} (f : FloatingForm S T M) (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} {M : Type u_3} (f : FloatingForm S T M) (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} {M : Type u_3} (f : FloatingForm S T M) (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} {M : Type u_3} (f : FloatingForm S T M) (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} {M : Type u_3} (f : FloatingForm S T M) (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)

@[reducible, inline]

abbrev Autosegmental.FloatingForm.SurfaceLinkedLower {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : FloatingForm S T M) (i : SegIdx) : Prop

The lower-tier slot i is linked on the surface.

Equations

• f.SurfaceLinkedLower i = ∃ l ∈ f.surfaceLinks, l.2 = i

def Autosegmental.FloatingForm.InBounds {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : FloatingForm S T M) : Prop

The presentation is in bounds: every link's endpoints index into the tiers.

Equations

• f.InBounds = ∀ p ∈ f.links, p.1 < f.upper.len ∧ p.2 < f.lower.len

@[instance_reducible]

instance Autosegmental.FloatingForm.instDecidableInBoundsOfDecidableEq {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : FloatingForm S T M) [DecidableEq S] [DecidableEq T] : Decidable f.InBounds

Equations

• f.instDecidableInBoundsOfDecidableEq = Autosegmental.FloatingForm.instDecidableInBoundsOfDecidableEq._aux_1 f

Input concatenation

def Autosegmental.FloatingForm.hconcat {S : Type u_1} {T : Type u_2} {M : Type u_3} (f g : FloatingForm S T M) : FloatingForm S T M

Concatenation of underlying input states ([JH15]): tier juxtaposition with index-shifted links, surface mirroring underlying.

Equations

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

@[simp]

theorem Autosegmental.FloatingForm.hconcat_upper {S : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq S] [DecidableEq T] [DecidableEq M] (f g : FloatingForm S T M) : (f.hconcat g).upper = f.upper.concat g.upper

@[simp]

theorem Autosegmental.FloatingForm.hconcat_lower {S : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq S] [DecidableEq T] [DecidableEq M] (f g : FloatingForm S T M) : (f.hconcat g).lower = f.lower.concat g.lower

@[simp]

theorem Autosegmental.FloatingForm.hconcat_links {S : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq S] [DecidableEq T] [DecidableEq M] (f g : FloatingForm S T M) : (f.hconcat g).links = f.links ∪ Finset.image (shiftLink f.upper.len f.lower.len) g.links

@[simp]

theorem Autosegmental.FloatingForm.hconcat_surfaceLinks {S : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq S] [DecidableEq T] [DecidableEq M] (f g : FloatingForm S T M) : (f.hconcat g).surfaceLinks = f.links ∪ Finset.image (shiftLink f.upper.len f.lower.len) g.links

@[simp]

theorem Autosegmental.FloatingForm.hconcat_deletedTier {S : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq S] [DecidableEq T] [DecidableEq M] (f g : FloatingForm S T M) : (f.hconcat g).deletedTier = ∅

Atomic GEN operations

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

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

Equations

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

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

Insert a surface link (k, i).

Equations

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

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

Delete the surface link (k, i).

Equations

• f.deleteLink k i = { upper := f.upper, lower := f.lower, links := f.links, 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} {M : Type u_3} (f : FloatingForm S T M) (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} {M : Type u_3} [DecidableEq S] [DecidableEq T] [DecidableEq M] (f : FloatingForm S T M) : Finset (FloatingForm S T M)

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} {M : Type u_3} [DecidableEq S] [DecidableEq T] [DecidableEq M] (f : FloatingForm S T M) (h : f.SurfaceIsPlanar) (g : FloatingForm S T M) : g ∈ f.gen → g.SurfaceIsPlanar

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} {M : Type u_3} (f : FloatingForm S T M) : 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} {M : Type u_3} (f : FloatingForm S T M) (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} {M : Type u_3} (f : FloatingForm S T M) (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} {M : Type u_3} (f : FloatingForm S T M) : 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} {M : Type u_3} [DecidableEq M] (f : FloatingForm S T M) (m : M) : 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} {M : Type u_3} (f : FloatingForm S T M) (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} {M : Type u_3} (f : FloatingForm S T M) (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)

def Autosegmental.FloatingForm.emptyInput {S : Type u_1} {T : Type u_2} {M : Type u_3} : FloatingForm S T M

The empty input.

Equations

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

def Autosegmental.FloatingForm.concatInputs {S : Type u_1} {T : Type u_2} {M : Type u_3} (gs : List (FloatingForm S T M)) : FloatingForm S T M

Left-to-right concatenation of a list of input states.

Equations

• Autosegmental.FloatingForm.concatInputs gs = List.foldr Autosegmental.FloatingForm.hconcat Autosegmental.FloatingForm.emptyInput gs