Documentation

Studies.McMullin2016

McMullin (2016): Tier-Based Locality in Long-Distance Phonotactics #

This file formalizes McMullin's argument for the tier-based description of long-distance phonotactics. A long-distance constraint can be stated over subsequences, a forbidden pair of segments however far apart, the strictly piecewise description, or over a tier projection, deleting transparent material and forbidding adjacent pairs, the tier-based strictly local description; the thesis argues for the tier-based class, since strictly piecewise grammars cannot see a blocker, an intervening segment that halts harmony, deletion never turning a legal word illegal. Both halves are stated. Transparent harmony, the Navajo sibilant harmony Hansson describes, is one stringset under either description, as every agreement language is strictly piecewise of width two, agreement being transitive; opaque harmony with a blocker is tier-based strictly local of width two but strictly piecewise at no width, since deleting the blocker leaves an illegal word and strictly piecewise languages are closed under subsequence.

Implementation notes #

The blocking alphabet is schematic, one blocker, one transparent segment, and the two harmonizing series, and stands in for no particular language; the attested opaque consonant-harmony systems surveyed by Hansson are not formalized.

References #

Transparent harmony: Navajo is SP_2 as well as TSL_2 #

source
theorem McMullin2016.navajoSibilantHarmony_lang_isSP2 :
Hansson2010.navajoSibilantHarmony.language.IsStrictlyPiecewise 2

Navajo sibilant harmony is strictly 2-piecewise. The subject is the very language Studies/Hansson2010.lean builds as TSL_2, the inverse image of agreement among the sibilant classes, and agreement is strictly 2-piecewise.

source
theorem McMullin2016.navajoSibilantHarmony_language_eq_sp :
Hansson2010.navajoSibilantHarmony.language = List.map Hansson2010.sibilantClass ⁻¹' StrictlyPiecewiseGrammar.language 2 (Subregular.StrictlyPiecewiseGrammar.agree fun (x : Option Bool) => x.isSome = true)

The tier-based and subsequence-based grammars for Navajo generate the same language, read through the sibilant classes.

source
theorem McMullin2016.ur_ex6a_ii_violates_sp :
Hansson2010.ur Hansson2010.Examples.ex6a_ii ∉ List.map Hansson2010.sibilantClass ⁻¹' StrictlyPiecewiseGrammar.language 2 (Subregular.StrictlyPiecewiseGrammar.agree fun (x : Option Bool) => x.isSome = true)

Under the SP_2 description Hansson's minimal pair comes out as before, the pre-harmony /si-dʒéːʔ/ rejected and the surface [ʃidʒéːʔ] accepted. Both transfer along the equality of languages rather than being recomputed.

Opaque harmony: blocking is strictly piecewise at no width #

source
inductive McMullin2016.BSeg :
Type

A schematic alphabet for an opaque long-distance pattern has 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 projects onto the tier, so it interrupts the harmony.

  • transparent : BSeg

    Transparent material is off the tier, hence invisible to the constraint.

Instances For
    source
    @[instance_reducible]
    instance McMullin2016.instDecidableEqBSeg :
    DecidableEq BSeg
    Equations
    source
    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
    Instances For
      source
      @[instance_reducible]
      instance McMullin2016.instDecidablePredBSegOnTier :
      DecidablePred BSeg.onTier
      Equations
      source
      def McMullin2016.BSeg.Mixed :
      BSeg → BSeg → Prop

      The two series may not be tier-adjacent.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance McMullin2016.instDecidableRelBSegMixed :
        DecidableRel BSeg.Mixed
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def McMullin2016.blockingLang :
        Language BSeg

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

        Equations
        Instances For
          source
          theorem McMullin2016.blockingLang_isTSL2 :
          Language.IsTierStrictlyLocal 2 blockingLang
          source
          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.

          source
          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.

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

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

          source
          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.

          source
          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.