Feature geometry

A feature geometry over a feature type F is a finite rooted tree of class nodes with each feature attached below at most one node: dominance is ≤, the root is ⊥, every principal downset is a chain, and the natural class of a node is the finite set of features it dominates, so natural classes are nested along dominance and disjoint across incomparable nodes. The class-node idea and the thesis that assimilation spreads one node are Clements's; Halle, Vaux and Wolfe record that no consensus exists among the later revisions and lets rules spread any set of terminals, and Padgett drops constituency altogether and lets constraints refer to classes as sets, which is how current analyses use them (Brown and Meyer's AGREE[place]). The class-set is therefore the primitive: spreading a class from src onto tgt is Finset.piecewise, agreement on a class is Set.EqOn, and a geometry is an instance naming which sets are natural. The feature type is a parameter, so an instance may range over a binary inventory, over feature tokens indexed by position as in Vowel-Place Theory, over privative elements, or over tone features; the flat segmental classes are Phonology/Segmental/FeatureClass.lean, and the trees of Clements, Sagey and Halle, Vaux and Wolfe are instances in their studies.

Main definitions

• FeatureGeometry — the class: isChain_Iic (principal downsets are chains) and node (each feature's class node, if the geometry places it).
• FeatureGeometry.naturalClass — the features a node dominates.

Main results

• naturalClass_anti, disjoint_naturalClass — natural classes shrink along dominance and are disjoint across incomparable nodes.
• eqOn_piecewise_of_le, eqOn_piecewise_of_not_le — spreading a node carries every class it dominates and leaves every incomparable class untouched.
• mem_naturalClass_bot — the root's class is every attached feature: total assimilation.

Implementation notes

The feature type is an outParam: a node type determines its features. Instances build dominance from a parent function: up n is n with its ancestors, PartialOrder.lift up is dominance, the root is ⊥, and the chain axiom is decided. node is Option-valued so a geometry may leave features unplaced. Spreading an arbitrary set of terminals (Halle, Vaux and Wolfe's partial spreading, Padgett's partial class behaviour) is Finset.piecewise on that set with no further apparatus, and single-feature spreading is Features.Bundle.assimilate (Finset.piecewise_singleton). The linking of a spread node to several anchors is the tier-association object AR (Autosegmental/AR.lean), not recorded on feature bundles.

References

• [G. N. Clements, The Geometry of Phonological Features (1985)][clements-1985]
• [M. Halle, B. Vaux and A. Wolfe, On Feature Spreading and the Representation of Place of Articulation (2000)][halle-vaux-wolfe-2000]
• [J. Padgett, Feature Classes in Phonology (2002)][padgett-2002]
• [J. Brown and J. Meyer, Assimilation and Morpheme Boundaries in Mgira (2024)][brown-meyer-2024]
• [E. C. Sagey, The Representation of Features and Relations in Non-Linear Phonology (1986)][sagey-1986]

class Phonology.FeatureGeometry (F : outParam (Type u_1)) (N : Type u_2) [PartialOrder N] [OrderBot N] : Type (max u_1 u_2)

A feature geometry over the features F: a finite rooted tree of class nodes — dominance ≤, root ⊥, every principal downset a chain — with each feature attached below at most one node.

• isChain_Iic (c : N) : IsChain (fun (x1 x2 : N) => x1 ≤ x2) (Set.Iic c)

  Every principal downset is a chain: the nodes dominating a node are linearly ordered.

• node : F → Option N

  The class node a feature hangs from, if the geometry places it.

Natural classes

def Phonology.FeatureGeometry.naturalClass {F : Type u_1} {N : Type u_2} [PartialOrder N] [OrderBot N] [FeatureGeometry F N] [DecidableLE N] [Fintype F] (a : N) : Finset F

The natural class of a node: the features attached at or below it.

Equations

• Phonology.FeatureGeometry.naturalClass a = {f : F | ∃ m ∈ Phonology.FeatureGeometry.node f, a ≤ m}

theorem Phonology.FeatureGeometry.mem_naturalClass {F : Type u_1} {N : Type u_2} [PartialOrder N] [OrderBot N] [FeatureGeometry F N] [DecidableLE N] [Fintype F] {a : N} {f : F} : f ∈ naturalClass a ↔ ∃ m ∈ node f, a ≤ m

theorem Phonology.FeatureGeometry.mem_naturalClass_bot {F : Type u_1} {N : Type u_2} [PartialOrder N] [OrderBot N] [FeatureGeometry F N] [DecidableLE N] [Fintype F] {f : F} : f ∈ naturalClass ⊥ ↔ (node f).isSome = true

The root's class is every attached feature: spreading it is total assimilation.

theorem Phonology.FeatureGeometry.naturalClass_anti {F : Type u_1} {N : Type u_2} [PartialOrder N] [OrderBot N] [FeatureGeometry F N] [DecidableLE N] [Fintype F] {a b : N} (h : a ≤ b) : naturalClass b ⊆ naturalClass a

Natural classes shrink along dominance.

theorem Phonology.FeatureGeometry.disjoint_naturalClass {F : Type u_1} {N : Type u_2} [PartialOrder N] [OrderBot N] [FeatureGeometry F N] [DecidableLE N] [Fintype F] {a b : N} (h₁ : ¬a ≤ b) (h₂ : ¬b ≤ a) : Disjoint (naturalClass a) (naturalClass b)

Incomparable nodes have disjoint natural classes.

Spreading

theorem Phonology.FeatureGeometry.eqOn_piecewise_of_le {F : Type u_1} {N : Type u_2} [PartialOrder N] [OrderBot N] [FeatureGeometry F N] [DecidableLE N] [Fintype F] {a b : N} [DecidableEq F] {β : Type u_3} (src tgt : F → β) (h : a ≤ b) : Set.EqOn ((naturalClass a).piecewise src tgt) src ↑(naturalClass b)

Spreading node a from src onto tgt carries every class a dominates.

theorem Phonology.FeatureGeometry.eqOn_piecewise_of_not_le {F : Type u_1} {N : Type u_2} [PartialOrder N] [OrderBot N] [FeatureGeometry F N] [DecidableLE N] [Fintype F] {a b : N} [DecidableEq F] {β : Type u_3} (src tgt : F → β) (h₁ : ¬a ≤ b) (h₂ : ¬b ≤ a) : Set.EqOn ((naturalClass a).piecewise src tgt) tgt ↑(naturalClass b)

Spreading node a leaves every class incomparable with a untouched.

@[instance_reducible]

instance Phonology.FeatureGeometry.instDecidableEqOnCoeFinsetNaturalClassOfDecidableEq {F : Type u_1} {N : Type u_2} [PartialOrder N] [OrderBot N] [FeatureGeometry F N] [DecidableLE N] [Fintype F] [DecidableEq F] {β : Type u_3} [DecidableEq β] (s₁ s₂ : F → β) (a : N) : Decidable (Set.EqOn s₁ s₂ ↑(naturalClass a))

Equations

• Phonology.FeatureGeometry.instDecidableEqOnCoeFinsetNaturalClassOfDecidableEq s₁ s₂ a = Set.decidableEqOnOfFintype s₁ s₂ ↑(Phonology.FeatureGeometry.naturalClass a)