AGREE as a tier-based strictly 2-local language

This file characterizes AGREE-style markedness as a tier-based strictly 2-local (TSL₂) language. AGREE requires tier-adjacent symbols to be equal, so it is the dual of the OCP, which requires them to differ. Both specialize the forbidden-pair constraint Constraint.forbidPairs of OptimalityTheory/Constraint/ForbiddenPairs.lean, AGREE with R := (· ≠ ·) and the OCP with R := (· = ·). Consonant harmony, vowel harmony, and tone spreading factor through TierStrictlyLocalGrammar.agree, while dissimilation, anti-gemination, and Meeussen's rule factor through TierStrictlyLocalGrammar.ocp, and asymmetric patterns instantiate the generic constructor with their own relation.

Because equality is transitive, AGREE is also strictly piecewise, and the tier projection is dispensable. So is any forbidden-pair grammar whose permitted pairs are transitive on the tier, such as agreement in a feature value. This lets transparent long-distance harmony be described either way, as McMullin observes, whereas the OCP has no such reading.

Main definitions

• agreeForbidden, AgreeCleanPair, TierStrictlyLocalGrammar.agree: the AGREE instances of the forbidden-pair constructions.
• StrictlyPiecewiseGrammar.ofForbiddenPairs, StrictlyPiecewiseGrammar.agree: the strictly 2-piecewise grammars banning a pair of on-tier symbols however far apart.

Main results

• Constraint.zeroSet_comap_filter_agree: on a tier, the zero set of the AGREE constraint is the language of TierStrictlyLocalGrammar.agree.
• TierStrictlyLocalGrammar.ofForbiddenPairs_language_eq_sp: when the permitted pairs are transitive on the tier, the tier-based and subsequence-based grammars generate the same language; TierStrictlyLocalGrammar.agree_language_eq_sp is the AGREE instance.

References

• [McM16]

def Subregular.agreeForbidden (α : Type u_2) [DecidableEq α] : Set (Augmented α)

The forbidden 2-factors for AGREE are the pairs [some x, some y] of two distinct non-boundary symbols, the inequality instance of forbiddenPairs.

Equations

• Subregular.agreeForbidden α = Subregular.forbiddenPairs fun (x1 x2 : α) => x1 ≠ x2

def Subregular.TierStrictlyLocalGrammar.agree {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] : TierStrictlyLocalGrammar 2 α

The TSL₂ grammar of AGREE forbids two adjacent distinct symbols on the tier defined by p, so every tier-adjacent pair agrees. It is the inequality instance of TierStrictlyLocalGrammar.ofForbiddenPairs.

Equations

• Subregular.TierStrictlyLocalGrammar.agree p = Subregular.TierStrictlyLocalGrammar.ofForbiddenPairs (fun (x1 x2 : α) => x1 ≠ x2) p

def Subregular.AgreeCleanPair {α : Type u_1} [DecidableEq α] : Option α → Option α → Prop

Two augmented symbols are AGREE-clean as a pair iff they are not both some of distinct values. This is the inequality instance of CleanPair.

Equations

• Subregular.AgreeCleanPair = Subregular.CleanPair fun (x1 x2 : α) => x1 ≠ x2

theorem Subregular.agreeCleanPair_some_some {α : Type u_1} [DecidableEq α] (a b : α) : AgreeCleanPair (some a) (some b) ↔ a = b

theorem Subregular.AgreeCleanPair.isBoundaryVacuous {α : Type u_1} [DecidableEq α] : IsBoundaryVacuous AgreeCleanPair

The AGREE relation is boundary-vacuous, the inequality instance of CleanPair.isBoundaryVacuous.

Transitive agreement is strictly piecewise

When the permitted pairs ¬ R are transitive on the tier, "every tier-adjacent pair is permitted" and "every pair of on-tier symbols is permitted, however far apart" are the same condition. The latter reads subsequences, which are blind to the intervening material the tier projection deletes, so the language is SP₂ as well as TSL₂. Equality is transitive, so AGREE languages are SP₂ ([McM16]), as is agreement in any feature value. The OCP has no such reading, since ≠ is not transitive.

def Subregular.StrictlyPiecewiseGrammar.ofForbiddenPairs {α : Type u_1} (R : α → α → Prop) (p : α → Prop) : StrictlyPiecewiseGrammar α

The SP₂ grammar dual to TierStrictlyLocalGrammar.ofForbiddenPairs R p permits every subsequence except an R-related pair of on-tier symbols, and permits shorter subsequences outright.

Equations

• Subregular.StrictlyPiecewiseGrammar.ofForbiddenPairs R p = {s : List α | ∀ (a b : α), s = [a, b] → p a → p b → ¬R a b}

def Subregular.StrictlyPiecewiseGrammar.agree {α : Type u_1} (p : α → Prop) : StrictlyPiecewiseGrammar α

The SP₂ grammar dual to TierStrictlyLocalGrammar.agree p permits every subsequence except a pair of disagreeing on-tier symbols.

Equations

• Subregular.StrictlyPiecewiseGrammar.agree p = Subregular.StrictlyPiecewiseGrammar.ofForbiddenPairs (fun (x1 x2 : α) => x1 ≠ x2) p

theorem Subregular.mem_ofForbiddenPairs_language_iff_forall_sublist_pair {α : Type u_1} {R : α → α → Prop} {p : α → Prop} [DecidablePred p] (hR : ∀ (a b c : α), p a → p b → p c → ¬R a b → ¬R b c → ¬R a c) (w : List α) : w ∈ (TierStrictlyLocalGrammar.ofForbiddenPairs R p).language ↔ ∀ (a b : α), [a, b].Sublist w → p a → p b → ¬R a b

If the permitted pairs are transitive on the tier, membership is permission of all pairs of on-tier symbols, not just the tier-adjacent ones.

theorem Subregular.TierStrictlyLocalGrammar.ofForbiddenPairs_language_eq_sp {α : Type u_1} {R : α → α → Prop} {p : α → Prop} [DecidablePred p] (hR : ∀ (a b c : α), p a → p b → p c → ¬R a b → ¬R b c → ¬R a c) : (ofForbiddenPairs R p).language = StrictlyPiecewiseGrammar.language 2 (StrictlyPiecewiseGrammar.ofForbiddenPairs R p)

The tier-based and subsequence-based descriptions generate the same language when the permitted pairs are transitive on the tier.

theorem Subregular.TierStrictlyLocalGrammar.ofForbiddenPairs_language_isStrictlyPiecewise {α : Type u_1} {R : α → α → Prop} {p : α → Prop} [DecidablePred p] (hR : ∀ (a b c : α), p a → p b → p c → ¬R a b → ¬R b c → ¬R a c) : (ofForbiddenPairs R p).language.IsStrictlyPiecewise 2

theorem Subregular.mem_agree_lang_iff_forall_sublist_pair {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (w : List α) : w ∈ (TierStrictlyLocalGrammar.agree p).language ↔ ∀ (a b : α), [a, b].Sublist w → p a → p b → a = b

Membership in the AGREE language is agreement of all pairs of on-tier symbols, not just the tier-adjacent ones.

theorem Subregular.TierStrictlyLocalGrammar.agree_language_eq_sp {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] : (agree p).language = StrictlyPiecewiseGrammar.language 2 (StrictlyPiecewiseGrammar.agree p)

The tier-based and subsequence-based descriptions of agreement generate the same language, for any tier predicate.

theorem Subregular.TierStrictlyLocalGrammar.agree_language_isStrictlyPiecewise {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] : (agree p).language.IsStrictlyPiecewise 2

Every AGREE language is strictly 2-piecewise.

theorem OptimalityTheory.Constraint.agree_eq_zero_iff {α : Type u_1} [DecidableEq α] (w : List α) : agree w = 0 ↔ List.IsChain (fun (x1 x2 : α) => x1 = x2) w

A string satisfies AGREE iff its adjacent elements are equal, so that all its elements are equal.

theorem OptimalityTheory.Constraint.zeroSet_comap_filter_agree {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] : (comap (fun (w : List α) => List.filter (fun (x : α) => decide (p x)) w) agree).zeroSet = (Subregular.TierStrictlyLocalGrammar.agree p).language

On the tier p, the zero set of AGREE is the language of the TSL₂ grammar TierStrictlyLocalGrammar.agree p, so the optimality-theoretic constraint and the subregular class are co-extensive.