Documentation

Linglib.Phonology.Segmental.Basic

Basic theory of segments #

This file develops the theory of the segments defined in Phonology/Segmental/Defs.lean. Natural-class membership is the bundle order: a specification matches a segment exactly when it lies below it in the subsumption order of Shieber and Carpenter, so having a value is lying above the bundle specifying that value alone, matching a specification list is having each listed value, and each conjunctive natural class is the segments above its specification. The remaining results concern the feature-change operations, the features on which sonority depends, the sonority rise between two classes, and the Parker sonority ranking.

Main results #

References #

Natural classes are the bundle order #

source
@[simp]
theorem Phonology.Segment.ofSpecs_apply (specs : List (Feature × Bool)) (f : Feature) :
ofSpecs specs f = List.lookup f specs
source
theorem Phonology.Segment.ofSpecs_le_iff (s : Segment) (specs : List (Feature × Bool)) :
ofSpecs specs ≤ s ↔ ∀ (f : Feature) (v : Bool), List.lookup f specs = some v → s.HasValue f v

A specification list lies below a segment exactly when the segment has every value the list looks up.

source
theorem Phonology.Segment.ofSpecs_le_iff_forall_mem (s : Segment) {specs : List (Feature × Bool)} (h : (List.map Prod.fst specs).Nodup) :
ofSpecs specs ≤ s ↔ ∀ p ∈ specs, s.HasValue p.1 p.2

With distinct features, a specification list lies below a segment exactly when the segment has each listed value.

source
theorem Phonology.Segment.hasValue_iff_ofSpecs_le (s : Segment) (f : Feature) (v : Bool) :
s.HasValue f v ↔ ofSpecs [(f, v)] ≤ s

Having a value is lying above the segment that specifies that value alone.

source
theorem Phonology.Segment.isVowel_iff_le (s : Segment) :
s.IsVowel ↔ ofSpecs [(Feature.syllabic, true)] ≤ s

The vowels are the segments above [+syllabic].

source
theorem Phonology.Segment.isConsonant_iff_le (s : Segment) :
s.IsConsonant ↔ ofSpecs [(Feature.consonantal, true)] ≤ s

The consonants are the segments above [+consonantal].

source
theorem Phonology.Segment.isObstruent_iff_le (s : Segment) :
s.IsObstruent ↔ ofSpecs [(Feature.consonantal, true), (Feature.sonorant, false)] ≤ s

The obstruents are the segments above [+cons, −son].

source
theorem Phonology.Segment.isStop_iff_le (s : Segment) :
s.IsStop ↔ ofSpecs [(Feature.consonantal, true), (Feature.sonorant, false), (Feature.continuant, false)] ≤ s

The stops are the segments above [+cons, −son, −cont].

source
theorem Phonology.Segment.isFricative_iff_le (s : Segment) :
s.IsFricative ↔ ofSpecs [(Feature.consonantal, true), (Feature.sonorant, false), (Feature.continuant, true)] ≤ s

The fricatives are the segments above [+cons, −son, +cont].

source
theorem Phonology.Segment.isNasal_iff_le (s : Segment) :
s.IsNasal ↔ ofSpecs [(Feature.nasal, true)] ≤ s

The nasals are the segments above [+nasal].

source
theorem Phonology.Segment.isSibilant_iff_le (s : Segment) :
s.IsSibilant ↔ ofSpecs [(Feature.strident, true)] ≤ s

The sibilants are the segments above [+strident].

source
theorem Phonology.Segment.isGlide_iff_le (s : Segment) :
s.IsGlide ↔ ofSpecs [(Feature.consonantal, false), (Feature.syllabic, false), (Feature.approximant, true)] ≤ s

The glides are the segments above [−cons, −syll, +approx].

Effect on the modified feature #

source
@[simp]
theorem Phonology.Segment.setFeature_hasValue (s : Segment) (f : Feature) (v : Bool) :
(s.setFeature f v).HasValue f v
source
theorem Phonology.Segment.fillFromContext_apply_self_of_unspecified (s : Segment) {f : Feature} (h : s.Unspecified f) (ctx : Segment) :
s.fillFromContext f ctx f = ctx f
source
theorem Phonology.Segment.fillFromContext_apply_self_of_specified (s : Segment) {f : Feature} {w : Bool} (h : s.HasValue f w) (ctx : Segment) :
s.fillFromContext f ctx f = some w

Value preserved on other features #

source
@[simp]
theorem Phonology.Segment.setFeature_apply_of_ne (s : Segment) {f g : Feature} (h : f ≠ g) (v : Bool) :
s.setFeature f v g = s g
source
@[simp]
theorem Phonology.Segment.fillFromContext_apply_of_ne (s : Segment) {f g : Feature} (h : f ≠ g) (ctx : Segment) :
s.fillFromContext f ctx g = s g

Distinctive feature sets #

source
theorem Phonology.Segment.restrict_eq_restrict_iff {C : Finset Feature} {s s' : Segment} :
restrict C s = restrict C s' ↔ Set.EqOn s s' ↑C

Two segments have the same restriction to a feature set iff they agree on it.

source
theorem Phonology.Segment.restrict_restrict {C D : Finset Feature} (s : Segment) :
restrict D (restrict C s) = restrict (C ∩ D) s

Restricting to one feature set and then another keeps the features in both.

source
def Phonology.IsDistinctive (C : Finset Feature) (I : Finset Segment) :
Prop

A feature set is distinctive for an inventory when no two segments of the inventory agree on it.

Equations
Instances For
    source
    @[instance_reducible]
    instance Phonology.instDecidableIsDistinctive {C : Finset Feature} {I : Finset Segment} :
    Decidable (IsDistinctive C I)
    Equations
    source
    theorem Phonology.IsDistinctive.mono {C D : Finset Feature} {I : Finset Segment} (h : IsDistinctive C I) (hCD : C ⊆ D) :
    IsDistinctive D I

    A larger feature set is still distinctive.

    source
    theorem Phonology.IsDistinctive.subset {C : Finset Feature} {I J : Finset Segment} (h : IsDistinctive C I) (hJI : J ⊆ I) :
    IsDistinctive C J

    A distinctive feature set is distinctive for every smaller inventory.

    Sonority #

    source
    theorem Phonology.Sonority.rank_strictMono :
    StrictMono rank
    source
    def Phonology.Sonority.features :
    Finset Feature

    The features ofSegment reads are the major-class features and continuancy. Place and laryngeal features are absent.

    Equations
    Instances For
      source
      theorem Phonology.Sonority.ofSegment_congr {s s' : Segment} (h : ∀ f ∈ features, s f = s' f) :
      ofSegment s = ofSegment s'

      Sonority depends on a segment only through Sonority.features.

      source
      theorem Phonology.Sonority.ofSegment_setFeature {f : Feature} (hf : f ∉ features) (s : Segment) (v : Bool) :
      ofSegment (s.setFeature f v) = ofSegment s

      Setting a feature that sonority does not read leaves sonority unchanged.

      source
      def Phonology.Sonority.rise (a b : Sonority) :
      ℤ

      The sonority rise from a to b is positive when sonority rises, zero on a plateau, and negative when it falls.

      Equations
      Instances For
        source
        @[simp]
        theorem Phonology.Sonority.rise_self (a : Sonority) :
        a.rise a = 0
        source
        theorem Phonology.Sonority.neg_rise (a b : Sonority) :
        -a.rise b = b.rise a
        source
        theorem Phonology.Sonority.rise_add_rise (a b c : Sonority) :
        a.rise b + b.rise c = a.rise c
        source
        @[simp]
        theorem Phonology.Sonority.rise_pos {a b : Sonority} :
        0 < a.rise b ↔ a < b
        source
        @[simp]
        theorem Phonology.Sonority.rise_neg {a b : Sonority} :
        a.rise b < 0 ↔ b < a
        source
        @[simp]
        theorem Phonology.Sonority.rise_eq_zero {a b : Sonority} :
        a.rise b = 0 ↔ a = b
        source
        theorem Phonology.Sonority.Class.parkerRank_injective :
        Function.Injective parkerRank

        The eight Parker classes receive distinct ranks ([Par02]). The ranking is Parker's reversible default, so injectivity is the faithful invariant, and no fixed order on Sonority.Class is implied.

        source
        theorem Phonology.Sonority.Class.toSonority_ofSegment (s : Segment) :
        (ofSegment s).toSonority = Sonority.ofSegment s

        Classifying on the Parker scale and collapsing the voicing split is the six-level classification.