Merging concatenation of autosegmental representations

Jardine and Heinz concatenate two representations by bridging them and merging the seam: on the melody tier, the last node of the first factor and the first node of the second become one node when they bear the same label, and that node keeps the lines of both. AR.mergeConcat m X Y is this concatenation, the repointing of X ⊗ Y along OCP.mergeIdx. A string realizes as the left fold of merging concatenation over its symbols' primitives (AR.mergeRealize).

The merge happens at the seam only, so a primitive that itself violates the OCP keeps its violation. Collapsing every run after concatenating, as realizeMerged does, would merge it away. The two realizations agree when the primitives are OCP-clean, because the collapse of a concatenation is the merging concatenation of the collapses.

Main definitions

• AR.mergeConcat: concatenation with the melody seam merged.
• AR.mergeRealize: the realization of a string as a left fold of merging concatenation.

Main statements

• AR.mergeConcatAssocFullIso: merging concatenation is associative.
• AR.noCrossing_mergeConcat, AR.isCleanAt_mergeConcat: it preserves the NCC, and the OCP of OCP-clean factors.
• AR.collapseTensorFullIso: the collapse of a concatenation is the merging concatenation of the collapses.
• AR.nonempty_fullIso_realizeMerged: over OCP-clean primitives, the realization by merging concatenation is the collapsed realization.

Implementation notes

Jardine and Heinz merge at every melody tier; mergeConcat merges at one tier m, the two-tier case their primitives assume. They prove associativity for the graphs generated from primitives, whose tiers are strings; Axioms 1 and 2 make every tier a string, so here it holds for all finite representations.

References

• [JH15]
• [Jar19]

noncomputable def Autosegmental.AR.mergeOffset {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] (X : TieredAR ι τ) (Y : TieredAR ι τ) [Finite X.obj.V] [Finite Y.obj.V] (i : ι) : ℕ

Where tier i of the second factor starts in a merging concatenation.

Equations

• Autosegmental.AR.mergeOffset m X Y i = if i = m then OCP.mergeOffset (Autosegmental.AR.tierWord m) (Autosegmental.AR.tierWord m) else Autosegmental.AR.tierLength X i

theorem Autosegmental.AR.repointIdx_mergeIdx_of_lt {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X : TieredAR ι τ} {Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] {i : ι} {p : ℕ} (hp : p < tierLength X i) : repointIdx m (OCP.mergeIdx (tierWord m) (tierWord m)) i p = p

theorem Autosegmental.AR.repointIdx_mergeIdx_add {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X : TieredAR ι τ} {Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] (i : ι) (p : ℕ) : repointIdx m (OCP.mergeIdx (tierWord m) (tierWord m)) i (tierLength X i + p) = mergeOffset m X Y i + p

theorem Autosegmental.AR.repointIdx_runIdx_append_left {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X : TieredAR ι τ} {Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] {i : ι} {p : ℕ} (hp : p < tierLength X i) : repointIdx m (OCP.runIdx (tierWord m ++ tierWord m)) i p = repointIdx m (OCP.runIdx (tierWord m)) i p

noncomputable def Autosegmental.AR.mergeConcat {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] (X Y : TieredAR ι τ) [Finite X.obj.V] [Finite Y.obj.V] : TieredAR ι τ

Merging concatenation: X ⊗ Y with the seam of melody tier m merged, the last node of X and the first node of Y becoming one node when they bear the same label.

Equations

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

instance Autosegmental.AR.instFiniteVSigmaObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesMergeConcat {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] (X Y : TieredAR ι τ) [Finite X.obj.V] [Finite Y.obj.V] [Finite ι] : Finite (mergeConcat m X Y).obj.V

@[simp]

theorem Autosegmental.AR.tierWord_mergeConcat_self {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] [Finite ι] : tierWord m = OCP.mergeAppend (tierWord m) (tierWord m)

@[simp]

theorem Autosegmental.AR.tierWord_mergeConcat_of_ne {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] [Finite ι] {i : ι} (h : i ≠ m) : tierWord i = tierWord i ++ tierWord i

@[simp]

theorem Autosegmental.AR.tierLength_mergeConcat_of_ne {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] [Finite ι] {i : ι} (h : i ≠ m) : tierLength (mergeConcat m X Y) i = tierLength X i + tierLength Y i

theorem Autosegmental.AR.link_mergeConcat {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] [Finite ι] (i j : ι) (r s : ℕ) : link (mergeConcat m X Y) i j r s ↔ link X i j r s ∨ ∃ (p : ℕ) (q : ℕ), link Y i j p q ∧ mergeOffset m X Y i + p = r ∧ mergeOffset m X Y j + q = s

A link of a merging concatenation is a link of the first factor, or a link of the second shifted to where that factor starts.

The theorems of Jardine and Heinz

noncomputable def Autosegmental.AR.emptyMergeConcatFullIso {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X : TieredAR ι τ} [Finite X.obj.V] [Finite ι] : (mergeConcat m (CategoryTheory.MonoidalCategoryStruct.tensorUnit (TieredAR ι τ)) X).obj.Iso X.obj

The empty representation is a left unit ([JH15] Theorem 1).

Equations

• Autosegmental.AR.emptyMergeConcatFullIso = Autosegmental.AR.fullIsoOfReaderEq ⋯ ⋯

noncomputable def Autosegmental.AR.mergeConcatEmptyFullIso {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X : TieredAR ι τ} [Finite X.obj.V] [Finite ι] : (mergeConcat m X (CategoryTheory.MonoidalCategoryStruct.tensorUnit (TieredAR ι τ))).obj.Iso X.obj

The empty representation is a right unit ([JH15] Theorem 1).

Equations

• Autosegmental.AR.mergeConcatEmptyFullIso = Autosegmental.AR.fullIsoOfReaderEq ⋯ ⋯

noncomputable def Autosegmental.AR.mergeConcatCongr {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] [Finite ι] {X' Y' : TieredAR ι τ} [Finite X'.obj.V] [Finite Y'.obj.V] (e₁ : X.obj.Iso X'.obj) (e₂ : Y.obj.Iso Y'.obj) : (mergeConcat m X Y).obj.Iso (mergeConcat m X' Y').obj

Merging concatenation respects full isomorphism.

Equations

• Autosegmental.AR.mergeConcatCongr e₁ e₂ = Autosegmental.AR.fullIsoOfReaderEq ⋯ ⋯

theorem Autosegmental.AR.mergeOffset_mergeConcat_left {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] [Finite ι] {Z : TieredAR ι τ} [Finite Z.obj.V] (i : ι) : mergeOffset m (mergeConcat m X Y) Z i = mergeOffset m X (mergeConcat m Y Z) i + mergeOffset m Y Z i

theorem Autosegmental.AR.mergeOffset_mergeConcat_right {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X : TieredAR ι τ} {Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] [Finite ι] {Z : TieredAR ι τ} [Finite Z.obj.V] {i : ι} (h : 0 < tierLength Y i) : mergeOffset m X (mergeConcat m Y Z) i = mergeOffset m X Y i

noncomputable def Autosegmental.AR.mergeConcatAssocFullIso {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] [Finite ι] {Z : TieredAR ι τ} [Finite Z.obj.V] : (mergeConcat m (mergeConcat m X Y) Z).obj.Iso (mergeConcat m X (mergeConcat m Y Z)).obj

Merging concatenation is associative ([JH15] Theorem 3).

Equations

• Autosegmental.AR.mergeConcatAssocFullIso = Autosegmental.AR.fullIsoOfReaderEq ⋯ ⋯

theorem Autosegmental.AR.noCrossing_mergeConcat {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] [Finite ι] (hX : NoCrossing X.obj.edges X.obj.arcs) (hY : NoCrossing Y.obj.edges Y.obj.arcs) : NoCrossing (mergeConcat m X Y).obj.edges (mergeConcat m X Y).obj.arcs

Merging concatenation preserves the NCC, the inductive step of [JH15] Theorem 4.

theorem Autosegmental.AR.isCleanAt_mergeConcat {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] [Finite ι] (hX : IsCleanAt X m) (hY : IsCleanAt Y m) : IsCleanAt (mergeConcat m X Y) m

Merging concatenation of OCP-clean factors is OCP-clean, the inductive step of [JH15] Theorem 5.

Collapse as a homomorphism

noncomputable def Autosegmental.AR.collapseTensorFullIso {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} {m : ι} [DecidableEq (τ m)] {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] [Finite ι] : (collapse (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) m).obj.Iso (mergeConcat m (collapse X m) (collapse Y m)).obj

The collapse of a concatenation is the merging concatenation of the collapses.

Equations

• Autosegmental.AR.collapseTensorFullIso = Autosegmental.AR.fullIsoOfReaderEq ⋯ ⋯

Realization by merging concatenation

noncomputable def Autosegmental.AR.mergeStep {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] [Finite ι] {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (A : { A : TieredAR ι τ // Finite A.obj.V }) (s : S) : { A : TieredAR ι τ // Finite A.obj.V }

A step of the left fold: the merging concatenation of a stage with a symbol's primitive.

Equations

• Autosegmental.AR.mergeStep m g₀ A s = ⟨Autosegmental.AR.mergeConcat m (↑A) (g₀ s), ⋯⟩

noncomputable def Autosegmental.AR.mergeRealize {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] [Finite ι] {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (w : List S) : TieredAR ι τ

The realization of a string by merging concatenation, the left fold g(uγ) = g(u) ∘ g(γ) from the empty representation ([JH15] Definition 5).

Equations

• Autosegmental.AR.mergeRealize m g₀ w = ↑(List.foldl (Autosegmental.AR.mergeStep m g₀) ⟨CategoryTheory.MonoidalCategoryStruct.tensorUnit (Autosegmental.TieredAR ι τ), ⋯⟩ w)

instance Autosegmental.AR.instFiniteVSigmaObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesMergeRealize {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] [Finite ι] {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (w : List S) : Finite (mergeRealize m g₀ w).obj.V

@[simp]

theorem Autosegmental.AR.mergeRealize_nil {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] [Finite ι] {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] : mergeRealize m g₀ [] = CategoryTheory.MonoidalCategoryStruct.tensorUnit (TieredAR ι τ)

theorem Autosegmental.AR.mergeRealize_append_singleton {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] [Finite ι] {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (w : List S) (s : S) : mergeRealize m g₀ (w ++ [s]) = mergeConcat m (mergeRealize m g₀ w) (g₀ s)

theorem Autosegmental.AR.noCrossing_mergeRealize {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] [Finite ι] {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), NoCrossing (g₀ s).obj.edges (g₀ s).obj.arcs) (w : List S) : NoCrossing (mergeRealize m g₀ w).obj.edges (mergeRealize m g₀ w).obj.arcs

Over primitives obeying the NCC, every realization obeys it ([JH15] Theorem 4).

theorem Autosegmental.AR.isCleanAt_mergeRealize {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] [Finite ι] {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), IsCleanAt (g₀ s) m) (w : List S) : IsCleanAt (mergeRealize m g₀ w) m

Over OCP-clean primitives, every realization is OCP-clean ([JH15] Theorem 5).

theorem Autosegmental.AR.nonempty_fullIso_realizeMerged {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] [Finite ι] {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), IsCleanAt (g₀ s) m) (w : List S) : Nonempty ((mergeRealize m g₀ w).obj.Iso (realizeMerged m g₀ w).obj)

Over OCP-clean primitives, the realization by merging concatenation is the collapsed realization.

theorem Autosegmental.AR.tierWord_mergeRealize {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] [Finite ι] {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), IsCleanAt (g₀ s) m) (w : List S) (i : ι) : tierWord i = tierWord i

theorem Autosegmental.AR.link_mergeRealize {ι : Type u_1} [DecidableEq ι] {τ : ι → Type u_2} (m : ι) [DecidableEq (τ m)] [Finite ι] {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), IsCleanAt (g₀ s) m) (w : List S) (i j : ι) (p q : ℕ) : link (mergeRealize m g₀ w) i j p q ↔ link (realizeMerged m g₀ w) i j p q