Factors and banned-subgraph grammars

[Jar17b]'s connected-subgraph embedding in position coordinates: a factor occurs at per-tier offsets when its tier words are windows of the host's and its links transport shifted. Banned-subgraph grammars ([Jar16b] Ch. 5) are lists of forbidden factors.

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.

Main results

• 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 — [Jar19]'s link-free fragment.

structure Autosegmental.AR.IsFactorAt {ι : Type u_1} {τ : ι → Type u_2} (F : TieredAR ι τ) (X : TieredAR ι τ) [Finite F.obj.V] [Finite X.obj.V] (o : ι → ℕ) : Prop

F occurs in X at per-tier offsets o.

• window (i : ι) (p : ℕ) : p < tierLength F i → (tierWord i)[p + o i]? = (tierWord i)[p]?

  Each tier word of F is the window of X's at the tier's offset.

• link_map (i j : ι) (p q : ℕ) : link F i j p q → link X i j (p + o i) (q + o j)

  Links transport by the offsets.

def Autosegmental.AR.FactorEmbeds {ι : Type u_1} {τ : ι → Type u_2} (F : TieredAR ι τ) (X : TieredAR ι τ) [Finite F.obj.V] [Finite X.obj.V] : Prop

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

Equations

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

def Autosegmental.AR.Free {ι : Type u_1} {τ : ι → Type u_2} (X : TieredAR ι τ) [Finite X.obj.V] (B : List { F : TieredAR ι τ // Finite F.obj.V }) : Prop

X avoids every forbidden factor of a banned-subgraph grammar ([Jar16b] Ch. 5's L^NL_G).

Equations

• Autosegmental.AR.Free X B = ∀ F ∈ B, ¬Autosegmental.AR.FactorEmbeds (↑F) X

theorem Autosegmental.AR.IsFactorAt.offset_le {ι : Type u_1} {τ : ι → Type u_2} {F : TieredAR ι τ} {X : TieredAR ι τ} [Finite F.obj.V] [Finite X.obj.V] {o : ι → ℕ} (h : IsFactorAt F X o) {i : ι} (hi : tierLength F i ≠ 0) : o i ≤ tierLength X i

On a tier where the factor is nonempty, the window equations force the offset in bounds.

theorem Autosegmental.AR.IsFactorAt.clamp {ι : Type u_1} {τ : ι → Type u_2} {F : TieredAR ι τ} {X : TieredAR ι τ} [Finite F.obj.V] [Finite X.obj.V] {o : ι → ℕ} (h : IsFactorAt F X o) : IsFactorAt F X fun (i : ι) => min (o i) (tierLength X i)

Offsets clamp to the host's tier lengths; the clamp only moves offsets on tiers where the factor is empty.

theorem Autosegmental.AR.factorEmbeds_iff_bounded {ι : Type u_1} {τ : ι → Type u_2} {F : TieredAR ι τ} {X : TieredAR ι τ} [Finite F.obj.V] [Finite X.obj.V] : FactorEmbeds F X ↔ ∃ (o : ι → ℕ), (∀ (i : ι), o i ≤ tierLength X i) ∧ IsFactorAt F X o

FactorEmbeds is a bounded search over offsets.

theorem Autosegmental.AR.factorEmbeds_iff_infix_of_link_free {ι : Type u_1} {τ : ι → Type u_2} {F : TieredAR ι τ} {X : TieredAR ι τ} [Finite F.obj.V] [Finite X.obj.V] (hF : ∀ (i j : ι) (p q : ℕ), ¬link F i j p q) : FactorEmbeds F X ↔ ∀ (i : ι), tierWord i <:+: tierWord i

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