Jardine (2016): Computationally, tone is different

Jardine argues that unbounded circumambient processes, whose application depends on material unboundedly far away on both sides of the target, (2), are common in tonal phonology and rare in segmental phonology. His witness is unbounded tonal plateauing, every TBU between two H-toned TBUs surfacing H (Hyman and Katamba's rule, (7)), as the string map (36) of Section 4.1, which is Tone.utp. The map is subsequential in neither direction (Section 4.2) but regular: the mark-up decomposition (43), a left-to-right pass writing ? after an H and a right-to-left pass resolving it, is computed by a bimachine. Read back into autosegmental representations by (40), the OCP-merged output is one H linked to the plateau (Section 4.4).

Main results

• utp_map_forms: the map reproduces the plateaus of Section 2.2
• utp_not_isSubsequential: plateauing is subsequential in neither direction
• utp_eq_resolve_mark, utp_isBimachineComputable: the mark-up decomposition (43)

Implementation notes

• The conjecture of Section 5.2, after Heinz and Lai, that plateauing has no mark-up-free decomposition and so is not weakly deterministic, is not stated.
• The words of Data/Forms/Jardine2016a.json carry the paper's string representation one symbol per mora, a long vowel counting two; the Digo, Xhosa and Yaka data, whose plateaus interact with tone shift or an accentual analysis, are not encoded.

References

• [Jar16a]
• [HK10]
• [HL13]
• [EM65]

The plateauing data

The words of Section 2.2 carry their underlying and surface TBU strings in 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, read off the paper's autosegmental diagrams.

def Jardine2016a.tbuString (s : String) : List Tone.TBU

tbuString s is the TBU string spelled s in H and O.

Equations

• Jardine2016a.tbuString s = List.map (fun (c : Char) => if c = 'H' then Tone.TBU.H else Tone.TBU.O) s.toList

def Jardine2016a.ofAnalysis (a : Forms.Analysis) : List Tone.TBU × List Tone.TBU

ofAnalysis a is the underlying and the surface TBU string of the word a analyses.

Equations

• Jardine2016a.ofAnalysis a = (Jardine2016a.tbuString a.underlyingTones, Jardine2016a.tbuString a.surfaceTones)

theorem Jardine2016a.utp_map_forms (a : Forms.Analysis) : a ∈ Forms.analyses → Tone.utp.map (ofAnalysis a).1 = (ofAnalysis a).2

The map (36) reproduces every plateau of Section 2.2, Luganda (8) to (12), Zulu (18b) and Saramaccan (21), with no change for at most one H and a plateau between the outermost Hs otherwise.

UTP is not subsequential

Whether a toneless TBU surfaces H depends on a H arbitrarily far away on each side of it, and the map preserves length, so a machine reading in either direction would have to withhold unboundedly many symbols.

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

UTP is subsequential in neither direction (§4.2, online appendix).

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 that Heinz and Lai's weak determinism disallows.

inductive Jardine2016a.Mark : Type

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

• H : Mark
• O : Mark
• Q : Mark

@[instance_reducible]

instance Jardine2016a.instDecidableEqMark : DecidableEq Mark

Equations

• Jardine2016a.instDecidableEqMark x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Jardine2016a.instReprMark.repr : Mark → ℕ → Std.Format

Equations

• Jardine2016a.instReprMark.repr Jardine2016a.Mark.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2016a.Mark.H")).group prec✝
• Jardine2016a.instReprMark.repr Jardine2016a.Mark.O prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2016a.Mark.O")).group prec✝
• Jardine2016a.instReprMark.repr Jardine2016a.Mark.Q prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2016a.Mark.Q")).group prec✝

@[instance_reducible]

instance Jardine2016a.instReprMark : Repr Mark

Equations

• Jardine2016a.instReprMark = { reprPrec := Jardine2016a.instReprMark.repr }

def Jardine2016a.markLeft : Mealy Bool Tone.TBU Mark

The left pass of (43) marks every toneless TBU after a H with ?.

Equations

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

def Jardine2016a.resolveRight : Mealy Bool Mark Tone.TBU

The right pass of (43), run right-to-left, resolves ? to H when a H follows, else to Ø.

Equations

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

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.

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

The (43) decomposition computes UTP, marking left-to-right and then resolving 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, Mealy.isRightSubsequential).

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 a bimachine computes such a composite, one deterministic pass per direction. What fails above is one-directional determinism, not finite-state computability.

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 and Katamba's rule as given in (7).

theorem Jardine2016a.link_collapse_realize_toAR_map {w : List Tone.TBU} {j k : ℕ} : Autosegmental.AR.link (Autosegmental.AR.collapse (Autosegmental.AR.realize Tone.TBU.toAR (Tone.utp.map w)) true) true false k j ↔ k = 0 ∧ Tone.utp.Surfaces w j

The merged output's links are the fused H over the surfacing positions.