Jardine (2016): Computationally, tone is different

[Jar16a] (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.twoSidedUnboundedDependence); this file keeps the paper's theorems about it.

Main definitions

• 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_weaklyDeterministic — §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.
• utp_isBimachineComputable — §4.2: UTP is regular, the (43) decomposition read through Elgot–Mezei composition.
• 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.

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 : ¬IsLeftSubsequential Tone.Plateauing.utp.map

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

theorem Jardine2016Tone.utp_not_isRightSubsequential : ¬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 : ScanDirection) : ¬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_weaklyDeterministic : ¬IsNonInteractingBimachineComputable 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

@[instance_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✝

@[instance_reducible]

instance Jardine2016Tone.instReprMark : Repr Mark

Equations

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

def Jardine2016Tone.markLeft : 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 : 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 (Mealy.runRight).

Equations

• Jardine2016Tone.resolve x = Jardine2016Tone.resolveRight.runRight x

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 : IsLeftSubsequential markLeft.run ∧ 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.

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

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

The autosegmental grounding ((40), §4.4)

The string representation reads back from the autosegmental one; the grounding claims are stated on the graph foundation below.

The autosegmental grounding in coordinates

The same claims on the graph foundation: the output representation's melody fuses to one H, linked exactly to the surfacing slots.

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

(7) in coordinates: the merged output's links are the fused H node over the surfacing positions.

theorem Jardine2016Tone.utp_fullyRegular : IsBimachineComputable Tone.Plateauing.utp.map ∧ (∀ (d : ScanDirection), ¬IsSubsequential d Tone.Plateauing.utp.map) ∧ ¬IsNonInteractingBimachineComputable 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.