McCollum, Baković, Mai and Meinhardt (2020): Unbounded circumambient patterns

ATR harmony in Tutrugbu spreads [+ATR] from the root leftward onto every prefix vowel unless the initial vowel is [+high], in which case a [−high] prefix vowel blocks it. McCollum, Baković, Mai and Meinhardt show that this segmental pattern is unbounded circumambient in Jardine's sense, their (13), like the tonal patterns Jardine took to be special: the surface value of a medial [−high] vowel depends at once on the root to its right and on the initial vowel to its left, however far away both are. No subsequential transducer computes the map in either direction, (27), but a right-to-left pass that leaves some vowels undecided followed by a left-to-right pass that decides them does, (28) and (29), so by Elgot and Mezei's composition theorem the map is regular.

Main definitions

• Seg: a prefix vowel with its height and ATR value, or a root with its ATR value
• Harmonizes: the paper's generalization, the context in which a prefix vowel harmonizes
• tutrugbu: the harmony as a docking process
• markRight, resolveLeft: the two passes of the mark-up analysis

Main results

• tutrugbu_map_forms: the map takes every word of (1) to (8) and (27) to its surface form
• tutrugbu_requiresBothSides, tutrugbu_twoSidedUnboundedDependence: unbounded circumambience, (13)
• tutrugbu_not_isSubsequential: no subsequential analysis in either direction, (27)
• tutrugbu_map_eq_resolve_mark, tutrugbu_isBimachineComputable: the mark-up analysis, and the regularity it shows

Implementation notes

• A word is its prefix vowels and its root, the consonants dropped as in the transducers of the paper's supplementary materials. Prefixes are underlyingly [−ATR] (§2.3.1), and docking raises a prefix vowel to [+ATR].
• The words of Data/Forms/McCollumEtAl2020.json are transcribed from the page images, with the source's misprints recorded in their comments. The vowel of the negation prefix, printed much like ⟨í⟩, is a distinct glyph in the PDF and is read as ⟨ɪ́⟩, as the column headers of (3) and (5) and the tape (26) require.
• Not modelled: the conditionally transparent variant of §2.2, the suffixes and enclitics of (10), and phrasal harmony (11).
• The paper's conclusion that the map is not weakly deterministic uses Heinz and Lai's definition (17) informally, and its fn. 10 records that the definition admits mark-up-free loopholes, so the conclusion is not stated here.

References

• [McCBMM20]
• [Jar16a]
• [HL13]
• [EM65]

The harmony

inductive McCollumEtAl2020.Seg : Type

A segment of a Tutrugbu word as harmony reads it is a prefix vowel with its height and ATR value, or a root with its ATR value.

• pfx (high atr : Bool) : Seg
• root (atr : Bool) : Seg

@[instance_reducible]

instance McCollumEtAl2020.instDecidableEqSeg : DecidableEq Seg

Equations

• McCollumEtAl2020.instDecidableEqSeg = McCollumEtAl2020.instDecidableEqSeg.decEq

def McCollumEtAl2020.instDecidableEqSeg.decEq (x✝ x✝¹ : Seg) : Decidable (x✝ = x✝¹)

Equations

• McCollumEtAl2020.instDecidableEqSeg.decEq (McCollumEtAl2020.Seg.pfx a a_1) (McCollumEtAl2020.Seg.pfx b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• McCollumEtAl2020.instDecidableEqSeg.decEq (McCollumEtAl2020.Seg.pfx high atr) (McCollumEtAl2020.Seg.root atr_1) = isFalse ⋯
• McCollumEtAl2020.instDecidableEqSeg.decEq (McCollumEtAl2020.Seg.root atr) (McCollumEtAl2020.Seg.pfx high atr_1) = isFalse ⋯
• McCollumEtAl2020.instDecidableEqSeg.decEq (McCollumEtAl2020.Seg.root a) (McCollumEtAl2020.Seg.root b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def McCollumEtAl2020.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance McCollumEtAl2020.instReprSeg : Repr Seg

Equations

• McCollumEtAl2020.instReprSeg = { reprPrec := McCollumEtAl2020.instReprSeg.repr }

def McCollumEtAl2020.Seg.raise : Seg → Seg

s.raise is s with [+ATR], if s is a prefix vowel.

Equations

• (McCollumEtAl2020.Seg.pfx h atr).raise = McCollumEtAl2020.Seg.pfx h true
• (McCollumEtAl2020.Seg.root a).raise = McCollumEtAl2020.Seg.root a

def McCollumEtAl2020.Seg.isHigh : Seg → Bool

s.isHigh is the height of a prefix vowel; a root counts as not [+high].

Equations

• (McCollumEtAl2020.Seg.pfx h atr).isHigh = h
• (McCollumEtAl2020.Seg.root a).isHigh = false

def McCollumEtAl2020.InitialHigh (w : List Seg) : Prop

The initial vowel of w is [+high].

Equations

• McCollumEtAl2020.InitialHigh w = ∃ (a : Bool), w.head? = some (McCollumEtAl2020.Seg.pfx true a)

@[instance_reducible]

instance McCollumEtAl2020.instDecidablePredListSegInitialHigh : DecidablePred InitialHigh

Equations

• McCollumEtAl2020.instDecidablePredListSegInitialHigh w = id inferInstance

def McCollumEtAl2020.Harmonizes (w : List Seg) (i : ℕ) : Prop

Prefix vowel i of w harmonizes when a [+ATR] root follows it, unless the initial vowel is [+high] and a [−high] vowel lies at or after i.

Equations

• McCollumEtAl2020.Harmonizes w i = (McCollumEtAl2020.Seg.root true ∈ List.drop (i + 1) w ∧ (McCollumEtAl2020.InitialHigh w → ∀ (a : Bool), McCollumEtAl2020.Seg.pfx false a ∉ List.drop i w))

@[instance_reducible]

instance McCollumEtAl2020.instDecidableHarmonizes (w : List Seg) (i : ℕ) : Decidable (Harmonizes w i)

Equations

• McCollumEtAl2020.instDecidableHarmonizes w i = id inferInstance

def McCollumEtAl2020.tutrugbu : Subregular.Docking Seg

Tutrugbu ATR harmony docks [+ATR] on the prefix vowels that harmonize.

Equations

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

The data

The words of (1) to (8) and (27) are read off their transcriptions: the morphemes of the underlying form give one segment per prefix vowel and one for the root, and the surface vowels are aligned with them.

def McCollumEtAl2020.vowelFeatures : Char → Option (Bool × Bool)

The height and ATR value of the vowel letter c, after the inventory of §2.1, in which ɪ and ʊ are the [+high, −ATR] vowels; any other character is no vowel.

Equations

• McCollumEtAl2020.vowelFeatures 'i' = some (true, true)
• McCollumEtAl2020.vowelFeatures 'í' = some (true, true)
• McCollumEtAl2020.vowelFeatures 'ī' = some (true, true)
• McCollumEtAl2020.vowelFeatures 'u' = some (true, true)
• McCollumEtAl2020.vowelFeatures 'ú' = some (true, true)
• McCollumEtAl2020.vowelFeatures 'ū' = some (true, true)
• McCollumEtAl2020.vowelFeatures 'ɪ' = some (true, false)
• McCollumEtAl2020.vowelFeatures 'ʊ' = some (true, false)
• McCollumEtAl2020.vowelFeatures 'e' = some (false, true)
• McCollumEtAl2020.vowelFeatures 'é' = some (false, true)
• McCollumEtAl2020.vowelFeatures 'ē' = some (false, true)
• McCollumEtAl2020.vowelFeatures 'o' = some (false, true)
• McCollumEtAl2020.vowelFeatures 'ó' = some (false, true)
• McCollumEtAl2020.vowelFeatures 'ō' = some (false, true)
• McCollumEtAl2020.vowelFeatures 'a' = some (false, false)
• McCollumEtAl2020.vowelFeatures 'á' = some (false, false)
• McCollumEtAl2020.vowelFeatures 'ā' = some (false, false)
• McCollumEtAl2020.vowelFeatures 'ɔ' = some (false, false)
• McCollumEtAl2020.vowelFeatures 'ɛ' = some (false, false)
• McCollumEtAl2020.vowelFeatures x✝ = none

def McCollumEtAl2020.ofAnalysis (a : Forms.Analysis) : Option (List Seg × List Seg)

ofAnalysis a is the underlying and the surface string of the word a analyses. The vowels of its underlying form after the last morpheme boundary are the root's, and its surface vowels are aligned with them.

Equations

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

theorem McCollumEtAl2020.tutrugbu_map_forms (a : Forms.Analysis) : a ∈ Forms.analyses → ∃ p ∈ ofAnalysis a, tutrugbu.map p.1 = p.2

The map takes the underlying form of every word of (1) to (8) and (27) to its surface form.

Unbounded circumambience

The witness is a run of [−high] vowels between the initial vowel and the root. With a [−high] initial and a [+ATR] root the whole run harmonizes, as in (8h); a [+high] initial blocks it, as in (8g); a [−ATR] root triggers nothing, as in (5a) against (5d).

theorem McCollumEtAl2020.tutrugbu_requiresBothSides : RequiresBothSides tutrugbu.map

Tutrugbu ATR harmony requires both sides. At every distance a medial [−high] vowel harmonizes, and changing either the initial vowel or the root alone undoes it.

theorem McCollumEtAl2020.tutrugbu_twoSidedUnboundedDependence : TwoSidedUnboundedDependence tutrugbu.map

Tutrugbu ATR harmony is unbounded circumambient in the sense of (13). At every distance one medial vowel changes under a far change on either side.

theorem McCollumEtAl2020.tutrugbu_not_isSubsequential (d : Edge) : ¬IsSubsequential d tutrugbu.map

No subsequential transducer computes Tutrugbu ATR harmony, in either direction, (27).

The mark-up analysis

The right-to-left pass (28), Fig. 8 of the supplementary materials, decides each prefix vowel it can: before a [−ATR] root a vowel stays [−ATR], and a [+high] vowel before a [+ATR] root with no [−high] vowel in between is [+ATR]. From the first [−high] vowel leftward it leaves the value open, writing Ê for a [+high] vowel and Ψ for a [−high] one. The left-to-right pass (29), Fig. 9, reads the height of the initial vowel: if it is [+high] the blocking conditions hold and every open vowel stays [−ATR], and otherwise every open vowel is [+ATR].

inductive McCollumEtAl2020.Mark : Type

A symbol of the intermediate alphabet is a decided segment, or a prefix vowel of known height whose ATR value is left open, Ê when [+high] and Ψ when [−high].

• seg (s : Seg) : Mark
• undecided (high : Bool) : Mark

@[instance_reducible]

instance McCollumEtAl2020.instDecidableEqMark : DecidableEq Mark

Equations

• McCollumEtAl2020.instDecidableEqMark = McCollumEtAl2020.instDecidableEqMark.decEq

def McCollumEtAl2020.instDecidableEqMark.decEq (x✝ x✝¹ : Mark) : Decidable (x✝ = x✝¹)

Equations

• McCollumEtAl2020.instDecidableEqMark.decEq (McCollumEtAl2020.Mark.seg a) (McCollumEtAl2020.Mark.seg b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• McCollumEtAl2020.instDecidableEqMark.decEq (McCollumEtAl2020.Mark.seg s) (McCollumEtAl2020.Mark.undecided high) = isFalse ⋯
• McCollumEtAl2020.instDecidableEqMark.decEq (McCollumEtAl2020.Mark.undecided high) (McCollumEtAl2020.Mark.seg s) = isFalse ⋯
• McCollumEtAl2020.instDecidableEqMark.decEq (McCollumEtAl2020.Mark.undecided a) (McCollumEtAl2020.Mark.undecided b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance McCollumEtAl2020.instReprMark : Repr Mark

Equations

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

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

Equations

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

def McCollumEtAl2020.Mark.isHigh : Mark → Bool

m.isHigh is the height of a marked segment.

Equations

• (McCollumEtAl2020.Mark.seg s).isHigh = s.isHigh
• (McCollumEtAl2020.Mark.undecided h).isHigh = h

def McCollumEtAl2020.markRight : Mealy (Bool × Bool) Seg Mark

The right-to-left pass (28). Its state records whether a [+ATR] root has been read and whether a [−high] vowel has.

Equations

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

def McCollumEtAl2020.resolveLeft : Mealy (Option Bool) Mark Seg

The left-to-right pass (29). Its state records the height of the initial vowel.

Equations

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

theorem McCollumEtAl2020.tutrugbu_map_eq_resolve_mark (w : List Seg) : tutrugbu.map w = resolveLeft.run (markRight.runRight w)

The mark-up analysis computes Tutrugbu ATR harmony, marking right to left and then resolving left to right.

theorem McCollumEtAl2020.tutrugbu_isBimachineComputable : IsBimachineComputable tutrugbu.map

Tutrugbu ATR harmony is regular. The mark-up analysis is a left-to-right Mealy pass after a right-to-left one, and a bimachine computes such a composite.