Sonority scales

import Linglib.Phonology.Segmental.Sonority · namespace Phonology

A sonority scale ranks segments, or classes of them, in a linear order. A set is a cut of a scale when it is what the scale places in an upper set of its points, and contiguous when it is what lies within some interval, the preimage of an order-connected set. A feature cuts a scale when the segments with one of its values form a cut. The cuts of a scale are nested, as the upper sets of a linear order are, so features whose values cross do not both cut it, and two features whose values combine freely do not both divide it into contiguous classes. A scale coarsens another when it preserves its order, and the cuts of the coarser scale are cuts of the finer one.

The base scale is the sonority hierarchy of Hayes's Table 4.1, the modal hierarchy of Parker: obstruents, nasals, liquids, glides and vowels. Each class is defined by the features of Hayes's p. 77, the columns of the table are cut by [sonorant], [approximant], [consonantal] and [syllabic], [continuant] is not a sonority feature, and among the columns the natural classes are the contiguous sets.

Main definitions

Phonology.Sonority.IsCut, Phonology.Sonority.Contiguous: the sets of a scale above a point and within an interval.
Phonology.Sonority.Coarsens: a scale preserves the order of another.
Phonology.Sonority.profile: whether sonority rises, plateaus or falls from one segment to another.
Phonology.Sonority: the classes of the hierarchy, with Sonority.toSegment the columns of Table 4.1, Sonority.description the features of p. 77, and Sonority.ofSegment.

Main results

Phonology.Sonority.IsCut.total: the cuts of a scale are nested.
Phonology.Sonority.not_contiguous_of_independent: two features whose values combine freely do not both divide a scale into contiguous classes.
Phonology.Sonority.IsCut.of_coarsens: the cuts of a coarser scale are cuts of a finer one.
Phonology.Sonority.ofSegment_eq_of_le, Phonology.Sonority.description_le_iff: a segment with the values of a column of Table 4.1 has that column's sonority and description.
Phonology.Sonority.isNaturalClass_image_iff: among the columns, the natural classes are the contiguous sets.

References

Hayes 2009, Introductory Phonology
Parker 2002, Quantifying the Sonority Hierarchy formalized

Scales

A set is a cut of a scale when it is what the scale places in an upper set of its points.

def Sonority.IsCut L71–72

{α : Type u_1} {β : Type u_2} [LinearOrder β] (σ : α → β) (S : Set α) :

Prop

Sonority.IsCut σ S = ∃ (U : UpperSet β), S = σ ⁻¹' ↑U

Used by Sonority.IsCut.total, Sonority.not_isCut_and_isCut, Sonority.IsCut.contiguous, Sonority.IsCut.of_coarsens, Sonority.isCut_features

A set is contiguous on a scale when it is the preimage of an order-connected set.

def Sonority.Contiguous L74–75

{α : Type u_1} {β : Type u_2} [LinearOrder β] (σ : α → β) (S : Set α) :

Prop

Sonority.Contiguous σ S = ∃ (I : Set β), I.OrdConnected ∧ S = σ ⁻¹' I

Used by Sonority.IsCut.contiguous, Sonority.contiguous_iff, Sonority.instDecidableContiguousOfFintypeOfDecidablePredMemSet, Sonority.not_contiguous_of_independent, Sonority.not_contiguous_continuant

Used in Parker2002

A scale τ coarsens a scale σ when it preserves its order.

def Sonority.Coarsens L77–78

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder β] [LinearOrder γ] (τ : α → γ) (σ : α → β) :

Prop

Sonority.Coarsens τ σ = ∀ (a b : α), σ a ≤ σ b → τ a ≤ τ b

Used by Sonority.IsCut.of_coarsens

Used in AfkirZellou2025, Benua1997, Parker2002

Whether sonority rises (lt), plateaus (eq) or falls (gt) from a to b.

def Sonority.profile L80–81

{α : Type u_1} {β : Type u_2} [LinearOrder β] (σ : α → β) (a b : α) :

Ordering

Sonority.profile σ a b = compare (σ a) (σ b)

Used in AfkirZellou2025, Benua1997, McCarthy2005

theorem Sonority.IsCut.total L83–86

{α : Type u_1} {β : Type u_2} [LinearOrder β] {σ : α → β} {S T : Set α} (hS : IsCut σ S) (hT : IsCut σ T) :

S ⊆ T ∨ T ⊆ S

Built from

theorem Sonority.IsCut.of_coarsens L109–113

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder β] [LinearOrder γ] {σ : α → β} {τ : α → γ} {S : Set α} (h : Coarsens τ σ) (hS : IsCut τ S) :

IsCut σ S

Built from ,

Two features whose values combine freely do not both divide a scale into contiguous classes.

theorem Sonority.not_contiguous_of_independent L115–129

{α : Type u_1} {β : Type u_2} [LinearOrder β] (σ : α → β) {φ ψ : α → Bool} (h : ∀ (x y : Bool), ∃ (a : α), φ a = x ∧ ψ a = y) :

¬((∀ (v : Bool), Contiguous σ {a : α | φ a = v}) ∧ ∀ (v : Bool), Contiguous σ {a : α | ψ a = v})

Built from

The sonority hierarchy

The sonority hierarchy, from least to most sonorous.

inductive Sonority L135–147

Type

obstruent : Sonority
The obstruents, [−sonorant].
nasal : Sonority
The nasals, [−approximant, +sonorant].
liquid : Sonority
The liquids, [+consonantal, +approximant].
glide : Sonority
The glides, [−syllabic, −consonantal].
vowel : Sonority
The vowels, [+syllabic].

Derives DecidableEq, Repr, Fintype.

Used by Sonority.rank, Sonority.instLinearOrder, Sonority.toSegment, Sonority.description, Sonority.ofSegment, Sonority.isCut_features, Sonority.ofSegment_toSegment, Sonority.apply_eq_toSegment_of_le, Sonority.ofSegment_eq_of_le, Sonority.description_le_iff, Sonority.description_le_iff_ofSegment_eq, Sonority.rise, Sonority.rise_self, Sonority.neg_rise, Sonority.rise_add_rise, Sonority.rise_pos, Sonority.rise_neg, Sonority.rise_eq_zero, Sonority.naturalClass_description, Sonority.isNaturalClass_image_iff

Used in Benua1997, Parker2002

L151–153

L155–156

The column of a class in Table 4.1: its values for [syllabic], [consonantal], [approximant] and [sonorant], the four features that cut the hierarchy.

def Sonority.toSegment L158–170

Sonority → Segment

The definition is too large to print here; read it in the source.

Built from

Used by Sonority.isCut_features, Sonority.ofSegment_toSegment, Sonority.apply_eq_toSegment_of_le, Sonority.ofSegment_eq_of_le, Sonority.description_le_iff, Sonority.description_le_iff_ofSegment_eq, Sonority.naturalClass_description, Sonority.isNaturalClass_image_iff

Used in Fragments/Finnish/Phonology

The features that define a class (Hayes p. 77): [−sonorant] for an obstruent, [−approximant, +sonorant] for a nasal, [+consonantal, +approximant] for a liquid, [−syllabic, −consonantal] for a glide and [+syllabic, −consonantal] for a vowel. Hayes lists a vowel as [+syllabic] with the complication of the syllabic consonants left to his next section, and his Table 4.1 has it [−consonantal].

def Sonority.description L172–182

Sonority → Segment

Equations

Sonority.obstruent.description = Segment.ofSpecs [(Feature.sonorant, false)]
Sonority.nasal.description = Segment.ofSpecs [(Feature.approximant, false), (Feature.sonorant, true)]
Sonority.liquid.description = Segment.ofSpecs [(Feature.consonantal, true), (Feature.approximant, true)]
Sonority.glide.description = Segment.ofSpecs [(Feature.syllabic, false), (Feature.consonantal, false)]
Sonority.vowel.description = Segment.ofSpecs [(Feature.syllabic, true), (Feature.consonantal, false)]

Built from

Used by Sonority.description_le_iff, Sonority.description_le_iff_ofSegment_eq, Sonority.naturalClass_description, Segment.isVowel_iff_le, Segment.isObstruent_iff_le, Segment.isNasal_iff_le

The sonority of a segment: an obstruent if [−sonorant], else a nasal if [−approximant], else a liquid if [+consonantal], else a vowel if [+syllabic], and otherwise a glide. A syllabic liquid or nasal keeps the sonority of its class.

def Sonority.ofSegment L184–192

(s : Segment) :

Sonority

The definition is too large to print here; read it in the source.

Built from

Used by Sonority.ofSegment_congr, Sonority.ofSegment_setFeature, Sonority.ofSegment_toSegment, Sonority.ofSegment_eq_of_le, Sonority.description_le_iff_ofSegment_eq, Sonority.not_contiguous_continuant

Used in Fragments/Latin/Phonology, Fragments/Romance/Italian/Phonology, AfkirZellou2025, Benua1997, Berent2026 and 1 more

L194

L196–205