Documentation

Linglib.Phonology.Segmental.FeatureClass

Feature classes #

The grouping of Hayes's features by the sections of his feature chapter — manner (§4.4, including the sonority features), laryngeal (§4.7), and the three major articulators (§4.6.1) with their dependents, [round] and [labiodental] under labial (§4.6.3), [anterior], [distributed], [strident] and [lateral] under coronal (§4.6.2), and the vowel features (§4.5) under dorsal (§4.6.4) — as plain finite sets, with Place their union (Padgett p. 83). The grouping is the inventory's own and makes no constituency claim, with no root, no order and no FeatureGeometry instance, because the current textbooks agree on the flat classes but not on a tree: Hayes draws none, nor do Bale and Reiss; Gussenhoven and Jacobs draw one with a supralaryngeal node and no manner constituent (the consensus tree of Broe), Davenport and Hannahs one with a manner class node, and Zsiga one with the manner features at the root together with the statement that no consensus exists, parting ways exactly where Clements, Sagey, and Halle, Vaux and Wolfe do, on the supralaryngeal node, a manner constituent, and the homes of [continuant], [strident], [lateral], [nasal] and [tense]. Trees are therefore instances of Phonology/FeatureGeometry.lean in the studies of the works that argue for them, and agreement on a class — Brown and Meyer's AGREE[place] — is Set.EqOn on the class. Designated articulators are the articulator features a segment is specified for (Halle, Vaux and Wolfe §1.2.2), and a complex segment has more than one (Sagey).

Main definitions #

Main results #

Implementation notes #

The contested placements are Hayes's: [strident] and [lateral] are coronal where Gussenhoven and Jacobs, Davenport and Hannahs and Clements make them manner features, and [tense] is a vowel feature under dorsal where the tree-drawing textbooks give [ATR] its own radical or pharyngeal node. Agreement on a class or on the place class is decidable, so AGREE-style facts about Fragment segments close by decide.

References #

The classes #

source
inductive Phonology.FeatureClass :
Type

Hayes's five feature classes: manner, laryngeal, and the three major articulators.

Instances For
    source
    @[instance_reducible]
    instance Phonology.instDecidableEqFeatureClass :
    DecidableEq FeatureClass
    Equations
    source
    @[instance_reducible]
    instance Phonology.instReprFeatureClass :
    Repr FeatureClass
    Equations
    source
    def Phonology.instReprFeatureClass.repr :
    FeatureClass → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Phonology.instFintypeFeatureClass :
      Fintype FeatureClass
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Phonology.Feature.featureClass :
      Feature → FeatureClass

      The class of each feature, by the sections of Hayes's feature chapter (see the module docstring).

      Equations
      Instances For
        source
        def Phonology.FeatureClass.features (c : FeatureClass) :
        Finset Feature

        The features of a class.

        Equations
        Instances For
          source
          def Phonology.FeatureClass.place :
          Finset Feature

          The place class: the union of the three articulator classes (Padgett p. 83's "Place simply stands for the set {[labial], [coronal], [dorsal], …}").

          Equations
          Instances For
            source
            theorem Phonology.FeatureClass.mem_features {f : Feature} {c : FeatureClass} :
            f ∈ c.features ↔ f.featureClass = c
            source
            theorem Phonology.FeatureClass.mem_place {f : Feature} :
            f ∈ place ↔ f.featureClass = labial ∨ f.featureClass = coronal ∨ f.featureClass = dorsal
            source
            @[instance_reducible]
            instance Phonology.FeatureClass.instDecidableEqOnFeatureFlatBoolCoeFinsetFeatures (s₁ s₂ : Segment) (c : FeatureClass) :
            Decidable (Set.EqOn s₁ s₂ ↑c.features)
            Equations
            source
            @[instance_reducible]
            instance Phonology.FeatureClass.instDecidableEqOnFeatureFlatBoolCoeFinsetPlace (s₁ s₂ : Segment) :
            Decidable (Set.EqOn s₁ s₂ ↑place)
            Equations

            Complex segments #

            source
            def Phonology.Segment.articulators (s : Segment) :
            Finset Feature

            The designated articulators of a segment, as the articulator features it is specified + for (Halle, Vaux and Wolfe §1.2.2).

            Equations
            Instances For
              source
              def Phonology.Segment.IsComplex (s : Segment) :
              Prop

              A complex segment has more than one designated articulator: the labiovelar [k͡p] carries [labial] and [dorsal], the labialised [kʷ] only [dorsal] beside [+round] (Sagey; Halle, Vaux and Wolfe p. 435).

              Equations
              Instances For
                source
                @[instance_reducible]
                instance Phonology.instDecidablePredSegmentIsComplex :
                DecidablePred Segment.IsComplex
                Equations