Docs / Phonology / Autosegmental / MergeAR

Merging concatenation of autosegmental representations

import Linglib.Phonology.Autosegmental.MergeAR · namespace Autosegmental

Source

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. MergeAR m τ is AR τ with this concatenation at melody tier m as its multiplication, the repointing of the bridging concatenation along OCP.mergeIdx; a string realizes as the product of its symbols' primitives.

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

Main definitions

  • MergeAR m τ: representations under merging concatenation at melody tier m, a monoid (Jardine and Heinz's Theorems 1 and 3).
  • MergeAR.collapseHom: the collapse, as a monoid hom from bridging concatenation.

Main statements

Implementation notes

Jardine and Heinz merge at every melody tier; MergeAR m τ 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; here the tiers are words, so it holds for all representations.

References

Declarations

Representations under merging concatenation at melody tier m: a type synonym of AR τ whose multiplication merges the seam of tier m.

def MergeARL55–57
{ι : Type u_1} (_m : ι) (τ : ι → Type u_2) :
Type (max u_2 u_1)

Used by MergeAR.ofAR, MergeAR.toAR, MergeAR.ofAR_toAR, MergeAR.instDecidableEqOfFintype, MergeAR.instOne, MergeAR.offset, MergeAR.instMul, MergeAR.toAR_mul, MergeAR.word_toAR_mul_self, MergeAR.word_toAR_mul_of_ne, MergeAR.link_toAR_mul, MergeAR.instMonoid, MergeAR.noCrossing_toAR_mul, MergeAR.isCleanAt_toAR_mul, MergeAR.noCrossing_toAR_prod, MergeAR.isCleanAt_toAR_prod, MergeAR.collapseHom

Used in Jardine2019, JardineHeinz2015

L66–67
L69
L71
L79
L119–126
L140–143

The theorems of Jardine and Heinz

L189–223
L240–248
L250–258

Collapse as a homomorphism

L307
L309–311

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

theorem MergeAR.prod_map_ofARL313–318
{ι : Type u_1} {τ : ι → Type u_2} {m : ι} [DecidableEq ι] [DecidableEq (τ m)] [Fintype ι] {S : Type u_3} {g₀ : S → AR τ} (hg : ∀ (s : S), (g₀ s).IsCleanAt m) (w : List S) :
(List.map (fun (s : S) => ofAR (g₀ s)) w).prod = ofAR ((List.map g₀ w).prod.collapse m)

Built from