Forbidden-pair TSL_2 grammars

A tier-based strictly 2-local schema: for a forbidden-pair relation R : α → α → Prop and tier predicate p, TierStrictlyLocalGrammar.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 (R := (· = ·)); OCP-Feature and single-tier harmony (with p carrying blocking/transparency) are other choices of R.

Main definitions

• Subregular.TierStrictlyLocalGrammar.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_language_iff_filter_isChain: membership reduces to an IsChain (¬ R · ·) check on the tier-projected string.
• Subregular.mem_ofForbiddenPairs_language_map_iff: a word's image under a letter map is in the language exactly when the word is in the language of the pulled-back grammar.

Implementation notes

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

References

• [HRT11]
• [McC86]
• [McM16]
• [Han10]

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

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

Equations

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

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

A pair is clean for R unless both symbols are some and R-related, so 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.TierStrictlyLocalGrammar.ofForbiddenPairs {α : Type u_1} (R : α → α → Prop) (p : α → Prop) [DecidablePred p] : TierStrictlyLocalGrammar 2 α

The TSL_2 grammar banning tier-adjacent pairs satisfying R has tier p and permits everything but forbiddenPairs R.

Equations

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

theorem Subregular.mem_ofForbiddenPairs_language_iff_filter_isChain {α : Type u_1} (R : α → α → Prop) (p : α → Prop) [DecidablePred p] (w : List α) : w ∈ (TierStrictlyLocalGrammar.ofForbiddenPairs R p).language ↔ 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.

theorem Subregular.ofForbiddenPairs_language_congr {α : Type u_1} {R R' : α → α → Prop} {p p' : α → Prop} [DecidablePred p] [DecidablePred p'] (hp : ∀ (a : α), p a ↔ p' a) (hR : ∀ (a b : α), p a → p b → (R a b ↔ R' a b)) : (TierStrictlyLocalGrammar.ofForbiddenPairs R p).language = (TierStrictlyLocalGrammar.ofForbiddenPairs R' p').language

The language depends only on which symbols project and on R between on-tier symbols.

theorem Subregular.mem_ofForbiddenPairs_language_map_iff {α : Type u_1} {R : α → α → Prop} {β : Type u_2} (f : β → α) (p : α → Prop) [DecidablePred p] (w : List β) : List.map f w ∈ (TierStrictlyLocalGrammar.ofForbiddenPairs R p).language ↔ w ∈ (TierStrictlyLocalGrammar.ofForbiddenPairs (fun (x y : β) => R (f x) (f y)) fun (x : β) => p (f x)).language

A word's image under a letter-to-letter map is in a forbidden-pair language exactly when the word is in the language of the grammar with the pulled-back relation and tier.

Adjacent-pair counting

countAdjacent is the violation-count companion of the membership view; the optimality-theoretic Constraint.forbidPairs R is countAdjacent R itself.

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_map {α : Type u_1} (R : α → α → Prop) {β : Type u_2} {S : β → β → Prop} [DecidableRel R] [DecidableRel S] {f : α → β} (hf : ∀ (a b : α), S (f a) (f b) ↔ R a b) (xs : List α) : countAdjacent S (List.map f xs) = countAdjacent R xs

Counting adjacent pairs commutes with a relabelling that preserves and reflects the relation.

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

@[instance_reducible]

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

Membership in (ofForbiddenPairs R p).language 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] : [] ∈ (TierStrictlyLocalGrammar.ofForbiddenPairs R p).language

The empty string is in every forbidden-pair language.

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

Forbidding more pairs shrinks the language, so R ≤ R' gives language R' ≤ language R.

@[simp]

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

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

@[simp]

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

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

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

With no tier filtering (p = ⊤) the language is the SL_2 case, in which no two adjacent symbols of the raw string are R-related.

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

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] : (TierStrictlyLocalGrammar.ofForbiddenPairs (fun (a b : α) => R₁ a b ∨ R₂ a b) p).language = (TierStrictlyLocalGrammar.ofForbiddenPairs R₁ p).language ⊓ (TierStrictlyLocalGrammar.ofForbiddenPairs R₂ p).language

In lattice form, language (R₁ ∨ R₂) = lang R₁ ⊓ lang R₂ (mem_language_R_sup_iff).

Design boundary: non-monotonicity in the tier predicate

(ofForbiddenPairs R p).language 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.