Segmental representation: definitions

The distinctive feature and the segment built over it. A feature is one of the 26 binary distinctive features of Hayes's chart, or one of the tongue-root features [ATR] and [RTR] of Halle, Vaux and Wolfe; 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.

References

• [Hay09]
• [HVW00]
• [CH68]
• [Cle90]
• [Par02]
• [Kea88]
• [Arc88]
• [Kip82]
• [IO95]
• [Ste95]
• [Sen15]
• [AZ25b]

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.) [ATR], the tongue-root feature of the sub-Saharan harmony systems, is the one feature [Hay09] names among the vowel features but leaves off his chart, noting that whether it is the same feature as [tense] is unsettled; it is kept distinct here. [RTR], the other tongue-root feature of [HVW00], distinguishes the pharyngealized consonants, which the PHOIBLE chart codes by it.

• 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
• atr : Feature
• rtr : Feature

@[instance_reducible]

instance Phonology.instDecidableEqFeature : DecidableEq Feature

Equations

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

@[instance_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✝
• Phonology.instReprFeature.repr Phonology.Feature.atr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.atr")).group prec✝
• Phonology.instReprFeature.repr Phonology.Feature.rtr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phonology.Feature.rtr")).group prec✝

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.

@[instance_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 := ⋯ }

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)

@[instance_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)

@[instance_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

The segment read off a list of (feature, value) pairs. Unmentioned features are unspecified, giving natural-class semantics: ofSpecs [(continuant, false)] lies below every [−cont] segment.

Equations

• Phonology.Segment.ofSpecs specs f = List.lookup f specs

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

@[instance_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

@[instance_reducible]

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

Equations

• s.instDecidableIsConsonant = id inferInstance

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

A segment is an obstruent iff it is [+cons, -son].

Equations

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

@[instance_reducible]

instance Phonology.Segment.instDecidableIsObstruent (s : Segment) : Decidable s.IsObstruent

Equations

• s.instDecidableIsObstruent = 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)

@[instance_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)

@[instance_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

@[instance_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.

@[instance_reducible]

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

Equations

• s.instDecidableIsLiquid = id inferInstance

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

A segment is a sibilant iff it is [+strident]. [strident] is a coronal feature, so the sibilants are the strident coronal fricatives and affricates.

Equations

• s.IsSibilant = s.HasValue Phonology.Feature.strident true

@[instance_reducible]

instance Phonology.Segment.instDecidableIsSibilant (s : Segment) : Decidable s.IsSibilant

Equations

• s.instDecidableIsSibilant = Phonology.Segment.instDecidableIsSibilant._aux_1 s

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)

@[instance_reducible]

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

Equations

• s.instDecidableIsGlide = id inferInstance

Feature changes

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. For default-fill semantics that only assign when f is currently unspecified, use fillFromContext.

Equations

• s.setFeature f v = Function.update s f (some v)

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

In categorical feature spreading from context, the target s, when unspecified for f, takes the f-value of ctx, and 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 g = (s g).or (Function.update ⊥ f (ctx f) g)

def Phonology.Segment.restrict (C : Finset Feature) (s : Segment) : Segment

The segment kept on the features in C and unspecified on the rest.

Equations

• Phonology.Segment.restrict C s = C.piecewise s ⊥

inductive Phonology.Segment.Class : Type

The coarse two-way classification of a segment, the commonest conditioning environment for morph-variant selection (pre-consonantal vs pre-vocalic).

• consonant : Class

  A consonant.

• vowel : Class

  A vowel.

@[instance_reducible]

instance Phonology.Segment.instDecidableEqClass : DecidableEq Class

Equations

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

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

Equations

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

@[instance_reducible]

instance Phonology.Segment.instReprClass : Repr Class

Equations

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

@[instance_reducible]

instance Phonology.Segment.instFintypeClass : Fintype Class

Equations

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

def Phonology.Segment.toClass (s : Segment) : Class

A segment's coarse class is vowel when it is [+syllabic] and consonant otherwise.

Equations

• s.toClass = if s.IsVowel then Phonology.Segment.Class.vowel else Phonology.Segment.Class.consonant

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

@[instance_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✝

@[instance_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

@[instance_reducible]

instance Phonology.Sonority.instLinearOrder : LinearOrder Sonority

Equations

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

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. It is the scale on which sonority-conditioned variation such as Tarifit intrusive vowels is stated ([AZ25b]).

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

@[instance_reducible]

instance Phonology.Sonority.instDecidableEqClass : DecidableEq Class

Equations

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

@[instance_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.Voiceless : Class → Prop

The voiceless obstruent classes.

Equations

• Phonology.Sonority.Class.vls.Voiceless = True
• Phonology.Sonority.Class.vlf.Voiceless = True
• x✝.Voiceless = False

@[instance_reducible]

instance Phonology.Sonority.instDecidablePredClassVoiceless : DecidablePred Class.Voiceless

Equations

• Phonology.Sonority.instDecidablePredClassVoiceless Phonology.Sonority.Class.vls = isTrue trivial
• Phonology.Sonority.instDecidablePredClassVoiceless Phonology.Sonority.Class.vlf = isTrue trivial
• Phonology.Sonority.instDecidablePredClassVoiceless Phonology.Sonority.Class.vds = isFalse ⋯
• Phonology.Sonority.instDecidablePredClassVoiceless Phonology.Sonority.Class.vdf = isFalse ⋯
• Phonology.Sonority.instDecidablePredClassVoiceless Phonology.Sonority.Class.nasal = isFalse ⋯
• Phonology.Sonority.instDecidablePredClassVoiceless Phonology.Sonority.Class.liquid = isFalse ⋯
• Phonology.Sonority.instDecidablePredClassVoiceless Phonology.Sonority.Class.glide = isFalse ⋯
• Phonology.Sonority.instDecidablePredClassVoiceless Phonology.Sonority.Class.vowel = isFalse ⋯

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

A segment's class on the Parker eight-level scale refines Sonority.ofSegment by splitting the 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