Autosegmental feature sharing

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 is the feature-geometry representation (segments plus feature-sharing specifications over geometric nodes). Feature geometry is an extension of autosegmental phonology ([Cle85], [CH95b]): spreading is the association of one node to multiple anchors ([Cle85]). So this SharingRep is a flattened, adjacency-indexed special case of the bipartite tier-association object AR (Graph.lean / AR.lean) — a single segment backbone with a feature-agreement-consistency law, not two materialized tiers. A faithful re-grounding of feature spreading as AR association is future work; for now the two are kept as separate carriers. It builds on the feature geometry (Geometry.lean) and segment type (Defs.lean) to provide feature agreement predicates, feature-sharing representations with consistency checking, and spread/delink operations.

Main definitions

• agreeAt, placeAssimilation, totalAssimilation — feature agreement predicates over a geometric node.
• Sharing, SharingRep — feature-sharing representations: a segmental backbone plus a list of feature-sharing specifications.
• SharingRep.inBounds, SharingRep.consistent — well-formedness checks.
• SharingRep.spread, SharingRep.delink, SharingRep.spreadFeatures — atomic operations on feature-sharing representations.
• copyFeaturesUnder — replace features under a geometric node.

The Sagey-1986 interval-overlap derivation of the No-Crossing Constraint (TierPosition/Association/no_crossing/…) lives with its paper in Studies/Sagey1986.lean, its sole consumer.

Implementation notes

The temporal NCC derivation chooses overlap (reflexive, symmetric, not transitive) over simultaneity as the association relation. Simultaneity would predict that contour segments and geminates are impossible, since two distinct elements cannot be identical to the same time point.

References

• [Gol76] — autosegmental phonology, original NCC.
• [Cle85] — feature geometry as an extension of autosegmental phonology; spreading = association of one node to multiple anchors.
• [CH95b] — handbook synthesis of autosegmental phonology and feature geometry.
• [Sag86] — temporal derivation of NCC and the negative argument against simultaneity.

Feature agreement

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

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

Equations

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

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

Place assimilation: agreement on all place features.

Equations

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

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

Total assimilation: agreement on all supralaryngeal features.

Equations

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

Feature sharing

structure Autosegmental.Sharing : Type

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

• left : ℕ
• node : Phonology.FeatureGeometry.Node

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

Equations

• 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 ⋯

@[implicit_reducible]

instance Autosegmental.instDecidableEqSharing : DecidableEq Sharing

Equations

• Autosegmental.instDecidableEqSharing = Autosegmental.instDecidableEqSharing.decEq

@[implicit_reducible]

instance Autosegmental.instReprSharing : Repr Sharing

Equations

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

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

Equations

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

Autosegmental representation

structure Autosegmental.SharingRep : Type

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

• segments : List Phonology.Segment
• sharing : List Sharing

def Autosegmental.SharingRep.inBounds (r : SharingRep) : Bool

Are all sharing specifications within bounds?

Equations

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

def Autosegmental.SharingRep.consistent (r : SharingRep) : Bool

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

Equations

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

Operations

def Autosegmental.SharingRep.spread (r : SharingRep) (pos : ℕ) (n : Phonology.FeatureGeometry.Node) : SharingRep

Spread node n rightward from position pos.

Equations

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

def Autosegmental.SharingRep.delink (r : SharingRep) (pos : ℕ) (n : Phonology.FeatureGeometry.Node) : SharingRep

Remove sharing at position pos for node n.

Equations

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

Feature spreading

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

Replace all features under geometric node n in tgt with src's values. This models node spreading specifically ([Cle85]'s class-node assimilation): the entire node — including features src leaves unspecified — is copied. (The node-spreading analysis; single-feature spreading and underspecification-sensitive variants behave differently.)

Equations

• Autosegmental.copyFeaturesUnder tgt src n f = if decide (f.DominatedBy n) = true then src f else tgt f

def Autosegmental.SharingRep.spreadFeatures (r : SharingRep) (pos : ℕ) (n : Phonology.FeatureGeometry.Node) : SharingRep

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 Autosegmental.copyFeaturesUnder_agreeAt (tgt src : Phonology.Segment) (n : Phonology.FeatureGeometry.Node) : agreeAt (copyFeaturesUnder tgt src n) src n = true

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

Verification theorems

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

Agreement is reflexive.

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

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

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

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

theorem Autosegmental.spread_delink_not_present (r : SharingRep) (pos : ℕ) (n : Phonology.FeatureGeometry.Node) (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.