The OCP as a tier-based strictly 2-local language

This file characterizes the Obligatory Contour Principle (OCP) of Goldsmith and McCarthy as a tier-based strictly 2-local (TSL₂) language. The OCP constraint Constraint.ocp is the identity instance of the forbidden-pair constraint Constraint.forbidPairs of OptimalityTheory/Constraint/ForbiddenPairs.lean. Its forbidden 2-factor is [some x, some x], and its TSL₂ grammar is TierStrictlyLocalGrammar.ofForbiddenPairs (· = ·) p. Without a tier, the OCP is the linguistic instance of Thue's square-free words. Thue showed that infinite square-free words exist over three letters, while every binary string of length at least 4 contains a square, so a binary tonal alphabet cannot satisfy a strict OCP at length.

The satisfaction predicate of the TSL₂ language is exactly OCP.IsClean, which the fusion repair OCP.collapse also lands in, and the repair is itself a 2-input strictly local map (Chandlee and Heinz). The prohibition and the merger are therefore the constraint and a retraction onto it, both subregular.

Main definitions

• ocpForbidden, OCPCleanPair, TierStrictlyLocalGrammar.ocp: the OCP instances of the forbidden-pair constructions.

Main results

• Constraint.ocp_eq_zero_iff_isClean: the OCP constraint scores zero exactly on OCP.IsClean strings.
• Constraint.zeroSet_comap_filter_ocp: on a tier, its zero set is the language of TierStrictlyLocalGrammar.ocp.
• collapse_isISL: the fusion repair OCP.collapse is 2-input strictly local.

References

• J. A. Goldsmith, Autosegmental Phonology (1976)
• J. J. McCarthy, OCP Effects: Gemination and Antigemination (1986)
• A. Thue, Über unendliche Zeichenreihen (1906)
• J. Chandlee and J. Heinz, Strict Locality and Phonological Maps (2018)
• J. Chandlee and A. Jardine, Autosegmental Input Strictly Local Functions (2019)

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

The forbidden 2-factors for the OCP are the pairs [some x, some x] of two identical non-boundary symbols, the identity instance of forbiddenPairs.

Equations

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

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

The TSL₂ grammar of the OCP forbids two adjacent identical symbols on the tier defined by p. It is the identity instance of TierStrictlyLocalGrammar.ofForbiddenPairs.

Equations

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

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

Two augmented symbols are OCP-clean as a pair iff they are not both some of the same value. This is the identity instance of CleanPair.

Equations

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

theorem Subregular.ocpCleanPair_some_some {α : Type u_1} [DecidableEq α] (a b : α) : OCPCleanPair (some a) (some b) ↔ a ≠ b

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

The OCP relation is boundary-vacuous, the identity instance of CleanPair.isBoundaryVacuous.

The repair is subregular

theorem Subregular.collapse_isISL {α : Type u_1} [DecidableEq α] : IsLeftInputStrictlyLocal 2 OCP.collapse

The OCP fusion repair OCP.collapse is a 2-input strictly local string function ([CH18]), which scans left to right with a one-symbol window and deletes a symbol iff it equals its predecessor. [CJ19] classify tonal OCP processes as autosegmental input strictly local.

theorem OptimalityTheory.Constraint.ocp_eq_zero_iff_isClean {α : Type u_1} [DecidableEq α] (w : List α) : ocp w = 0 ↔ OCP.IsClean w

A string satisfies the OCP iff it is OCP.IsClean. Since the fusion repair OCP.collapse also characterizes OCP.IsClean, the prohibition and the repair are two faces of one principle rather than parallel formalizations.

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

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