Documentation

Linglib.Phonology.Segmental.NaturalClass

Natural classes #

This file defines the natural classes of an inventory. In Hayes's definition a natural class is any complete set of sounds of a language that share the same value for a feature or set of features, so that /p t k/ are the voiceless stops of English and not of Persian, which has /q/ as well. A feature description is an underspecified segment d, a segment x has the values of d when d ≤ x, and the natural class of d in an inventory is the set of its members above d.

What the segments of a set share is their meet, the description Albright and Hayes's minimal generalization reduces two differing segments to. The natural class of that meet is the smallest natural class containing the set. A set of segments is a natural class when it is that smallest class, and it then has a description. It fails to be one when every description its members meet is met by some other segment of the inventory as well.

Main definitions #

Main results #

Implementation notes #

Descriptions are ordered by subsumption and natural classes by inclusion, and the two maps naturalClass and Finset.inf' form an antitone Galois connection, which is that of formal concept analysis for the relation d ≤ x. The meet of the empty set would be an inconsistent description, which Segment lacks, so the statements about meets are for nonempty sets, and a natural class is nonempty by definition.

References #

source
def Phonology.Segment.naturalClass (d : Segment) (I : Finset Segment) :
Finset Segment

The natural class of a description d in an inventory I is the complete set of segments of I that have the values of d.

Equations
Instances For
    source
    @[simp]
    theorem Phonology.Segment.mem_naturalClass {I : Finset Segment} {d x : Segment} :
    x ∈ d.naturalClass I ↔ x ∈ I ∧ d ≤ x
    source
    theorem Phonology.Segment.naturalClass_subset (d : Segment) (I : Finset Segment) :
    d.naturalClass I ⊆ I
    source
    @[simp]
    theorem Phonology.Segment.naturalClass_bot (I : Finset Segment) :
    ⊥.naturalClass I = I

    The empty description is met by the whole inventory.

    source
    theorem Phonology.Segment.naturalClass_anti {I : Finset Segment} {d e : Segment} (h : d ≤ e) :
    e.naturalClass I ⊆ d.naturalClass I

    A more specific description has a smaller natural class.

    source
    theorem Phonology.Segment.naturalClass_mono {I S : Finset Segment} (h : S ⊆ I) (d : Segment) :
    d.naturalClass S ⊆ d.naturalClass I

    A larger inventory has larger natural classes.

    source
    theorem Phonology.Segment.subset_naturalClass_iff {I S : Finset Segment} {d : Segment} (hS : S ⊆ I) :
    S ⊆ d.naturalClass I ↔ ∀ x ∈ S, d ≤ x

    A set of segments of the inventory lies in the natural class of d exactly when each of its members has the values of d.

    source
    theorem Phonology.Segment.subset_naturalClass_iff_le_inf' {I S : Finset Segment} {d : Segment} (hS : S ⊆ I) (hne : S.Nonempty) :
    S ⊆ d.naturalClass I ↔ d ≤ S.inf' hne id

    A set lies in the natural class of d exactly when d is below what the set shares.

    source
    theorem Phonology.Segment.subset_naturalClass_inf' {I S : Finset Segment} (hS : S ⊆ I) (hne : S.Nonempty) :
    S ⊆ (S.inf' hne id).naturalClass I

    A set lies in the natural class of what it shares.

    source
    theorem Phonology.Segment.naturalClass_inf'_subset_iff {I S : Finset Segment} {d : Segment} (hS : S ⊆ I) (hne : S.Nonempty) :
    (S.inf' hne id).naturalClass I ⊆ d.naturalClass I ↔ S ⊆ d.naturalClass I

    The natural class of what a set shares is the smallest natural class containing the set.

    source
    def Phonology.IsNaturalClass (I S : Finset Segment) :
    Prop

    A nonempty set of segments is a natural class of the inventory I when it is the complete set of segments of I that have the values of some description.

    Equations
    Instances For
      source
      theorem Phonology.IsNaturalClass.nonempty {I S : Finset Segment} (h : IsNaturalClass I S) :
      S.Nonempty
      source
      theorem Phonology.IsNaturalClass.subset {I S : Finset Segment} (h : IsNaturalClass I S) :
      S ⊆ I
      source
      theorem Phonology.isNaturalClass_iff {I S : Finset Segment} :
      IsNaturalClass I S ↔ ∃ (hne : S.Nonempty), (S.inf' hne id).naturalClass I = S

      A set is a natural class exactly when it is the natural class of what its members share.

      source
      @[instance_reducible]
      instance Phonology.instDecidableIsNaturalClass (I S : Finset Segment) :
      Decidable (IsNaturalClass I S)
      Equations