Autosegmental Representations

@cite{goldsmith-1976} @cite{sagey-1986}

Autosegmental phonology adds feature sharing to segmental representations: when adjacent segments share a geometric node's features, they are linked to a single autosegmental element on that node's tier. This module builds on the feature geometry (FeatureGeometry.lean) and segment type (Features.lean) to provide feature agreement predicates, autosegmental representations with consistency checking, spread/delink operations, and a temporal derivation of the no-crossing constraint (@cite{sagey-1986} §5.3) including the negative argument against simultaneity (§5.2.2).

def Phonology.Autosegmental.agreeAt (s1 s2 : Segment) (n : FeatureGeometry.GeomNode) : Bool

Do s1 and s2 agree on all features dominated by node n?

Equations

• Phonology.Autosegmental.agreeAt s1 s2 n = n.features.all fun (f : Phonology.Feature) => s1.spec f == s2.spec f

def Phonology.Autosegmental.placeAssimilation (s1 s2 : Segment) : Bool

Place assimilation: agreement on all place features.

Equations

• Phonology.Autosegmental.placeAssimilation s1 s2 = Phonology.Autosegmental.agreeAt s1 s2 Phonology.FeatureGeometry.GeomNode.place

def Phonology.Autosegmental.totalAssimilation (s1 s2 : Segment) : Bool

Total assimilation: agreement on all supralaryngeal features.

Equations

• Phonology.Autosegmental.totalAssimilation s1 s2 = Phonology.Autosegmental.agreeAt s1 s2 Phonology.FeatureGeometry.GeomNode.supralaryngeal

structure Phonology.Autosegmental.Sharing : Type

Segments at positions left and left + 1 share all features dominated by node.

• left : ℕ
• node : FeatureGeometry.GeomNode

@[implicit_reducible]

instance Phonology.Autosegmental.instDecidableEqSharing : DecidableEq Sharing

Equations

• Phonology.Autosegmental.instDecidableEqSharing = Phonology.Autosegmental.instDecidableEqSharing.decEq

def Phonology.Autosegmental.instDecidableEqSharing.decEq (x✝ x✝¹ : Sharing) : Decidable (x✝ = x✝¹)

Equations

• Phonology.Autosegmental.instDecidableEqSharing.decEq { left := a, node := a_1 } { left := b, node := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Phonology.Autosegmental.instReprSharing.repr : Sharing → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.instReprSharing : Repr Sharing

Equations

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

structure Phonology.Autosegmental.AutosegRep : Type

An autosegmental representation: a sequence of segments with an explicit record of which adjacent pairs share features under which geometric nodes.

• segments : List Segment
• sharing : List Sharing

def Phonology.Autosegmental.AutosegRep.inBounds (r : AutosegRep) : Bool

Are all sharing specifications within bounds?

Equations

• r.inBounds = r.sharing.all fun (s : Phonology.Autosegmental.Sharing) => decide (s.left + 1 < r.segments.length)

def Phonology.Autosegmental.AutosegRep.consistent (r : AutosegRep) : Bool

Is each sharing specification consistent with the segments' feature values?

Equations

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

def Phonology.Autosegmental.AutosegRep.spread (r : AutosegRep) (pos : ℕ) (n : FeatureGeometry.GeomNode) : AutosegRep

Spread node n rightward from position pos.

Equations

• r.spread pos n = { segments := r.segments, sharing := { left := pos, node := n } :: r.sharing }

def Phonology.Autosegmental.AutosegRep.delink (r : AutosegRep) (pos : ℕ) (n : FeatureGeometry.GeomNode) : AutosegRep

Remove sharing at position pos for node n.

Equations

• r.delink pos n = { segments := r.segments, sharing := List.filter (fun (s : Phonology.Autosegmental.Sharing) => !(s.left == pos && s.node == n)) r.sharing }

def Phonology.Autosegmental.copyFeaturesUnder (tgt src : Segment) (n : FeatureGeometry.GeomNode) : Segment

Replace all features under geometric node n in tgt with src's values. This models autosegmental node replacement: when a place node spreads, the entire node (including unspecified features) is copied, not just the specified ones.

Equations

• Phonology.Autosegmental.copyFeaturesUnder tgt src n = { spec := fun (f : Phonology.Feature) => if decide (f.DominatedBy n) = true then src.spec f else tgt.spec f }

def Phonology.Autosegmental.AutosegRep.spreadFeatures (r : AutosegRep) (pos : ℕ) (n : FeatureGeometry.GeomNode) : AutosegRep

Spread node n from position pos + 1 onto position pos, replacing the target's features under n with the trigger's values and recording the sharing link.

Equations

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

theorem Phonology.Autosegmental.copyFeaturesUnder_agreeAt (tgt src : Segment) (n : FeatureGeometry.GeomNode) : agreeAt (copyFeaturesUnder tgt src n) src n = true

After copying features under node n, the result agrees with the source at that node.

theorem Phonology.Autosegmental.agreeAt_refl (s : Segment) (n : FeatureGeometry.GeomNode) : agreeAt s s n = true

Agreement is reflexive.

theorem Phonology.Autosegmental.place_assimilation_checks_14 : FeatureGeometry.GeomNode.place.features.length = 14

Place assimilation checks 14 features (the place node's natural class).

theorem Phonology.Autosegmental.total_assimilation_checks_16 : FeatureGeometry.GeomNode.supralaryngeal.features.length = 16

Total assimilation checks 16 features (the supralaryngeal node's natural class, including [nasal] via the soft palate node).

theorem Phonology.Autosegmental.spread_delink_not_present (r : AutosegRep) (pos : ℕ) (n : FeatureGeometry.GeomNode) (h : (r.sharing.all fun (s : Sharing) => !(s.left == pos && s.node == n)) = true) : (r.spread pos n).delink pos n = r

Spreading and then delinking returns the original representation when the position/node pair was not already present in the sharing list.

Temporal derivation of the No-Crossing Constraint

@cite{sagey-1986} §5.3 derives the ban on crossing association lines from temporal precedence rather than stipulating it as a well-formedness condition.

The key move is choosing the right temporal relation for association lines. Simultaneity (identity of time points) is too strong — it predicts that contour segments and geminates are impossible, since two distinct elements cannot both be identical to the same time point (§5.2.2). Overlap is the correct relation: it is reflexive and symmetric but crucially NOT transitive (Interval.overlaps_not_transitive), which is what allows the NCC proof to go through via a contradiction chain (§5.2.3, fn. 6).

The derivation (§5.3, p.294): if timing₁ ≺ timing₂ on the timing tier but melody₂ ≺ melody₁ on the melody tier, the overlap requirements on valid associations produce a chain melody₂.finish < melody₁.start ≤ timing₁.finish < timing₂.start ≤ melody₂.finish — a contradiction. Crossing is therefore logically impossible for valid associations.

This section formalizes the derivation using Core.Time.Interval for temporal intervals and its precedes/overlaps relations.

structure Phonology.Autosegmental.TierPosition (T : Type u_2) [LinearOrder T] : Type u_2

A position on an autosegmental tier, occupying a temporal interval.

• interval : Core.Time.Interval T

structure Phonology.Autosegmental.Association (T : Type u_2) [LinearOrder T] : Type u_2

An association between a timing-tier position and a melody-tier position. An association line represents temporal overlap: the melody element is realized during the timing position's interval.

• timing : TierPosition T
• melody : TierPosition T

def Phonology.Autosegmental.validAssociation {T : Type u_1} [LinearOrder T] (a : Association T) : Prop

Association validity: the timing and melody intervals must overlap. This is the phonetic grounding — an association line means the melodic content is realized during the timing slot.

Equations

• Phonology.Autosegmental.validAssociation a = a.timing.interval.overlaps a.melody.interval

theorem Phonology.Autosegmental.simultaneity_no_contours {T : Type u_2} (t m₁ m₂ : T) (h₁ : t = m₁) (h₂ : t = m₂) : m₁ = m₂

Simultaneity contradicts contours (@cite{sagey-1986} §5.2.2): if association required temporal identity (simultaneity), contour segments — two distinct melody elements F ≠ G associated to the same timing position x — would be impossible, since F = x and G = x imply F = G by transitivity. This is Sagey's negative argument for why association must be overlap, not identity.

def Phonology.Autosegmental.crosses {T : Type u_1} [LinearOrder T] (a₁ a₂ : Association T) : Prop

Two associations cross iff their timing positions are ordered one way but their melody positions are ordered the other way. Crossing(a₁, a₂) ≡ timing₁ ≺ timing₂ ∧ melody₂ ≺ melody₁.

Equations

• Phonology.Autosegmental.crosses a₁ a₂ = (a₁.timing.interval.precedes a₂.timing.interval ∧ a₂.melody.interval.precedes a₁.melody.interval)

theorem Phonology.Autosegmental.no_crossing {T : Type u_1} [LinearOrder T] (a₁ a₂ : Association T) (h₁ : validAssociation a₁) (h₂ : validAssociation a₂) : ¬crosses a₁ a₂

No-Crossing Constraint (@cite{sagey-1986} §5.3, @cite{goldsmith-1976}): Two valid associations cannot cross.

If timing₁ ≺ timing₂, then timing₁.finish < timing₂.start. Validity requires timing₁ overlaps melody₁ and timing₂ overlaps melody₂. If melodies also cross (melody₂ ≺ melody₁), then melody₂.finish < melody₁.start.

From timing₁ overlaps melody₁: melody₁.start ≤ timing₁.finish. From timing₂ overlaps melody₂: timing₂.start ≤ melody₂.finish.

Chaining: melody₂.finish < melody₁.start ≤ timing₁.finish < timing₂.start ≤ melody₂.finish. This gives melody₂.finish < melody₂.finish — a contradiction.

theorem Phonology.Autosegmental.no_crossing_symm {T : Type u_1} [LinearOrder T] (a₁ a₂ : Association T) (h₁ : validAssociation a₁) (h₂ : validAssociation a₂) : ¬crosses a₂ a₁

Crossing is also impossible in the symmetric direction: if timing₂ ≺ timing₁ and melody₁ ≺ melody₂, the same contradiction arises.

def Phonology.Autosegmental.geminate {T : Type u_1} [LinearOrder T] (t1s t1f t2s t2f ms mf : T) (h1 : t1s ≤ t1f) (h2 : t2s ≤ t2f) (hm : ms ≤ mf) : Association T × Association T

A geminate consonant: two adjacent timing positions associated to a single melodic element. The melodic element's interval spans both timing slots.

Example: /t/ linked to two C-slots in [atta].

C-tier:    C₁    C₂
            \  /
melody:     t

Equations

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

def Phonology.Autosegmental.contourTone {T : Type u_1} [LinearOrder T] (ts tf m1s m1f m2s m2f : T) (ht : ts ≤ tf) (hm1 : m1s ≤ m1f) (hm2 : m2s ≤ m2f) : Association T × Association T

A contour tone: one timing position associated to two tonal elements sequenced within it. The two tonal elements occupy sub-intervals.

Example: falling tone HL on a single syllable.

timing:     σ
           / \
tone:     H   L

Equations

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