Definite and Reverse-Definite Languages (D_k, RD_k)

A language L is k-definite when membership is determined by the last k symbols of the input @cite{rogers-pullum-2011} @cite{lambert-2022}: any two strings agreeing on their length-k suffix are L-equivalent. The dual notion, reverse k-definite (RD_k), checks the length-k prefix instead.

These are weaker than SL_k in expressive power — they look at one fixed position (the edge) rather than every contiguous window — but they are foundational for the right- and left-context-only fragments of finite-state computation. Concrete linguistic uses include word-final neutralization (D_1 / D_2: a constraint on the last few segments) and word-initial prosodic templates (RD_k).

Strictly definite vs definite

The classical definite/strictly-definite distinction collapses for the generative formulation used here: a language is definite iff it is strictly definite (the permitted-suffix set is just the suffixes of L-members), so we use a single DefiniteGrammar type and elide the "strictly" qualifier.

No boundary augmentation

Unlike SL/LT, D and RD do not use boundary symbols: the suffix/prefix already privileges the edge structurally, and adding none markers would just shift indexing by k - 1. The grammar's permitted set is over the raw alphabet α, not Augmented α.

Edge parameterization

Both D_k and RD_k are parameterized over an Edge (right vs left), so a single EdgeDefiniteGrammar covers both classes; DefiniteGrammar and ReverseDefiniteGrammar are abbreviations selecting the right and left edges respectively.

Generalised definite and finite-or-cofinite

This file also houses two related affix-based classes from @cite{lambert-2026}:

• IsGeneralizedDefinite k (Lambert's ℒℐ_k): membership is determined by the joint length-k prefix and length-k suffix. Strictly more expressive than IsDefinite k ⊔ IsReverseDefinite k because a single formula can simultaneously constrain both edges.
• IsFiniteOrCofinite (Lambert's 𝒩, see Lambert (2026) p. 8 fn. 4): the classical co/finite class, finite sets and complements thereof. Equals IsDefinite k ∩ IsReverseDefinite k for sufficiently large k.

Both are derived predicates (not new structural grammars): the algebra they characterise is already captured by EdgeDefiniteGrammar and Set.Finite.

inductive Core.Computability.Subregular.Edge : Type

Which edge of the string the definite test inspects. right gives classical D_k (final substring); left gives RD_k (initial substring).

• left : Edge
• right : Edge

@[implicit_reducible]

instance Core.Computability.Subregular.instDecidableEqEdge : DecidableEq Edge

Equations

• Core.Computability.Subregular.instDecidableEqEdge x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Computability.Subregular.instReprEdge : Repr Edge

Equations

• Core.Computability.Subregular.instReprEdge = { reprPrec := Core.Computability.Subregular.instReprEdge.repr }

def Core.Computability.Subregular.instReprEdge.repr : Edge → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Core.Computability.Subregular.Edge.takeAt {α : Type u_1} (e : Edge) (k : ℕ) (xs : List α) : List α

Take the length-k substring at this edge of xs. right returns the last k symbols; left returns the first k. Strings shorter than k are returned in full.

Equations

• Core.Computability.Subregular.Edge.left.takeAt k xs = List.take k xs
• Core.Computability.Subregular.Edge.right.takeAt k xs = List.drop (xs.length - k) xs

def Core.Computability.Subregular.Edge.combine {M : Type u_2} [Mul M] (e : Edge) (x s : M) : M

Edge-parameterized monoid combination. The "anchor" element x sits on the side dictated by e (left edge → x is on the left, right edge → x is on the right); s multiplies on the opposite side. Concretely:

• combine .left x s = x * s (anchor on left, s appended)
• combine .right x s = s * x (anchor on right, s prepended)

This unifies the two structurally-symmetric monoid operations that appear in Pin's algebraic equations:

• D (definite, suffix-determined) uses combine .right [αs] s = s · [αs]
• K (reverse-definite, prefix-determined) uses combine .left [αs] s = [αs] · s

The Edge tag selects which edge is "load-bearing" for membership; s is the absorbed element acting from the opposite end.

Equations

• Core.Computability.Subregular.Edge.left.combine x s = x * s
• Core.Computability.Subregular.Edge.right.combine x s = s * x

@[simp]

theorem Core.Computability.Subregular.Edge.combine_left {M : Type u_2} [Mul M] (x s : M) : left.combine x s = x * s

@[simp]

theorem Core.Computability.Subregular.Edge.combine_right {M : Type u_2} [Mul M] (x s : M) : right.combine x s = s * x

structure Core.Computability.Subregular.EdgeDefiniteGrammar (k : ℕ) (e : Edge) (α : Type u_2) : Type u_2

An edge-definite k-grammar over α: a set of permitted length-(≤k) edge substrings. A string is accepted iff its Edge length-k substring is permitted.

• permitted : Set (List α)

  The set of permitted length-(≤k) edge substrings.

theorem Core.Computability.Subregular.EdgeDefiniteGrammar.ext {k : ℕ} {e : Edge} {α : Type u_2} {x y : EdgeDefiniteGrammar k e α} (permitted : x.permitted = y.permitted) : x = y

theorem Core.Computability.Subregular.EdgeDefiniteGrammar.ext_iff {k : ℕ} {e : Edge} {α : Type u_2} {x y : EdgeDefiniteGrammar k e α} : x = y ↔ x.permitted = y.permitted

@[implicit_reducible]

instance Core.Computability.Subregular.EdgeDefiniteGrammar.instInhabited {α : Type u_1} {k : ℕ} {e : Edge} : Inhabited (EdgeDefiniteGrammar k e α)

Equations

• Core.Computability.Subregular.EdgeDefiniteGrammar.instInhabited = { default := { permitted := Set.univ } }

def Core.Computability.Subregular.EdgeDefiniteGrammar.lang {α : Type u_1} {k : ℕ} {e : Edge} (G : EdgeDefiniteGrammar k e α) : Language α

The language generated: strings whose Edge length-k substring is permitted.

Equations

• G.lang w = (e.takeAt k w ∈ G.permitted)

@[simp]

theorem Core.Computability.Subregular.EdgeDefiniteGrammar.mem_lang {α : Type u_1} {k : ℕ} {e : Edge} (G : EdgeDefiniteGrammar k e α) (w : List α) : w ∈ G.lang ↔ e.takeAt k w ∈ G.permitted

@[reducible, inline]

abbrev Core.Computability.Subregular.DefiniteGrammar (k : ℕ) (α : Type u_2) : Type u_2

A k-definite grammar: edge-definite at the right (final substring).

Equations

• Core.Computability.Subregular.DefiniteGrammar k α = Core.Computability.Subregular.EdgeDefiniteGrammar k Core.Computability.Subregular.Edge.right α

@[reducible, inline]

abbrev Core.Computability.Subregular.ReverseDefiniteGrammar (k : ℕ) (α : Type u_2) : Type u_2

A reverse k-definite grammar: edge-definite at the left (initial substring).

Equations

• Core.Computability.Subregular.ReverseDefiniteGrammar k α = Core.Computability.Subregular.EdgeDefiniteGrammar k Core.Computability.Subregular.Edge.left α

def Core.Computability.Subregular.IsDefinite {α : Type u_1} (k : ℕ) (L : Language α) : Prop

A language L is k-definite at the right edge iff some DefiniteGrammar k α generates exactly L.

Equations

• Core.Computability.Subregular.IsDefinite k L = ∃ (G : Core.Computability.Subregular.DefiniteGrammar k α), Core.Computability.Subregular.EdgeDefiniteGrammar.lang G = L

def Core.Computability.Subregular.IsReverseDefinite {α : Type u_1} (k : ℕ) (L : Language α) : Prop

A language L is reverse k-definite (left-edge) iff some ReverseDefiniteGrammar k α generates exactly L.

Equations

• Core.Computability.Subregular.IsReverseDefinite k L = ∃ (G : Core.Computability.Subregular.ReverseDefiniteGrammar k α), Core.Computability.Subregular.EdgeDefiniteGrammar.lang G = L

Generalised definite (ℒℐ_k)

def Core.Computability.Subregular.IsGeneralizedDefinite {α : Type u_1} (k : ℕ) (L : Language α) : Prop

A language L is generalized k-definite iff strings agreeing on both their length-k prefix and length-k suffix have the same membership in L (@cite{lambert-2026} Prop 16). Derived predicate: the class is the conjunction of left-edge and right-edge k-definite tests, no new structural grammar required.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Computability.Subregular.IsDefinite.toIsGeneralizedDefinite {α : Type u_1} {k : ℕ} {L : Language α} (h : IsDefinite k L) : IsGeneralizedDefinite k L

D_k ⊆ ℒℐ_k: every k-definite language is generalized k-definite. The right-edge test alone determines membership, so the joint prefix-and-suffix hypothesis is more than sufficient.

theorem Core.Computability.Subregular.IsReverseDefinite.toIsGeneralizedDefinite {α : Type u_1} {k : ℕ} {L : Language α} (h : IsReverseDefinite k L) : IsGeneralizedDefinite k L

RD_k ⊆ ℒℐ_k: every reverse k-definite language is generalized k-definite.

Finite or cofinite (𝒩)

def Core.Computability.Subregular.IsFiniteOrCofinite {α : Type u_1} (L : Language α) : Prop

A language L is finite-or-cofinite iff either L itself is finite, or its complement Lᶜ is finite (@cite{lambert-2026} p. 8 fn 4). This is the smallest interesting Boolean-closed subregular class: intersection of the definite and reverse-definite classes for sufficiently large k.

Equations

• Core.Computability.Subregular.IsFiniteOrCofinite L = (Set.Finite L ∨ Set.Finite Lᶜ)

Co/finite = D ∩ RD (classical Pin/Eilenberg theorem)

A language is finite-or-cofinite iff it is k-definite for some k and reverse-k'-definite for some k'. This is a language-level theorem: pure list combinatorics, no syntactic-monoid content. The algebraic counterpart (Pin's 𝒩 = ⟦sx^ω = x^ω = x^ω s⟧ characterization) lives in SyntacticMonoid/Pin.lean.

theorem Core.Computability.Subregular.IsFiniteOrCofinite.exists_isDefinite_and_isReverseDefinite {α : Type u_1} {L : Language α} (h : IsFiniteOrCofinite L) : (∃ (k : ℕ), IsDefinite k L) ∧ ∃ (k' : ℕ), IsReverseDefinite k' L

Forward direction of Pin's 𝒩 = 𝒟 ∩ 𝒦 theorem: a finite-or-cofinite language is both k-definite and reverse-k'-definite for some k, k'.

theorem Core.Computability.Subregular.isFiniteOrCofinite_of_isDefinite_and_isReverseDefinite {α : Type u_1} [Finite α] {L : Language α} (h : (∃ (k : ℕ), IsDefinite k L) ∧ ∃ (k' : ℕ), IsReverseDefinite k' L) : IsFiniteOrCofinite L

Reverse direction of Pin's 𝒩 = 𝒟 ∩ 𝒦 theorem (α-finite case): if L is both k-definite and reverse-k'-definite, AND the alphabet is finite, then L is finite-or-cofinite.

The α-finiteness hypothesis is necessary: with infinite α, words of bounded length need not form a finite set. The phonology context (@cite{lambert-2026}) implicitly assumes finite alphabets.

Proof sketch: for words of length ≥ k + k', membership is constant. Bridge argument: any two such words w₁, w₂ are related via w' = w₂.take k' ++ w₁.drop (w₁.length - k) of length k' + k. By k-definiteness applied to (w₁, w'), they share L-membership; by reverse-k'-definiteness applied to (w', w₂), they share L-membership. Then either all long words are in L (so Lᶜ is bounded, hence finite) or none are (so L is bounded).

theorem Core.Computability.Subregular.isFiniteOrCofinite_iff_exists_isDefinite_and_isReverseDefinite {α : Type u_1} [Finite α] {L : Language α} : IsFiniteOrCofinite L ↔ (∃ (k : ℕ), IsDefinite k L) ∧ ∃ (k' : ℕ), IsReverseDefinite k' L

Pin's 𝒩 = 𝒟 ∩ 𝒦 theorem (α-finite case): a language over a finite alphabet is finite-or-cofinite iff it is both k-definite for some k and reverse-k'-definite for some k'.