Hansson (2010): Consonant Harmony: Long-Distance Interaction in Phonology

This file formalizes the Navajo sibilant harmony with which Hansson opens his survey of consonant harmony (section 1.1, and the case study of section 2.4.1.1). The alveolar and postalveolar sibilant series cannot co-occur, and when morpheme concatenation juxtaposes them the rightmost sibilant determines the anteriority of every sibilant before it, across any vowels and non-sibilant consonants in between (3), (4), (6). The sibilants are the [+strident] segments, and the harmony is agreement in [anterior] on their tier, a tier-based strictly 2-local language. The map anticipatory writes the rightmost sibilant's [anterior] value into every sibilant, and its fixed points are exactly the words of that language, mem_language_iff_anticipatory_eq. It leaves the trigger and everything off the tier in place and neutralizes the contrast in the sibilants it targets, the three characteristics the book draws from (4). It is the search-and-copy run, from the right, of the substrate's harmony System over segments with [anterior] as its feature, the decomposition Rose and Walker share with the vowel harmonies of the fragments, anticipatory_eq_apply. The book's own qualification (section 3.1.2) is the perseveratory assimilation of the first-person subject prefix after the s-perfective and s-destruct prefixes (12), (14), which the anticipatory map mispredicts, perseveratory_rows, while harmony from the root still overrides it (15).

Implementation notes

A segment's class on the tier, sibilantClass, is its [anterior] value, and the book's claims about the examples concern the classes on the tier, so the rows of Data.Examples.Hansson2010 are read for their sibilants and compared class by class. Voicing, which the s-perfective changes in (4b) and (4c) under a condition the book sets aside, and the glottalization of affricates are not compared. The Navajo sibilants are the chart's without [distributed], on which the chart's alveolar and postalveolar series also differ, so that anteriority is the whole of the contrast the harmony changes. The book's correspondence-theoretic analysis (chapters 4 and 5), its typological survey (chapter 2), and its speech-error account (chapter 6) are not formalized; Rose and Walker's Agreement by Correspondence is in Studies/RoseWalker2004.lean.

References

• [Han10]
• [RW11]
• [RW04a]
• [McD91]
• [SH67]

The harmony tier

def Hansson2010.sibilantClass (x : Phonology.Segment) : Option Bool

The class of a sibilant is its [anterior] value, true for the alveolar series and false for the postalveolar, and a segment that is not a sibilant has none.

Equations

• Hansson2010.sibilantClass x = if x.IsSibilant then x Phonology.Feature.anterior else none

def Hansson2010.OnTier (x : Phonology.Segment) : Prop

A segment is on the harmony tier when it has a class.

Equations

• Hansson2010.OnTier x = ((Hansson2010.sibilantClass x).isSome = true)

@[instance_reducible]

instance Hansson2010.instDecidablePredSegmentOnTier : DecidablePred OnTier

Equations

• Hansson2010.instDecidablePredSegmentOnTier x✝ = Hansson2010.instDecidablePredSegmentOnTier._aux_1 x✝

theorem Hansson2010.isSibilant_of_onTier {x : Phonology.Segment} (h : OnTier x) : x.IsSibilant

theorem Hansson2010.sibilantClass_of_onTier {x : Phonology.Segment} (h : OnTier x) : sibilantClass x = x Phonology.Feature.anterior

theorem Hansson2010.setFeature_anterior_isSibilant (x : Phonology.Segment) (v : Bool) : (x.setFeature Phonology.Feature.anterior v).IsSibilant ↔ x.IsSibilant

theorem Hansson2010.sibilantClass_setFeature {x : Phonology.Segment} (h : OnTier x) (v : Bool) : sibilantClass (x.setFeature Phonology.Feature.anterior v) = some v

theorem Hansson2010.onTier_setFeature {x : Phonology.Segment} (h : OnTier x) (v : Bool) : OnTier (x.setFeature Phonology.Feature.anterior v)

Navajo sibilants and the transcriptions

def Hansson2010.sibilant (m : Data.PHOIBLE.FeatureMatrix) : Phonology.Segment

A Navajo sibilant is its chart entry's segment without [distributed].

Equations

• Hansson2010.sibilant m = Phonology.Segment.ofChart m ⊥ {Phonology.Feature.distributed}ᶜ

def Hansson2010.s : Phonology.Segment

The alveolar fricative /s/.

Equations

• Hansson2010.s = Hansson2010.sibilant Data.PHOIBLE.FeatureMatrix.s

def Hansson2010.z : Phonology.Segment

The voiced alveolar fricative /z/.

Equations

• Hansson2010.z = Hansson2010.sibilant Data.PHOIBLE.FeatureMatrix.z

def Hansson2010.esh : Phonology.Segment

The postalveolar fricative /ʃ/.

Equations

• Hansson2010.esh = Hansson2010.sibilant Data.PHOIBLE.FeatureMatrix.«ʃ»

def Hansson2010.ezh : Phonology.Segment

The voiced postalveolar fricative /ʒ/.

Equations

• Hansson2010.ezh = Hansson2010.sibilant Data.PHOIBLE.FeatureMatrix.«ʒ»

def Hansson2010.ts : Phonology.Segment

The alveolar affricate /ts/.

Equations

• Hansson2010.ts = Hansson2010.sibilant Data.PHOIBLE.FeatureMatrix.ts

def Hansson2010.dz : Phonology.Segment

The voiced alveolar affricate /dz/.

Equations

• Hansson2010.dz = Hansson2010.sibilant Data.PHOIBLE.FeatureMatrix.dz

def Hansson2010.tesh : Phonology.Segment

The postalveolar affricate /tʃ/.

Equations

• Hansson2010.tesh = Hansson2010.sibilant Data.PHOIBLE.FeatureMatrix.«t̠ʃ»

def Hansson2010.dezh : Phonology.Segment

The voiced postalveolar affricate /dʒ/.

Equations

• Hansson2010.dezh = Hansson2010.sibilant Data.PHOIBLE.FeatureMatrix.«d̠ʒ»

theorem Hansson2010.eqOn_anterior_compl (p : Phonology.Segment × Phonology.Segment) : p ∈ [(s, esh), (z, ezh), (ts, tesh), (dz, dezh)] → ∀ (f : Phonology.Feature), f ≠ Phonology.Feature.anterior → p.1 f = p.2 f

The two series differ in [anterior] alone, pair by pair.

def Hansson2010.sibilantsOf : List Char → List Phonology.Segment

The sibilants of a transcription, in order, an affricate being written with two letters.

Equations

• Hansson2010.sibilantsOf ('t' :: 's' :: cs) = Hansson2010.ts :: Hansson2010.sibilantsOf cs
• Hansson2010.sibilantsOf ('t' :: 'ʃ' :: cs) = Hansson2010.tesh :: Hansson2010.sibilantsOf cs
• Hansson2010.sibilantsOf ('d' :: 'z' :: cs) = Hansson2010.dz :: Hansson2010.sibilantsOf cs
• Hansson2010.sibilantsOf ('d' :: 'ʒ' :: cs) = Hansson2010.dezh :: Hansson2010.sibilantsOf cs
• Hansson2010.sibilantsOf ('s' :: cs) = Hansson2010.s :: Hansson2010.sibilantsOf cs
• Hansson2010.sibilantsOf ('z' :: cs) = Hansson2010.z :: Hansson2010.sibilantsOf cs
• Hansson2010.sibilantsOf ('ʃ' :: cs) = Hansson2010.esh :: Hansson2010.sibilantsOf cs
• Hansson2010.sibilantsOf ('ʒ' :: cs) = Hansson2010.ezh :: Hansson2010.sibilantsOf cs
• Hansson2010.sibilantsOf (head :: cs) = Hansson2010.sibilantsOf cs
• Hansson2010.sibilantsOf [] = []

def Hansson2010.ur (e : Datum) : List Phonology.Segment

The underlying sibilants of a row, from its underlying feature.

Equations

• Hansson2010.ur e = Hansson2010.sibilantsOf ((e.feature? "underlying").getD "").toList

def Hansson2010.sr (e : Datum) : List Phonology.Segment

The surface sibilants of a row.

Equations

• Hansson2010.sr e = Hansson2010.sibilantsOf e.primaryText.toList

@[reducible, inline]

abbrev Hansson2010.sibilants (w : List Phonology.Segment) : List Phonology.Segment

The sibilants of a word, in order.

Equations

• Hansson2010.sibilants w = List.filter (fun (x : Phonology.Segment) => decide (Hansson2010.OnTier x)) w

theorem Hansson2010.onTier_of_mem_sibilants {w : List Phonology.Segment} {x : Phonology.Segment} (h : x ∈ sibilants w) : OnTier x

The surface language

@[reducible, inline]

abbrev Hansson2010.navajoSibilantHarmony : Subregular.TierStrictlyLocalGrammar 2 Phonology.Segment

The surface phonotactic of section 2.4.1.1 requires adjacent sibilants on the tier to agree in [anterior].

Equations

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

theorem Hansson2010.isTierStrictlyLocal : Language.IsTierStrictlyLocal 2 navajoSibilantHarmony.language

theorem Hansson2010.isBTSL : Language.IsBTSL 2 navajoSibilantHarmony.language

theorem Hansson2010.mem_language_iff (w : List Phonology.Segment) : w ∈ navajoSibilantHarmony.language ↔ ∀ x ∈ sibilants w, ∀ y ∈ sibilants w, x Phonology.Feature.anterior = y Phonology.Feature.anterior

A word is harmonic iff its sibilants agree in [anterior], however far apart.

theorem Hansson2010.language_eq_preimage : navajoSibilantHarmony.language = List.map sibilantClass ⁻¹' (Subregular.TierStrictlyLocalGrammar.agree fun (x : Option Bool) => x.isSome = true).language

The language is the inverse image, under the sibilant class, of agreement among the classes.

Anticipatory harmony, section 1.1

def Hansson2010.trigger (w : List Phonology.Segment) : Option Bool

The trigger is the class of the rightmost sibilant of a word.

Equations

• Hansson2010.trigger w = (Hansson2010.sibilants w).getLast?.bind Hansson2010.sibilantClass

def Hansson2010.harmonize (t : Option Bool) (x : Phonology.Segment) : Phonology.Segment

A sibilant takes the trigger's [anterior] value, and anything off the tier is untouched.

Equations

• Hansson2010.harmonize t x = if Hansson2010.OnTier x then t.elim x (x.setFeature Phonology.Feature.anterior) else x

def Hansson2010.anticipatory (w : List Phonology.Segment) : List Phonology.Segment

Anticipatory sibilant harmony gives every sibilant the class of the rightmost one.

Equations

• Hansson2010.anticipatory w = List.map (Hansson2010.harmonize (Hansson2010.trigger w)) w

theorem Hansson2010.harmonize_of_not_onTier {t : Option Bool} {x : Phonology.Segment} (h : ¬OnTier x) : harmonize t x = x

theorem Hansson2010.harmonize_none (x : Phonology.Segment) : harmonize none x = x

theorem Hansson2010.harmonize_some {x : Phonology.Segment} (h : OnTier x) (v : Bool) : harmonize (some v) x = x.setFeature Phonology.Feature.anterior v

theorem Hansson2010.onTier_harmonize (t : Option Bool) (x : Phonology.Segment) : OnTier (harmonize t x) ↔ OnTier x

theorem Hansson2010.sibilants_map_harmonize (t : Option Bool) (w : List Phonology.Segment) : sibilants (List.map (harmonize t) w) = List.map (harmonize t) (sibilants w)

theorem Hansson2010.trigger_eq_none_iff (w : List Phonology.Segment) : trigger w = none ↔ sibilants w = []

A word has a trigger exactly when it has a sibilant.

theorem Hansson2010.trigger_anticipatory (w : List Phonology.Segment) : trigger (anticipatory w) = trigger w

The harmony leaves the trigger in place, so the rightmost sibilant determines the rest.

theorem Hansson2010.anticipatory_mem_language (w : List Phonology.Segment) : anticipatory w ∈ navajoSibilantHarmony.language

The harmonized word is harmonic.

theorem Hansson2010.anticipatory_eq_self_of_mem {w : List Phonology.Segment} (h : w ∈ navajoSibilantHarmony.language) : anticipatory w = w

A harmonic word is a fixed point of the harmony.

theorem Hansson2010.mem_language_iff_anticipatory_eq (w : List Phonology.Segment) : w ∈ navajoSibilantHarmony.language ↔ anticipatory w = w

The surface language is exactly the set of fixed points of anticipatory harmony: the stringset the tier-based grammar recognizes and the map the harmony computes are one object.

theorem Hansson2010.anticipatory_cons_eq {a b : Phonology.Segment} {w : List Phonology.Segment} (ha : OnTier a) (hb : OnTier b) (hab : ∀ (f : Phonology.Feature), f ≠ Phonology.Feature.anterior → a f = b f) (hw : sibilants w ≠ []) : anticipatory (a :: w) = anticipatory (b :: w)

Neutralization (4): prefixes whose sibilants differ only in [anterior] surface alike once a sibilant follows.

The examples

theorem Hansson2010.anticipatory_rows (e : Datum) : e ∈ Examples.all → e.feature? "directionality" = some "anticipatory" → List.map sibilantClass (anticipatory (ur e)) = List.map sibilantClass (sr e)

The anticipatory examples of (3), (4), (6), (11), (13), and (15): the map takes each underlying form to the classes of its surface sibilants.

theorem Hansson2010.perseveratory_rows (e : Datum) : e ∈ Examples.all → e.feature? "directionality" = some "perseveratory" → List.map sibilantClass (anticipatory (ur e)) ≠ List.map sibilantClass (sr e)

The book's qualification (section 3.1.2): the s-perfective (12) and s-destruct (14) prefixes assimilate the following first-person prefix perseveratively, which the anticipatory map mispredicts.

theorem Hansson2010.ur_ex6a_ii_violates : ur Examples.ex6a_ii ∉ navajoSibilantHarmony.language

The underlying form of (6a) is disharmonic.

theorem Hansson2010.sr_ex6a_ii_legal : sr Examples.ex6a_ii ∈ navajoSibilantHarmony.language

Its surface form is harmonic.

The harmony system

def Hansson2010.navajo : Phonology.Harmony.System Phonology.Segment

Navajo sibilant harmony is the harmony System over segments with [anterior] as its feature, in which the sibilants are targets, all else is transparent, nothing blocks, and the direction is leftward.

Equations

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

theorem Hansson2010.pattern_onTier_iff (x : Phonology.Segment) : navajo.pattern.OnTier x ↔ OnTier x

theorem Hansson2010.pattern_tier (w : List Phonology.Segment) : navajo.pattern.tier w = sibilants w

theorem Hansson2010.saturated : navajo.Saturated

Every sibilant is a participating target with a value.

theorem Hansson2010.tierClosed : navajo.searchCopy.TierClosed

theorem Hansson2010.pattern_project : navajo.pattern.project = sibilantClass

The sibilant class is the system's tier projection.

theorem Hansson2010.harmonic_iff_mem_language (w : List Phonology.Segment) : navajo.pattern.Harmonic w ↔ w ∈ navajoSibilantHarmony.language

The system's surface harmonicity is the tier-based language.

def Hansson2010.first (w : List Phonology.Segment) : Option Bool

The class of the leftmost sibilant of a word.

Equations

• Hansson2010.first w = (Hansson2010.sibilants w).head?.bind Hansson2010.sibilantClass

theorem Hansson2010.scan_eq (w : List Phonology.Segment) : navajo.searchCopy.scan w = List.map (harmonize (first w)) w

The substrate's progressive harmony over the Navajo system gives every sibilant the class of the leftmost one.

theorem Hansson2010.anticipatory_eq_apply (w : List Phonology.Segment) : anticipatory w = navajo.searchCopy.apply w

Anticipatory harmony is the search-and-copy run of the system in its direction.