Jardine (2016): Computationally, tone is different

[Jar16] (Phonology 33) characterises a typological asymmetry computationally: unbounded circumambient processes — application depends on unboundedly distant material on both sides of the target — are common in tone but rare in segmental phonology, and they are exactly the attested maps exceeding weak determinism. The flagship witness is unbounded tonal plateauing (UTP; [HK10]): every TBU between two H-toned TBUs surfaces H. This file formalizes the paper's formal skeleton over its string representation (§4.1: H a H-toned TBU, O the paper's Ø).

The map itself and its plateau/circumambience API live in Phonology/Tone/Plateauing (the rule set (36) as utp.map_toneless/utp.map_single/utp.map_plateau; definition (2) as utp.isUnboundedCircumambient); this file keeps the paper's theorems about it.

Main definitions

• utpBM — a bimachine computing UTP.
• markLeft, resolve — the (43) two-pass decomposition over the ?-enlarged alphabet.
• toAR — the (40) translation into autosegmental representations.

Main results

• utp_not_isSubsequential — the central theorem (§4.2, online appendix): no deterministic FST computes UTP in either direction, via IsLeftSubsequential.bounded_delay and the reversal symmetry utp.map_reverse.
• utp_not_isBimachineWeaklyDeterministic — §5.2, via RequiresBothSides: no union of one-sided rules expresses UTP's conjunctive trigger.
• utp_markup_decomposition — (43): with the mark ?, UTP is right-subsequential after left-subsequential; weak determinism forbids exactly this enlargement.
• readTBU_linearize_realize — §4.4: the TBU string is the linearization of the realized AR ((37a)), so string look-ahead is timing-tier look-ahead.
• links_realizeMerged_utp, upper_realizeMerged_utp — the OCP-merged realization of the UTP output is a single H multiply linked to the plateau ([HK10] (7)).
• utp_fullyRegular — §7: UTP is regular but neither subsequential nor weakly deterministic.

Contrast Studies/MeinhardtEtAl2024: ATR spreading is circumambient as covariation yet weakly deterministic; UTP's RequiresBothSides pushes it above that bound.

UTP is regular

§4.2 exhibits a nondeterministic FST (Fig. 5); here UTP is computed by a bimachine — one deterministic pass per direction — so what fails below is one-directional determinism.

def Jardine2016Tone.utpBM : Subregular.Bimachine Bool Bool Tone.Plateauing.TBU Tone.Plateauing.TBU

The UTP bimachine: each side flags "a H occurs on my side"; a toneless cell surfaces H exactly when both flags are set.

Equations

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

theorem Jardine2016Tone.utpBM_run : utpBM.run = Tone.Plateauing.utp.map

The bimachine computes UTP.

theorem Jardine2016Tone.utp_isBimachineComputable : Subregular.IsBimachineComputable Tone.Plateauing.utp.map

UTP is regular (§4.2): computable by a finite bimachine.

UTP is not subsequential

The paper's central theorem (§4.2, online appendix), by bounded delay: a left machine reading H Øⁿ has emitted at most one symbol (utp.map (H Øⁿ) = H Øⁿ and utp.map (H Øⁿ H) = H^(n+2) diverge at position 1), so it withholds n symbols.

theorem Jardine2016Tone.utp_not_isLeftSubsequential : ¬Subregular.IsLeftSubsequential Tone.Plateauing.utp.map

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

theorem Jardine2016Tone.utp_not_isRightSubsequential : ¬Subregular.IsRightSubsequential Tone.Plateauing.utp.map

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

theorem Jardine2016Tone.utp_not_isSubsequential (d : Subregular.Direction) : ¬Subregular.IsSubsequential d Tone.Plateauing.utp.map

UTP is subsequential in neither direction.

UTP is not weakly deterministic

Under the non-interacting-bimachine rendering of [HL13]'s weak determinism, §5.2's claim is a theorem: UTP RequiresBothSides, which no union of one-sided rules expresses.

theorem Jardine2016Tone.utp_not_isBimachineWeaklyDeterministic : ¬Subregular.IsBimachineWeaklyDeterministic Tone.Plateauing.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.

inductive Jardine2016Tone.Mark : Type

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

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

@[implicit_reducible]

instance Jardine2016Tone.instDecidableEqMark : DecidableEq Mark

Equations

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

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

Equations

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

@[implicit_reducible]

instance Jardine2016Tone.instReprMark : Repr Mark

Equations

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

def Jardine2016Tone.markLeft : Subregular.Mealy Bool Tone.Plateauing.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.

def Jardine2016Tone.resolveRight : Subregular.Mealy Bool Mark Tone.Plateauing.TBU

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

Equations

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

def Jardine2016Tone.resolve (x : List Mark) : List Tone.Plateauing.TBU

The right pass as a right-to-left string function: reverse, run, reverse.

Equations

• Jardine2016Tone.resolve x = (Jardine2016Tone.resolveRight.run x.reverse).reverse

theorem Jardine2016Tone.utp_eq_resolve_mark (w : List Tone.Plateauing.TBU) : Tone.Plateauing.utp.map w = resolve (markLeft.run w)

The (43) decomposition computes UTP.

theorem Jardine2016Tone.utp_markup_decomposition : Subregular.IsLeftSubsequential markLeft.run ∧ Subregular.IsRightSubsequential resolve ∧ Tone.Plateauing.utp.map = resolve ∘ markLeft.run

The (43) mark-up decomposition (§5.2): over the ?-enlarged alphabet, UTP is a right-subsequential map after a left-subsequential map.

The autosegmental grounding ((40), §4.4)

The string representation is the linearisation of the autosegmental one: toAR is the paper's (40) translation, and by Autosegmental.linearize_realize the association-state string of the realized AR is the input string. So the TBU string is recoverable from the AR ((37a)) and string look-ahead is timing-tier look-ahead ((37b)).

def Jardine2016Tone.readTBU (s : Unit × List Tone.TRN) : Tone.Plateauing.TBU

Read a timing unit's association state back as a TBU symbol.

Equations

• Jardine2016Tone.readTBU s = if s.2.isEmpty = true then Tone.Plateauing.TBU.O else Tone.Plateauing.TBU.H

theorem Jardine2016Tone.readTBU_linearize_realize (w : List Tone.Plateauing.TBU) : List.map readTBU (Autosegmental.realize Tone.Plateauing.toAR w).linearize = w

(37a): the TBU string is recoverable from the realized AR, so the complexity results transfer to the autosegmental analysis.

The fused plateau ([HK10] (7))

The OCP-merging realization Autosegmental.realizeMerged fuses the plateau's run of H nodes into one, giving [HK10]'s output representation (7): a single H autosegment multiply linked to exactly the plateau, over an unchanged timing tier.

theorem Jardine2016Tone.mem_links_realizeMerged_utp {w : List Tone.Plateauing.TBU} (p : ℕ × ℕ) : p ∈ (Autosegmental.realizeMerged Tone.Plateauing.toAR (Tone.Plateauing.utp.map w)).links ↔ p.1 = 0 ∧ Tone.Plateauing.utp.Surfaces w p.2

theorem Jardine2016Tone.links_realizeMerged_utp {w : List Tone.Plateauing.TBU} : (Autosegmental.realizeMerged Tone.Plateauing.toAR (Tone.Plateauing.utp.map w)).links = {0} ×ˢ Tone.Plateauing.plateau w

Multiple association ((7)): the merged realization links melody node 0 to exactly the plateau. Unconditional: a toneless word has an empty plateau and no lines.

theorem Jardine2016Tone.lower_realizeMerged_utp {w : List Tone.Plateauing.TBU} : (Autosegmental.realizeMerged Tone.Plateauing.toAR (Tone.Plateauing.utp.map w)).lower.toList = List.replicate w.length ()

The timing tier survives the merge: one slot per input TBU.

theorem Jardine2016Tone.upper_realizeMerged_utp {w : List Tone.Plateauing.TBU} (hw : Tone.Plateauing.TBU.H ∈ w) : (Autosegmental.realizeMerged Tone.Plateauing.toAR (Tone.Plateauing.utp.map w)).upper.toList = [Tone.TRN.H]

The fused plateau ((7)): with at least one H, the merged melody tier is a single H autosegment.

theorem Jardine2016Tone.utp_fullyRegular : Subregular.IsBimachineComputable Tone.Plateauing.utp.map ∧ (∀ (d : Subregular.Direction), ¬Subregular.IsSubsequential d Tone.Plateauing.utp.map) ∧ ¬Subregular.IsBimachineWeaklyDeterministic Tone.Plateauing.utp.map

Computationally, tone is different (§7): UTP is fully regular — regular but neither subsequential in either direction nor weakly deterministic, the bound segmental phonology respects.