Autosegmental Representations

@cite{goldsmith-1976}

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 association lines, feature agreement predicates, autosegmental representations with consistency checking, spread/delink operations, and OCP violation counting.

structure Theories.Phonology.Autosegmental.AssocLine : Type

An association line connects a source position to a target position on an autosegmental tier.

• src : Nat
• tgt : Nat

def Theories.Phonology.Autosegmental.instDecidableEqAssocLine.decEq (x✝ x✝¹ : AssocLine) : Decidable (x✝ = x✝¹)

Equations

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

instance Theories.Phonology.Autosegmental.instDecidableEqAssocLine : DecidableEq AssocLine

Equations

• Theories.Phonology.Autosegmental.instDecidableEqAssocLine = Theories.Phonology.Autosegmental.instDecidableEqAssocLine.decEq

instance Theories.Phonology.Autosegmental.instBEqAssocLine : BEq AssocLine

Equations

• Theories.Phonology.Autosegmental.instBEqAssocLine = { beq := Theories.Phonology.Autosegmental.instBEqAssocLine.beq }

def Theories.Phonology.Autosegmental.instBEqAssocLine.beq : AssocLine → AssocLine → Bool

Equations

• Theories.Phonology.Autosegmental.instBEqAssocLine.beq { src := a, tgt := a_1 } { src := b, tgt := b_1 } = (a == b && a_1 == b_1)
• Theories.Phonology.Autosegmental.instBEqAssocLine.beq x✝¹ x✝ = false

instance Theories.Phonology.Autosegmental.instReprAssocLine : Repr AssocLine

Equations

• Theories.Phonology.Autosegmental.instReprAssocLine = { reprPrec := Theories.Phonology.Autosegmental.instReprAssocLine.repr }

def Theories.Phonology.Autosegmental.instReprAssocLine.repr : AssocLine → Nat → Std.Format

Equations

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

def Theories.Phonology.Autosegmental.noCrossing (lines : List AssocLine) : Bool

Association lines do not cross: if src₁ < src₂ then tgt₁ ≤ tgt₂.

Equations

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

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

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

Equations

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

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

Place assimilation: agreement on all place features.

Equations

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

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

Total assimilation: agreement on all supralaryngeal features.

Equations

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

structure Theories.Phonology.Autosegmental.Sharing : Type

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

• left : Nat
• node : FeatureGeometry.GeomNode

instance Theories.Phonology.Autosegmental.instDecidableEqSharing : DecidableEq Sharing

Equations

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

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

Equations

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

instance Theories.Phonology.Autosegmental.instBEqSharing : BEq Sharing

Equations

• Theories.Phonology.Autosegmental.instBEqSharing = { beq := Theories.Phonology.Autosegmental.instBEqSharing.beq }

def Theories.Phonology.Autosegmental.instBEqSharing.beq : Sharing → Sharing → Bool

Equations

• Theories.Phonology.Autosegmental.instBEqSharing.beq { left := a, node := a_1 } { left := b, node := b_1 } = (a == b && a_1 == b_1)
• Theories.Phonology.Autosegmental.instBEqSharing.beq x✝¹ x✝ = false

def Theories.Phonology.Autosegmental.instReprSharing.repr : Sharing → Nat → Std.Format

Equations

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

instance Theories.Phonology.Autosegmental.instReprSharing : Repr Sharing

Equations

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

structure Theories.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 Theories.Phonology.Autosegmental.AutosegRep.inBounds (r : AutosegRep) : Bool

Are all sharing specifications within bounds?

Equations

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

def Theories.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 Theories.Phonology.Autosegmental.AutosegRep.spread (r : AutosegRep) (pos : Nat) (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 Theories.Phonology.Autosegmental.AutosegRep.delink (r : AutosegRep) (pos : Nat) (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 : Theories.Phonology.Autosegmental.Sharing) => !(s.left == pos && s.node == n)) r.sharing }

def Theories.Phonology.Autosegmental.AutosegRep.delinkAll (r : AutosegRep) (n : FeatureGeometry.GeomNode) : AutosegRep

Remove all sharing involving node n.

Equations

• r.delinkAll n = { segments := r.segments, sharing := List.filter (fun (s : Theories.Phonology.Autosegmental.Sharing) => s.node != n) r.sharing }

def Theories.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

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

def Theories.Phonology.Autosegmental.AutosegRep.spreadFeatures (r : AutosegRep) (pos : Nat) (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 Theories.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.

def Theories.Phonology.Autosegmental.ocpViolations (segs : List Segment) (n : FeatureGeometry.GeomNode) : Nat

Count OCP violations for node n: adjacent segments that agree on all features dominated by n. Returns Nat matching OT/Core.lean's NamedConstraint.eval.

Equations

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

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

Agreement is reflexive.

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

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

theorem Theories.Phonology.Autosegmental.total_assimilation_checks_15 : FeatureGeometry.GeomNode.supralaryngeal.features.length = 15

Total assimilation checks 15 features (the supralaryngeal node's natural class).

theorem Theories.Phonology.Autosegmental.spread_delink_not_present (r : AutosegRep) (pos : Nat) (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.