Feature bundles

The representation-polymorphic interface for feature bundles, and the canonical extensional representation Features.Bundle.

A feature bundle assigns values to features. Theories disagree about what a bundle is — a list of valued features, a finite set, a partial assignment over a feature space, an attribute-value structure, a hierarchical tree whose root label is the flat bundle. They agree about what a bundle says: which features it specifies, with which values. BundleLike captures that shared observation language — a single valuation val : B → (t : F) → S t — so that specification, subsumption, and the information order are stated once and inherited by every representation.

Extensionality is deliberately not part of BundleLike: structured representations (assembly trees, feature-geometric hierarchies) can present the same valuation in distinct ways, and that multiplicity can itself carry theoretical content. Representations whose valuation is injective opt into LawfulBundleLike and get extensionality and the subsumption partial order.

All three parameters are fully general. The feature space F is data, not a built-in inventory, so per-language and per-theory feature sets are choices of F. The slot family S : F → Type* is the per-feature information space — it carries its own order, so each slot may be (a) Flat (V t) for a single atom from an enum V t (the determinate case: privative if V t := Unit, bivalent if V t := Bool, multivalent for an enum, mode-tagged products for valued/unvalued distinctions, ℚ for gradient theories); or (b) (Finset α)ᵒᵈ for indeterminate values in the sense of [DK00]; or (c) some richer order for layered or hierarchical features. The lattice theory is proved once at the Pi level and inherited by every choice of S.

Main declarations

• BundleLike — the valuation interface
• LawfulBundleLike — extensional representations; gives BundleLike.ext and BundleLike.partialOrder
• BundleLike.Specifies, BundleLike.Subsumes — the derived API; Subsumes is the subsumption order of the unification-grammar tradition ([Shi86])
• Features.Bundle F V — the canonical extensional carrier, a partial assignment (t : F) → Option (V t), carrying the subsumption PartialOrder with ⊥ the everywhere-underspecified bundle
• BundleLike.subsumptionPreorder — any representation pulls the subsumption order back along val, as a Core.Order.PullbackPreorder

Implementation notes

Features.Bundle is an abbrev over the Pi type of Flat slots (Core/Order/Flat.lean): the reducibility barrier sits at Flat, so the subsumption order does not leak onto bare Option-valued Pi types, while mathlib's Pi instances supply the whole order stack — the subsumption PartialOrder, OrderBot (⊥ = everywhere underspecified), SemilatticeInf (generalization/anti-unification), and the partial join PartialUnify (unification). This is the bounded complete partial order of the unification tradition ([Car92] Definition 2.1; "a finite BCPO is nothing more nor less than a finite meet semilattice", presented through its joins). Features.Bundle is unrelated to mathlib's fiber-bundle Bundle namespace; qualify when both are in scope.

Instances live with their carriers, not here: this file imports only Core and mathlib, and e.g. Morphology.UD.MorphFeatures instantiates BundleLike in its own file.

The phonological carrier uses Bundle directly: Phonology.Segment's spec field is Features.Bundle Feature (fun _ => Bool) (in unfolded Feature → Option Bool form), with the shared merge/set/delete algebra below.

Todo

• Instantiate BundleLike at the Minimalist FeatureBundle (lawful only after the planned list-to-assignment retype).
• Per-slot generality: Bundle fixes the flat slot order. UD-practice pressure (multivalued features as Finset-superset slots, layered features as a nested index) is accommodated by working with (t : F) → S t for other slot orders S; the PartialUnify Pi instance is already stated at that generality.
• A hierarchical assembly-tree carrier with the flattening valuation — BundleLike but not LawfulBundleLike.

class BundleLike (B : Type u_1) (F : outParam (Type u_2)) (S : outParam (F → Type u_3)) : Type (max (max u_1 u_2) u_3)

BundleLike B F S: B presents feature bundles over the feature space F, with slot t taking values in the order space S t. The single primitive is the valuation: a function reading off the slot value at each feature.

The slot type S t carries its own order. The canonical flat-atomic slot is Flat (V t) for an atom enum V t; richer slot orders (Finset α for indeterminacy in the sense of [DK00], nested attribute spaces for UD layered features) are obtained by choosing different S.

• val : B → (t : F) → S t

  The value the bundle assigns to feature t.

class LawfulBundleLike (B : Type u_1) {F : Type u_2} {S : F → Type u_3} [BundleLike B F S] : Prop

An extensional bundle representation: bundles with the same valuation are equal. Structured representations whose internal organization outruns their valuation are deliberately not lawful.

• val_injective : Function.Injective BundleLike.val

theorem BundleLike.ext {B : Type u_1} {F : Type u_2} {S : F → Type u_3} [BundleLike B F S] [LawfulBundleLike B] {b₁ b₂ : B} (h : ∀ (t : F), val b₁ t = val b₂ t) : b₁ = b₂

Extensionality for lawful representations.

theorem BundleLike.ext_iff {B : Type u_1} {F : Type u_2} {S : F → Type u_3} [BundleLike B F S] [LawfulBundleLike B] {b₁ b₂ : B} : b₁ = b₂ ↔ ∀ (t : F), val b₁ t = val b₂ t

def BundleLike.Specifies {B : Type u_1} {F : Type u_2} {S : F → Type u_3} [BundleLike B F S] [(t : F) → Bot (S t)] (b : B) (t : F) : Prop

b specifies feature t (assigns it more than the slot's bottom information). For flat slots this coincides with "the slot is some"; for richer slots (set-valued indeterminacy) it means "the slot has not been left at Finset.univ" (in the order dual where superset = less determinate). Only Bot is required; the order is not.

Equations

• BundleLike.Specifies b t = (BundleLike.val b t ≠ ⊥)

@[implicit_reducible]

instance BundleLike.instDecidableSpecifiesOfDecidableEq {B : Type u_1} {F : Type u_2} {S : F → Type u_3} [BundleLike B F S] [(t : F) → Bot (S t)] [(t : F) → DecidableEq (S t)] (b : B) (t : F) : Decidable (Specifies b t)

Equations

• BundleLike.instDecidableSpecifiesOfDecidableEq b t = BundleLike.instDecidableSpecifiesOfDecidableEq._aux_1 b t

def BundleLike.Subsumes {B : Type u_1} {F : Type u_2} {S : F → Type u_3} [BundleLike B F S] [(t : F) → PartialOrder (S t)] (b₁ b₂ : B) : Prop

Subsumption: pointwise ≤ on slots — b₂ is at least as specified as b₁ ([Shi86] §3.2.2; [Car92] Definition 2.1). For flat slots this is Option.FlatLE; for set-valued slots it is the indeterminacy order ([DK00]: superset = less determinate).

Equations

• BundleLike.Subsumes b₁ b₂ = ∀ (t : F), BundleLike.val b₁ t ≤ BundleLike.val b₂ t

theorem BundleLike.subsumes_refl {B : Type u_1} {F : Type u_2} {S : F → Type u_3} [BundleLike B F S] [(t : F) → PartialOrder (S t)] (b : B) : Subsumes b b

theorem BundleLike.subsumes_trans {B : Type u_1} {F : Type u_2} {S : F → Type u_3} [BundleLike B F S] [(t : F) → PartialOrder (S t)] {b₁ b₂ b₃ : B} (h₁₂ : Subsumes b₁ b₂) (h₂₃ : Subsumes b₂ b₃) : Subsumes b₁ b₃

theorem BundleLike.subsumes_antisymm {B : Type u_1} {F : Type u_2} {S : F → Type u_3} [BundleLike B F S] [(t : F) → PartialOrder (S t)] [LawfulBundleLike B] {b₁ b₂ : B} (h₁ : Subsumes b₁ b₂) (h₂ : Subsumes b₂ b₁) : b₁ = b₂

On a lawful representation with partial slot orders, subsumption is antisymmetric.

@[implicit_reducible]

instance BundleLike.instDecidableSubsumesOfFintypeOfDecidableLE {B : Type u_1} {F : Type u_2} {S : F → Type u_3} [BundleLike B F S] [(t : F) → PartialOrder (S t)] [Fintype F] [(t : F) → DecidableLE (S t)] (b₁ b₂ : B) : Decidable (Subsumes b₁ b₂)

Equations

• BundleLike.instDecidableSubsumesOfFintypeOfDecidableLE b₁ b₂ = BundleLike.instDecidableSubsumesOfFintypeOfDecidableLE._aux_1 b₁ b₂

@[reducible]

def BundleLike.partialOrder {B : Type u_1} {F : Type u_2} {S : F → Type u_3} [BundleLike B F S] [(t : F) → PartialOrder (S t)] [LawfulBundleLike B] : PartialOrder B

The subsumption partial order on a lawful representation. Not an instance: a representation may carry its own canonical order.

Equations

• BundleLike.partialOrder = { le := BundleLike.Subsumes, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[reducible, inline]

abbrev Features.Bundle (F : Type u) (V : F → Type v) : Type (max u v)

The canonical extensional feature bundle: a partial assignment of values to features, as a Pi type of Flat slots. Underspecification is none; at most one value per feature holds by construction. The order stack — subsumption PartialOrder, OrderBot, SemilatticeInf, PartialUnify — is inherited from the slots through mathlib's Pi instances (the reducibility barrier lives at Flat, see the module docstring).

Equations

• Features.Bundle F V = ((t : F) → Flat (V t))

@[implicit_reducible]

instance Features.Bundle.instBundleLikeFlat {F : Type u} {V : F → Type v} : BundleLike (Bundle F V) F fun (t : F) => Flat (V t)

Equations

• Features.Bundle.instBundleLikeFlat = { val := fun (b : Features.Bundle F V) => b }

instance Features.Bundle.instLawfulBundleLikeFlat {F : Type u} {V : F → Type v} : LawfulBundleLike (Bundle F V)

theorem Features.Bundle.le_iff_subsumes {F : Type u} {V : F → Type v} {b₁ b₂ : Bundle F V} : b₁ ≤ b₂ ↔ BundleLike.Subsumes b₁ b₂

The Pi subsumption order agrees with the interface-level BundleLike.Subsumes.

@[implicit_reducible]

instance Features.Bundle.instDecidableLeOfFintypeOfDecidableEq {F : Type u} {V : F → Type v} [Fintype F] [(t : F) → DecidableEq (V t)] (b₁ b₂ : Bundle F V) : Decidable (b₁ ≤ b₂)

Equations

• b₁.instDecidableLeOfFintypeOfDecidableEq b₂ = Fintype.decidableForallFintype

@[simp]

theorem Features.Bundle.val_bot {F : Type u} {V : F → Type v} (t : F) : BundleLike.val ⊥ t = none

def Features.Bundle.single {F : Type u} {V : F → Type v} [DecidableEq F] (t : F) (v : V t) : Bundle F V

The bundle specifying exactly one feature.

Equations

• Features.Bundle.single t v = Function.update ⊥ t (some v)

@[simp]

theorem Features.Bundle.val_single_self {F : Type u} {V : F → Type v} [DecidableEq F] (t : F) (v : V t) : BundleLike.val (single t v) t = some v

@[simp]

theorem Features.Bundle.val_single_of_ne {F : Type u} {V : F → Type v} [DecidableEq F] {s t : F} (h : s ≠ t) (v : V t) : BundleLike.val (single t v) s = none

@[simp]

theorem Features.Bundle.not_specifies_bot {F : Type u} {V : F → Type v} (t : F) : ¬BundleLike.Specifies ⊥ t

@[simp]

theorem Features.Bundle.specifies_single {F : Type u} {V : F → Type v} [DecidableEq F] {s t : F} (v : V t) : BundleLike.Specifies (single t v) s ↔ s = t

Mutation algebra

Function.update/orElse-based operations for building and combining bundles, dual to the order/lattice stack above. General over any Bundle F V; the phonological Segment and tonal TRN specialize them at V := fun _ => Bool.

def Features.Bundle.merge {F : Type u} {V : F → Type v} (b₁ b₂ : Bundle F V) : Bundle F V

Override merge: take b₁'s value where specified, else b₂'s.

Equations

• b₁.merge b₂ t = match b₁ t with | some v => some v | none => b₂ t

@[simp]

theorem Features.Bundle.merge_self {F : Type u} {V : F → Type v} (b : Bundle F V) : b.merge b = b

def Features.Bundle.set {F : Type u} {V : F → Type v} [DecidableEq F] (t : F) (v : V t) (b : Bundle F V) : Bundle F V

Override: set feature t to some v, regardless of current value.

Equations

• Features.Bundle.set t v b = Function.update b t (some v)

def Features.Bundle.delete {F : Type u} {V : F → Type v} [DecidableEq F] (t : F) (b : Bundle F V) : Bundle F V

Deletion: return feature t to underspecified (none).

Equations

• Features.Bundle.delete t b = Function.update b t none

def Features.Bundle.assimilate {F : Type u} {V : F → Type v} [DecidableEq F] (t : F) (src tgt : Bundle F V) : Bundle F V

Single-feature assimilation: tgt adopts src's value at t, leaving every other feature untouched.

Equations

• Features.Bundle.assimilate t src tgt = Function.update tgt t (src t)

def BundleLike.subsumptionPreorder {B : Type u_1} {F : Type u_2} {S : F → Type u_3} [BundleLike B F S] [Fintype F] [(t : F) → PartialOrder (S t)] [(t : F) → DecidableLE (S t)] : Core.Order.PullbackPreorder B ((t : F) → S t)

Any bundle representation with a finite signature carries the subsumption order pulled back along its valuation into the Pi (t : F) → S t, packaged as a Core.Order.PullbackPreorder. Coarsenings between representations factor through Core.Order.PullbackPreorder.coarsen_via_monotone. A def, not an instance, matching PullbackPreorder's own convention.

Equations

• BundleLike.subsumptionPreorder = Core.Order.PullbackPreorder.ofProj (fun (b : B) => BundleLike.val b) fun (a a' : B) => Fintype.decidableForallFintype