Docs / Phonology / Autosegmental / Factors

Factors and banned-subgraph grammars

import Linglib.Phonology.Autosegmental.Factors · namespace Autosegmental.AR

A factor occurs in a representation at per-tier offsets when its words are windows of the host's and its lines transport shifted, Jardine's subgraph embedding in position coordinates. Embedding is a preorder, the analogue of mathlib's SimpleGraph.IsContained with contiguous tier windows. A banned-subgraph grammar is a list of forbidden factors, and a string is a one-tier representation without lines.

Main definitions

AR.IsFactorAt, AR.FactorEmbeds (⊑): factor occurrence at given offsets, and its existential closure.
AR.Free: avoidance of every factor of a banned-subgraph grammar.
AR.ofList: a string as a one-tier representation.

Main results

AR.FactorEmbeds.refl, AR.FactorEmbeds.trans: embedding is a preorder.
AR.factorEmbeds_iff_bounded: embedding is a bounded search over offsets.
AR.factorEmbeds_iff_infix_of_link_free: for link-free factors, embedding is independent per-tier infix occurrence.
AR.factorEmbeds_ofList_iff: one string embeds in another iff it is an infix.

Implementation notes

Jardine's grammars ban only connected subgraphs. IsFactorAt places the windows of a factor's tiers independently, so a factor with two nonempty tiers and no line embeds whenever its tier words occur anywhere; Free admits such factors, and its languages contain Jardine's.

References

Jardine 2017, The local nature of tone-association patterns
Jardine 2016b, Locality and Non-linear Representations in Tonal Phonology formalized
Jardine 2019, The expressivity of autosegmental grammars formalized

Declarations

F occurs in X at per-tier offsets o.

structure IsFactorAt L57–62

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

window (i : ι) (p : ℕ) : p < (F.word i).length → (X.word i)[p + o i]? = (F.word i)[p]?
Each word of F is the window of X's at the tier's offset.
link_map (i j : ι) (p q : ℕ) : F.Link i j p q → X.Link i j (p + o i) (q + o j)
Lines transport by the offsets.

Used by FactorEmbeds, IsFactorAt.trans, IsFactorAt.refl, IsFactorAt.offset_le, IsFactorAt.clamp, factorEmbeds_iff_bounded

F subgraph-embeds in X when some offsets place it as a factor (Jardine 2017's connected-subgraph embedding).

def FactorEmbeds L64–66

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

F.FactorEmbeds X = ∃ (o : ι → ℕ), F.IsFactorAt X o

Built from

Instances Autosegmental.AR.instDecidableFactorEmbedsBoolTwoTierOfWordsOfDecidableEq

Used by Free, free_cons, FactorEmbeds.trans, FactorEmbeds.refl, factorEmbeds_iff_bounded, factorEmbeds_iff_infix_of_link_free, factorEmbeds_ofList_iff

Used in Phonology/Autosegmental/TwoTier, Phonology/Subregular/AutosegmentalStrictlyLocal, Jardine2016b, Jardine2017, Jardine2019

X avoids every forbidden factor of a banned-subgraph grammar (Jardine 2016b Ch. 5's L^NL_G).

def Free L68–70

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

X.Free B = ∀ F ∈ B, ¬F.FactorEmbeds X

Built from

Instances Jardine2016b.instDecidableFreeBoolTwoTierSegGenVoicingGrammar, Jardine2017.Hausa.instDecidableFreeBoolTwoTierTRNTBUKindArGrammar, Jardine2017.Mende.instDecidableFreeBoolTwoTierTRNTBUKindArGrammar

Used by free_nil, free_cons

Used in Phonology/Subregular/AutosegmentalStrictlyLocal, Jardine2016b, Jardine2017, Jardine2019

Factor embedding is transitive.

theorem FactorEmbeds.trans L93–98

{ι : Type u_1} {τ : ι → Type u_2} {F X Y : AR τ} (h : F.FactorEmbeds X) (h' : X.FactorEmbeds Y) :

F.FactorEmbeds Y

Built from

theorem FactorEmbeds.refl L105–106

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

X.FactorEmbeds X

Built from

FactorEmbeds is a bounded search over offsets.

theorem factorEmbeds_iff_bounded L134–138

{ι : Type u_1} {τ : ι → Type u_2} {F X : AR τ} :

F.FactorEmbeds X ↔ ∃ (o : ι → ℕ), (∀ (i : ι), o i ≤ (X.word i).length) ∧ F.IsFactorAt X o

Built from ,

For a link-free factor, embedding reduces to independent per-tier infix occurrences (Jardine 2019's link-free fragment).

theorem factorEmbeds_iff_infix_of_link_free L140–157

{ι : Type u_1} {τ : ι → Type u_2} {F X : AR τ} (hF : ∀ (i j : ι) (p q : ℕ), ¬F.Link i j p q) :

F.FactorEmbeds X ↔ ∀ (i : ι), F.word i <:+: X.word i

Built from

Strings as one-tier representations

A string is a representation with one tier and no association lines.

def ofList L165–166

{α : Type u_3} (w : List α) :

AR fun (x : Unit) => α

ofList w = { word := fun (x : Unit) => w, assoc := ⊥, assoc_le := ⋯, decidableAdj := inferInstance }

Used by word_ofList, not_link_ofList, factorEmbeds_ofList_iff

Used in Phonology/Subregular/AutosegmentalStrictlyLocal

One string embeds in another as a factor iff it is an infix.

@[simp] theorem factorEmbeds_ofList_iff L173–177

{α : Type u_3} (f w : List α) :

(ofList f).FactorEmbeds (ofList w) ↔ f <:+: w

Built from ,

Connections

Builds on

Phonology / Autosegmental / Basic Autosegmental.AR, Link, mk, word

Theory built on it

Studies using it

Also in Phonology / Autosegmental

Basic Autosegmental representations
Correspondence Phonological transformations as correspondence relations
Floating Floating autosegmental forms
Graph Autosegmental representations as labeled mixed graphs
Hull The association hull
IntervalOrder Representations in time
Melody Lexical melodies
MergeAR Merging concatenation of autosegmental representations

and 5 more

NonCrossing Non-crossing association relations
OCP OCP-merging collapse of autosegmental representations
Realization Realization of strings as representations
Skeleton The CV skeleton
TwoTier Two-tier autosegmental representations

All 2 imports

All 2 importers