McMullin (2016) [McM16]

Tier-based locality in long-distance phonotactics: learnability and typology. PhD thesis, University of British Columbia.

A long-distance phonotactic can be stated over subsequences — a forbidden pair of segments however far apart, the strictly piecewise (SP) description — or over a tier projection — delete the transparent material, then forbid adjacent pairs, the tier-based strictly local (TSL) description. [McM16] argues for the tier-based class: SP grammars cannot see a blocker, an intervening segment that halts harmony, because deleting material can never turn an SP-legal word illegal.

Both halves are formalised here.

• Transparent harmony: the classes coincide. Navajo sibilant harmony — the [Han10] case study formalised as TSL_2 in Studies/Hansson2010.lean — is the same stringset as an SP_2 grammar. This is not an artefact of the toy alphabet: every AGREE language is SP_2 (Subregular.TSLGrammar.agree_lang_eq_sp), because equality is transitive, so constraining tier-adjacent pairs already constrains pairs at arbitrary distance.
• Opaque harmony: they come apart. A blocking pattern is TSL_2 but SP at no width, since deleting the blocker leaves an illegal word and SP languages are subsequence-closed.

The blocking alphabet BSeg is schematic — one blocker, one transparent segment, and the two harmonizing series — and stands in for no particular language. Opaque consonant-harmony systems are rare; [Han10] surveys the attested cases and none is formalised here.

Transparent harmony: Navajo is SP_2 as well as TSL_2

theorem McMullin2016.navajoSibilantHarmony_lang_isSP2 : Phonology.Studies.Hansson2010.navajoSibilantHarmony.lang.IsStrictlyPiecewise 2

Navajo sibilant harmony is strictly 2-piecewise. The subject is the very language Studies/Hansson2010.lean builds as TSL_2, not a parallel SP stipulation, so the two classifications are of one stringset by construction.

theorem McMullin2016.navajoSibilantHarmony_lang_eq_sp : Phonology.Studies.Hansson2010.navajoSibilantHarmony.lang = SPGrammar.language 2 (Subregular.SPGrammar.agree Phonology.Studies.Hansson2010.NSeg.onTier)

The tier-based and subsequence-based grammars for Navajo generate the same language — the instance at NSeg.onTier of TSLGrammar.agree_lang_eq_sp.

theorem McMullin2016.preSiDze_violates_sp : Phonology.Studies.Hansson2010.preSiDze ∉ SPGrammar.language 2 (Subregular.SPGrammar.agree Phonology.Studies.Hansson2010.NSeg.onTier)

[Han10]'s minimal pair under the SP_2 description: the pre-harmony /si-dʒéːʔ/ is rejected and the surface [ʃidʒéːʔ] accepted. Both transfer along the equality of languages rather than being recomputed.

theorem McMullin2016.postShiDze_legal_sp : Phonology.Studies.Hansson2010.postShiDze ∈ SPGrammar.language 2 (Subregular.SPGrammar.agree Phonology.Studies.Hansson2010.NSeg.onTier)

Opaque harmony: blocking is strictly piecewise at no width

inductive McMullin2016.BSeg : Type

A schematic alphabet for an opaque long-distance pattern: the two harmonizing series, a blocker, and transparent material.

• ant : BSeg

  Anterior member of the harmonizing series.

• post : BSeg

  Posterior member of the harmonizing series.

• blocker : BSeg

  The blocker: it projects onto the tier, so it interrupts the harmony.

• transparent : BSeg

  Transparent material: off-tier, hence invisible to the constraint.

@[instance_reducible]

instance McMullin2016.instDecidableEqBSeg : DecidableEq BSeg

Equations

• McMullin2016.instDecidableEqBSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def McMullin2016.BSeg.onTier (s : BSeg) : Prop

Everything but the transparent segment projects. A blocker is a segment that the tier keeps — that is the whole of its opacity.

Equations

• s.onTier = (s ≠ McMullin2016.BSeg.transparent)

@[instance_reducible]

instance McMullin2016.instDecidablePredBSegOnTier : DecidablePred BSeg.onTier

Equations

• McMullin2016.instDecidablePredBSegOnTier s = McMullin2016.instDecidablePredBSegOnTier._aux_1 s

def McMullin2016.BSeg.Mixed : BSeg → BSeg → Prop

The forbidden tier-adjacent pairs: the two series may not be tier-adjacent.

Equations

• McMullin2016.BSeg.ant.Mixed McMullin2016.BSeg.post = True
• McMullin2016.BSeg.post.Mixed McMullin2016.BSeg.ant = True
• x✝¹.Mixed x✝ = False

@[instance_reducible]

instance McMullin2016.instDecidableRelBSegMixed : DecidableRel BSeg.Mixed

Equations

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

def McMullin2016.blockingLang : Language BSeg

The schematic blocking language: harmony across transparent material, halted by a blocker.

Equations

• McMullin2016.blockingLang = (Subregular.TSLGrammar.ofForbiddenPairs McMullin2016.BSeg.Mixed McMullin2016.BSeg.onTier).lang

theorem McMullin2016.blockingLang_isTSL2 : Language.IsTierStrictlyLocal 2 blockingLang

theorem McMullin2016.transparent_not_mem : [BSeg.ant, BSeg.transparent, BSeg.post] ∉ blockingLang

Transparent material does not license a mixed pair: it is deleted by the projection, leaving the two series tier-adjacent.

theorem McMullin2016.blocked_mem : [BSeg.ant, BSeg.blocker, BSeg.post] ∈ blockingLang

A blocker does license it: the blocker projects, so the two series are no longer tier-adjacent.

theorem McMullin2016.unblocked_not_mem : [BSeg.ant, BSeg.post] ∉ blockingLang

Deleting the blocker leaves an illegal word — the configuration no subsequence grammar can distinguish.

theorem McMullin2016.blockingLang_not_isStrictlyPiecewise (k : ℕ) : ¬blockingLang.IsStrictlyPiecewise k

Blocking is not strictly piecewise, at any width ([McM16]). SP languages are subsequence-closed, so a legal word whose blocker-deletion is illegal rules out every SP grammar at once.

theorem McMullin2016.exists_isTierStrictlyLocal_not_isStrictlyPiecewise : ∃ (L : Language BSeg), Language.IsTierStrictlyLocal 2 L ∧ ∀ (k : ℕ), ¬L.IsStrictlyPiecewise k

The tier buys expressive power ([McM16]): some TSL_2 language is strictly piecewise at no width. With navajoSibilantHarmony_lang_isSP2 — where the two descriptions do coincide — this is the thesis's typological argument in miniature: SP suffices for transparency, and only for transparency.