Subregular Languages — Boundaries and k-Factors

Common infrastructure for the subregular hierarchy @cite{lambert-2022} @cite{heinz-rogers-2010} @cite{rogers-pullum-2011}: boundary augmentation of strings, contiguous k-factors with boundary padding, and the factor-membership predicate that all of StrictlyLocal, LocallyTestable, and their tier-relativized variants build on.

Why Option α for boundaries

The canonical subregular convention extends the alphabet with edge markers ⋊ (left) and ⋉ (right) and studies k-factors of ⋊ᵏ⁻¹ · w · ⋉ᵏ⁻¹. Mathlib's idiomatic way to extend an alphabet by one fresh symbol is Option α: none is the new boundary, some a an original symbol. Two distinct edges are unnecessary — boundary symbols only appear at fixed positions by construction.

Main definitions

• Augmented α — abbreviation for List (Option α).
• boundary k w — w.map some padded with k - 1 boundary symbols on each side.
• kFactors k xs — the contiguous length-k infixes of xs, built as (xs.tails.filter (k ≤ ·.length)).map (·.take k).

@[reducible, inline]

abbrev Core.Computability.Subregular.Augmented (α : Type u_3) : Type u_3

A boundary-augmented string: an alphabet symbol or the boundary marker none. Lambert's ⋊ and ⋉ collapse to the single none symbol here, since edges only appear at fixed positions by construction.

Equations

• Core.Computability.Subregular.Augmented α = List (Option α)

def Core.Computability.Subregular.boundary {α : Type u_1} (k : ℕ) (w : List α) : Augmented α

Boundary-augment a string with k - 1 boundary markers on each side. For k ≤ 1 no padding is added (no k-factor can span the edge).

Equations

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

@[simp]

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

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

def Core.Computability.Subregular.kFactors {β : Type u_2} (k : ℕ) (xs : List β) : List (List β)

The contiguous length-k infixes of xs. Built by enumerating suffixes and taking each one's length-k prefix; suffixes shorter than k are filtered out.

Equations

• Core.Computability.Subregular.kFactors k xs = List.map (fun (x : List β) => List.take k x) (List.filter (fun (x : List β) => decide (k ≤ x.length)) xs.tails)

theorem Core.Computability.Subregular.length_of_mem_kFactors {β : Type u_2} {k : ℕ} {f xs : List β} (h : f ∈ kFactors k xs) : f.length = k

Every member of kFactors k xs has length exactly k.

theorem Core.Computability.Subregular.isInfix_of_mem_kFactors {β : Type u_2} {k : ℕ} {f xs : List β} (h : f ∈ kFactors k xs) : f <:+: xs

A k-factor of xs is a contiguous infix of xs. The witness is a prefix (take) of a suffix (tails), and prefix-of-suffix is infix.

@[implicit_reducible]

instance Core.Computability.Subregular.instDecidableMemListKFactorsOfDecidableEq {β : Type u_2} [DecidableEq β] (k : ℕ) (f xs : List β) : Decidable (f ∈ kFactors k xs)

Equations

• Core.Computability.Subregular.instDecidableMemListKFactorsOfDecidableEq k f xs = id inferInstance

theorem Core.Computability.Subregular.kFactors_two_cons_cons {β : Type u_2} (a b : β) (rest : List β) : kFactors 2 (a :: b :: rest) = [a, b] :: kFactors 2 (b :: rest)

The 2-factors of a :: b :: rest are [a, b] followed by the 2-factors of b :: rest. Specialization of kFactors to k = 2 for the inductive step in chain-based characterizations of SL_2 and TSL_2 languages.

@[simp]

theorem Core.Computability.Subregular.kFactors_two_nil {β : Type u_2} : kFactors 2 [] = []

An empty list has no 2-factors.

@[simp]

theorem Core.Computability.Subregular.kFactors_two_singleton {β : Type u_2} (a : β) : kFactors 2 [a] = []

A singleton list has no 2-factors.

structure Core.Computability.Subregular.IsBoundaryVacuous {α : Type u_1} (R : Option α → Option α → Prop) : Prop

A relation on Option α is boundary-vacuous when the boundary marker none satisfies it on either side: R none u and R u none always hold. Equivalently, only (some a, some b) pairs can witness a violation.

Boundary-vacuity captures the property of subregular constraints that hold trivially at string edges — the OCP relation, the no-clash relation, the no-lapse relation all share this shape. The chain-membership of a boundary-padded augmented string is then equivalent to the chain-membership of the unpadded core (isChain_boundary_two_iff).

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

theorem Core.Computability.Subregular.IsBoundaryVacuous.isChain_none_cons_iff {α : Type u_1} {R : Option α → Option α → Prop} (hR : IsBoundaryVacuous R) (xs : Augmented α) : List.IsChain R (none :: xs) ↔ List.IsChain R xs

Prepending none to a list preserves chain-membership for any boundary-vacuous relation.

theorem Core.Computability.Subregular.IsBoundaryVacuous.isChain_append_singleton_none_iff {α : Type u_1} {R : Option α → Option α → Prop} (hR : IsBoundaryVacuous R) (xs : Augmented α) : List.IsChain R (xs ++ [none]) ↔ List.IsChain R xs

Appending [none] to a list preserves chain-membership for any boundary-vacuous relation.

theorem Core.Computability.Subregular.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)

The 2-boundary padding [none] · _ · [none] preserves chain-membership for any boundary-vacuous relation.

Generic List.IsChain helpers

Alphabet-generic facts about List.IsChain that mathlib does not currently expose; the natural home is Mathlib.Data.List.Chain once they pay for themselves across more consumers (a future MTSL formalisation will combine per-tier IsChain witnesses via List.IsChain.and).

theorem List.isChain_top {α : Type u_1} (l : List α) : IsChain (fun (x x_1 : α) => True) l

Any list is a chain for the universal-true relation. The trivial case of IsChain for a relation that places no constraint on adjacent elements.

theorem List.IsChain.and {α : Type u_1} {S T : α → α → Prop} {l : List α} : IsChain S l → IsChain T l → IsChain (fun (a b : α) => S a b ∧ T a b) l

Two IsChain witnesses on the same list combine into a chain for the conjunction relation. The companion of mathlib's List.IsChain.imp.