The association hull

AR.hull m closes each node of melody tier m to the interval hull of its links on every other tier: a melody node links to a position iff that position lies between two of its links. Applied after OCP fusion, the hull of the fused H's links is the plateau of [HK10]'s plateauing rule (Phonology/Tone/Plateauing). The hull of a melody with several nodes can violate the No-Crossing Constraint, since two interleaved hulls cross; the rule applies to the fused representation, whose melody is a single node.

Main results

• AR.link_hull_left: a melody node links to the positions between two of its links.
• AR.link_subset_hull: the hull extends the link relation.
• AR.link_hull_convex: each melody node's links form an interval.

References

• [HK10]

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

The hull closes each tier-m node's association set to its interval hull on each other tier.

Equations

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

instance Autosegmental.instFiniteVSigmaObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesHull {ι : Type u_1} [Finite ι] {τ : ι → Type u_2} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] : Finite (AR.hull m X).obj.V

@[simp]

theorem Autosegmental.AR.tierWord_hull {ι : Type u_1} [Finite ι] {τ : ι → Type u_2} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] (i : ι) : tierWord i = tierWord i

@[simp]

theorem Autosegmental.AR.tierLength_hull {ι : Type u_1} [Finite ι] {τ : ι → Type u_2} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] (i : ι) : tierLength (hull m X) i = tierLength X i

theorem Autosegmental.AR.link_hull_left {ι : Type u_1} [Finite ι] {τ : ι → Type u_2} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] {j : ι} (hj : m ≠ j) {p q : ℕ} (hq : q < tierLength X j) : link (hull m X) m j p q ↔ ∃ (q₁ : ℕ) (q₂ : ℕ), link X m j p q₁ ∧ link X m j p q₂ ∧ q₁ ≤ q ∧ q ≤ q₂

In the hull, melody node p links to q iff q lies between two of p's links.

theorem Autosegmental.AR.link_hull_of_ne {ι : Type u_1} [Finite ι] {τ : ι → Type u_2} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] {i j : ι} (hi : i ≠ m) (hj : j ≠ m) (p q : ℕ) : link (hull m X) i j p q ↔ link X i j p q

Links not involving the melody tier pass through the hull unchanged.

theorem Autosegmental.AR.link_subset_hull {ι : Type u_1} [Finite ι] {τ : ι → Type u_2} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] {i j : ι} {p q : ℕ} (h : link X i j p q) : link (hull m X) i j p q

Melody links flank themselves: the hull extends the link relation.

theorem Autosegmental.AR.link_hull_convex {ι : Type u_1} [Finite ι] {τ : ι → Type u_2} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] {j : ι} (hj : m ≠ j) {p q₁ q q₂ : ℕ} (hq : q < tierLength X j) (h₁ : link (hull m X) m j p q₁) (h₂ : link (hull m X) m j p q₂) (hle₁ : q₁ ≤ q) (hle₂ : q ≤ q₂) : link (hull m X) m j p q

Each melody node's hull links form an interval.