Tonal root nodes and subtonal features

Tone is paradigmatic: a tonal root node (TRN) bundles the two subtonal features [±upper] (which register half) and [±raised] (which target within it) of [Yip80] and [Pul86], each possibly unspecified, and links to a tone-bearing unit. Following [Lio22], the features are paradigmatic targets, not [Sni99]'s syntagmatic shifts; the terracing reading of [raised] is Tone.Register.

Main definitions

• Subtonal, TRN — the two feature dimensions and the root node; TRN.bundleEquiv identifies a root node with its feature bundle Subtonal → Option Bool.
• TRN.H, TRN.M, TRN.L, TRN.superHigh — the four full specifications; TRN.empty, TRN.downstep, TRN.upstep — the register-only nodes.
• TRN.assimilate, TRN.merge, TRN.dock — the feature operations, through the bundle.
• TBUKind, IsRegisterOnly — the tone-bearing unit and [Lio25]'s register-only inventories.

inductive Tone.Subtonal : Type

The two subtonal feature dimensions ([Lio22] ex. 51, after [Yip80], [Pul86]): upper, which register half; raised, which target within it. A value is some true (+), some false (-), or none (unspecified).

• upper : Subtonal
• raised : Subtonal

@[instance_reducible]

instance Tone.instDecidableEqSubtonal : DecidableEq Subtonal

Equations

• Tone.instDecidableEqSubtonal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Tone.instReprSubtonal : Repr Subtonal

Equations

• Tone.instReprSubtonal = { reprPrec := Tone.instReprSubtonal.repr }

def Tone.instReprSubtonal.repr : Subtonal → Nat → Std.Format

Equations

• Tone.instReprSubtonal.repr Tone.Subtonal.upper prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.Subtonal.upper")).group prec✝
• Tone.instReprSubtonal.repr Tone.Subtonal.raised prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.Subtonal.raised")).group prec✝

@[instance_reducible]

instance Tone.instInhabitedSubtonal : Inhabited Subtonal

Equations

• Tone.instInhabitedSubtonal = { default := Tone.instInhabitedSubtonal.default }

structure Tone.TRN : Type

A tonal root node: a [±upper] and a [±raised] value, each possibly unspecified. A structure rather than the bundle Subtonal → Option Bool, so that DecidableEq derives and literals reduce; TRN.bundleEquiv is the bundle view.

• upper : Option Bool
• raised : Option Bool

@[instance_reducible]

instance Tone.instDecidableEqTRN : DecidableEq TRN

Equations

• Tone.instDecidableEqTRN = Tone.instDecidableEqTRN.decEq

def Tone.instDecidableEqTRN.decEq (x✝ x✝¹ : TRN) : Decidable (x✝ = x✝¹)

Equations

• Tone.instDecidableEqTRN.decEq { upper := a, raised := a_1 } { upper := b, raised := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Tone.instReprTRN.repr : TRN → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Tone.instReprTRN : Repr TRN

Equations

• Tone.instReprTRN = { reprPrec := Tone.instReprTRN.repr }

@[instance_reducible]

instance Tone.instInhabitedTRN : Inhabited TRN

Equations

• Tone.instInhabitedTRN = { default := Tone.instInhabitedTRN.default }

@[match_pattern]

def Tone.TRN.empty : TRN

The fully unspecified node.

Equations

• Tone.TRN.empty = { upper := none, raised := none }

@[match_pattern]

def Tone.TRN.downstep : TRN

A floating [-raised]: the downstep node of a register-only system.

Equations

• Tone.TRN.downstep = { upper := none, raised := some false }

@[match_pattern]

def Tone.TRN.upstep : TRN

A floating [+raised]: the upstep node.

Equations

• Tone.TRN.upstep = { upper := none, raised := some true }

@[match_pattern]

def Tone.TRN.H : TRN

High, [+upper, -raised] ([Lio22] ex. 51).

Equations

• Tone.TRN.H = { upper := some true, raised := some false }

@[match_pattern]

def Tone.TRN.M : TRN

Mid, [-upper, +raised] ([Lio22] ex. 51).

Equations

• Tone.TRN.M = { upper := some false, raised := some true }

@[match_pattern]

def Tone.TRN.L : TRN

Low, [-upper, -raised] ([Lio22] ex. 51).

Equations

• Tone.TRN.L = { upper := some false, raised := some false }

@[match_pattern]

def Tone.TRN.superHigh : TRN

The fourth specification [+upper, +raised]: the gap of Laal's three-tone system ([Lio22] ex. 51).

Equations

• Tone.TRN.superHigh = { upper := some true, raised := some true }

def Tone.TRN.toBundle (t : TRN) : Subtonal → Option Bool

The feature bundle of a node.

Equations

• t.toBundle Tone.Subtonal.upper = t.upper
• t.toBundle Tone.Subtonal.raised = t.raised

def Tone.TRN.ofBundle (b : Subtonal → Option Bool) : TRN

The node of a feature bundle.

Equations

• Tone.TRN.ofBundle b = { upper := b Tone.Subtonal.upper, raised := b Tone.Subtonal.raised }

@[simp]

theorem Tone.TRN.toBundle_upper (t : TRN) : t.toBundle Subtonal.upper = t.upper

@[simp]

theorem Tone.TRN.toBundle_raised (t : TRN) : t.toBundle Subtonal.raised = t.raised

@[simp]

theorem Tone.TRN.ofBundle_toBundle (t : TRN) : ofBundle t.toBundle = t

@[simp]

theorem Tone.TRN.toBundle_ofBundle (b : Subtonal → Option Bool) : (ofBundle b).toBundle = b

def Tone.TRN.bundleEquiv : TRN ≃ (Subtonal → Option Bool)

A root node is its feature bundle.

Equations

• Tone.TRN.bundleEquiv = { toFun := Tone.TRN.toBundle, invFun := Tone.TRN.ofBundle, left_inv := Tone.TRN.ofBundle_toBundle, right_inv := Tone.TRN.toBundle_ofBundle }

def Tone.TRN.assimilate (f : Subtonal) (src tgt : TRN) : TRN

Subtonal assimilation at f: the target takes its value at f from the source, its other feature untouched. Laal M-lowering ([Lio22] §5.2) is assimilate .raised: a [-raised] value spreads onto M, [-upper, +raised], giving L.

Equations

• Tone.TRN.assimilate f src tgt = Tone.TRN.ofBundle (Function.update tgt.toBundle f (src.toBundle f))

def Tone.TRN.merge (t₁ t₂ : TRN) : TRN

Merger of two nodes ([Lio22] ex. 53–54): each feature from the left node where it is specified, else from the right — the fusion of two associated tones ([Gol76]); the tier-level merger of a run of identical tones is OCP.collapse.

Equations

• t₁.merge t₂ = Tone.TRN.ofBundle fun (f : Tone.Subtonal) => (t₁.toBundle f).or (t₂.toBundle f)

@[simp]

theorem Tone.TRN.merge_self (t : TRN) : t.merge t = t

def Tone.TRN.dock (f : Subtonal) (v : Bool) (t : TRN) : TRN

Docking of a floating feature ([Lio22] §5.3): a free [±f] lands on a node, overwriting its value at f.

Equations

• Tone.TRN.dock f v t = Tone.TRN.ofBundle (Function.update t.toBundle f (some v))

Tone-bearing units and word-prosodic types

inductive Tone.TBUKind : Type

The prosodic unit that carries a node: the syllable in most tone languages, the mora in Drubea and Numèè ([Lio25]).

• mora : TBUKind
• syllable : TBUKind

@[instance_reducible]

instance Tone.instDecidableEqTBUKind : DecidableEq TBUKind

Equations

• Tone.instDecidableEqTBUKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Tone.instReprTBUKind.repr : TBUKind → Nat → Std.Format

Equations

• Tone.instReprTBUKind.repr Tone.TBUKind.mora prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.TBUKind.mora")).group prec✝
• Tone.instReprTBUKind.repr Tone.TBUKind.syllable prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.TBUKind.syllable")).group prec✝

@[instance_reducible]

instance Tone.instReprTBUKind : Repr TBUKind

Equations

• Tone.instReprTBUKind = { reprPrec := Tone.instReprTBUKind.repr }

def Tone.IsRegisterOnly (ts : List TRN) : Prop

A register-only inventory ([Lio25]): no node specifies [upper], so only the syntagmatic [raised] is contrastive. Lionnet's split of [Hym06]'s tone prototype — register-based systems (Drubea, Numèè) against tone-based ones with paradigmatic [upper] contrasts (Yoruba, Mandarin) and mixed ones (Paicî, Baga Pukur) — is read off the lexical inventory rather than recorded.

Equations

• Tone.IsRegisterOnly ts = ∀ (t : Tone.TRN), t ∈ ts → t.upper = none

@[instance_reducible]

instance Tone.instDecidableIsRegisterOnly (ts : List TRN) : Decidable (IsRegisterOnly ts)

Equations

• Tone.instDecidableIsRegisterOnly ts = List.decidableBAll (fun (t : Tone.TRN) => t.upper = none) ts