Segmental representation: definitions

The distinctive feature and the segment built over it. A feature is one of the 26 binary distinctive features of [Hay09]; a segment is a partial specification of those features — each +, −, or unspecified — ordered by specificity (the unification-grammar subsumption order, inherited as a feature bundle), with the unspecified archisegment least and natural-class generalization as meet.

This file collects definitions only — the feature inventory, the segment and its valuation/construction/change API, the natural-class predicates, and the sonority scales. The theorems about them live in Phonology/Segmental/Basic.lean.

Feature inventory

inductive Phonology.Feature : Type

A binary distinctive phonological feature, following [Hay09]'s segmental inventory. (The stress and length features are excluded: [Hay09] treats stress as a syllable-level property, not a segmental feature.)

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

@[implicit_reducible]

instance Phonology.instReprFeature : Repr Feature

Equations

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

def Phonology.instReprFeature.repr : Feature → ℕ → 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✝

Feature classification

inductive Phonology.Feature.Category : Type

The articulator category of a feature: manner/root, laryngeal, or place.

• manner : Category
• laryngeal : Category
• labial : Category
• coronal : Category
• dorsal : Category

@[implicit_reducible]

instance Phonology.Feature.instDecidableEqCategory : DecidableEq Category

Equations

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

@[implicit_reducible]

instance Phonology.Feature.instReprCategory : Repr Category

Equations

• Phonology.Feature.instReprCategory = { reprPrec := Phonology.Feature.instReprCategory.repr }

def Phonology.Feature.instReprCategory.repr : Category → ℕ → Std.Format

Equations

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

def Phonology.Feature.category : Feature → Category

The articulator category of each distinctive feature.

Equations

• Phonology.Feature.syllabic.category = Phonology.Feature.Category.manner
• Phonology.Feature.consonantal.category = Phonology.Feature.Category.manner
• Phonology.Feature.sonorant.category = Phonology.Feature.Category.manner
• Phonology.Feature.approximant.category = Phonology.Feature.Category.manner
• Phonology.Feature.continuant.category = Phonology.Feature.Category.manner
• Phonology.Feature.delayedRelease.category = Phonology.Feature.Category.manner
• Phonology.Feature.nasal.category = Phonology.Feature.Category.manner
• Phonology.Feature.lateral.category = Phonology.Feature.Category.manner
• Phonology.Feature.strident.category = Phonology.Feature.Category.manner
• Phonology.Feature.tap.category = Phonology.Feature.Category.manner
• Phonology.Feature.trill.category = Phonology.Feature.Category.manner
• Phonology.Feature.voice.category = Phonology.Feature.Category.laryngeal
• Phonology.Feature.spreadGlottis.category = Phonology.Feature.Category.laryngeal
• Phonology.Feature.constrGlottis.category = Phonology.Feature.Category.laryngeal
• Phonology.Feature.labial.category = Phonology.Feature.Category.labial
• Phonology.Feature.round.category = Phonology.Feature.Category.labial
• Phonology.Feature.labiodental.category = Phonology.Feature.Category.labial
• Phonology.Feature.coronal.category = Phonology.Feature.Category.coronal
• Phonology.Feature.anterior.category = Phonology.Feature.Category.coronal
• Phonology.Feature.distributed.category = Phonology.Feature.Category.coronal
• Phonology.Feature.dorsal.category = Phonology.Feature.Category.dorsal
• Phonology.Feature.high.category = Phonology.Feature.Category.dorsal
• Phonology.Feature.low.category = Phonology.Feature.Category.dorsal
• Phonology.Feature.front.category = Phonology.Feature.Category.dorsal
• Phonology.Feature.back.category = Phonology.Feature.Category.dorsal
• Phonology.Feature.tense.category = Phonology.Feature.Category.dorsal

@[reducible, inline]

abbrev Phonology.Feature.IsLaryngeal (f : Feature) : Prop

Is this a laryngeal feature?

Equations

• f.IsLaryngeal = (f.category = Phonology.Feature.Category.laryngeal)

@[reducible, inline]

abbrev Phonology.Feature.IsDorsal (f : Feature) : Prop

Is this a dorsal place feature?

Equations

• f.IsDorsal = (f.category = Phonology.Feature.Category.dorsal)

@[reducible, inline]

abbrev Phonology.Feature.IsPlace (f : Feature) : Prop

Is this a place feature (any articulator node)?

Equations

• f.IsPlace = (f.category = Phonology.Feature.Category.labial ∨ f.category = Phonology.Feature.Category.coronal ∨ f.category = Phonology.Feature.Category.dorsal)

Enumeration

def Phonology.Feature.allFeatures : List Feature

All features, in declaration order.

Equations

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

@[implicit_reducible]

instance Phonology.Feature.instFintype : Fintype Feature

allFeatures is the canonical enumeration: completeness is the Fintype law, not a theorem re-proved beside it.

Equations

• Phonology.Feature.instFintype = { elems := { val := ↑Phonology.Feature.allFeatures, nodup := Phonology.Feature.instFintype._proof_1 }, complete := Phonology.Feature.instFintype._proof_2 }

The segment bundle

@[reducible, inline]

abbrev Phonology.Segment : Type

A segment: a partial specification of the distinctive features — each feature is +, −, or left unspecified. Segments are ordered by specificity: one refines another when it agrees on every feature the other commits to, and possibly more. The fully unspecified segment is least; the most specific class common to two segments is their meet.

Equations

• Phonology.Segment = (Phonology.Feature → Flat Bool)

Valuation

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

Does feature f have value v?

Equations

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

@[implicit_reducible]

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

Equations

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

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

A segment is unspecified for feature f iff its value there is none.

Equations

• s.Unspecified f = (s f = none)

@[implicit_reducible]

instance Phonology.Segment.instDecidableUnspecified (s : Segment) (f : Feature) : Decidable (s.Unspecified f)

Equations

• s.instDecidableUnspecified f = Phonology.Segment.instDecidableUnspecified._aux_1 s f

Construction

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

• Phonology.Segment.ofSpecs specs f = match List.find? (fun (p : Phonology.Feature × Bool) => p.1 == f) specs with | some (fst, v) => some v | none => none

Natural-class predicates

Language-neutral natural-class membership predicates, by the SPE feature decompositions standard since [CH68] and codified in textbook form by [Hay09]. Pure substrate: they project information already encoded in a segment, consumed by per-language Fragment files rather than redefined locally.

def Phonology.Segment.IsVowel (s : Segment) : Prop

A segment is a vowel iff it is [+syllabic].

Equations

• s.IsVowel = s.HasValue Phonology.Feature.syllabic true

@[implicit_reducible]

instance Phonology.Segment.instDecidableIsVowel (s : Segment) : Decidable s.IsVowel

Equations

• s.instDecidableIsVowel = id inferInstance

def Phonology.Segment.IsConsonant (s : Segment) : Prop

A segment is a consonant iff it is [+consonantal].

Equations

• s.IsConsonant = s.HasValue Phonology.Feature.consonantal true

@[implicit_reducible]

instance Phonology.Segment.instDecidableIsConsonant (s : Segment) : Decidable s.IsConsonant

Equations

• s.instDecidableIsConsonant = id inferInstance

def Phonology.Segment.IsStop (s : Segment) : Prop

A segment is an oral stop iff it is [+cons, -son, -cont].

Equations

• s.IsStop = (s.HasValue Phonology.Feature.consonantal true ∧ s.HasValue Phonology.Feature.sonorant false ∧ s.HasValue Phonology.Feature.continuant false)

@[implicit_reducible]

instance Phonology.Segment.instDecidableIsStop (s : Segment) : Decidable s.IsStop

Equations

• s.instDecidableIsStop = id inferInstance

def Phonology.Segment.IsFricative (s : Segment) : Prop

A segment is a fricative iff it is [+cons, -son, +cont].

Equations

• s.IsFricative = (s.HasValue Phonology.Feature.consonantal true ∧ s.HasValue Phonology.Feature.sonorant false ∧ s.HasValue Phonology.Feature.continuant true)

@[implicit_reducible]

instance Phonology.Segment.instDecidableIsFricative (s : Segment) : Decidable s.IsFricative

Equations

• s.instDecidableIsFricative = id inferInstance

def Phonology.Segment.IsNasal (s : Segment) : Prop

A segment is a nasal iff it is [+nasal].

Equations

• s.IsNasal = s.HasValue Phonology.Feature.nasal true

@[implicit_reducible]

instance Phonology.Segment.instDecidableIsNasal (s : Segment) : Decidable s.IsNasal

Equations

• s.instDecidableIsNasal = id inferInstance

def Phonology.Segment.IsLiquid (s : Segment) : Prop

A segment is a liquid iff it is [+cons, +son] and one of [+lateral], [+trill], [+tap] — the lateral /l/, the trill /r/, and the flap /ɾ/ under one class.

Equations

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

@[implicit_reducible]

instance Phonology.Segment.instDecidableIsLiquid (s : Segment) : Decidable s.IsLiquid

Equations

• s.instDecidableIsLiquid = id inferInstance

def Phonology.Segment.IsGlide (s : Segment) : Prop

A segment is a glide iff it is [-cons, -syllabic, +approximant].

Equations

• s.IsGlide = (s.HasValue Phonology.Feature.consonantal false ∧ s.HasValue Phonology.Feature.syllabic false ∧ s.HasValue Phonology.Feature.approximant true)

@[implicit_reducible]

instance Phonology.Segment.instDecidableIsGlide (s : Segment) : Decidable s.IsGlide

Equations

• s.instDecidableIsGlide = id inferInstance

Feature changes

The segment-level operations are thin lifts of the shared Features.Bundle algebra. Three-valued (+ / − / ∅) specification is standard in [Kea88], [IO95], and [Ste95]; fillFromContext is default-fill, preserving existing values per [Kip82] [Arc88], while setFeature overrides. The Latin coda /l/ analysis in [Sen15] is a worked example.

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

Set feature f to value v, overriding any existing specification (the Features.Bundle.set slot operation). For default-fill semantics that only assign when f is currently unspecified, use fillFromContext.

Equations

• s.setFeature f v = Features.Bundle.set f v s

def Phonology.Segment.fillFromContext (s : Segment) (f : Feature) (ctx : Segment) : Segment

Categorical feature spreading from context: the target s, when unspecified for f, takes the f-value of ctx; already-specified targets and features other than f are untouched. When ctx is itself unspecified for f, the target stays unspecified.

This is a [Kea88] context rule: the target acquires a categorical feature value from its neighbour and that value blocks further interactions. It is distinct from her gradient phonetic interpolation (her unspecified /h/ example), in which an unspecified segment stays unspecified and the phonetics builds a continuous trajectory through it; gradient phonetic interpolation is out of scope at this categorical-featural substrate.

Equations

• s.fillFromContext f ctx = Features.Bundle.merge s (Function.update ⊥ f (ctx f))

Sonority

inductive Phonology.Sonority : Type

The abstract sonority hierarchy ([Cle90]): what the synchronic grammar operates on, ordering segments from least to most sonorous.

Rank	Class
0	Stop
1	Fricative
2	Nasal
3	Liquid
4	Glide
5	Vowel

For the finer 8-level scale that splits obstruents by voice, see Sonority.Class.

• stop : Sonority
• fricative : Sonority
• nasal : Sonority
• liquid : Sonority
• glide : Sonority
• vowel : Sonority

@[implicit_reducible]

instance Phonology.instDecidableEqSonority : DecidableEq Sonority

Equations

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

def Phonology.instReprSonority.repr : Sonority → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Phonology.instReprSonority.repr Phonology.Sonority.stop prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Sonority.stop")).group prec✝
• Phonology.instReprSonority.repr Phonology.Sonority.nasal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Sonority.nasal")).group prec✝
• Phonology.instReprSonority.repr Phonology.Sonority.liquid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Sonority.liquid")).group prec✝
• Phonology.instReprSonority.repr Phonology.Sonority.glide prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Sonority.glide")).group prec✝
• Phonology.instReprSonority.repr Phonology.Sonority.vowel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Sonority.vowel")).group prec✝

@[implicit_reducible]

instance Phonology.instReprSonority : Repr Sonority

Equations

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

def Phonology.Sonority.rank : Sonority → ℕ

Numeric rank (0 = least sonorous).

Equations

• Phonology.Sonority.stop.rank = 0
• Phonology.Sonority.fricative.rank = 1
• Phonology.Sonority.nasal.rank = 2
• Phonology.Sonority.liquid.rank = 3
• Phonology.Sonority.glide.rank = 4
• Phonology.Sonority.vowel.rank = 5

@[implicit_reducible]

instance Phonology.Sonority.instLinearOrder : LinearOrder Sonority

Equations

• Phonology.Sonority.instLinearOrder = LinearOrder.lift' Phonology.Sonority.rank Phonology.Sonority.instLinearOrder._proof_1

def Phonology.Sonority.ofSegment (s : Segment) : Sonority

The sonority of a segment, read off its features ([Hay09], [Cle90]).

Equations

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

The Parker sonority scale

inductive Phonology.Sonority.Class : Type

The 8-level Parker sonority partition ([Par02]) — a refinement of Sonority that splits obstruents by [±continuant] and [±voice]. This is the sonority scale; it is distinct from the natural-class predicates above (Segment.IsVowel &c.), which are feature membership.

Crucially [Par02] ranks voiced stops above voiceless fricatives (vds = 3 > vlf = 2) — his intensity-based default universal, reversible in particular languages. The finer granularity is needed for sonority-conditioned gradient phenomena such as Tarifit intrusive vowels ([AZ25b]).

• vls : Class
• vds : Class
• vlf : Class
• vdf : Class
• nasal : Class
• liquid : Class
• glide : Class
• vowel : Class

@[implicit_reducible]

instance Phonology.Sonority.instDecidableEqClass : DecidableEq Class

Equations

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

@[implicit_reducible]

instance Phonology.Sonority.instReprClass : Repr Class

Equations

• Phonology.Sonority.instReprClass = { reprPrec := Phonology.Sonority.instReprClass.repr }

def Phonology.Sonority.instReprClass.repr : Class → ℕ → Std.Format

Equations

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

def Phonology.Sonority.Class.parkerRank : Class → ℕ

Parker's default universal 8-level ranking ([Par02]): voiced stops (vds = 3) outrank voiceless fricatives (vlf = 2).

Equations

• Phonology.Sonority.Class.vls.parkerRank = 1
• Phonology.Sonority.Class.vlf.parkerRank = 2
• Phonology.Sonority.Class.vds.parkerRank = 3
• Phonology.Sonority.Class.vdf.parkerRank = 4
• Phonology.Sonority.Class.nasal.parkerRank = 5
• Phonology.Sonority.Class.liquid.parkerRank = 6
• Phonology.Sonority.Class.glide.parkerRank = 7
• Phonology.Sonority.Class.vowel.parkerRank = 8

def Phonology.Sonority.Class.ofSegment (s : Segment) : Class

Classify a segment on the Parker 8-level scale: as Sonority.ofSegment, but additionally splitting obstruents by [±voice] ([Par02]).

Equations

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

def Phonology.Sonority.Class.toSonority : Class → Sonority

Coarsen to the substance-free Sonority, collapsing the voicing split.

Equations

• Phonology.Sonority.Class.vls.toSonority = Phonology.Sonority.stop
• Phonology.Sonority.Class.vds.toSonority = Phonology.Sonority.stop
• Phonology.Sonority.Class.vlf.toSonority = Phonology.Sonority.fricative
• Phonology.Sonority.Class.vdf.toSonority = Phonology.Sonority.fricative
• Phonology.Sonority.Class.nasal.toSonority = Phonology.Sonority.nasal
• Phonology.Sonority.Class.liquid.toSonority = Phonology.Sonority.liquid
• Phonology.Sonority.Class.glide.toSonority = Phonology.Sonority.glide
• Phonology.Sonority.Class.vowel.toSonority = Phonology.Sonority.vowel