Two-tier autosegmental representations

A two-tier representation has a melody tier over true and a timing tier over false, labelled by TwoTier α β. AR.ofWords as bs L presents one by its two tier words and a relation L between their positions, the form in which the tone studies write representations; AR.primitive is [Jar19]'s autosegmental graph primitive, a melody over one timing slot. On these presentations the No-Crossing Constraint is order-respecting association, factor embedding is a bounded search over a pair of tier offsets, and the realization of a string of presentations is again one.

Main definitions

• TwoTier α β, AR.ofWords: the two-tier alphabet, and a representation from words.
• AR.primitive: a melody fully associated to one timing slot ([Jar19] Definition 1).
• BlockLinks: the lines of a realized string of presentations.
• AR.SurfacesWith: a timing slot linked to a given melody label.

Main results

• AR.noCrossing_ofWords_iff, AR.noCrossing_primitive: the NCC on presentations, and for primitives ([Jar16b] Theorem 4).
• AR.factorEmbeds_ofWords_iff: factor embedding between presentations, hence decidable.
• AR.free_realize_ofWords_iff: a realized string of presentations reads as one.

References

• [Jar16b]
• [Jar19]

@[reducible, inline]

abbrev Autosegmental.TwoTier (α β : Type u) : Bool → Type u

The two-tier alphabet puts melody labels over true and timing labels over false.

Equations

• Autosegmental.TwoTier α β b = bif b then α else β

@[instance_reducible]

instance Autosegmental.instDecidableEqTwoTierTrue {α β : Type u} [DecidableEq α] : DecidableEq (TwoTier α β true)

Equations

• Autosegmental.instDecidableEqTwoTierTrue = Autosegmental.instDecidableEqTwoTierTrue._aux_1

@[instance_reducible]

instance Autosegmental.instDecidableEqTwoTierFalse {α β : Type u} [DecidableEq β] : DecidableEq (TwoTier α β false)

Equations

• Autosegmental.instDecidableEqTwoTierFalse = Autosegmental.instDecidableEqTwoTierFalse._aux_1

def Autosegmental.TwoTier.words {α β : Type u} (as : List α) (bs : List β) (b : Bool) : List (TwoTier α β b)

The tier words of a melody word and a timing word.

Equations

• Autosegmental.TwoTier.words as bs true = as
• Autosegmental.TwoTier.words as bs false = bs

@[simp]

theorem Autosegmental.TwoTier.words_true {α β : Type u} (as : List α) (bs : List β) : words as bs true = as

@[simp]

theorem Autosegmental.TwoTier.words_false {α β : Type u} (as : List α) (bs : List β) : words as bs false = bs

def Autosegmental.TwoTier.Links (L : ℕ → ℕ → Prop) (i j : Bool) (p q : ℕ) : Prop

Lines from melody position p to timing position q under L.

Equations

• Autosegmental.TwoTier.Links L i j p q = (i = true ∧ j = false ∧ L p q)

@[instance_reducible]

instance Autosegmental.TwoTier.instDecidableLinksOfDecidableRelNat (L : ℕ → ℕ → Prop) [DecidableRel L] (i j : Bool) (p q : ℕ) : Decidable (Links L i j p q)

Equations

• Autosegmental.TwoTier.instDecidableLinksOfDecidableRelNat L i j p q = { decide := decide (i = true) && decide (j = false ∧ L p q), reflects_decide := ⋯ }

Representations from words

def Autosegmental.AR.ofWords {α β : Type u} (as : List α) (bs : List β) (L : ℕ → ℕ → Prop) : TieredAR Bool (TwoTier α β)

The representation of a melody as over a timing word bs, associated by L on positions.

Equations

• Autosegmental.AR.ofWords as bs L = Autosegmental.AR.ofData (Autosegmental.TwoTier.words as bs) (Autosegmental.TwoTier.Links L)

instance Autosegmental.AR.instFiniteVSigmaBoolTwoTierObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesOfWords {α β : Type u} {as : List α} {bs : List β} {L : ℕ → ℕ → Prop} : Finite (ofWords as bs L).obj.V

@[simp]

theorem Autosegmental.AR.tierWord_ofWords_true {α β : Type u} {as : List α} {bs : List β} {L : ℕ → ℕ → Prop} : tierWord true = as

@[simp]

theorem Autosegmental.AR.tierWord_ofWords_false {α β : Type u} {as : List α} {bs : List β} {L : ℕ → ℕ → Prop} : tierWord false = bs

@[simp]

theorem Autosegmental.AR.tierLength_ofWords_true {α β : Type u} {as : List α} {bs : List β} {L : ℕ → ℕ → Prop} : tierLength (ofWords as bs L) true = as.length

@[simp]

theorem Autosegmental.AR.tierLength_ofWords_false {α β : Type u} {as : List α} {bs : List β} {L : ℕ → ℕ → Prop} : tierLength (ofWords as bs L) false = bs.length

@[simp]

theorem Autosegmental.AR.link_ofWords {α β : Type u} {as : List α} {bs : List β} {L : ℕ → ℕ → Prop} {p q : ℕ} : link (ofWords as bs L) true false p q ↔ p < as.length ∧ q < bs.length ∧ L p q

theorem Autosegmental.AR.not_link_ofWords_false {α β : Type u} {as : List α} {bs : List β} (i j : Bool) (p q : ℕ) : ¬link (ofWords as bs fun (x x_1 : ℕ) => False) i j p q

theorem Autosegmental.AR.link_iff_of_true_false {τ : Bool → Type u_1} {X : TieredAR Bool τ} {Y : TieredAR Bool τ} [Finite X.obj.V] [Finite Y.obj.V] (h : ∀ (p q : ℕ), link X true false p q ↔ link Y true false p q) (i j : Bool) (p q : ℕ) : link X i j p q ↔ link Y i j p q

Two-tier links are determined by the melody-to-timing case.

@[reducible, inline]

abbrev Autosegmental.AR.primitive {α β : Type u} (as : List α) (b : β) : TieredAR Bool (TwoTier α β)

An autosegmental graph primitive ([Jar19] Definition 1): one timing slot b, with every node of the melody as associated to it, as in the primitives of gT.

Equations

• Autosegmental.AR.primitive as b = Autosegmental.AR.ofWords as [b] fun (x x_1 : ℕ) => True

The No-Crossing Constraint on two tiers

theorem Autosegmental.AR.noCrossing_iff_two_tier {τ : Bool → Type u_1} (X : TieredAR Bool τ) [Finite X.obj.V] : NoCrossing X.obj.edges X.obj.arcs ↔ MonovaryOn Prod.snd Prod.fst {x : ℕ × ℕ | link X true false x.1 x.2}

On two tiers, the NCC is order-respecting association from melody to timing.

theorem Autosegmental.AR.noCrossing_ofWords_iff {α β : Type u} {as : List α} {bs : List β} {L : ℕ → ℕ → Prop} : NoCrossing (ofWords as bs L).obj.edges (ofWords as bs L).obj.arcs ↔ MonovaryOn Prod.snd Prod.fst {x : ℕ × ℕ | x.1 < as.length ∧ x.2 < bs.length ∧ L x.1 x.2}

theorem Autosegmental.AR.noCrossing_of_tierLength_false_le_one {τ : Bool → Type u_1} (X : TieredAR Bool τ) [Finite X.obj.V] (h : tierLength X false ≤ 1) : NoCrossing X.obj.edges X.obj.arcs

A two-tier representation with at most one timing slot obeys the NCC.

theorem Autosegmental.AR.noCrossing_primitive {α β : Type u} (as : List α) (b : β) : NoCrossing (primitive as b).obj.edges (primitive as b).obj.arcs

Primitives obey the NCC, having one timing slot ([Jar16b] Theorem 4).

Factor embedding

theorem Autosegmental.AR.factorEmbeds_ofWords_iff {α β : Type u} {as as' : List α} {bs bs' : List β} {L L' : ℕ → ℕ → Prop} : FactorEmbeds (ofWords as bs L) (ofWords as' bs' L') ↔ ∃ ot ≤ as'.length, ∃ of ≤ bs'.length, as <+: List.drop ot as' ∧ bs <+: List.drop of bs' ∧ ∀ p < as.length, ∀ q < bs.length, L p q → L' (p + ot) (q + of)

One presentation embeds in another as a factor iff its tier words occur in the host's at a pair of bounded offsets and its lines transport there.

@[instance_reducible]

instance Autosegmental.AR.instDecidableFactorEmbedsBoolTwoTierOfWordsOfDecidableEqOfDecidableRelNat {α β : Type u} {as as' : List α} {bs bs' : List β} {L L' : ℕ → ℕ → Prop} [DecidableEq α] [DecidableEq β] [DecidableRel L] [DecidableRel L'] : Decidable (FactorEmbeds (ofWords as bs L) (ofWords as' bs' L'))

Equations

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

Realization of strings of presentations

def Autosegmental.BlockLinks {α β : Type u} {S : Type u_1} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) : List S → ℕ → ℕ → Prop

A line of a string of presentations lies inside the first symbol's presentation, or past its tier lengths inside the rest.

Equations

• One or more equations did not get rendered due to their size.
• Autosegmental.BlockLinks as bs L [] x✝¹ x✝ = False

@[instance_reducible]

instance Autosegmental.instDecidableRelNatBlockLinks {α β : Type u} {S : Type u_1} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) [(s : S) → DecidableRel (L s)] (w : List S) : DecidableRel (BlockLinks as bs L w)

Equations

• One or more equations did not get rendered due to their size.
• Autosegmental.instDecidableRelNatBlockLinks as bs L [] x✝¹ x✝ = { decide := false, reflects_decide := ⋯ }

theorem Autosegmental.BlockLinks.lt {α β : Type u} {S : Type u_1} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) {w : List S} {p q : ℕ} (h : BlockLinks as bs L w p q) : p < (List.map as w).flatten.length ∧ q < (List.map bs w).flatten.length

theorem Autosegmental.AR.tierWord_realize_ofWords_true {α β : Type u} {S : Type u_1} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (w : List S) : tierWord true = (List.map as w).flatten

theorem Autosegmental.AR.tierWord_realize_ofWords_false {α β : Type u} {S : Type u_1} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (w : List S) : tierWord false = (List.map bs w).flatten

theorem Autosegmental.AR.link_realize_ofWords {α β : Type u} {S : Type u_1} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (w : List S) (p q : ℕ) : link (realize (fun (s : S) => ofWords (as s) (bs s) (L s)) w) true false p q ↔ BlockLinks as bs L w p q

theorem Autosegmental.AR.link_realize_iff_link_ofWords {α β : Type u} {S : Type u_1} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (w : List S) (i j : Bool) (p q : ℕ) : link (realize (fun (s : S) => ofWords (as s) (bs s) (L s)) w) i j p q ↔ link (ofWords (List.map as w).flatten (List.map bs w).flatten (BlockLinks as bs L w)) i j p q

A realized string of presentations has the links of one presentation.

theorem Autosegmental.AR.free_realize_ofWords_iff {α β : Type u} {S : Type u_1} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (B : List { F : TieredAR Bool (TwoTier α β) // Finite F.obj.V }) (w : List S) : Free (realize (fun (s : S) => ofWords (as s) (bs s) (L s)) w) B ↔ Free (ofWords (List.map as w).flatten (List.map bs w).flatten (BlockLinks as bs L w)) B

def Autosegmental.AR.SurfacesWith {α β : Type u} (X : TieredAR Bool (TwoTier α β)) [Finite X.obj.V] (a : α) (j : ℕ) : Prop

Timing slot j surfaces with melody label a when some a-labelled melody node links to it.

Equations

• Autosegmental.AR.SurfacesWith X a j = ∃ (k : ℕ), Autosegmental.AR.link X true false k j ∧ (Autosegmental.AR.tierWord true)[k]? = some a