Factors and banned-subgraph grammars

[jardine-2017]'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 ([jardine-2016b] 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 — [jardine-2019]'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 ([jardine-2017]'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 ([jardine-2016b] Ch. 5's L^NL_G).

Equations

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

instance Autosegmental.AR.instFiniteVSigmaObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesValTieredAR {ι : Type u_1} {τ : ι → Type u_2} (G : { F : TieredAR ι τ // Finite F.obj.V }) : Finite (↑G).obj.V

@[simp]

theorem Autosegmental.AR.free_nil {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] : Free X []

theorem Autosegmental.AR.free_cons {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] {F : { F : TieredAR ι τ // Finite F.obj.V }} {B : List { F : TieredAR ι τ // Finite F.obj.V }} : Free X (F :: B) ↔ ¬FactorEmbeds (↑F) X ∧ Free X B

A grammar tests its forbidden factors one by one.

theorem Autosegmental.AR.factorEmbeds_congr {ι : Type u_1} {τ : ι → Type u_2} {F : TieredAR ι τ} {X : TieredAR ι τ} [Finite F.obj.V] [Finite X.obj.V] {F' : TieredAR ι τ} {X' : TieredAR ι τ} [Finite F'.obj.V] [Finite X'.obj.V] (hwF : ∀ (i : ι), tierWord i = tierWord i) (hlF : ∀ (i j : ι) (p q : ℕ), link F i j p q ↔ link F' i j p q) (hwX : ∀ (i : ι), tierWord i = tierWord i) (hlX : ∀ (i j : ι) (p q : ℕ), link X i j p q ↔ link X' i j p q) : FactorEmbeds F X ↔ FactorEmbeds F' X'

Embedding reads only the tier words and links of the two representations.

theorem Autosegmental.AR.free_congr {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] {Y : TieredAR ι τ} [Finite Y.obj.V] (hw : ∀ (i : ι), tierWord i = tierWord i) (hl : ∀ (i j : ι) (p q : ℕ), link X i j p q ↔ link Y i j p q) (B : List { F : TieredAR ι τ // Finite F.obj.V }) : Free X B ↔ Free Y B

Freeness reads only the tier words and links.

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

Factor occurrences compose, offsets adding.

theorem Autosegmental.AR.FactorEmbeds.trans {ι : Type u_1} {τ : ι → Type u_2} {F : TieredAR ι τ} {X : TieredAR ι τ} [Finite F.obj.V] [Finite X.obj.V] {Y : TieredAR ι τ} [Finite Y.obj.V] (h : FactorEmbeds F X) (h' : FactorEmbeds X Y) : FactorEmbeds F Y

Factor embedding is transitive.

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 ([jardine-2019]'s link-free fragment).