Subregular Languages: Boundary Augmentation

Boundary augmentation of strings and a boundary-vacuity predicate relating the chain-membership of a padded string to that of its unpadded core. The strictly-local, locally-testable, and tier-relativized classes are built on this infrastructure. The contiguous k-factors the hierarchy quantifies over are a generic list combinator and live in Core/Data/List/Factors.lean (List.kFactors).

Main definitions

• Augmented α: boundary-augmented strings List (Option α), with none the boundary marker.
• boundary k w: w injected into Augmented α and padded with k - 1 boundary markers on each side.
• IsBoundaryVacuous R: R holds whenever either argument is the boundary marker none.

Main results

• IsBoundaryVacuous.isChain_boundary_two_iff: boundary padding does not change IsChain-membership for a boundary-vacuous relation.

Implementation notes

The standard subregular convention extends the alphabet with two edge markers ⋊, ⋉ and studies the k-factors of ⋊ᵏ⁻¹ · w · ⋉ᵏ⁻¹. We instead use the one-fresh-symbol extension Option α (none = boundary, some a = original symbol): a single marker suffices because boundary symbols only ever occur at fixed positions, so the two edges are never confused.

References

• [RP11]
• [HR10]
• [Lam22a]

Boundary augmentation

@[reducible, inline]

abbrev Augmented (α : Type u_2) : Type u_2

A boundary-augmented string has the original symbols (some a) and the boundary marker none.

Equations

• Augmented α = List (Option α)

def boundary {α : Type u_1} (k : ℕ) (w : List α) : Augmented α

w padded with k - 1 boundary markers (none) on each side.

Equations

• boundary k w = List.replicate (k - 1) none ++ List.map some w ++ List.replicate (k - 1) none

@[simp]

theorem boundary_one {α : Type u_1} (w : List α) : boundary 1 w = List.map some w

theorem length_boundary {α : Type u_1} (k : ℕ) (w : List α) : List.length (boundary k w) = w.length + 2 * (k - 1)

Position discrimination and windows

Entries of boundary k y are integer-indexed entries of the word (w[i]? with i : ℤ, blank outside [0, w.length)), shifted by the pad width; consequently the k-factors of the augmented word are exactly its windows (window).

def window {α : Type u_1} (k : ℕ) (w : List α) (i : ℤ) : List (Option α)

The width-k window of w at i lists its integer-indexed entries on [i, i + k).

Equations

• window k w i = List.ofFn fun (j : Fin k) => w[i + ↑↑j]?

@[simp]

theorem length_window {α : Type u_1} {k : ℕ} {w : List α} {i : ℤ} : (window k w i).length = k

theorem getElem?_window {α : Type u_1} {k j : ℕ} {w : List α} {i : ℤ} (h : j < k) : (window k w i)[j]? = some w[i + ↑j]?

theorem window_eq_window_iff {α : Type u_1} {k : ℕ} {w y : List α} {i q : ℤ} : window k w i = window k y q ↔ ∀ (j : ℕ), j < k → w[i + ↑j]? = y[q + ↑j]?

theorem getElem?_boundary {α : Type u_1} {k : ℕ} {w : List α} (j : ℕ) : (boundary k w)[j]? = if j < k - 1 then some none else if j < k - 1 + w.length then Option.map some w[j - (k - 1)]? else if j < w.length + 2 * (k - 1) then some none else none

The augmented string's entries split by region into left pad, letters, and right pad.

theorem of_getElem?_boundary_eq_some {α : Type u_1} {k : ℕ} {w : List α} {j : ℕ} {a : α} (h : (boundary k w)[j]? = some (some a)) : k - 1 ≤ j ∧ w[j - (k - 1)]? = some a

A letter entry sits in the letter region.

theorem of_getElem?_boundary_eq_none {α : Type u_1} {k : ℕ} {w : List α} {j : ℕ} (h : (boundary k w)[j]? = some none) : j < k - 1 ∨ k - 1 + w.length ≤ j

A marker entry sits in one of the pads.

theorem getElem?_boundary_eq_getElem?_int {α : Type u_1} {k : ℕ} {w : List α} {q : ℕ} (h : q < w.length + 2 * (k - 1)) : (boundary k w)[q]? = some w[↑q - ↑(k - 1)]?

Boundary entries are configuration values, shifted by the pad width.

theorem mem_kFactors_boundary_iff {α : Type u_1} {k : ℕ} {y : List α} {f : List (Option α)} (hk : 1 ≤ k) : f ∈ List.kFactors k (boundary k y) ↔ ∃ (i : ℤ), 1 - ↑k ≤ i ∧ i < ↑y.length ∧ f = window k y i

The k-factors of the augmented word are exactly its windows over [1 - k, w.length).

Boundary-vacuous relations

structure IsBoundaryVacuous {α : Type u_1} (R : Option α → Option α → Prop) : Prop

A relation on Option α is boundary-vacuous when none satisfies it on either side (R none u, R u none) — so only (some a, some b) pairs can witness a violation. Subregular edge constraints (OCP, no-clash, no-lapse) all share this shape.

• none_left (u : Option α) : R none u
• none_right (u : Option α) : R u none

theorem IsBoundaryVacuous.isChain_boundary_two_iff {α : Type u_1} {R : Option α → Option α → Prop} (hR : IsBoundaryVacuous R) (ys : List α) : List.IsChain R (boundary 2 ys) ↔ List.IsChain R (List.map some ys)

2-boundary padding preserves IsChain for a boundary-vacuous relation.