Featural Bundles

@cite{lionnet-2022} @cite{pulleyblank-1986} @cite{yip-1980} @cite{clements-1985} @cite{reiss-2017}

A feature bundle is a partial assignment over a feature index space. This is the most general primitive of autosegmental / featural phonology: every concrete feature theory (Snider Register Tier Theory @cite{snider-1999} @cite{snider-1990}; Lionnet's subtonal features @cite{lionnet-2022}; vowel or consonant harmony; nasal, laryngeal, place tiers) is a specialization of FeatureBundle F V for some feature index F and value type V.

Design

A bundle is a partial assignment F → Option V:

• none at f means underspecified — the language assigns no value to that feature on that bearer, leaving it open to fill in by default, spread, or remain underspecified at the surface.
• some v at f means specified with value v.

The value type V is parametric:

• Bool recovers classical binary features [±F] (Snider, Lionnet 2022, most generative phonology).
• ℚ or ℝ recovers Gradient Symbolic Computation @cite{smolensky-goldrick-2016} and probabilistic / weighted feature theories @cite{pater-2009}.
• A finite enum recovers privative / multivalued features.

Why this is the right primitive

1. @cite{reiss-2017}'s Substance-Free Phonology argues features are language-particular. Parameterising over F is exactly the right move: the feature space is data, not built into the type.

2. The autosegmental tier is just a sequence of bundles (Tier F V := List (FeatureBundle F V)). Association to bearers and no-crossing constraints can be added on top without changing the bundle algebra.

3. Tonal Root Nodes (Snider, Lionnet) are bundles over a tonal feature space (Subtonal := {upper, raised} for Lionnet 2022). H/M/L are not primitive types — they are named bundles.

4. Operations on bundles (merge for OCP, spread for assimilation, delete for replaceness) are pure functions on the parametric type, so each specialization inherits them.

Connection to existing infrastructure

• Core/StringHom.lean (Kleisli morphisms of Option) is exactly the type of tier-projection homomorphisms Tier F V → Tier F' V'.
• Core/Order/FeaturePreorder.lean gives the satisfaction preorder on bundles when V carries an order.
• Theories/Phonology/Autosegmental/Tier.lean (already present) collects tier-rule infrastructure that the bundle algebra slots into.

@[reducible, inline]

abbrev Phonology.Featural.FeatureBundle (F : Type u) (V : Type v) : Type (max u v)

A feature bundle: a partial assignment of values from V to features in F. none is underspecified, some v is specified.

For binary features, take V = Bool. For gradient / probabilistic features, take V = ℚ or ℝ. For privative features, take V = Unit (presence vs absence).

Equations

• Phonology.Featural.FeatureBundle F V = (F → Option V)

@[reducible, inline]

abbrev Phonology.Featural.Tier (F : Type u) (V : Type v) : Type (max u v)

A tier is a sequence of bundles over the same feature space. The sequence captures paradigmatic feature content; syntagmatic relations (adjacency, no-crossing, association to a TBU tier) are layered on top.

Equations

• Phonology.Featural.Tier F V = List (Phonology.Featural.FeatureBundle F V)

def Phonology.Featural.FeatureBundle.empty {F : Type u} {V : Type v} : FeatureBundle F V

The empty bundle: every feature is underspecified.

Equations

• Phonology.Featural.FeatureBundle.empty x✝ = none

def Phonology.Featural.FeatureBundle.single {F : Type u} {V : Type v} [DecidableEq F] (f : F) (v : V) : FeatureBundle F V

A bundle that specifies a single feature f with value v and leaves everything else underspecified. Defined via Function.update so that Function.update_same/update_noteq lemmas apply.

Equations

• Phonology.Featural.FeatureBundle.single f v = Function.update Phonology.Featural.FeatureBundle.empty f (some v)

def Phonology.Featural.FeatureBundle.isSpec {F : Type u} {V : Type v} (b : FeatureBundle F V) (f : F) : Bool

Test whether a bundle specifies feature f (i.e. assigns it some value rather than none).

Equations

• b.isSpec f = (b f).isSome

def Phonology.Featural.FeatureBundle.agreesOn {F : Type u} {V : Type v} [DecidableEq V] (b₁ b₂ : FeatureBundle F V) (f : F) : Bool

Test whether two bundles agree on feature f: either both leave it unspecified, or both assign it the same value. Conflict (one specifies v₁, the other v₂ with v₁ ≠ v₂) returns false.

Equations

• b₁.agreesOn b₂ f = match b₁ f, b₂ f with | none, none => true | some v₁, some v₂ => decide (v₁ = v₂) | x, x_1 => false

def Phonology.Featural.FeatureBundle.merge {F : Type u} {V : Type v} (b₁ b₂ : FeatureBundle F V) : FeatureBundle F V

Bundle merger (OCP-style): combine two bundles, taking the value from b₁ where it is specified and falling back to b₂ otherwise. Underspecification on both sides remains underspecified.

Used for OCP merger of adjacent identical features (@cite{lionnet-2022} ex. 53–54) and for default-fill operations.

Equations

• b₁.merge b₂ f = (b₁ f).orElse fun (x : Unit) => b₂ f

def Phonology.Featural.FeatureBundle.assimilate {F : Type u} {V : Type v} [DecidableEq F] (f : F) (src tgt : FeatureBundle F V) : FeatureBundle F V

Subtonal / featural assimilation at feature f: the target bundle tgt adopts whatever value src specifies for f (if any). All other features of tgt are unchanged.

This is the building block of M-lowering in Laal (@cite{lionnet-2022} §5.2): a [-raised] value spreads from a trigger bundle to a target bundle on the [raised] feature alone, leaving [upper] untouched.

Equations

• Phonology.Featural.FeatureBundle.assimilate f src tgt = Function.update tgt f (src f)

def Phonology.Featural.FeatureBundle.delete {F : Type u} {V : Type v} [DecidableEq F] (f : F) (b : FeatureBundle F V) : FeatureBundle F V

Feature deletion at f: zero out the assignment, returning to underspecified. The complement to assimilate.

Equations

• Phonology.Featural.FeatureBundle.delete f b = Function.update b f none

def Phonology.Featural.FeatureBundle.set {F : Type u} {V : Type v} [DecidableEq F] (f : F) (v : V) (b : FeatureBundle F V) : FeatureBundle F V

Bundle override: set feature f to some v, regardless of the current value. Useful for floating features that dock onto a target.

Equations

• Phonology.Featural.FeatureBundle.set f v b = Function.update b f (some v)

def Phonology.Featural.Tier.mergeAdjacent {F : Type u} {V : Type v} : Tier F V → Tier F V

Tier-level merger at adjacent positions: pairwise merge between the bundle at position i and the bundle at position i+1. This is the primitive operation behind the OCP — a constraint that drives merger of adjacent identical features.

Equations

• Phonology.Featural.Tier.mergeAdjacent [] = []
• Phonology.Featural.Tier.mergeAdjacent [b] = [b]
• Phonology.Featural.Tier.mergeAdjacent (b₁ :: b₂ :: rest) = b₁.merge b₂ :: Phonology.Featural.Tier.mergeAdjacent (b₂ :: rest)

@[irreducible]

def Phonology.Featural.Tier.assimilateLeftward {F : Type u} {V : Type v} [DecidableEq F] (f : F) : Tier F V → Tier F V

Local assimilation along a tier at feature f: each bundle takes its value at f from its left neighbour (when the left neighbour specifies f). Models leftward-trigger spreading.

Equations

• Phonology.Featural.Tier.assimilateLeftward f [] = []
• Phonology.Featural.Tier.assimilateLeftward f [b] = [b]
• Phonology.Featural.Tier.assimilateLeftward f (b₁ :: b₂ :: rest) = b₁ :: Phonology.Featural.Tier.assimilateLeftward f (Phonology.Featural.FeatureBundle.assimilate f b₁ b₂ :: rest)