Docs / Phonology / OptimalityTheory / Correspondence / Deletion

Deletion and insertion

import Linglib.Phonology.OptimalityTheory.Correspondence.Deletion · namespace OptimalityTheory.Correspondence

A deletion relates each position of the shorter string to the position of the longer one it comes from, and an insertion is the converse. Deleting the segment at position i goes along Fin.succAbove i, so it violates MAX once, at i; deleting the positions D violates MAX once at each of them. When no other segment changes, neither deletion nor insertion violates IDENT.

Main definitions

Correspondence.deletion: the deletion along a map of positions, the other segments free to change.
Correspondence.eraseIdx, Correspondence.eraseIdxs: the deletion of the segment at a position, and of the segments at a set of positions, the other segments unchanged.
Correspondence.insertIdx: the insertion of a segment, the converse of a deletion.

Main results

Correspondence.maxViolAt_deletion: a deletion violates a positional MAX at the protected positions off the range of its map; maxViolAt_deletion_succAbove is the case of one position.
Correspondence.maxViolAt_eraseIdxs: deleting the positions D violates a positional MAX once for each protected position in D.
Correspondence.depViolAt_insertIdx: an insertion violates a positional DEP exactly when the constraint covers the inserted position.
Correspondence.identViol_eraseIdx, identViol_eraseIdxs, identViol_insertIdx: none of them changes another segment.

References

McCarthy & Prince 1995, Faithfulness and Reduplicative Identity formalized

Deletion along a map of positions

deletion s t f relates s to the string t along f: each position j of t corresponds to position f j of s alone, and the positions of s off the range of f are deleted. The segments of t need not be those of s, so a deletion may come with changes elsewhere.

def deletion L45–49

{α : Type u_1} (s t : List α) (f : Fin t.length → Fin s.length) :

Correspondence BinaryRole α

deletion s t f = (ofFun t s f).swap

Used by deletion_form_lhs, deletion_form_rhs, mem_deletion_edge, deletion_isSymmetric, maxViolAt_deletion, depViol_deletion, identViol_deletion_eq_zero_iff, maxViolAt_deletion_succAbove, eraseIdx, insertIdx

Used in Stojkovic2026

A deletion violates a positional MAX at the protected positions off the range of its map.

theorem maxViolAt_deletion L66–71

{α : Type u_1} {s t : List α} {f : Fin t.length → Fin s.length} (P : ℕ → Prop) [DecidablePred P] :

maxViolAt P (deletion s t f) BinaryRole.lhs BinaryRole.rhs = ({i : Fin s.length | P ↑i} \ Finset.image f Finset.univ).card

Built from

L73–75

L77–81

A deletion along Fin.succAbove p violates a positional MAX exactly when the constraint protects position p.

theorem maxViolAt_deletion_succAbove L83–95

{α : Type u_1} {s t : List α} (p : Fin (t.length + 1)) (h : t.length + 1 = s.length) (P : ℕ → Prop) [DecidablePred P] :

maxViolAt P (deletion s t fun (j : Fin t.length) => Fin.cast h (p.succAbove j)) BinaryRole.lhs BinaryRole.rhs = if P ↑p then 1 else 0

Built from

One segment

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

def eraseIdx L101–106

{α : Type u_1} (s : List α) (i : Fin s.length) :

Correspondence BinaryRole α

eraseIdx s i = deletion s (s.eraseIdx ↑i) fun (j : Fin (s.eraseIdx ↑i).length) => Fin.cast ⋯ ((Fin.cast ⋯ i).succAbove j)

Built from

Used by eraseIdx_form_lhs, eraseIdx_form_rhs, maxViolAt_eraseIdx, maxViol_eraseIdx, depViol_eraseIdx, identViol_eraseIdx

Used in Phonology/OptimalityTheory/PositionalFaithfulness, Casali1997, Storme2026

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.

def insertIdx L108–112

{α : Type u_1} (s : List α) (i : Fin (s.length + 1)) (a : α) :

Correspondence BinaryRole α

insertIdx s i a = (deletion (s.insertIdx (↑i) a) s fun (j : Fin s.length) => Fin.cast ⋯ (i.succAbove j)).swap

Built from

Used by insertIdx_form_lhs, insertIdx_form_rhs, depViolAt_insertIdx, depViol_insertIdx, maxViol_insertIdx, identViol_insertIdx

Used in Storme2026

A deletion of one segment changes no other.

theorem identViol_eraseIdx L131–137

{α : Type u_1} {s : List α} {i : Fin s.length} [DecidableEq α] :

(eraseIdx s i).identViol BinaryRole.lhs BinaryRole.rhs = 0

Built from

L145

L147

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

theorem depViolAt_insertIdx L149–154

{α : Type u_1} {s : List α} {i : Fin (s.length + 1)} {a : α} (P : ℕ → Prop) [DecidablePred P] :

depViolAt P (insertIdx s i a) BinaryRole.lhs BinaryRole.rhs = if P ↑i then 1 else 0

Built from

L156–157

L159–161

An insertion of one segment changes no other.

theorem identViol_insertIdx L163–171

{α : Type u_1} {s : List α} {i : Fin (s.length + 1)} {a : α} [DecidableEq α] :

(insertIdx s i a).identViol BinaryRole.lhs BinaryRole.rhs = 0

Built from

Deletion of a set of positions

eraseIdxs s D is the deletion of the segments at the positions D of s with every other segment unchanged, each surviving segment corresponding to itself. Positions past the end of s delete nothing.

def eraseIdxs L177–184