The Obligatory Contour Principle

The Obligatory Contour Principle (OCP) bans two identical adjacent autosegments on one tier. Here it is categorical and bans strict identity, either on the tier itself (IsClean, after Leben and McCarthy) or on a projection of it (IsCleanOn, after Chandlee and Jardine). Fusion, collapse, repairs a violation by merging each run of identical elements into one; it is List.destutter (· ≠ ·), a retraction onto the clean tiers. mergeAppend concatenates two words and merges identical elements at the seam only; the collapse of a concatenation is the merging append of the collapses. The run index runIdx tracks where each position lands under fusion. Phonology/Subregular/OCP.lean shows that the constraint is tier-based strictly local and that fusion is input strictly local.

The gradient OCP of Frisch, Pierrehumbert and Broe, which scales with the similarity of the two consonants, is a different object and lives in that paper's study.

Main definitions

• OCP.IsClean, OCP.IsCleanOn: no two identical adjacent elements, on the tier or on a projection of it.
• OCP.collapse: the fusion repair.
• OCP.mergeAppend: concatenation that merges identical elements at the seam.
• OCP.runIdx: the index of the run containing a position.

Main statements

• OCP.collapse_eq_self_iff: collapse fixes exactly the clean tiers.
• OCP.collapse_append: the collapse of a concatenation is the merging append of the collapses.
• OCP.runIdx_append_left, OCP.runIdx_append_right: the run indices of a concatenation.

References

• [Leb73]
• [Gol76]
• [McC86]
• [McCP95]
• [FPB04]
• [HRT11]
• [CH18]
• [CJ19]

The constraint

@[reducible, inline]

abbrev OCP.IsClean {α : Type u_1} (xs : List α) : Prop

A tier is OCP-clean when no two adjacent elements are identical. This is weaker than List.Nodup, since [1, 2, 1] is clean. It is a reducible alias of List.IsChain (· ≠ ·), so that API applies.

Equations

• OCP.IsClean xs = List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) xs

@[simp]

theorem OCP.isClean_nil {α : Type u_1} : IsClean []

@[simp]

theorem OCP.isClean_singleton {α : Type u_1} (x : α) : IsClean [x]

@[simp]

theorem OCP.isClean_cons_cons_iff {α : Type u_1} (x y : α) (rs : List α) : IsClean (x :: y :: rs) ↔ x ≠ y ∧ IsClean (y :: rs)

def OCP.IsCleanOn {α : Type u_1} {β : Type u_2} (p : α → Prop) [DecidablePred p] (proj : α → β) (xs : List α) : Prop

The OCP on the tier projected from xs by keeping the p-elements and reading them through proj. Flat IsClean is the case p = ⊤, proj = id.

Equations

• OCP.IsCleanOn p proj xs = OCP.IsClean (List.map proj (List.filter (fun (a : α) => decide (p a)) xs))

@[instance_reducible]

instance OCP.decidableIsClean {α : Type u_1} [DecidableEq α] : DecidablePred IsClean

Equations

• OCP.decidableIsClean xs = xs.instDecidableIsChainOfDecidableRel

@[instance_reducible]

instance OCP.decidableIsCleanOn {α : Type u_1} {β : Type u_2} [DecidableEq β] (p : α → Prop) [DecidablePred p] (proj : α → β) : DecidablePred (IsCleanOn p proj)

Equations

• OCP.decidableIsCleanOn p proj x✝ = OCP.decidableIsCleanOn._aux_1 p proj x✝

The fusion repair

def OCP.collapse {α : Type u_1} [DecidableEq α] (xs : List α) : List α

The fusion repair merges each maximal run of identical adjacent elements into one.

Equations

• OCP.collapse xs = List.destutter (fun (x1 x2 : α) => x1 ≠ x2) xs

theorem OCP.collapse_eq_destutter {α : Type u_1} [DecidableEq α] (xs : List α) : collapse xs = List.destutter (fun (x1 x2 : α) => x1 ≠ x2) xs

@[simp]

theorem OCP.collapse_nil {α : Type u_1} [DecidableEq α] : collapse [] = []

@[simp]

theorem OCP.collapse_singleton {α : Type u_1} [DecidableEq α] (x : α) : collapse [x] = [x]

@[simp]

theorem OCP.collapse_replicate {α : Type u_1} [DecidableEq α] (n : ℕ) (a : α) : collapse (List.replicate (n + 1) a) = [a]

collapse fuses a constant run into its single autosegment.

theorem OCP.collapse_clean {α : Type u_1} [DecidableEq α] (xs : List α) : IsClean (collapse xs)

collapse lands in the OCP-clean set.

theorem OCP.collapse_idempotent_on_clean {α : Type u_1} [DecidableEq α] {xs : List α} (h : IsClean xs) : collapse xs = xs

collapse fixes OCP-clean lists.

@[simp]

theorem OCP.collapse_eq_self_iff {α : Type u_1} [DecidableEq α] (xs : List α) : collapse xs = xs ↔ IsClean xs

collapse fixes exactly the OCP-clean tiers, so with collapse_clean it is a retraction onto them.

theorem OCP.collapse_idempotent {α : Type u_1} [DecidableEq α] (xs : List α) : collapse (collapse xs) = collapse xs

The fusion repair is a retraction onto the OCP-clean set.

Normal-form lemmas

@[simp]

theorem OCP.collapse_eq_nil {α : Type u_1} [DecidableEq α] {xs : List α} : collapse xs = [] ↔ xs = []

theorem OCP.collapse_sublist {α : Type u_1} [DecidableEq α] (xs : List α) : (collapse xs).Sublist xs

The output of the fusion repair is a sublist of its input.

theorem OCP.collapse_length_le {α : Type u_1} [DecidableEq α] (xs : List α) : (collapse xs).length ≤ xs.length

theorem OCP.mem_collapse {α : Type u_1} [DecidableEq α] {a : α} {xs : List α} (ha : a ∈ collapse xs) : a ∈ xs

Merging at a seam

Appending with the seam merged drops the head of the second word when it repeats the last element of the first; this is Jardine and Heinz's concatenation on a single tier. On clean words it is the collapse of the concatenation, and the collapse of any concatenation is the merging append of the collapses.

def OCP.mergeAppend {α : Type u_1} [DecidableEq α] (xs ys : List α) : List α

Append ys to xs, dropping the head of ys when it repeats the last element of xs.

Equations

• OCP.mergeAppend xs ys = if xs.getLast? = ys.head? then xs ++ ys.tail else xs ++ ys

def OCP.mergeOffset {α : Type u_1} [DecidableEq α] (xs ys : List α) : ℕ

The position at which ys starts in mergeAppend xs ys.

Equations

• OCP.mergeOffset xs ys = if xs.getLast? = ys.head? then xs.length - 1 else xs.length

def OCP.mergeIdx {α : Type u_1} [DecidableEq α] (xs ys : List α) (p : ℕ) : ℕ

The position in mergeAppend xs ys of position p of xs ++ ys.

Equations

• OCP.mergeIdx xs ys p = if p < xs.length then p else OCP.mergeOffset xs ys + (p - xs.length)

@[simp]

theorem OCP.nil_mergeAppend {α : Type u_1} [DecidableEq α] (ys : List α) : mergeAppend [] ys = ys

@[simp]

theorem OCP.mergeAppend_nil {α : Type u_1} [DecidableEq α] (xs : List α) : mergeAppend xs [] = xs

@[simp]

theorem OCP.mergeOffset_nil_left {α : Type u_1} [DecidableEq α] (ys : List α) : mergeOffset [] ys = 0

theorem OCP.length_mergeAppend {α : Type u_1} [DecidableEq α] (xs ys : List α) : (mergeAppend xs ys).length = mergeOffset xs ys + ys.length

theorem OCP.getLast?_mergeAppend {α : Type u_1} [DecidableEq α] {xs ys : List α} (hys : ys ≠ []) : (mergeAppend xs ys).getLast? = ys.getLast?

theorem OCP.head?_mergeAppend {α : Type u_1} [DecidableEq α] {xs ys : List α} (hxs : xs ≠ []) : (mergeAppend xs ys).head? = xs.head?

theorem OCP.mergeAppend_assoc {α : Type u_1} [DecidableEq α] (xs ys zs : List α) : mergeAppend (mergeAppend xs ys) zs = mergeAppend xs (mergeAppend ys zs)

theorem OCP.mergeOffset_congr_right {α : Type u_1} [DecidableEq α] {xs ys zs : List α} (h : ys.head? = zs.head?) : mergeOffset xs ys = mergeOffset xs zs

theorem OCP.mergeOffset_mergeAppend_right {α : Type u_1} [DecidableEq α] {xs ys zs : List α} (hys : ys ≠ []) : mergeOffset xs (mergeAppend ys zs) = mergeOffset xs ys

theorem OCP.mergeOffset_mergeAppend_left {α : Type u_1} [DecidableEq α] (xs ys zs : List α) : mergeOffset (mergeAppend xs ys) zs = mergeOffset xs (mergeAppend ys zs) + mergeOffset ys zs

theorem OCP.mergeIdx_of_lt {α : Type u_1} [DecidableEq α] {xs ys : List α} {p : ℕ} (h : p < xs.length) : mergeIdx xs ys p = p

@[simp]

theorem OCP.mergeIdx_length_add {α : Type u_1} [DecidableEq α] {xs ys : List α} (a : ℕ) : mergeIdx xs ys (xs.length + a) = mergeOffset xs ys + a

theorem OCP.mergeIdx_monotone {α : Type u_1} [DecidableEq α] {xs ys : List α} : Monotone (mergeIdx xs ys)

theorem OCP.mergeIdx_lt {α : Type u_1} [DecidableEq α] {xs ys : List α} {p : ℕ} (h : p < xs.length + ys.length) : mergeIdx xs ys p < (mergeAppend xs ys).length

theorem OCP.collapse_append_of_isClean {α : Type u_1} [DecidableEq α] {xs ys : List α} (hx : IsClean xs) (hy : IsClean ys) : collapse (xs ++ ys) = mergeAppend xs ys

On clean words, merging at the seam is collapsing the concatenation.

theorem OCP.collapse_append {α : Type u_1} [DecidableEq α] (xs ys : List α) : collapse (xs ++ ys) = mergeAppend (collapse xs) (collapse ys)

The OCP congruence. The collapse of a concatenation is the merging append of the collapses.

theorem OCP.isClean_mergeAppend {α : Type u_1} [DecidableEq α] {xs ys : List α} (hx : IsClean xs) (hy : IsClean ys) : IsClean (mergeAppend xs ys)

Merging at the seam keeps clean words clean.

The run-index map

def OCP.runIdx {α : Type u_3} [DecidableEq α] (xs : List α) (k : ℕ) : ℕ

The run index of position k in xs is the 0-based index of the run of identical elements containing it, one less than the number of runs in xs.take (k + 1).

Equations

• OCP.runIdx xs k = (OCP.collapse (List.take (k + 1) xs)).length - 1

theorem OCP.runIdx_monotone {α : Type u_3} [DecidableEq α] (xs : List α) : Monotone (runIdx xs)

Later positions sit in the same or later runs.

theorem OCP.runIdx_lt_collapse_length {α : Type u_3} [DecidableEq α] (xs : List α) {k : ℕ} (hk : k < xs.length) : runIdx xs k < (collapse xs).length

An in-bounds position has an in-bounds run index in the collapsed tier.

@[simp]

theorem OCP.runIdx_replicate {α : Type u_3} [DecidableEq α] (n : ℕ) (a : α) (k : ℕ) : runIdx (List.replicate n a) k = 0

On a constant tier every position lies in the single run.

theorem OCP.runIdx_clean {α : Type u_3} [DecidableEq α] {xs : List α} (hc : IsClean xs) {k : ℕ} (h : k < xs.length) : runIdx xs k = k

On a clean tier runIdx is the identity.

Run indices of a concatenation

A position of xs ++ ys keeps its run index in xs when it lies in xs; a position in ys moves to its run index in ys, offset by where collapse ys starts in the merging append of the collapses.

theorem OCP.runIdx_append_left {α : Type u_3} [DecidableEq α] {xs ys : List α} {k : ℕ} (h : k < xs.length) : runIdx (xs ++ ys) k = runIdx xs k

The run index of a prefix position is unaffected by a right append.

theorem OCP.runIdx_append_right {α : Type u_3} [DecidableEq α] {xs ys : List α} {a : ℕ} (ha : a < ys.length) : runIdx (xs ++ ys) (xs.length + a) = mergeOffset (collapse xs) (collapse ys) + runIdx ys a

The run index of a suffix position is its run index in the suffix, offset by where the collapsed suffix starts in the merging append of the collapses.