OCP-merging collapse of autosegmental representations

import Linglib.Phonology.Autosegmental.OCP · namespace Autosegmental

Merging melody nodes moves the positions of the melody tier along a monotone map. X.repoint m w f reads melody tier m as the word w, moves each of its positions p to f p, and carries the links along, so a merged node keeps every line of the nodes merged into it. AR.collapse m is the repointing that destutters the tier word (OCP.collapse) through the run index runIdx, merging every run of identical melody nodes; a melody Hⁿ collapses to one H linked to n timing slots. Collapsing a realization (w.map g₀).prod merges every run of its melody. Jardine and Heinz instead merge only at the seam of each concatenation (Autosegmental/MergeAR.lean), and the two agree when the primitives are OCP-clean, as in Jardine's tonal realization.

Main definitions

AR.repoint: a representation with one tier moved along a map of its positions.
AR.collapse: the OCP merge of melody tier m.
AR.IsCleanAt: no adjacent repeats on melody tier m.
MergedLinks: the lines of a two-tier presentation with its melody collapsed.

Main results

AR.link_repoint, AR.noCrossing_repoint: repointing carries the links, and a monotone repointing preserves the NCC.
AR.isCleanAt_collapse, AR.noCrossing_collapse: the collapse is OCP-clean and preserves the NCC; AR.IsCleanAt.collapse_eq: collapsing a clean tier changes nothing.
AR.collapse_ofWords, AR.prod_ofWords_collapse: collapsing a presentation, or a realized string of presentations, gives a presentation.

References

Jardine 2019, The expressivity of autosegmental grammars formalized
Jardine & Heinz 2015, A Concatenation Operation to Derive Autosegmental Graphs formalized
Jardine 2016b, Locality and Non-linear Representations in Tonal Phonology formalized

Repointing a tier

X with tier m read as the word w and its positions moved along f, the lines following the positions they join.

def AR.repoint L81–89

{ι : Type u_1} [Fintype ι] [DecidableEq ι] {τ : ι → Type u_2} (X : AR τ) (m : ι) (w : List (τ m)) {f : ℕ → ℕ} (hf : ∀ p < (X.word m).length, f p < w.length) :

AR τ

X.repoint m w hf = X.map (Function.update X.word m w) fun (i : ι) (p : Fin (X.word i).length) => ⟨repointIdx m f i ↑p, ⋯⟩

Built from

Used by AR.word_repoint_self, AR.word_repoint_of_ne, AR.link_repoint, AR.NoCrossing.repoint, AR.collapse

Used in Phonology/Autosegmental/MergeAR

L91

L93–94

The lines of a repointing are the repointed lines.

theorem AR.link_repoint L98–107

{ι : Type u_1} [Fintype ι] [DecidableEq ι] {τ : ι → Type u_2} {X : AR τ} {m : ι} {w : List (τ m)} {f : ℕ → ℕ} (hf : ∀ p < (X.word m).length, f p < w.length) {i j : ι} {r s : ℕ} :

(X.repoint m w hf).Link i j r s ↔ ∃ (p : ℕ) (q : ℕ), X.Link i j p q ∧ repointIdx m f i p = r ∧ repointIdx m f j q = s

Built from ,

L109–112

The collapse

X is OCP-clean at melody tier m when that tier word has no adjacent repeats.

def AR.IsCleanAt L121–122

{ι : Type u_1} {τ : ι → Type u_2} (X : AR τ) (m : ι) :

Prop

X.IsCleanAt m = OCP.IsClean (X.word m)

Used by AR.IsCleanAt.repointIdx_runIdx, AR.isCleanAt_collapse, AR.IsCleanAt.collapse_eq

Used in Phonology/Autosegmental/Graph, Phonology/Autosegmental/MergeAR, Jardine2019, JardineHeinz2015

L127–131

The OCP-merging collapse of melody tier m merges every run of identical melody nodes, repointing the tier through its run index.

def AR.collapse L135–138

{ι : Type u_1} {τ : ι → Type u_2} (X : AR τ) (m : ι) [DecidableEq ι] [DecidableEq (τ m)] [Fintype ι] :

AR τ

X.collapse m = X.repoint m (OCP.collapse (X.word m)) ⋯

Built from

Used by AR.word_collapse_self, AR.word_collapse_of_ne, AR.link_collapse, AR.isCleanAt_collapse, AR.NoCrossing.collapse, AR.IsCleanAt.collapse_eq, AR.link_collapse_true_false, AR.collapse_ofWords, AR.prod_ofWords_collapse

Used in Phonology/Autosegmental/MergeAR, Phonology/Tone/Plateauing, Jardine2016a, JardineHeinz2015

L140–141

L143–144

L148–152

The collapse is OCP-clean at the collapsed tier.

theorem AR.isCleanAt_collapse L154–156

{ι : Type u_1} {τ : ι → Type u_2} {X : AR τ} {m : ι} [DecidableEq ι] [DecidableEq (τ m)] [Fintype ι] :

(X.collapse m).IsCleanAt m

Built from ,

L158–160

Collapsing a representation that is clean at m changes nothing.

theorem AR.IsCleanAt.collapse_eq L162–173

{ι : Type u_1} {τ : ι → Type u_2} {X : AR τ} {m : ι} [DecidableEq ι] [DecidableEq (τ m)] [Fintype ι] (h : X.IsCleanAt m) :

X.collapse m = X

Built from ,

Collapsing two-tier presentations

In the two-tier case, with the melody over true, collapsing a presentation gives the presentation whose melody is destuttered and whose lines are repointed through the run index of the melody.

A line of an OCP-merged presentation is a line of the presentation with its melody position repointed through the run index of the melody.

def MergedLinks L188–191

{α : Type u} [DecidableEq α] (melody : List α) (Lk : ℕ → ℕ → Prop) (r s : ℕ) :

Prop

MergedLinks melody Lk r s = ∃ p < melody.length, Lk p s ∧ OCP.runIdx melody p = r

Used by AR.instDecidableRelNatMergedLinks, AR.collapse_ofWords, AR.prod_ofWords_collapse

L193–195

L197–206

Collapsing the melody of a presentation gives a presentation.

theorem AR.collapse_ofWords L210–220

{α β : Type u} [DecidableEq α] [DecidableEq β] {as : List α} {bs : List β} {L : ℕ → ℕ → Prop} [DecidableRel L] :

(ofWords as bs L).collapse true = ofWords (OCP.collapse as) bs (MergedLinks as L)

Built from ,

The merged realization of a string of presentations is one presentation.

theorem AR.prod_ofWords_collapse L225–230

{α β : Type u} [DecidableEq α] [DecidableEq β] {S : Type u_1} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) [(s : S) → DecidableRel (L s)] (w : List S) :

(List.map (fun (s : S) => ofWords (as s) (bs s) (L s)) w).prod.collapse true = ofWords (OCP.collapse (List.map as w).flatten) (List.map bs w).flatten (MergedLinks (List.map as w).flatten (BlockLinks as bs L w))

Built from ,