Autosegmental realization of strings

The realization of a string maps each symbol to its autosegmental graph primitive and concatenates them ([Jar19]'s mapping g): realize g₀ w = ∏ (w.map g₀) in the concatenation monoid Monoid (AR α β).

This is a string→AR monoid homomorphism (realize_append), the exact analogue — one categorical level up — of the string→tier-string projection TierProjection.apply (= List.filterMap, also concat-distributing): both are free-monoid homomorphisms built from a per-symbol map, used to define a subregular class as a preimage (Phonology/Autosegmental/ASL.lean for the realization, Subregular.Language.TierStrictlyLocal for the projection). The realization keeps the association structure the tier projection discards — see [Jar19] on ASL vs TSL.

def Autosegmental.realize {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) (w : List S) : AR α β

Realize a string as an autosegmental representation: concatenate the graph primitives g₀ a of its symbols ([Jar19]'s g).

Equations

• Autosegmental.realize g₀ w = (List.map g₀ w).prod

@[simp]

theorem Autosegmental.realize_nil {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) : realize g₀ [] = AR.empty

@[simp]

theorem Autosegmental.realize_cons {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) (a : S) (w : List S) : realize g₀ (a :: w) = (g₀ a).concat (realize g₀ w)

theorem Autosegmental.realize_append {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) (xs ys : List S) : realize g₀ (xs ++ ys) = (realize g₀ xs).concat (realize g₀ ys)

The realization is a monoid homomorphism: it distributes over concatenation — the string→AR analogue of TierProjection.apply_append.

Tier projections

The realization composed with a tier accessor is itself a free-monoid hom into that tier's free monoid: upperProj g₀ sends a string to the concatenation of its symbols' upper tiers (the underlying list of realize g₀ w's upper tier), and likewise lowerProj. These factor the realization's tier content through FreeMonoid and are the bridge used to place link-free ASL sets in SF (Studies.Jardine2019): a per-tier factor constraint on the realization is the comap of a factor language along the tier projection.

def Autosegmental.upperProj {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) : FreeMonoid S →* FreeMonoid α

The upper-tier realization as a free-monoid hom FreeMonoid S →* FreeMonoid α: each symbol maps to its primitive's upper tier, concatenated.

Equations

• Autosegmental.upperProj g₀ = FreeMonoid.lift fun (s : S) => FreeMonoid.ofList (g₀ s).upper.toList

def Autosegmental.lowerProj {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) : FreeMonoid S →* FreeMonoid β

The lower-tier realization as a free-monoid hom FreeMonoid S →* FreeMonoid β.

Equations

• Autosegmental.lowerProj g₀ = FreeMonoid.lift fun (s : S) => FreeMonoid.ofList (g₀ s).lower.toList

@[simp]

theorem Autosegmental.upperProj_of {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) (s : S) : (upperProj g₀) (FreeMonoid.of s) = FreeMonoid.ofList (g₀ s).upper.toList

@[simp]

theorem Autosegmental.lowerProj_of {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) (s : S) : (lowerProj g₀) (FreeMonoid.of s) = FreeMonoid.ofList (g₀ s).lower.toList

theorem Autosegmental.realize_upper_toList {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) (w : List S) : (realize g₀ w).upper.toList = (upperProj g₀) (FreeMonoid.ofList w)

The upper tier of a realization is its upper projection: (realize g₀ w).upper's underlying list is upperProj g₀ w.

theorem Autosegmental.realize_lower_toList {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) (w : List S) : (realize g₀ w).lower.toList = (lowerProj g₀) (FreeMonoid.ofList w)

The lower tier of a realization is its lower projection.

Linearization: the association-state string of an AR

The inverse direction of the bridge. Where realize builds an AR from a string, linearize reads the association-state string off an AR: per timing-tier position, its label together with the labels of the melody nodes linked to it, in tier order. This is the linearisation phonologists use implicitly when writing a tonal input as a string of TBU symbols — [Jar16] §4.4: each string symbol records one timing unit's associations, so transducer look-ahead is measured on the timing tier. Like realize, it is a monoid homomorphism into (List, ++) (AR.linearize_concat), so the linearization of a realization is the concatenation of the per-symbol association profiles (linearize_realize).

def Autosegmental.Graph.linkedLabels {α : Type u_2} {β : Type u_3} (A : Graph α β) (j : ℕ) : List α

The labels of the upper (melody) nodes linked to lower position j, in tier order.

Equations

• A.linkedLabels j = List.filterMap A.upper.get? (List.filter (fun (i : ℕ) => decide ((i, j) ∈ A.links)) (List.range A.upper.len))

theorem Autosegmental.Graph.linkedLabels_concat_left {α : Type u_2} {β : Type u_3} {A B : Graph α β} (hA : A.InBounds) {j : ℕ} (hj : j < A.lower.len) : (A.concat B).linkedLabels j = A.linkedLabels j

Positions inside A see only A's links.

theorem Autosegmental.Graph.linkedLabels_concat_right {α : Type u_2} {β : Type u_3} {A B : Graph α β} (hA : A.InBounds) {j : ℕ} (hj : A.lower.len ≤ j) : (A.concat B).linkedLabels j = B.linkedLabels (j - A.lower.len)

Positions past A see exactly B's links, shifted down by A's length.

def Autosegmental.AR.linearize {α : Type u_2} {β : Type u_3} (A : AR α β) : List (β × List α)

A.linearize is the association-state string of A ([Jar16] (40)): position j carries its timing-unit label together with the labels of the melody nodes linked to it.

Equations

• A.linearize = List.mapIdx (fun (j : ℕ) (b : β) => (b, A.linkedLabels j)) A.lower.toList

@[simp]

theorem Autosegmental.AR.linearize_length {α : Type u_2} {β : Type u_3} (A : AR α β) : A.linearize.length = A.lower.len

theorem Autosegmental.AR.linearize_getElem? {α : Type u_2} {β : Type u_3} (A : AR α β) (j : ℕ) : A.linearize[j]? = Option.map (fun (b : β) => (b, A.linkedLabels j)) (A.lower.get? j)

theorem Autosegmental.AR.isLinkedLower_iff_linearize {α : Type u_2} {β : Type u_3} (A : AR α β) {j : ℕ} : A.IsLinkedLower j ↔ ∃ (b : β) (as : List α), A.linearize[j]? = some (b, as) ∧ as ≠ []

Linkedness is readable off the linearization: slot j is linked iff its association-state entry carries a nonempty melody.

@[simp]

theorem Autosegmental.AR.linearize_empty {α : Type u_2} {β : Type u_3} : empty.linearize = []

theorem Autosegmental.AR.linearize_concat {α : Type u_2} {β : Type u_3} (A B : AR α β) : (A.concat B).linearize = A.linearize ++ B.linearize

Linearization sends concatenation of ARs to concatenation of association-state strings; the inBounds fields keep each side's links on its own positions.

theorem Autosegmental.linearize_realize {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) (w : List S) : (realize g₀ w).linearize = List.flatMap (fun (a : S) => (g₀ a).linearize) w

The linearization of a realization is the concatenation of the per-symbol association profiles ([Jar16] (40)).