Documentation

Linglib.Phonology.Segmental.PHOIBLE

Segments from PHOIBLE feature matrices #

This file turns a PHOIBLE feature matrix into a Segment, so that a fragment can take the feature values of its phonemes from the PHOIBLE chart instead of listing them. PHOIBLE's features extend those of Hayes, which Phonology.Feature follows, with length, tone, stress, clicks and further laryngeal features. Each feature of Phonology.Feature is a PHOIBLE column, under another name for [voice], [constricted glottis], [ATR] and [RTR], and the segment of a matrix reads the matrix along that correspondence, dropping the columns it lacks.

The two systems differ in one convention. PHOIBLE specifies [round] only on labial segments and marks it not applicable elsewhere, where Hayes's charts give every other segment [−round]. The segment of a matrix therefore takes [−round] as its default.

PHOIBLE also codes the tongue-root contrast of plain vowel glyphs by [tense], /i e o u/ against /ɪ ɛ ɔ ʊ/, and gives every plain vowel [−ATR]; only glyphs with the diacritic ◌̘ are [+ATR]. A language whose vowels contrast in [ATR] reads a chart entry through its tongue-root reading, which carries the [tense] value as the [ATR] value.

A fragment gives each phoneme by Segment.ofChart. It reads a chart entry, merges over it the values on which a grammar departs from the chart, and keeps the result on the features the grammar treats as contrastive. A phoneme is then a segment, named by its symbol, and an inventory is a finite set of segments, which a fragment shows to lie among the segments of a PHOIBLE inventory.

Main definitions #

Main results #

Implementation notes #

Dropping PHOIBLE's further features can identify two phonemes of an inventory, a long and a short vowel or a plain and a fortis stop, which then have one segment. A fragment guards against this by giving its inventory as a list of segments with a proof that it has no duplicates. PHOIBLE also leaves [round] unspecified on its less-rounded segments, written with ◌̜, which therefore come out [−round]. Velar consonants are [−front, −back] in PHOIBLE, so a vowel tier is picked out by Segment.IsVowel and not by the absence of a [back] value.

References #

source
def Phonology.Feature.toPHOIBLE :
Feature → Data.PHOIBLE.Feature

The PHOIBLE column of a feature.

Equations
Instances For
    source
    theorem Phonology.Feature.toPHOIBLE_injective :
    Function.Injective toPHOIBLE
    source
    def Data.PHOIBLE.FeatureMatrix.toSegment (m : FeatureMatrix) :
    Phonology.Segment

    The segment of a feature matrix reads the matrix along Feature.toPHOIBLE, with [−round] where PHOIBLE marks [round] not applicable.

    Equations
    Instances For
      source
      theorem Data.PHOIBLE.FeatureMatrix.toSegment_apply_of_ne_round (m : FeatureMatrix) {f : Phonology.Feature} (h : f ≠ Phonology.Feature.round) :
      m.toSegment f = m f.toPHOIBLE
      source
      @[simp]
      theorem Data.PHOIBLE.FeatureMatrix.toSegment_round (m : FeatureMatrix) :
      m.toSegment Phonology.Feature.round = ↑(Flat.unbotD false (m Feature.round))
      source
      theorem Data.PHOIBLE.FeatureMatrix.range_toSegment :
      Set.range toSegment = {s : Phonology.Segment | s Phonology.Feature.round ≠ ⊥}

      The segments of feature matrices are exactly those specified for [round], since each other feature of Phonology.Feature is a column of its own.

      The tongue-root reading #

      source
      def Data.PHOIBLE.FeatureMatrix.tenseAsATR (m : FeatureMatrix) :
      FeatureMatrix

      The tongue-root reading of a matrix carries its [tense] value as its tongue-root value, keeping its own tongue-root value where it has no [tense], and has no [tense].

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem Data.PHOIBLE.FeatureMatrix.toSegment_tenseAsATR_atr (m : FeatureMatrix) :
        m.tenseAsATR.toSegment Phonology.Feature.atr = (m Feature.tense).or (m Feature.advancedTongueRoot)
        source
        @[simp]
        theorem Data.PHOIBLE.FeatureMatrix.toSegment_tenseAsATR_tense (m : FeatureMatrix) :
        m.tenseAsATR.toSegment Phonology.Feature.tense = ⊥
        source
        theorem Data.PHOIBLE.FeatureMatrix.toSegment_tenseAsATR_of_ne (m : FeatureMatrix) {f : Phonology.Feature} (ha : f ≠ Phonology.Feature.atr) (ht : f ≠ Phonology.Feature.tense) :
        m.tenseAsATR.toSegment f = m.toSegment f

        Off [ATR] and [tense], the tongue-root reading has the matrix's values.

        Witnesses from the chart #

        source
        def Data.PHOIBLE.Inventory.segments (I : Inventory) :
        Finset Phonology.Segment

        The segments of an inventory's phonemes.

        Equations
        Instances For
          source
          @[simp]
          theorem Data.PHOIBLE.Inventory.mem_segments {I : Inventory} {s : Phonology.Segment} :
          s ∈ I.segments ↔ ∃ y ∈ I.phonemes, y.features.toSegment = s
          source
          theorem Data.PHOIBLE.Inventory.subset_segments_iff {I : Inventory} {S : Finset Phonology.Segment} :
          S ⊆ I.segments ↔ ∀ x ∈ S, ∃ y ∈ I.phonemes, y.features.toSegment = x

          A set of segments lies among those of an inventory when each is the segment of one of its phonemes, a condition decide checks without deduplicating the inventory.

          source
          def Phonology.Segment.ofChart (m : Data.PHOIBLE.FeatureMatrix) (departure : Segment := ⊥) (contrastive : Finset Feature := Finset.univ) :
          Segment

          The segment of a chart entry m has the values of departure where that is specified and those of m elsewhere, kept on the features in contrastive.

          Equations
          Instances For
            source
            theorem Phonology.Segment.ofChart_apply {m : Data.PHOIBLE.FeatureMatrix} {departure : Segment} {contrastive : Finset Feature} {f : Feature} (hf : f ∈ contrastive) (hd : departure f = ⊥) :
            ofChart m departure contrastive f = m.toSegment f
            source
            @[simp]
            theorem Phonology.Segment.ofChart_eq_toSegment (m : Data.PHOIBLE.FeatureMatrix) :
            ofChart m = m.toSegment

            With no departure and every feature contrastive, a chart entry's segment is its matrix's.