Sagey (1986): The Representation of Features and Relations in Non-Linear Phonology

This file formalizes the feature geometry of the dissertation and its account of association lines. The geometry has a class node for each independently functioning articulator, the larynx, the soft palate, the lips, the tongue front and the tongue body, grouped under a laryngeal and a supralaryngeal node with a place node over the three oral articulators, and each terminal feature hangs from one class node, the degree-of-closure features [continuant] and [consonantal] directly from the root (Node, node). A class node is present or absent, never minus, and a terminal feature under an articulator node implies that articulator (Segment.Licensed). Three consequences follow from the natural classes of the tree: place assimilation leaves degree of closure and nasality untouched, as in Kpelle and Sanskrit (degreeOfClosure_mem_naturalClass_iff), features of distinct articulators can stand in no dependency, so the rounding-under-height structure proposed for Yawelmani is unrepresentable (disjoint_naturalClass_of_articulators), and a rounded coronal is a complex segment, so a language that admits one articulator under the place node rounds only labials (isComplex_of_round_of_coronal).

Association lines represent overlap in time rather than simultaneity (Association.Valid), which lets a contour segment share one timing slot and a geminate one melody. Two valid associations cannot cross (Association.Valid.not_crosses), so the well-formedness condition of [Gol76] is eliminated: the index-level No-Crossing Constraint of Phonology/Autosegmental/NonCrossing holds of any link set realised by valid associations (isNonCrossing_of_valid).

Implementation notes

The substrate's features are mapped onto the dissertation's: [voice] stands in for the laryngeal stiffness and slackness features, [lateral] is placed under the supralaryngeal node, which the Klamath evidence supports without fixing the node below it, and the acoustic residue [sonorant] and [strident] together with the features the dissertation lacks are left unplaced. The major-articulator pointer from the root and the phonetic default degree of closure of minor articulators are not formalized; the root placement of the degree-of-closure features that motivates the pointer is.

References

• [Sag86]
• [Gol76]
• [Cle85]

The articulator geometry

inductive Sagey1986.Node : Type

The class nodes are the root, the laryngeal and supralaryngeal nodes, the soft palate and place nodes under the latter, and the articulators labial, coronal and dorsal under place.

• root : Node
• laryngeal : Node
• supralaryngeal : Node
• softPalate : Node
• place : Node
• labial : Node
• coronal : Node
• dorsal : Node

@[instance_reducible]

instance Sagey1986.instDecidableEqNode : DecidableEq Node

Equations

• Sagey1986.instDecidableEqNode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Sagey1986.instReprNode : Repr Node

Equations

• Sagey1986.instReprNode = { reprPrec := Sagey1986.instReprNode.repr }

def Sagey1986.instReprNode.repr : Node → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Sagey1986.instReprNode.repr Sagey1986.Node.root prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sagey1986.Node.root")).group prec✝
• Sagey1986.instReprNode.repr Sagey1986.Node.laryngeal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sagey1986.Node.laryngeal")).group prec✝
• Sagey1986.instReprNode.repr Sagey1986.Node.softPalate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sagey1986.Node.softPalate")).group prec✝
• Sagey1986.instReprNode.repr Sagey1986.Node.place prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sagey1986.Node.place")).group prec✝
• Sagey1986.instReprNode.repr Sagey1986.Node.labial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sagey1986.Node.labial")).group prec✝
• Sagey1986.instReprNode.repr Sagey1986.Node.coronal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sagey1986.Node.coronal")).group prec✝
• Sagey1986.instReprNode.repr Sagey1986.Node.dorsal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sagey1986.Node.dorsal")).group prec✝

@[instance_reducible]

instance Sagey1986.instFintypeNode : Fintype Node

Equations

• Sagey1986.instFintypeNode = { elems := { val := ↑Sagey1986.Node.enumList, nodup := Sagey1986.Node.enumList_nodup }, complete := Sagey1986.instFintypeNode._proof_1 }

def Sagey1986.Node.pred : Node → Node

The node immediately dominating each node, the root fixed.

Equations

• Sagey1986.Node.root.pred = Sagey1986.Node.root
• Sagey1986.Node.laryngeal.pred = Sagey1986.Node.root
• Sagey1986.Node.supralaryngeal.pred = Sagey1986.Node.root
• Sagey1986.Node.softPalate.pred = Sagey1986.Node.supralaryngeal
• Sagey1986.Node.place.pred = Sagey1986.Node.supralaryngeal
• Sagey1986.Node.labial.pred = Sagey1986.Node.place
• Sagey1986.Node.coronal.pred = Sagey1986.Node.place
• Sagey1986.Node.dorsal.pred = Sagey1986.Node.place

@[instance_reducible]

instance Sagey1986.Node.instPartialOrder : PartialOrder Node

a ≤ b when a lies on the walk from b up to the root, so the root is ⊥ and the parent is Order.pred.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Sagey1986.Node.instDecidableLE : DecidableLE Node

Equations

• a.instDecidableLE b = { decide := decide (List.elem a (List.iterate Sagey1986.Node.pred b (Fintype.card Sagey1986.Node)) = true), reflects_decide := ⋯ }

@[instance_reducible]

instance Sagey1986.Node.instDecidableLT : DecidableLT Node

Equations

• Sagey1986.Node.instDecidableLT = decidableLTOfDecidableLE

@[instance_reducible]

instance Sagey1986.Node.instOrderBot : OrderBot Node

Equations

• Sagey1986.Node.instOrderBot = { bot := Sagey1986.Node.root, bot_le := Sagey1986.Node.instOrderBot._proof_1 }

@[instance_reducible]

instance Sagey1986.Node.instPredOrder : PredOrder Node

The parent as the predecessor.

Equations

• One or more equations did not get rendered due to their size.

def Sagey1986.Node.feature? : Node → Option Phonology.Feature

The class feature of an articulator node, present exactly when the articulator is active in the segment.

Equations

• Sagey1986.Node.labial.feature? = some Phonology.Feature.labial
• Sagey1986.Node.coronal.feature? = some Phonology.Feature.coronal
• Sagey1986.Node.dorsal.feature? = some Phonology.Feature.dorsal
• x✝.feature? = none

def Sagey1986.Node.articulators : Finset Node

The articulator nodes under place, whose distinct combinations are the complex segments.

Equations

• Sagey1986.Node.articulators = {Sagey1986.Node.labial, Sagey1986.Node.coronal, Sagey1986.Node.dorsal}

theorem Sagey1986.Node.not_le_of_mem_articulators {a b : Node} (ha : a ∈ articulators) (hb : b ∈ articulators) (hab : a ≠ b) : ¬a ≤ b

Distinct articulators are independent: neither dominates the other.

def Sagey1986.node : Phonology.Feature → Option Node

Each terminal feature hangs from a class node: the degree-of-closure features from the root, the glottal features from the laryngeal node, nasality from the soft palate, laterality from the supralaryngeal node, and the place features from their articulators.

Equations

• Sagey1986.node Phonology.Feature.continuant = some Sagey1986.Node.root
• Sagey1986.node Phonology.Feature.consonantal = some Sagey1986.Node.root
• Sagey1986.node Phonology.Feature.voice = some Sagey1986.Node.laryngeal
• Sagey1986.node Phonology.Feature.spreadGlottis = some Sagey1986.Node.laryngeal
• Sagey1986.node Phonology.Feature.constrGlottis = some Sagey1986.Node.laryngeal
• Sagey1986.node Phonology.Feature.nasal = some Sagey1986.Node.softPalate
• Sagey1986.node Phonology.Feature.lateral = some Sagey1986.Node.supralaryngeal
• Sagey1986.node Phonology.Feature.labial = some Sagey1986.Node.labial
• Sagey1986.node Phonology.Feature.round = some Sagey1986.Node.labial
• Sagey1986.node Phonology.Feature.coronal = some Sagey1986.Node.coronal
• Sagey1986.node Phonology.Feature.anterior = some Sagey1986.Node.coronal
• Sagey1986.node Phonology.Feature.distributed = some Sagey1986.Node.coronal
• Sagey1986.node Phonology.Feature.dorsal = some Sagey1986.Node.dorsal
• Sagey1986.node Phonology.Feature.high = some Sagey1986.Node.dorsal
• Sagey1986.node Phonology.Feature.low = some Sagey1986.Node.dorsal
• Sagey1986.node Phonology.Feature.back = some Sagey1986.Node.dorsal
• Sagey1986.node Phonology.Feature.syllabic = none
• Sagey1986.node Phonology.Feature.sonorant = none
• Sagey1986.node Phonology.Feature.approximant = none
• Sagey1986.node Phonology.Feature.delayedRelease = none
• Sagey1986.node Phonology.Feature.strident = none
• Sagey1986.node Phonology.Feature.tap = none
• Sagey1986.node Phonology.Feature.trill = none
• Sagey1986.node Phonology.Feature.labiodental = none
• Sagey1986.node Phonology.Feature.front = none
• Sagey1986.node Phonology.Feature.tense = none
• Sagey1986.node Phonology.Feature.atr = none
• Sagey1986.node Phonology.Feature.rtr = none

Natural classes

theorem Sagey1986.degreeOfClosure_mem_naturalClass_iff (f : Phonology.Feature) : f ∈ {Phonology.Feature.continuant, Phonology.Feature.consonantal} → ∀ (a : Node), f ∈ Phonology.FeatureGeometry.naturalClass node a ↔ a = ⊥

The degree-of-closure features belong to the root's class alone: spreading any class node below the root, as place assimilation does, leaves the degree of closure untouched.

theorem Sagey1986.nasal_mem_naturalClass_iff (a : Node) : Phonology.Feature.nasal ∈ Phonology.FeatureGeometry.naturalClass node a ↔ a ≤ Node.softPalate

Nasality is in the classes of the soft palate node and its ancestors alone: place assimilation leaves it, and spreading the supralaryngeal node carries it, as in Klamath.

theorem Sagey1986.disjoint_naturalClass_of_articulators {a b : Node} (ha : a ∈ Node.articulators) (hb : b ∈ Node.articulators) (hab : a ≠ b) : Disjoint (Phonology.FeatureGeometry.naturalClass node a) (Phonology.FeatureGeometry.naturalClass node b)

Distinct articulators have disjoint classes: a feature of one, such as rounding, can depend on no node of another, such as height.

Complex segments

def Phonology.Segment.Licensed (s : Segment) : Prop

A segment is licensed when every terminal feature it specifies under an articulator node, whichever its value, activates that articulator.

Equations

• s.Licensed = ∀ (f : Phonology.Feature), Option.isSome (s f) = true → ∀ n ∈ Sagey1986.node f, ∀ g ∈ n.feature?, s g = some true

@[instance_reducible]

instance Sagey1986.instDecidableLicensed (s : Phonology.Segment) : Decidable s.Licensed

Equations

• Sagey1986.instDecidableLicensed s = id inferInstance

theorem Sagey1986.isComplex_of_round_of_coronal {s : Phonology.Segment} (hs : s.Licensed) (hr : Option.isSome (s Phonology.Feature.round) = true) (hc : s Phonology.Feature.coronal = some true) : s.IsComplex

A rounded coronal is complex, since rounding activates the labial articulator; a language that admits one articulator under the place node therefore rounds only labials.

def Sagey1986.kp : Phonology.Segment

The double occlusions of Halle's survey and the Kinyarwanda triple occlusion are the labiovelar, labiocoronal, coronovelar and labiocoronovelar stops.

Equations

• Sagey1986.kp = Phonology.Segment.ofSpecs [(Phonology.Feature.consonantal, true), (Phonology.Feature.continuant, false), (Phonology.Feature.labial, true), (Phonology.Feature.dorsal, true)]

def Sagey1986.pt : Phonology.Segment

Equations

• One or more equations did not get rendered due to their size.

def Sagey1986.click : Phonology.Segment

Equations

• One or more equations did not get rendered due to their size.

def Sagey1986.tkw : Phonology.Segment

Equations

• One or more equations did not get rendered due to their size.

def Sagey1986.mw : Phonology.Segment

The rounded labial nasal of Aneityum, whose inventory admits one articulator under place.

Equations

• One or more equations did not get rendered due to their size.

theorem Sagey1986.occlusions_isComplex : kp.IsComplex ∧ pt.IsComplex ∧ click.IsComplex ∧ tkw.IsComplex ∧ mw.Licensed ∧ ¬mw.IsComplex

Every multiple occlusion is complex, and the rounded labial is licensed yet simple.

Association lines

structure Sagey1986.Association (T : Type u_2) [LinearOrder T] : Type u_2

An association line between a timing position and a melodic element, each occupying an interval of time.

• timing : NonemptyInterval T
• melody : NonemptyInterval T

def Sagey1986.Association.Valid {T : Type u_1} [LinearOrder T] (a : Association T) : Prop

An association line represents overlap in time: some instant of the melody is simultaneous with some instant of the timing position.

Equations

• a.Valid = a.timing.Overlaps a.melody

@[instance_reducible]

instance Sagey1986.instDecidableValid {T : Type u_1} [LinearOrder T] (a : Association T) : Decidable a.Valid

Equations

• Sagey1986.instDecidableValid a = { decide := decide (a.timing.toProd.1 ≤ a.melody.toProd.2) && decide (a.melody.toProd.1 ≤ a.timing.toProd.2), reflects_decide := ⋯ }

def Sagey1986.Association.Crosses {T : Type u_1} [LinearOrder T] (a b : Association T) : Prop

Two associations cross when their timing positions are ordered one way and their melodies the other.

Equations

• a.Crosses b = (a.timing.Precedes b.timing ∧ b.melody.Precedes a.melody)

theorem Sagey1986.Association.Valid.not_crosses {T : Type u_1} [LinearOrder T] {a b : Association T} (ha : a.Valid) (hb : b.Valid) : ¬a.Crosses b

Valid associations do not cross: the two precedences and the two overlaps would chain into an instant preceding itself, so the relations a crossing encodes are contradictory.

def Sagey1986.IsNoCrossing {T : Type u_1} [LinearOrder T] (S : Set (Association T)) : Prop

A set of association lines satisfies the No-Crossing Constraint when no two of them cross.

Equations

• Sagey1986.IsNoCrossing S = S.Pairwise fun (a b : Sagey1986.Association T) => ¬a.Crosses b

theorem Sagey1986.isNoCrossing_of_forall_valid {T : Type u_1} [LinearOrder T] {S : Set (Association T)} (h : ∀ a ∈ S, a.Valid) : IsNoCrossing S

Any set of valid associations satisfies the No-Crossing Constraint.

structure Sagey1986.TierRealization (T : Type u_2) [LinearOrder T] : Type u_2

A realisation places two tiers in time, with intervals for the timing positions and for the melodic elements and each tier's order realised as precedence.

• timing : ℕ → NonemptyInterval T
• melody : ℕ → NonemptyInterval T
• timing_precedes {i j : ℕ} : i < j → (self.timing i).Precedes (self.timing j)
• melody_precedes {k l : ℕ} : k < l → (self.melody k).Precedes (self.melody l)

def Sagey1986.TierRealization.assoc {T : Type u_1} [LinearOrder T] (R : TierRealization T) (k i : ℕ) : Association T

The association realising the link of melodic element k to timing position i.

Equations

• R.assoc k i = { timing := R.timing i, melody := R.melody k }

theorem Sagey1986.isNonCrossing_of_valid {T : Type u_1} [LinearOrder T] (R : TierRealization T) {links : Finset (ℕ × ℕ)} (h : ∀ p ∈ links, (R.assoc p.1 p.2).Valid) : Autosegmental.IsNonCrossing links

Goldsmith's index-level No-Crossing Constraint is derived: a link set whose links are all realised as valid associations satisfies it.

def Sagey1986.TierRealization.canonical : TierRealization ℤ

Position n of either tier occupies the interval from 2n to 2n + 1.

Equations

• One or more equations did not get rendered due to their size.

theorem Sagey1986.canonical_diagonal_valid (n : ℕ) : (TierRealization.canonical.assoc n n).Valid

Every diagonal link is valid under the canonical realisation, so the hypothesis of isNonCrossing_of_valid is satisfiable.

def Sagey1986.assoc (ts tf ms mf : ℤ) (ht : ts ≤ tf := by omega) (hm : ms ≤ mf := by omega) : Association ℤ

Equations

• Sagey1986.assoc ts tf ms mf ht hm = { timing := { fst := ts, snd := tf, fst_le_snd := ht }, melody := { fst := ms, snd := mf, fst_le_snd := hm } }

theorem Sagey1986.contour_geminate_valid : ((assoc 0 4 0 2 contour_geminate_valid._proof_2 contour_geminate_valid._proof_4).Valid ∧ (assoc 0 4 2 4 contour_geminate_valid._proof_2 contour_geminate_valid._proof_6).Valid) ∧ (assoc 0 1 0 3 contour_geminate_valid._proof_8 contour_geminate_valid._proof_10).Valid ∧ (assoc 2 3 0 3 contour_geminate_valid._proof_12 contour_geminate_valid._proof_10).Valid

A contour segment, two melodies sequenced within one timing slot, and a geminate, one melody spanning two timing slots, are both pairs of valid associations, which simultaneity would forbid by identifying the two melodies, or the two slots.