Forbidden-pair TSL_2 grammars

A tier-based strictly 2-local schema [HRT11]: for a forbidden-pair relation R : α → α → Prop and tier predicate p, TSLGrammar.ofForbiddenPairs R p bans any string whose tier projection has an adjacent pair (a, b) with R a b. The canonical instance is the OCP [McC86] (R := (· = ·)); OCP-Feature and single-tier harmony (with p carrying blocking/transparency [McM16]) are other choices of R.

Main definitions

• Subregular.TSLGrammar.ofForbiddenPairs R p — the TSL_2 grammar above.
• Subregular.countAdjacent R xs — count of R-related adjacent pairs in xs.

Main results

• Subregular.mem_ofForbiddenPairs_lang_iff_filter_isChain — membership reduces to an IsChain (¬ R · ·) check on the tier-projected string.

Implementation notes

Out of scope (they need a richer-than-segmental alphabet): *Lapse/*Clash (SL_2 over a syllable alphabet) and *Coda (SL_1, via mkForbidSingletonOnTier). Similarity-graded [Han10] and interval-conditioned (ITSL) harmony, and cross-tier dependencies (MTSL), also fall outside this single-tier constructor.

def Subregular.forbiddenPairs {α : Type u_1} (R : α → α → Prop) : Set (Augmented α)

The forbidden 2-factors induced by R: the pairs [some a, some b] with R a b.

Equations

• Subregular.forbiddenPairs R = {f : Subregular.Augmented α | ∃ (a : α) (b : α), R a b ∧ f = [some a, some b]}

def Subregular.CleanPair {α : Type u_1} (R : α → α → Prop) : Option α → Option α → Prop

The adjacency relation for R: a pair is clean unless both symbols are some and R-related (none is vacuously clean — CleanPair.isBoundaryVacuous).

Equations

• Subregular.CleanPair R (some a) (some b) = ¬R a b
• Subregular.CleanPair R x✝¹ x✝ = True

@[simp]

theorem Subregular.CleanPair.none_left {α : Type u_1} {R : α → α → Prop} (u : Option α) : CleanPair R none u

@[simp]

theorem Subregular.CleanPair.none_right {α : Type u_1} {R : α → α → Prop} (u : Option α) : CleanPair R u none

theorem Subregular.CleanPair.some_some {α : Type u_1} {R : α → α → Prop} (a b : α) : CleanPair R (some a) (some b) ↔ ¬R a b

theorem Subregular.CleanPair.isBoundaryVacuous {α : Type u_1} {R : α → α → Prop} : IsBoundaryVacuous (CleanPair R)

CleanPair R is boundary-vacuous: none satisfies it on either side.

theorem Subregular.forbiddenPairFree_iff_isChain {α : Type u_1} (R : α → α → Prop) (xs : Augmented α) : (∀ f ∈ List.kFactors 2 xs, f ∉ forbiddenPairs R) ↔ List.IsChain (CleanPair R) xs

A list has no forbidden 2-factor iff it is a chain for CleanPair R.

def Subregular.TSLGrammar.ofForbiddenPairs {α : Type u_1} (R : α → α → Prop) (p : α → Prop) [DecidablePred p] : TSLGrammar 2 α

The TSL_2 grammar banning tier-adjacent pairs satisfying R: tier p, permitting everything but forbiddenPairs R.

Equations

• Subregular.TSLGrammar.ofForbiddenPairs R p = { tier := p, decTier := inst✝, permitted := (Subregular.forbiddenPairs R)ᶜ }

theorem Subregular.mem_ofForbiddenPairs_lang_iff_filter_isChain {α : Type u_1} (R : α → α → Prop) (p : α → Prop) [DecidablePred p] (w : List α) : w ∈ (TSLGrammar.ofForbiddenPairs R p).lang ↔ List.IsChain (fun (a b : α) => ¬R a b) (List.filter (fun (x : α) => decide (p x)) w)

Membership in ofForbiddenPairs R p reduces to an IsChain (¬ R · ·) check on the tier-projected string — the characterization all forbidden-pair constraints inherit.

Adjacent-pair counting

countAdjacent is the violation-count companion of the membership view; the OT-side mkForbidPairsOnTier consumes it via countAdjacent_eq_zero_iff_isChain.

def Subregular.countAdjacent {α : Type u_1} (R : α → α → Prop) [DecidableRel R] : List α → ℕ

Count of adjacent pairs (a, b) in xs with R a b.

Equations

• Subregular.countAdjacent R [] = 0
• Subregular.countAdjacent R [head] = 0
• Subregular.countAdjacent R (a :: b :: rest) = (if R a b then 1 else 0) + Subregular.countAdjacent R (b :: rest)

theorem Subregular.countAdjacent_eq_zero_iff_isChain {α : Type u_1} (R : α → α → Prop) [DecidableRel R] (xs : List α) : countAdjacent R xs = 0 ↔ List.IsChain (fun (a b : α) => ¬R a b) xs

countAdjacent R xs = 0 iff xs is a chain for ¬ R · ·.

API around ofForbiddenPairs

@[implicit_reducible]

instance Subregular.decidableMemOfForbiddenPairsLang {α : Type u_1} (R : α → α → Prop) [DecidableRel R] (p : α → Prop) [DecidablePred p] (w : List α) : Decidable (w ∈ (TSLGrammar.ofForbiddenPairs R p).lang)

Membership in (ofForbiddenPairs R p).lang is decidable, via the IsChain characterization.

Equations

• Subregular.decidableMemOfForbiddenPairsLang R p w = decidable_of_iff (List.IsChain (fun (a b : α) => ¬R a b) (List.filter (fun (x : α) => decide (p x)) w)) ⋯

@[simp]

theorem Subregular.nil_mem_ofForbiddenPairs_lang {α : Type u_1} (R : α → α → Prop) (p : α → Prop) [DecidablePred p] : [] ∈ (TSLGrammar.ofForbiddenPairs R p).lang

The empty string is in every forbidden-pair language.

theorem Subregular.lang_antitone_R {α : Type u_1} {R R' : α → α → Prop} (h : ∀ (a b : α), R a b → R' a b) (p : α → Prop) [DecidablePred p] : (TSLGrammar.ofForbiddenPairs R' p).lang ≤ (TSLGrammar.ofForbiddenPairs R p).lang

Forbidding more pairs shrinks the language: R ≤ R' gives lang R' ≤ lang R.

@[simp]

theorem Subregular.lang_R_bot {α : Type u_1} (p : α → Prop) [DecidablePred p] : (TSLGrammar.ofForbiddenPairs (fun (x x_1 : α) => False) p).lang = Set.univ

If no pair is forbidden (R = ⊥), the language is universal.

@[simp]

theorem Subregular.lang_p_bot {α : Type u_1} (R : α → α → Prop) : (TSLGrammar.ofForbiddenPairs R fun (x : α) => False).lang = Set.univ

If no symbol is on the tier (p = ⊥), the language is universal.

theorem Subregular.lang_p_top {α : Type u_1} (R : α → α → Prop) : (TSLGrammar.ofForbiddenPairs R fun (x : α) => True).lang = {w : List α | List.IsChain (fun (a b : α) => ¬R a b) w}

With no tier filtering (p = ⊤) the language is the SL_2 case: no two adjacent symbols of the raw string are R-related. (Not @[simp]: the RHS is no simpler than the LHS.)

theorem Subregular.mem_lang_R_sup_iff {α : Type u_1} (R₁ R₂ : α → α → Prop) (p : α → Prop) [DecidablePred p] (w : List α) : w ∈ (TSLGrammar.ofForbiddenPairs (fun (a b : α) => R₁ a b ∨ R₂ a b) p).lang ↔ w ∈ (TSLGrammar.ofForbiddenPairs R₁ p).lang ∧ w ∈ (TSLGrammar.ofForbiddenPairs R₂ p).lang

Forbidding R₁ ∨ R₂ on one tier is conjunctive membership in the two languages. (Cross-tier composition needs MTSL, not this constructor.)

theorem Subregular.lang_R_sup_eq_inf {α : Type u_1} (R₁ R₂ : α → α → Prop) (p : α → Prop) [DecidablePred p] : (TSLGrammar.ofForbiddenPairs (fun (a b : α) => R₁ a b ∨ R₂ a b) p).lang = (TSLGrammar.ofForbiddenPairs R₁ p).lang ⊓ (TSLGrammar.ofForbiddenPairs R₂ p).lang

Lattice form of mem_lang_R_sup_iff: lang (R₁ ∨ R₂) = lang R₁ ⊓ lang R₂.

Design boundary: non-monotonicity in the tier predicate

(ofForbiddenPairs R p).lang is neither monotone nor antitone in the tier predicate p (lang_p_not_monotone/lang_p_not_antitone below): which segments project is a substantive commitment, not just a monotone refinement.

@[implicit_reducible]

instance Subregular.instDecidableEqTwoSym : DecidableEq Subregular.TwoSym✝

Equations

• Subregular.instDecidableEqTwoSym x✝ y✝ = if h : Subregular.TwoSym.ctorIdx✝ x✝ = Subregular.TwoSym.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯