Documentation

Linglib.Studies.Jardine2016a

Jardine (2016): Computationally, tone is different #

This file formalizes [jardine-2016a], the computational characterization of a typological asymmetry: unbounded circumambient processes, whose application depends on unboundedly distant material on both sides of the target, (2), are common in tonal phonology and rare in segmental phonology, and they are the attested maps beyond weak determinism. The witness is unbounded tonal plateauing, every TBU between two H-toned TBUs surfacing H ([hyman-katamba-2010]'s rule, (7)), as the string map (36) of Section 4.1 over H and Ø, which is Tone.utp and reproduces the plateaus of Section 2.2 (utp_map_rows). The map is neither left- nor right-subsequential, Section 4.2 (utp_not_isSubsequential), by bounded delay and the reversal symmetry; it is regular, since the mark-up decomposition (43), a left-to-right pass writing ? after a H and a right-to-left pass resolving ?, is a bimachine ([elgot-mezei-1965], utp_eq_resolve_mark, utp_isBimachineComputable); and it is not weakly deterministic, Section 5.2, no union of one-sided rules expressing a map that requires both sides (utp_not_weaklyDeterministic), so it is fully regular, the class Section 5.3 places tone in and bars segmental phonology from (utp_fullyRegular). Read back into autosegmental representations by (40), the OCP-merged output is one H linked to the plateau, Section 4.4.

Implementation notes #

References #

The plateauing data #

The paper's string representation of Section 4.1, one symbol per mora, H a TBU associated to a H tone and Ø, written O, an unspecified one.

source
structure Jardine2016a.Row :
Type

A row of Section 2.2: the underlying and surface TBU strings.

Instances For
    source
    def Jardine2016a.instDecidableEqRow.decEq (x✝ x✝¹ : Row) :
    Decidable (x✝ = x✝¹)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Jardine2016a.instDecidableEqRow :
      DecidableEq Row
      Equations
      source
      def Jardine2016a.tbuString (s : String) :
      List Tone.TBU

      A TBU string from its H/O spelling.

      Equations
      Instances For
        source
        def Jardine2016a.Row.ofExample (e : Data.Examples.LinguisticExample) :
        Option Row

        A row from the paper's features.

        Equations
        Instances For
          source
          def Jardine2016a.rows :
          List Row

          The plateauing data of Section 2.2: Luganda (8) to (12), Zulu (18b) and Saramaccan (21).

          Equations
          Instances For
            source
            theorem Jardine2016a.utp_map_rows (r : Row) :
            r ∈ rows → Tone.utp.map r.underlying = r.surface

            The map (36) reproduces every row: no change with at most one H, a plateau between the outermost Hs otherwise.

            UTP is not subsequential #

            By bounded delay: a left machine reading H Øⁿ⁺¹ has emitted at most one symbol, since utp.map (H Øⁿ⁺¹) = H Øⁿ⁺¹ and utp.map (H Øⁿ⁺¹ H) = Hⁿ⁺³ already differ at position 1; so it withholds n + 1 symbols.

            source
            theorem Jardine2016a.utp_not_isLeftSubsequential :
            ¬IsLeftSubsequential Tone.utp.map

            UTP is not left-subsequential (§4.2, online appendix).

            source
            theorem Jardine2016a.utp_not_isRightSubsequential :
            ¬IsRightSubsequential Tone.utp.map

            UTP is not right-subsequential: by the reversal symmetry, a right machine faces the mirror-image unbounded look-ahead.

            source
            theorem Jardine2016a.utp_not_isSubsequential (d : ScanDirection) :
            ¬IsSubsequential d Tone.utp.map

            UTP is subsequential in neither direction.

            UTP is not weakly deterministic #

            Under the non-interacting-bimachine rendering of weak determinism, the conjecture of Section 5.2, that UTP has no mark-up-free decomposition, is a theorem: UTP RequiresBothSides, which no union of one-sided rules expresses.

            source
            theorem Jardine2016a.utp_not_weaklyDeterministic :
            ¬IsNonInteractingBimachineComputable Tone.utp.map

            UTP is not weakly deterministic (§5.2).

            The (43) mark-up decomposition #

            With one extra symbol the two-pass decomposition exists: a left pass marks every toneless TBU after a H with ?; a right pass resolves ? by whether a H follows. The mark is exactly the alphabet enlargement weak determinism disallows, so with the impossibility theorem this locates UTP precisely.

            source
            inductive Jardine2016a.Mark :
            Type

            The mark-up alphabet of (43): Q is the paper's ?.

            Instances For
              source
              @[instance_reducible]
              instance Jardine2016a.instDecidableEqMark :
              DecidableEq Mark
              Equations
              source
              @[instance_reducible]
              instance Jardine2016a.instReprMark :
              Repr Mark
              Equations
              source
              def Jardine2016a.instReprMark.repr :
              Mark → ℕ → Std.Format
              Equations
              Instances For
                source
                def Jardine2016a.markLeft :
                Mealy Bool Tone.TBU Mark

                Left pass of (43): mark every toneless TBU after a H with ?.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Jardine2016a.resolveRight :
                  Mealy Bool Mark Tone.TBU

                  Right pass of (43), run right-to-left: resolve ? to H when a H follows, else to Ø.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem Jardine2016a.markLeft_run_getElem?_H_iff {w : List Tone.TBU} {j : ℕ} :
                    (markLeft.run w)[j]? = some Mark.H ↔ w[j]? = some Tone.TBU.H

                    The left pass writes H exactly where the input has H.

                    source
                    theorem Jardine2016a.utp_eq_resolve_mark (w : List Tone.TBU) :
                    Tone.utp.map w = resolveRight.runRight (markLeft.run w)

                    The (43) decomposition computes UTP: mark left-to-right, then resolve right-to-left. Both passes run finite Mealy machines, so this exhibits UTP as a right-subsequential map after a left-subsequential one (Mealy.isLeftSubsequential_run, Mealy.isRightSubsequential_runRight).

                    source
                    theorem Jardine2016a.utp_isBimachineComputable :
                    IsBimachineComputable Tone.utp.map

                    UTP is regular (§4.2): the (43) decomposition is a right-to-left Mealy pass after a left-to-right one, and such a composite is computed by a bimachine — one deterministic pass per direction ([elgot-mezei-1965]). So what fails above is one-directional determinism, not finite-state computability.

                    source
                    theorem Jardine2016a.utp_fullyRegular :
                    IsBimachineComputable Tone.utp.map ∧ ¬IsNonInteractingBimachineComputable Tone.utp.map

                    UTP is fully regular (§5.3): regular but not weakly deterministic — the class the paper places tone in and bars segmental phonology from.

                    The autosegmental reading (§4.4) #

                    The string representation reads back into autosegmental representations by TBU.toAR ((40)); the OCP-merged representation of the output has one H, linked exactly to the plateau — [hyman-katamba-2010]'s rule as given in (7).