Docs / Phonology / Autosegmental / Basic

Autosegmental representations

import Linglib.Phonology.Autosegmental.Basic · namespace Autosegmental

An autosegmental representation has a word on each tier and association lines joining positions on distinct tiers. Representations concatenate tier by tier, appending the words and keeping the lines of both factors, and form a monoid.

Main definitions

AR τ: a representation with alphabet τ i on tier i.
AR.Link: association of two positions given in ℕ coordinates.
AR.NoCrossing: the No-Crossing Constraint.
AR.fromRel: the representation with given words and the lines a relation specifies.
AR.map: a representation with its positions moved along maps of each tier.
AR.wordHom: the word on one tier, as a monoid hom.

Main results

AR.link_mul: the lines of a concatenation are those of its factors, the right factor's shifted past the left one.
AR.NoCrossing.mul, AR.NoCrossing.map: concatenation and monotone moves preserve the No-Crossing Constraint.

References

Goldsmith 1976, Autosegmental Phonology
Coleman & Local 1991, The ‘No Crossing Constraint’ in autosegmental phonology
Jardine & Heinz 2015, A Concatenation Operation to Derive Autosegmental Graphs formalized
Jardine 2019, The expressivity of autosegmental grammars formalized

Declarations

An autosegmental representation: a word on each tier, and association lines between positions on distinct tiers.

structure AR L50–61

{ι : Type u_1} (τ : ι → Type u_3) :

Type (max u_1 u_3)

word (i : ι) : List (τ i)
The word on tier i.
assoc : SimpleGraph ((i : ι) × Fin (self.word i).length)
The association lines, a graph on the positions.
assoc_le : self.assoc ≤ SimpleGraph.completeMultipartiteGraph fun (i : ι) => Fin (self.word i).length
Lines join distinct tiers: association lies in the complete multipartite graph on the tiers.
decidableAdj : DecidableRel self.assoc.Adj
Association is decidable.

Used by AR.Pos, AR.label, AR.instInhabited, AR.fst_ne_of_adj, AR.Link, AR.instDecidableLink, AR.link_iff_adj, AR.Link.lt_left, AR.Link.lt_right, AR.Link.symm, AR.Link.ne, AR.link_comm, AR.ext, AR.ext_iff, AR.ext_iff_bounded, AR.instDecidableEqOfFintype, AR.posMulEquiv, AR.posMulEquiv_of_lt, AR.posMulEquiv_of_le, AR.instMul, AR.instOne, AR.word_mul, AR.link_mul, AR.instMonoid, AR.wordHom, AR.wordHom_apply, AR.wordHom_comp_lift, AR.lines, AR.mem_lines, AR.NoCrossing, AR.instDecidablePredProdFinLengthWordMemSetRelLines, AR.instDecidableNoCrossingOfFintype, AR.isNonCrossing_lines_iff, AR.isNonCrossing_lines_iff_link, AR.isNonCrossing_lines_self, AR.isNonCrossing_lines_comm, AR.NoCrossing.mul, AR.map, AR.lines_map, AR.link_map, AR.NoCrossing.map, AR.map_id, AR.map_map, AR.fromRel

Used in Phonology/Autosegmental/Correspondence, Phonology/Autosegmental/Factors, Phonology/Autosegmental/Floating, Phonology/Autosegmental/Graph, Phonology/Autosegmental/Hull and 12 more

Lines in ℕ coordinates

Position p of tier i is associated with position q of tier j; positions beyond the end of a word are associated with nothing.

def AR.Link L82–86

{ι : Type u_1} {τ : ι → Type u_2} (X : AR τ) (i j : ι) (p q : ℕ) :

Prop

X.Link i j p q = ∃ (hp : p < (X.word i).length) (hq : q < (X.word j).length), X.assoc.Adj ⟨i, ⟨p, hp⟩⟩ ⟨j, ⟨q, hq⟩⟩

Built from

Used by AR.instDecidableLink, AR.link_iff_adj, AR.Link.lt_left, AR.Link.lt_right, AR.Link.symm, AR.Link.ne, AR.link_comm, AR.ext, AR.ext_iff, AR.ext_iff_bounded, AR.not_link_one, AR.link_mul, AR.mem_lines, AR.isNonCrossing_lines_iff, AR.isNonCrossing_lines_iff_link, AR.link_map, AR.link_fromRel

Used in Fragments/Tangale/Phonology, Phonology/Autosegmental/Factors, Phonology/Autosegmental/Floating, Phonology/Autosegmental/Hull, Phonology/Autosegmental/MergeAR and 7 more

Concatenation

theorem AR.link_mul L199–226

{ι : Type u_1} {τ : ι → Type u_2} {X Y : AR τ} (i j : ι) (p q : ℕ) :

(X * Y).Link i j p q ↔ X.Link i j p q ∨ (X.word i).length ≤ p ∧ (X.word j).length ≤ q ∧ Y.Link i j (p - (X.word i).length) (q - (X.word j).length)

Built from ,

L228–240

The word on tier i, as a monoid hom.

def AR.wordHom L242–246

{ι : Type u_1} {τ : ι → Type u_2} (i : ι) :

AR τ →* FreeMonoid (τ i)

AR.wordHom i = { toFun := fun (X : AR τ) => FreeMonoid.ofList (X.word i), map_one' := ⋯, map_mul' := ⋯ }

Built from

Used by AR.wordHom_apply, AR.wordHom_comp_lift

Used in Phonology/Subregular/AutosegmentalStrictlyLocal

L248

L250–252

The No-Crossing Constraint

L259–261

L263–265

The No-Crossing Constraint: between any two tiers, no two lines cross.

def AR.NoCrossing L268–269

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

Prop

X.NoCrossing = ∀ (i j : ι), IsNonCrossing (X.lines i j)

Built from ,

Used by AR.instDecidableNoCrossingOfFintype, AR.NoCrossing.one, AR.NoCrossing.mul, AR.NoCrossing.map

Used in Phonology/Autosegmental/Floating, Phonology/Autosegmental/Graph, Phonology/Autosegmental/IntervalOrder, Phonology/Autosegmental/MergeAR, Phonology/Autosegmental/OCP and 5 more

Concatenation preserves the No-Crossing Constraint. With NoCrossing.repoint under the merge this gives the inductive step of Jardine & Heinz 2015's Theorem 4 for their merging concatenation, MergeAR.noCrossing_toAR_mul.

theorem AR.NoCrossing.mul L299–312

{ι : Type u_1} {τ : ι → Type u_2} {X Y : AR τ} (hX : X.NoCrossing) (hY : Y.NoCrossing) :

(X * Y).NoCrossing

Built from ,

Moving positions

The representation with words w whose lines are those of X, each position moved along f on its tier; positions merged by f keep the lines of all of them.

def AR.map L322–329

{ι : Type u_1} {τ : ι → Type u_2} (X : AR τ) [Fintype ι] [DecidableEq ι] (w : (i : ι) → List (τ i)) (f : (i : ι) → Fin (X.word i).length → Fin (w i).length) :

AR τ

X.map w f = { word := w, assoc := SimpleGraph.map (Sigma.map id f) X.assoc, assoc_le := ⋯, decidableAdj := inferInstance }

Built from

Used by AR.lines_map, AR.link_map, AR.NoCrossing.map, AR.map_id, AR.map_map

Used in Phonology/Autosegmental/OCP

L331–342

L344–354

Moving positions monotonically preserves the No-Crossing Constraint.

theorem AR.NoCrossing.map L356–360

{ι : Type u_1} {τ : ι → Type u_2} {X : AR τ} [Fintype ι] [DecidableEq ι] (w : (i : ι) → List (τ i)) (f : (i : ι) → Fin (X.word i).length → Fin (w i).length) (hf : ∀ (i : ι), Monotone (f i)) (h : X.NoCrossing) :

(X.map w f).NoCrossing

Built from , ,

L363–365

L367–369

Representations from words and a relation

The representation with words w and a line between positions on distinct tiers wherever L holds in either direction: the symmetric closure SimpleGraph.fromRel, restricted to the complete multipartite graph on the tiers.

def AR.fromRel L380–386

{ι : Type u_1} {τ : ι → Type u_2} [DecidableEq ι] (w : (i : ι) → List (τ i)) (L : ι → ι → ℕ → ℕ → Prop) [(i j : ι) → DecidableRel (L i j)] :

AR τ

The definition is too large to print here; read it in the source.

Built from

Used by AR.word_fromRel, AR.link_fromRel

Used in Fragments/Tangale/Phonology, Phonology/Autosegmental/TwoTier, BirdKlein1990, Lionnet2022

L388

L391–400