Phonological Features

Complete segmental feature inventory following @cite{hayes-2009} Introductory Phonology, Ch 4. The 26 binary features are organized into manner (root), laryngeal, and place (labial, coronal, dorsal) categories.

Prosodic features [stress] and [long] are excluded — Hayes treats stress as a syllable-level property (Ch 14), not a segmental feature.

This module provides the feature inventory consumed by OT, autosegmental, and syllable analyses.

@cite{hayes-2009}

inductive Phonology.Feature : Type

Distinctive phonological features (binary-valued).

Complete segmental inventory from @cite{hayes-2009}:

• Manner (root): syllabic, consonantal, sonorant, approximant, continuant, delayedRelease, nasal, lateral, strident, tap, trill
• Laryngeal: voice, spreadGlottis, constrGlottis
• Place (Labial): labial, round, labiodental
• Place (Coronal): coronal, anterior, distributed
• Place (Dorsal): dorsal, high, low, front, back, tense

Note: The grouping above follows Hayes's flat classification. The hierarchical feature geometry (FeatureGeometry.lean) re-maps some of these features to different nodes: [nasal] → soft palate, [continuant] → supralaryngeal, [lateral]/[strident] → coronal. The flat isMajorClass predicate has no single geometric counterpart — see subsumption theorems in FeatureGeometry.lean §6.

The sonority hierarchy (Hayes Table 4.1) is decomposed as: [±sonorant] > [±approximant] > [±consonantal] > [±syllabic], yielding 5 natural classes (obstruent, nasal, liquid, glide, vowel).

• syllabic : Feature
• consonantal : Feature
• sonorant : Feature
• approximant : Feature
• continuant : Feature
• delayedRelease : Feature
• nasal : Feature
• lateral : Feature
• strident : Feature
• tap : Feature
• trill : Feature
• voice : Feature
• spreadGlottis : Feature
• constrGlottis : Feature
• labial : Feature
• round : Feature
• labiodental : Feature
• coronal : Feature
• anterior : Feature
• distributed : Feature
• dorsal : Feature
• high : Feature
• low : Feature
• front : Feature
• back : Feature
• tense : Feature

@[implicit_reducible]

instance Phonology.instDecidableEqFeature : DecidableEq Feature

Equations

• Phonology.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phonology.instReprFeature.repr : Feature → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Phonology.instReprFeature.repr Phonology.Feature.syllabic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.syllabic")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.sonorant prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.sonorant")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.nasal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.nasal")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.lateral prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.lateral")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.strident prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.strident")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.tap prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.tap")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.trill prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.trill")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.voice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.voice")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.labial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.labial")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.round prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.round")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.coronal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.coronal")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.anterior prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.anterior")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.dorsal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.dorsal")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.high prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.high")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.low prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.low")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.front prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.front")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.back prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.back")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.tense prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.tense")).group prec✝

@[implicit_reducible]

instance Phonology.instReprFeature : Repr Feature

Equations

• Phonology.instReprFeature = { reprPrec := Phonology.instReprFeature.repr }

@[reducible, inline]

abbrev Phonology.FeatureVal : Type

A feature value: some true = [+F], some false = [−F], none = unspecified.

Equations

• Phonology.FeatureVal = Option Bool

def Phonology.Feature.IsMajorClass : Feature → Prop

Is this a manner / root feature?

Equations

• Phonology.Feature.syllabic.IsMajorClass = True
• Phonology.Feature.consonantal.IsMajorClass = True
• Phonology.Feature.sonorant.IsMajorClass = True
• Phonology.Feature.approximant.IsMajorClass = True
• Phonology.Feature.continuant.IsMajorClass = True
• Phonology.Feature.delayedRelease.IsMajorClass = True
• Phonology.Feature.nasal.IsMajorClass = True
• Phonology.Feature.lateral.IsMajorClass = True
• Phonology.Feature.strident.IsMajorClass = True
• Phonology.Feature.tap.IsMajorClass = True
• Phonology.Feature.trill.IsMajorClass = True
• x✝.IsMajorClass = False

@[implicit_reducible]

instance Phonology.instDecidablePredFeatureIsMajorClass : DecidablePred Feature.IsMajorClass

Equations

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

def Phonology.Feature.IsLaryngeal : Feature → Prop

Is this a laryngeal feature?

Equations

• Phonology.Feature.voice.IsLaryngeal = True
• Phonology.Feature.spreadGlottis.IsLaryngeal = True
• Phonology.Feature.constrGlottis.IsLaryngeal = True
• x✝.IsLaryngeal = False

@[implicit_reducible]

instance Phonology.instDecidablePredFeatureIsLaryngeal : DecidablePred Feature.IsLaryngeal

Equations

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

def Phonology.Feature.IsPlace : Feature → Prop

Is this a place feature (any articulator node)?

Equations

• Phonology.Feature.labial.IsPlace = True
• Phonology.Feature.round.IsPlace = True
• Phonology.Feature.labiodental.IsPlace = True
• Phonology.Feature.coronal.IsPlace = True
• Phonology.Feature.anterior.IsPlace = True
• Phonology.Feature.distributed.IsPlace = True
• Phonology.Feature.dorsal.IsPlace = True
• Phonology.Feature.high.IsPlace = True
• Phonology.Feature.low.IsPlace = True
• Phonology.Feature.front.IsPlace = True
• Phonology.Feature.back.IsPlace = True
• Phonology.Feature.tense.IsPlace = True
• x✝.IsPlace = False

@[implicit_reducible]

instance Phonology.instDecidablePredFeatureIsPlace : DecidablePred Feature.IsPlace

Equations

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

def Phonology.Feature.IsLabial : Feature → Prop

Is this a labial place feature?

Equations

• Phonology.Feature.labial.IsLabial = True
• Phonology.Feature.round.IsLabial = True
• Phonology.Feature.labiodental.IsLabial = True
• x✝.IsLabial = False

@[implicit_reducible]

instance Phonology.instDecidablePredFeatureIsLabial : DecidablePred Feature.IsLabial

Equations

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

def Phonology.Feature.IsCoronal : Feature → Prop

Is this a coronal place feature?

Equations

• Phonology.Feature.coronal.IsCoronal = True
• Phonology.Feature.anterior.IsCoronal = True
• Phonology.Feature.distributed.IsCoronal = True
• x✝.IsCoronal = False

@[implicit_reducible]

instance Phonology.instDecidablePredFeatureIsCoronal : DecidablePred Feature.IsCoronal

Equations

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

def Phonology.Feature.IsDorsal : Feature → Prop

Is this a dorsal place feature?

Equations

• Phonology.Feature.dorsal.IsDorsal = True
• Phonology.Feature.high.IsDorsal = True
• Phonology.Feature.low.IsDorsal = True
• Phonology.Feature.front.IsDorsal = True
• Phonology.Feature.back.IsDorsal = True
• Phonology.Feature.tense.IsDorsal = True
• x✝.IsDorsal = False

@[implicit_reducible]

instance Phonology.instDecidablePredFeatureIsDorsal : DecidablePred Feature.IsDorsal

Equations

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

structure Phonology.Segment : Type

A segment represented as a (partial) specification of features. Unspecified features return none.

• spec : Feature → FeatureVal

def Phonology.Segment.Specified (s : Segment) (f : Feature) : Prop

Is feature f specified (either [+F] or [−F])?

Equations

• s.Specified f = (Option.isSome (s.spec f) = true)

@[implicit_reducible]

instance Phonology.instDecidablePredFeatureSpecified (s : Segment) : DecidablePred s.Specified

Equations

• Phonology.instDecidablePredFeatureSpecified s x✝ = Phonology.instDecidablePredFeatureSpecified._aux_1 s x✝

def Phonology.Segment.HasValue (s : Segment) (f : Feature) (v : Bool) : Prop

Does feature f have value v?

Equations

• s.HasValue f v = (s.spec f = some v)

@[implicit_reducible]

instance Phonology.instDecidableHasValue (s : Segment) (f : Feature) (v : Bool) : Decidable (s.HasValue f v)

Equations

• Phonology.instDecidableHasValue s f v = Phonology.instDecidableHasValue._aux_1 s f v

def Phonology.Feature.allFeatures : List Feature

All 26 features in declaration order.

Equations

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

theorem Phonology.allFeatures_length : Feature.allFeatures.length = 26

theorem Phonology.allFeatures_complete (f : Feature) : f ∈ Feature.allFeatures

Every Feature constructor appears in allFeatures.

@[implicit_reducible]

instance Phonology.instBEqSegment : BEq Segment

Segment equality by checking all 26 features. Two segments are BEq-equal iff they agree on every feature value.

Equations

• Phonology.instBEqSegment = { beq := fun (s1 s2 : Phonology.Segment) => Phonology.Feature.allFeatures.all fun (f : Phonology.Feature) => s1.spec f == s2.spec f }

@[implicit_reducible]

instance Phonology.instDecidableEqSegment : DecidableEq Segment

Decidable equality on segments via exhaustive feature comparison. Enables decide on segment-level goals and OT tableaux over List Segment candidates.

Equations

• Phonology.instDecidableEqSegment s1 s2 = if h : (Phonology.Feature.allFeatures.all fun (f : Phonology.Feature) => s1.spec f == s2.spec f) = true then isTrue ⋯ else isFalse ⋯

def Phonology.Segment.ofSpecs (specs : List (Feature × Bool)) : Segment

Build a segment from a list of (feature, value) pairs. Unmentioned features are unspecified (none), giving natural-class semantics: ofSpecs [(continuant, false)] matches all [-cont] segments.

Equations

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

def Phonology.Segment.matchesPattern (s p : Segment) : Bool

Bool: does segment s match natural-class pattern p? True when every feature specified in p agrees with s; unspecified features in p match anything.

Equations

• s.matchesPattern p = Phonology.Feature.allFeatures.all fun (f : Phonology.Feature) => match p.spec f with | none => true | some v => s.spec f == some v

def Phonology.Segment.MatchesPattern (s p : Segment) : Prop

Prop wrapper around matchesPattern (mirrors Segment.HasValue from § 3). Lets consumers write mathlib-style universally-quantified theorems with Decidable inference via the Bool computation.

Equations

• s.MatchesPattern p = (s.matchesPattern p = true)

@[implicit_reducible]

instance Phonology.instDecidableMatchesPattern (s p : Segment) : Decidable (s.MatchesPattern p)

Equations

• Phonology.instDecidableMatchesPattern s p = Phonology.instDecidableMatchesPattern._aux_1 s p

def Phonology.Segment.applyChanges (s change : Segment) : Segment

Merge feature changes from change into s: features specified in change override s's values; unspecified features in change are preserved. Implements the SPE structural change A → B when B is a partial feature bundle.

Equations

• s.applyChanges change = { spec := fun (f : Phonology.Feature) => match change.spec f with | some v => some v | none => s.spec f }

theorem Phonology.Segment.ext {s t : Segment} (h : ∀ (f : Feature), s.spec f = t.spec f) : s = t

Two segments are equal iff their spec functions agree on every feature.

theorem Phonology.Segment.ext_iff {s t : Segment} : s = t ↔ ∀ (f : Feature), s.spec f = t.spec f

@[simp]

theorem Phonology.Segment.matchesPattern_self (s : Segment) : s.matchesPattern s = true

Every segment matches itself as a pattern.

@[simp]

theorem Phonology.Segment.applyChanges_ofSpecs_nil (s : Segment) : s.applyChanges (ofSpecs []) = s

Applying the empty change list is the identity.

@[simp]

theorem Phonology.Segment.applyChanges_idem (s change : Segment) : (s.applyChanges change).applyChanges change = s.applyChanges change

Applying the same change twice equals applying it once.