Deletion and insertion of one segment

This file defines the two elementary unfaithful mappings of Correspondence Theory. The deletion of the segment at a position relates a string to the string without it, every other segment corresponding to itself. The insertion of a segment at a position is the converse.

The violation profile of each is a theorem. A deletion violates MAX once and DEP never, and it violates a positional MAX exactly when the deleted position is one the constraint protects. An insertion violates DEP once and MAX never.

Main definitions

• Correspondence.deletion, Correspondence.eraseIdx: the deletion of the segment at a position, with and without changes to the other segments.
• Correspondence.insertIdx: the insertion of a segment at a position.

Main results

• Correspondence.maxViol_deletion, depViol_deletion, maxViolAt_deletion: the profile of a deletion.
• Correspondence.depViol_insertIdx, maxViol_insertIdx, depViolAt_insertIdx: the profile of an insertion.

References

• [McCP95]

def OptimalityTheory.Correspondence.skip (m n i : ℕ) : Finset (Fin m × Fin n)

skip m n i is the order-preserving relation between Fin m and Fin n that skips position i of the first, relating a to b when a is b below i and b + 1 from i on.

Equations

• OptimalityTheory.Correspondence.skip m n i = {p : Fin m × Fin n | ↑p.1 = if ↑p.2 < i then ↑p.2 else ↑p.2 + 1}

@[simp]

theorem OptimalityTheory.Correspondence.mem_skip {m n i : ℕ} {p : Fin m × Fin n} : p ∈ skip m n i ↔ ↑p.1 = if ↑p.2 < i then ↑p.2 else ↑p.2 + 1

theorem OptimalityTheory.Correspondence.mem_image_fst_skip {m n i : ℕ} (hm : m = n + 1) (hi : i < m) {a : Fin m} : a ∈ Finset.image Prod.fst (skip m n i) ↔ ↑a ≠ i

With one position fewer on the right, the positions of the left related to some position of the right are those other than i.

theorem OptimalityTheory.Correspondence.image_snd_skip {m n i : ℕ} (hm : m = n + 1) : Finset.image Prod.snd (skip m n i) = Finset.univ

With one position fewer on the right, every position of the right is related to some position of the left.

def OptimalityTheory.Correspondence.deletion {α : Type u_1} (s t : List α) (i : ℕ) : Correspondence BinaryRole α

deletion s t i relates s to a string t one segment shorter by skipping position i of s, every other position of s corresponding to the position of t in the same order. The segments of t need not be those of s, so a deletion may come with changes elsewhere.

Equations

• One or more equations did not get rendered due to their size.

def OptimalityTheory.Correspondence.eraseIdx {α : Type u_1} (s : List α) (i : ℕ) : Correspondence BinaryRole α

eraseIdx s i is the deletion of the segment at position i of s with every other segment unchanged.

Equations

• OptimalityTheory.Correspondence.eraseIdx s i = OptimalityTheory.Correspondence.deletion s (s.eraseIdx i) i

def OptimalityTheory.Correspondence.insertIdx {α : Type u_1} (s : List α) (i : ℕ) (a : α) : Correspondence BinaryRole α

insertIdx s i a is the insertion of the segment a at position i of s, the converse of the deletion of position i from the longer string.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OptimalityTheory.Correspondence.deletion_form_lhs {α : Type u_1} (s t : List α) (i : ℕ) : (deletion s t i).form BinaryRole.lhs = s

@[simp]

theorem OptimalityTheory.Correspondence.deletion_form_rhs {α : Type u_1} (s t : List α) (i : ℕ) : (deletion s t i).form BinaryRole.rhs = t

@[simp]

theorem OptimalityTheory.Correspondence.eraseIdx_form_lhs {α : Type u_1} (s : List α) (i : ℕ) : (eraseIdx s i).form BinaryRole.lhs = s

@[simp]

theorem OptimalityTheory.Correspondence.eraseIdx_form_rhs {α : Type u_1} (s : List α) (i : ℕ) : (eraseIdx s i).form BinaryRole.rhs = s.eraseIdx i

@[simp]

theorem OptimalityTheory.Correspondence.insertIdx_form_lhs {α : Type u_1} (s : List α) (i : ℕ) (a : α) : (insertIdx s i a).form BinaryRole.lhs = s

@[simp]

theorem OptimalityTheory.Correspondence.insertIdx_form_rhs {α : Type u_1} (s : List α) (i : ℕ) (a : α) : (insertIdx s i a).form BinaryRole.rhs = s.insertIdx i a

The profile of a deletion

theorem OptimalityTheory.Correspondence.maxViolAt_deletion {α : Type u_1} {s t : List α} {i : ℕ} (hlen : s.length = t.length + 1) (hi : i < s.length) (P : ℕ → Prop) [DecidablePred P] : maxViolAt P (deletion s t i) BinaryRole.lhs BinaryRole.rhs = if P i then 1 else 0

A deletion violates a positional MAX exactly when the deleted position is protected.

theorem OptimalityTheory.Correspondence.maxViol_deletion {α : Type u_1} {s t : List α} {i : ℕ} (hlen : s.length = t.length + 1) (hi : i < s.length) : (deletion s t i).maxViol BinaryRole.lhs BinaryRole.rhs = 1

A deletion violates MAX once.

theorem OptimalityTheory.Correspondence.depViol_deletion {α : Type u_1} {s t : List α} {i : ℕ} (hlen : s.length = t.length + 1) : (deletion s t i).depViol BinaryRole.lhs BinaryRole.rhs = 0

A deletion does not violate DEP.

theorem OptimalityTheory.Correspondence.maxViolAt_eraseIdx {α : Type u_1} {s : List α} {i : ℕ} (hi : i < s.length) (P : ℕ → Prop) [DecidablePred P] : maxViolAt P (eraseIdx s i) BinaryRole.lhs BinaryRole.rhs = if P i then 1 else 0

theorem OptimalityTheory.Correspondence.maxViol_eraseIdx {α : Type u_1} {s : List α} {i : ℕ} (hi : i < s.length) : (eraseIdx s i).maxViol BinaryRole.lhs BinaryRole.rhs = 1

theorem OptimalityTheory.Correspondence.depViol_eraseIdx {α : Type u_1} {s : List α} {i : ℕ} (hi : i < s.length) : (eraseIdx s i).depViol BinaryRole.lhs BinaryRole.rhs = 0

The profile of an insertion

theorem OptimalityTheory.Correspondence.depViolAt_insertIdx {α : Type u_1} {s : List α} {i : ℕ} (a : α) (hi : i ≤ s.length) (P : ℕ → Prop) [DecidablePred P] : depViolAt P (insertIdx s i a) BinaryRole.lhs BinaryRole.rhs = if P i then 1 else 0

An insertion violates a positional DEP exactly when the inserted position is one the constraint covers.

theorem OptimalityTheory.Correspondence.depViol_insertIdx {α : Type u_1} {s : List α} {i : ℕ} (a : α) (hi : i ≤ s.length) : (insertIdx s i a).depViol BinaryRole.lhs BinaryRole.rhs = 1

An insertion violates DEP once.

theorem OptimalityTheory.Correspondence.maxViol_insertIdx {α : Type u_1} {s : List α} {i : ℕ} (a : α) (hi : i ≤ s.length) : (insertIdx s i a).maxViol BinaryRole.lhs BinaryRole.rhs = 0

An insertion does not violate MAX.